# HG changeset patch
# User nipkow
# Date 922792675 -7200
# Node ID 0f6076dca73757133131f5f609aaddc9e677a64c
# Parent  39922bfb7107fd2bd1c911c0ece6f94eb908b5c8
arith_tac

diff -r 39922bfb7107 -r 0f6076dca737 doc-src/Logics/HOL.tex
--- a/doc-src/Logics/HOL.tex	Fri Mar 19 11:26:40 1999 +0100
+++ b/doc-src/Logics/HOL.tex	Tue Mar 30 13:17:55 1999 +0200
@@ -1269,21 +1269,22 @@
 \end{ttbox}
 
 
-Reasoning about arithmetic inequalities can be tedious.  A minimal amount of
-automation is provided by the tactic \ttindex{trans_tac} of type \texttt{int ->
-tactic} that deals with simple inequalities.  Note that it only knows about
-\texttt{0}, \texttt{Suc}, {\tt<} and {\tt<=}.  The following goals are all solved by
-\texttt{trans_tac 1}:
-\begin{ttbox}
-{\out  1. \dots ==> m <= Suc(Suc m)}
-{\out  1. [| \dots i <= j \dots Suc j <= k \dots |] ==> i < k}
-{\out  1. [| \dots Suc m <= n \dots ~ m < n \dots |] ==> \dots}
-\end{ttbox}
-For a complete description of the limitations of the tactic and how to avoid
-some of them, see the comments at the start of the file {\tt
-Provers/nat_transitive.ML}.
-
-If \texttt{trans_tac} fails you, try to find relevant arithmetic results in
+Reasoning about arithmetic inequalities can be tedious.  Fortunately HOL
+provides a decision procedure for quantifier-free linear arithmetic (i.e.\ 
+only 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 type $nat$ 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
+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