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

Question

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

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

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

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

非常感谢

score 4 · Accepted Answer

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

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

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

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

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

您可以在Isabelle/Isar 参考手册中找到更多详细信息，该手册也包含在 Isabelle2014 安装中。

score 3 · Accepted Answer

如果您对下载一两个文件感到满意，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的是，它不会告诉您应用定理的顺序。但是，它能够与每种方法（simp、clarsimp、fastforce、auto等）一起使用，而simp_trace仅适用于基于简化器的方法。

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

2 回答 2