# HG changeset patch
# User blanchet
# Date 1378936547 -7200
# Node ID eed6efba4e3f685ca4471523519ac6a76552a0af
# Parent  7b779c075de9b50f9a2a01a9da9d6a015fe28017
more (co)datatype docs

diff -r 7b779c075de9 -r eed6efba4e3f src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Wed Sep 11 22:20:45 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Wed Sep 11 23:55:47 2013 +0200
@@ -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 @{text "HOL-BNF"} image. The following commands show
+can be precompiled into the \texttt{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:
 *}
@@ -94,7 +94,9 @@
 \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}.
+\cite{traytel-et-al-2012,blanchette-et-al-wit}. The central notion is that of a
+\emph{bounded natural functor} (BNF)---a well-behaved type constructor for which
+nested (co)recursion is supported.
 
 This tutorial is organized as follows:
 
@@ -116,13 +118,15 @@
 @{command primcorec} command.
 
 \item Section \ref{sec:registering-bounded-natural-functors}, ``Registering
-Bounded Natural Functors,'' explains how to set up the package to allow nested
-recursion through custom well-behaved type constructors.
+Bounded Natural Functors,'' explains how to use the @{command bnf} command
+to register arbitrary type constructors as BNFs.
 
-\item Section \ref{sec:generating-free-constructor-theorems}, ``Generating Free
-Constructor Theorems,'' explains how to derive convenience theorems for free
-constructors using the @{command wrap_free_constructors} command, as performed
-internally by @{command datatype_new} and @{command codatatype}.
+\item Section
+\ref{sec:generating-destructors-and-theorems-for-free-constructors},
+``Generating 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.
@@ -163,7 +167,6 @@
 for its appearance. If you have ideas regarding material that should be
 included, please let the authors know.
 \end{framed}
-
 *}
 
 
@@ -253,17 +256,17 @@
 
 text {*
 \noindent
-Nonatomic types must be enclosed in double quotes on the right-hand side of the
-equal sign, as is customary in Isabelle.
+Occurrences of nonatomic types on the right-hand side of the equal sign must be
+enclosed in double quotes, as is customary in Isabelle.
 *}
 
 
 subsubsection {* Mutual Recursion *}
 
 text {*
-\emph{Mutually recursive} types are introduced simultaneously and may refer to each
-other. The example below introduces a pair of types for even and odd natural
-numbers:
+\emph{Mutually recursive} types are introduced simultaneously and may refer to
+each other. The example below introduces a pair of types for even and odd
+natural numbers:
 *}
 
     datatype_new enat = EZero | ESuc onat
@@ -321,6 +324,12 @@
 @{text 'a\<^sub>m}. These type arguments are called \emph{live}; the remaining
 type arguments are called \emph{dead}. In @{typ "'a \<Rightarrow> 'b"} and
 @{typ "('a, 'b) fn"}, the type variable @{typ 'a} is dead and @{typ 'b} is live.
+
+Type constructors must be registered as bounded natural functors (BNFs) to have
+live arguments. This is done automatically for datatypes and codatatypes
+introduced by the @{command datatype_new} and @{command codatatype} commands.
+Section~\ref{sec:registering-bounded-natural-functors} explains how to register
+arbitrary type constructors as BNFs.
 *}
 
 
@@ -418,8 +427,9 @@
 (*<*)
     end
 (*>*)
-    datatype_new ('a, 'b) prod (infixr "*" 20) =
-      Pair 'a 'b
+    datatype_new ('a, 'b) prod (infixr "*" 20) = Pair 'a 'b
+
+text {* \blankline *}
 
     datatype_new (set: 'a) list (map: map rel: list_all2) =
       null: Nil ("[]")
@@ -432,6 +442,8 @@
 
     syntax "_list" :: "args \<Rightarrow> 'a list" ("[(_)]")
 
+text {* \blankline *}
+
     translations
       "[x, xs]" == "x # [xs]"
       "[x]" == "x # []"
@@ -542,16 +554,19 @@
 and destructors that can be derived for any freely generated type. Internally,
 the derivation is performed by @{command wrap_free_constructors}.
 
-\item The \emph{inductive theorems} are properties of datatypes that rely on
+\item The \emph{functorial theorems} are properties of datatypes related to
+their BNF nature.
+
+\item The \emph{inductive theorems} are properties of datatypes related to
 their inductive nature.
+
 \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.
 This list normally excludes low-level theorems that reveal internal
-constructions. To make these accessible, add the following line to the top of your
-theory file:
+constructions. To make these accessible, add the line
 *}
 
     declare [[bnf_note_all]]
@@ -559,6 +574,10 @@
     declare [[bnf_note_all = false]]
 (*>*)
 
+text {*
+\noindent
+to the top of the theory file.
+*}
 
 subsubsection {* Free Constructor Theorems *}
 
@@ -570,134 +589,157 @@
 The first subgroup of properties are concerned with the constructors.
 They are listed below for @{typ "'a list"}:
 
+\begin{indentblock}
 \begin{description}
 
-\item[@{text "t."}\hthm{inject} @{text "[iff, induct_simp]"}:] ~ \\
+\item[@{text "t."}\hthm{inject} @{text "[iff, induct_simp]"}\upshape:] ~ \\
 @{thm list.inject[no_vars]}
 
-\item[@{text "t."}\hthm{distinct} @{text "[simp, induct_simp]"}:] ~ \\
+\item[@{text "t."}\hthm{distinct} @{text "[simp, induct_simp]"}\upshape:] ~ \\
 @{thm list.distinct(1)[no_vars]} \\
 @{thm list.distinct(2)[no_vars]}
 
-\item[@{text "t."}\hthm{exhaust} @{text "[cases t, case_names C\<^sub>1 \<dots> C\<^sub>n]"}:] ~ \\
+\item[@{text "t."}\hthm{exhaust} @{text "[cases t, case_names C\<^sub>1 \<dots> C\<^sub>n]"}\upshape:] ~ \\
 @{thm list.exhaust[no_vars]}
 
-\item[@{text "t."}\hthm{nchotomy}:] ~ \\
+\item[@{text "t."}\hthm{nchotomy}\upshape:] ~ \\
 @{thm list.nchotomy[no_vars]}
 
 \end{description}
+\end{indentblock}
 
 \noindent
 The next subgroup is concerned with the case combinator:
 
+\begin{indentblock}
 \begin{description}
 
-\item[@{text "t."}\hthm{case} @{text "[simp]"}:] ~ \\
+\item[@{text "t."}\hthm{case} @{text "[simp]"}\upshape:] ~ \\
 @{thm list.case(1)[no_vars]} \\
 @{thm list.case(2)[no_vars]}
 
-\item[@{text "t."}\hthm{case\_cong}:] ~ \\
+\item[@{text "t."}\hthm{case\_cong}\upshape:] ~ \\
 @{thm list.case_cong[no_vars]}
 
-\item[@{text "t."}\hthm{weak\_case\_cong} @{text "[cong]"}:] ~ \\
+\item[@{text "t."}\hthm{weak\_case\_cong} @{text "[cong]"}\upshape:] ~ \\
 @{thm list.weak_case_cong[no_vars]}
 
-\item[@{text "t."}\hthm{split}:] ~ \\
+\item[@{text "t."}\hthm{split}\upshape:] ~ \\
 @{thm list.split[no_vars]}
 
-\item[@{text "t."}\hthm{split\_asm}:] ~ \\
+\item[@{text "t."}\hthm{split\_asm}\upshape:] ~ \\
 @{thm list.split_asm[no_vars]}
 
 \item[@{text "t."}\hthm{splits} = @{text "split split_asm"}]
 
 \end{description}
+\end{indentblock}
 
 \noindent
 The third and last subgroup revolves around discriminators and selectors:
 
+\begin{indentblock}
 \begin{description}
 
-\item[@{text "t."}\hthm{discs} @{text "[simp]"}:] ~ \\
+\item[@{text "t."}\hthm{discs} @{text "[simp]"}\upshape:] ~ \\
 @{thm list.discs(1)[no_vars]} \\
 @{thm list.discs(2)[no_vars]}
 
-\item[@{text "t."}\hthm{sels} @{text "[simp]"}:] ~ \\
+\item[@{text "t."}\hthm{sels} @{text "[simp]"}\upshape:] ~ \\
 @{thm list.sels(1)[no_vars]} \\
 @{thm list.sels(2)[no_vars]}
 
-\item[@{text "t."}\hthm{collapse} @{text "[simp]"}:] ~ \\
+\item[@{text "t."}\hthm{collapse} @{text "[simp]"}\upshape:] ~ \\
 @{thm list.collapse(1)[no_vars]} \\
 @{thm list.collapse(2)[no_vars]}
 
-\item[@{text "t."}\hthm{disc\_exclude}:] ~ \\
+\item[@{text "t."}\hthm{disc\_exclude}\upshape:] ~ \\
 These properties are missing for @{typ "'a list"} because there is only one
 proper discriminator. Had the datatype been introduced with a second
 discriminator called @{const is_Cons}, they would have read thusly: \\[\jot]
 @{prop "null list \<Longrightarrow> \<not> is_Cons list"} \\
 @{prop "is_Cons list \<Longrightarrow> \<not> null list"}
 
-\item[@{text "t."}\hthm{disc\_exhaust} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}:] ~ \\
+\item[@{text "t."}\hthm{disc\_exhaust} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\upshape:] ~ \\
 @{thm list.disc_exhaust[no_vars]}
 
-\item[@{text "t."}\hthm{expand}:] ~ \\
+\item[@{text "t."}\hthm{expand}\upshape:] ~ \\
 @{thm list.expand[no_vars]}
 
-\item[@{text "t."}\hthm{case\_conv}:] ~ \\
+\item[@{text "t."}\hthm{case\_conv}\upshape:] ~ \\
 @{thm list.case_conv[no_vars]}
 
 \end{description}
+\end{indentblock}
+*}
+
+
+subsubsection {* Functorial Theorems *}
+
+text {*
+The BNF-related theorem are listed below:
+
+\begin{indentblock}
+\begin{description}
+
+\item[@{text "t."}\hthm{sets} @{text "[code]"}\upshape:] ~ \\
+@{thm list.sets(1)[no_vars]} \\
+@{thm list.sets(2)[no_vars]}
+
+\item[@{text "t."}\hthm{map} @{text "[code]"}\upshape:] ~ \\
+@{thm list.map(1)[no_vars]} \\
+@{thm list.map(2)[no_vars]}
+
+\item[@{text "t."}\hthm{rel\_inject} @{text "[code]"}\upshape:] ~ \\
+@{thm list.rel_inject(1)[no_vars]} \\
+@{thm list.rel_inject(2)[no_vars]}
+
+\item[@{text "t."}\hthm{rel\_distinct} @{text "[code]"}\upshape:] ~ \\
+@{thm list.rel_distinct(1)[no_vars]} \\
+@{thm list.rel_distinct(2)[no_vars]}
+
+\end{description}
+\end{indentblock}
 *}
 
 
 subsubsection {* Inductive Theorems *}
 
 text {*
+The inductive theorems are listed below:
 
+\begin{indentblock}
 \begin{description}
 
-\item[@{text "t."}\hthm{induct} @{text "[induct t, case_names C\<^sub>1 \<dots> C\<^sub>n]"}:] ~ \\
+\item[@{text "t."}\hthm{induct} @{text "[induct t, case_names C\<^sub>1 \<dots> C\<^sub>n]"}\upshape:] ~ \\
 @{thm list.induct[no_vars]}
 
-\item[@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{induct}: @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}:] ~ \\
+\item[@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{induct} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\upshape:] ~ \\
 Given $m > 1$ mutually recursive datatypes, this induction rule can be used to
 prove $m$ properties simultaneously.
 
-\item[@{text "t."}\hthm{fold} @{text "[code]"}:] ~ \\
+\item[@{text "t."}\hthm{fold} @{text "[code]"}\upshape:] ~ \\
 @{thm list.fold(1)[no_vars]} \\
 @{thm list.fold(2)[no_vars]}
 
-\item[@{text "t."}\hthm{rec} @{text "[code]"}:] ~ \\
+\item[@{text "t."}\hthm{rec} @{text "[code]"}\upshape:] ~ \\
 @{thm list.rec(1)[no_vars]} \\
 @{thm list.rec(2)[no_vars]}
 
-\item[@{text "t."}\hthm{sets}: @{text "[code]"}] ~ \\
-@{thm list.sets(1)[no_vars]} \\
-@{thm list.sets(2)[no_vars]}
-
-\item[@{text "t."}\hthm{map}: @{text "[code]"}] ~ \\
-@{thm list.map(1)[no_vars]} \\
-@{thm list.map(2)[no_vars]}
-
-\item[@{text "t."}\hthm{rel\_inject} @{text "[code]"}:] ~ \\
-@{thm list.rel_inject(1)[no_vars]} \\
-@{thm list.rel_inject(2)[no_vars]}
-
-\item[@{text "t."}\hthm{rel\_distinct} @{text "[code]"}:] ~ \\
-@{thm list.rel_distinct(1)[no_vars]} \\
-@{thm list.rel_distinct(2)[no_vars]}
-
 \end{description}
+\end{indentblock}
 
 \noindent
 For convenience, @{command datatype_new} also provides the following collection:
 
+\begin{indentblock}
 \begin{description}
 
 \item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.rec} @{text t.fold} @{text t.map} @{text t.rel_inject}] ~ \\
 @{text t.rel_distinct} @{text t.sets}
 
 \end{description}
-
+\end{indentblock}
 *}
 
 
@@ -1170,7 +1212,6 @@
   \label{ssec:bnf-syntax} *}
 
 text {*
-
 @{rail "
   @@{command_def bnf} target? (name ':')? term \\
     term_list term term_list term?
@@ -1181,8 +1222,8 @@
 options: no_discs_sels rep_compat
 *}
 
-section {* Generating Free Constructor Theorems
-  \label{sec:generating-free-constructor-theorems} *}
+section {* Generating Destructors and Theorems for Free Constructors
+  \label{sec:generating-destructors-and-theorems-for-free-constructors} *}
 
 text {*
 This section explains how to derive convenience theorems for free constructors,
@@ -1292,7 +1333,6 @@
 * no way to register same type as both data- and codatatype?
 
 * no recursion through unused arguments (unlike with the old package)
-
 *}
 
 
diff -r 7b779c075de9 -r eed6efba4e3f src/Doc/Datatypes/document/root.tex
--- a/src/Doc/Datatypes/document/root.tex	Wed Sep 11 22:20:45 2013 +0200
+++ b/src/Doc/Datatypes/document/root.tex	Wed Sep 11 23:55:47 2013 +0200
@@ -13,10 +13,17 @@
 \usepackage{railsetup}
 \usepackage{framed}
 
+\setcounter{secnumdepth}{3}
+\setcounter{tocdepth}{3}
+
 \newbox\boxA
 \setbox\boxA=\hbox{\ }
 \parindent=4\wd\boxA
 
+\newcommand\blankline{\vskip-.5\baselineskip}
+
+\newenvironment{indentblock}{\list{}{}\item[]}{\endlist}
+
 \newcommand{\keyw}[1]{\isacommand{#1}}
 \newcommand{\synt}[1]{\textit{#1}}
 \newcommand{\hthm}[1]{\textbf{\textit{#1}}}