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

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

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

在上面的代码中， simp 方法证明了引理。我有兴趣查看并打印出简化方法为证明此引理而采取的详细(重写/简化)步骤(并且可能能够对所有其他证明方法执行相同的操作)。这怎么可能？

我正在使用 isabelle 2014 和 JEdit 编辑器。

非常感谢

最佳答案

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

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

如果光标位于 simp 步骤之后，则输出 Pane 将显示内嵌的重写跟踪(列出添加了哪些规则、应用了哪些内容以及重写了哪些术语)。
simp_trace_new 允许在单独的窗口中查看更紧凑的跟踪变体(重写的内容)(通过按下消息的突出显示部分激活跟踪 Pane 在输出 Pane 中查看 简化程序跟踪 ，跟踪本身通过按下显示一个按钮显示跟踪)。添加选项 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 安装中。

关于isabelle - 在 isabelle 的证明中打印/显示证明方法(如 simp)的详细步骤，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/26825747/