Apply a method if and only if it solves the current goal

Question

Sometimes, when I’m writing apply-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, revert to the original state and 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 (solve_goal(subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail))+

or (alternative suggested synatx)

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

or (maybe even nicer syntax)

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.

Answer 1

Isabelle has no such combinator, which is something I miss, too. Often, I can avoid the need for such a combinator if I replace auto or simp calls by fastforce or force (which have the solve-or-fail behaviour).

So, if the simp in your example is supposed to solve the goal (without looping),

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

might be a more robust variant.

Answer 2

Since the advent of the Eisbach proof script language, this is now supported. After importing "~~/src/HOL/Eisbach/Eisbach", one can replace

apply foo

with

apply (solves ‹foo›)

and the line will fail if solves produces any new goals. This can be combined with [1] as in

apply (solves ‹(auto)[1]›)

if desired.

The definition of solves is actually quite simple:

method solves methods m = (m; fail)