1.1 --- a/src/Doc/Datatypes/Datatypes.thy Fri Sep 13 19:38:09 2013 +0200
1.2 +++ b/src/Doc/Datatypes/Datatypes.thy Fri Sep 13 21:28:57 2013 +0200
1.3 @@ -51,7 +51,11 @@
1.4 finite and infinite values:
1.5 *}
1.6
1.7 - codatatype 'a llist (*<*)(map: lmap) (*>*)= LNil | LCons 'a "'a llist"
1.8 +(*<*)
1.9 + locale dummy_llist
1.10 + begin
1.11 +(*>*)
1.12 + codatatype 'a llist = LNil | LCons 'a "'a llist"
1.13
1.14 text {*
1.15 \noindent
1.16 @@ -59,10 +63,6 @@
1.17 following four Rose tree examples:
1.18 *}
1.19
1.20 -(*<*)
1.21 - locale dummy_tree
1.22 - begin
1.23 -(*>*)
1.24 datatype_new 'a tree\<^sub>f\<^sub>f = Node\<^sub>f\<^sub>f 'a "'a tree\<^sub>f\<^sub>f list"
1.25 datatype_new 'a tree\<^sub>f\<^sub>i = Node\<^sub>f\<^sub>i 'a "'a tree\<^sub>f\<^sub>i llist"
1.26 codatatype 'a tree\<^sub>i\<^sub>f = Node\<^sub>i\<^sub>f 'a "'a tree\<^sub>i\<^sub>f list"
1.27 @@ -177,10 +177,10 @@
1.28 \label{sec:defining-datatypes} *}
1.29
1.30 text {*
1.31 -This section describes how to specify datatypes using the @{command
1.32 -datatype_new} command. The command is first illustrated through concrete
1.33 -examples featuring different flavors of recursion. More examples can be found in
1.34 -the directory \verb|~~/src/HOL/BNF/Examples|.
1.35 +Datatypes can be specified using the @{command datatype_new} command. The
1.36 +command is first illustrated through concrete examples featuring different
1.37 +flavors of recursion. More examples can be found in the directory
1.38 +\verb|~~/src/HOL/BNF/Examples|.
1.39 *}
1.40
1.41
1.42 @@ -272,8 +272,8 @@
1.43 natural numbers:
1.44 *}
1.45
1.46 - datatype_new enat = EZero | ESuc onat
1.47 - and onat = OSuc enat
1.48 + datatype_new even_nat = Even_Zero | Even_Suc odd_nat
1.49 + and odd_nat = Odd_Suc even_nat
1.50
1.51 text {*
1.52 \noindent
1.53 @@ -443,7 +443,7 @@
1.54 @@{command_def datatype_new} target? @{syntax dt_options}? \\
1.55 (@{syntax dt_name} '=' (@{syntax ctor} + '|') + @'and')
1.56 ;
1.57 - @{syntax_def dt_options}: '(' ((@'no_discs_sels' | @'rep_compat') + ',') ')'
1.58 + @{syntax_def dt_options}: '(' (('no_discs_sels' | 'rep_compat') + ',') ')'
1.59 "}
1.60
1.61 The syntactic quantity \synt{target} can be used to specify a local
1.62 @@ -456,11 +456,11 @@
1.63 \setlength{\itemsep}{0pt}
1.64
1.65 \item
1.66 -The \keyw{no\_discs\_sels} option indicates that no discriminators or selectors
1.67 +The @{text "no_discs_sels"} option indicates that no discriminators or selectors
1.68 should be generated.
1.69
1.70 \item
1.71 -The \keyw{rep\_compat} option indicates that the names generated by the
1.72 +The @{text "rep_compat"} option indicates that the names generated by the
1.73 package should contain optional (and normally not displayed) ``@{text "new."}''
1.74 components to prevent clashes with a later call to \keyw{rep\_datatype}. See
1.75 Section~\ref{ssec:datatype-compatibility-issues} for details.
1.76 @@ -557,15 +557,15 @@
1.77 that are mutually recursive. For example:
1.78 *}
1.79
1.80 - datatype_new_compat enat onat
1.81 + datatype_new_compat even_nat odd_nat
1.82
1.83 text {* \blankline *}
1.84
1.85 - thm enat_onat.size
1.86 + thm even_nat_odd_nat.size
1.87
1.88 text {* \blankline *}
1.89
1.90 - ML {* Datatype_Data.get_info @{theory} @{type_name enat} *}
1.91 + ML {* Datatype_Data.get_info @{theory} @{type_name even_nat} *}
1.92
1.93 text {*
1.94 For nested recursive datatypes, all types through which recursion takes place
1.95 @@ -578,7 +578,7 @@
1.96 \label{ssec:datatype-generated-constants} *}
1.97
1.98 text {*
1.99 -Given a type @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"}
1.100 +Given a datatype @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"}
1.101 with $m > 0$ live type variables and $n$ constructors
1.102 @{text "t.C\<^sub>1"}, \ldots, @{text "t.C\<^sub>n"}, the
1.103 following auxiliary constants are introduced:
1.104 @@ -622,7 +622,7 @@
1.105
1.106 text {*
1.107 The characteristic theorems generated by @{command datatype_new} are grouped in
1.108 -two broad categories:
1.109 +three broad categories:
1.110
1.111 \begin{itemize}
1.112 \item The \emph{free constructor theorems} are properties about the constructors
1.113 @@ -767,7 +767,7 @@
1.114 \label{sssec:functorial-theorems} *}
1.115
1.116 text {*
1.117 -The BNF-related theorem are listed below:
1.118 +The BNF-related theorem are as follows:
1.119
1.120 \begin{indentblock}
1.121 \begin{description}
1.122 @@ -797,7 +797,7 @@
1.123 \label{sssec:inductive-theorems} *}
1.124
1.125 text {*
1.126 -The inductive theorems are listed below:
1.127 +The inductive theorems are as follows:
1.128
1.129 \begin{indentblock}
1.130 \begin{description}
1.131 @@ -856,7 +856,7 @@
1.132 % Nitpick
1.133 % * provide exactly the same theorems with the same names (compatibility)
1.134 % * option 1
1.135 -% * \keyw{rep\_compat}
1.136 +% * @{text "rep_compat"}
1.137 % * \keyw{rep\_datatype}
1.138 % * has some limitations
1.139 % * mutually recursive datatypes? (fails with rep_datatype?)
1.140 @@ -989,12 +989,12 @@
1.141 *}
1.142
1.143 primrec_new
1.144 - nat_of_enat :: "enat \<Rightarrow> nat" and
1.145 - nat_of_onat :: "onat \<Rightarrow> nat"
1.146 + nat_of_even_nat :: "even_nat \<Rightarrow> nat" and
1.147 + nat_of_odd_nat :: "odd_nat \<Rightarrow> nat"
1.148 where
1.149 - "nat_of_enat EZero = Zero" |
1.150 - "nat_of_enat (ESuc n) = Suc (nat_of_onat n)" |
1.151 - "nat_of_onat (OSuc n) = Suc (nat_of_enat n)"
1.152 + "nat_of_even_nat Even_Zero = Zero" |
1.153 + "nat_of_even_nat (Even_Suc n) = Suc (nat_of_odd_nat n)" |
1.154 + "nat_of_odd_nat (Odd_Suc n) = Suc (nat_of_even_nat n)"
1.155
1.156 primrec_new
1.157 eval\<^sub>e :: "('a \<Rightarrow> int) \<Rightarrow> ('b \<Rightarrow> int) \<Rightarrow> ('a, 'b) exp \<Rightarrow> int" and
1.158 @@ -1035,7 +1035,6 @@
1.159
1.160 (*<*)
1.161 datatype_new 'a tree\<^sub>f\<^sub>f = Node\<^sub>f\<^sub>f 'a "'a tree\<^sub>f\<^sub>f list"
1.162 - datatype_new 'a tree\<^sub>f\<^sub>i = Node\<^sub>f\<^sub>i 'a "'a tree\<^sub>f\<^sub>i llist"
1.163
1.164 context dummy_tlist
1.165 begin
1.166 @@ -1051,7 +1050,7 @@
1.167
1.168 text {*
1.169 The next example features recursion through the @{text option} type. Although
1.170 -@{text option} is not a new-style datatype, it is registered as a BNF, with the
1.171 +@{text option} is not a new-style datatype, it is registered as a BNF with the
1.172 map function @{const option_map}:
1.173 *}
1.174
1.175 @@ -1187,7 +1186,7 @@
1.176
1.177
1.178 subsection {* Recursive Default Values for Selectors
1.179 - \label{ssec:recursive-default-values-for-selectors} *}
1.180 + \label{ssec:primrec-recursive-default-values-for-selectors} *}
1.181
1.182 text {*
1.183 A datatype selector @{text un_D} can have a default value for each constructor
1.184 @@ -1269,23 +1268,71 @@
1.185 \label{sec:defining-codatatypes} *}
1.186
1.187 text {*
1.188 -This section describes how to specify codatatypes using the @{command
1.189 -codatatype} command. The command is first illustrated through concrete examples
1.190 -featuring different flavors of corecursion. More examples can be found in the
1.191 -directory \verb|~~/src/HOL/BNF/Examples|. The \emph{Archive of Formal Proofs}
1.192 -also includes some useful codatatypes, notably for lazy lists
1.193 -\cite{lochbihler-2010}.
1.194 +Codatatypes can be specified using the @{command codatatype} command. The
1.195 +command is first illustrated through concrete examples featuring different
1.196 +flavors of corecursion. More examples can be found in the directory
1.197 +\verb|~~/src/HOL/BNF/Examples|. The \emph{Archive of Formal Proofs} also
1.198 +includes some useful codatatypes, notably for lazy lists \cite{lochbihler-2010}.
1.199 *}
1.200
1.201
1.202 -(*
1.203 subsection {* Introductory Examples
1.204 \label{ssec:codatatype-introductory-examples} *}
1.205
1.206 +
1.207 +subsubsection {* Simple Corecursion
1.208 + \label{sssec:codatatype-simple-corecursion} *}
1.209 +
1.210 text {*
1.211 -More examples in \verb|~~/src/HOL/BNF/Examples|.
1.212 +Noncorecursive codatatypes coincide with the corresponding datatypes, so
1.213 +they have no practical uses. \emph{Corecursive codatatypes} have the same syntax
1.214 +as recursive datatypes, except for the command name. For example, here is the
1.215 +definition of lazy lists:
1.216 *}
1.217 -*)
1.218 +
1.219 + codatatype (lset: 'a) llist (map: lmap rel: llist_all2) =
1.220 + lnull: LNil (defaults ltl: LNil)
1.221 + | LCons (lhd: 'a) (ltl: "'a llist")
1.222 +
1.223 +text {*
1.224 +\noindent
1.225 +Lazy lists can be infinite, such as @{text "LCons 0 (LCons 0 (\<dots>))"} and
1.226 +@{text "LCons 0 (LCons 1 (LCons 2 (\<dots>)))"}. Another interesting type that can
1.227 +be defined as a codatatype is that of the extended natural numbers:
1.228 +*}
1.229 +
1.230 + codatatype enat = EZero | ESuc nat
1.231 +
1.232 +text {*
1.233 +\noindent
1.234 +This type has exactly one infinite element, @{text "ESuc (ESuc (ESuc (\<dots>)))"},
1.235 +that represents $\infty$. In addition, it has finite values of the form
1.236 +@{text "ESuc (\<dots> (ESuc EZero)\<dots>)"}.
1.237 +*}
1.238 +
1.239 +
1.240 +subsubsection {* Mutual Corecursion
1.241 + \label{sssec:codatatype-mutual-corecursion} *}
1.242 +
1.243 +text {*
1.244 +\noindent
1.245 +The example below introduces a pair of \emph{mutually corecursive} types:
1.246 +*}
1.247 +
1.248 + codatatype even_enat = Even_EZero | Even_ESuc odd_enat
1.249 + and odd_enat = Odd_ESuc even_enat
1.250 +
1.251 +
1.252 +subsubsection {* Nested Corecursion
1.253 + \label{sssec:codatatype-nested-corecursion} *}
1.254 +
1.255 +text {*
1.256 +\noindent
1.257 +The next two examples feature \emph{nested corecursion}:
1.258 +*}
1.259 +
1.260 + codatatype 'a tree\<^sub>i\<^sub>i = Node\<^sub>i\<^sub>i 'a "'a tree\<^sub>i\<^sub>i llist"
1.261 + codatatype 'a tree\<^sub>i\<^sub>s = Node\<^sub>i\<^sub>s 'a "'a tree\<^sub>i\<^sub>s fset"
1.262
1.263
1.264 subsection {* Command Syntax
1.265 @@ -1298,29 +1345,116 @@
1.266 text {*
1.267 Definitions of codatatypes have almost exactly the same syntax as for datatypes
1.268 (Section~\ref{ssec:datatype-command-syntax}), with two exceptions: The command
1.269 -is called @{command codatatype}; the \keyw{no\_discs\_sels} option is not
1.270 -available, because destructors are a central notion for codatatypes.
1.271 +is called @{command codatatype}. The @{text "no_discs_sels"} option is not
1.272 +available, because destructors are a crucial notion for codatatypes.
1.273 *}
1.274
1.275
1.276 -(*
1.277 subsection {* Generated Constants
1.278 \label{ssec:codatatype-generated-constants} *}
1.279 -*)
1.280
1.281 +text {*
1.282 +Given a codatatype @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"}
1.283 +with $m > 0$ live type variables and $n$ constructors @{text "t.C\<^sub>1"},
1.284 +\ldots, @{text "t.C\<^sub>n"}, the same auxiliary constants are generated as for
1.285 +datatypes (Section~\ref{ssec:datatype-generated-constants}), except that the
1.286 +iterator and the recursor are replaced by dual concepts:
1.287
1.288 -(*
1.289 +\begin{itemize}
1.290 +\setlength{\itemsep}{0pt}
1.291 +
1.292 +\item \relax{Coiterator}: @{text t_unfold}
1.293 +
1.294 +\item \relax{Corecursor}: @{text t_corec}
1.295 +
1.296 +\end{itemize}
1.297 +*}
1.298 +
1.299 +
1.300 subsection {* Generated Theorems
1.301 \label{ssec:codatatype-generated-theorems} *}
1.302 -*)
1.303 +
1.304 +text {*
1.305 +The characteristic theorems generated by @{command codatatype} are grouped in
1.306 +three broad categories:
1.307 +
1.308 +\begin{itemize}
1.309 +\item The \emph{free constructor theorems} are properties about the constructors
1.310 +and destructors that can be derived for any freely generated type.
1.311 +
1.312 +\item The \emph{functorial theorems} are properties of datatypes related to
1.313 +their BNF nature.
1.314 +
1.315 +\item The \emph{coinductive theorems} are properties of datatypes related to
1.316 +their coinductive nature.
1.317 +\end{itemize}
1.318 +
1.319 +\noindent
1.320 +The first two categories are exactly as for datatypes and are described in
1.321 +Sections \ref{ssec:free-constructor-theorems}~and~\ref{ssec:functorial-theorems}.
1.322 +*}
1.323 +
1.324 +
1.325 +subsubsection {* Coinductive Theorems
1.326 + \label{sssec:coinductive-theorems} *}
1.327 +
1.328 +text {*
1.329 +The coinductive theorems are as follows:
1.330 +
1.331 +% [(coinductN, map single coinduct_thms,
1.332 +% fn T_name => coinduct_attrs @ [coinduct_type_attr T_name]),
1.333 +% (corecN, corec_thmss, K coiter_attrs),
1.334 +% (disc_corecN, disc_corec_thmss, K disc_coiter_attrs),
1.335 +% (disc_corec_iffN, disc_corec_iff_thmss, K disc_coiter_iff_attrs),
1.336 +% (disc_unfoldN, disc_unfold_thmss, K disc_coiter_attrs),
1.337 +% (disc_unfold_iffN, disc_unfold_iff_thmss, K disc_coiter_iff_attrs),
1.338 +% (sel_corecN, sel_corec_thmss, K sel_coiter_attrs),
1.339 +% (sel_unfoldN, sel_unfold_thmss, K sel_coiter_attrs),
1.340 +% (simpsN, simp_thmss, K []),
1.341 +% (strong_coinductN, map single strong_coinduct_thms, K coinduct_attrs),
1.342 +% (unfoldN, unfold_thmss, K coiter_attrs)]
1.343 +% |> massage_multi_notes;
1.344 +
1.345 +\begin{indentblock}
1.346 +\begin{description}
1.347 +
1.348 +\item[@{text "t."}\hthm{coinduct} @{text "[induct t, case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rmfamily:] ~ \\
1.349 +@{thm llist.coinduct[no_vars]}
1.350 +
1.351 +\item[@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{coinduct} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rmfamily:] ~ \\
1.352 +Given $m > 1$ mutually recursive datatypes, this induction rule can be used to
1.353 +prove $m$ properties simultaneously.
1.354 +
1.355 +\item[@{text "t."}\hthm{unfold} @{text "[code]"}\rmfamily:] ~ \\
1.356 +@{thm llist.unfold(1)[no_vars]} \\
1.357 +@{thm llist.unfold(2)[no_vars]}
1.358 +
1.359 +\item[@{text "t."}\hthm{corec} @{text "[code]"}\rmfamily:] ~ \\
1.360 +@{thm llist.corec(1)[no_vars]} \\
1.361 +@{thm llist.corec(2)[no_vars]}
1.362 +
1.363 +\end{description}
1.364 +\end{indentblock}
1.365 +
1.366 +\noindent
1.367 +For convenience, @{command codatatype} also provides the following collection:
1.368 +
1.369 +\begin{indentblock}
1.370 +\begin{description}
1.371 +
1.372 +\item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.rec} @{text t.fold} @{text t.map} @{text t.rel_inject}] ~ \\
1.373 +@{text t.rel_distinct} @{text t.sets}
1.374 +
1.375 +\end{description}
1.376 +\end{indentblock}
1.377 +*}
1.378
1.379
1.380 section {* Defining Corecursive Functions
1.381 \label{sec:defining-corecursive-functions} *}
1.382
1.383 text {*
1.384 -This section describes how to specify corecursive functions using the
1.385 -@{command primcorec} command.
1.386 +Corecursive functions can be specified using the @{command primcorec} command.
1.387
1.388 %%% TODO: partial_function? E.g. for defining tail recursive function on lazy
1.389 %%% lists (cf. terminal0 in TLList.thy)
1.390 @@ -1333,9 +1467,6 @@
1.391
1.392 text {*
1.393 More examples in \verb|~~/src/HOL/BNF/Examples|.
1.394 -
1.395 -Also, for default values, the same trick as for datatypes is possible for
1.396 -codatatypes (Section~\ref{ssec:recursive-default-values-for-selectors}).
1.397 *}
1.398 *)
1.399
1.400 @@ -1365,13 +1496,23 @@
1.401 *)
1.402
1.403
1.404 +(*
1.405 +subsection {* Recursive Default Values for Selectors
1.406 + \label{ssec:primcorec-recursive-default-values-for-selectors} *}
1.407 +
1.408 +text {*
1.409 +partial_function to the rescue
1.410 +*}
1.411 +*)
1.412 +
1.413 +
1.414 section {* Registering Bounded Natural Functors
1.415 \label{sec:registering-bounded-natural-functors} *}
1.416
1.417 text {*
1.418 -This section explains how to set up the (co)datatype package to allow nested
1.419 -recursion through custom well-behaved type constructors. The key concept is that
1.420 -of a bounded natural functor (BNF).
1.421 +The (co)datatype package can be set up to allow nested recursion through custom
1.422 +well-behaved type constructors. The key concept is that of a bounded natural
1.423 +functor (BNF).
1.424
1.425 *}
1.426
1.427 @@ -1420,8 +1561,9 @@
1.428 \label{sec:deriving-destructors-and-theorems-for-free-constructors} *}
1.429
1.430 text {*
1.431 -This section explains how to derive convenience theorems for free constructors,
1.432 -as performed internally by @{command datatype_new} and @{command codatatype}.
1.433 +The derivation of convenience theorems for types equipped with free constructors,
1.434 +as performed internally by @{command datatype_new} and @{command codatatype},
1.435 +is available as a stand-alone command called @{command wrap_free_constructors}.
1.436
1.437 % * need for this is rare but may arise if you want e.g. to add destructors to
1.438 % a type not introduced by ...
1.439 @@ -1430,7 +1572,7 @@
1.440 % old \keyw{datatype}
1.441 %
1.442 % * @{command wrap_free_constructors}
1.443 -% * \keyw{no\_discs\_sels}, \keyw{rep\_compat}
1.444 +% * @{text "no_discs_sels"}, @{text "rep_compat"}
1.445 % * hack to have both co and nonco view via locale (cf. ext nats)
1.446 *}
1.447
1.448 @@ -1473,7 +1615,7 @@
1.449 \label{sec:standard-ml-interface} *}
1.450
1.451 text {*
1.452 -This section describes the package's programmatic interface.
1.453 +The package's programmatic interface.
1.454 *}
1.455 *)
1.456
1.457 @@ -1483,9 +1625,8 @@
1.458 \label{sec:interoperability} *}
1.459
1.460 text {*
1.461 -This section is concerned with the packages' interaction with other Isabelle
1.462 -packages and tools, such as the code generator and the counterexample
1.463 -generators.
1.464 +The package's interaction with other Isabelle packages and tools, such as the
1.465 +code generator and the counterexample generators.
1.466 *}
1.467
1.468
1.469 @@ -1515,7 +1656,7 @@
1.470 \label{sec:known-bugs-and-limitations} *}
1.471
1.472 text {*
1.473 -This section lists known open issues of the package.
1.474 +Known open issues of the package.
1.475 *}
1.476
1.477 text {*