prove_constructors_one_one : (thm -> thm)
STRUCTURE
Prim_rec
SYNOPSIS
Proves that the constructors of an automatically-defined concrete type are injective.
DESCRIPTION
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
Given the following primitive recursion theorem for labelled binary trees: 
   |- !f0 f1.
        ?! fn.
        (!x. fn(LEAF x) = f0 x) /\
        (!b1 b2. fn(NODE b1 b2) = f1(fn b1)(fn b2)b1 b2)
prove_constructors_one_one proves and returns the theorem: 
   |- (!x x'. (LEAF x = LEAF x') = (x = x')) /\
      (!b1 b2 b1' b2'.
        (NODE b1 b2 = NODE b1' b2') = (b1 = b1') /\ (b2 = b2'))
This states that the constructors LEAF and NODE are both injective.
SEEALSO
INDUCT_THEN, new_recursive_definition, prove_cases_thm, prove_constructors_distinct, prove_induction_thm, prove_rec_fn_exists
HOL  Kananaskis-13