# HG changeset patch
# User paulson
# Date 1106580336 -3600
# Node ID 735dd4260500c8afcc81ed0f8b759fca9cb38d0c
# Parent  4b339d3907a091e3bea1314ec0f208de99fc9c17
updated description of arith_tac

diff -r 4b339d3907a0 -r 735dd4260500 doc-src/HOL/HOL.tex
--- 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);