[isabelle] Modular definition of type class constants for datatypes with nested recursion
- To: <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] Modular definition of type class constants for datatypes with nested recursion
- From: Lars Hupel <hupel at in.tum.de>
- Date: Tue, 10 Jun 2014 18:50:05 +0200
- User-agent: Host Europe Webmailer/2.0
Assume the following simple type class:
class foo =
fixes count :: "'a ⇒ nat"
Instantiations for simple recursive data types are trivial:
instantiation list :: (foo) foo
fun count_list where
"count  = 0" |
"count (x # xs) = count x + count xs"
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
fun count_rose where
"count (Fork a as) = count a + count as"
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and