5

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

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

但是，有时这样的证明不被接受，导致错误消息“无法应用初始证明方法”。

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

还是取决于个人情况？我可以尝试制定一个最小的示例并将其附加到这个问题上。

4

3 回答 3

5

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

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直接暴露 by 使用的策略，如下所示：

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你遇到的任何问题。

于 2013-08-30T00:12:48.450 回答
1

我找到了另一种使用solve_direct's 建议的方式by rule。当Hilbert_Choice.someI2建议图书馆中的某些非常基本的规则（例如 以下至少在两种具体情况下对我有用（来源）：

  1. 重新检查“类似规则”的事实、其他事实（如果有的话）和目标
  2. 如有必要，重新排列其他事实
  3. 做证明using <other_facts> ... by (rule <rule-like-fact>)
于 2013-09-11T11:45:27.990 回答
0

你可以试试fact或rule_tac。如果我没记错的话，rule有时在存在其他事实的情况下无法应用给定规则，我不完全确定原因；这个问题必须由比我更熟悉这些方法的实现细节的人来回答。

于 2013-08-29T13:38:41.593 回答