Isabelle终止了包含自身映射的数据类型上的函数

Question

是否可以在Isabelle中定义一个终止递归函数f，其中

• f具有t类型的单个参数，使得t类型的值可以包含到t类型的值的映射，并且
• f对这种映射范围内的所有元素执行递归调用

例如，考虑理论上定义的数据类型trieTrie_Fun:

datatype 'a trie = Nd bool "'a ⇒ 'a trie option"

以及我对一个简单函数height的尝试，该函数旨在计算尝试的高度(具有有限多个传出边(：

theory Scratch
imports "HOL-Data_Structures.Trie_Fun"
begin
function height :: "'a trie ⇒ nat" where
"height (Nd _ edges) = (if dom edges = Set.empty ∨ ¬ finite (dom edges)
then 0
else 1 + Max (height ` ran edges))"
by pat_completeness auto
termination (* ??? *)
end

这里，lexicographic_order不足以证明函数是终止的，但到目前为止，我还不能对trie(用于终止(制定任何本身不需要类似递归的度量。我必须承认，我不确定我是否正确理解了Isabelle/HOL中的数据类型(即，上述定义的trie实际上是否总是有限高度(。

是否可以显示height终止？

Answer 1

根据Peter Zeller的评论，我能够通过将(domintros)添加到定义中，然后使用事实height.domintros对trie进行归纳来证明height的终止，从而得到以下终止证明：

function (domintros) height :: "'a trie ⇒ nat" where
"height (Nd _ edges) = (if dom edges = Set.empty ∨ ¬ finite (dom edges)
then 0
else 1 + Max (height ` ran edges))"
by pat_completeness auto
termination apply auto
proof -
fix x :: "'a trie"
show "height_dom x"
proof (induction)
case (Nd b edges)
have "(⋀x. x ∈ ran edges ⟹ height_dom x)"
proof -
fix x assume "x ∈ ran edges" 
then have "∃a. edges a = Some x"
unfolding ran_def by blast
then have "∃a. Some x = edges a"
by (metis (no_types))
then have "Some x ∈ range edges"
by blast
then show "height_dom x"
using Nd by auto
qed
then show ?case
using height.domintros by blast
qed
qed