如何解决Isabelle定义非递归两参数nat max时的termination _dom错误

已有的定义与报错 #

函数定义代码：

fun two_integer_max_case :: "nat ⇒ nat ⇒ nat" where
"two_integer_max_case a b = (case a > b of True ⇒ a | False ⇒ b)"

termination by auto

编译时的完整报错信息：

proof (prove)
goal (1 subgoal):
 1. All two_integer_max_case_dom 
Ignoring duplicate rewrite rule:
two_integer_max_case ?a1 ?b1 ≡ case ?b1 < ?a1 of True ⇒ ?a1 | False ⇒ ?b1 
Duplicate fact declaration "Max_Of_Two_Integers.two_integer_max_case.simps" vs. "Max_Of_Two_Integers.two_integer_max_case.simps"⌂ 
Failed to finish proof⌂:
goal (1 subgoal):
 1. ⋀a b. two_integer_max_case_dom (a, b)

核心待证目标：

1. ⋀a b. two_integer_max_case_dom (a, b)

核心概念解释 #

• *xxx_dom*条件的含义：
  该谓词是Isabelle的fun命令为所有通过该命令定义的函数自动生成的合法域标记谓词，作用是约束函数定义成立的输入范围。对于递归函数，这个谓词的归纳结构和函数的递归调用路径严格绑定；对于非递归函数，该谓词的定义默认是无约束的恒真形式。
• 报错的实际要求：
  待证目标⋀a b. two_integer_max_case_dom (a, b)的本质是证明：所有类型为nat * nat的输入对，都满足该函数的合法域约束。
  出现未完成证明的原因是：auto策略无法自动展开无递归函数的域谓词定义，因此没法自动推导出“全输入都在合法域内”的结论。
• 报错附带提示的说明：
  报错中附带的“Ignoring duplicate rewrite rule”、“Duplicate fact declaration”是无害的冗余提示，是fun命令对同一组等式规则的重复声明检测，不影响证明逻辑正确性。

参考资料查阅位置 #

• Isabelle2021官方《Tutorial》3.5章节，关于fun命令的基础使用规则
• Isabelle官方《Functions》参考文档8.1章节，关于域谓词的生成逻辑、证明规则和相关API

适配非递归代码生成需求的解决方案 #

• 该问题不需要引入任何递归定义即可解决，完全不影响最终生成非递归的目标语言代码。
• 补证方法：手动展开域谓词的定义完成证明，替换原有的auto证明步骤即可：

  termination by (auto simp: two_integer_max_case_dom_def)
  

• 代码生成效果：上述定义生成的Haskell/Scala代码会直接映射为非递归的分支判断结构，完全保留定义中的比较、分支逻辑，不会插入任何递归调用。
• 相关事实说明：
  • Isabelle基础标准库中已内置自然数类型的max函数，其定义本身就是完全非递归的分支判断形式，生成的代码不存在递归逻辑。
  • Isabelle的代码生成机制会严格忠实于函数定义的结构：只要定义中不包含递归调用，生成的目标语言代码就不会强行转换为递归形式，不存在为了证明便利性牺牲代码可读性的默认行为。

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