--- 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