[isabelle-dev] Feature suggestion: apply (meth[1!])
makarius at sketis.net
Sat Mar 9 21:03:23 CET 2013
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.
More information about the isabelle-dev