[isabelle-dev] Feature suggestion: apply (meth[1!])

[Lars Noschinski]

There is definitely an use case for such an operation. When doing program verification, I often have long sequences of apply commands. These are either applications of the VCG or (mostly) oneliners to solve the verification conditions. To keep the proof as robust as possible, I use the classical method of indentation (=number of goals) and try to use only fastforce. But there are cases where I need to use auto[] or simp and in this cases it would be neat if I easily could indicate that a step has to solve a subgoal. 



Makarius <makarius at sketis.net> schrieb:

>On Fri, 8 Mar 2013, Joachim Breitner wrote:
>
>> Sometimes, when I’m writing apply-script style proofs, I have wanted a 
>> way to modify a proof method foo to “Try foo on the first goal. If it 
>> solves the goal, good, if it does not solve it, fail”.
>
>Such non-trivial control structures are usually done via tactics and 
>tacticals.  There is a whole zoo of tacticals, and no point to hardwire 
>them in the Isar method combinator syntax.
>
>The "implementation" manual in Isabelle2013 contains an up-to-date chapter 
>4 on tactical reasoning, which was derived from the classic Isabelle 
>manuals from many years ago.
>
>There is also some explanation what it means formally to be a "tactic" and 
>a proof "method".  The method_setup command can then be used to provide 
>concrete Isar syntax to suitable methods in the usual manner.
>
>
>The Isar proof method language was designed a certain way, to arrive at 
>"stilized" specifications of some operational aspects in the proof text. 
>It has excluded any kind of programming or sophisticated control 
>structures on purpose.  In 1998 it was not clear yet if that would work 
>out, since the big applications of that time (e.g. HOL-Bali) were done 
>differently.  In retrospect the Isar method language was more succesful in 
>this respect than I had anticipated.  We see big applications today 
>without lots of specialized goal-state manipulation.
>
>In general the problem of what is a good proof interaction language is a 
>very delicate one.  To make serious progress, one would have to revisit 
>what you see as Ltac and SSReflect in Coq today, and revisit it on the 
>background of profound understanding how Isar works.  Then maybe also 
>combine it with IDE-style templating and outlines produced by the prover.
>
>
> 	Makarius
>_______________________________________________
>isabelle-dev mailing list
>isabelle-dev at in.tum.de
>https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev