*To*: Joachim Breitner <breitner at kit.edu>, isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] primcorec error: Type unification failed*From*: Dmitriy Traytel <traytel at in.tum.de>*Date*: Wed, 12 Nov 2014 13:59:22 +0100*In-reply-to*: <1415795909.1417.8.camel@kit.edu>*References*: <1415795909.1417.8.camel@kit.edu>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.2.0

Dear Joachim,

Hope that helps, Dmitriy [1] http://www21.in.tum.de/~traytel/papers/fouco/fouco.pdf On 12.11.2014 13:38, Joachim Breitner wrote:

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

**References**:**[isabelle] primcorec error: Type unification failed***From:*Joachim Breitner

- Previous by Date: [isabelle] primcorec error: Type unification failed
- Next by Date: Re: [isabelle] Generic Contexts and Generic Data
- Previous by Thread: [isabelle] primcorec error: Type unification failed
- Next by Thread: Re: [isabelle] Problems with BNF_LFP_Rec_Sugar.add_primrec...
- 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