我已经为我的数据类型编写了一个自定义大小函数 size2
。使用这个函数,我可以手动证明我的函数的终止:
termination
apply (relation "measure (λ(a,b,c). size2 c)")
apply auto
done
有没有办法让
fun
使用我的替代大小函数进行自动终止证明? 最佳答案
通过使用属性 f
声明引理 is_measure f
,可以将函数 measure_function
注册为终止证明器的度量函数。在您的情况下,这看起来如下。
lemma is_measure_size2 [measure_function]: "is_measure size2" ..
然后,
lexicographic_order
使用的 fun
和 size_change
也尝试使用 size2
。关于isabelle - 使自动终止证明使用不同的大小功能,我们在Stack Overflow上找到一个类似的问题:https://stackoverflow.com/questions/29534558/