Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Simultaneous rule induction

Email Gateway (Aug 18 2022 at 10:46):

From: Randy Pollack <rpollack@inf.ed.ac.uk>
Hi,

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

Makarius' paper "Structured Induction proofs ..." implies this is well
supported, but I don't see any examples there.

Thanks,
Randy

Email Gateway (Aug 18 2022 at 10:47):

From: Makarius <makarius@sketis.net>
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

Last updated: Nov 21 2024 at 12:39 UTC