updated BNF docs
authorblanchet
Wed Apr 23 10:23:27 2014 +0200 (2014-04-23)
changeset 5665534f2fe40dc7b
parent 56654 54326fa7afe6
child 56656 7f9b686bf30a
updated BNF docs
src/Doc/Datatypes/Datatypes.thy
     1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Wed Apr 23 10:23:27 2014 +0200
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Wed Apr 23 10:23:27 2014 +0200
     1.3 @@ -103,7 +103,7 @@
     1.4  
     1.5  \item Section \ref{sec:defining-recursive-functions}, ``Defining Recursive
     1.6  Functions,'' describes how to specify recursive functions using
     1.7 -@{command primrec}, \keyw{fun}, and \keyw{function}.
     1.8 +@{command primrec}.
     1.9  
    1.10  \item Section \ref{sec:defining-codatatypes}, ``Defining Codatatypes,''
    1.11  describes how to specify codatatypes using the @{command codatatype} command.
    1.12 @@ -599,17 +599,8 @@
    1.13  The syntactic entity \synt{name} denotes an identifier \cite{isabelle-isar-ref}.
    1.14  
    1.15  The command is interesting because the old datatype package provides some
    1.16 -functionality that is not yet replicated in the new package:
    1.17 -
    1.18 -\begin{itemize}
    1.19 -\setlength{\itemsep}{0pt}
    1.20 -
    1.21 -\item It is integrated with \keyw{fun} \cite{isabelle-function},
    1.22 -Nitpick \cite{isabelle-nitpick}, Quickcheck, and other packages.
    1.23 -
    1.24 -\item It is extended by various add-ons, notably to produce instances of the
    1.25 -@{const size} function.
    1.26 -\end{itemize}
    1.27 +functionality that is not yet replicated in the new package, such as the
    1.28 +integration with Quickcheck.
    1.29  
    1.30  A few remarks concern nested recursive datatypes:
    1.31  
    1.32 @@ -626,8 +617,8 @@
    1.33  no way to register old-style datatypes as new-style datatypes).
    1.34  
    1.35  \item The recursor produced for types that recurse through functions has a
    1.36 -different signature than with the old package. This makes it impossible to use
    1.37 -the old \keyw{primrec} command.
    1.38 +different signature than with the old package. This might affect the behavior of
    1.39 +some third-party extensions.
    1.40  \end{itemize}
    1.41  
    1.42  An alternative to @{command datatype_compat} is to use the old package's
    1.43 @@ -657,13 +648,15 @@
    1.44  & \quad\vdots \\
    1.45  & @{text t.un_C\<^sub>n1}$, \ldots, $@{text t.un_C\<^sub>nk\<^sub>n} \\
    1.46  Set functions: &
    1.47 -  @{text set1_t}, \ldots, @{text t.setm_t} \\
    1.48 +  @{text t.set1_t}, \ldots, @{text t.setm_t} \\
    1.49  Map function: &
    1.50    @{text t.map_t} \\
    1.51  Relator: &
    1.52    @{text t.rel_t} \\
    1.53  Recursor: &
    1.54 -  @{text t.rec_t}
    1.55 +  @{text t.rec_t} \\
    1.56 +Size function: &
    1.57 +  @{text t.size_t}
    1.58  \end{tabular}
    1.59  
    1.60  \medskip
    1.61 @@ -672,6 +665,9 @@
    1.62  The case combinator, discriminators, and selectors are collectively called
    1.63  \emph{destructors}. The prefix ``@{text "t."}'' is an optional component of the
    1.64  names and is normally hidden.
    1.65 +
    1.66 +In addition to the above, the @{class size} class is instantiated to overload the
    1.67 +@{const size} function based on @{text t.size_t}.
    1.68  *}
    1.69  
    1.70  
    1.71 @@ -685,15 +681,16 @@
    1.72  \begin{itemize}
    1.73  \setlength{\itemsep}{0pt}
    1.74  
    1.75 -\item The \emph{free constructor theorems} are properties about the constructors
    1.76 -and destructors that can be derived for any freely generated type. Internally,
    1.77 -the derivation is performed by @{command free_constructors}.
    1.78 -
    1.79 -\item The \emph{functorial theorems} are properties of datatypes related to
    1.80 -their BNF nature.
    1.81 -
    1.82 -\item The \emph{inductive theorems} are properties of datatypes related to
    1.83 -their inductive nature.
    1.84 +\item The \emph{free constructor theorems}
    1.85 +(Section~\ref{sssec:free-constructor-theorems}) are properties of the
    1.86 +constructors and destructors that can be derived for any freely generated type.
    1.87 +Internally, the derivation is performed by @{command free_constructors}.
    1.88 +
    1.89 +\item The \emph{functorial theorems} (Section~\ref{sssec:functorial-theorems})
    1.90 +are properties of datatypes related to their BNF nature.
    1.91 +
    1.92 +\item The \emph{inductive theorems} (Section~\ref{sssec:inductive-theorems})
    1.93 +are properties of datatypes related to their inductive nature.
    1.94  
    1.95  \end{itemize}
    1.96  
    1.97 @@ -933,6 +930,18 @@
    1.98  @{thm list.rec(1)[no_vars]} \\
    1.99  @{thm list.rec(2)[no_vars]}
   1.100  
   1.101 +\item[@{text "t."}\hthm{rec\_o\_map}\rm:] ~ \\
   1.102 +@{thm list.rec_o_map[no_vars]}
   1.103 +
   1.104 +\item[@{text "t."}\hthm{size} @{text "[simp, code]"}\rm:] ~ \\
   1.105 +@{thm list.size(1)[no_vars]} \\
   1.106 +@{thm list.size(2)[no_vars]} \\
   1.107 +@{thm list.size(3)[no_vars]} \\
   1.108 +@{thm list.size(4)[no_vars]}
   1.109 +
   1.110 +\item[@{text "t."}\hthm{size\_o\_map}\rm:] ~ \\
   1.111 +@{thm list.size_o_map[no_vars]}
   1.112 +
   1.113  \end{description}
   1.114  \end{indentblock}
   1.115  
   1.116 @@ -963,9 +972,9 @@
   1.117  
   1.118  \item \emph{The Standard ML interfaces are different.} Tools and extensions
   1.119  written to call the old ML interfaces will need to be adapted to the new
   1.120 -interfaces. Little has been done so far in this direction. Whenever possible, it
   1.121 -is recommended to use @{command datatype_compat} or \keyw{rep\_datatype}
   1.122 -to register new-style datatypes as old-style datatypes.
   1.123 +interfaces. This concerns Quickcheck in particular. Whenever possible, it is
   1.124 +recommended to use @{command datatype_compat} to register new-style datatypes
   1.125 +as old-style datatypes.
   1.126  
   1.127  \item \emph{The constants @{text t_case}, @{text t_rec}, and @{text t_size} are
   1.128  now called @{text case_t}, @{text rec_t}, and @{text size_t}.}
   1.129 @@ -976,15 +985,14 @@
   1.130  type of the recursor, used by \keyw{primrec}. Recursion through functions was
   1.131  handled specially. In the new package, nested recursion (for functions and
   1.132  non-functions) is handled in a more modular fashion. The old-style recursor can
   1.133 -be generated on demand using @{command primrec}, as explained in
   1.134 -Section~\ref{sssec:primrec-nested-as-mutual-recursion}, if the recursion is via
   1.135 -new-style datatypes.
   1.136 +be generated on demand using @{command primrec} if the recursion is via
   1.137 +new-style datatypes, as explained in
   1.138 +Section~\ref{sssec:primrec-nested-as-mutual-recursion}.
   1.139  
   1.140  \item \emph{Accordingly, the induction rule is different for nested recursive
   1.141  datatypes.} Again, the old-style induction rule can be generated on demand using
   1.142 -@{command primrec}, as explained in
   1.143 -Section~\ref{sssec:primrec-nested-as-mutual-recursion}, if the recursion is via
   1.144 -new-style datatypes.
   1.145 +@{command primrec} if the recursion is via new-style datatypes, as explained in
   1.146 +Section~\ref{sssec:primrec-nested-as-mutual-recursion}.
   1.147  
   1.148  \item \emph{The internal constructions are completely different.} Proof texts
   1.149  that unfold the definition of constants introduced by \keyw{datatype} will be
   1.150 @@ -1634,13 +1642,13 @@
   1.151  with $m > 0$ live type variables and $n$ constructors @{text "t.C\<^sub>1"},
   1.152  \ldots, @{text "t.C\<^sub>n"}, the same auxiliary constants are generated as for
   1.153  datatypes (Section~\ref{ssec:datatype-generated-constants}), except that the
   1.154 -recursor is replaced by a dual concept:
   1.155 +recursor is replaced by a dual concept and no size function is produced:
   1.156  
   1.157  \medskip
   1.158  
   1.159  \begin{tabular}{@ {}ll@ {}}
   1.160  Corecursor: &
   1.161 -  @{text corec_t}
   1.162 +  @{text t.corec_t}
   1.163  \end{tabular}
   1.164  *}
   1.165  
   1.166 @@ -1655,20 +1663,20 @@
   1.167  \begin{itemize}
   1.168  \setlength{\itemsep}{0pt}
   1.169  
   1.170 -\item The \emph{free constructor theorems} are properties about the constructors
   1.171 -and destructors that can be derived for any freely generated type.
   1.172 -
   1.173 -\item The \emph{functorial theorems} are properties of datatypes related to
   1.174 +\item The \emph{free constructor theorems}
   1.175 +(Section~\ref{sssec:free-constructor-theorems}) are properties of the
   1.176 +constructors and destructors that can be derived for any freely generated type.
   1.177 +
   1.178 +\item The \emph{functorial theorems}
   1.179 +(Section~\ref{sssec:functorial-theorems}) are properties of datatypes related to
   1.180  their BNF nature.
   1.181  
   1.182 -\item The \emph{coinductive theorems} are properties of datatypes related to
   1.183 -their coinductive nature.
   1.184 +\item The \emph{coinductive theorems} (Section~\ref{sssec:coinductive-theorems})
   1.185 +are properties of datatypes related to their coinductive nature.
   1.186  \end{itemize}
   1.187  
   1.188  \noindent
   1.189 -The first two categories are exactly as for datatypes and are described in
   1.190 -Sections
   1.191 -\ref{sssec:free-constructor-theorems}~and~\ref{sssec:functorial-theorems}.
   1.192 +The first two categories are exactly as for datatypes.
   1.193  *}
   1.194  
   1.195  
   1.196 @@ -2717,7 +2725,7 @@
   1.197  
   1.198  Tobias Nipkow and Makarius Wenzel encouraged us to implement the new
   1.199  (co)datatype package. Andreas Lochbihler provided lots of comments on earlier
   1.200 -versions of the package, especially for the coinductive part. Brian Huffman
   1.201 +versions of the package, especially on the coinductive part. Brian Huffman
   1.202  suggested major simplifications to the internal constructions, many of which
   1.203  have yet to be implemented. Florian Haftmann and Christian Urban provided
   1.204  general advice on Isabelle and package writing. Stefan Milius and Lutz