使用集合理解的函数的终止证明

Question

考虑以下树和子树的愚蠢 Isabelle 定义：

datatype tree = Leaf int
              | Node tree tree

fun children :: "tree ⇒ tree set" where
"children (Leaf _) = {}" |
"children (Node a b) = {a, b}"

lemma children_decreasing_size:
  assumes "c ∈ children t"
  shows   "size c < size t"
using assms
by (induction t, auto)

function subtrees :: "tree ⇒ tree set" where
"subtrees t = { s | c s. c ∈ children t ∧ s ∈ subtrees c }"
by auto
termination
apply (relation "measure size", simp)

尽管递归调用仅在 children 上进行，但 subtrees 的终止证明在这一点上卡住了，well-founded size 关系（如微不足道的引理所示）。

证明状态如下：

goal (1 subgoal):
 1. ⋀t x xa xb. (xa, t) ∈ measure size

当然，这是不可能证明的，因为 xa 是 t 的 child 的信息丢失了。我做错什么了吗？我能做些什么来保存证明吗？我注意到我可以使用列表而不是集合来制定相同的定义：

fun children_list :: "tree ⇒ tree list" where
"children_list (Leaf _) = []" |
"children_list (Node a b) = [a, b]"

function subtrees_list :: "tree ⇒ tree list" where
"subtrees_list t = concat (map subtrees_list (children_list t))"
by auto
termination
apply (relation "measure size", simp)

并获得更多信息、可证明的终止目标：

goal (1 subgoal):
 1. ⋀t x.
       x ∈ set (children_list t) ⟹
       (x, t) ∈ measure size

这是否是 Isabelle 的一些限制，我应该通过不使用集合来解决这个问题？

Answer 1

subtrees 的集合推导中对 c : children t 的限制不会出现在终止证明义务中，因为函数包先验地不知道 & 的任何事情。可以使用一致性规则来实现这一点。在这种情况下，您可以在本地将 conj_cong 声明为 [fundef_cong] 以实质上模拟从左到右的评估顺序（尽管 HOL 中没有评估这样的东西）。例如，

context notes conj_cong[fundef_cong] begin
fun subtrees :: ...
termination ...
end

上下文块确保声明 conj_cong[fundef_cong] 仅对该函数定义有效。

带有列表的版本可以工作，因为它使用函数 map，默认情况下有一个同余规则。如果您在集合上使用了 monadic 绑定操作（而不是集合推导），那么同样应该适用于集合。

使用集合理解的函数的终止证明

Termination proof with functions using set comprehensions

termination

isabelle