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

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".
Quoting Peter Chapman <pc at>:


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

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