[isabelle-dev] Feature suggestion: apply (meth[1!])
noschinl at in.tum.de
Sun Mar 10 04:31:41 CET 2013
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.
>isabelle-dev mailing list
>isabelle-dev at in.tum.de
More information about the isabelle-dev