我已经为我的数据类型编写了一个自定义大小函数 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 使用的 funsize_change 也尝试使用 size2

关于isabelle - 使自动终止证明使用不同的大小功能,我们在Stack Overflow上找到一个类似的问题:https://stackoverflow.com/questions/29534558/

10-11 22:58
查看更多