isabelle - 使用不同大小的函数进行自动终止证明

Question

我为我的数据类型编写了一个自定义大小函数size2。使用此函数，我可以手动证明函数的终止:

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

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

Answer 1

通过使用属性 measure_function 声明引理 is_measure f，可以将函数 f 注册为终止证明者的测量函数。对于您的情况，如下所示。

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

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