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

The simplifier trace can be enabled by specifying attributes simp_trace or simp_trace_new:

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

If the cursor is positioned after the simp step, the output pane shows the rewrite trace inline (with the list what rules are added, what are applied and what terms are rewritten).

simp_trace_new allows seeing a more compact variant of the trace (what is rewritten) in a separate window (the trace pane is activated by pressing a highlighted part of a message See simplifier trace in the output pane, the trace itself is shown by pressing a button Show trace). Adding an option mode=full generates a more detailed output similar to simp_trace, but in a more structured way:

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

You can find more details in The Isabelle/Isar Reference Manual that is also included in Isabelle2014 installation.