# HG changeset patch # User blanchet # Date 1378911301 -7200 # Node ID 14000a283ce001106428c4034788185b02e7805d # Parent 73d4c76d8eb2dfb3fe547f59f34b9ad922b2f0b9 more (co)data docs diff -r 73d4c76d8eb2 -r 14000a283ce0 src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Wed Sep 11 16:16:45 2013 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Wed Sep 11 16:55:01 2013 +0200 @@ -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 \textit{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}. @@ -121,8 +121,8 @@ \item Section \ref{sec:generating-free-constructor-theorems}, ``Generating Free Constructor Theorems,'' explains how to derive convenience theorems for free -constructors, as performed internally by @{command datatype_new} and -@{command codatatype}. +constructors using the @{command wrap_free_constructors} command, 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. @@ -301,7 +301,7 @@ *} datatype_new 'a wrong = Wrong (*<*)'a - typ (*>*)"'a wrong \ 'a wrong" + typ (*>*)"'a wrong \ 'a" text {* \noindent @@ -312,7 +312,7 @@ datatype_new ('a, 'b) fn = Fn "'a \ 'b" datatype_new 'a also_wrong = Also_Wrong (*<*)'a - typ (*>*)"('a also_wrong, 'a also_wrong) fn" + typ (*>*)"('a also_wrong, 'a) fn" text {* \noindent @@ -456,11 +456,11 @@ \setlength{\itemsep}{0pt} \item -The \keyw{no\_discs\_sels} option indicates that no destructors (i.e., +The \keyw{no_discs_sels} option indicates that no destructors (i.e., discriminators and 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 Section~\ref{ssec:datatype-compatibility-issues} for details. @@ -535,8 +535,8 @@ \begin{enumerate} \item The free constructor theorems are properties about the constructors and -destructors that can be derived for any freely generated type. In particular, -@{command codatatype} also produces these theorems. +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. @@ -546,10 +546,17 @@ \end{enumerate} \noindent -The list of available \keyw{print_theorem} +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 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: +*} -bnf_note_all -*} + declare [[bnf_note_all]] +(*<*) + declare [[bnf_note_all = false]] +(*>*) subsubsection {* Free Constructor Theorems *} @@ -558,7 +565,7 @@ * free ctor theorems * case syntax - * Section~\label{sec:generating-free-constructor-theorems} + * Section~\label{sec:generating-free-constructor-theorems} *} @@ -600,13 +607,13 @@ 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?) + * mutually recursive datatypes? (fails with rep_datatype?) + * nested datatypes? (fails with datatype_new?) * option 2 - * \keyw{datatype\_compat} + * \keyw{datatype_compat} * not fully implemented yet? * register old datatype as new datatype @@ -964,7 +971,7 @@ 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 +@{command codatatype}; the \keyw{no_discs_sels} option is not available, because destructors are a central notion for codatatypes. *} @@ -1069,7 +1076,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) *} @@ -1097,11 +1104,9 @@ X_list is as for BNF +Section~\ref{ssec:datatype-generated-theorems} lists the generated theorems. *} -subsection {* Generated Theorems - \label{ssec:ctors-generated-theorems} *} - section {* Standard ML Interface \label{sec:standard-ml-interface} *} @@ -1149,7 +1154,7 @@ *} text {* -* primrec\_new and primcorec are vaporware +* primcorec is unfinished * slow n-ary mutual (co)datatype, avoid as much as possible (e.g. using nesting) @@ -1163,7 +1168,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 datatype_compat and prim(co)rec) * no way to register same type as both data- and codatatype? diff -r 73d4c76d8eb2 -r 14000a283ce0 src/Doc/ROOT --- a/src/Doc/ROOT Wed Sep 11 16:16:45 2013 +0200 +++ b/src/Doc/ROOT Wed Sep 11 16:55:01 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