*To*: Lars Hupel <hupel at in.tum.de>*Subject*: Re: [isabelle] Modular definition of type class constants for datatypes with nested recursion*From*: Jasmin Christian Blanchette <jasmin.blanchette at gmail.com>*Date*: Tue, 10 Jun 2014 19:33:33 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <754300cfd012d184c95def922fbb4a43-EhVcX1hCQQpcRwURGhY3AF9BdAJSS1xcXF9EBlw1UENGV1gNQV53A0tUVFYwQEECXV5YSVhVXQ==-webmailer2@server02.webmailer.hosteurope.de>*References*: <754300cfd012d184c95def922fbb4a43-EhVcX1hCQQpcRwURGhY3AF9BdAJSS1xcXF9EBlw1UENGV1gNQV53A0tUVFYwQEECXV5YSVhVXQ==-webmailer2@server02.webmailer.hosteurope.de>

Hi Lars, Am 10.06.2014 um 18:50 schrieb Lars Hupel <hupel at in.tum.de>: > Now, consider a more elaborate data type: > > datatype_new 'a rose = Fork 'a "'a rose list" > > The naive attempt to instantiate "foo" for "rose" fails, as I expected: > > instantiation rose :: (foo) foo > begin > fun count_rose where > "count (Fork a as) = count a + count as" > > instance .. > end > > My question is: How to define "count_rose" in such a way that I don't have to repeat large parts of "count_list"? Here's one way, perhaps: class foo = fixes count :: "'a => nat" instantiation nat :: foo begin definition count_nat where "count n = n" instance .. end instantiation list :: (foo) foo begin primrec count_list where "count [] = 0" | "count (x # xs) = count x + count xs" instance .. end datatype_new 'a rose = Fork 'a "'a rose list" instantiation rose :: (foo) foo begin primrec count_rose where "count (Fork a as) = count a + count (map count as)" instance .. end Notice that the above solution works with "primrec" -- no ad hoc termination arguments! But it does cheat a little bit in "count (map count as)", first counting the elements of the list, then counting the list of nats. You might want to take a look at the BNF-based size extension. Try thm list.size thm rose.size to see what it has to offer. I suspect that you could base "count" on "size_xxx" (e.g. "size_list"). If not, the idiom used to derive "size" systematically for all BNF-based datatypes might still serve as an inspiration. Another possible source of inspiration is our sketch for a "countable" extension to BNF datatypes. I'm attaching the theory file. This development is somewhat simpler than the "size" extension, because it doesn't need to maintain two series of symbols in parallel (e.g. "size" instances vs. "size_xxx"). Hence, it appears to be a better model for what you want to do (assuming the "count (map count as)" cheat works for you). > The ultimate goal is to derive these instances automatically. I know about the relevant AFP entry (<http://afp.sourceforge.net/entries/Datatype_Order_Generator.shtml>), but as far as I can see, it builds on the old datatype package, and I'd rather like to have something for the new BNF package. The author of this entry is all in favor of porting it to the new package, and it is, from what I understand, only a matter of time until he gets to it. ;) Jasmin

**Attachment:
BNF_LFP_Countable.thy**

**Follow-Ups**:

**References**:

- Previous by Date: Re: [isabelle] Modular definition of type class constants for datatypes with nested recursion
- Next by Date: Re: [isabelle] Modular definition of type class constants for datatypes with nested recursion
- Previous by Thread: Re: [isabelle] Modular definition of type class constants for datatypes with nested recursion
- Next by Thread: Re: [isabelle] Modular definition of type class constants for datatypes with nested recursion
- Cl-isabelle-users June 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