[isabelle-dev] New (Co)datatypes: Status & Plan 2
Jasmin Christian Blanchette
jasmin.blanchette at gmail.com
Mon Nov 18 18:58:52 CET 2013
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
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"
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":
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":
by Tobias Nipkow, Christian Sternagel, and Markus Wenzel.
Then LFP and GFP need the following cardinals theories (all by Popescu &
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
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:
And part of GFP:
Apart from the folding of "_More" files, all these files would be moved to
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. ;)
More information about the isabelle-dev