Isabelle：函数没有代码方程

Question

这是我的理论，在代码生成之前获得 OK 状态：

theory Max_Of_Two_Integers
  imports (* Main *)
    "../Imperative_HOL" 
    Subarray
    "HOL-Library.Multiset"
    "HOL-Library.Code_Target_Numeral"
    "HOL-Library.Code_Target_Nat"  
begin

function two_integer_max :: "nat ⇒ nat ⇒ nat Heap"
  where
 "two_integer_max first second =
     (if (first > second)  then
        return first
      else
        return second) "
  by pat_completeness auto

code_reserved SML upto

definition "example = do {
   a ← two_integer_max 1 2;
   return a
  }"

export_code example checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala Scala_impL

(*    
value "example"
 *)

end

代码生成创建关于错误的输出：

No code equations for two_integer_max

我正在密切关注 https://isabelle.in.tum.de/library/HOL/HOL-Imperative_HOL/Imperative_Quicksort.html 并且我使用相同的导入和相同的语法，但仍然 - 这个错误。我猜 - 代码生成器在 two_integer_max 的未指定生成方面存在问题，但 Imperative_Quicksort 管理器生成涉及相似结构的更复杂代码。

当然，我正在阅读 https://isabelle.in.tum.de/doc/codegen.pdf 中有关代码方程的第 2 章，但如果能够在基本管道正常工作时快速继续并构建剩余的管道并研究复杂的理论，那就太好了。

也许有跟踪工具可以检查代码生成的中间步骤？

当我添加

termination by auto

然后该行失败

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

也许缺少终止证明禁止代码生成？我还在研究如何完成这个终止证明..

Answer 1

您可以添加终止证明：

termination by size_change

方法size_change 是一种简单的启发式终止证明。对于更复杂的情况，您通常可以改用 relation 方法。

或者您可以使用 fun 而不是 function。在那种情况下，您既不需要明确定义证明 (by pat_completeness auto) 也不需要手动终止证明。

Isabelle：函数没有代码方程

Isabelle: No code equations for the function

isabelle