Arithmetic.

--- a/doc-src/Tutorial/Misc/ROOT.ML	Tue May 04 16:18:16 1999 +0200
+++ b/doc-src/Tutorial/Misc/ROOT.ML	Tue May 04 16:49:24 1999 +0200
@@ -1,3 +1,11 @@
+context Main.thy;
+use "arith1.ML";
+by(Auto_tac);
+use "arith2.ML";
+by(arith_tac 1);
+use "arith3.ML";
+by(arith_tac 1);
+
 use_thy "Tree";
 
 context Main.thy;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/arith1.ML	Tue May 04 16:49:24 1999 +0200
@@ -0,0 +1,1 @@
+Goal "[| ~ m < n; m < n+1 |] ==> m = n";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/arith2.ML	Tue May 04 16:49:24 1999 +0200
@@ -0,0 +1,1 @@
+Goal "min i (max j (k*k)) = max (min (k*k) i) (min i (j::nat))";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/arith3.ML	Tue May 04 16:49:24 1999 +0200
@@ -0,0 +1,1 @@
+Goal "~ m < n & m < n+1 ==> m = n";

--- a/doc-src/Tutorial/fp.tex	Tue May 04 16:18:16 1999 +0200
+++ b/doc-src/Tutorial/fp.tex	Tue May 04 16:49:24 1999 +0200
@@ -338,8 +338,8 @@
 loaded already. If you modify \texttt{T.thy} or \texttt{T.ML}, you can
 reload it by typing \texttt{use_thy~"T";} again. This time, however, only
 \texttt{T} is reloaded. If some of \texttt{T}'s parents have changed as well,
-type \ttindexbold{update}\texttt{();} to reload all theories that have
-changed.
+type \ttindexbold{update_thy}~\texttt{"T";} to reload \texttt{T} and all of
+its parents that have changed (or have changed parents).
 \end{description}
 Further commands are found in the Reference Manual.
 
@@ -578,7 +578,9 @@
 
 \section{Some basic types}
 
+
 \subsection{Natural numbers}
+\index{arithmetic|(}
 
 The type \ttindexbold{nat} of natural numbers is predefined and behaves like
 \begin{ttbox}
@@ -599,17 +601,19 @@
 \end{ttbox}
 
 The usual arithmetic operations \ttindexbold{+}, \ttindexbold{-},
-\ttindexbold{*}, \ttindexbold{div} and \ttindexbold{mod} are predefined, as
-are the relations \ttindexbold{<=} and \ttindexbold{<}. There is even a least
-number operation \ttindexbold{LEAST}. For example, \texttt{(LEAST n.$\,$1 <
-  n) = 2} (HOL does not prove this completely automatically).
+\ttindexbold{*}, \ttindexbold{div}, \ttindexbold{mod}, \ttindexbold{min} and
+\ttindexbold{max} are predefined, as are the relations \ttindexbold{<=} and
+\ttindexbold{<}. There is even a least number operation \ttindexbold{LEAST}.
+For example, \texttt{(LEAST n.$\,$1 < n) = 2} (HOL does not prove this
+completely automatically).
 
 \begin{warn}
-  The operations \ttindexbold{+}, \ttindexbold{-}, \ttindexbold{*} are
-  overloaded, i.e.\ they are available not just for natural numbers but at
-  other types as well (see \S\ref{sec:TypeClasses}). For example, given
+  The operations \ttindexbold{+}, \ttindexbold{-}, \ttindexbold{*},
+  \ttindexbold{min}, \ttindexbold{max}, \ttindexbold{<=} and \ttindexbold{<}
+  are overloaded, i.e.\ they are available not just for natural numbers but
+  at other types as well (see \S\ref{sec:TypeClasses}). For example, given
   the goal \texttt{x+y = y+x}, there is nothing to indicate that you are
-  talking about natural numbers. Hence Isabelle can only infer that
+  talking about natural numbers.  Hence Isabelle can only infer that
   \texttt{x} and \texttt{y} are of some arbitrary type where \texttt{+} is
   declared. As a consequence, you will be unable to prove the goal (although
   it may take you some time to realize what has happened if
@@ -619,6 +623,39 @@
   \texttt{x+0 = x} automatically implies \texttt{x::nat}.
 \end{warn}
 
+Simple arithmetic goals are proved automatically by both \texttt{Auto_tac}
+and the simplification tactics introduced in \S\ref{sec:Simplification}.  For
+example, the goal
+\begin{ttbox}
+\input{Misc/arith1.ML}\end{ttbox}
+is proved automatically. The main restriction is that only addition is taken
+into account; other arithmetic operations and quantified formulae are ignored.
+
+For more complex goals, there is the special tactic \ttindexbold{arith_tac}. It
+proves arithmetic goals involving the usual logical connectives (\verb$~$,
+\verb$&$, \verb$|$, \verb$-->$), the relations \texttt{<=} and \texttt{<},
+and the operations \ttindexbold{+}, \ttindexbold{-}, \ttindexbold{min} and
+\ttindexbold{max}. For example, it can prove
+\begin{ttbox}
+\input{Misc/arith2.ML}\end{ttbox}
+because \texttt{k*k} can be treated as atomic.
+In contrast, $n*n = n \Longrightarrow n=0 \lor n=1$ is not
+even proved by \texttt{arith_tac} because the proof relies essentially on
+properties of multiplication.
+
+\begin{warn}
+  The running time of \texttt{arith_tac} is exponential in the number of
+  occurrences of \ttindexbold{-}, \ttindexbold{min} and \ttindexbold{max}
+  because they are first eliminated by case distinctions.
+
+  \texttt{arith_tac} is incomplete even for the restricted class of formulae
+  described above (known as ``linear arithmetic''). 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.
+\end{warn}
+
+\index{arithmetic|)}
+
 
 \subsection{Products}
 
@@ -1010,6 +1047,20 @@
 \end{ttbox}
 
 
+\subsubsection{Arithmetic}
+\index{arithmetic}
+
+The simplifier routinely solves a small class of linear arithmetic formulae
+(over types \texttt{nat} and \texttt{int}): it only takes into account
+assumptions and conclusions that are (possibly negated) (in)equalities
+(\texttt{=}, \texttt{<=}, \texttt{<}) and it only knows about addition. Thus
+\begin{ttbox}
+\input{Misc/arith1.ML}\end{ttbox}
+is proved by simplification, whereas the only slightly more complex
+\begin{ttbox}
+\input{Misc/arith3.ML}\end{ttbox}
+is not proved by simplification and requires \texttt{arith_tac}.
+
 \subsubsection{Permutative rewrite rules}
 
 A rewrite rule is {\bf permutative} if the left-hand side and right-hand side

--- a/doc-src/Tutorial/tutorial.bbl	Tue May 04 16:18:16 1999 +0200
+++ b/doc-src/Tutorial/tutorial.bbl	Tue May 04 16:49:24 1999 +0200
@@ -21,7 +21,8 @@
 \bibitem{MuellerNvOS98}
 Olaf M\"uller, Tobias Nipkow, David~von Oheimb, and Oskar Slotosch.
 \newblock {HOLCF = HOL + LCF}.
-\newblock Submitted for publication, 1998.
+\newblock {\em J. Functional Programming}, 1999.
+\newblock To appear.
 
 \bibitem{Isa-Ref-Man}
 Lawrence~C. Paulson.

--- a/doc-src/Tutorial/tutorial.ind	Tue May 04 16:18:16 1999 +0200
+++ b/doc-src/Tutorial/tutorial.ind	Tue May 04 16:49:24 1999 +0200
@@ -11,13 +11,13 @@
   \item {\ttuniquex}, \bold{3}
   \item {\tt *}, \bold{17}
   \item {\tt +}, \bold{17}
-  \item {\tt -}, \bold{17}
+  \item {\tt -}, \bold{17, 18}
   \item {\tt <}, \bold{17}
   \item {\tt <=}, \bold{17}
   \item \ttlbr, \bold{9}
   \item \ttrbr, \bold{9}
   \item {\tt==>}, \bold{9}
-  \item {\tt==}, \bold{18}
+  \item {\tt==}, \bold{19}
   \item {\tt\%}, \bold{3}
   \item {\tt =>}, \bold{2}
 
@@ -27,6 +27,8 @@
   \item {\tt Addsplits}, \bold{24}
   \item {\tt addsplits}, \bold{24}
   \item {\tt and}, \bold{29}
+  \item {\tt arith_tac}, \bold{17}
+  \item arithmetic, 17--18, 24
   \item {\tt Asm_full_simp_tac}, \bold{21}
   \item {\tt asm_full_simp_tac}, \bold{22}
   \item {\tt Asm_simp_tac}, \bold{21}
@@ -39,7 +41,7 @@
   \indexspace
 
   \item {\tt case}, \bold{3}, 4, \bold{13}, 24
-  \item {\tt constdefs}, \bold{18}
+  \item {\tt constdefs}, \bold{19}
   \item {\tt consts}, \bold{7}
   \item {\tt context}, \bold{11}
   \item current theory, \bold{11}
@@ -47,7 +49,7 @@
   \indexspace
 
   \item {\tt datatype}, \bold{7}, 29--33
-  \item {\tt defs}, \bold{18}
+  \item {\tt defs}, \bold{19}
   \item {\tt delsimps}, \bold{22}
   \item {\tt Delsplits}, \bold{24}
   \item {\tt delsplits}, \bold{24}
@@ -84,7 +86,9 @@
   \indexspace
 
   \item {\tt Main}, \bold{2}
-  \item measure function, \bold{35}
+  \item {\tt max}, \bold{17, 18}
+  \item measure function, \bold{36}
+  \item {\tt min}, \bold{17, 18}
   \item {\tt mod}, \bold{17}
   \item {\tt mutual_induct_tac}, \bold{30}
 
@@ -138,7 +142,7 @@
   \indexspace
 
   \item unknown, \bold{4}
-  \item {\tt update}, \bold{12}
+  \item {\tt update_thy}, \bold{12}
   \item {\tt use_thy}, \bold{2}, 12
 
 \end{theindex}