# 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.*