Stream: Archive Mirror: Isabelle Users Mailing List

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

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

From: Christian Urban <urbanc@in.tum.de>
Hi Peter,

Peter Chapman writes:

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 generalisation over X needs to be done with the
command "arbitrary" instead of "fixing" (this change of
syntax was decided after the paper of Markus came
out). So the proof-line should be

proof (induct X fixing: Gam)

Best wishes,
Christian

Last updated: May 03 2024 at 12:27 UTC