如何查看Isabelle中value命令底层执行？是否有类似simp_trace的工具？

Isabelle的value命令确实支持类似simp_trace的追踪方式，具体可以通过code_trace选项实现：

• 启用追踪的示例代码：

  value using [[code_trace]] "2+4::nat"
  

  执行这条命令后，输出窗口会打印出value执行过程中的详细步骤，包括从高阶逻辑表达式转换为可执行代码的过程、具体的求值路径（比如自然数加法的递归展开或底层实现调用）。

• 额外说明：

  • code_trace是专门针对value命令设计的追踪选项，对应simp_trace在化简过程中的作用，能直观展示value的底层执行逻辑。
  • 若需要进一步查看代码生成的细节，还可以结合code_printing相关配置，但code_trace是最直接满足需求的方式。

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