我最近开始学习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证明？需要逐步演绎的情况是例如存在性定理的证明，它们通常提供有用的显式构造。我浏览了一些教程，但找不到答案...
isabelle ×1