--- a/src/Doc/Datatypes/Datatypes.thy Thu Aug 01 14:22:21 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Thu Aug 01 15:50:16 2013 +0200
@@ -5,10 +5,9 @@
*)
theory Datatypes
-imports Setup BNF
+imports Setup
begin
-
section {* Introduction *}
text {*
@@ -95,14 +94,14 @@
\item Section \ref{sec:defining-recursive-functions}, ``Defining Recursive
Functions,'' describes how to specify recursive functions using
-\cmd{primrec\_new}, @{command fun}, and @{command function}.
+\keyw{primrec\_new}, @{command fun}, and @{command 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
-\cmd{primcorec} command.
+\keyw{primcorec} command.
\item Section \ref{sec:registering-bounded-natural-functors}, ``Registering
Bounded Natural Functors,'' explains how to set up the (co)datatype package to
@@ -158,6 +157,7 @@
\verb|~~/src/HOL/BNF/Examples|.
*}
+
subsection {* Introductory Examples *}
subsubsection {* Nonrecursive Types *}
@@ -180,6 +180,7 @@
datatype_new ('a, 'b, 'c) triple = Triple 'a 'b 'c
+
subsubsection {* Simple Recursion *}
text {*
@@ -201,6 +202,7 @@
Nonatomic types must be enclosed in double quotes.
*}
+
subsubsection {* Mutual Recursion *}
text {*
@@ -223,6 +225,7 @@
and ('a, 'b) factor =
Const 'a | Var 'b | Sub_Expr "('a, 'b) expr"
+
subsubsection {* Nested Recursion *}
text {*
@@ -308,7 +311,7 @@
For two-constructor datatypes, a single discriminator constant suffices. The
discriminator associated with @{const Cons} is simply @{text "\<not> null"}.
-The \cmd{defaults} keyword following the @{const Nil} constructor specifies a
+The \keyw{defaults} keyword following the @{const Nil} constructor specifies a
default value for selectors associated with other constructors. Here, it is
used to specify that the tail of the empty list is the empty list (instead of
being unspecified).
@@ -335,79 +338,82 @@
null: Nil ("[]")
| Cons (hd: 'a) (tl: "'a list_") (infixr "#" 65)
+
subsection {* General Syntax *}
text {*
Datatype definitions have the following general syntax:
-@{rail
- "@@{command datatype_new} @{syntax flags}?"
- }
+@{rail "
+ @@{command datatype_new} ('(' (@{syntax dt_option} + ',') ')')? \\
+ (@{syntax dt_name} '=' (@{syntax ctor} + '|') + @'and')
+"}
+
+Two options are supported:
-\noindent
-\ \ \ \ @{command datatype_new} [<flags>] @{text "\<langle>lhs\<rangle>"} @{text "="} @{text "\<langle>rhs\<rangle>"} \\
-\noindent
-\ \ \ \ \cmd{and} @{text "\<langle>lhs\<rangle>"} @{text "="} @{text "\<langle>rhs\<rangle>"} \\
-\noindent
-\ \ \ \ \quad$\vdots$ \\
-\noindent
-\ \ \ \ \cmd{and} @{text "\<langle>lhs\<rangle>"} @{text "="} @{text "\<langle>rhs\<rangle>"}
+@{rail "
+ @{syntax_def dt_option}: @'no_dests' | @'rep_compat'
+"}
-<flags> ::= (<flag>, ..., <flag>) \\
-<flag> ::= no_dests | rep_compat
+\begin{itemize}
+\setlength{\itemsep}{0pt}
+
+\item
+The \keyw{no\_dests} option indicates that no destructors (i.e.,
+discriminators and selectors) should be generated.
-Left-hand sides:
+\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
+Section~\ref{ssec:datatype-compatibility-issues} for details.
+\end{itemize}
-<lhs> ::= [<type_params>] <name> [<map_rel>] [<mixfix>] \\
-
-<name> specifies the type name
+Left-hand sides specify the name of the type to define, its type parameters,
+and more:
-<type_params> ::= ([<name>:] <type_var>, \ldots, [<name>:] <type_var>)
-<type_params> ::= <type_var> \\
-
-The names are for the set functions.
+@{rail "
+ @{syntax_def dt_name}: @{syntax type_params}? @{syntax name} \\
+ @{syntax map_rel}? @{syntax mixfix}?
+ ;
+ @{syntax_def type_params}: @{syntax typefree} | '(' ((@{syntax name} ':')? @{syntax typefree} + ',') ')'
+ ;
+ @{syntax_def map_rel}: '(' ((('map' | 'rel') ':' @{syntax name}) +) ')'
+"}
-<type_var> is type variable ('a, 'b, \ldots)
+@{syntax name} specifies the type name ...
-<map_rel> ::= ([map: <map_name>] [rel: <rel_name>])
-
-<mixfix> is the usual parenthesized mixfix notation
+@{syntax typefree} is type variable ('a, 'b, \ldots)
+The names are for the set functions.
Additional constraint: All mutually recursive datatypes defined together must
specify the same type variables in the same order.
-<rhs> ::= <ctor> | ... | <ctor>
+@{syntax mixfix} is the usual parenthesized mixfix notation, documented in the
+Isar reference manual \cite{isabelle-isar-ref}.
-<ctor> :: [<name>:] <name> <ctor_arg> [<defaults>] [<mixfix>]
+@{rail "
+ @{syntax_def ctor}: (@{syntax name} ':')? @{syntax name} (@{syntax ctor_arg} *) \\
+ @{syntax sel_defaults}? @{syntax mixfix}?
+"}
+
First, optional name: discriminator. Second, mandatory name: name of
constructor. Default names for discriminators are generated.
-<ctor_arg> ::= ([<name>:] <type>) \\
-<ctor_arg> ::= <type>
-
-<defaults> ::= defaults (<name>: <term>)*
-
-\noindent
-Each left-hand side @{text "\<langle>lhsJ\<rangle>"} is of the form
-
-\noindent
-
-'a
-([set1:] 'a1, ..., [setM:] 'aN)
-
-
-Each right-hand side @{text "\<langle>rhsJ\<rangle>"} is of the form
-
-\ \ \ \ \cmd{and} (@{text 'a1}, \ldots, @{text 'aM}) @{text t1} @{text "="} @{text "\<langle>rhs1\<rangle>"}
-
-(@{text 'a1}, \ldots, @{text 'aM}) @{text t1}
+@{rail "
+ @{syntax_def ctor_arg}: @{syntax type} | '(' (@{syntax name} ':')? @{syntax type} ')'
+ ;
+ @{syntax_def sel_defaults}: '(' @'defaults' (@{syntax name} ':' @{syntax term} *) ')'
+"}
*}
subsection {* Characteristic Theorems *}
-subsection {* Compatibility Issues *}
+
+subsection {* Compatibility Issues%
+ \label{ssec:datatype-compatibility-issues} *}
section {* Defining Recursive Functions%
@@ -415,23 +421,27 @@
text {*
This describes how to specify recursive functions over datatypes
-specified using @{command datatype_new}. The focus in on the \cmd{primrec\_new}
+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}.
%%% TODO: partial_function?
*}
+
subsection {* Introductory Examples *}
text {*
More examples in \verb|~~/src/HOL/BNF/Examples|.
*}
+
subsection {* General Syntax *}
+
subsection {* Characteristic Theorems *}
+
subsection {* Compatibility Issues *}
@@ -443,14 +453,20 @@
command.
*}
+
subsection {* Introductory Examples *}
text {*
More examples in \verb|~~/src/HOL/BNF/Examples|.
*}
+
subsection {* General Syntax *}
+text {*
+\keyw{no\_dests} is not available.
+*}
+
subsection {* Characteristic Theorems *}
@@ -459,17 +475,20 @@
text {*
This section describes how to specify corecursive functions using the
-\cmd{primcorec} command.
+\keyw{primcorec} command.
*}
+
subsection {* Introductory Examples *}
text {*
More examples in \verb|~~/src/HOL/BNF/Examples|.
*}
+
subsection {* General Syntax *}
+
subsection {* Characteristic Theorems *}
@@ -482,6 +501,7 @@
of a bounded natural functor (BNF).
*}
+
subsection {* Introductory Example *}
text {*
@@ -492,6 +512,7 @@
mention =>.
*}
+
subsection {* General Syntax *}
@@ -509,8 +530,10 @@
old @{command datatype}
*}
+
subsection {* Introductory Example *}
+
subsection {* General Syntax *}
@@ -531,14 +554,19 @@
generators.
*}
+
subsection {* Transfer and Lifting *}
+
subsection {* Code Generator *}
+
subsection {* Quickcheck *}
+
subsection {* Nitpick *}
+
subsection {* Nominal Isabelle *}
@@ -570,8 +598,13 @@
text {*
* same people as usual
+ * Tobias Nipkow
+ * Makarius Wenzel
+ * Andreas Lochbihler
* Brian Huffman
- * Lutz Schr\"oder and Stefan Milius
+ * also:
+ * Stefan Milius
+ * Lutz Schr\"oder
*}
end
--- a/src/Doc/Datatypes/document/root.tex Thu Aug 01 14:22:21 2013 +0200
+++ b/src/Doc/Datatypes/document/root.tex Thu Aug 01 15:50:16 2013 +0200
@@ -17,7 +17,7 @@
\setbox\boxA=\hbox{\ }
\parindent=4\wd\boxA
-\newcommand{\cmd}[1]{\isacommand{#1}}
+\newcommand{\keyw}[1]{\isacommand{#1}}
\renewcommand{\isacharprime}{\isamath{{'}\mskip-2mu}}
\renewcommand{\isacharunderscore}{\mbox{\_}}
@@ -46,8 +46,8 @@
\noindent
This tutorial describes how to use the new package for defining datatypes and
codatatypes in Isabelle/HOL. The package provides four main user-level commands:
-\cmd{datatype\_new}, \cmd{codatatype}, \cmd{primrec\_new}, and \cmd{primcorec}.
-The commands suffixed by \cmd{\_new} are intended to subsume, and eventually
+\keyw{datatype\_new}, \keyw{codatatype}, \keyw{primrec\_new}, and \keyw{primcorec}.
+The commands suffixed by \keyw{\_new} are intended to subsume, and eventually
replace, the corresponding commands from the old datatype package.
\end{abstract}