[isabelle-dev] NEWS: Roll your own induction schemes with the "induct_scheme" method
krauss at in.tum.de
Fri Dec 7 11:11:01 CET 2007
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):
"[| 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.
More information about the isabelle-dev