prove_induction_thm : (thm -> thm)

- STRUCTURE
- SYNOPSIS
- Derives structural induction for an automatically-defined concrete type.
- DESCRIPTION
- prove_induction_thm takes as its argument a primitive recursion theorem, in the form returned by define_type for an automatically-defined concrete type. When applied to such a theorem, prove_induction_thm automatically proves and returns a theorem that states a structural induction principle for the concrete type described by the argument theorem. The theorem returned by prove_induction_thm is in a form suitable for use with the general structural induction tactic INDUCT_THEN.
- FAILURE
- Fails if the argument is not a theorem of the form returned by define_type.
- EXAMPLE
- Given the following primitive recursion theorem for labelled binary trees:prove_induction_thm proves and returns the theorem:
|- !f0 f1. ?! fn. (!x. fn(LEAF x) = f0 x) /\ (!b1 b2. fn(NODE b1 b2) = f1(fn b1)(fn b2)b1 b2)

This theorem states the principle of structural induction on labelled binary trees: if a predicate P is true of all leaf nodes, and if whenever it is true of two subtrees b1 and b2 it is also true of the tree NODE b1 b2, then P is true of all labelled binary trees.|- !P. (!x. P(LEAF x)) /\ (!b1 b2. P b1 /\ P b2 ==> P(NODE b1 b2)) ==> (!b. P b)

- SEEALSO

HOL Kananaskis-14