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

[Jasmin Blanchette]

Hi Florian,

> a huge bunch indeed, but I am sure you will find ways to work this out.
> From a theoretic point of view it is a little bit – irritating that so
> much stuff is needed to issue something so fundamental as datatypes, but
> similar opinions have been held about blast in its beginning.

In a separate branch, Brian has demonstrated that the cardinals (and their dependencies) can be avoided -- but while his branch was a nice proof of concept, it was never finished and is now hopelessly outdated. In the longer term, we still have the hope of "cleaning up things" following his approach.

In fact, we did ask ourselves the question last time Makarius was in town: clean up then move to HOL or vice versa. The concensus was on "landing", i.e. getting something out the door and see later if it can be further improved.

> Have you already thought about bootstrap order?  If the datatype
> construction demands already lists, there is a problem ;-)…

Yes, we have thought about this. GFP requires lists, but LFP doesn't, so we should be in good shape. This having been said, we'll need to massage the background theories a bit more to get there. This will become relevant starting with Isabelle2015 (and the development branch leading to it) according to our roadmap.

Jasmin