Re: [isabelle] Modular definition of type class constants for datatypes with nested recursion
the best way to approach this is to replace count_rose mentally by a
syntactically different operation f and write down a specification
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
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)
The error message is:
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