prove_constructors_distinct : thm -> thm
Proves that the constructors of an automatically-defined concrete type yield
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
- FAILURE CONDITIONS
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.
The following type definition for labelled binary trees:
returns a recursion theorem rth that can then be fed to
# 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))
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.
# prove_constructors_distinct rth;;
val it : thm = |- !a a0' a1'. ~(LEAF a = NODE a0' a1')
An easier interface is distinctness "tree"; this function is mainly intended
to generate that theorem internally.
- SEE ALSO
define_type, distinctness, INDUCT_THEN, new_recursive_definition,
prove_cases_thm, prove_constructors_one_one, prove_induction_thm,