[isabelle-dev] New (Co)datatypes: Status & Plan (FYI)

[Dmitriy Traytel]

Am 04.08.2013 18:57, schrieb Florian Haftmann:
>> For nonnested recursive datatypes, compatibility is quasi-100%; and for nested
>> datatypes, the package will support an optional "nested to mutual" reduction to
>> simulate the old package, so that the same theorems as before are available
>> (albeit under different names).
> has an explicit need for a »nested to mutual« mode ever been
> articulated?  In my personal opinion this construction has always
> appeared counter-intuitive, because the inherent redundancy with an
> existing type springs to your eyes after you have done this game a few
> times.  Maybe a chance to save some work.
I also find it always counter-intuitive when I have to use it (of course 
the "have to" will not apply anymore in our case). However the 
"mutualized" primrec seems to be more flexible. Without the 
mutualization, in order to define a primitive recursive function on say

datatype 'a tree = Node 'a "'a tree list"

one is allowed to apply the recursive calls through the "map" on lists 
only. Defining a function that additionally filters the nested list of 
children becomes counter-intuitive then.

There is also a more technical reason why we want to perform the "nested 
to mutual" reduction: It gives us a very cheap compatibility layer for 
the old package. I.e. everything that is defined by the new package and 
falls into the fragment of the old package can be registered as an old 
datatype benefiting from all the infrastructure built around it (e.g. 
size function, Quickcheck, and other "datatype interpretations"). We 
expect this actually to save much work, compared to reimplementing that 
functionality now before moving to Main (instead we can do it in a lazy 
fashion).

Dmitriy