# HG changeset patch # User blanchet # Date 1379082579 -7200 # Node ID da5e1887d7a74f769a47558e95cc41827d6f3c02 # Parent ff37dc246b1012cf5970849e065a2c3b94c42f64 more (co)data doc diff -r ff37dc246b10 -r da5e1887d7a7 src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Tue Aug 20 17:34:11 2013 +0900 +++ b/src/Doc/Datatypes/Datatypes.thy Fri Sep 13 16:29:39 2013 +0200 @@ -1,5 +1,8 @@ (* Title: Doc/Datatypes/Datatypes.thy Author: Jasmin Blanchette, TU Muenchen + Author: Lorenz Panny, TU Muenchen + Author: Andrei Popescu, TU Muenchen + Author: Dmitriy Traytel, TU Muenchen Tutorial for (co)datatype definitions with the new package. *) @@ -122,21 +125,21 @@ to register arbitrary type constructors as BNFs. \item Section -\ref{sec:generating-destructors-and-theorems-for-free-constructors}, -``Generating Destructors and Theorems for Free Constructors,'' explains how to +\ref{sec:deriving-destructors-and-theorems-for-free-constructors}, +``Deriving Destructors and Theorems for Free Constructors,'' explains how to use the command @{command wrap_free_constructors} to derive destructor constants and theorems for freely generated types, as performed internally by @{command datatype_new} and @{command codatatype}. -\item Section \ref{sec:standard-ml-interface}, ``Standard ML Interface,'' -describes the package's programmatic interface. +%\item Section \ref{sec:standard-ml-interface}, ``Standard ML Interface,'' +%describes the package's programmatic interface. -\item Section \ref{sec:interoperability}, ``Interoperability,'' -is concerned with the packages' interaction with other Isabelle packages and -tools, such as the code generator and the counterexample generators. +%\item Section \ref{sec:interoperability}, ``Interoperability,'' +%is concerned with the packages' interaction with other Isabelle packages and +%tools, such as the code generator and the counterexample generators. -\item Section \ref{sec:known-bugs-and-limitations}, ``Known Bugs and -Limitations,'' concludes with known open issues at the time of writing. +%\item Section \ref{sec:known-bugs-and-limitations}, ``Known Bugs and +%Limitations,'' concludes with known open issues at the time of writing. \end{itemize} @@ -181,8 +184,8 @@ *} -subsection {* Examples - \label{ssec:datatype-examples} *} +subsection {* Introductory Examples + \label{ssec:datatype-introductory-examples} *} subsubsection {* Nonrecursive Types *} @@ -333,48 +336,16 @@ *} -subsubsection {* Auxiliary Constants and Syntaxes *} +subsubsection {* Custom Names and Syntaxes *} text {* The @{command datatype_new} command introduces various constants in addition to -the constructors. Given a type @{text "('a\<^sub>1, \, 'a\<^sub>m) t"} -with $m > 0$ live type variables and $n$ constructors -@{text "t.C\<^sub>1"}, \ldots, @{text "t.C\<^sub>n"}, the -following auxiliary constants are introduced (among others): - -\begin{itemize} -\setlength{\itemsep}{0pt} - -\item \relax{Case combinator}: @{text t_case} (rendered using the familiar -@{text case}--@{text of} syntax) - -\item \relax{Iterator}: @{text t_fold} - -\item \relax{Recursor}: @{text t_rec} - -\item \relax{Discriminators}: @{text "t.is_C\<^sub>1"}, \ldots, -@{text "t.is_C\<^sub>n"} - -\item \relax{Selectors}: -@{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_C\<^sub>n1}$, \ldots, @{text t.un_C\<^sub>nk\<^sub>n}. - -\item \relax{Set functions} (or \relax{natural transformations}): -@{text t_set1}, \ldots, @{text t_setm} - -\item \relax{Map function} (or \relax{functorial action}): @{text t_map} - -\item \relax{Relator}: @{text t_rel} - -\end{itemize} - -\noindent -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: +the constructors. With each datatype are associated set functions, a map +function, a relator, discriminators, and selectors, all of which can be given +custom names. In the example below, the traditional names +@{text set}, @{text map}, @{text list_all2}, @{text null}, @{text hd}, and +@{text tl} override the default names @{text list_set}, @{text list_map}, @{text +list_rel}, @{text is_Nil}, @{text un_Cons1}, and @{text un_Cons2}: *} (*<*) @@ -413,7 +384,7 @@ to ensure that the tail of the empty list is itself (instead of being left unspecified). -Because @{const Nil} is a nullary constructor, it is also possible to use +Because @{const Nil} is nullary, it is also possible to use @{term "\xs. xs = Nil"} as a discriminator. This is specified by entering ``@{text "="}'' instead of the identifier @{const null}. Although this may look appealing, the mixture of constructors and selectors in the @@ -449,8 +420,11 @@ "[x]" == "x # []" -subsection {* Syntax - \label{ssec:datatype-syntax} *} +subsection {* Command Syntax + \label{ssec:datatype-command-syntax} *} + + +subsubsection {* \keyw{datatype\_new} *} text {* Datatype definitions have the following general syntax: @@ -543,6 +517,59 @@ (i.e., it may depends on @{text C}'s arguments). *} + +subsubsection {* \keyw{datatype\_new\_compat} *} + +text {* +@{rail " + @@{command_def datatype_new_compat} types +"} +*} + + +subsection {* Generated Constants + \label{ssec:datatype-generated-constants} *} + +text {* +Given a type @{text "('a\<^sub>1, \, 'a\<^sub>m) t"} +with $m > 0$ live type variables and $n$ constructors +@{text "t.C\<^sub>1"}, \ldots, @{text "t.C\<^sub>n"}, the +following auxiliary constants are introduced: + +\begin{itemize} +\setlength{\itemsep}{0pt} + +\item \relax{Case combinator}: @{text t_case} (rendered using the familiar +@{text case}--@{text of} syntax) + +\item \relax{Discriminators}: @{text "t.is_C\<^sub>1"}, \ldots, +@{text "t.is_C\<^sub>n"} + +\item \relax{Selectors}: +@{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_C\<^sub>n1}$, \ldots, @{text t.un_C\<^sub>nk\<^sub>n}. + +\item \relax{Set functions} (or \relax{natural transformations}): +@{text t_set1}, \ldots, @{text t_setm} + +\item \relax{Map function} (or \relax{functorial action}): @{text t_map} + +\item \relax{Relator}: @{text t_rel} + +\item \relax{Iterator}: @{text t_fold} + +\item \relax{Recursor}: @{text t_rec} + +\end{itemize} + +\noindent +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. +*} + + subsection {* Generated Theorems \label{ssec:datatype-generated-theorems} *} @@ -744,47 +771,45 @@ *} +(* subsection {* Compatibility Issues \label{ssec:datatype-compatibility-issues} *} text {* - * main incompabilities between two packages - * differences in theorem names (e.g. singular vs. plural for some props?) - * differences in "simps"? - * different recursor/induction in nested case - * discussed in Section~\ref{sec:defining-recursive-functions} - * different ML interfaces / extension mechanisms +% * main incompabilities between two packages +% * differences in theorem names (e.g. singular vs. plural for some props?) +% * differences in "simps"? +% * different recursor/induction in nested case +% * discussed in Section~\ref{sec:defining-recursive-functions} +% * different ML interfaces / extension mechanisms +% +% * register new datatype as old datatype +% * motivation: +% * do recursion through new datatype in old datatype +% (e.g. useful when porting to the new package one type at a time) +% * use old primrec +% * use fun +% * use extensions like size (needed for fun), the AFP order, Quickcheck, +% Nitpick +% * provide exactly the same theorems with the same names (compatibility) +% * option 1 +% * \keyw{rep\_compat} +% * \keyw{rep\_datatype} +% * has some limitations +% * mutually recursive datatypes? (fails with rep_datatype?) +% * nested datatypes? (fails with datatype_new?) +% * option 2 +% * @{command datatype_new_compat} +% * not fully implemented yet? - * register new datatype as old datatype - * motivation: - * do recursion through new datatype in old datatype - (e.g. useful when porting to the new package one type at a time) - * use old primrec - * use fun - * use extensions like size (needed for fun), the AFP order, Quickcheck, - Nitpick - * provide exactly the same theorems with the same names (compatibility) - * option 1 - * \keyw{rep\_compat} - * \keyw{rep\_datatype} - * has some limitations - * mutually recursive datatypes? (fails with rep_datatype?) - * nested datatypes? (fails with datatype_new?) - * option 2 - * @{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 - a BNF (Section XXX) - * can also derive destructors etc. using @{command wrap_free_constructors} - (Section XXX) +% * register old datatype as new datatype +% * no clean way yet +% * if the goal is to do recursion through old datatypes, can register it as +% a BNF (Section XXX) +% * can also derive destructors etc. using @{command wrap_free_constructors} +% (Section XXX) *} +*) section {* Defining Recursive Functions @@ -804,13 +829,13 @@ More examples in \verb|~~/src/HOL/BNF/Examples|. *} -subsection {* Examples - \label{ssec:primrec-examples} *} +subsection {* Introductory Examples + \label{ssec:primrec-introductory-examples} *} subsubsection {* Nonrecursive Types *} text {* - * simple (depth 1) pattern matching on the left-hand side +% * simple (depth 1) pattern matching on the left-hand side *} primrec_new bool_of_trool :: "trool \ bool" where @@ -818,10 +843,10 @@ "bool_of_trool Truue = True" text {* - * OK to specify the cases in a different order - * OK to leave out some case (but get a warning -- maybe we need a "quiet" - or "silent" flag?) - * case is then unspecified +% * OK to specify the cases in a different order +% * OK to leave out some case (but get a warning -- maybe we need a "quiet" +% or "silent" flag?) +% * case is then unspecified More examples: *} @@ -954,9 +979,9 @@ subsubsection {* Nested-as-Mutual Recursion *} text {* - * can pretend a nested type is mutually recursive (if purely inductive) - * avoids the higher-order map - * e.g. +% * can pretend a nested type is mutually recursive (if purely inductive) +% * avoids the higher-order map +% * e.g. *} primrec_new @@ -982,34 +1007,36 @@ "sum_btree_option (Some t) = sum_btree t" text {* - * this can always be avoided; - * e.g. in our previous example, we first mapped the recursive - calls, then we used a generic at function to retrieve the result - - * there's no hard-and-fast rule of when to use one or the other, - just like there's no rule when to use fold and when to use - primrec_new - - * higher-order approach, considering nesting as nesting, is more - compositional -- e.g. we saw how we could reuse an existing polymorphic - at or the_default, whereas @{text at_trees\<^sub>f\<^sub>f} is much more specific - - * but: - * is perhaps less intuitive, because it requires higher-order thinking - * may seem inefficient, and indeed with the code generator the - mutually recursive version might be nicer - * is somewhat indirect -- must apply a map first, then compute a result - (cannot mix) - * the auxiliary functions like @{text at_trees\<^sub>f\<^sub>f} are sometimes useful in own right - - * impact on automation unclear - -%%% TODO: change text antiquotation to const once the real primrec is used +% * this can always be avoided; +% * e.g. in our previous example, we first mapped the recursive +% calls, then we used a generic at function to retrieve the result +% +% * there's no hard-and-fast rule of when to use one or the other, +% just like there's no rule when to use fold and when to use +% primrec_new +% +% * higher-order approach, considering nesting as nesting, is more +% compositional -- e.g. we saw how we could reuse an existing polymorphic +% at or the_default, whereas @{const at_trees\<^sub>f\<^sub>f} is much more specific +% +% * but: +% * is perhaps less intuitive, because it requires higher-order thinking +% * may seem inefficient, and indeed with the code generator the +% mutually recursive version might be nicer +% * is somewhat indirect -- must apply a map first, then compute a result +% (cannot mix) +% * the auxiliary functions like @{const at_trees\<^sub>f\<^sub>f} are sometimes useful in own right +% +% * impact on automation unclear +% *} -subsection {* Syntax - \label{ssec:primrec-syntax} *} +subsection {* Command Syntax + \label{ssec:primrec-command-syntax} *} + + +subsubsection {* \keyw{primrec\_new} *} text {* Primitive recursive functions have the following general syntax: @@ -1027,14 +1054,14 @@ \label{ssec:primrec-generated-theorems} *} text {* - * synthesized nonrecursive definition - * user specification is rederived from it, exactly as entered - - * induct - * mutualized - * without some needless induction hypotheses if not used - * fold, rec - * mutualized +% * synthesized nonrecursive definition +% * user specification is rederived from it, exactly as entered +% +% * induct +% * mutualized +% * without some needless induction hypotheses if not used +% * fold, rec +% * mutualized *} subsection {* Recursive Default Values for Selectors @@ -1093,18 +1120,20 @@ by (cases xs) auto +(* subsection {* Compatibility Issues - \label{ssec:datatype-compatibility-issues} *} + \label{ssec:primrec-compatibility-issues} *} text {* - * different induction in nested case - * solution: define nested-as-mutual functions with primrec, - and look at .induct - - * different induction and recursor in nested case - * only matters to low-level users; they can define a dummy function to force - generation of mutualized recursor +% * different induction in nested case +% * solution: define nested-as-mutual functions with primrec, +% and look at .induct +% +% * different induction and recursor in nested case +% * only matters to low-level users; they can define a dummy function to force +% generation of mutualized recursor *} +*) section {* Defining Codatatypes @@ -1114,29 +1143,34 @@ This section describes how to specify codatatypes using the @{command codatatype} command. - * libraries include some useful codatatypes, notably lazy lists; - see the ``Coinductive'' AFP entry \cite{xxx} for an elaborate library +% * libraries include some useful codatatypes, notably lazy lists; +% see the ``Coinductive'' AFP entry \cite{xxx} for an elaborate library *} -subsection {* Examples - \label{ssec:codatatype-examples} *} +subsection {* Introductory Examples + \label{ssec:codatatype-introductory-examples} *} text {* More examples in \verb|~~/src/HOL/BNF/Examples|. *} -subsection {* Syntax - \label{ssec:codatatype-syntax} *} +subsection {* Command Syntax + \label{ssec:codatatype-command-syntax} *} 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. +(Section~\ref{ssec:datatype-command-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. *} + +subsection {* Generated Constants + \label{ssec:codatatype-generated-constants} *} + + subsection {* Generated Theorems \label{ssec:codatatype-generated-theorems} *} @@ -1153,8 +1187,8 @@ *} -subsection {* Examples - \label{ssec:primcorec-examples} *} +subsection {* Introductory Examples + \label{ssec:primcorec-introductory-examples} *} text {* More examples in \verb|~~/src/HOL/BNF/Examples|. @@ -1164,8 +1198,11 @@ *} -subsection {* Syntax - \label{ssec:primcorec-syntax} *} +subsection {* Command Syntax + \label{ssec:primcorec-command-syntax} *} + + +subsubsection {* \keyw{primcorec} *} text {* Primitive corecursive definitions have the following general syntax: @@ -1191,26 +1228,27 @@ recursion through custom well-behaved type constructors. The key concept is that of a bounded natural functor (BNF). - * @{command bnf} - * @{command print_bnfs} *} -subsection {* Example - \label{ssec:bnf-examples} *} +subsection {* Introductory Example + \label{ssec:bnf-introductory-example} *} text {* More examples in \verb|~~/src/HOL/BNF/Basic_BNFs.thy| and \verb|~~/src/HOL/BNF/More_BNFs.thy|. -Mention distinction between live and dead type arguments; - * and existence of map, set for those -mention =>. +%Mention distinction between live and dead type arguments; +% * and existence of map, set for those +%mention =>. *} -subsection {* Syntax - \label{ssec:bnf-syntax} *} +subsection {* Command Syntax + \label{ssec:bnf-command-syntax} *} + + +subsubsection {* \keyw{bnf} *} text {* @{rail " @@ -1223,31 +1261,42 @@ options: no_discs_sels rep_compat *} -section {* Generating Destructors and Theorems for Free Constructors - \label{sec:generating-destructors-and-theorems-for-free-constructors} *} + +subsubsection {* \keyw{print\_bnfs} *} + +text {* +@{command print_bnfs} +*} + + +section {* Deriving Destructors and Theorems for Free Constructors + \label{sec:deriving-destructors-and-theorems-for-free-constructors} *} text {* This section explains how to derive convenience theorems for free constructors, as performed internally by @{command datatype_new} and @{command codatatype}. - * need for this is rare but may arise if you want e.g. to add destructors to - a type not introduced by ... - - * also useful for compatibility with old package, e.g. add destructors to - old \keyw{datatype} - - * @{command wrap_free_constructors} - * \keyw{no\_discs\_sels}, \keyw{rep\_compat} - * hack to have both co and nonco view via locale (cf. ext nats) +% * need for this is rare but may arise if you want e.g. to add destructors to +% a type not introduced by ... +% +% * also useful for compatibility with old package, e.g. add destructors to +% old \keyw{datatype} +% +% * @{command wrap_free_constructors} +% * \keyw{no\_discs\_sels}, \keyw{rep\_compat} +% * hack to have both co and nonco view via locale (cf. ext nats) *} -subsection {* Example - \label{ssec:ctors-examples} *} +subsection {* Introductory Example + \label{ssec:ctors-introductory-example} *} -subsection {* Syntax - \label{ssec:ctors-syntax} *} +subsection {* Command Syntax + \label{ssec:ctors-command-syntax} *} + + +subsubsection {* \keyw{wrap\_free\_constructors} *} text {* Free constructor wrapping has the following general syntax: @@ -1261,22 +1310,25 @@ @{syntax_def name_term}: (name ':' term) "} -options: no_discs_sels rep_compat +% options: no_discs_sels rep_compat -X_list is as for BNF +% X_list is as for BNF Section~\ref{ssec:datatype-generated-theorems} lists the generated theorems. *} +(* section {* Standard ML Interface \label{sec:standard-ml-interface} *} text {* This section describes the package's programmatic interface. *} +*) +(* section {* Interoperability \label{sec:interoperability} *} @@ -1305,8 +1357,10 @@ subsection {* Nominal Isabelle \label{ssec:nominal-isabelle} *} +*) +(* section {* Known Bugs and Limitations \label{sec:known-bugs-and-limitations} *} @@ -1315,27 +1369,27 @@ *} text {* -* primcorec is unfinished - -* slow n-ary mutual (co)datatype, avoid as much as possible (e.g. using nesting) - -* issues with HOL-Proofs? - -* partial documentation - -* too much output by commands like "datatype_new" and "codatatype" - -* no direct way to define recursive functions for default values -- but show trick - based on overloading - -* no way to register "sum" and "prod" as (co)datatypes to enable N2M reduction for them - (for @{command datatype_new_compat} and prim(co)rec) - -* no way to register same type as both data- and codatatype? - -* no recursion through unused arguments (unlike with the old package) - -* in a locale, cannot use locally fixed types (because of limitation in typedef)? +%* primcorec is unfinished +% +%* slow n-ary mutual (co)datatype, avoid as much as possible (e.g. using nesting) +% +%* issues with HOL-Proofs? +% +%* partial documentation +% +%* too much output by commands like "datatype_new" and "codatatype" +% +%* no direct way to define recursive functions for default values -- but show trick +% based on overloading +% +%* no way to register "sum" and "prod" as (co)datatypes to enable N2M reduction for them +% (for @{command datatype_new_compat} and prim(co)rec) +% +%* no way to register same type as both data- and codatatype? +% +%* no recursion through unused arguments (unlike with the old package) +% +%* in a locale, cannot use locally fixed types (because of limitation in typedef)? *} @@ -1343,13 +1397,15 @@ \label{sec:acknowledgments} *} text {* -Tobias Nipkow and Makarius Wenzel made this work possible. Andreas Lochbihler -provided lots of comments on earlier versions of the package, especially for the -coinductive part. Brian Huffman suggested major simplifications to the internal -constructions, much of which has yet to be implemented. Florian Haftmann and -Christian Urban provided general advice advice on Isabelle and package writing. -Stefan Milius and Lutz Schr\"oder suggested an elegant proof to eliminate one of -the BNF assumptions. +Tobias Nipkow and Makarius Wenzel have encouraged us to implement the new +(co)datatype package. Andreas Lochbihler provided lots of comments on earlier +versions of the package, especially for the coinductive part. Brian Huffman +suggested major simplifications to the internal constructions, much of which has +yet to be implemented. Florian Haftmann and Christian Urban provided general +advice advice on Isabelle and package writing. Stefan Milius and Lutz Schr\"oder +suggested an elegant proof to eliminate one of the BNF assumptions. *} +*) + end diff -r ff37dc246b10 -r da5e1887d7a7 src/Doc/Datatypes/document/root.tex --- a/src/Doc/Datatypes/document/root.tex Tue Aug 20 17:34:11 2013 +0900 +++ b/src/Doc/Datatypes/document/root.tex Fri Sep 13 16:29:39 2013 +0200 @@ -24,7 +24,7 @@ \newenvironment{indentblock}{\list{}{}\item[]}{\endlist} -\newcommand{\keyw}[1]{\isacommand{#1}} +\newcommand{\keyw}[1]{\textbf{#1}} \newcommand{\synt}[1]{\textit{#1}} \newcommand{\hthm}[1]{\textbf{\textit{#1}}} diff -r ff37dc246b10 -r da5e1887d7a7 src/Doc/ROOT --- a/src/Doc/ROOT Tue Aug 20 17:34:11 2013 +0900 +++ b/src/Doc/ROOT Fri Sep 13 16:29:39 2013 +0200 @@ -38,7 +38,7 @@ "document/style.sty" session Datatypes (doc) in "Datatypes" = "HOL-BNF" + - options [document_variants = "datatypes"] + options [document_variants = "datatypes", document_output = "/tmp/isa-output"] theories [document = false] Setup theories Datatypes files