Search code examples
isabelleisar

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

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

Solution

  • 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.