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

Hi Florian,

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.

unfortunately, this approach isn't modular. If I pull out the specification of "count_rose" into a different constant, e.g. "count_rose_pre", ideally I'd still want to use the instance "list :: foo", but this requires the element type ("rose") to have a "foo" instance. This naive translation merely trades a "circular constant dependency" error message for a circular dependency which is impossible to express.

Surely I can also pull out the definition of "count_list" and refer to that, but my attempt failed:

datatype_new 'a seq = Cons 'a "'a seq" | Nil
datatype_new 'a rose = Fork 'a "'a rose seq"

primrec_new count_seq_pre where
"count_seq_pre _ Nil = 0" |
"count_seq_pre f (Cons x xs) = f x + count_seq_pre f xs"

primrec_new count_rose_pre where
"count_rose_pre f (Fork a as) = f a + count_seq_pre (count_rose_pre f) as"

The error message is:

primrec_new error:
  Invalid map function in "count_seq_pre (count_rose_pre f)"

If I change everything to "fun" and use "datatype_new_compat", the function package is unable to find a termination order.


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