--- 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$}
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Wed May 25 22:21:38 2011 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Thu May 26 13:37:11 2011 +0200
@@ -458,14 +458,26 @@
HOL.
\item @{command (HOL) "rep_datatype"} represents existing types as
- inductive ones, generating the standard infrastructure of derived
- concepts (primitive recursion etc.).
+ datatypes.
+
+ For foundational reasons, some basic types such as @{typ nat}, @{typ
+ "'a \<times> 'b"}, @{typ "'a + 'b"}, @{typ bool} and @{typ unit} are
+ introduced by more primitive means using @{command_ref typedef}. To
+ recover the rich infrastructure of @{command datatype} (e.g.\ rules
+ for @{method cases} and @{method induct} and the primitive recursion
+ combinators), such types may be represented as actual datatypes
+ later. This is done by specifying the constructors of the desired
+ type, and giving a proof of the induction rule, distinctness and
+ injectivity of constructors.
+
+ For example, see @{file "~~/src/HOL/Sum_Type.thy"} for the
+ representation of the primitive sum type as fully-featured datatype.
\end{description}
- The induction and exhaustion theorems generated provide case names
- according to the constructors involved, while parameters are named
- after the types (see also \secref{sec:cases-induct}).
+ The generated rules for @{method induct} and @{method cases} provide
+ case names according to the given constructors, while parameters are
+ named after the types (see also \secref{sec:cases-induct}).
See \cite{isabelle-HOL} for more details on datatypes, but beware of
the old-style theory syntax being used there! Apart from proper
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed May 25 22:21:38 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu May 26 13:37:11 2011 +0200
@@ -729,14 +729,25 @@
HOL.
\item \hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isaliteral{5F}{\isacharunderscore}}datatype}}}} represents existing types as
- inductive ones, generating the standard infrastructure of derived
- concepts (primitive recursion etc.).
+ datatypes.
+
+ For foundational reasons, some basic types such as \isa{nat}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{22}{\isachardoublequote}}}, \isa{bool} and \isa{unit} are
+ introduced by more primitive means using \indexref{}{command}{typedef}\hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}}. To
+ recover the rich infrastructure of \hyperlink{command.datatype}{\mbox{\isa{\isacommand{datatype}}}} (e.g.\ rules
+ for \hyperlink{method.cases}{\mbox{\isa{cases}}} and \hyperlink{method.induct}{\mbox{\isa{induct}}} and the primitive recursion
+ combinators), such types may be represented as actual datatypes
+ later. This is done by specifying the constructors of the desired
+ type, and giving a proof of the induction rule, distinctness and
+ injectivity of constructors.
+
+ For example, see \verb|~~/src/HOL/Sum_Type.thy| for the
+ representation of the primitive sum type as fully-featured datatype.
\end{description}
- The induction and exhaustion theorems generated provide case names
- according to the constructors involved, while parameters are named
- after the types (see also \secref{sec:cases-induct}).
+ The generated rules for \hyperlink{method.induct}{\mbox{\isa{induct}}} and \hyperlink{method.cases}{\mbox{\isa{cases}}} provide
+ case names according to the given constructors, while parameters are
+ named after the types (see also \secref{sec:cases-induct}).
See \cite{isabelle-HOL} for more details on datatypes, but beware of
the old-style theory syntax being used there! Apart from proper