--- a/doc-src/HOL/HOL.tex Mon Jan 24 12:41:06 2005 +0100
+++ b/doc-src/HOL/HOL.tex Mon Jan 24 16:25:36 2005 +0100
@@ -1337,20 +1337,20 @@
\subsection{The type of natural numbers, \textit{nat}}
\index{nat@{\textit{nat}} type|(}
-The theory \thydx{NatDef} defines the natural numbers in a roundabout but
+The theory \thydx{Nat} defines the natural numbers in a roundabout but
traditional way. The axiom of infinity postulates a type~\tydx{ind} of
individuals, which is non-empty and closed under an injective operation. The
natural numbers are inductively generated by choosing an arbitrary individual
for~0 and using the injective operation to take successors. This is a least
-fixedpoint construction. For details see the file \texttt{NatDef.thy}.
+fixedpoint construction.
Type~\tydx{nat} is an instance of class~\cldx{ord}, which makes the overloaded
functions of this class (especially \cdx{<} and \cdx{<=}, but also \cdx{min},
-\cdx{max} and \cdx{LEAST}) available on \tydx{nat}. Theory \thydx{Nat} builds
-on \texttt{NatDef} and shows that {\tt<=} is a linear order, so \tydx{nat} is
+\cdx{max} and \cdx{LEAST}) available on \tydx{nat}. Theory \thydx{Nat}
+also shows that {\tt<=} is a linear order, so \tydx{nat} is
also an instance of class \cldx{linorder}.
-Theory \thydx{Arith} develops arithmetic on the natural numbers. It defines
+Theory \thydx{NatArith} develops arithmetic on the natural numbers. It defines
addition, multiplication and subtraction. Theory \thydx{Divides} defines
division, remainder and the ``divides'' relation. The numerous theorems
proved include commutative, associative, distributive, identity and
@@ -1423,27 +1423,25 @@
fancier simplifications by using a basic simpset such as \texttt{HOL_ss}
rather than the default one, \texttt{simpset()}.
-Reasoning about arithmetic inequalities can be tedious. Fortunately HOL
-provides a decision procedure for quantifier-free linear arithmetic (that is,
-addition and subtraction). The simplifier invokes a weak version of this
+Reasoning about arithmetic inequalities can be tedious. Fortunately, HOL
+provides a decision procedure for \emph{linear arithmetic}: formulae involving
+addition and subtraction. The simplifier invokes a weak version of this
decision procedure automatically. If this is not sufficent, you can invoke the
full procedure \ttindex{arith_tac} explicitly. It copes with arbitrary
formulae involving {\tt=}, {\tt<}, {\tt<=}, {\tt+}, {\tt-}, {\tt Suc}, {\tt
- min}, {\tt max} and numerical constants; other subterms are treated as
-atomic; subformulae not involving numerical types are ignored; quantified
+ min}, {\tt max} and numerical constants. Other subterms are treated as
+atomic, while subformulae not involving numerical types are ignored. Quantified
subformulae are ignored unless they are positive universal or negative
-existential. Note that the running time is exponential in the number of
+existential. The running time is exponential in the number of
occurrences of {\tt min}, {\tt max}, and {\tt-} because they require case
-distinctions. Note also that \texttt{arith_tac} is not complete: if
-divisibility plays a role, it may fail to prove a valid formula, for example
-$m+m \neq n+n+1$. Fortunately such examples are rare in practice.
-
-If \texttt{arith_tac} fails you, try to find relevant arithmetic results in
-the library. The theory \texttt{NatDef} contains theorems about {\tt<} and
-{\tt<=}, the theory \texttt{Arith} contains theorems about \texttt{+},
-\texttt{-} and \texttt{*}, and theory \texttt{Divides} contains theorems about
-\texttt{div} and \texttt{mod}. Use \texttt{thms_containing} or the
-\texttt{find}-functions to locate them (see the {\em Reference Manual\/}).
+distinctions.
+If {\tt k} is a numeral, then {\tt div k}, {\tt mod k} and
+{\tt k dvd} are also supported. The former two are eliminated
+by case distinctions, again blowing up the running time.
+If the formula involves explicit quantifiers, \texttt{arith_tac} may take
+super-exponential time and space.
+
+If \texttt{arith_tac} fails, try to find relevant arithmetic results in
the library. The theories \texttt{Nat} and \texttt{NatArith} contain
theorems about {\tt<}, {\tt<=}, \texttt{+}, \texttt{-} and \texttt{*}.
Theory \texttt{Divides} contains theorems about \texttt{div} and
\texttt{mod}. Use Proof General's \emph{find} button (or other search
facilities) to locate them.
\index{nat@{\textit{nat}} type|)}
@@ -1962,7 +1960,7 @@
\subsubsection{The function \cdx{size}}\label{sec:HOL:size}
-Theory \texttt{Arith} declares a generic function \texttt{size} of type
+Theory \texttt{NatArith} declares a generic function \texttt{size} of type
$\alpha\To nat$. Each datatype defines a particular instance of \texttt{size}
by overloading according to the following scheme:
%%% FIXME: This formula is too big and is completely unreadable
@@ -2171,7 +2169,7 @@
Because there are more than 6 constructors, inequality is expressed via a function
\verb|days_ord|. The theorem \verb|Mon ~= Tue| is not directly
contained among the distinctness theorems, but the simplifier can
-prove it thanks to rewrite rules inherited from theory \texttt{Arith}:
+prove it thanks to rewrite rules inherited from theory \texttt{NatArith}:
\begin{ttbox}
Goal "Mon ~= Tue";
by (Simp_tac 1);