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

[Jasmin Blanchette]

Hi Makarius,

Am 20.11.2013 um 14:12 schrieb Makarius <makarius at sketis.net>:

> Dmitriy had sent me some explanations which sessions represent the material to be moved to HOL in either case, but I never tried it out myself.  It is high time to do that now.  In particularly I would like to get a feeling for HOL-Proofs.  We also had some obscure drop-outs in summer with TTY / Proof General, if that is still relevant.

I seem to recall that the dropouts were in "HOL-BNF-Examples". This is of course suboptimal, but it isn't directly related to the move from "HOL-BNF" to "HOL".

> Can you say again which sessions/theories in which repository version constitute the datatype vs. codatatype part?

Version d983a020489d.

The sessions "HOL-Cardinals-FP" and "HOL-BNF-FP" would be the things we need to move to HOL. They look like this:

    session "HOL-Cardinals-FP" in Cardinals = HOL +
      theories Cardinal_Arithmetic_FP

    session "HOL-BNF-FP" in BNF = "HOL-Cardinals-FP" +
      theories BNF_LFP BNF_GFP

To compile the timing statistics I mentioned in my original email (e.g. 26 s for LFP + GFP), I ran (without building) the following session:

    session "HOL-BNF-FP" in BNF = HOL +
      theories BNF_LFP BNF_GFP

with and without "BNF_GFP". Since then I've optimized the dependencies further -- the difference between LFP and GFP is now a couple of seconds only, and three theory files ("BNF_GFP.thy", "Equiv_Relations_More.thy", and "Sublist.thy") are needed by GFP only. Since codatatypes are spreading like a disease (with Andreas, Andrei, Dmitriy, and Johannes using them already) and are a central feature of other proof assistants, it would perhaps be nicer if we put them in "HOL" as well.

(At some point, I had started splitting "HOL-Cardinals-FP" into "HOL-Cardinals-LFP" and "HOL-Cardinals-GFP", but there were so few theorems needed only for GFP that I discontinued that idea. My attempts are recorded in the hg history.)

I should also mention that some of the theories that are pulled in, like "Sublist.thy" and "Zorn.thy", could be rearranged or split in two. For example, we need only list prefixes, so we could have a theory called "List_Prefix.thy" that moves to "HOL" and keep the rest of "Sublist.thy" in "HOL/Library".

My plan is to start moving theories slowly over the coming weeks.

Jasmin