[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
underlying principles:

  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.
  DOI=http://dx.doi.org/10.1109/LICS.2012.75

There are additional references at the end of the tutorial for the
datatype package,

  https://isabelle.in.tum.de/dist/Isabelle2016/doc/datatypes.pdf

--
cmr
+610481782084
http://octayn.net/




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.