--- a/src/Doc/Datatypes/Datatypes.thy Wed Sep 11 15:54:53 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Wed Sep 11 16:16:45 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,19 +397,16 @@
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} in the
-declaration above. Although this may look appealing, the mixture of constructors
-and selectors in the resulting characteristic theorems can lead Isabelle's
-automation to switch between the constructor and the destructor view in
-surprising ways.
-*}
+entering ``@{text "="}'' instead of the identifier @{const null}. Although this
+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.
-text {*
The usual mixfix syntaxes are available for both types and constructors. For
example:
*}
@@ -423,6 +422,7 @@
| Cons (hd: 'a) (tl: "'a list") (infixr "#" 65)
text {*
+\noindent
Incidentally, this is how the traditional syntaxes can be set up:
*}
@@ -440,17 +440,17 @@
Datatype definitions have the following general syntax:
@{rail "
- @@{command datatype_new} @{syntax target}? @{syntax dt_options}? \\
+ @@{command_def datatype_new} target? @{syntax dt_options}? \\
(@{syntax dt_name} '=' (@{syntax ctor} + '|') + @'and')
;
@{syntax_def dt_options}: '(' ((@'no_discs_sels' | @'rep_compat') + ',') ')'
"}
-The syntactic quantity @{syntax target} can be used to specify a local context
-(e.g., @{text "(in linorder)"}). It is documented in the Isar reference manual
-\cite{isabelle-isar-ref}.
-
-The optional target is followed by optional options:
+The syntactic quantity \synt{target} can be used to specify a local
+context---e.g., @{text "(in linorder)"}. It is documented in the Isar reference
+manual \cite{isabelle-isar-ref}.
+%
+The optional target is optionally followed by datatype-specific options:
\begin{itemize}
\setlength{\itemsep}{0pt}
@@ -461,28 +461,27 @@
\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
+package should contain optional (and normally not displayed) ``@{text "new."}''
+components to prevent clashes with a later call to \keyw{rep_datatype}. See
Section~\ref{ssec:datatype-compatibility-issues} for details.
\end{itemize}
The left-hand sides of the datatype equations specify the name of the type to
-define, its type parameters, and optional additional information:
+define, its type parameters, and additional information:
@{rail "
- @{syntax_def dt_name}: @{syntax tyargs}? @{syntax name}
- @{syntax map_rel}? @{syntax mixfix}?
+ @{syntax_def dt_name}: @{syntax tyargs}? name @{syntax map_rel}? mixfix?
;
- @{syntax_def tyargs}: @{syntax typefree} | '(' ((@{syntax name} ':')? @{syntax typefree} + ',') ')'
+ @{syntax_def tyargs}: typefree | '(' ((name ':')? typefree + ',') ')'
;
- @{syntax_def map_rel}: '(' ((('map' | 'rel') ':' @{syntax name}) +) ')'
+ @{syntax_def map_rel}: '(' ((('map' | 'rel') ':' name) +) ')'
"}
\noindent
-The syntactic quantity @{syntax name} denotes an identifier, @{syntax typefree}
-denotes fixed type variable (@{typ 'a}, @{typ 'b}, \ldots), and @{syntax
-mixfix} denotes the usual parenthesized mixfix notation. They are documented in
-the Isar reference manual \cite{isabelle-isar-ref}.
+The syntactic quantity \synt{name} denotes an identifier, \synt{typefree}
+denotes fixed type variable (@{typ 'a}, @{typ 'b}, \ldots), and \synt{mixfix}
+denotes the usual parenthesized mixfix notation. They are documented in the Isar
+reference manual \cite{isabelle-isar-ref}.
The optional names preceding the type variables allow to override the default
names of the set functions (@{text t_set1}, \ldots, @{text t_setM}).
@@ -490,20 +489,23 @@
specify exactly the same type variables in the same order.
@{rail "
- @{syntax_def ctor}: (@{syntax name} ':')? @{syntax name} (@{syntax ctor_arg} * ) \\
- @{syntax dt_sel_defaults}? @{syntax mixfix}?
+ @{syntax_def ctor}: (name ':')? name (@{syntax ctor_arg} * ) \\
+ @{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}: @{syntax type} | '(' @{syntax name} ':' @{syntax type} ')'
+ @{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
@@ -511,7 +513,7 @@
constructors as long as they have the same type.
@{rail "
- @{syntax_def dt_sel_defaults}: '(' @'defaults' (@{syntax name} ':' @{syntax term} +) ')'
+ @{syntax_def dt_sel_defaults}: '(' @'defaults' (name ':' term +) ')'
"}
\noindent
@@ -519,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
*}
@@ -587,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?
*}
@@ -811,10 +846,10 @@
Primitive recursive functions have the following general syntax:
@{rail "
- @@{command primrec_new} @{syntax target}? @{syntax \"fixes\"} \\ @'where'
+ @@{command_def primrec_new} target? fixes \\ @'where'
(@{syntax primrec_equation} + '|')
;
- @{syntax_def primrec_equation}: @{syntax thmdecl}? @{syntax prop}
+ @{syntax_def primrec_equation}: thmdecl? prop
"}
*}
@@ -856,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
@@ -941,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)
@@ -966,11 +1002,10 @@
Primitive corecursive definitions have the following general syntax:
@{rail "
- @@{command primcorec} @{syntax target}? @{syntax \"fixes\"} \\ @'where'
+ @@{command_def primcorec} target? fixes \\ @'where'
(@{syntax primcorec_formula} + '|')
;
- @{syntax_def primcorec_formula}: @{syntax thmdecl}? @{syntax prop}
- (@'of' (@{syntax term} * ))?
+ @{syntax_def primcorec_formula}: thmdecl? prop (@'of' (term * ))?
"}
*}
@@ -1011,10 +1046,10 @@
text {*
@{rail "
- @@{command bnf} @{syntax target}? (@{syntax name} ':')? @{syntax term} \\
- @{syntax term_list} @{syntax term} @{syntax term_list} @{syntax term}?
+ @@{command_def bnf} target? (name ':')? term \\
+ term_list term term_list term?
;
- @{syntax_def X_list}: '[' (@{syntax X} + ',') ']'
+ X_list: '[' (X + ',') ']'
"}
options: no_discs_sels rep_compat
@@ -1031,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}
@@ -1050,12 +1085,12 @@
Free constructor wrapping has the following general syntax:
@{rail "
- @@{command wrap_free_constructors} @{syntax target}? @{syntax dt_options} \\
- @{syntax term_list} @{syntax name} @{syntax fc_discs_sels}?
+ @@{command_def wrap_free_constructors} target? @{syntax dt_options} \\
+ term_list name @{syntax fc_discs_sels}?
;
- @{syntax_def fc_discs_sels}: @{syntax name_list} (@{syntax name_list_list} @{syntax name_term_list_list}? )?
+ @{syntax_def fc_discs_sels}: name_list (name_list_list name_term_list_list? )?
;
- @{syntax_def name_term}: (@{syntax name} ':' @{syntax term})
+ @{syntax_def name_term}: (name ':' term)
"}
options: no_discs_sels rep_compat