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

[Joachim Breitner]

Dear Isabelle developers,

I’d like to suggest a feature, and submit a patch:

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”.

This came up in the following code:

qed (subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail)+

After some change further up, the call to simp would not fully solve a
goal any more, and then this would loop. If I could have specified
something like

qed ((subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail)[1!])+

It would have stopped at the first goal that was not solvable by this
script.

(Originally posted at http://stackoverflow.com/questions/15290300)

It would also be useful to annotate large apply-script style proof, to
record where goals are closed. This way, after later changes, it is
easier to fix the proofs.


I’d like to propose a syntax that extends the existing [n] modifier by
an exclamation mark, with the intended meaning that I know or expect the
method to solve these goals, and that I want it to fail if it does not.


As the n in [n] is already optional with a default to 1, this implies
that appending [!] to a method will either solve the first goal or 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? If accepted I
will follow up with a documentation patch to §6.3.1 of the reference
manual.

Greetings,
Joachim

-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner
-------------- next part --------------
A non-text attachment was scrubbed...
Name: solve_or_fail_method.patch
Type: text/x-patch
Size: 3726 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130308/8185f1ed/attachment.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130308/8185f1ed/attachment.asc>