distinctness : string -> thm
Produce distinctness theorem for an inductive type.
A call distinctness "ty" where "ty" is the name of a recursive type defined
with define_type, returns a ``distinctness'' theorem asserting that elements
constructed by different type constructors are always different. The effect is
exactly the same is if prove_constructors_distinct were applied to the
recursion theorem produced by define_type, and the documentation for
prove_constructors_distinct gives a lengthier discussion.
- FAILURE CONDITIONS
Fails if ty is not the name of a recursive type, or if the type has only one
# distinctness "num";;
val it : thm = |- !n'. ~(0 = SUC n')
# distinctness "list";;
val it : thm = |- !a0' a1'. ~( = CONS a0' a1')
- SEE ALSO
cases, define_type, injectivity, prove_constructors_distinct.