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

[Jasmin Christian Blanchette]

Hi all,

Back in August, I advertised our plan with the Bounded Natural Functor (BNF)
package. One of the items on the plan was to move the "datatype_new" command
into Isabelle before the Isabelle2013-1 release. After some reflection,
Makarius, Dmitriy, and I decided to postpone it to after the release, which
means now.

The updated plan is as follows (assuming a 8-month release schedule):

 1. Have "datatype_new" next to "datatype" in "HOL" for Isabelle2014.

 2. Rename "datatype" |-> "legacy_datatype" and "datatype_new" |-> "datatype"
    for Isabelle2015.

 3. Move "legacy_datatype" to "src/HOL/Library" for Isabelle2015-1.

Recall that the motivation for "datatype_new" is to make it possible to do
recursion through non-datatypes (e.g. datatype hfset = HFset "hfset fset"); to
support local definitions; and to play well with the new codatatypes.

The rest of this email is about step 1.

A question that arises is whether we should have only "datatype_new" (and
"primrec_new"; i.e. the LFP part) in "HOL" or also "codatatype" (and
"primcorec"; i.e. the GFP part). The BNF package is organized in such a way that
it can be split in the middle, so we really have both options. The "HOL" build
time is a criterion. On my 4-core laptop from 2010, running LFP (+ dependencies)
on top of HOL takes 18 to 20 s of wall-clock time; adding GFP adds about 6 s.
This leaves us under our planned budget of 30 s. If we stick to the plan above,
we will have recovered some of that time by Isabelle2015-1.

The next concern is the dependencies, which would have to be moved to "HOL" as
well. They're part of the time calculation, but time is not the only roadblock
before moving something to "HOL".

First, LFP needs these five theories from "Library":

    Library/Wfrec.thy
    Library/Infinite_Set.thy
    Library/Order_Relation.thy
    Library/Order_Union.thy
    Library/Zorn.thy

These were developed by various people: Jacques Fleuriot, Stephan Merz, Tobias
Nipkow, Larry Paulson, Andrei Popescu, Konrad Slind, and Christian Sternagel.
GFP also needs one more theory from "Library":

    Library/Sublist.thy

by Tobias Nipkow, Christian Sternagel, and Markus Wenzel.

Then LFP and GFP need the following cardinals theories (all by Popescu &
Traytel):

    Cardinals/Fun_More_FP.thy
    Cardinals/Order_Relation_More_FP.thy
    Cardinals/Wellfounded_More_FP.thy
    Cardinals/Wellorder_Relation_FP.thy
    Cardinals/Wellorder_Embedding_FP.thy
    Cardinals/Constructions_on_Wellorders_FP.thy
    Cardinals/Cardinal_Order_Relation_FP.thy
    Cardinals/Cardinal_Arithmetic_FP.thy

A few remarks on the cardinals theories:

 1. The "_FP" suffix is because those are already minimized w.r.t. LFP/GFP.
    Results not needed for the FP constructions are put in theories without the
    suffix.

 2. Theories with "_More" in their names are meant to be natural extensions of
    existing theories in "HOL" (e.g. "Fun_More.thy" vs. "Fun.thy"). As part of
    the move, we would probably fold them.

 3. It would make sense to clean them up a bit so that they don't export
    abbreviations etc. They're already in a pretty good shape, e.g. they hardly
    define any "simp" rules.

For completeness, these are the theories that are genuinely part of LFP:

    BNF/BNF_Util.thy
    BNF/BNF_Def.thy
    BNF/Basic_BNFs.thy
    BNF/BNF_Comp.thy
    BNF/BNF_FP_Base.thy
    BNF/BNF_LFP.thy

And part of GFP:

    BNF/Equiv_Relations_More.thy
    BNF/BNF_GFP.thy

Apart from the folding of "_More" files, all these files would be moved to
"src/HOL".

I fully realize this is a large change. Yet, beyond the particulars, this is
nothing new since we've been saying for over two years that our long-term goals
is to replace the old datatype package -- indeed, Makarius has put the
"localization" of the old package on hold trusting that we would one day deliver
on our promises -- and we've spelled out our plans on this mailing list back in
August. Still, I want to make sure there is wide agreement before proceeding. So
please speak now or forever hold your peace. ;)

Regards,

Jasmin