[isabelle] Declaration of (co)datatypes (was: Some corrections and amendments)
Ken Kubota <mail at kenkubota.de> writes:
> This is, of course, correct, but doesn't justify the specific mode of type
> introduction used here, namely the Backus-Naur form (BNF). The BNF was designed
> to specify formal grammars in computer science, but (mathematical) types are
> objects that must have certain logical properties, such as being non-empty.
> Thus the introduction of additional mathematical types should be subject to
> proof, and not a matter of mere declaration via the BNF.
The datatype declarations written in theory files is surface syntax for
the underlying datatype package which handles proving non-emptiness
among many other properties. The ML-style declaration is a convenient
abstraction that is easy to use. The following paper explains the
Dmitry Traytel, Andrei Popescu, and Jasmin C. Blanchette. 2012.
Foundational, Compositional (Co)datatypes for Higher-Order Logic:
Category Theory Applied to Theorem Proving. In Proceedings of the 2012
27th Annual IEEE/ACM Symposium on Logic in Computer Science (LICS '12).
IEEE Computer Society, Washington, DC, USA, 596-605.
There are additional references at the end of the tutorial for the
This archive was generated by a fusion of
Pipermail (Mailman edition) and