[isabelle-dev] Feature suggestion: apply (meth[1!])
makarius at sketis.net
Thu Mar 14 12:34:04 CET 2013
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
> 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
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
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
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.)
More information about the isabelle-dev