[isabelle] primcorec error: Type unification failed



Hi,

I’m doing my first steps with coinductive data type, and I’m struggling
with primcorec (probably due to a lack of understanding of the syntactic
requirements and the usual ways to work around them).

I created a data type for possibly infinite labeled trees:

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


With help of Andreas¹ I managed to define an „or“ operation: A path in
the resulting tree is a path in either one or the other:

primcorec lor :: "'a ltree ⇒ 'a ltree ⇒ 'a ltree"
  where "lnext (lor t1 t2) = (λ x.
           case (lnext t1 x) of Some t1' ⇒ (case lnext t2 x of Some t2' ⇒ Some (lor t1' t2') | None ⇒ Some t1')
                              | None     ⇒ lnext t2 x)"

Now I try to define an "and" operation: A path in the resulting tree is
an interleaving of paths in one or the other tree. I tried it like this:

primcorec land :: "'a ltree ⇒ 'a ltree ⇒ 'a ltree"
   where "lnext (land t1 t2) = (λ x.
      case (lnext t1 x) of Some t1' ⇒ (case lnext t2 x of Some t2' ⇒ Some (lor (land t1' t2) (land t1 t2')) | None ⇒ Some (land t1' t2))
                         | None     ⇒ (case lnext t2 x of Some t2' ⇒ Some (land t1 t2')                     | None ⇒ None))"

but it does not like the recursion via lor and gives this error message:

primcorec error:
  Type unification failed: Clash of types "_ + _" and "_ ltree"

Type error in application: incompatible operand type

Operator:  lor :: 'a ltree ⇒ 'a ltree ⇒ 'a ltree
Operand:   Inr (t1', t2) :: 'a ltree + 'a ltree × 'a ltree


It seems that primcorec likes definitions of the form

primcorec land :: "'a ltree ⇒ 'a ltree ⇒ 'a ltree"
   where "lnext (land t1 t2) = map_option (λ (x,y). land x y) o (λ x. ...)

better, but I couldn’t figure out how to use that here, where in once
case I need to invoke land twice and pass the result to lor.

Can I rewrite the definition in a way that primcorec likes it?


Greetings,
Joachim


¹ http://stackoverflow.com/questions/26883229/invalid-map-function-when-defining-a-corecursive-tree


-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.