使自动终止证明使用不同大小的功能

Question

我已经为我的数据类型编写了自定义大小函数 size2。使用这个函数我可以手动证明我的函数终止：

termination 
apply (relation "measure (λ(a,b,c). size2 c)")
apply auto
done

有没有办法让 fun 使用我的替代大小函数来自动终止证明？

Answer 1

函数f 可以通过声明带有属性measure_function 的引理is_measure f 来注册为终止证明者的度量函数。在您的情况下，这看起来如下。

lemma is_measure_size2 [measure_function]: "is_measure size2" ..

然后，lexicographic_order，fun 使用，size_change 也尝试 size2。