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

[Makarius]

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