derive_strong_induction : thm * thm -> thm

SYNOPSIS

Derive stronger induction theorem from inductive definition.

DESCRIPTION

The function derive_strong_induction is applied to a pair of theorems as returned by new_inductive_definition. The first theorem is the `rule' theorem, the second the `induction' theorem; the `case' theorem returned by new_inductive_definition is not needed. It returns a stronger induction theorem where instances of each inductive predicate occurring in hypotheses is conjoined with the corresponding inductive relation too.

FAILURE CONDITIONS

Fails if the two input theorems are not of the correct form for rule and induction theorems returned by new_inductive_definition.

EXAMPLE

A simple example of a mutually inductive definition is:

  # let eo_RULES,eo_INDUCT, eo_CASES = new_inductive_definition
     `even(0) /\ odd(1) /\
      (!n. even(n) ==> odd(n + 1)) /\
      (!n. odd(n) ==> even(n + 1))`;;
  val eo_RULES : thm =
    |- even 0 /\
       odd 1 /\
       (!n. even n ==> odd (n + 1)) /\
       (!n. odd n ==> even (n + 1))
  val eo_INDUCT : thm =
    |- !odd' even'.
           even' 0 /\
           odd' 1 /\
           (!n. even' n ==> odd' (n + 1)) /\
           (!n. odd' n ==> even' (n + 1))
           ==> (!a0. odd a0 ==> odd' a0) /\ (!a1. even a1 ==> even' a1)
  val eo_CASES : thm =
    |- (!a0. odd a0 <=> a0 = 1 \/ (?n. a0 = n + 1 /\ even n)) /\
       (!a1. even a1 <=> a1 = 0 \/ (?n. a1 = n + 1 /\ odd n))

The stronger induction theorem can be derived as follows. Note that it is similar in form to eo_INDUCT but has stronger hypotheses for two of the conjuncts in the antecedent.

  # derive_strong_induction(eo_RULES,eo_INDUCT);;
  val it : thm =
    |- !odd' even'.
           even' 0 /\
           odd' 1 /\
           (!n. even n /\ even' n ==> odd' (n + 1)) /\
           (!n. odd n /\ odd' n ==> even' (n + 1))
           ==> (!a0. odd a0 ==> odd' a0) /\ (!a1. even a1 ==> even' a1)

COMMENTS

This function needs to discharge monotonicity theorems as part of its internal working, just as new_inductive_definition does when the inductive definition is made. Usually this is automatic and the user doesn't see it, but in difficult cases, the theorem returned may have additional monotonicity hypotheses that are unproven. In such cases, you can either try to prove them manually or extend monotonicity_theorems to make the built-in monotonicity prover more powerful.