如何解决 Isabelle termination _dom 错误信息（避免双参数最大值的递归定义）？

Question

我正在尝试在 Isabelle 中定义我自己的简单 max 函数并证明它的终止：

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)

我特别关注消息：

Failed to finish proof⌂:
goal (1 subgoal):
1. ⋀a b. two_integer_max_case_dom (a, b)

这是什么意思？对我有什么要求？这个..._dom条件。我在哪里可以读到它？

我已阅读 https://isabelle.in.tum.de/dist/Isabelle2021/doc/tutorial.pdf and now I am reading Chapter 8.1 of https://isabelle.in.tum.de/dist/Isabelle2021/doc/functions.pdf 的第 3.5 章有关域谓词的内容。好吧，我希望我设法找到解决方案。

我知道如果我设法提出我的 max 函数（两个自然类型参数）的递归定义，事情会很容易（至少在终止证明中）。但是我还没有设法找到这样的定义（我想在基础理论中已经有一些创造性的定义）而且我不确定我是否会对递归定义感到满意，因为我的目的是生成 Haskell 或我的函数中的 Scala 代码，我希望这段代码不是递归的，而是使用各自语言的标准 less、equality 运算符。

好吧 - Isabelle 的代码合成通常是我的问题 - 如果 Isabelle 更喜欢工业编程风格（无论是什么）的算法结构的递归定义不需要递归，则生成的代码可维护性和人类理解能力较差（在AI进入程序合成领域之前仍然是一个问题）。

Answer 1

使用 fun 时无需证明终止，因为此 Isabelle-command 仅接受可以自动证明终止的函数定义。因此，您的 termination-command 根本没有必要，并且实际上会使系统感到困惑，因为它已经被证明已终止。

只有在使用function而不是fun的情况下，之后才需要手动证明termination。

希望这对你有所帮助，René

如何解决 Isabelle termination _dom 错误信息（避免双参数最大值的递归定义）？

How to resolve Isabelle termination _dom error message (avoiding recursive definition of two-argument max)?

isabelle