如何调试Isabelle中的无限simp循环及查看化简器循环执行内容？

以下是几种实用的调试手段，帮你定位化简器（如clarsimp）陷入无限循环的原因：

• 启用化简器跟踪输出
  在执行化简命令前，先设置跟踪选项：

  set trace_simp = true
  set trace_simp_depth = 20  -- 限制输出深度，避免刷屏
  

  之后执行apply clarsimp，控制台会打印每一步应用的化简规则、匹配的子项和化简后的结果。观察输出中重复出现的规则序列，通常就是触发循环的根源。

• 使用simp_debug交互式调试
  用simp_debug替代普通的simp或clarsimp：

  apply (simp_debug)
  

  这个命令会逐步执行化简步骤，每一步都会暂停并等待你输入指令（如c继续、s单步、q退出），能精准定位到循环开始的具体步骤和对应的规则。

• 限制或筛选化简规则

  • 尝试只加载必要的规则，逐步排查：

    apply (clarsimp only: your_rule1 your_rule2)
    

    若不再循环，说明问题出在未加载的规则中，逐步添加规则找到触发循环的那个。
  • 反之，删除可疑规则测试：

    apply (clarsimp del: suspicious_rule)
    

    若循环消失，即可确定该规则是问题所在。

• 设置循环终止阈值
  修改化简器的循环限制，让它提前终止并保留当前状态：

  set simp_loop_limit = 500  -- 默认值通常更高，改小后会触发提前终止
  apply clarsimp
  print_state  -- 查看终止时的目标状态，分析未完成的化简项
  

• 拆分化简步骤
  不要直接使用clarsimp（它是simp+clarify的组合），拆分执行：

  apply simp
  apply clarify
  

  或者用subgoal命令拆分目标，逐个处理子目标，缩小循环可能出现的范围。

内容的提问来源于stack exchange，提问作者Mathieu Paturel