1\DOC prove_induction_thm
2
3\TYPE {prove_induction_thm : (thm -> thm)}
4
5\SYNOPSIS
6Derives structural induction for an automatically-defined concrete type.
7
8\DESCRIBE
9{prove_induction_thm} takes as its argument a primitive recursion theorem, in
10the form returned by {define_type} for an automatically-defined concrete type.
11When applied to such a theorem, {prove_induction_thm} automatically proves and
12returns a theorem that states a structural induction principle for the concrete
13type described by the argument theorem. The theorem returned by
14{prove_induction_thm} is in a form suitable for use with the general structural
15induction tactic {INDUCT_THEN}.
16
17\FAILURE
18Fails if the argument is not a theorem of the form returned by {define_type}.
19
20\EXAMPLE
21Given the following primitive recursion theorem for labelled binary trees:
22{
23   |- !f0 f1.
24        ?! fn.
25        (!x. fn(LEAF x) = f0 x) /\
26        (!b1 b2. fn(NODE b1 b2) = f1(fn b1)(fn b2)b1 b2)
27}
28{prove_induction_thm} proves and returns the theorem:
29{
30   |- !P. (!x. P(LEAF x)) /\ (!b1 b2. P b1 /\ P b2 ==> P(NODE b1 b2)) ==>
31          (!b. P b)
32}
33This theorem states the principle of structural induction on labelled
34binary trees: if a predicate {P} is true of all leaf nodes, and if whenever it
35is true of two subtrees {b1} and {b2} it is also true of the tree {NODE b1 b2},
36then {P} is true of all labelled binary trees.
37
38\SEEALSO
39Prim_rec.INDUCT_THEN, Prim_rec.new_recursive_definition,
40Prim_rec.prove_cases_thm, Prim_rec.prove_constructors_distinct,
41Prim_rec.prove_constructors_one_one, Prim_rec.prove_rec_fn_exists.
42
43\ENDDOC
44