Dear developers,
I've just added an experimental method to prove user-specified induction
rules (by deriving them from wellfounded induction). This factors out
some operations that are done internally by the function package and
makes them available separately.
To prove your induction principle, you need to show that the cases are
complete (automated for datatypes by "pat_completeness") and that the
principle is well-founded (automated e.g. by "lexicographic_order").
This is usually much simpler than deriving the scheme manually from some
other induction rule:
Small example (cf. Nat.thy):
lemma nat_induct2:
"[| P 0;
P (Suc 0);
!!k. P k ==> P (Suc (Suc k)) |]
==> P n"
by induct_scheme (pat_completeness, lexicographic_order)
See "HOL/ex/Induction_Scheme.thy" for some more examples, including
mutual induction rules.
Alex
