# HG changeset patch
# User blanchet
# Date 1378917163 -7200
# Node ID 2176a7e407863753c3121f0717366649b492702c
# Parent  c6c8dce7e9ab0eb9fd1c54f6a6eac6afaac047e8
more (co)data docs

diff -r c6c8dce7e9ab -r 2176a7e40786 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Wed Sep 11 17:17:58 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Wed Sep 11 18:32:43 2013 +0200
@@ -336,13 +336,6 @@
 \begin{itemize}
 \setlength{\itemsep}{0pt}
 
-\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{Case combinator}: @{text t_case} (rendered using the familiar
 @{text case}--@{text of} syntax)
 
@@ -357,6 +350,14 @@
 @{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
@@ -377,7 +378,7 @@
       Cons (infixr "#" 65)
 
     hide_type list
-    hide_const Nil Cons hd tl map
+    hide_const Nil Cons hd tl set map list_all2 list_case list_rec
 
     locale dummy_list
     begin
@@ -533,26 +534,23 @@
   \label{ssec:datatype-generated-theorems} *}
 
 text {*
-The characteristic theorems generated by @{command datatype_new} are
-grouped in three broad categories:
+The characteristic theorems generated by @{command datatype_new} are grouped in
+two broad categories:
 
 \begin{itemize}
 \item The \emph{free constructor theorems} are properties about the constructors
 and destructors that can be derived for any freely generated type. Internally,
 the derivation is performed by @{command wrap_free_constructors}.
 
-\item The \emph{per-datatype theorems} are properties connected to individual
-datatypes and that rely on their inductive nature.
-
-\item The \emph{mutual datatype theorems} are properties associated to mutually
-recursive groups of datatypes.
+\item The \emph{inductive theorems} are properties of datatypes that rely on
+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 see these as well, add the following line to the top of your
+constructions. To make these accessible, add the following line to the top of your
 theory file:
 *}
 
@@ -573,17 +571,18 @@
 They are listed below for @{typ "'a list"}:
 
 \begin{description}
-\item[@{text "t.distinct [simp, induct_simp]"}:] ~ \\
+
+\item[@{text "t."}\hthm{inject} @{text "[iff, induct_simp]"}:] ~ \\
+@{thm list.inject[no_vars]}
+
+\item[@{text "t."}\hthm{distinct} @{text "[simp, induct_simp]"}:] ~ \\
 @{thm list.distinct(1)[no_vars]} \\
 @{thm list.distinct(2)[no_vars]}
 
-\item[@{text "t.inject [iff, induct_simp]"}:] ~ \\
-@{thm list.inject[no_vars]}
-
-\item[@{text "t.exhaust [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]"}:] ~ \\
 @{thm list.exhaust[no_vars]}
 
-\item[@{text t.nchotomy}:] ~ \\
+\item[@{text "t."}\hthm{nchotomy}:] ~ \\
 @{thm list.nchotomy[no_vars]}
 
 \end{description}
@@ -592,23 +591,24 @@
 The next subgroup is concerned with the case combinator:
 
 \begin{description}
-\item[@{text "t.case [simp]"}:] ~ \\
+
+\item[@{text "t."}\hthm{case} @{text "[simp]"}:] ~ \\
 @{thm list.case(1)[no_vars]} \\
 @{thm list.case(2)[no_vars]}
 
-\item[@{text t.case_cong}:] ~ \\
+\item[@{text "t."}\hthm{case\_cong}:] ~ \\
 @{thm list.case_cong[no_vars]}
 
-\item[@{text "t.weak_case_cong [cong]"}:] ~ \\
+\item[@{text "t."}\hthm{weak\_case\_cong} @{text "[cong]"}:] ~ \\
 @{thm list.weak_case_cong[no_vars]}
 
-\item[@{text t.split}:] ~ \\
+\item[@{text "t."}\hthm{split}:] ~ \\
 @{thm list.split[no_vars]}
 
-\item[@{text t.split_asm}:] ~ \\
+\item[@{text "t."}\hthm{split\_asm}:] ~ \\
 @{thm list.split_asm[no_vars]}
 
-\item[@{text "t.splits = split split_asm"}]
+\item[@{text "t."}\hthm{splits} = @{text "split split_asm"}]
 
 \end{description}
 
@@ -616,54 +616,88 @@
 The third and last subgroup revolves around discriminators and selectors:
 
 \begin{description}
-\item[@{text "discs [simp]"}:] ~ \\
+
+\item[@{text "t."}\hthm{discs} @{text "[simp]"}:] ~ \\
 @{thm list.discs(1)[no_vars]} \\
 @{thm list.discs(2)[no_vars]}
 
-\item[@{text "sels [simp]"}:] ~ \\
+\item[@{text "t."}\hthm{sels} @{text "[simp]"}:] ~ \\
 @{thm list.sels(1)[no_vars]} \\
 @{thm list.sels(2)[no_vars]}
 
-\item[@{text "collapse [simp]"}:] ~ \\
+\item[@{text "t."}\hthm{collapse} @{text "[simp]"}:] ~ \\
 @{thm list.collapse(1)[no_vars]} \\
 @{thm list.collapse(2)[no_vars]}
 
-\item[@{text disc_exclude}:] ~ \\
+\item[@{text "t."}\hthm{disc\_exclude}:] ~ \\
 These properties are missing for @{typ "'a list"} because there is only one
 proper discriminator. Had the datatype been introduced with a second
-discriminator (@{const is_Cons}), they would have read thusly: \\
+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 "disc_exhaust [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]"}:] ~ \\
 @{thm list.disc_exhaust[no_vars]}
 
-\item[@{text expand}:] ~ \\
+\item[@{text "t."}\hthm{expand}:] ~ \\
 @{thm list.expand[no_vars]}
 
-\item[@{text t.case_conv}:] ~ \\
+\item[@{text "t."}\hthm{case\_conv}:] ~ \\
 @{thm list.case_conv[no_vars]}
 
 \end{description}
-
-  * Section~\label{sec:generating-free-constructor-theorems}
 *}
 
 
-subsubsection {* Per-Datatype Theorems *}
+subsubsection {* Inductive Theorems *}
 
 text {*
-    * sets, map, rel
-    * induct, fold, rec
-    * simps
-*}
+
+\begin{description}
+
+\item[@{text "t."}\hthm{induct} @{text "[induct t, case_names C\<^sub>1 \<dots> C\<^sub>n]"}:] ~ \\
+@{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]"}:] ~ \\
+Given $m > 1$ mutually recursive datatypes, this induction rule can be used to
+prove $m$ properties simultaneously.
 
+\item[@{text "t."}\hthm{fold} @{text "[code]"}:] ~ \\
+@{thm list.fold(1)[no_vars]} \\
+@{thm list.fold(2)[no_vars]}
+
+\item[@{text "t."}\hthm{rec} @{text "[code]"}:] ~ \\
+@{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]}
 
-subsubsection {* Mutual Datatype Theorems *}
+\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]}
 
-text {*
-  * multi-type (``common'') theorems
-    * induct
+\end{description}
+
+\noindent
+For convenience, @{command datatype_new} also provides the following collection:
+
+\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}
+
 *}
 
 
diff -r c6c8dce7e9ab -r 2176a7e40786 src/Doc/Datatypes/document/root.tex
--- a/src/Doc/Datatypes/document/root.tex	Wed Sep 11 17:17:58 2013 +0200
+++ b/src/Doc/Datatypes/document/root.tex	Wed Sep 11 18:32:43 2013 +0200
@@ -19,6 +19,7 @@
 
 \newcommand{\keyw}[1]{\isacommand{#1}}
 \newcommand{\synt}[1]{\textit{#1}}
+\newcommand{\hthm}[1]{\textbf{\textit{#1}}}
 
 %\renewcommand{\isactrlsub}[1]{\/$\sb{\mathrm{#1}}$}
 \renewcommand{\isactrlsub}[1]{\/$\sb{#1}$}
diff -r c6c8dce7e9ab -r 2176a7e40786 src/Doc/ROOT
--- a/src/Doc/ROOT	Wed Sep 11 17:17:58 2013 +0200
+++ b/src/Doc/ROOT	Wed Sep 11 18:32:43 2013 +0200
@@ -38,7 +38,7 @@
     "document/style.sty"
 
 session Datatypes (doc) in "Datatypes" = "HOL-BNF" +
-  options [document_variants = "datatypes", document_output = "/tmp/isa-output"]
+  options [document_variants = "datatypes"]
   theories [document = false] Setup
   theories Datatypes
   files