1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
|
\DOC prove_constructors_injective
\TYPE {prove_constructors_injective : thm -> thm}
\SYNOPSIS
Proves that the constructors of an automatically-defined concrete type are
injective.
\DESCRIBE
{prove_constructors_one_one} takes as its argument a primitive recursion
theorem, in the form returned by {define_type} for an automatically-defined
concrete type. When applied to such a theorem, {prove_constructors_one_one}
automatically proves and returns a theorem which states that the constructors
of the concrete type in question are injective (one-to-one). The resulting
theorem covers only those constructors that take arguments (i.e. that are not
just constant values).
\FAILURE
Fails if the argument is not a theorem of the form returned by {define_type},
or if all the constructors of the concrete type in question are simply
constants of that type.
\EXAMPLE
The following type definition for labelled binary trees:
{
# let ith,rth = define_type "tree = LEAF num | NODE tree tree";;
val ith : thm =
|- !P. (!a. P (LEAF a)) /\ (!a0 a1. P a0 /\ P a1 ==> P (NODE a0 a1))
==> (!x. P x)
val rth : thm =
|- !f0 f1.
?fn. (!a. fn (LEAF a) = f0 a) /\
(!a0 a1. fn (NODE a0 a1) = f1 a0 a1 (fn a0) (fn a1))
}
\noindent returns a recursion theorem {rth} that can then be fed to
{prove_constructors_injective}:
{
# prove_constructors_injective rth;;
val it : thm =
|- (!a a'. LEAF a = LEAF a' <=> a = a') /\
(!a0 a1 a0' a1'. NODE a0 a1 = NODE a0' a1' <=> a0 = a0' /\ a1 = a1')
}
\noindent This states that the constructors {LEAF} and {NODE} are both
injective.
\COMMENTS
An easier interface is {injectivity "tree"}; the present function is mainly
intended to generate that theorem internally.
\SEEALSO
define_type, INDUCT_THEN, injectivity, new_recursive_definition,
prove_cases_thm, prove_constructors_distinct, prove_induction_thm,
prove_rec_fn_exists.
\ENDDOC
|
