--- a/doc-src/HOL/HOL.tex Wed May 25 22:21:38 2011 +0200
+++ b/doc-src/HOL/HOL.tex Thu May 26 13:37:11 2011 +0200
@@ -1249,9 +1249,7 @@
shown. The constructions are fairly standard and can be found in the
respective theory files. Although the sum and product types are
constructed manually for foundational reasons, they are represented as
-actual datatypes later (see {\S}\ref{subsec:datatype:rep_datatype}).
-Therefore, the theory \texttt{Datatype} should be used instead of
-\texttt{Sum} or \texttt{Prod}.
+actual datatypes later.
\begin{figure}
\begin{constants}
@@ -1375,7 +1373,7 @@
the order of the two cases.
Both \texttt{primrec} and \texttt{case} are realized by a recursion operator
\cdx{nat_rec}, which is available because \textit{nat} is represented as
-a datatype (see {\S}\ref{subsec:datatype:rep_datatype}).
+a datatype.
%The predecessor relation, \cdx{pred_nat}, is shown to be well-founded.
%Recursion along this relation resembles primitive recursion, but is
@@ -1940,32 +1938,6 @@
and \texttt{simps} are contained in a separate structure named $t@1_\ldots_t@n$.
-\subsection{Representing existing types as datatypes}\label{subsec:datatype:rep_datatype}
-
-For foundational reasons, some basic types such as \texttt{nat}, \texttt{*}, {\tt
- +}, \texttt{bool} and \texttt{unit} are not defined in a \texttt{datatype} section,
-but by more primitive means using \texttt{typedef}. To be able to use the
-tactics \texttt{induct_tac} and \texttt{case_tac} and to define functions by
-primitive recursion on these types, such types may be represented as actual
-datatypes. This is done by specifying the constructors of the desired type,
-plus a proof of the induction rule, as well as theorems
-stating the distinctness and injectivity of constructors in a {\tt
-rep_datatype} section. For the sum type this works as follows:
-\begin{ttbox}
-rep_datatype (sum) Inl Inr
-proof -
- fix P
- fix s :: "'a + 'b"
- assume x: "!!x::'a. P (Inl x)" and y: "!!y::'b. P (Inr y)"
- then show "P s" by (auto intro: sumE [of s])
-qed simp_all
-\end{ttbox}
-The datatype package automatically derives additional theorems for recursion
-and case combinators from these rules. Any of the basic HOL types mentioned
-above are represented as datatypes. Try an induction on \texttt{bool}
-today.
-
-
\subsection{Examples}
\subsubsection{The datatype $\alpha~mylist$}