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

[Makarius]

On Tue, 30 Jul 2013, Jasmin Christian Blanchette wrote:

> The package introduces a pair of commands: "datatype_new" and "codatatype". The
> main features are:
>
>  * Support for recursion via well-behaved type constructors (BNFs), e.g. "fset"
>  * Support for codatatypes (coinductive datatypes)
>  * More modular architecture, allowing mixed (co)recursion
>  * Work inside local theories
>
> Interestingly, the first three features are in essence what is mentioned 
> as future work in Berghofer & Wenzel's TPHOLs '99 paper [3], and the 
> fourth feature is of course highly desirable.

I am looking forward to that.

In retrospect, the TPHOLs'99 specification of future work was a bit 
speculative.  We've had some categorical guy telling us that it was "in 
pricinple trivial" to do all these three points, but you know yourself 
better how hard it is to make it really happen.

Point 4: local theories only emerged in 2006, so localization was not on 
the horizon yet.  The 1998 version of the datatype package was much more 
archaic in that respect -- actually the very first "definitional package" 
in the sense of having some theory data, or even just producing theorems 
under program control.  (That was not possible before 1997 or so, since 
the theory draft stamp mechanism did not exist yet.)


> Our first goal was to bring codatatypes to those who really need them. 
> Thanks to Andreas Lochbihler's efforts, the AFP entry "Coinductive" and 
> its dependencies ("JinjaThreads" and "Lazy-Lists-II") have now been 
> ported to the new package (instead of relying on heavy manual 
> constructions).

I've come across the excellent AFP/Coinductive material myself recently, 
when giving some hints to a user who was stuck with finite thinking for 
modelling operating systems.


> Another important missing piece is "primcorec".

What is the proper technical term for that?  Isn't it just "corec"?


 	Makarius