--- 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}
+
*}
--- 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}$}
--- 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