more (co)data docs
authorblanchet
Wed Sep 11 17:17:58 2013 +0200 (2013-09-11)
changeset 53543c6c8dce7e9ab
parent 53542 14000a283ce0
child 53544 2176a7e40786
more (co)data docs
src/Doc/Datatypes/Datatypes.thy
     1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Wed Sep 11 16:55:01 2013 +0200
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Wed Sep 11 17:17:58 2013 +0200
     1.3 @@ -40,7 +40,7 @@
     1.4  text {*
     1.5  \noindent
     1.6  The package also provides some convenience, notably automatically generated
     1.7 -destructors (discriminators and selectors).
     1.8 +discriminators and selectors.
     1.9  
    1.10  In addition to plain inductive datatypes, the new package supports coinductive
    1.11  datatypes, or \emph{codatatypes}, which may have infinite values. For example,
    1.12 @@ -75,7 +75,7 @@
    1.13  infinitely many direct subtrees.
    1.14  
    1.15  To use the package, it is necessary to import the @{theory BNF} theory, which
    1.16 -can be precompiled into the \textit{HOL-BNF} image. The following commands show
    1.17 +can be precompiled into the @{text "HOL-BNF"} image. The following commands show
    1.18  how to launch jEdit/PIDE with the image loaded and how to build the image
    1.19  without launching jEdit:
    1.20  *}
    1.21 @@ -91,7 +91,7 @@
    1.22  The package, like its predecessor, fully adheres to the LCF philosophy
    1.23  \cite{mgordon79}: The characteristic theorems associated with the specified
    1.24  (co)datatypes are derived rather than introduced axiomatically.%
    1.25 -\footnote{If the \textit{quick_and_dirty} option is enabled, some of the
    1.26 +\footnote{If the @{text quick_and_dirty} option is enabled, some of the
    1.27  internal constructions and most of the internal proof obligations are skipped.}
    1.28  The package's metatheory is described in a pair of papers
    1.29  \cite{traytel-et-al-2012,blanchette-et-al-wit}.
    1.30 @@ -343,7 +343,8 @@
    1.31  
    1.32  \item \relax{Relator}: @{text t_rel}
    1.33  
    1.34 -\item \relax{Case combinator}: @{text t_case}
    1.35 +\item \relax{Case combinator}: @{text t_case} (rendered using the familiar
    1.36 +@{text case}--@{text of} syntax)
    1.37  
    1.38  \item \relax{Iterator}: @{text t_fold}
    1.39  
    1.40 @@ -353,16 +354,17 @@
    1.41  @{text "t.is_C\<^sub>n"}
    1.42  
    1.43  \item \relax{Selectors}:
    1.44 -@{text t.un_C11}$, \ldots, @{text t.un_C1k\<^sub>1}, \\
    1.45 +@{text t.un_C\<^sub>11}$, \ldots, @{text t.un_C\<^sub>1k\<^sub>1}, \\
    1.46  \phantom{\relax{Selectors:}} \quad\vdots \\
    1.47 -\phantom{\relax{Selectors:}} @{text t.un_Cn1}$, \ldots, @{text t.un_Cnk\<^sub>n}.
    1.48 +\phantom{\relax{Selectors:}} @{text t.un_C\<^sub>n1}$, \ldots, @{text t.un_C\<^sub>nk\<^sub>n}.
    1.49  \end{itemize}
    1.50  
    1.51  \noindent
    1.52 -The discriminators and selectors are collectively called \emph{destructors}. The
    1.53 -prefix ``@{text "t."}'' is an optional component of the name and is normally
    1.54 -hidden. The set functions, map function, relator, discriminators, and selectors
    1.55 -can be given custom names, as in the example below:
    1.56 +The case combinator, discriminators, and selectors are collectively called
    1.57 +\emph{destructors}. The prefix ``@{text "t."}'' is an optional component of the
    1.58 +name and is normally hidden. The set functions, map function, relator,
    1.59 +discriminators, and selectors can be given custom names, as in the example
    1.60 +below:
    1.61  *}
    1.62  
    1.63  (*<*)
    1.64 @@ -374,6 +376,7 @@
    1.65        Nil ("[]") and
    1.66        Cons (infixr "#" 65)
    1.67  
    1.68 +    hide_type list
    1.69      hide_const Nil Cons hd tl map
    1.70  
    1.71      locale dummy_list
    1.72 @@ -456,13 +459,13 @@
    1.73  \setlength{\itemsep}{0pt}
    1.74  
    1.75  \item
    1.76 -The \keyw{no_discs_sels} option indicates that no destructors (i.e.,
    1.77 -discriminators and selectors) should be generated.
    1.78 +The \keyw{no\_discs\_sels} option indicates that no discriminators or selectors
    1.79 +should be generated.
    1.80  
    1.81  \item
    1.82 -The \keyw{rep_compat} option indicates that the names generated by the
    1.83 +The \keyw{rep\_compat} option indicates that the names generated by the
    1.84  package should contain optional (and normally not displayed) ``@{text "new."}''
    1.85 -components to prevent clashes with a later call to \keyw{rep_datatype}. See
    1.86 +components to prevent clashes with a later call to \keyw{rep\_datatype}. See
    1.87  Section~\ref{ssec:datatype-compatibility-issues} for details.
    1.88  \end{itemize}
    1.89  
    1.90 @@ -533,21 +536,21 @@
    1.91  The characteristic theorems generated by @{command datatype_new} are
    1.92  grouped in three broad categories:
    1.93  
    1.94 -\begin{enumerate}
    1.95 -\item The free constructor theorems are properties about the constructors and
    1.96 -destructors that can be derived for any freely generated type. Internally,
    1.97 +\begin{itemize}
    1.98 +\item The \emph{free constructor theorems} are properties about the constructors
    1.99 +and destructors that can be derived for any freely generated type. Internally,
   1.100  the derivation is performed by @{command wrap_free_constructors}.
   1.101  
   1.102 -\item The per-datatype theorems are properties connected to individual datatypes
   1.103 -and that rely on their inductive nature.
   1.104 +\item The \emph{per-datatype theorems} are properties connected to individual
   1.105 +datatypes and that rely on their inductive nature.
   1.106  
   1.107 -\item The mutual datatype theorems are properties of mutually recursive groups
   1.108 -of datatypes.
   1.109 -\end{enumerate}
   1.110 +\item The \emph{mutual datatype theorems} are properties associated to mutually
   1.111 +recursive groups of datatypes.
   1.112 +\end{itemize}
   1.113  
   1.114  \noindent
   1.115  The full list of named theorems can be obtained as usual by entering the
   1.116 -command \keyw{print_theorems} immediately after the datatype definition.
   1.117 +command \keyw{print\_theorems} immediately after the datatype definition.
   1.118  This list normally excludes low-level theorems that reveal internal
   1.119  constructions. To see these as well, add the following line to the top of your
   1.120  theory file:
   1.121 @@ -561,9 +564,87 @@
   1.122  
   1.123  subsubsection {* Free Constructor Theorems *}
   1.124  
   1.125 +(*<*)
   1.126 +    consts is_Cons :: 'a
   1.127 +(*>*)
   1.128 +
   1.129  text {*
   1.130 -  * free ctor theorems
   1.131 -    * case syntax
   1.132 +The first subgroup of properties are concerned with the constructors.
   1.133 +They are listed below for @{typ "'a list"}:
   1.134 +
   1.135 +\begin{description}
   1.136 +\item[@{text "t.distinct [simp, induct_simp]"}:] ~ \\
   1.137 +@{thm list.distinct(1)[no_vars]} \\
   1.138 +@{thm list.distinct(2)[no_vars]}
   1.139 +
   1.140 +\item[@{text "t.inject [iff, induct_simp]"}:] ~ \\
   1.141 +@{thm list.inject[no_vars]}
   1.142 +
   1.143 +\item[@{text "t.exhaust [cases t, case_names C\<^sub>1 \<dots> C\<^sub>n]"}:] ~ \\
   1.144 +@{thm list.exhaust[no_vars]}
   1.145 +
   1.146 +\item[@{text t.nchotomy}:] ~ \\
   1.147 +@{thm list.nchotomy[no_vars]}
   1.148 +
   1.149 +\end{description}
   1.150 +
   1.151 +\noindent
   1.152 +The next subgroup is concerned with the case combinator:
   1.153 +
   1.154 +\begin{description}
   1.155 +\item[@{text "t.case [simp]"}:] ~ \\
   1.156 +@{thm list.case(1)[no_vars]} \\
   1.157 +@{thm list.case(2)[no_vars]}
   1.158 +
   1.159 +\item[@{text t.case_cong}:] ~ \\
   1.160 +@{thm list.case_cong[no_vars]}
   1.161 +
   1.162 +\item[@{text "t.weak_case_cong [cong]"}:] ~ \\
   1.163 +@{thm list.weak_case_cong[no_vars]}
   1.164 +
   1.165 +\item[@{text t.split}:] ~ \\
   1.166 +@{thm list.split[no_vars]}
   1.167 +
   1.168 +\item[@{text t.split_asm}:] ~ \\
   1.169 +@{thm list.split_asm[no_vars]}
   1.170 +
   1.171 +\item[@{text "t.splits = split split_asm"}]
   1.172 +
   1.173 +\end{description}
   1.174 +
   1.175 +\noindent
   1.176 +The third and last subgroup revolves around discriminators and selectors:
   1.177 +
   1.178 +\begin{description}
   1.179 +\item[@{text "discs [simp]"}:] ~ \\
   1.180 +@{thm list.discs(1)[no_vars]} \\
   1.181 +@{thm list.discs(2)[no_vars]}
   1.182 +
   1.183 +\item[@{text "sels [simp]"}:] ~ \\
   1.184 +@{thm list.sels(1)[no_vars]} \\
   1.185 +@{thm list.sels(2)[no_vars]}
   1.186 +
   1.187 +\item[@{text "collapse [simp]"}:] ~ \\
   1.188 +@{thm list.collapse(1)[no_vars]} \\
   1.189 +@{thm list.collapse(2)[no_vars]}
   1.190 +
   1.191 +\item[@{text disc_exclude}:] ~ \\
   1.192 +These properties are missing for @{typ "'a list"} because there is only one
   1.193 +proper discriminator. Had the datatype been introduced with a second
   1.194 +discriminator (@{const is_Cons}), they would have read thusly: \\
   1.195 +@{prop "null list \<Longrightarrow> \<not> is_Cons list"} \\
   1.196 +@{prop "is_Cons list \<Longrightarrow> \<not> null list"}
   1.197 +
   1.198 +\item[@{text "disc_exhaust [case_names C\<^sub>1 \<dots> C\<^sub>n]]"}:] ~ \\
   1.199 +@{thm list.disc_exhaust[no_vars]}
   1.200 +
   1.201 +\item[@{text expand}:] ~ \\
   1.202 +@{thm list.expand[no_vars]}
   1.203 +
   1.204 +\item[@{text t.case_conv}:] ~ \\
   1.205 +@{thm list.case_conv[no_vars]}
   1.206 +
   1.207 +\end{description}
   1.208  
   1.209    * Section~\label{sec:generating-free-constructor-theorems}
   1.210  *}
   1.211 @@ -607,15 +688,19 @@
   1.212          Nitpick
   1.213        * provide exactly the same theorems with the same names (compatibility)
   1.214      * option 1
   1.215 -      * \keyw{rep_compat}
   1.216 -      * \keyw{rep_datatype}
   1.217 +      * \keyw{rep\_compat}
   1.218 +      * \keyw{rep\_datatype}
   1.219        * has some limitations
   1.220          * mutually recursive datatypes? (fails with rep_datatype?)
   1.221          * nested datatypes? (fails with datatype_new?)
   1.222      * option 2
   1.223 -      * \keyw{datatype_compat}
   1.224 +      * @{command datatype_new_compat}
   1.225        * not fully implemented yet?
   1.226  
   1.227 +@{rail "
   1.228 +  @@{command_def datatype_new_compat} types
   1.229 +"}
   1.230 +
   1.231    * register old datatype as new datatype
   1.232      * no clean way yet
   1.233      * if the goal is to do recursion through old datatypes, can register it as
   1.234 @@ -971,8 +1056,8 @@
   1.235  text {*
   1.236  Definitions of codatatypes have almost exactly the same syntax as for datatypes
   1.237  (Section~\ref{ssec:datatype-syntax}), with two exceptions: The command is called
   1.238 -@{command codatatype}; the \keyw{no_discs_sels} option is not available, because
   1.239 -destructors are a central notion for codatatypes.
   1.240 +@{command codatatype}; the \keyw{no\_discs\_sels} option is not available,
   1.241 +because destructors are a central notion for codatatypes.
   1.242  *}
   1.243  
   1.244  subsection {* Generated Theorems
   1.245 @@ -1076,7 +1161,7 @@
   1.246      old \keyw{datatype}
   1.247  
   1.248    * @{command wrap_free_constructors}
   1.249 -    * \keyw{no_discs_sels}, \keyw{rep_compat}
   1.250 +    * \keyw{no\_discs\_sels}, \keyw{rep\_compat}
   1.251      * hack to have both co and nonco view via locale (cf. ext nats)
   1.252  *}
   1.253  
   1.254 @@ -1168,7 +1253,7 @@
   1.255    based on overloading
   1.256  
   1.257  * no way to register "sum" and "prod" as (co)datatypes to enable N2M reduction for them
   1.258 -  (for datatype_compat and prim(co)rec)
   1.259 +  (for @{command datatype_new_compat} and prim(co)rec)
   1.260  
   1.261  * no way to register same type as both data- and codatatype?
   1.262