(Temporarily) disabling backtracking in Eisbach method

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)?)

1 answer

  • answered 2018-03-14 09:16 lsf37

    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 =>
         fun tac st' = method_evaluate m ctxt facts st'
       in SIMPLE_METHOD (DETERM tac) facts end)


    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