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

Question

Sometimes when Im writing proofs like application type, I need a way to change the proof method foo to

Try foo for the first goal. If he decides the goal, good; if this happens do not solve it, return to their original state and fail.

This appeared in the following code:

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

After simp some further changes, calling simp will no longer completely solve the target, and then it will be a loop. If I could specify something like

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

or (alternative suggested syntax)

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

or (perhaps even nicer syntax)

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

he would stop at the first target that was not resolved by this script.

Answer 1

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

 apply foo 

with

 apply (solves ‹foo›) 

and the line will fail if solves creates new targets. 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 doesn't have such a combinator, which I miss too. Often, I can avoid the need for such a combinator if I replace auto or simp with fastforce or force (which have a resolution or error behavior).

So, if simp in your example should solve the goal (without a loop),

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

may be a more reliable option.

Answer 3

While there is no built-in tactic or combinator, you can implement it 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 solved method, which will be successful if the current goal is completely resolved or will fail if one or more subgoals remain.

It can be used, for example, as follows:

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

Without the solved Isabelle will choose the rule disjI1 side of the apply step, leaving you with an unsolvable target. With a solved on each side, Isabelle tries to use rule disjI1 and, when he cannot solve the goal, switches to simp , which is then successfully executed.

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

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

Answer 4

Isabelle's exquisite language does not provide this feature; this is intentional and not an error, as described in the isabelle developer list :

The language of the Isar proof method was developed in a specific way to “stylized” the specifications of certain operational aspects in the proof text. He ruled out any programming or complex control of structures as intended.