Re: [isabelle] Simultaneous rule induction



On Sun, 26 Aug 2007, Randy Pollack wrote:

> Please point me to some examples of simultaneous rule induction using 
> the "induct" method.

In the library there are surprisingly few non-trivial examples of mutual 
induction stemming from inductive definitions, not datatypes.  Some more 
interesting applications are in afp-devel/POPLmark-deBruijn by Stefan 
Berghofer, see http://afp.sourceforge.net/download.shtml

Induction with multiple rules stemming from sets/predicates A and B works 
essentially like this:

  lemma
    "A m ==> P m"
    "B n ==> Q n"
  proof (induct rule: A_B.inducts)

Here the inductive entity to be eliminated needs to be included in an 
explicit implication.  The more common ``using'' form does not work here, 
because the fact involved is different for each goal.

Note that when giving additional method arguments, each bunch of 
parameters needs to be separated by 'and', e.g. like this:

  lemma
    "A x m ==> P x m"
    "B y z n ==> Q y z n"
  proof (induct arbitrary: x and y z rule: A_B.inducts)

(This sectioning of arguments follows the collection of rules, not goals.)


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.