4

我对证明感到困惑

A ==> B ==> C ==> B

在伊莎贝尔。显然你可以

apply simp

但是我如何使用规则来证明这一点？

或者，有没有办法转储simp使用的规则？谢谢。

4

2 回答 2

6

如果你真的想了解证明是如何工作的，你应该忘记有趣的策略和自动推理工具作为开始。

Isabelle/Pure的陈述A ==> B ==> C ==> B（使用这个特殊==>的连接词）立即为真，因此它在 Isabelle/Isar 中的证明是：

lemma "A ==> B ==> C ==> B" .

就是这样，只是.（缩写为by this，但this这里实际上是空的）。

由于稍微不那么空洞的证明使用实际的 Isabelle/HOL 连接词，然后您可以通过标准的引入或消除步骤来处理。比如像这样：

lemma "A --> B --> C --> B"
proof
  show "B --> C --> B"
  proof
    assume b: B
    show "C --> B"
    proof
      show B by (rule b)
    qed
  qed
qed

但这也不是那么有趣：你建立了一个无聊的暗示，然后将其分解，直到你完成。

要找到更有趣的 Isabelle/Isar 证明，只需进行一些网络搜索，或查看系统附带的资源。这里有一个完全任意的例子：Drinker。

还有大量的手册，实际上太多了。

于 2014-03-14T20:34:24.760 回答
4

您可以启用简化器跟踪；在 Proof General 中，您可以使用 Isabelle → Settings → Tracing → Trace Simplifier 执行此操作，我不了解 jEdit。

编辑：在这种情况下，simp 跟踪不会很有帮助，因为simp它不使用重写规则来解决这个问题，而是在前提中“看到”A、B 和 C，并得出结论认为它可以，在此语句的上下文中, rewrite A = True, B = True, and C = True，然后将目标重写B为True，您就完成了。

但是，证明此类陈述的“正常”方法是使用将assumption目标与前提相匹配的方法，在这种情况下B。可能也有一种方法可以证明这一点rule，但这会不必要地复杂。assumptionuses assume_tac，而这又只是一个非常基本的function的包装Thm.assumption，所以这真的可以被认为是 Isabelle 中最基本的证明方法之一。所以就写吧by assumption。

于 2013-11-28T18:05:35.850 回答