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