Printing out / showing detailed steps of proof methods (like simp) in a proof in isabelle

Question

Suppose I have the following code in Isabelle:

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

In the above code, The simp method proves the lemma. I am interested to see and print out the detailed (rewriting /simplification) steps that the simplification method takes to prove this lemma ( and possibly be able to do the same for all the other proof methods). How this is possible?

I am using isabelle 2014 with JEdit editor.

Many Thanks

Answer 1

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

\n\n

lemma "\xe2\x9f\xa6xs @ zs = ys @ xs; [] @ xs = [] @ [] \xe2\x9f\xa7 \xe2\x9f\xb9 ys = zs"\n  using [[simp_trace]]\n  apply simp\ndone\n

\n\n

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

\n\n

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

\n\n

lemma "\xe2\x9f\xa6xs @ zs = ys @ xs; [] @ xs = [] @ [] \xe2\x9f\xa7 \xe2\x9f\xb9 ys = zs"\n  using [[simp_trace_new mode=full]]\n  apply simp\ndone\n

\n\n

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

\n