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

[Makarius]

On Thu, 14 Mar 2013, David Greenaway wrote:

> On 08/03/13 23:46, 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”.
> [...]
>> I wanted to see if I could implement such a feature myself and came up
>> with the attached patch – maybe it is already sufficient?
>
> Sorry to raise this thread again, but what was the outcome of this
> patch?
>
> Was the general concept of a "solve" tactical rejected, or just the 
> particular choice of syntax / implementation? (If so, how could it be 
> improved?) Or have the core developers just been busy? (I apologise if 
> so!)

Isar method syntax does not have "tacticals" at all.  The few method 
combinators are fixed, and not meant to be extended by adhoc patching. 
It is also conceptually hard to do that, because of the way how a method 
differs from a tactic in its notion of proof state and goal addressing.

So the proposed patch did not make it beyond thise first static 
type-check.


Just last week, I was myself reconsidering the old question if there could 
be a "parallel" method combinator, to speedup things like "blast+" or 
"force+", but failed to fit it adequately into the existing structures. 
So its simply not going to happen now.  Applying force works for some 
proofs, but not for systems doing proofs that are meant to be around a bit 
longer.

Of course, I don't want to discourage experimentation, and discussing 
ideas with an open mind.  Getting things accepted into the main code base 
is a few more orders of magnitude more difficult, though.  Even ideas that 
are commonly understood and generally found beneficial usually sit in the 
pipeline for several years before they hit the repository. (Compared to 
Sun/Oracle/Apple and Java the Isabelle development process is incredibly 
fast; even just compared to Coq.)


 	Makarius