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



Yet a few more thoughts.

To get a deeper understanding of the specification, you could try the
following:

a) provide a f corresponding to count ['a list] but abstracted over
count ['a] (»dictionary«)

b) define count ['a list] in terms of f

c) try to write down your specification for a g corresponding to count
['a rose].

If your specification mechanisms chokes then, its beyond the borders of
the specification mechanisms itself (at least in its particular setup).

If no, try to replace g by count ['a rose] using plain overloading
target (remove the const constraint from count if necessary).  If this
is rejected, it is just not covered by overloaded definitions in Isabelle.

If no, the instantiation target itself cannot cover your specification.

Beyond that, I can emphasize what Jasmin has hinted at: particularly
concerning automatically derived specifications, you should not rely on
fun.  For systematic instantiation, usually primrec specifications can
be achieved, perhaps including funny combinators defined once and for
all by hand.

	Florian

On 10.06.2014 18:50, Lars Hupel wrote:
> 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
> 

-- 

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.