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



Assume the following simple type class:

class foo =
  fixes count :: "'a ⇒ nat"

Instantiations for simple recursive data types are trivial:

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

  instance ..
end

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"?

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.

Cheers
Lars




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