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