[isabelle-dev] NEWS: Roll your own induction schemes with the "induct_scheme" method

[Alexander Krauss]

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