--- a/src/Doc/Datatypes/Datatypes.thy Wed Sep 11 16:55:01 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Wed Sep 11 17:17:58 2013 +0200
@@ -40,7 +40,7 @@
text {*
\noindent
The package also provides some convenience, notably automatically generated
-destructors (discriminators and selectors).
+discriminators and selectors.
In addition to plain inductive datatypes, the new package supports coinductive
datatypes, or \emph{codatatypes}, which may have infinite values. For example,
@@ -75,7 +75,7 @@
infinitely many direct subtrees.
To use the package, it is necessary to import the @{theory BNF} theory, which
-can be precompiled into the \textit{HOL-BNF} image. The following commands show
+can be precompiled into the @{text "HOL-BNF"} image. The following commands show
how to launch jEdit/PIDE with the image loaded and how to build the image
without launching jEdit:
*}
@@ -91,7 +91,7 @@
The package, like its predecessor, fully adheres to the LCF philosophy
\cite{mgordon79}: The characteristic theorems associated with the specified
(co)datatypes are derived rather than introduced axiomatically.%
-\footnote{If the \textit{quick_and_dirty} option is enabled, some of the
+\footnote{If the @{text quick_and_dirty} option is enabled, some of the
internal constructions and most of the internal proof obligations are skipped.}
The package's metatheory is described in a pair of papers
\cite{traytel-et-al-2012,blanchette-et-al-wit}.
@@ -343,7 +343,8 @@
\item \relax{Relator}: @{text t_rel}
-\item \relax{Case combinator}: @{text t_case}
+\item \relax{Case combinator}: @{text t_case} (rendered using the familiar
+@{text case}--@{text of} syntax)
\item \relax{Iterator}: @{text t_fold}
@@ -353,16 +354,17 @@
@{text "t.is_C\<^sub>n"}
\item \relax{Selectors}:
-@{text t.un_C11}$, \ldots, @{text t.un_C1k\<^sub>1}, \\
+@{text t.un_C\<^sub>11}$, \ldots, @{text t.un_C\<^sub>1k\<^sub>1}, \\
\phantom{\relax{Selectors:}} \quad\vdots \\
-\phantom{\relax{Selectors:}} @{text t.un_Cn1}$, \ldots, @{text t.un_Cnk\<^sub>n}.
+\phantom{\relax{Selectors:}} @{text t.un_C\<^sub>n1}$, \ldots, @{text t.un_C\<^sub>nk\<^sub>n}.
\end{itemize}
\noindent
-The discriminators and selectors are collectively called \emph{destructors}. The
-prefix ``@{text "t."}'' is an optional component of the name and is normally
-hidden. The set functions, map function, relator, discriminators, and selectors
-can be given custom names, as in the example below:
+The case combinator, discriminators, and selectors are collectively called
+\emph{destructors}. The prefix ``@{text "t."}'' is an optional component of the
+name and is normally hidden. The set functions, map function, relator,
+discriminators, and selectors can be given custom names, as in the example
+below:
*}
(*<*)
@@ -374,6 +376,7 @@
Nil ("[]") and
Cons (infixr "#" 65)
+ hide_type list
hide_const Nil Cons hd tl map
locale dummy_list
@@ -456,13 +459,13 @@
\setlength{\itemsep}{0pt}
\item
-The \keyw{no_discs_sels} option indicates that no destructors (i.e.,
-discriminators and selectors) should be generated.
+The \keyw{no\_discs\_sels} option indicates that no discriminators or selectors
+should be generated.
\item
-The \keyw{rep_compat} option indicates that the names generated by the
+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 \keyw{rep_datatype}. See
+components to prevent clashes with a later call to \keyw{rep\_datatype}. See
Section~\ref{ssec:datatype-compatibility-issues} for details.
\end{itemize}
@@ -533,21 +536,21 @@
The characteristic theorems generated by @{command datatype_new} are
grouped in three broad categories:
-\begin{enumerate}
-\item The free constructor theorems are properties about the constructors and
-destructors that can be derived for any freely generated type. Internally,
+\begin{itemize}
+\item The \emph{free constructor theorems} are properties about the constructors
+and destructors that can be derived for any freely generated type. Internally,
the derivation is performed by @{command wrap_free_constructors}.
-\item The per-datatype theorems are properties connected to individual datatypes
-and that rely on their inductive nature.
+\item The \emph{per-datatype theorems} are properties connected to individual
+datatypes and that rely on their inductive nature.
-\item The mutual datatype theorems are properties of mutually recursive groups
-of datatypes.
-\end{enumerate}
+\item The \emph{mutual datatype theorems} are properties associated to mutually
+recursive groups of datatypes.
+\end{itemize}
\noindent
The full list of named theorems can be obtained as usual by entering the
-command \keyw{print_theorems} immediately after the datatype definition.
+command \keyw{print\_theorems} immediately after the datatype definition.
This list normally excludes low-level theorems that reveal internal
constructions. To see these as well, add the following line to the top of your
theory file:
@@ -561,9 +564,87 @@
subsubsection {* Free Constructor Theorems *}
+(*<*)
+ consts is_Cons :: 'a
+(*>*)
+
text {*
- * free ctor theorems
- * case syntax
+The first subgroup of properties are concerned with the constructors.
+They are listed below for @{typ "'a list"}:
+
+\begin{description}
+\item[@{text "t.distinct [simp, induct_simp]"}:] ~ \\
+@{thm list.distinct(1)[no_vars]} \\
+@{thm list.distinct(2)[no_vars]}
+
+\item[@{text "t.inject [iff, induct_simp]"}:] ~ \\
+@{thm list.inject[no_vars]}
+
+\item[@{text "t.exhaust [cases t, case_names C\<^sub>1 \<dots> C\<^sub>n]"}:] ~ \\
+@{thm list.exhaust[no_vars]}
+
+\item[@{text t.nchotomy}:] ~ \\
+@{thm list.nchotomy[no_vars]}
+
+\end{description}
+
+\noindent
+The next subgroup is concerned with the case combinator:
+
+\begin{description}
+\item[@{text "t.case [simp]"}:] ~ \\
+@{thm list.case(1)[no_vars]} \\
+@{thm list.case(2)[no_vars]}
+
+\item[@{text t.case_cong}:] ~ \\
+@{thm list.case_cong[no_vars]}
+
+\item[@{text "t.weak_case_cong [cong]"}:] ~ \\
+@{thm list.weak_case_cong[no_vars]}
+
+\item[@{text t.split}:] ~ \\
+@{thm list.split[no_vars]}
+
+\item[@{text t.split_asm}:] ~ \\
+@{thm list.split_asm[no_vars]}
+
+\item[@{text "t.splits = split split_asm"}]
+
+\end{description}
+
+\noindent
+The third and last subgroup revolves around discriminators and selectors:
+
+\begin{description}
+\item[@{text "discs [simp]"}:] ~ \\
+@{thm list.discs(1)[no_vars]} \\
+@{thm list.discs(2)[no_vars]}
+
+\item[@{text "sels [simp]"}:] ~ \\
+@{thm list.sels(1)[no_vars]} \\
+@{thm list.sels(2)[no_vars]}
+
+\item[@{text "collapse [simp]"}:] ~ \\
+@{thm list.collapse(1)[no_vars]} \\
+@{thm list.collapse(2)[no_vars]}
+
+\item[@{text disc_exclude}:] ~ \\
+These properties are missing for @{typ "'a list"} because there is only one
+proper discriminator. Had the datatype been introduced with a second
+discriminator (@{const is_Cons}), they would have read thusly: \\
+@{prop "null list \<Longrightarrow> \<not> is_Cons list"} \\
+@{prop "is_Cons list \<Longrightarrow> \<not> null list"}
+
+\item[@{text "disc_exhaust [case_names C\<^sub>1 \<dots> C\<^sub>n]]"}:] ~ \\
+@{thm list.disc_exhaust[no_vars]}
+
+\item[@{text expand}:] ~ \\
+@{thm list.expand[no_vars]}
+
+\item[@{text t.case_conv}:] ~ \\
+@{thm list.case_conv[no_vars]}
+
+\end{description}
* Section~\label{sec:generating-free-constructor-theorems}
*}
@@ -607,15 +688,19 @@
Nitpick
* provide exactly the same theorems with the same names (compatibility)
* option 1
- * \keyw{rep_compat}
- * \keyw{rep_datatype}
+ * \keyw{rep\_compat}
+ * \keyw{rep\_datatype}
* has some limitations
* mutually recursive datatypes? (fails with rep_datatype?)
* nested datatypes? (fails with datatype_new?)
* option 2
- * \keyw{datatype_compat}
+ * @{command datatype_new_compat}
* not fully implemented yet?
+@{rail "
+ @@{command_def datatype_new_compat} types
+"}
+
* register old datatype as new datatype
* no clean way yet
* if the goal is to do recursion through old datatypes, can register it as
@@ -971,8 +1056,8 @@
text {*
Definitions of codatatypes have almost exactly the same syntax as for datatypes
(Section~\ref{ssec:datatype-syntax}), with two exceptions: The command is called
-@{command codatatype}; the \keyw{no_discs_sels} option is not available, because
-destructors are a central notion for codatatypes.
+@{command codatatype}; the \keyw{no\_discs\_sels} option is not available,
+because destructors are a central notion for codatatypes.
*}
subsection {* Generated Theorems
@@ -1076,7 +1161,7 @@
old \keyw{datatype}
* @{command wrap_free_constructors}
- * \keyw{no_discs_sels}, \keyw{rep_compat}
+ * \keyw{no\_discs\_sels}, \keyw{rep\_compat}
* hack to have both co and nonco view via locale (cf. ext nats)
*}
@@ -1168,7 +1253,7 @@
based on overloading
* no way to register "sum" and "prod" as (co)datatypes to enable N2M reduction for them
- (for datatype_compat and prim(co)rec)
+ (for @{command datatype_new_compat} and prim(co)rec)
* no way to register same type as both data- and codatatype?