# HG changeset patch
# User paulson
# Date 979312315 -3600
# Node ID 03f06372230b9300895a01ff1dfc52b4b64ea223
# Parent  729a36e469ec46b6484aecbef069405c00c6dc02
abs and other small changes

diff -r 729a36e469ec -r 03f06372230b doc-src/TutorialI/Types/numerics.tex
--- a/doc-src/TutorialI/Types/numerics.tex	Fri Jan 12 16:10:56 2001 +0100
+++ b/doc-src/TutorialI/Types/numerics.tex	Fri Jan 12 16:11:55 2001 +0100
@@ -4,7 +4,7 @@
 zero  and successor, so it works well with inductive proofs and primitive
 recursive function definitions. Isabelle/HOL also provides the type
 \isa{int} of \textbf{integers}, which lack induction but support true
-subtraction. The logic HOL-Real\REMARK{now part of HOL?} also has the type \isa{real} of real
+subtraction. The logic HOL-Real also has the type \isa{real} of real
 numbers.  Isabelle has no subtyping,  so the numeric types are distinct and
 there are  functions to convert between them. 
 
@@ -25,10 +25,10 @@
 
 The simplifier reduces arithmetic expressions in other
 ways, such as dividing through by common factors.  For problems that lie
-outside the scope of automation, the library has hundreds of
+outside the scope of automation, HOL provides hundreds of
 theorems about multiplication, division, etc., that can be brought to
-bear.  You can find find them by browsing the library or by using the Find
-button in Proof General.  A few lemmas are given below to show what
+bear.  You can locate them using Proof General's Find
+button.  A few lemmas are given below to show what
 is available.
 
 \subsection{Numeric Literals}
@@ -69,6 +69,21 @@
 constraint such as \isa{nat}, \isa{int} or \isa{real}, it becomes trivial.
 \end{warn}
 
+\begin{warn}
+Numeric literals are not constructors and therefore must not be used in
+patterns.  For example, this declaration is rejected:
+\begin{isabelle}
+\isacommand{recdef}\ h\ "\isacharbraceleft \isacharbraceright "\isanewline
+h\ \#3\ =\ \#2\isanewline
+h\ i\ \ =\ i
+\end{isabelle}
+
+You should use a conditional expression instead:
+\begin{isabelle}
+"h\ i\ =\ (if\ i\ =\ \#3\ then\ \#2\ else\ i)"
+\end{isabelle}
+\end{warn}
+
 
 
 \subsection{The type of natural numbers, {\tt\slshape nat}}
@@ -128,8 +143,9 @@
 \end{isabelle}
 
 \subsubsection{Division}
-The library contains the basic facts about quotient and remainder
-(including the analogous equation, \isa{div_if}):
+The infix operators \isa{div} and \isa{mod} are overloaded.
+Isabelle/HOL provides the basic facts about quotient and remainder
+on the natural numbers:
 \begin{isabelle}
 m\ mod\ n\ =\ (if\ m\ <\ n\ then\ m\ else\ (m\ -\ n)\ mod\ n)
 \rulename{mod_if}\isanewline
@@ -238,7 +254,7 @@
 \subsection{The type of integers, {\tt\slshape int}}
 
 Reasoning methods resemble those for the natural numbers, but induction and
-the constant \isa{Suc} are not available.  The library provides many lemmas
+the constant \isa{Suc} are not available.  HOL provides many lemmas
 for proving inequalities involving integer multiplication and division,
 similar to those shown above for type~\isa{nat}.  
 
@@ -255,6 +271,12 @@
 get \isa{\isasymbar x\isasymbar}.
 \end{warn}
 
+The \isa{arith} method can prove facts about \isa{abs} automatically, 
+though as it does so by case analysis, the cost can be exponential.
+\begin{isabelle}
+\isacommand{lemma}\ "\isasymlbrakk abs\ x\ <\ a;\ abs\ y\ <\ b\isasymrbrakk \ \isasymLongrightarrow \ abs\ x\ +\ abs\ y\ <\ (a\ +\ b\ ::\ int)"\isanewline
+\isacommand{by}\ arith
+\end{isabelle}
 
 Concerning simplifier tricks, we have no need to eliminate subtraction: it
 is well-behaved.  As with the natural numbers, the simplifier can sort the
@@ -308,7 +330,7 @@
 \isa{c} to be zero.  However, \isa{c} cannot be negative: a counterexample
 is
 $\isa{a} = 7$, $\isa{b} = 2$ and $\isa{c} = -3$, when the left-hand side of
-\isa{zdiv_zmult2_eq} is $-2$ while the right-hand side is $-1$.
+\isa{zdiv_zmult2_eq} is $-2$ while the right-hand side is~$-1$.
 
 
 \subsection{The type of real numbers, {\tt\slshape real}}
@@ -374,9 +396,11 @@
 \rulename{realpow_abs}
 \end{isabelle}
 
-\emph{Note}: Type \isa{real} is only available in the logic HOL-Real\REMARK{now part of HOL?}, which
+\begin{warn}
+Type \isa{real} is only available in the logic HOL-Real, which
 is  HOL extended with the rather substantial development of the real
 numbers.  Base your theory upon theory \isa{Real}, not the usual \isa{Main}.
+\end{warn}
 
 Also distributed with Isabelle is HOL-Hyperreal,
 whose theory \isa{Hyperreal} defines the type \isa{hypreal} of non-standard
@@ -385,5 +409,5 @@
 small and infinitely large quantities; they facilitate proofs
 about limits, differentiation and integration~\cite{fleuriot-jcm}.  The
 development defines an infinitely large number, \isa{omega} and an
-infinitely small positive number, \isa{epsilon}.  Also available is the
-approximates relation, written $\approx$.
+infinitely small positive number, \isa{epsilon}.  The 
+relation $x\approx y$ means ``$x$ is infinitely close to~$y$''.