4

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.

Peter Zeller
  • 2,245
  • 19
  • 23
  • `auto` and `clarify` do some classical reasoning on your lemma and there doesn't seem to be an easy way to trace that. Also `x ∉ dom S ⟹ Something` and `¬ Something ⟹ ∃y. S x = Some y` are logically equivalent. Why can't you work on the second form of the lemma? – ammbauer Mar 01 '17 at 19:47
  • I had some other simplification rules with `x ∉ dom S` as a premise, so when it got moved to the right these other simplification rules could no longer be used. I changed everything to `S x = None` now, but my question is more how to see the used lemmas in general. Thanks for the hint with the classical reasoning, I did not think of that. – Peter Zeller Mar 01 '17 at 22:55
  • There doesn't seem to be an easy way. You could ask on the mailing list for a reason why. – ammbauer Mar 03 '17 at 21:13

1 Answers1

2

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.

MercedesJones
  • 164
  • 6
  • Thanks for the answer. There is no "necroposting" on Stackoverflow (see https://meta.stackexchange.com/a/125967/644502 ). Another option available since Isabelle 2020 is the `thm_deps` command, which prints the direct dependencies of a theorem. – Peter Zeller Aug 31 '20 at 18:04