isabelle - primcofix中的相互递归

Question

当我写

codatatype inftree = node nat inftree inftree

primcorec one :: inftree and two :: inftree where
    "one = node 1 one two"
  | "two = node 2 one two"

我明白了

"inftree" 既不与 "inftree" 相互核递归，也不是通过自身嵌套核递归

为什么，我该如何避免呢？

Answer 1

该命令primcorec仅支持原始 corecursion，因此互 corecursion 仅支持相互 corecursive codatatypes。one您的两个函数two并不是原始的核心递归，因此不直接支持。如果更通用的命令corec支持相互共游，它将落入其片段中，但尚未实现相互共游corec。因此，您必须找到一个非相互的核心递归定义，然后将oneand定义two为派生函数。规范的解决方案是使用 abool作为参数：

 primcorec one_two :: "bool => inftree" where
    "one_two is_one = Node (if is_one then 1 else 2) (one_two True) (one_two False)"

 definition "one = one_two True"
 definition "two = one_two False"

此外，在通过共归纳法证明它们之前one，您two 必须首先概括大多数性质。one_two