more (co)datatype docs
authorblanchet
Thu Aug 01 14:22:10 2013 +0200 (2013-08-01)
changeset 52822ae938ac9a721
parent 52821 05eb2d77b195
child 52823 0d2778860da4
more (co)datatype docs
src/Doc/Datatypes/Datatypes.thy
src/Doc/Datatypes/Setup.thy
src/Doc/Datatypes/document/root.tex
src/Doc/ROOT
     1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Thu Aug 01 00:18:45 2013 +0200
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Thu Aug 01 14:22:10 2013 +0200
     1.3 @@ -5,16 +5,17 @@
     1.4  *)
     1.5  
     1.6  theory Datatypes
     1.7 -imports BNF
     1.8 +imports Setup BNF
     1.9  begin
    1.10  
    1.11 +
    1.12  section {* Introduction *}
    1.13  
    1.14  text {*
    1.15  The 2013 edition of Isabelle introduced new definitional package for datatypes
    1.16  and codatatypes. The datatype support is similar to that provided by the earlier
    1.17  package due to Berghofer and Wenzel \cite{Berghofer-Wenzel:1999:TPHOL};
    1.18 -indeed, replacing \cmd{datatype} by \cmd{datatype\_new} is usually sufficient
    1.19 +indeed, replacing @{command datatype} by @{command datatype_new} is usually sufficient
    1.20  to port existing specifications to the new package. What makes the new package
    1.21  attractive is that it supports definitions with recursion through a large class
    1.22  of non-datatypes, notably finite sets:
    1.23 @@ -35,21 +36,10 @@
    1.24  text {*
    1.25  \noindent
    1.26  Finally, the package also provides some convenience, notably automatically
    1.27 -generated destructors. For example, the command
    1.28 -*}
    1.29 -
    1.30 -(*<*)hide_const Nil Cons hd tl(*>*)
    1.31 -    datatype_new 'a list = null: Nil | Cons (hd: 'a) (tl: "'a list")
    1.32 +generated destructors.
    1.33  
    1.34 -text {*
    1.35 -\noindent
    1.36 -introduces a discriminator @{const null} and a pair of selectors @{const hd} and
    1.37 -@{const tl} characterized as follows:
    1.38 -%
    1.39 -\[@{thm list.collapse(1)[no_vars]}\qquad @{thm list.collapse(2)[no_vars]}\]
    1.40 -
    1.41 -The command \cmd{datatype\_new} is expected to displace \cmd{datatype} in a future
    1.42 -release. Authors of new theories are encouraged to use \cmd{datatype\_new}, and
    1.43 +The command @{command datatype_new} is expected to displace @{command datatype} in a future
    1.44 +release. Authors of new theories are encouraged to use @{command datatype_new}, and
    1.45  maintainers of older theories may want to consider upgrading in the coming months.
    1.46  
    1.47  The package also provides codatatypes (or ``coinductive datatypes''), which may
    1.48 @@ -98,15 +88,17 @@
    1.49  This tutorial is organized as follows:
    1.50  
    1.51  \begin{itemize}
    1.52 +\setlength{\itemsep}{0pt}
    1.53 +
    1.54  \item Section \ref{sec:defining-datatypes}, ``Defining Datatypes,''
    1.55 -describes how to specify datatypes using the \cmd{datatype\_new} command.
    1.56 +describes how to specify datatypes using the @{command datatype_new} command.
    1.57  
    1.58  \item Section \ref{sec:defining-recursive-functions}, ``Defining Recursive 
    1.59  Functions,'' describes how to specify recursive functions using
    1.60 -\cmd{primrec\_new}, \cmd{fun}, and \cmd{function}.
    1.61 +\cmd{primrec\_new}, @{command fun}, and @{command function}.
    1.62  
    1.63  \item Section \ref{sec:defining-codatatypes}, ``Defining Codatatypes,''
    1.64 -describes how to specify codatatypes using the \cmd{codatatype} command.
    1.65 +describes how to specify codatatypes using the @{command codatatype} command.
    1.66  
    1.67  \item Section \ref{sec:defining-corecursive-functions}, ``Defining Corecursive 
    1.68  Functions,'' describes how to specify corecursive functions using the
    1.69 @@ -118,8 +110,8 @@
    1.70  
    1.71  \item Section \ref{sec:generating-free-constructor-theorems}, ``Generating Free 
    1.72  Constructor Theorems,'' explains how to derive convenience theorems for free
    1.73 -constructors, as performed internally by \cmd{datatype\_new} and
    1.74 -\cmd{codatatype}.
    1.75 +constructors, as performed internally by @{command datatype_new} and
    1.76 +@{command codatatype}.
    1.77  
    1.78  \item Section \ref{sec:standard-ml-interface}, ``Standard ML Interface,''
    1.79  describes the package's programmatic interface.
    1.80 @@ -129,19 +121,41 @@
    1.81  tools, such as the code generator and the counterexample generators.
    1.82  
    1.83  \item Section \ref{sec:known-bugs-and-limitations}, ``Known Bugs and 
    1.84 -Limitations,'' concludes with open issues.
    1.85 +Limitations,'' concludes with known open issues at the time of writing.
    1.86  \end{itemize}
    1.87 +
    1.88 +
    1.89 +\newbox\boxA
    1.90 +\setbox\boxA=\hbox{\texttt{nospam}}
    1.91 +
    1.92 +\newcommand\authoremaili{\texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@\allowbreak
    1.93 +in.\allowbreak tum.\allowbreak de}}
    1.94 +\newcommand\authoremailii{\texttt{pope{\color{white}nospam}\kern-\wd\boxA{}scua@\allowbreak
    1.95 +in.\allowbreak tum.\allowbreak de}}
    1.96 +\newcommand\authoremailiii{\texttt{tray{\color{white}nospam}\kern-\wd\boxA{}tel@\allowbreak
    1.97 +in.\allowbreak tum.\allowbreak de}}
    1.98 +
    1.99 +\noindent
   1.100 +Comments and bug reports concerning either
   1.101 +the tool or the manual should be directed to the authors at
   1.102 +\authoremaili, \authoremailii, and \authoremailiii.
   1.103 +
   1.104 +\begin{framed}
   1.105 +\noindent
   1.106 +\textbf{Warning:} This document is under heavy construction. Please apologise
   1.107 +for its appearance and come back in a few months.
   1.108 +\end{framed}
   1.109 +
   1.110  *}
   1.111  
   1.112  section {* Defining Datatypes%
   1.113    \label{sec:defining-datatypes} *}
   1.114  
   1.115  text {*
   1.116 -This section describes how to specify datatypes using the \cmd{datatype\_new}
   1.117 +This section describes how to specify datatypes using the @{command datatype_new}
   1.118  command. The command is first illustrated through concrete examples featuring
   1.119 -different flavors of recursion. More examples are available in
   1.120 -\verb|~~/src/HOL/BNF/Examples|. The syntax is largely modeled after that of the
   1.121 -existing \cmd{datatype} command.
   1.122 +different flavors of recursion. More examples can be found in the directory
   1.123 +\verb|~~/src/HOL/BNF/Examples|.
   1.124  *}
   1.125  
   1.126  subsection {* Introductory Examples *}
   1.127 @@ -245,12 +259,152 @@
   1.128  subsubsection {* Auxiliary Constants and Syntaxes *}
   1.129  
   1.130  text {*
   1.131 -* destructors
   1.132 -* also mention special syntaxes
   1.133 +The @{command datatype_new} command introduces various constants in addition to the
   1.134 +constructors. Given a type @{text "('a1,\<dots>,'aM) t"} with constructors
   1.135 +@{text t.C1}, \ldots, @{text t.C}$\!M,$ the following auxiliary constants are
   1.136 +introduced (among others):
   1.137 +
   1.138 +\begin{itemize}
   1.139 +\setlength{\itemsep}{0pt}
   1.140 +
   1.141 +\item \emph{Set functions} (\emph{natural transformations}): @{text t_set1},
   1.142 +\ldots, @{text t_set}$M$
   1.143 +
   1.144 +\item \emph{Map function} (\emph{functorial action}): @{text t_map}
   1.145 +
   1.146 +\item \emph{Relator}: @{text t_rel}
   1.147 +
   1.148 +\item \emph{Iterator}: @{text t_fold}
   1.149 +
   1.150 +\item \emph{Recursor}: @{text t_rec}
   1.151 +
   1.152 +\item \emph{Discriminators}: @{text t.is_C1}, \ldots, @{text t.is_C}$\!M$
   1.153 +
   1.154 +\item \emph{Selectors}:
   1.155 +@{text t.un_C11}, \ldots, @{text t.un_C1}$k_1$, \ldots,
   1.156 +@{text t.un_C}$\!M$@{text 1}, \ldots, @{text t.un_C}$\!Mk_M$
   1.157 +\end{itemize}
   1.158 +
   1.159 +The discriminators and selectors are collectively called \emph{destructors}.
   1.160 +The @{text "t."} prefix is optional.
   1.161 +
   1.162 +The set functions, map function, relator, discriminators, and selectors can be
   1.163 +given custom names, as in the example below:
   1.164 +*}
   1.165 +
   1.166 +(*<*)hide_const Nil Cons hd tl(*>*)
   1.167 +    datatype_new (set: 'a) list (map: map rel: list_all2) =
   1.168 +      null: Nil (defaults tl: Nil)
   1.169 +    | Cons (hd: 'a) (tl: "'a list")
   1.170 +
   1.171 +text {*
   1.172 +\noindent
   1.173 +The command introduces a discriminator @{const null} and a pair of selectors
   1.174 +@{const hd} and @{const tl} characterized as follows:
   1.175 +%
   1.176 +\[@{thm list.collapse(1)[of xs, no_vars]}
   1.177 +  \qquad @{thm list.collapse(2)[of xs, no_vars]}\]
   1.178 +%
   1.179 +For two-constructor datatypes, a single discriminator constant suffices. The
   1.180 +discriminator associated with @{const Cons} is simply @{text "\<not> null"}.
   1.181 +
   1.182 +The \cmd{defaults} keyword following the @{const Nil} constructor specifies a
   1.183 +default value for selectors associated with other constructors. Here, it is
   1.184 +used to specify that the tail of the empty list is the empty list (instead of
   1.185 +being unspecified).
   1.186 +
   1.187 +Because @{const Nil} is a nullary constructor, it is also possible to use @{text
   1.188 +"= Nil"} as a discriminator. This is specified by specifying @{text "="} instead
   1.189 +of the identifier @{const null} in the declaration above. Although this may look
   1.190 +appealing, the mixture of constructors and selectors in the resulting
   1.191 +characteristic theorems can lead Isabelle's automation to switch between the
   1.192 +constructor and the destructor view in surprising ways.
   1.193 +*}
   1.194 +
   1.195 +text {*
   1.196 +The usual mixfix syntaxes are available for both types and constructors. For example:
   1.197 +
   1.198 +%%% FIXME: remove trailing underscore and use locale trick instead once this is
   1.199 +%%% supported.
   1.200  *}
   1.201  
   1.202 +    datatype_new ('a, 'b) prod (infixr "*" 20) =
   1.203 +      Pair 'a 'b
   1.204 +
   1.205 +    datatype_new (set_: 'a) list_ =
   1.206 +      null: Nil ("[]")
   1.207 +    | Cons (hd: 'a) (tl: "'a list_") (infixr "#" 65)
   1.208 +
   1.209  subsection {* General Syntax *}
   1.210  
   1.211 +text {*
   1.212 +Datatype definitions have the following general syntax:
   1.213 +
   1.214 +@{rail
   1.215 +  "@@{command datatype_new} @{syntax flags}?"
   1.216 + }
   1.217 +
   1.218 +\noindent
   1.219 +\ \ \ \ @{command datatype_new} [<flags>] @{text "\<langle>lhs\<rangle>"} @{text "="} @{text "\<langle>rhs\<rangle>"} \\
   1.220 +\noindent
   1.221 +\ \ \ \ \cmd{and} @{text "\<langle>lhs\<rangle>"} @{text "="} @{text "\<langle>rhs\<rangle>"} \\
   1.222 +\noindent
   1.223 +\ \ \ \ \quad$\vdots$ \\
   1.224 +\noindent
   1.225 +\ \ \ \ \cmd{and} @{text "\<langle>lhs\<rangle>"} @{text "="} @{text "\<langle>rhs\<rangle>"}
   1.226 +
   1.227 +<flags> ::= (<flag>, ..., <flag>) \\
   1.228 +<flag> ::= no_dests | rep_compat
   1.229 +
   1.230 +Left-hand sides:
   1.231 +
   1.232 +<lhs> ::= [<type_params>] <name> [<map_rel>] [<mixfix>] \\
   1.233 +
   1.234 +<name> specifies the type name
   1.235 +
   1.236 +<type_params> ::= ([<name>:] <type_var>, \ldots, [<name>:] <type_var>)
   1.237 +<type_params> ::= <type_var> \\
   1.238 +
   1.239 +The names are for the set functions.
   1.240 +
   1.241 +<type_var> is type variable ('a, 'b, \ldots)
   1.242 +
   1.243 +<map_rel> ::= ([map: <map_name>] [rel: <rel_name>])
   1.244 +
   1.245 +<mixfix> is the usual parenthesized mixfix notation
   1.246 +
   1.247 +Additional constraint: All mutually recursive datatypes defined together must
   1.248 +specify the same type variables in the same order.
   1.249 +
   1.250 +<rhs> ::= <ctor> | ... | <ctor>
   1.251 +
   1.252 +<ctor> :: [<name>:] <name> <ctor_arg> [<defaults>] [<mixfix>]
   1.253 +
   1.254 +First, optional name: discriminator. Second, mandatory name: name of
   1.255 +constructor. Default names for discriminators are generated.
   1.256 +
   1.257 +<ctor_arg> ::= ([<name>:] <type>) \\
   1.258 +<ctor_arg> ::= <type>
   1.259 +
   1.260 +<defaults> ::= defaults (<name>: <term>)*
   1.261 +
   1.262 +\noindent
   1.263 +Each left-hand side @{text "\<langle>lhsJ\<rangle>"} is of the form
   1.264 +
   1.265 +\noindent
   1.266 +
   1.267 +'a
   1.268 +([set1:] 'a1, ..., [setM:] 'aN)
   1.269 +
   1.270 +
   1.271 +Each right-hand side @{text "\<langle>rhsJ\<rangle>"} is of the form
   1.272 +
   1.273 +\ \ \ \ \cmd{and} (@{text 'a1}, \ldots, @{text 'aM}) @{text t1} @{text "="} @{text "\<langle>rhs1\<rangle>"}
   1.274 +
   1.275 +(@{text 'a1}, \ldots, @{text 'aM}) @{text t1}
   1.276 +*}
   1.277 +
   1.278 +
   1.279  subsection {* Characteristic Theorems *}
   1.280  
   1.281  subsection {* Compatibility Issues *}
   1.282 @@ -261,10 +415,10 @@
   1.283  
   1.284  text {*
   1.285  This describes how to specify recursive functions over datatypes
   1.286 -specified using \cmd{datatype\_new}. The focus in on the \cmd{primrec\_new}
   1.287 +specified using @{command datatype_new}. The focus in on the \cmd{primrec\_new}
   1.288  command, which supports primitive recursion. A few examples feature the
   1.289 -\cmd{fun} and \cmd{function} commands, described in a separate tutorial  
   1.290 -\cite{isabelle-function}.
   1.291 +@{command fun} and @{command function} commands, described in a separate
   1.292 +tutorial \cite{isabelle-function}.
   1.293  %%% TODO: partial_function?
   1.294  *}
   1.295  
   1.296 @@ -285,7 +439,7 @@
   1.297    \label{sec:defining-codatatypes} *}
   1.298  
   1.299  text {*
   1.300 -This section describes how to specify codatatypes using the \cmd{codatatype}
   1.301 +This section describes how to specify codatatypes using the @{command codatatype}
   1.302  command.
   1.303  *}
   1.304  
   1.305 @@ -346,13 +500,13 @@
   1.306  
   1.307  text {*
   1.308  This section explains how to derive convenience theorems for free constructors,
   1.309 -as performed internally by \cmd{datatype\_new} and \cmd{codatatype}.
   1.310 +as performed internally by @{command datatype_new} and @{command codatatype}.
   1.311  
   1.312    * need for this is rare but may arise if you want e.g. to add destructors to
   1.313      a type not introduced by ...
   1.314  
   1.315    * also useful for compatibility with old package, e.g. add destructors to
   1.316 -    old \cmd{datatype}
   1.317 +    old @{command datatype}
   1.318  *}
   1.319  
   1.320  subsection {* Introductory Example *}
   1.321 @@ -405,6 +559,19 @@
   1.322  * partial documentation
   1.323  
   1.324  * too much output by commands like "datatype_new" and "codatatype"
   1.325 +
   1.326 +* no direct way to define recursive functions for default values -- but show trick
   1.327 +  based on overloading
   1.328 +*}
   1.329 +
   1.330 +
   1.331 +section {* Acknowledgments%
   1.332 +  \label{sec:acknowledgments} *}
   1.333 +
   1.334 +text {*
   1.335 +  * same people as usual
   1.336 +    * Brian Huffman
   1.337 +  * Lutz Schr\"oder and Stefan Milius 
   1.338  *}
   1.339  
   1.340  end
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Doc/Datatypes/Setup.thy	Thu Aug 01 14:22:10 2013 +0200
     2.3 @@ -0,0 +1,9 @@
     2.4 +theory Setup
     2.5 +imports Main
     2.6 +begin
     2.7 +
     2.8 +ML_file "../antiquote_setup.ML"
     2.9 +
    2.10 +setup Antiquote_Setup.setup
    2.11 +
    2.12 +end
     3.1 --- a/src/Doc/Datatypes/document/root.tex	Thu Aug 01 00:18:45 2013 +0200
     3.2 +++ b/src/Doc/Datatypes/document/root.tex	Thu Aug 01 14:22:10 2013 +0200
     3.3 @@ -10,6 +10,8 @@
     3.4  \usepackage{isabellesym}
     3.5  \usepackage{style}
     3.6  \usepackage{pdfsetup}
     3.7 +\usepackage{railsetup}
     3.8 +\usepackage{framed}
     3.9  
    3.10  \newbox\boxA
    3.11  \setbox\boxA=\hbox{\ }
    3.12 @@ -17,7 +19,7 @@
    3.13  
    3.14  \newcommand{\cmd}[1]{\isacommand{#1}}
    3.15  
    3.16 -\def\isacharprime{\isamath{{'}\mskip-2mu}}
    3.17 +\renewcommand{\isacharprime}{\isamath{{'}\mskip-2mu}}
    3.18  \renewcommand{\isacharunderscore}{\mbox{\_}}
    3.19  \renewcommand{\isacharunderscorekeyword}{\mbox{\_}}
    3.20  \renewcommand{\isachardoublequote}{\mbox{\upshape{``}}}
     4.1 --- a/src/Doc/ROOT	Thu Aug 01 00:18:45 2013 +0200
     4.2 +++ b/src/Doc/ROOT	Thu Aug 01 14:22:10 2013 +0200
     4.3 @@ -39,6 +39,7 @@
     4.4  
     4.5  session Datatypes (doc) in "Datatypes" = "HOL-BNF" +
     4.6    options [document_variants = "datatypes"]
     4.7 +  theories [document = false] Setup
     4.8    theories Datatypes
     4.9    files
    4.10      "../prepare_document"