1\DOC prove_constructors_distinct
2
3\TYPE {prove_constructors_distinct : (thm -> thm)}
4
5\SYNOPSIS
6Proves that the constructors of an automatically-defined concrete type yield
7distinct values.
8
9\DESCRIBE
10{prove_constructors_distinct} takes as its argument a primitive recursion
11theorem, in the form returned by {define_type} for an automatically-defined
12concrete type.  When applied to such a theorem, {prove_constructors_distinct}
13automatically proves and returns a theorem which states that distinct
14constructors of the concrete type in question yield distinct values of this
15type.
16
17\FAILURE
18Fails if the argument is not a theorem of the form returned by {define_type},
19or if the concrete type in question has only one constructor.
20
21\EXAMPLE
22Given the following primitive recursion theorem for labelled binary trees:
23{
24   |- !f0 f1.
25        ?! fn.
26        (!x. fn(LEAF x) = f0 x) /\
27        (!b1 b2. fn(NODE b1 b2) = f1(fn b1)(fn b2)b1 b2)
28}
29{prove_constructors_distinct} proves and returns the theorem:
30{
31   |- !x b1 b2. ~(LEAF x = NODE b1 b2)
32}
33This states that leaf nodes are different from internal nodes.  When
34the concrete type in question has more than two constructors, the resulting
35theorem is just conjunction of inequalities of this kind.
36
37\SEEALSO
38Prim_rec.INDUCT_THEN, Prim_rec.new_recursive_definition,
39Prim_rec.prove_cases_thm, Prim_rec.prove_constructors_one_one,
40Prim_rec.prove_induction_thm, Prim_rec.prove_rec_fn_exists.
41
42\ENDDOC
43