1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
|
\DOC injectivity
\TYPE {injectivity : string -> thm}
\SYNOPSIS
Produce injectivity theorem for an inductive type.
\DESCRIBE
A call {injectivity "ty"} where {"ty"} is the name of a recursive type defined
with {define_type}, returns a ``injectivity'' theorem asserting that elements
constructed by different type constructors are always different. The effect is
exactly the same is if {prove_constructors_injective} were applied to the
recursion theorem produced by {define_type}, and the documentation for
{prove_constructors_injective} gives a lengthier discussion.
\FAILURE
Fails if {ty} is not the name of a recursive type, or if all its constructors
are nullary.
\EXAMPLE
{
# injectivity "num";;
val it : thm = |- !n n'. SUC n = SUC n' <=> n = n'
# injectivity "list";;
val it : thm =
|- !a0 a1 a0' a1'. CONS a0 a1 = CONS a0' a1' <=> a0 = a0' /\ a1 = a1'
}
\SEEALSO
cases, define_type, distinctness, prove_constructors_injective.
\ENDDOC
|
