110420Salanb\DOC prove_induction_thm
212585Salanb
310420Salanb\TYPE {prove_induction_thm : (thm -> thm)}
410420Salanb
510420Salanb\SYNOPSIS
610420SalanbDerives structural induction for an automatically-defined concrete type.
710420Salanb
810420Salanb\DESCRIBE
910420Salanb{prove_induction_thm} takes as its argument a primitive recursion theorem, in
1010420Salanbthe form returned by {define_type} for an automatically-defined concrete type.
1110420SalanbWhen applied to such a theorem, {prove_induction_thm} automatically proves and
1210420Salanbreturns a theorem that states a structural induction principle for the concrete
1310420Salanbtype described by the argument theorem. The theorem returned by
1410420Salanb{prove_induction_thm} is in a form suitable for use with the general structural
1510420Salanbinduction tactic {INDUCT_THEN}.
1610420Salanb
1710420Salanb\FAILURE
1810420SalanbFails if the argument is not a theorem of the form returned by {define_type}.
1910420Salanb
2010420Salanb\EXAMPLE
2110420SalanbGiven the following primitive recursion theorem for labelled binary trees:
2210420Salanb{
2310420Salanb   |- !f0 f1.
2410420Salanb        ?! fn.
2510420Salanb        (!x. fn(LEAF x) = f0 x) /\
2610420Salanb        (!b1 b2. fn(NODE b1 b2) = f1(fn b1)(fn b2)b1 b2)
2710420Salanb}
2810420Salanb{prove_induction_thm} proves and returns the theorem:
2912585Salanb{
3010420Salanb   |- !P. (!x. P(LEAF x)) /\ (!b1 b2. P b1 /\ P b2 ==> P(NODE b1 b2)) ==>
3110420Salanb          (!b. P b)
3210420Salanb}
3310420SalanbThis 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