author wenzelm Thu, 26 May 2011 13:37:11 +0200 changeset 42909 66b189dc5b83 parent 42908 eb94cfaaf5d4 child 42910 6834af822a8b
updated and re-unified HOL rep_datatype;
 doc-src/HOL/HOL.tex file | annotate | diff | comparison | revisions doc-src/IsarRef/Thy/HOL_Specific.thy file | annotate | diff | comparison | revisions doc-src/IsarRef/Thy/document/HOL_Specific.tex file | annotate | diff | comparison | revisions
--- 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
+  The generated rules for @{method induct} and @{method cases} provide
+  case names according to the given constructors, while parameters are

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
+  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
the old-style theory syntax being used there!  Apart from proper