isabelle - 在 Isabelle 中证明 A ==> B ==> C ==> B

Question

我对证明感到困惑

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

在伊莎贝尔。显然你可以

apply simp

但是我怎么能用规则来证明这一点呢？

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

Answer 1

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

声明A ==> B ==> C ==> B (使用这个特殊的 ==> 连接词) Isabelle/Pure 立即为真，所以它在 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 .

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