author berghofe Mon, 23 Aug 1999 16:38:29 +0200 changeset 7325 01bb8abb5a91 parent 7324 6cb0d0202298 child 7326 a1555491a966
Some changes in sections about Sum and Nat.
 doc-src/HOL/HOL.tex file | annotate | diff | comparison | revisions
--- 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,