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关于代码方程的第二章，但如果能快速地继续构建剩余的管道，并在基本管道工作时研究理论的复杂性，那将是一件很好的事情。

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

当我添加

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)，也不需要手动终止证明。