在 isabelle 的证明中打印/显示证明方法的详细步骤（如 simp）

Posted 2023-03-28

【中文标题】在 isabelle 的证明中打印/显示证明方法的详细步骤（如 simp）

【英文标题】：Printing out / showing detailed steps of proof methods (like simp) in a proof in isabelle

【发布时间】：2014-11-09 06:42:53

【问题描述】：

假设我在 Isabelle 中有以下代码：

lemma"[| xs@zs = ys@xs ;[]@xs = []@[] |] => ys=zs" (*never mind the lemma body*)
apply simp
done

在上面的代码中，simp 方法证明了引理。我有兴趣查看并打印出简化方法用来证明这个引理的详细（重写/简化）步骤（并且可能能够对所有其他证明方法做同样的事情）。这怎么可能？

我正在使用带有 JEdit 编辑器的 isabelle 2014。

非常感谢

【参考方案1】：

可以通过指定属性simp_trace 或simp_trace_new 来启用简化跟踪：

lemma "⟦xs @ zs = ys @ xs; [] @ xs = [] @ [] ⟧ ⟹ ys = zs"
  using [[simp_trace]]
  apply simp
done

如果光标位于simp 步骤之后，则输出窗格会显示内联的重写跟踪（并列出添加了哪些规则、应用了什么以及重写了哪些术语）。

simp_trace_new 允许在单独的窗口中查看更紧凑的跟踪变体（重写的内容）（通过按下消息的突出显示部分激活跟踪窗格请参阅简化跟踪 在输出窗格中，通过按下按钮 Show trace 会显示跟踪本身）。添加选项mode=full 会生成类似于simp_trace 的更详细的输出，但以更结构化的方式：

lemma "⟦xs @ zs = ys @ xs; [] @ xs = [] @ [] ⟧ ⟹ ys = zs"
  using [[simp_trace_new mode=full]]
  apply simp
done

您可以在 The Isabelle/Isar Reference Manual 中找到更多详细信息，它也包含在 Isabelle2014 安装中。

【参考方案2】：

如果您愿意下载一两个文件，l4.verified 项目包含一个名为 Apply Trace 的工具，由 Daniel Matichuk 编写。它为您提供了一个新命令 apply_trace，可以在您通常使用 apply 的任何地方使用，但会显示该步骤中使用的定理。

例如写作：

lemma "⟦xs @ zs = ys @ xs; [] @ xs = [] @ [] ⟧ ⟹ ys = zs"
  apply_trace simp

产生：

used theorems:
  simp_thms(6): (?x = ?x) = True
  append_Nil: [] @ ?ys = ?ys
  append_Nil2: ?xs @ [] = ?xs

与simp_trace 不同，它不会告诉您应用定理的顺序。但是，它能够处理every 方法（simp、clarsimp、@987654332 @、auto 等），而 simp_trace 仅适用于基于简化器的方法。

要使用它，您需要同时获取文件Apply_Trace_Cmd.thy 和Apply_Trace.thy 并导入Apply_Trace_Cmd。

【讨论】：

酷！我希望这样的事情能在伊莎贝尔身上找到。