# HG changeset patch # User blanchet # Date 1378912678 -7200 # Node ID c6c8dce7e9ab0eb9fd1c54f6a6eac6afaac047e8 # Parent 14000a283ce001106428c4034788185b02e7805d more (co)data docs diff -r 14000a283ce0 -r c6c8dce7e9ab src/Doc/Datatypes/Datatypes.thy --- 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 \ 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 \ \ is_Cons list"} \\ +@{prop "is_Cons list \ \ null list"} + +\item[@{text "disc_exhaust [case_names C\<^sub>1 \ 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?