正确使用 prefer_tac

Question

我目前无法弄清楚如何正确使用 prefer_tac。 (伊莎贝尔2019 Linux)

我正在执行以下操作（最小工作示例）：

theory MWE
imports
  Main
begin

lemma "False ∧ True ∧ A"
  apply (intro conjI)
    apply (tactic ‹prefer_tac 2›) (* Exception *)
    apply (tactic ‹SELECT_GOAL all_tac 2 THEN prefer_tac 2›) (* Works *)
  oops

end

第一次 prefer_tac 调用时出现异常（第一次调用时的状态）：

proof (prove)
goal (3 subgoals):
 1. False
 2. True
 3. A 
exception Subscript raised (line 75 of "./basis/List.sml")

虽然我希望它能正常工作。为什么不呢？如果这有一些微不足道的原因，我很抱歉。我真的不是伊莎贝尔内部专家。

第二次调用有效。第二次调用状态：

proof (prove)
goal (3 subgoals):
 1. True
 2. False
 3. A

我在问自己为什么这行得通。哪个看不见的效果 SELECT_GOAL 调用是否使 prefer_tac 起作用？我认为 SELECT_GOAL 选择第二个目标只是为了调用 all_tac?

函数 permute_prems (thm.ML) List.take 有一个异常处理程序，但是 List.drop 没有。这对我来说很奇怪。这应该与我的问题没有任何关系，因为那样我只会得到更好的错误消息。

Answer 1

我没有详细调查问题。然而，在 apply (tactic ‹...›) 的第一次调用时，该策略是在虚拟模式上调用的（请参阅 this post on the mailing list for details）。接收到虚拟模式后，Thm.permute_prems 会抛出 prefer_tac 未处理的异常。通常（但不总是），策略在失败时被期望 return 一个空的结果序列（参见 Isabelle/Isar 实施手册中的第 4.2 节）。在第一次调用 SELECT_GOAL all_tac 2... 时，all_tac 收到的虚拟模式不会导致异常，它只会将有效目标传递给 prefer_tac.

我很难说在 prefer_tac 中是否有理由承认未处理的异常。但是，您可以轻松修改策略 prefer_tac 的原始规范，以确保它不会抛出异常，并且 return 在失败的情况下返回空结果序列：

ML‹
fun prefer_tac' i thm = thm
  |> PRIMITIVE (Thm.permute_prems (i - 1) 1 #> Thm.permute_prems 0 ~1)
  handle Subscript => Seq.empty;
  (* of course, you can add other exceptions if necessary *)
›

lemma "False ∧ True ∧ A"
  apply (intro conjI)
  apply (tactic ‹prefer_tac' 2›) (* Works *)
  oops

备注：

As a side note (I should probably write this to the mailing list) in the function permute_prems (thm.ML) List.take has an exception handler, but List.drop doesn't. This looks odd to me. This shouldn't have anything to do with my problem, because then I would just get a nicer error message.

确实，这看起来有点奇怪，可能值得在邮件列表中提及。不过，我对Isabelle的实现细节也知之甚少。

伊莎贝尔版本：Isabelle2020

正确使用 prefer_tac

Using prefer_tac correctly

isabelle