如何使用solve_direct 建议的规则？（按（规则……）并不总是有效）

Question

有时<statement> solve_direct（我通常通过调用<statement> try）列出一些库定理并说“当前的目标可以直接解决：……”。

设<theorem>一个搜索结果solve_direct，然后在大多数情况下我可以证明<statement> by (rule theorem)。

然而，有时这样的证明不被接受，导致错误信息“应用初始证明方法失败”。

是否有一种通用的、不同的技术来重用由 找到的定理solve_direct？

还是要看个人情况？我可以尝试找出一个最小的例子并将其附加到这个问题上。

Answer 1

就个人而言，我只是倾向于使用：

apply (metis thm)

这在大多数情况下都有效，而不会迫使我非常努力地思考（但如果需要棘手的解决方案，它仍然偶尔会失败）。

其他通常也有效的方法包括：

apply (rule thm)                 (* If "thm" has no premises. *)
apply (erule thm)                (* If "thm" has a single premise. *)
apply (erule thm, assumption+)   (* If "thm" has multiple premises. *)

为什么没有一个答案？答案有点复杂：

在内部，solve_direct调用find_theorems solves，然后执行以下操作：

fun etacn thm i = Seq.take (! tac_limit) o etac thm i;
(* ... *)
if Thm.no_prems thm then rtac thm 1 goal
else (etacn thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt)) 1 goal;

这是类似于rule thm如果规则没有前提的东西的 ML 代码，或者：

apply (erule thm, assumption+)

如果规则中有多个前提。正如 Brian 对您的问题所评论的那样，如果假设中存在复杂的元逻辑连接词，则上述内容可能仍会失败（norm_hhf_tac处理的内容，但据我所知并未直接公开为 Isabelle 方法）。

如果你愿意，你可以编写一个新的方法来暴露find_theorems直接使用的策略，如下所示：

ML {*
  fun solve_direct_tac thm ctxt goal =
  if Thm.no_prems thm then rtac thm 1 goal
  else (etac thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt)) 1 goal;
*}

method_setup solve =
  {* Attrib.thm >> (fn thm => fn ctxt =>
        SIMPLE_METHOD' (K (solve_direct_tac thm ctxt ))) *}
  "directly solve a rule"

这可以按如下方式使用：

lemma "? a; b ? ? a ? b"
  by (solve conjI)

这应该有望解决任何问题solve_direct。