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



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





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