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 <makar...@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-...@in.tum.de >https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev