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

[David Greenaway]

On 10/03/13 07:03, Makarius wrote:
> 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”.
>
> 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.

As a data point, inside the seL4 proof, a largish application of
Isabelle, such a "solve-or-fail" mechanism would have been very helpful.

First of all, we found that examples such as that given by Joachim come
up quite frequently.

Additionally, such syntax would be very helpful in proof maintenance,
where you ideally want the proof script to break at the source of an
error, instead of 12 lines further down. Liberal use of "apply (foo)!"
in the more complex proof scripts would help maintainers find the source
of an error more quickly.

Cheers,
David

--


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.