How can I find which lemmas are used by the simp, auto methods, etc?
In one concrete case, I have a goal like:
lemma "x ∉ dom S ⟹ Something"
apply auto
and after applying auto I get: ¬ Something ⟹ ∃y. S x = Some y. I would like to find out why the whole goal is reversed like this, so that I can delete the respective rules from the rewriting.
I already tried using [[simp_trace_new mode=full]] apply auto and using [[simp_trace]] apply auto, but did not find information about what exactly caused auto to do this transformation.
I know this is necroposting. But for everyone stumbling over this question now, I want to point out that apply_trace is what OP was searching for. For more info see davidgs answer in this thread: Printing out / showing detailed steps of proof methods (like simp) in a proof in isabelle.