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



Hi Lars,

> instantiation list :: (foo) foo
> begin
>   fun count_list where
>   "count [] = 0" |
>   "count (x # xs) = count x + count xs"
> 
>   instance ..
> end
> 
> 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

the best way to approach this is to replace count_rose mentally by a
syntactically different operation f and write down a specification for f
accordingly.  This then should be transferable to an instantiation.

> 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.

Well, sounds there is some work to do there.

Hope this helps,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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