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

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)

Answer 2

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 3

While there is no built-in tactic or combinator available, you can implement one yourself as follows:

ML {*
fun solved_tac thm =
  if nprems_of thm = 0 then Seq.single thm else Seq.empty
*}

method_setup solved = {*
  Scan.succeed (K (SIMPLE_METHOD solved_tac))
*}

This creates a new method solved that will succeed if the current goal has been completely solved, or fail if there is one or more subgoals still remaining.

It can be used, for example, as follows:

lemma "a ∨ ¬ a "
  apply ((rule disjI1, solved) | (simp, solved))
  done

Without the solved clause, Isabelle will select the rule disjI1 side of the apply step, leaving you with an unsolvable goal. With the solved clause in each side, Isabelle attempts to use rule disjI1 and, when it fails to solve the goal, switches to the simp which is then successful.

This can be used to solve individual goals by using Isabelle's (...)[1] syntax. For example, the following statement will attempt to solve as many subgoals as possible using simp, but will leave a subgoal unchanged if simp fails to completely solve it:

apply ((simp, solved)[1])+

Answer 4

The Isar language of Isabelle does not provide that feature; this is intentional and not a bug, as explained on the isabelle developer list:

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.