# HG changeset patch
# User berghofe
# Date 935419109 -7200
# Node ID 01bb8abb5a91063233291fe456fb4b8dab941b14
# Parent 6cb0d0202298b5f23d9753602d4c932bfca4785c
Some changes in sections about Sum and Nat.
diff -r 6cb0d0202298 -r 01bb8abb5a91 doc-src/HOL/HOL.tex
--- a/doc-src/HOL/HOL.tex Mon Aug 23 16:22:23 1999 +0200
+++ b/doc-src/HOL/HOL.tex Mon Aug 23 16:38:29 1999 +0200
@@ -1223,7 +1223,11 @@
The definition of products and sums in terms of existing types is not
shown. The constructions are fairly standard and can be found in the
-respective theory files.
+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}.
\begin{figure}
\begin{constants}
@@ -1234,9 +1238,6 @@
& & conditional
\end{constants}
\begin{ttbox}\makeatletter
-%\tdx{sum_case_def} sum_case == (\%f g p. @z. (!x. p=Inl x --> z=f x) &
-% (!y. p=Inr y --> z=g y))
-%
\tdx{Inl_not_Inr} Inl a ~= Inr b
\tdx{inj_Inl} inj Inl
@@ -1248,7 +1249,7 @@
\tdx{sum_case_Inr} sum_case f g (Inr x) = g x
\tdx{surjective_sum} sum_case (\%x. f(Inl x)) (\%y. f(Inr y)) s = f s
-\tdx{split_sum_case} R(sum_case f g s) = ((! x. s = Inl(x) --> R(f(x))) &
+\tdx{sum.split_case} R(sum_case f g s) = ((! x. s = Inl(x) --> R(f(x))) &
(! y. s = Inr(y) --> R(g(y))))
\end{ttbox}
\caption{Type $\alpha+\beta$}\label{hol-sum}
@@ -1350,7 +1351,8 @@
Note that Isabelle insists on precisely this format; you may not even change
the order of the two cases.
Both \texttt{primrec} and \texttt{case} are realized by a recursion operator
-\cdx{nat_rec}, the details of which can be found in theory \texttt{NatDef}.
+\cdx{nat_rec}, which is available because \textit{nat} is represented as
+a datatype (see \S\ref{subsec:datatype:rep_datatype}).
%The predecessor relation, \cdx{pred_nat}, is shown to be well-founded.
%Recursion along this relation resembles primitive recursion, but is
@@ -2225,7 +2227,7 @@
and \texttt{simps} are contained in a separate structure named $t@1_\ldots_t@n$.
-\subsection{Representing existing types as datatypes}
+\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,