Isabelle：没有函数

如何解决Isabelle：没有函数

这是我的理论，让代码生成正常状态：

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)

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

解决方法

您可以添加终止证明：

termination by size_change

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

或者您可以使用 fun 代替 function。在这种情况下，您既不需要定义良好的证明 (by pat_completeness auto) 也不需要手动终止证明。