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
34
35
36
37
|
\DOC prove_cases_thm
\TYPE {prove_cases_thm : (thm -> thm)}
\SYNOPSIS
Proves a structural cases theorem for an automatically-defined concrete type.
\DESCRIBE
{prove_cases_thm} takes as its argument a structural induction theorem, in the
form returned by {prove_induction_thm} for an automatically-defined concrete
type. When applied to such a theorem, {prove_cases_thm} automatically proves
and returns a theorem which states that every value the concrete type in
question is denoted by the value returned by some constructor of the type.
\FAILURE
Fails if the argument is not a theorem of the form returned by
{prove_induction_thm}
\EXAMPLE
Given the following structural induction theorem for labelled binary trees:
{
|- !P. (!x. P(LEAF x)) /\ (!b1 b2. P b1 /\ P b2 ==> P(NODE b1 b2)) ==>
(!b. P b)
}
\noindent {prove_cases_thm} proves and returns the theorem:
{
|- !b. (?x. b = LEAF x) \/ (?b1 b2. b = NODE b1 b2)
}
\noindent This states that every labelled binary tree {b} is either a leaf node
with a label {x} or a tree with two subtrees {b1} and {b2}.
\SEEALSO
define_type, INDUCT_THEN, new_recursive_definition,
prove_constructors_distinct, prove_constructors_one_one, prove_induction_thm,
prove_rec_fn_exists.
\ENDDOC
|
