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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
