在Isabelle中证明A ==> B ==> C ==> B.

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

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样张,只需进行一些网络搜索,或查看系统附带的来源.这里有一个完全随意的例子:饮酒者.

还有很多手册,实际上太多了.