isabelle - (暂时)禁用 Eisbach 方法中的回溯

Question

我有一个生成大量可能状态的方法，当使用 , 链接它时与(有条件的)fail或 tactic no_tac ，由此产生的组合方法需要很长时间才能终止并导致 Isabelle 界面滞后。但是，当使用两个 apply 分别应用相同的方法时s，终止非常快。有没有办法强制 Eisbach 方法在失败时不回溯，而是立即失败？ (本质上，功能是 apply <method> apply cond_fail 而不是 apply (<method>, cond_fail) ？)

Answer 1

我不认为有一种方法可以直接在 vanilla Eisbach 中执行此操作，但定义新的组合器(即高阶方法)相对容易。

我们在 https://github.com/seL4/l4v/blob/796887/lib/Eisbach_Methods.thy 中有一些这样的.具体针对您的情况，determ方法看起来像你想要的。它提升了 ML DETERM组合器进入艾斯巴赫:

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 )

这些组合器已被添加到 Isabelle 发行版中，应该会出现在即将发布的 Isabelle2018 版本中。

DETERM切断所有回溯，只传递第一个选择。有了那个

apply (determ <f>, g)

应该等同于

apply f
apply g