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:
   |- !f0 f1.
        ?! fn.
        (!x. fn(LEAF x) = f0 x) /\
        (!b1 b2. fn(NODE b1 b2) = f1(fn b1)(fn b2)b1 b2)
prove_induction_thm proves and returns the theorem:
   |- !P. (!x. P(LEAF x)) /\ (!b1 b2. P b1 /\ P b2 ==> P(NODE b1 b2)) ==>
          (!b. P b)
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.
SEEALSO
HOL  Kananaskis-14