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



Hi Lars,

Am 10.06.2014 um 20:10 schrieb Lars Hupel <hupel at in.tum.de>:

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

Yes, I ran into this issue when implementing the "size" extension. To sort this out, it should be possible to rephrase the "primrec" specification so that it's expressed in terms of "map". Then you can derive the desired specification without "map" as a theorem. Perhaps we can discuss this live if you're in the office tomorrow.

Jasmin





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