Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Problem with Isar/Isabelle Induct method

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

From: Peter Chapman <pc@cs.st-and.ac.uk>
Hi

I have written an inductive proof in Isabelle, and was trying to
rewrite it in Isar/Isabelle style to be human readable. Following
the document "Structured Induction Proofs in Isabelle/Isar", I wrote

lemma isar_many_step_from_list:
fixes Gam :: "form set"
and X :: "var list"
and d :: "deriv"
and A :: "form"
assumes As1: "is_wf d & root d = (Gam, A)"
and As2: "set X < {y. y \<sharp> Gam}"
shows "? d'. is_wf d' & root d' = (Gam, quantify X A)"
proof (induct X fixing: "Gam")

but got the error

*** Error in method "HOL.induct":
*** method "HOL.induct": bad arguments
*** : "Gam"
*** At command "proof".

The same thing happened regardless of what I put after the colon. If
I omit this part, then the induction proceeds as usual, but I cannot
refer each case, so in the first case for X=[ ], I cannot write

case "[ ]"
...

and so on. Could anyone point out what I'm doing wrong? If it is
relevant, I'm working in HOL-Nominal.

Many thanks

Peter Chapman

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

From: Makarius <makarius@sketis.net>
On Fri, 29 Jun 2007, Peter Chapman wrote:

I have written an inductive proof in Isabelle, and was trying to rewrite
it in Isar/Isabelle style to be human readable. Following the document
"Structured Induction Proofs in Isabelle/Isar", I wrote

lemma isar_many_step_from_list:
...
proof (induct X fixing: "Gam")

but got the error

*** Error in method "HOL.induct":
*** method "HOL.induct": bad arguments
*** : "Gam"
*** At command "proof".

Unfortunately, the present syntax of the "induct" method (of Isabelle2007
development snapshots) is no longer that of the mentioned paper. The
"fixing" part is now introcuded by "arbitrary". See also the NEWS and the
isar-ref manual on the "induct" method.

but I cannot refer each case, so in the first case for X=[ ], I cannot
write case "[ ]"

Note that the 'print_cases' command (or corresponding Proof General
menu/key) will show the cases available in the present proof context.
(Some of these may stem from earlier method invocations, and be no longer
valid.)

Makarius

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

From: rpollack@inf.ed.ac.uk
Hi Peter,

The keyword has changed. Instead of "fixing" try "arbitrary". It also
appears
that if the keyword "rule" is used, "arbitrary" must occur before "rule".
Randy

Last updated: May 03 2024 at 04:19 UTC