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