more (co)datatype documentation

--- a/src/Doc/Datatypes/Datatypes.thy	Tue Jul 30 23:17:26 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Wed Jul 31 11:28:59 2013 +0200
@@ -20,17 +20,17 @@
 of non-datatypes, notably finite sets:
 *}
 
-datatype_new 'a tree = Node 'a "('a tree fset)"
+    datatype_new 'a treeFS = TreeFS 'a "'a treeFS fset"
 
 text {*
 \noindent
 Another advantage of the new package is that it supports local definitions:
 *}
 
-context linorder
-begin
-  datatype_new flag = Less | Eq | Greater
-end
+    context linorder
+    begin
+      datatype_new flag = Less | Eq | Greater
+    end
 
 text {*
 \noindent
@@ -39,25 +39,25 @@
 *}
 
 (*<*)hide_const Nil Cons hd tl(*>*)
-datatype_new 'a list = null: Nil | Cons (hd: 'a) (tl: "'a list")
+    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]}
+%
+\[@{thm list.collapse(1)[no_vars]}\qquad @{thm list.collapse(2)[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.
+maintainers of older theories may want to consider upgrading in the coming months.
 
 The package also provides codatatypes (or ``coinductive datatypes''), which may
-have infinite values. The following command introduces a type of infinite
+have infinite values. The following command introduces a codatatype of infinite
 streams:
 *}
 
-codatatype 'a stream = Stream 'a "('a stream)"
+    codatatype 'a stream = Stream 'a "'a stream"
 
 text {*
 \noindent
@@ -65,60 +65,174 @@
 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)"
+    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}:
+can be precompiled as the \textit{HOL-BNF} image:
 *}
 
 text {*
 \noindent
-\texttt{isabelle build -b HOL-BNF}
+\ \ \ \ \texttt{isabelle build -b HOL-BNF}
 *}
 
 text {*
-  * TODO: LCF tradition
-  * internals: LICS paper
+The package, like its predecessor, fully adheres to the LCF philosophy
+\cite{mgordon79}: The characteristic theorems associated with the specified
+(co)datatypes are derived rather than introduced axiomatically.%
+\footnote{Nonetheless, if the \textit{quick\_and\_dirty} option is enabled, some
+of the internal constructions and most of the internal proof obligations are
+skipped.}
+The package's metatheory is described in a pair of papers
+\cite{traytel-et-al-2012,blanchette-et-al-wit}.
 *}
 
 text {*
 This tutorial is organized as follows:
 
-  * datatypes
-  * primitive recursive functions
-  * codatatypes
-  * primitive corecursive functions
+\begin{itemize}
+\item Section \ref{sec:defining-datatypes}, ``Defining Datatypes,''
+describes how to specify datatypes using the \cmd{datatype\_new} command.
+
+\item Section \ref{sec:defining-recursive-functions}, ``Defining Recursive 
+Functions,'' describes how to specify recursive functions using
+\cmd{primrec\_new}, \cmd{fun}, and \cmd{function}.
+
+\item Section \ref{sec:defining-codatatypes}, ``Defining Codatatypes,''
+describes how to specify codatatypes using the \cmd{codatatype} command.
+
+\item Section \ref{sec:defining-corecursive-functions}, ``Defining Corecursive 
+Functions,'' describes how to specify corecursive functions using the
+\cmd{primcorec} command.
 
-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}.
+\item Section \ref{sec:registering-bounded-natural-functors}, ``Registering 
+Bounded Natural Functors,'' explains how to set up the (co)datatype package to
+allow nested recursion through custom well-behaved type constructors.
+
+\item Section \ref{sec:generating-free-constructor-theorems}, ``Generating Free 
+Constructor Theorems,'' explains how to derive convenience theorems for free
+constructors, as performed internally by \cmd{datatype\_new} and
+\cmd{codatatype}.
 
-then: Standard ML interface
+\item Section \ref{sec:standard-ml-interface}, ``Standard ML Interface,''
+describes the package's programmatic interface.
 
-interaction with other tools
-  * code generator (and Quickcheck)
-  * Nitpick
+\item Section \ref{sec:interoperability}, ``Interoperability,''
+is concerned with the packages' interaction with other Isabelle packages and
+tools, such as the code generator and the counterexample generators.
+
+\item Section \ref{sec:known-bugs-and-limitations}, ``Known Bugs and 
+Limitations,'' concludes with open issues.
+\end{itemize}
 *}
 
-section {* Defining Datatypes *}
+section {* Defining Datatypes%
+  \label{sec:defining-datatypes} *}
+
+text {*
+This section describes how to specify datatypes using the \cmd{datatype\_new}
+command. The command is first illustrated through concrete examples featuring
+different flavors of recursion. More examples are available in
+\verb|~~/src/HOL/BNF/Examples|. The syntax is largely modeled after that of the
+existing \cmd{datatype} command.
+*}
 
 subsection {* Introductory Examples *}
 
 subsubsection {* Nonrecursive Types *}
 
+text {*
+enumeration type:
+*}
+
+    datatype_new trool = Truue | Faalse | Maaybe
+
+text {*
+Haskell-style option type:
+*}
+
+    datatype_new 'a maybe = Nothing | Just 'a
+
+text {*
+triple:
+*}
+
+    datatype_new ('a, 'b, 'c) triple = Triple 'a 'b 'c
+
 subsubsection {* Simple Recursion *}
 
+text {*
+simplest recursive type: natural numbers
+*}
+
+    datatype_new nat = Zero | Suc nat
+
+text {*
+lists were shown in the introduction
+
+terminated lists are a variant:
+*}
+
+    datatype_new ('a, 'b) tlist = TNil 'b | TCons 'a "('a, 'b) tlist"
+
+text {*
+On the right-hand side of the equal sign, the usual Isabelle conventions apply:
+Nonatomic types must be enclosed in double quotes.
+*}
+
 subsubsection {* Mutual Recursion *}
 
+text {*
+Mutual recursion = Define several types simultaneously, referring to each other.
+
+Simple example: distinction between even and odd natural numbers:
+*}
+
+    datatype_new even_nat = Zero | Even_Suc odd_nat
+    and odd_nat = Odd_Suc even_nat
+
+text {*
+More complex, and more realistic, example:
+*}
+
+    datatype_new ('a, 'b) expr =
+      Term "('a, 'b) term" | Sum "('a, 'b) term" "('a, 'b) expr"
+    and ('a, 'b) trm =
+      Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm"
+    and ('a, 'b) factor =
+      Const 'a | Var 'b | Sub_Expr "('a, 'b) expr"
+
 subsubsection {* Nested Recursion *}
 
-subsubsection {* Auxiliary Constants *}
+text {*
+Nested recursion = Have recursion through a type constructor.
+
+The introduction showed some examples of trees with nesting through lists.
+
+More complex example, which reuses our maybe and triple types:
+*}
+
+    datatype_new 'a triple_tree =
+      Triple_Tree "('a triple_tree maybe, bool, 'a triple_tree maybe) triple"
+
+text {*
+Recursion may not be arbitrary; e.g. impossible to define
+*}
+
+(*
+    datatype_new 'a foo = Foo (*<*) datatype_new 'a bar = Bar  "'a foo \<Rightarrow> 'a foo"
+*)
+
+subsubsection {* Auxiliary Constants and Syntaxes *}
+
+text {*
+* destructors
+* also mention special syntaxes
+*}
 
 subsection {* General Syntax *}
 
@@ -127,10 +241,24 @@
 subsection {* Compatibility Issues *}
 
 
-section {* Defining Primitive Recursive Functions *}
+section {* Defining Recursive Functions%
+  \label{sec:defining-recursive-functions} *}
+
+text {*
+This describes how to specify recursive functions over datatypes
+specified using \cmd{datatype\_new}. The focus in on the \cmd{primrec\_new}
+command, which supports primitive recursion. A few examples feature the
+\cmd{fun} and \cmd{function} commands, described in a separate tutorial  
+\cite{isabelle-function}.
+%%% TODO: partial_function?
+*}
 
 subsection {* Introductory Examples *}
 
+text {*
+More examples in \verb|~~/src/HOL/BNF/Examples|.
+*}
+
 subsection {* General Syntax *}
 
 subsection {* Characteristic Theorems *}
@@ -138,44 +266,98 @@
 subsection {* Compatibility Issues *}
 
 
-section {* Defining Codatatypes *}
+section {* Defining Codatatypes%
+  \label{sec:defining-codatatypes} *}
+
+text {*
+This section describes how to specify codatatypes using the \cmd{codatatype}
+command.
+*}
 
 subsection {* Introductory Examples *}
 
+text {*
+More examples in \verb|~~/src/HOL/BNF/Examples|.
+*}
+
+subsection {* General Syntax *}
+
+subsection {* Characteristic Theorems *}
+
+
+section {* Defining Corecursive Functions%
+  \label{sec:defining-corecursive-functions} *}
+
+text {*
+This section describes how to specify corecursive functions using the
+\cmd{primcorec} command.
+*}
+
+subsection {* Introductory Examples *}
+
+text {*
+More examples in \verb|~~/src/HOL/BNF/Examples|.
+*}
+
 subsection {* General Syntax *}
 
 subsection {* Characteristic Theorems *}
 
 
-section {* Defining Primitive Corecursive Functions *}
+section {* Registering Bounded Natural Functors%
+  \label{sec:registering-bounded-natural-functors} *}
 
-subsection {* Introductory Examples *}
+text {*
+This section explains how to set up the (co)datatype package to allow nested
+recursion through custom well-behaved type constructors. The key concept is that
+of a bounded natural functor (BNF).
+*}
+
+subsection {* Introductory Example *}
+
+text {*
+More examples in \verb|~~/src/HOL/BNF/Basic_BNFs.thy| and
+\verb|~~/src/HOL/BNF/More_BNFs.thy|.
+*}
 
 subsection {* General Syntax *}
 
-subsection {* Characteristic Theorems *}
+
+section {* Generating Free Constructor Theorems%
+  \label{sec:generating-free-constructor-theorems} *}
 
-subsection {* Compatibility Issues *}
+text {*
+This section explains how to derive convenience theorems for free constructors,
+as performed internally by \cmd{datatype\_new} and \cmd{codatatype}.
 
+  * need for this is rare but may arise if you want e.g. to add destructors to
+    a type not introduced by ...
 
-section {* Registering Bounded Natural Functors *}
+  * also useful for compatibility with old package, e.g. add destructors to
+    old \cmd{datatype}
+*}
 
 subsection {* Introductory Example *}
 
 subsection {* General Syntax *}
 
 
-section {* Generating Free Constructor Theorems *}
+section {* Standard ML Interface%
+  \label{sec:standard-ml-interface} *}
 
-subsection {* Introductory Example *}
+text {*
+This section describes the package's programmatic interface.
+*}
 
-subsection {* General Syntax *}
 
-section {* Registering Bounded Natural Functors *}
+section {* Interoperability%
+  \label{sec:interoperability} *}
 
-section {* Standard ML Interface *}
-
-section {* Interoperability Issues *}
+text {*
+This section is concerned with the packages' interaction with other Isabelle
+packages and tools, such as the code generator and the counterexample
+generators.
+*}
 
 subsection {* Transfer and Lifting *}
 
@@ -187,7 +369,13 @@
 
 subsection {* Nominal Isabelle *}
 
-section {* Known Bugs and Limitations *}
+
+section {* Known Bugs and Limitations%
+  \label{sec:known-bugs-and-limitations} *}
+
+text {*
+This section lists known open issues of the package.
+*}
 
 text {*
 * slow n-ary mutual (co)datatype, avoid as much as possible (e.g. using nesting)

--- a/src/Doc/Datatypes/document/root.tex	Tue Jul 30 23:17:26 2013 +0200
+++ b/src/Doc/Datatypes/document/root.tex	Wed Jul 31 11:28:59 2013 +0200
@@ -1,4 +1,6 @@
 \documentclass[12pt,a4paper]{article} % fleqn
+\usepackage{cite}
+\usepackage{enumitem}
 \usepackage{latexsym}
 \usepackage{graphicx}
 \usepackage{iman}
@@ -9,10 +11,17 @@
 \usepackage{style}
 \usepackage{pdfsetup}
 
+\newbox\boxA
+\setbox\boxA=\hbox{\ }
+\parindent=4\wd\boxA
+
 \newcommand{\cmd}[1]{\isacommand{#1}}
 
 \renewcommand{\isacharunderscore}{\mbox{\_}}
 \renewcommand{\isacharunderscorekeyword}{\mbox{\_}}
+\renewcommand{\isachardoublequote}{\mbox{\upshape{``}}}
+\renewcommand{\isachardoublequoteopen}{\mbox{\upshape{``}}}
+\renewcommand{\isachardoublequoteclose}{\mbox{\upshape{''}}}
 
 \hyphenation{isa-belle}
 
@@ -21,7 +30,9 @@
 \title{%\includegraphics[scale=0.5]{isabelle_hol} \\[4ex]
 Defining (Co)datatypes in Isabelle/HOL}
 \author{\hbox{} \\
-Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel \\
+Jasmin Christian Blanchette \\
+Andrei Popescu \\
+Dmitriy Traytel \\
 {\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\
 \hbox{}}
 \begin{document}

--- a/src/Doc/manual.bib	Tue Jul 30 23:17:26 2013 +0200
+++ b/src/Doc/manual.bib	Wed Jul 31 11:28:59 2013 +0200
@@ -301,6 +301,12 @@
   author = "Jasmin Christian Blanchette and Tobias Nipkow",
   crossref = {itp2010}}
 
+@unpublished{blanchette-et-al-wit,
+  author = {J.C. Blanchette and A. Popescu and D. Traytel},
+  title = {Witnessing (Co)datatypes},
+  year = 2013,
+  note = {\url{http://www21.in.tum.de/~traytel/papers/witness/wit.pdf}}}
+
 @inproceedings{why3,
   author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and Claude March\'e and Andrei Paskevich},
   title = {{Why3}: Shepherd Your Herd of Provers},
@@ -1662,7 +1668,16 @@
       Subtyping (long version)},
   year = 2011,
   note = {Submitted,
-      \url{http://isabelle.in.tum.de/doc/implementation.pdf}}},
+      \url{http://isabelle.in.tum.de/doc/implementation.pdf}}}
+
+@inproceedings{traytel-et-al-2012,
+  author = "Dmitriy Traytel and Andrei Popescu and Jasmin Christian Blanchette",
+  title     = {Foundational, Compositional (Co)datatypes for Higher-Order
+               Logic---{C}ategory Theory Applied to Theorem Proving},
+  year      = {2012},
+  pages     = {596--605},
+  booktitle = {LICS 2012},
+  publisher = {IEEE}
 }
 
 @Unpublished{Trybulec:1993:MizarFeatures,