diff -r 1b4dc8a9f7d9 -r c5f6e2c4472c src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Mon Jan 05 10:09:42 2015 +0100 +++ b/src/Doc/Datatypes/Datatypes.thy Mon Jan 05 11:00:12 2015 +0100 @@ -124,9 +124,9 @@ %\item Section \ref{sec:using-the-standard-ml-interface}, ``Using the Standard ML Interface,'' %describes the package's programmatic interface. -\item Section \ref{sec:controlling-plugins}, ``Controlling Plugins,'' -is concerned with the package's interoperability with other Isabelle packages -and tools, such as the code generator, Transfer, Lifting, and Quickcheck. +\item Section \ref{sec:selecting-plugins}, ``Selecting Plugins,'' is concerned +with the package's interoperability with other Isabelle packages and tools, such +as the code generator, Transfer, Lifting, and Quickcheck. \item Section \ref{sec:known-bugs-and-limitations}, ``Known Bugs and Limitations,'' concludes with known open issues at the time of writing. @@ -184,7 +184,7 @@ text {* \noindent -Here, @{const Truue}, @{const Faalse}, and @{const Perhaaps} have the type @{typ trool}. +@{const Truue}, @{const Faalse}, and @{const Perhaaps} have the type @{typ trool}. Polymorphic types are possible, such as the following option type, modeled after its homologue from the @{theory Option} theory: @@ -198,8 +198,8 @@ text {* \noindent -The constructors are @{text "None :: 'a option"} and -@{text "Some :: 'a \ 'a option"}. +The constructors are @{text "None \ 'a option"} and +@{text "Some \ 'a \ 'a option"}. The next example has three type parameters: *} @@ -209,7 +209,7 @@ text {* \noindent The constructor is -@{text "Triple :: 'a \ 'b \ 'c \ ('a, 'b, 'c) triple"}. +@{text "Triple \ 'a \ 'b \ 'c \ ('a, 'b, 'c) triple"}. Unlike in Standard ML, curried constructors are supported. The uncurried variant is also possible: *} @@ -417,8 +417,8 @@ The \keyw{where} clause at the end of the command specifies a default value for selectors applied to constructors on which they are not a priori specified. -Here, it is used to ensure that the tail of the empty list is itself (instead of -being left unspecified). +In the example, it is used to ensure that the tail of the empty list is itself +(instead of being left unspecified). Because @{const Nil} is nullary, it is also possible to use @{term "\xs. xs = Nil"} as a discriminator. This is the default behavior @@ -471,14 +471,15 @@ \end{matharray} @{rail \ - @@{command datatype} target? @{syntax dt_options}? \ - (@{syntax dt_name} '=' (@{syntax dt_ctor} + '|') \ - @{syntax map_rel}? (@'where' (prop + '|'))? + @'and') + @@{command datatype} target? @{syntax dt_options}? @{syntax dt_spec} ; @{syntax_def dt_options}: '(' ((@{syntax plugins} | 'discs_sels') + ',') ')' ; @{syntax_def plugins}: 'plugins' ('only' | 'del') ':' (name +) ; + @{syntax_def dt_spec}: (@{syntax dt_name} '=' (@{syntax dt_ctor} + '|') \ + @{syntax map_rel}? (@'where' (prop + '|'))? + @'and') + ; @{syntax_def map_rel}: @'for' ((('map' | 'rel') ':' name) +) \} @@ -653,7 +654,7 @@ \noindent In addition, some of the plugins introduce their own constants -(Section~\ref{sec:controlling-plugins}). The case combinator, discriminators, +(Section~\ref{sec:selecting-plugins}). The case combinator, discriminators, and selectors are collectively called \emph{destructors}. The prefix ``@{text "t."}'' is an optional component of the names and is normally hidden. *} @@ -686,7 +687,7 @@ The full list of named theorems can be obtained as usual by entering the command \keyw{print_theorems} immediately after the datatype definition. This list includes theorems produced by plugins -(Section~\ref{sec:controlling-plugins}), but normally excludes low-level +(Section~\ref{sec:selecting-plugins}), but normally excludes low-level theorems that reveal internal constructions. To make these accessible, add the line *} @@ -1104,7 +1105,7 @@ @{const size} in terms of the generic function @{text "t.size_t"}. Moreover, the new function considers nested occurrences of a value, in the nested recursive case. The old behavior can be obtained by disabling the @{text size} -plugin (Section~\ref{sec:controlling-plugins}) and instantiating the +plugin (Section~\ref{sec:selecting-plugins}) and instantiating the @{text size} type class manually. \item \emph{The internal constructions are completely different.} Proof texts @@ -1149,7 +1150,7 @@ text {* Recursive functions over datatypes can be specified using the @{command primrec} command, which supports primitive recursion, or using the more general -\keyw{fun} and \keyw{function} commands. Here, the focus is on +\keyw{fun} and \keyw{function} commands. In this tutorial, the focus is on @{command primrec}; the other two commands are described in a separate tutorial @{cite "isabelle-function"}. @@ -1489,7 +1490,7 @@ @@{command primrec} target? @{syntax pr_options}? fixes \ @'where' (@{syntax pr_equation} + '|') ; - @{syntax_def pr_options}: '(' (('nonexhaustive' | 'transfer') + ',') ')' + @{syntax_def pr_options}: '(' ((@{syntax plugins} | 'nonexhaustive' | 'transfer') + ',') ')' ; @{syntax_def pr_equation}: thmdecl? prop \} @@ -1512,12 +1513,16 @@ \setlength{\itemsep}{0pt} \item -The @{text "nonexhaustive"} option indicates that the functions are not +The @{text plugins} option indicates which plugins should be enabled +(@{text only}) or disabled (@{text del}). By default, all plugins are enabled. + +\item +The @{text nonexhaustive} option indicates that the functions are not necessarily specified for all constructors. It can be used to suppress the warning that is normally emitted when some constructors are missing. \item -The @{text "transfer"} option indicates that an unconditional transfer rule +The @{text transfer} option indicates that an unconditional transfer rule should be generated and proved @{text "by transfer_prover"}. The @{text "[transfer_rule]"} attribute is set on the generated theorem. \end{itemize} @@ -1754,8 +1759,7 @@ \end{matharray} @{rail \ - @@{command codatatype} target? \ - (@{syntax dt_name} '=' (@{syntax dt_ctor} + '|') + @'and') + @@{command codatatype} target? @{syntax dt_options}? @{syntax dt_spec} \} \medskip @@ -1912,9 +1916,9 @@ text {* Corecursive functions can be specified using the @{command primcorec} and \keyw{prim\-corec\-ursive} commands, which support primitive corecursion, or -using the more general \keyw{partial_function} command. Here, the focus is on -the first two. More examples can be found in the directory -\verb|~~/src/HOL/Datatype_Examples|. +using the more general \keyw{partial_function} command. In this tutorial, the +focus is on the first two. More examples can be found in the directory +\verb|~~/src/HOL/Datatype_|\allowbreak\verb|Examples|. Whereas recursive functions consume datatypes one constructor at a time, corecursive functions construct codatatypes one constructor at a time. @@ -2435,7 +2439,7 @@ (@@{command primcorec} | @@{command primcorecursive}) target? \ @{syntax pcr_options}? fixes @'where' (@{syntax pcr_formula} + '|') ; - @{syntax_def pcr_options}: '(' (('sequential' | 'exhaustive' | 'transfer') + ',') ')' + @{syntax_def pcr_options}: '(' ((@{syntax plugins} | 'sequential' | 'exhaustive' | 'transfer') + ',') ')' ; @{syntax_def pcr_formula}: thmdecl? prop (@'of' (term * ))? \} @@ -2458,16 +2462,20 @@ \setlength{\itemsep}{0pt} \item -The @{text "sequential"} option indicates that the conditions in specifications +The @{text plugins} option indicates which plugins should be enabled +(@{text only}) or disabled (@{text del}). By default, all plugins are enabled. + +\item +The @{text sequential} option indicates that the conditions in specifications expressed using the constructor or destructor view are to be interpreted sequentially. \item -The @{text "exhaustive"} option indicates that the conditions in specifications +The @{text exhaustive} option indicates that the conditions in specifications expressed using the constructor or destructor view cover all possible cases. \item -The @{text "transfer"} option indicates that an unconditional transfer rule +The @{text transfer} option indicates that an unconditional transfer rule should be generated and proved @{text "by transfer_prover"}. The @{text "[transfer_rule]"} attribute is set on the generated theorem. \end{itemize} @@ -2832,8 +2840,8 @@ *) -section {* Controlling Plugins - \label{sec:controlling-plugins} *} +section {* Selecting Plugins + \label{sec:selecting-plugins} *} text {* Plugins extend the (co)datatype package to interoperate with other Isabelle @@ -2964,6 +2972,10 @@ \end{description} \end{indentblock} + +For @{command primrec}, @{command primcorec}, and @{command primcorecursive}, +the \hthm{transfer} plugin implements the generation of the @{text "f.transfer"} +property, conditioned by the @{text transfer} option. *} @@ -2998,7 +3010,7 @@ text {* The integration of datatypes with Quickcheck is accomplished by the -\hthm{quickcheck} plugin. It combines a number of subplugins that instantiate +\hthm{quick\-check} plugin. It combines a number of subplugins that instantiate specific type classes. The subplugins can be enabled or disabled individually. They are listed below: