--- a/src/Doc/Datatypes/Datatypes.thy Tue Jul 30 16:22:39 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Tue Jul 30 19:49:42 2013 +0200
@@ -11,52 +11,194 @@
section {* Introduction *}
text {*
- * Isabelle2013 introduced new definitional package for datatypes and codatatypes
-
- * datatype support is similar to old package, due to Berghofer \& Wenzel \cite{xxx}
- * indeed, replacing \cmd{datatype} by \cmd{datatype\_new} is usually sufficient
- to port existing specifications to the new package
-
- * but it is more powerful, because it is now possible to have nested recursion
- through a large class of non-datatypes, notably finite sets:
+The 2013 edition of Isabelle introduced new definitional package for datatypes
+and codatatypes. The datatype support is similar to that provided by the earlier
+package due to Berghofer and Wenzel \cite{Berghofer-Wenzel:1999:TPHOL};
+indeed, replacing \cmd{datatype} by \cmd{datatype\_new} is usually sufficient
+to port existing specifications to the new package. What makes the new package
+attractive is that it supports definitions with recursion through a large class
+of non-datatypes, notably finite sets:
*}
datatype_new 'a tree = Node 'a "('a tree fset)"
text {*
- * another advantage: it supports local definitions:
+\noindent
+Another advantage of the new package is that it supports local definitions:
*}
context linorder
begin
-
-datatype_new flag = Less | Eq | Greater
-
+ datatype_new flag = Less | Eq | Greater
end
text {*
+\noindent
+Finally, the package also provides some convenience, notably automatically
+generated destructors. For example, the command
+*}
- * in a future release, \cmd{datatype\_new} is expected to displace \cmd{datatype}
+(*<*)hide_const Nil Cons hd tl(*>*)
+datatype_new 'a list = null: Nil | Cons (hd: 'a) (tl: "'a list")
+
+text {*
+\noindent
+introduces a discriminator @{const null} and a pair of selectors @{const hd} and
+@{const tl} characterized as follows:
+
+@{thm [display] list.collapse[no_vars]}
+
+The command \cmd{datatype\_new} is expected to displace \cmd{datatype} in a future
+release. Authors of new theories are encouraged to use \cmd{datatype\_new}, and
+maintainers of older theories might want to consider upgrading now.
+
+The package also provides codatatypes (or ``coinductive datatypes''), which may
+have infinite values. The following command introduces a type of infinite
+streams:
+*}
+
+codatatype 'a stream = Stream 'a "('a stream)"
+
+text {*
+\noindent
+Mixed inductive--coinductive recursion is possible via nesting.
+Compare the following four examples:
+*}
+
+datatype_new 'a treeFF = TreeFF 'a "('a treeFF list)"
+datatype_new 'a treeFI = TreeFI 'a "('a treeFF stream)"
+codatatype 'a treeIF = TreeIF 'a "('a treeFF list)"
+codatatype 'a treeII = TreeII 'a "('a treeFF stream)"
- *
+text {*
+To use the package, it is necessary to import the @{theory BNF} theory, which
+can be precompiled as the \textit{HOL-BNF}:
+*}
+
+text {*
+\noindent
+\texttt{isabelle build -b HOL-BNF}
+*}
+
+text {*
+ * TODO: LCF tradition
+ * internals: LICS paper
*}
+text {*
+This tutorial is organized as follows:
+
+ * datatypes
+ * primitive recursive functions
+ * codatatypes
+ * primitive corecursive functions
+
+the following sections focus on more technical aspects:
+how to register bounded natural functors (BNFs), i.e., type
+constructors via which (co)datatypes can (co)recurse,
+and how to derive convenience theorems for free constructors,
+as performed internally by \cmd{datatype\_new} and \cmd{codatatype}.
+
+then: Standard ML interface
+
+interaction with other tools
+ * code generator (and Quickcheck)
+ * Nitpick
+*}
+
+section {* Registering Bounded Natural Functors *}
+
+subsection {* Introductory Example *}
+
+subsection {* General Syntax *}
+
+section {* Generating Free Constructor Theorems *}
+
section {* Defining Datatypes *}
-text {*
- * theory to include
-*}
+subsection {* Introductory Examples *}
+
+subsubsection {* Nonrecursive Types *}
+
+subsubsection {* Simple Recursion *}
+
+subsubsection {* Mutual Recursion *}
+
+subsubsection {* Nested Recursion *}
+
+subsubsection {* Auxiliary Constants *}
+
+subsection {* General Syntax *}
+
+subsection {* Characteristic Theorems *}
+
+subsection {* Compatibility Issues *}
+
section {* Defining Primitive Recursive Functions *}
+subsection {* Introductory Examples *}
+
+subsection {* General Syntax *}
+
+subsection {* Characteristic Theorems *}
+
+subsection {* Compatibility Issues *}
+
+
section {* Defining Codatatypes *}
+subsection {* Introductory Examples *}
+
+subsection {* General Syntax *}
+
+subsection {* Characteristic Theorems *}
+
+
section {* Defining Primitive Corecursive Functions *}
+subsection {* Introductory Examples *}
+
+subsection {* General Syntax *}
+
+subsection {* Characteristic Theorems *}
+
+subsection {* Compatibility Issues *}
+
+
section {* Registering Bounded Natural Functors *}
+subsection {* Introductory Example *}
+
+subsection {* General Syntax *}
+
+
section {* Generating Free Constructor Theorems *}
-section {* Conclusion *}
+subsection {* Introductory Example *}
+
+subsection {* General Syntax *}
+
+section {* Registering Bounded Natural Functors *}
+
+section {* Standard ML Interface *}
+
+section {* Interoperability Issues *}
+
+subsection {* Transfer and Lifting *}
+
+subsection {* Code Generator *}
+
+subsection {* Quickcheck *}
+
+subsection {* Nitpick *}
+
+subsection {* Nominal Isabelle *}
+
+section {* Known Bugs and Limitations *}
+
+text {*
+* slow n-ary mutual (co)datatype, avoid as much as possible (e.g. using nesting)
+*}
end
--- a/src/Doc/Datatypes/document/root.tex Tue Jul 30 16:22:39 2013 +0200
+++ b/src/Doc/Datatypes/document/root.tex Tue Jul 30 19:49:42 2013 +0200
@@ -1,4 +1,4 @@
-\documentclass[12pt,a4paper,fleqn]{article}
+\documentclass[12pt,a4paper]{article} % fleqn
\usepackage{latexsym}
\usepackage{graphicx}
\usepackage{iman}
@@ -11,6 +11,9 @@
\newcommand{\cmd}[1]{\isacommand{#1}}
+\renewcommand{\isacharunderscore}{\mbox{\_}}
+\renewcommand{\isacharunderscorekeyword}{\mbox{\_}}
+
\hyphenation{isa-belle}
\isadroptag{theory}
@@ -27,13 +30,15 @@
\begin{abstract}
\noindent
-This tutorial describes how to use the new package for defining
-datatypes and codatatypes in Isabelle/HOL. The package provides four
-main user-level commands: \cmd{datatype\_new}, \cmd{codatatype}, \cmd{primrec\_new}, and
-\cmd{primcorec}. The \cmd{\_new} commands are designed to subsume, and eventually
+This tutorial describes how to use the new package for defining datatypes and
+codatatypes in Isabelle/HOL. The package provides four main user-level commands:
+\cmd{datatype\_new}, \cmd{codatatype}, \cmd{primrec\_new}, and \cmd{primcorec}.
+The commands suffixed by \cmd{\_new} are intended to subsume, and eventually
replace, the corresponding commands from the old datatype package.
\end{abstract}
+\tableofcontents
+
\input{Datatypes.tex}
\let\em=\sl
--- a/src/HOL/BNF/README.html Tue Jul 30 16:22:39 2013 +0200
+++ b/src/HOL/BNF/README.html Tue Jul 30 19:49:42 2013 +0200
@@ -23,7 +23,7 @@
The package is described in the following paper:
<ul>
- <li><a href="http://www21.in.tum.de/~traytel/papers/codatatypes/index.html">Foundational, Compositional (Co)datatypes for Higher-Order Logic—Category Theory Applied to Theorem Proving</a>, <br>
+ <li><a href="http://www21.in.tum.de/~traytel/papers/lics12-codatatypes/index.html">Foundational, Compositional (Co)datatypes for Higher-Order Logic—Category Theory Applied to Theorem Proving</a>, <br>
Dmitriy Traytel, Andrei Popescu, and Jasmin Christian Blanchette.<br>
<i>Logic in Computer Science (LICS 2012)</i>, 2012.
</ul>