--- a/src/Doc/Datatypes/Datatypes.thy Wed Apr 23 10:23:27 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Wed Apr 23 10:23:27 2014 +0200
@@ -103,7 +103,7 @@
\item Section \ref{sec:defining-recursive-functions}, ``Defining Recursive
Functions,'' describes how to specify recursive functions using
-@{command primrec}, \keyw{fun}, and \keyw{function}.
+@{command primrec}.
\item Section \ref{sec:defining-codatatypes}, ``Defining Codatatypes,''
describes how to specify codatatypes using the @{command codatatype} command.
@@ -599,17 +599,8 @@
The syntactic entity \synt{name} denotes an identifier \cite{isabelle-isar-ref}.
The command is interesting because the old datatype package provides some
-functionality that is not yet replicated in the new package:
-
-\begin{itemize}
-\setlength{\itemsep}{0pt}
-
-\item It is integrated with \keyw{fun} \cite{isabelle-function},
-Nitpick \cite{isabelle-nitpick}, Quickcheck, and other packages.
-
-\item It is extended by various add-ons, notably to produce instances of the
-@{const size} function.
-\end{itemize}
+functionality that is not yet replicated in the new package, such as the
+integration with Quickcheck.
A few remarks concern nested recursive datatypes:
@@ -626,8 +617,8 @@
no way to register old-style datatypes as new-style datatypes).
\item The recursor produced for types that recurse through functions has a
-different signature than with the old package. This makes it impossible to use
-the old \keyw{primrec} command.
+different signature than with the old package. This might affect the behavior of
+some third-party extensions.
\end{itemize}
An alternative to @{command datatype_compat} is to use the old package's
@@ -657,13 +648,15 @@
& \quad\vdots \\
& @{text t.un_C\<^sub>n1}$, \ldots, $@{text t.un_C\<^sub>nk\<^sub>n} \\
Set functions: &
- @{text set1_t}, \ldots, @{text t.setm_t} \\
+ @{text t.set1_t}, \ldots, @{text t.setm_t} \\
Map function: &
@{text t.map_t} \\
Relator: &
@{text t.rel_t} \\
Recursor: &
- @{text t.rec_t}
+ @{text t.rec_t} \\
+Size function: &
+ @{text t.size_t}
\end{tabular}
\medskip
@@ -672,6 +665,9 @@
The case combinator, discriminators, and selectors are collectively called
\emph{destructors}. The prefix ``@{text "t."}'' is an optional component of the
names and is normally hidden.
+
+In addition to the above, the @{class size} class is instantiated to overload the
+@{const size} function based on @{text t.size_t}.
*}
@@ -685,15 +681,16 @@
\begin{itemize}
\setlength{\itemsep}{0pt}
-\item The \emph{free constructor theorems} are properties about the constructors
-and destructors that can be derived for any freely generated type. Internally,
-the derivation is performed by @{command free_constructors}.
-
-\item The \emph{functorial theorems} are properties of datatypes related to
-their BNF nature.
-
-\item The \emph{inductive theorems} are properties of datatypes related to
-their inductive nature.
+\item The \emph{free constructor theorems}
+(Section~\ref{sssec:free-constructor-theorems}) are properties of the
+constructors and destructors that can be derived for any freely generated type.
+Internally, the derivation is performed by @{command free_constructors}.
+
+\item The \emph{functorial theorems} (Section~\ref{sssec:functorial-theorems})
+are properties of datatypes related to their BNF nature.
+
+\item The \emph{inductive theorems} (Section~\ref{sssec:inductive-theorems})
+are properties of datatypes related to their inductive nature.
\end{itemize}
@@ -933,6 +930,18 @@
@{thm list.rec(1)[no_vars]} \\
@{thm list.rec(2)[no_vars]}
+\item[@{text "t."}\hthm{rec\_o\_map}\rm:] ~ \\
+@{thm list.rec_o_map[no_vars]}
+
+\item[@{text "t."}\hthm{size} @{text "[simp, code]"}\rm:] ~ \\
+@{thm list.size(1)[no_vars]} \\
+@{thm list.size(2)[no_vars]} \\
+@{thm list.size(3)[no_vars]} \\
+@{thm list.size(4)[no_vars]}
+
+\item[@{text "t."}\hthm{size\_o\_map}\rm:] ~ \\
+@{thm list.size_o_map[no_vars]}
+
\end{description}
\end{indentblock}
@@ -963,9 +972,9 @@
\item \emph{The Standard ML interfaces are different.} Tools and extensions
written to call the old ML interfaces will need to be adapted to the new
-interfaces. Little has been done so far in this direction. Whenever possible, it
-is recommended to use @{command datatype_compat} or \keyw{rep\_datatype}
-to register new-style datatypes as old-style datatypes.
+interfaces. This concerns Quickcheck in particular. Whenever possible, it is
+recommended to use @{command datatype_compat} to register new-style datatypes
+as old-style datatypes.
\item \emph{The constants @{text t_case}, @{text t_rec}, and @{text t_size} are
now called @{text case_t}, @{text rec_t}, and @{text size_t}.}
@@ -976,15 +985,14 @@
type of the recursor, used by \keyw{primrec}. Recursion through functions was
handled specially. In the new package, nested recursion (for functions and
non-functions) is handled in a more modular fashion. The old-style recursor can
-be generated on demand using @{command primrec}, as explained in
-Section~\ref{sssec:primrec-nested-as-mutual-recursion}, if the recursion is via
-new-style datatypes.
+be generated on demand using @{command primrec} if the recursion is via
+new-style datatypes, as explained in
+Section~\ref{sssec:primrec-nested-as-mutual-recursion}.
\item \emph{Accordingly, the induction rule is different for nested recursive
datatypes.} Again, the old-style induction rule can be generated on demand using
-@{command primrec}, as explained in
-Section~\ref{sssec:primrec-nested-as-mutual-recursion}, if the recursion is via
-new-style datatypes.
+@{command primrec} if the recursion is via new-style datatypes, as explained in
+Section~\ref{sssec:primrec-nested-as-mutual-recursion}.
\item \emph{The internal constructions are completely different.} Proof texts
that unfold the definition of constants introduced by \keyw{datatype} will be
@@ -1634,13 +1642,13 @@
with $m > 0$ live type variables and $n$ constructors @{text "t.C\<^sub>1"},
\ldots, @{text "t.C\<^sub>n"}, the same auxiliary constants are generated as for
datatypes (Section~\ref{ssec:datatype-generated-constants}), except that the
-recursor is replaced by a dual concept:
+recursor is replaced by a dual concept and no size function is produced:
\medskip
\begin{tabular}{@ {}ll@ {}}
Corecursor: &
- @{text corec_t}
+ @{text t.corec_t}
\end{tabular}
*}
@@ -1655,20 +1663,20 @@
\begin{itemize}
\setlength{\itemsep}{0pt}
-\item The \emph{free constructor theorems} are properties about the constructors
-and destructors that can be derived for any freely generated type.
-
-\item The \emph{functorial theorems} are properties of datatypes related to
+\item The \emph{free constructor theorems}
+(Section~\ref{sssec:free-constructor-theorems}) are properties of the
+constructors and destructors that can be derived for any freely generated type.
+
+\item The \emph{functorial theorems}
+(Section~\ref{sssec:functorial-theorems}) are properties of datatypes related to
their BNF nature.
-\item The \emph{coinductive theorems} are properties of datatypes related to
-their coinductive nature.
+\item The \emph{coinductive theorems} (Section~\ref{sssec:coinductive-theorems})
+are properties of datatypes related to their coinductive nature.
\end{itemize}
\noindent
-The first two categories are exactly as for datatypes and are described in
-Sections
-\ref{sssec:free-constructor-theorems}~and~\ref{sssec:functorial-theorems}.
+The first two categories are exactly as for datatypes.
*}
@@ -2717,7 +2725,7 @@
Tobias Nipkow and Makarius Wenzel encouraged us to implement the new
(co)datatype package. Andreas Lochbihler provided lots of comments on earlier
-versions of the package, especially for the coinductive part. Brian Huffman
+versions of the package, especially on the coinductive part. Brian Huffman
suggested major simplifications to the internal constructions, many of which
have yet to be implemented. Florian Haftmann and Christian Urban provided
general advice on Isabelle and package writing. Stefan Milius and Lutz