"invalid map function" when defining a corecursive tree

Question

I’m doing my first experiments with codatatype, but I’m stuck rather early. I started with this definition of a branching, possibly infinite tree:

codatatype (lset: 'a) ltree = Node (lnext : "'a ⇒ 'a ltree option")

and some definitions work fine:

primcorec lempty :: "'a ltree"
  where "lnext lempty = (λ _ . None)"

primcorec single :: "'a ⇒ 'a ltree"
  where "lnext (single x) = (λ _ . None)(x := Some lempty)"

but this does not work:

primcorec many :: "'a ⇒ 'a ltree"
  where "lnext (many x) = (λ _ . None)(x := Some (many x))"

as I get the error message

primcorec error:
  Invalid map function in "[x ↦ many x]"

I could work around it by writing

primcorec many :: "'a ⇒ 'a ltree"
  where "lnext (many x) = (λ x'. if x' = x then Some (many x) else None)"

which makes be believe that primcorec needs to “know something about” the function update operator, similar to how fun needs fundef_cong lemmas and inductive needs mono lemmas. But what exactly?

Answer 1

If the codatatype recurses through other type constructors, then primcorec expects that the recursive calls are properly nested in the map functions of these type constructors. In the example, the recursion goes through the function type and the option type, whose map functions are op o and map_option. Consequently, the recursive call to many should have the form op o (map_option many). Hence, the following definition works:

primcorec many :: "'a ⇒ 'a ltree"
where "lnext (many x) = map_option many ∘ [x ↦ x]"

For convenience, primcorec supports a few more syntactic input formats. In particular, the map function for the function type can be also written using lambda abstractions. Additionally, it supports case distinctions and ifs. This is why your second version is accepted. However, when you look at the generated definition many_def, you will see that it is more complicated than with the explicit map functions.

primcorec does not suport registration of arbitrary functions, so you cannot use fun_upd in the original form. Primitive corecursion is syntactical. Maybe in the future there will be a corecursive counterpart to function.

The map functions are explained in the tutorial on datatypes and in this paper.