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}