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