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