# HG changeset patch # User blanchet # Date 1392360826 -3600 # Node ID 501df9ad117b0a52bd09085f5dca79a8599b10e6 # Parent c582a7893dcddbfc63b8838b65900097a8f672c6 more (co)datatype docs diff -r c582a7893dcd -r 501df9ad117b src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Fri Feb 14 07:53:46 2014 +0100 +++ b/src/Doc/Datatypes/Datatypes.thy Fri Feb 14 07:53:46 2014 +0100 @@ -480,8 +480,7 @@ datatypes specified by their constructors. The syntactic entity \synt{target} can be used to specify a local -context---e.g., @{text "(in linorder)"}. It is documented in the Isar reference -manual \cite{isabelle-isar-ref}. +context---e.g., @{text "(in linorder)"} \cite{isabelle-isar-ref}. The optional target is potentially followed by datatype-specific options: @@ -511,10 +510,9 @@ \medskip \noindent -The syntactic entity \synt{name} denotes an identifier, \synt{typefree} -denotes fixed type variable (@{typ 'a}, @{typ 'b}, \ldots), and \synt{mixfix} -denotes the usual parenthesized mixfix notation. They are documented in the Isar -reference manual \cite{isabelle-isar-ref}. +The syntactic entity \synt{name} denotes an identifier, \synt{mixfix} denotes +the usual parenthesized mixfix notation, and \synt{typefree} denotes fixed type +variable (@{typ 'a}, @{typ 'b}, \ldots) \cite{isabelle-isar-ref}. The optional names preceding the type variables allow to override the default names of the set functions (@{text set1_t}, \ldots, @{text setM_t}). @@ -541,6 +539,8 @@ \medskip \noindent +The syntactic entity \synt{type} denotes a HOL type \cite{isabelle-isar-ref}. + In addition to the type of a constructor argument, it is possible to specify a name for the corresponding selector to override the default name (@{text un_C\<^sub>ji}). The same selector names can be reused for several @@ -572,30 +572,14 @@ \end{matharray} @{rail \ - @@{command datatype_new_compat} names + @@{command datatype_new_compat} (name +) \} \medskip \noindent -The old datatype package provides some functionality that is not yet -replicated in the new package: - -\begin{itemize} -\setlength{\itemsep}{0pt} - -\item It is integrated with \keyw{fun} and \keyw{function} -\cite{isabelle-function}, Nitpick \cite{isabelle-nitpick}, Quickcheck, -and other packages. - -\item It is extended by various add-ons, notably to produce instances of the -@{const size} function. -\end{itemize} - -\noindent -New-style datatypes can in most cases be registered as old-style datatypes using -@{command datatype_new_compat}. The \textit{names} argument is a space-separated -list of type names that are mutually recursive. For example: +The @{command datatype_new_compat} command registers new-style datatypes as +old-style datatypes. For example: *} datatype_new_compat even_nat odd_nat @@ -609,7 +593,22 @@ ML {* Datatype_Data.get_info @{theory} @{type_name even_nat} *} text {* -A few remarks concern nested recursive datatypes only: +The syntactic entity \synt{name} denotes an identifier \cite{isabelle-isar-ref}. + +The command is interesting because the old datatype package provides some +functionality that is not yet replicated in the new package: + +\begin{itemize} +\setlength{\itemsep}{0pt} + +\item It is integrated with \keyw{fun} \cite{isabelle-function}, +Nitpick \cite{isabelle-nitpick}, Quickcheck, and other packages. + +\item It is extended by various add-ons, notably to produce instances of the +@{const size} function. +\end{itemize} + +A few remarks concern nested recursive datatypes: \begin{itemize} \setlength{\itemsep}{0pt} @@ -620,8 +619,8 @@ \item All types through which recursion takes place must be new-style datatypes or the function type. In principle, it should be possible to support old-style -datatypes as well, but the command does not support this yet (and there is -currently no way to register old-style datatypes as new-style datatypes). +datatypes as well, but this has not been implemented yet (and there is currently +no way to register old-style datatypes as new-style datatypes). \item The recursor produced for types that recurse through functions has a different signature than with the old package. This makes it impossible to use @@ -1375,13 +1374,12 @@ \noindent The @{command primrec_new} command introduces a set of mutually recursive -functions over a datatype. +functions over datatypes. The syntactic entity \synt{target} can be used to specify a local context, -\synt{fixes} is a list of names with optional type signatures, \synt{thmdecl} -is an optional name for the formula that follows, and \synt{prop} is a HOL -proposition. They are is documented in the Isar reference manual -\cite{isabelle-isar-ref}. +\synt{fixes} denotes a list of names with optional type signatures, +\synt{thmdecl} denotes an optional name for the formula that follows, and +\synt{prop} denotes a HOL proposition \cite{isabelle-isar-ref}. %%% TODO: elaborate on format of the equations %%% TODO: elaborate on mutual and nested-to-mutual @@ -2279,14 +2277,13 @@ \medskip \noindent -The @{command primcorec} command introduces a set of mutually corecursive -functions over a codatatype. +The @{command primcorec} and @{command primcorecursive} commands introduce a set +of mutually corecursive functions over codatatypes. The syntactic entity \synt{target} can be used to specify a local context, -\synt{fixes} is a list of names with optional type signatures, \synt{thmdecl} -is an optional name for the formula that follows, and \synt{prop} is a HOL -proposition. They are is documented in the Isar reference manual -\cite{isabelle-isar-ref}. +\synt{fixes} denotes a list of names with optional type signatures, +\synt{thmdecl} denotes an optional name for the formula that follows, and +\synt{prop} denotes a HOL proposition \cite{isabelle-isar-ref}. The optional target is potentially followed by a corecursion-specific option: @@ -2303,9 +2300,9 @@ expressed using the constructor or destructor view cover all possible cases. \end{itemize} -\noindent -The @{command primcorec} command is an abbreviation for @{command primcorecursive} with -@{text "by auto?"} to discharge any emerging proof obligations. +The @{command primcorec} command is an abbreviation for @{command +primcorecursive} with @{text "by auto?"} to discharge any emerging proof +obligations. %%% TODO: elaborate on format of the propositions %%% TODO: elaborate on mutual and nested-to-mutual @@ -2504,7 +2501,7 @@ \end{matharray} @{rail \ - @@{command bnf} target? (name ':')? typ \ + @@{command bnf} target? (name ':')? type \ 'map:' term ('sets:' (term +))? 'bd:' term \ ('wits:' (term +))? ('rel:' term)? \} @@ -2517,9 +2514,11 @@ (functorial action). In addition, custom set functions, relators, and nonemptiness witnesses can be specified; otherwise, default versions are used. -The syntactic entity \synt{target} can be used to specify a local -context---e.g., @{text "(in linorder)"}. It is documented in the Isar -reference manual \cite{isabelle-isar-ref}. +The syntactic entity \synt{target} can be used to specify a local context, +\synt{type} denotes a HOL type, and \synt{term} denotes a HOL term +\cite{isabelle-isar-ref}. + +%%% TODO: elaborate on proof obligations *} @@ -2551,9 +2550,10 @@ (map, set, relator, and cardinal bound) and asserts the BNF properties for these constants as axioms. -The syntactic entity \synt{target} can be used to specify a local -context---e.g., @{text "(in linorder)"}. It is documented in the Isar reference -manual \cite{isabelle-isar-ref}. +The syntactic entity \synt{target} can be used to specify a local context, +\synt{name} denotes an identifier, \synt{typefree} denotes fixed type variable +(@{typ 'a}, @{typ 'b}, \ldots), and \synt{mixfix} denotes the usual +parenthesized mixfix notation \cite{isabelle-isar-ref}. Type arguments are live by default; they can be marked as dead by entering ``-'' (hyphen) instead of an identifier for the corresponding set function. @@ -2638,11 +2638,15 @@ destructors. It also registers the constants and theorems in a data structure that is queried by various tools (e.g., \keyw{function}). -The syntactic entity \synt{target} can be used to specify a local -context---e.g., @{text "(in linorder)"}. It is documented in the Isar reference -manual \cite{isabelle-isar-ref}. - -% options: no_discs_sels no_code +The syntactic entity \synt{target} can be used to specify a local context, +\synt{name} denotes an identifier, and \synt{term} denotes a HOL term +\cite{isabelle-isar-ref}. + +The syntax resembles that of @{command datatype_new} and @{command codatatype} +definitions (Sections +\ref{ssec:datatype-command-syntax}~and~\ref{ssec:codatatype-command-syntax}). +A constructor is specified by an optional name for the discriminator, the +constructor itself (as a term), and a list of optional names for the selectors. Section~\ref{ssec:datatype-generated-theorems} lists the generated theorems. For technical reasons, the @{text "[fundef_cong]"} attribute is not set on the