[isabelle] Problem with Isar/Isabelle Induct method



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






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