--- a/src/Doc/Datatypes/Datatypes.thy Wed Sep 11 15:22:43 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Wed Sep 11 15:49:39 2013 +0200
@@ -17,7 +17,7 @@
generated 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}, documented in the Isar reference manual
-\cite{isabelle-isar-ref}; indeed, replacing the keyword @{command datatype} by
+\cite{isabelle-isar-ref}; indeed, replacing the keyword \keyw{datatype} by
@{command datatype_new} is usually all that is needed to port existing theories
to use the new package.
@@ -106,14 +106,14 @@
\item Section \ref{sec:defining-recursive-functions}, ``Defining Recursive
Functions,'' describes how to specify recursive functions using
-\keyw{primrec\_new}, @{command fun}, and @{command function}.
+@{command primrec_new}, \keyw{fun}, and \keyw{function}.
\item Section \ref{sec:defining-codatatypes}, ``Defining Codatatypes,''
describes how to specify codatatypes using the @{command codatatype} command.
\item Section \ref{sec:defining-corecursive-functions}, ``Defining Corecursive
Functions,'' describes how to specify corecursive functions using the
-\keyw{primcorec} command.
+@{command primcorec} command.
\item Section \ref{sec:registering-bounded-natural-functors}, ``Registering
Bounded Natural Functors,'' explains how to set up the package to allow nested
@@ -149,8 +149,8 @@
in.\allowbreak tum.\allowbreak de}}
The commands @{command datatype_new} and @{command primrec_new} are expected to
-displace @{command datatype} and @{command primrec} in a future release. Authors
-of new theories are encouraged to use the new commands, and maintainers of older
+displace \keyw{datatype} and \keyw{primrec} in a future release. Authors of new
+theories are encouraged to use the new commands, and maintainers of older
theories may want to consider upgrading.
Comments and bug reports concerning either the tool or this tutorial should be
@@ -171,10 +171,10 @@
\label{sec:defining-datatypes} *}
text {*
-This section describes how to specify datatypes using the @{command datatype_new}
-command. The command is first illustrated through concrete examples featuring
-different flavors of recursion. More examples can be found in the directory
-\verb|~~/src/HOL/BNF/Examples|.
+This section describes how to specify datatypes using the @{command
+datatype_new} command. The command is first illustrated through concrete
+examples featuring different flavors of recursion. More examples can be found in
+the directory \verb|~~/src/HOL/BNF/Examples|.
*}
@@ -343,6 +343,8 @@
\item \relax{Relator}: @{text t_rel}
+\item \relax{Case combinator}: @{text t_case}
+
\item \relax{Iterator}: @{text t_fold}
\item \relax{Recursor}: @{text t_rec}
@@ -395,13 +397,13 @@
The @{text "defaults"} keyword following the @{const Nil} constructor specifies
a default value for selectors associated with other constructors. Here, it is
-used to ensure that the tail of the empty list is the empty list (instead of
-being left unspecified).
+used to ensure that the tail of the empty list is itself (instead of being left
+unspecified).
Because @{const Nil} is a nullary constructor, it is also possible to use
@{term "\<lambda>xs. xs = Nil"} as a discriminator. This is specified by
entering ``@{text "="}'' instead of the identifier @{const null}. Although this
-may look appealing, the mixture of constructors and selectors in the resulting
+may look appealing, the mixture of constructors and selectors in the
characteristic theorems can lead Isabelle's automation to switch between the
constructor and the destructor view in surprising ways.
@@ -420,6 +422,7 @@
| Cons (hd: 'a) (tl: "'a list") (infixr "#" 65)
text {*
+\noindent
Incidentally, this is how the traditional syntaxes can be set up:
*}
@@ -459,7 +462,7 @@
\item
The \keyw{rep\_compat} option indicates that the names generated by the
package should contain optional (and normally not displayed) ``@{text "new."}''
-components to prevent clashes with a later call to @{command rep_datatype}. See
+components to prevent clashes with a later call to \keyw{rep_datatype}. See
Section~\ref{ssec:datatype-compatibility-issues} for details.
\end{itemize}
@@ -490,16 +493,19 @@
@{syntax dt_sel_defaults}? mixfix?
"}
+\medskip
+
\noindent
The main constituents of a constructor specification is the name of the
constructor and the list of its argument types. An optional discriminator name
-can be supplied at the front to override the default name
-(@{text t.un_C}$_{ij}$).
+can be supplied at the front to override the default name (@{text t.un_Cji}).
@{rail "
@{syntax_def ctor_arg}: type | '(' name ':' type ')'
"}
+\medskip
+
\noindent
In addition to the type of a constructor argument, it is possible to specify a
name for the corresponding selector to override the default name
@@ -515,28 +521,61 @@
@{text "C \<Colon> \<sigma>\<^sub>1 \<Rightarrow> \<dots> \<Rightarrow> \<sigma>\<^sub>p \<Rightarrow> \<sigma>"},
default values can be specified for any selector
@{text "un_D \<Colon> \<sigma> \<Rightarrow> \<tau>"}
-associated with other constructors. The specified default value must have type
+associated with other constructors. The specified default value must be of type
@{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<Rightarrow> \<sigma>\<^sub>p \<Rightarrow> \<tau>"}
-(i.e., it may dependend on @{text C}'s arguments).
+(i.e., it may depends on @{text C}'s arguments).
*}
subsection {* Generated Theorems
\label{ssec:datatype-generated-theorems} *}
text {*
+The characteristic theorems generated by @{command datatype_new} are
+grouped in three broad categories:
+
+\begin{enumerate}
+\item The free constructor theorems are properties about the constructors and
+destructors that can be derived for any freely generated type. In particular,
+@{command codatatype} also produces these theorems.
+
+\item The per-datatype theorems are properties connected to individual datatypes
+and that rely on their inductive nature.
+
+\item The mutual datatype theorems are properties of mutually recursive groups
+of datatypes.
+\end{enumerate}
+
+\noindent
+The list of available \keyw{print_theorem}
+
+bnf_note_all
+*}
+
+
+subsubsection {* Free Constructor Theorems *}
+
+text {*
* free ctor theorems
* case syntax
- * per-type theorems
+ * Section~\label{sec:generating-free-constructor-theorems}
+*}
+
+
+subsubsection {* Per-Datatype Theorems *}
+
+text {*
* sets, map, rel
* induct, fold, rec
* simps
+*}
+
+subsubsection {* Mutual Datatype Theorems *}
+
+text {*
* multi-type (``common'') theorems
* induct
-
- * mention what is registered with which attribute
- * and also nameless safes
*}
@@ -583,11 +622,11 @@
\label{sec:defining-recursive-functions} *}
text {*
-This describes how to specify recursive functions over datatypes
-specified using @{command datatype_new}. The focus in on the \keyw{primrec\_new}
-command, which supports primitive recursion. A few examples feature the
-@{command fun} and @{command function} commands, described in a separate
-tutorial \cite{isabelle-function}.
+This describes how to specify recursive functions over datatypes specified using
+@{command datatype_new}. The focus in on the @{command primrec_new} command,
+which supports primitive recursion. A few examples feature the \keyw{fun} and
+\keyw{function} commands, described in a separate tutorial
+\cite{isabelle-function}.
%%% TODO: partial_function?
*}
@@ -807,7 +846,7 @@
Primitive recursive functions have the following general syntax:
@{rail "
- @@{command primrec_new} target? fixes \\ @'where'
+ @@{command_def primrec_new} target? fixes \\ @'where'
(@{syntax primrec_equation} + '|')
;
@{syntax_def primrec_equation}: thmdecl? prop
@@ -852,11 +891,12 @@
@{keyword consts}.
\item
-Define the datatype, specifying @{text "un_D\<^sub>0"} as the selector's default value.
+Define the datatype, specifying @{text "un_D\<^sub>0"} as the selector's default
+value.
\item
-Define the behavior of @{text "un_D\<^sub>0"} on values of the newly introduced datatype
-using the @{command overloading} command.
+Define the behavior of @{text "un_D\<^sub>0"} on values of the newly introduced
+datatype using the \keyw{overloading} command.
\item
Derive the desired equation on @{text un_D} from the characteristic equations
@@ -937,7 +977,7 @@
text {*
This section describes how to specify corecursive functions using the
-\keyw{primcorec} command.
+@{command primcorec} command.
%%% TODO: partial_function? E.g. for defining tail recursive function on lazy
%%% lists (cf. terminal0 in TLList.thy)
@@ -962,7 +1002,7 @@
Primitive corecursive definitions have the following general syntax:
@{rail "
- @@{command primcorec} target? fixes \\ @'where'
+ @@{command_def primcorec} target? fixes \\ @'where'
(@{syntax primcorec_formula} + '|')
;
@{syntax_def primcorec_formula}: thmdecl? prop (@'of' (term * ))?
@@ -1006,7 +1046,7 @@
text {*
@{rail "
- @@{command bnf} target? (name ':')? term \\
+ @@{command_def bnf} target? (name ':')? term \\
term_list term term_list term?
;
X_list: '[' (X + ',') ']'
@@ -1026,7 +1066,7 @@
a type not introduced by ...
* also useful for compatibility with old package, e.g. add destructors to
- old @{command datatype}
+ old \keyw{datatype}
* @{command wrap_free_constructors}
* \keyw{no\_discs\_sels}, \keyw{rep\_compat}
@@ -1045,7 +1085,7 @@
Free constructor wrapping has the following general syntax:
@{rail "
- @@{command wrap_free_constructors} target? @{syntax dt_options} \\
+ @@{command_def wrap_free_constructors} target? @{syntax dt_options} \\
term_list name @{syntax fc_discs_sels}?
;
@{syntax_def fc_discs_sels}: name_list (name_list_list name_term_list_list? )?