When I write
codatatype inftree = node nat inftree inftree
primcorec one :: inftree and two :: inftree where
"one = node 1 one two"
| "two = node 2 one two"
I get
"inftree" is neither mutually corecursive with "inftree" nor nested corecursive through itself
Why, and how can I avoid it?
The command primcorec supports only primitive corecursion, so mutual corecursion is only supported for mutually corecursive codatatypes. Your two functions one and two are not primitively corecursive and therefore not directly supported. If the more general command corec supported mutual corecursion, it would fall into its fragment, but mutual corecursion has not yet been implemented for corec. Therefore, you have to find a non-mutual corecursive definition and then define one and two as derived functions. The canonical solution would be to use a bool as an argument:
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"
Also, you will have to generalise most properties about one and two to one_two first before you can prove them by coinduction.