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

[Jasmin Blanchette]

Hi Alex,

(Briefly reviving an old thread...)

Am 06.08.2013 um 00:36 schrieb Alexander Krauss <krauss at in.tum.de>:

> In summary, except for the size functions which are somewhat special
> (and only used for termination proofs), the function package never uses
> any inductiveness and would happily swallow codatatypes as well.
> 
> Thus, I would propose to model the concept of a "type made of
> constructors" explicitly as a declaration which other tools can look up
> and add further interpretations to (in the sense of datatype
> interpretations). The function package would only depend on that. If I
> understand correctly, that declaration would essentially be rep_datatype
> without the induction rule. The function package (and I assume other
> tools, such as case syntax generation) can only rely on that and thus
> treat datatypes and codadatypes uniformly.
> 
> But, according to your schedule, these considerations become important
> only after the coming release, so I'll shut up for the moment.

The repository version of Isabelle (e95831757903) now has such a concept as part of the "HOL" image. It is called "Ctr_Sugar" [*]. Datatypes defined using "datatype" or "datatype_new", and codatatypes defined using "codatatype", are registered there; and using the ML interface, users can extend the database. Users can also use the command "wrap_free_constructors" to derive case constants (+ syntax), discriminators, selectors, and a wealth of properties about them.

I have also ported some of the existing code, including the function package (except "size" and "fundef_cong"), to use the new interface.

Jasmin

[*] Name suggestions welcome.