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

Question

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

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

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

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

非常感谢

Answer 1

可以通过指定属性 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 安装中。