solver - 如何使用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+)

如果规则中有多个前提。正如布莱恩对您的问题所评论的那样，如果假设中存在复杂的元逻辑连接词( norm_hhf_tac 处理，但据我所知没有直接公开为伊莎贝尔方法)，上述内容可能仍然失败。

如果您愿意，您可以编写一个新方法来公开 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向你扔。