Re: [isabelle] Modular definition of type class constants for datatypes with nested recursion

Hi Lars,

Am 10.06.2014 um 18:50 schrieb Lars Hupel <hupel at>:

> 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
     definition count_nat where "count n = n"

     instance ..

    instantiation list :: (foo) foo
     primrec count_list where
     "count [] = 0" |
     "count (x # xs) = count x + count xs"

     instance ..

    datatype_new 'a rose = Fork 'a "'a rose list"

    instantiation rose :: (foo) foo
     primrec count_rose where
     "count (Fork a as) = count a + count (map count as)"

     instance ..

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 (<>), 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. ;)


Attachment: BNF_LFP_Countable.thy
Description: Binary data

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