`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)
```