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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
