(Temporarily) disabling backtracking in Eisbach method

Question

I have a method that generates a large number of possible states, and when chaining it using , with a (conditional) fail or tactic no_tac, the resulting combined method takes a very long time to terminate and causes the Isabelle interface to lag. However, when the same methods are applied separately using two applys, termination is very quick. Is there a way to force the Eisbach method to not backtrack on failure, and instead just fail right away? (In essence, functioning as apply <method> apply cond_fail rather than apply (<method>, cond_fail)?)

Answer 1

I don't think there's a way to do this directly in vanilla Eisbach, but it is relatively easy to define new combinators (i.e. higher-order methods).

We have a few of these in https://github.com/seL4/l4v/blob/796887/lib/Eisbach_Methods.thy. For your case specifically, the determ method looks like what you want. It lifts the ML DETERM combinator into Eisbach:

method_setup determ =
 \<open>Method.text_closure >> (fn m => fn ctxt => fn facts =>
   let
     fun tac st' = method_evaluate m ctxt facts st'
   in SIMPLE_METHOD (DETERM tac) facts end)
\<close>

(https://github.com/seL4/l4v/blob/796887/lib/Eisbach_Methods.thy#L59)

Those combinators have since been added to the Isabelle distribution and should appear in the upcoming Isabelle2018 release.

DETERM cuts off all backtracking, and passes on only the first alternative. With that

apply (determ <f>, g)

should be equivalent to

apply f
apply g