*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] primcorec error: Type unification failed*From*: Joachim Breitner <breitner at kit.edu>*Date*: Wed, 12 Nov 2014 13:38:29 +0100

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**

**Follow-Ups**:**Re: [isabelle] primcorec error: Type unification failed***From:*Dmitriy Traytel

- Previous by Date: Re: [isabelle] AFP installation instructions
- Next by Date: Re: [isabelle] primcorec error: Type unification failed
- Previous by Thread: Re: [isabelle] AFP installation instructions
- Next by Thread: Re: [isabelle] primcorec error: Type unification failed
- Cl-isabelle-users November 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list