Is there a nice way to print what the simplifier (apply clarsimp, for example) is doing when it goes into an infinite loop?
using [[simp_trace]]
logs what the simplifier is doing (pretty unreadable, but you’re just looking for which theorems are applied in a loop”. using [[simp_trace_new]] gives a slightly cleaner log, but its slow.
Example
lemma "Q (f b) ⟹ b = f a ⟹ a = b ⟹ Q a"
using [[simp_trace, simp_trace_depth_limit = 5]]
apply simp
done
After a quick glance at the log, you can see that the log always applies b = f a and b = a in a loop.
It also works even if simp doesn’t diverge.
simp_trace_depth_limit limits the effect of simp_trace to the given depth
of recursive Simplifier invocations (when solving conditions of rewrite
rules).— https://www.isabelle.in.tum.de/website-Isabelle2024/dist/Isabelle2024/doc/isar-ref.pdf