Isabelle/HOL中如何配置simp仅使用set_rec引理进行化简

要实现仅用引理set_rec进行化简、清空默认所有定理的需求，你不需要用del_all这类虚构语法——Isabelle的simp早已提供了直接的解决方案：使用only:参数。

正确写法 #

by (simp only: set_rec)

细节解释 #

• 当你使用only:时，化简器会完全清空默认的重写规则集合，只把你指定的set_rec作为唯一可用的重写规则来使用。
• 对比其他参数的作用，能更清晰理解差异：
  • del:：从默认的化简规则集合中删除指定条目（比如你提到的by (simp del: less_imp_le_nat)）
  • add:：在默认集合的基础上额外添加指定规则
  • only:：彻底替换默认集合，只保留你列出的规则

这样写就完全符合你“仅用set_rec化简”的需求啦。

内容的提问来源于stack exchange，提问作者P. Ez