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









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