isabelle - 如何查看Isabelle的分步推理 'proofs'

Question

我最近开始学习Isabelle，但我找不到一个非常重要的问题的答案:一个人如何看到Isabelle发现的“证明”的逐步推理？我对“自动”或“通过爆炸使用Theorem_A”这样的行不满意，我想检查逐步推演。
当然，我了解了Isar的“证明”，但是1. Sledgehammer不能总是找到这样的Isar证明，并且2.甚至Isar证明也不能总是给出循序渐进的推理。例如，由Sledgehammer生成的我的一个定理的Isar证明如下所示:

     proof -
  have "... here is my formula ...."
    using My_Theorem_1 My_axiom_2 by blast
  thus ?thesis
    by metis
qed

当然，不能像伊莎贝尔(Isabelle)和伊萨尔(Isar)的发烧友那样称呼这种证明为“人类可读的证明”。
现在我的问题是:是否可以从伊莎贝尔(Isabelle)发现的“证明”中逐步得出推论？或者至少有可能将“自动”之类的“证明”转换为Isar证明？例如，需要逐步推演的情况。存在定理的证明，它们通常提供有用的显式构造。
我浏览了一些教程，但找不到答案...

Answer 1

首先，我将解释为什么您的问题通常不像您认为的那么重要。然后我会回答您的实际问题。

Isabelle的设计使您完全不必“信任”其证明方法(例如simp，auto和metis)。所有证明都必须经过Isabelle的推理内核，因为该内核是Isabelle中唯一可以产生定理的部分:如果您信任(相对较小的)内核，则可以信任所有证明方法。证明方法直接或间接调用内核导出的函数来操纵定理。

内核包含反射(reflect)Isabelle/Pure公理的功能，我认为这是自然推论。然后，您将获得对象逻辑(在大多数情况下为HOL)，定义和typedef的公理。所有Isabelle定理都有证明，这些证明基本上是由这些推理步骤组成的证明树。

因此，您要查找的“逐步”证明就是这棵树，它被称为证明对象或证明术语。这些东西的问题在于它们非常大且非常不可读(请参阅Russell和Whitehead撰写的The Principia Mathematica，以了解它们的大小和不可读性)。我认为您可以告诉Isabelle以某种方式生成这些证明条款，但是我不知道如何生成。我确实找到了一组slides by Stefan Berghofer。

我不明白为什么您会说您所举的例子难以理解。读者可以隐藏一些细节，是的，但是几乎所有普通的数学证明也是如此。 blast和metis不能正常工作； blast是一阶表格证明者，metis是分辨率证明者。如果blast和metis可以在一个步骤中证明某事，则数学家可能也不会在该步骤上做更多详细说明。

至于具有存在性的显式构造:Isabelle/HOL不是一种构造逻辑。从经典证明中提取程序是正在进行的研究，并且非常困难。如果您想在Isabelle/HOL中进行某些事物的显式构造，我的建议不是证明存在性，而是直接证明您的显式构造。如果您可以通过auto一步证明您的存在，那么我相信构造非常简单。