有没有一种很好的方法来打印简化器(例如,
apply clarsimp
)在进入无限循环时正在做什么?
using [[simp_trace]]
记录简化器正在做什么(非常难以阅读,但您只是在寻找在循环中应用哪些定理”。
lemma "Q (f b) ⟹ b = f a ⟹ a = b ⟹ Q a"
using [[simp_trace, simp_trace_depth_limit = 5]]
apply simp
done
快速浏览一下日志后,您可以看到日志始终循环应用
b = f a
和 b = a
。
即使 simp 不发散,它也能工作。
simp_trace_depth_limit 将 simp_trace 的效果限制在给定深度 递归简化器调用(当解决重写条件时 规则)。
--- https://www.isabelle.in.tum.de/website-Isabelle2024/dist/Isabelle2024/doc/isar-ref.pdf