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
|
\DOC prove_constructors_distinct
\TYPE {prove_constructors_distinct : thm -> thm}
\SYNOPSIS
Proves that the constructors of an automatically-defined concrete type yield
distinct values.
\DESCRIBE
{prove_constructors_distinct} 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_distinct}
automatically proves and returns a theorem which states that distinct
constructors of the concrete type in question yield distinct values of this
type.
\FAILURE
Fails if the argument is not a theorem of the form returned by {define_type},
or if the concrete type in question has only one constructor.
\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_distinct}:
{
# prove_constructors_distinct rth;;
val it : thm = |- !a a0' a1'. ~(LEAF a = NODE a0' a1')
}
This states that leaf nodes are different from internal nodes. When the
concrete type in question has more than two constructors, the resulting theorem
is just conjunction of inequalities of this kind.
\COMMENTS
An easier interface is {distinctness "tree"}; this function is mainly intended
to generate that theorem internally.
\SEEALSO
define_type, distinctness, INDUCT_THEN, new_recursive_definition,
prove_cases_thm, prove_constructors_one_one, prove_induction_thm,
prove_rec_fn_exists.
\ENDDOC
|
