--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Types/numerics.tex Tue Dec 05 18:55:18 2000 +0100
@@ -0,0 +1,311 @@
+Our examples until now have used the type of \textbf{natural numbers},
+\isa{nat}. This is a recursive datatype generated by the constructors
+zero and successor, so it works well with inductive proofs and primitive
+recursive function definitions. Isabelle/HOL also has the type \isa{int}
+of \textbf{integers}, which gives up induction in exchange for proper subtraction.
+
+The integers are preferable to the natural numbers for reasoning about
+complicated arithmetic expressions. For example, a termination proof
+typically involves an integer metric that is shown to decrease at each
+loop iteration. Even if the metric cannot become negative, proofs about it
+are usually easier if the integers are used rather than the natural
+numbers.
+
+The logic Isabelle/HOL-Real also has the type \isa{real} of real numbers
+and even the type \isa{hypreal} of non-standard reals. These
+\textbf{hyperreals} include infinitesimals, which represent infinitely
+small and infinitely large quantities; they greatly facilitate proofs
+about limits, differentiation and integration. Isabelle has no subtyping,
+so the numeric types are distinct and there are
+functions to convert between them.
+
+Many theorems involving numeric types can be proved automatically by
+Isabelle's arithmetic decision procedure, the method
+\isa{arith}. Linear arithmetic comprises addition, subtraction
+and multiplication by constant factors; subterms involving other operators
+are regarded as variables. The procedure can be slow, especially if the
+subgoal to be proved involves subtraction over type \isa{nat}, which
+causes case splits.
+
+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
+theorems about multiplication, division, etc., that can be brought to
+bear. You can find find them by browsing the library. Some
+useful lemmas are shown below.
+
+\subsection{Numeric Literals}
+
+Literals are available for the types of natural numbers, integers
+and reals and denote integer values of arbitrary size.
+\REMARK{hypreal?}
+They begin
+with a number sign (\isa{\#}), have an optional minus sign (\isa{-}) and
+then one or more decimal digits. Examples are \isa{\#0}, \isa{\#-3}
+and \isa{\#441223334678}.
+
+Literals look like constants, but they abbreviate
+terms, representing the number in a two's complement binary notation.
+Isabelle performs arithmetic on literals by rewriting, rather
+than using the hardware arithmetic. In most cases arithmetic
+is fast enough, even for large numbers. The arithmetic operations
+provided for literals are addition, subtraction, multiplication,
+integer division and remainder.
+
+\emph{Beware}: the arithmetic operators are
+overloaded, so you must be careful to ensure that each numeric
+expression refers to a specific type, if necessary by inserting
+type constraints. Here is an example of what can go wrong:
+\begin{isabelle}
+\isacommand{lemma}\ "\#2\ *\ m\ =\ m\ +\ m"
+\end{isabelle}
+%
+Carefully observe how Isabelle displays the subgoal:
+\begin{isabelle}
+\ 1.\ (\#2::'a)\ *\ m\ =\ m\ +\ m
+\end{isabelle}
+The type \isa{'a} given for the literal \isa{\#2} warns us that no numeric
+type has been specified. The problem is underspecified. Given a type
+constraint such as \isa{nat}, \isa{int} or \isa{real}, it becomes trivial.
+
+
+\subsection{The type of natural numbers, {\tt\slshape nat}}
+
+This type requires no introduction: we have been using it from the
+start. Hundreds of useful lemmas about arithmetic on type \isa{nat} are
+proved in the theories \isa{Nat}, \isa{NatArith} and \isa{Divides}. Only
+in exceptional circumstances should you resort to induction.
+
+\subsubsection{Literals}
+The notational options for the natural numbers can be confusing. The
+constant \isa{0} is overloaded to serve as the neutral value
+in a variety of additive types. The symbols \isa{1} and \isa{2} are
+not constants but abbreviations for \isa{Suc 0} and \isa{Suc(Suc 0)},
+respectively. The literals \isa{\#0}, \isa{\#1} and \isa{\#2} are
+entirely different from \isa{0}, \isa{1} and \isa{2}. You will
+sometimes prefer one notation to the other. Literals are obviously
+necessary to express large values, while \isa{0} and \isa{Suc} are
+needed in order to match many theorems, including the rewrite rules for
+primitive recursive functions. The following default simplification rules
+replace small literals by zero and successor:
+\begin{isabelle}
+\#0\ =\ 0
+\rulename{numeral_0_eq_0}\isanewline
+\#1\ =\ 1
+\rulename{numeral_1_eq_1}\isanewline
+\#2\ +\ n\ =\ Suc\ (Suc\ n)
+\rulename{add_2_eq_Suc}\isanewline
+n\ +\ \#2\ =\ Suc\ (Suc\ n)
+\rulename{add_2_eq_Suc'}
+\end{isabelle}
+In special circumstances, you may wish to remove or reorient
+these rules.
+
+\subsubsection{Typical lemmas}
+Inequalities involving addition and subtraction alone can be proved
+automatically. Lemmas such as these can be used to prove inequalities
+involving multiplication and division:
+\begin{isabelle}
+\isasymlbrakk i\ \isasymle \ j;\ k\ \isasymle \ l\isasymrbrakk \ \isasymLongrightarrow \ i\ *\ k\ \isasymle \ j\ *\ l%
+\rulename{mult_le_mono}\isanewline
+\isasymlbrakk i\ <\ j;\ 0\ <\ k\isasymrbrakk \ \isasymLongrightarrow \ i\
+*\ k\ <\ j\ *\ k%
+\rulename{mult_less_mono1}\isanewline
+m\ \isasymle \ n\ \isasymLongrightarrow \ m\ div\ k\ \isasymle \ n\ div\ k%
+\rulename{div_le_mono}
+\end{isabelle}
+%
+Various distributive laws concerning multiplication are available:
+\begin{isabelle}
+(m\ +\ n)\ *\ k\ =\ m\ *\ k\ +\ n\ *\ k%
+\rulename{add_mult_distrib}\isanewline
+(m\ -\ n)\ *\ k\ =\ m\ *\ k\ -\ n\ *\ k%
+\rulename{diff_mult_distrib}\isanewline
+(m\ mod\ n)\ *\ k\ =\ (m\ *\ k)\ mod\ (n\ *\ k)
+\rulename{mod_mult_distrib}
+\end{isabelle}
+
+\subsubsection{Division}
+The library contains the basic facts about quotient and remainder
+(including the analogous equation, \isa{div_if}):
+\begin{isabelle}
+m\ mod\ n\ =\ (if\ m\ <\ n\ then\ m\ else\ (m\ -\ n)\ mod\ n)
+\rulename{mod_if}\isanewline
+m\ div\ n\ *\ n\ +\ m\ mod\ n\ =\ m%
+\rulename{mod_div_equality}
+\end{isabelle}
+
+Many less obvious facts about quotient and remainder are also provided.
+Here is a selection:
+\begin{isabelle}
+a\ *\ b\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c%
+\rulename{div_mult1_eq}\isanewline
+a\ *\ b\ mod\ c\ =\ a\ *\ (b\ mod\ c)\ mod\ c%
+\rulename{mod_mult1_eq}\isanewline
+a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%
+\rulename{div_mult2_eq}\isanewline
+a\ mod\ (b*c)\ =\ b * (a\ div\ b\ mod\ c)\ +\ a\ mod\ b%
+\rulename{mod_mult2_eq}\isanewline
+0\ <\ c\ \isasymLongrightarrow \ (c\ *\ a)\ div\ (c\ *\ b)\ =\ a\ div\ b%
+\rulename{div_mult_mult1}
+\end{isabelle}
+
+Surprisingly few of these results depend upon the
+divisors' being nonzero. Isabelle/HOL defines division by zero:
+\begin{isabelle}
+a\ div\ 0\ =\ 0
+\rulename{DIVISION_BY_ZERO_DIV}\isanewline
+a\ mod\ 0\ =\ a%
+\rulename{DIVISION_BY_ZERO_MOD}
+\end{isabelle}
+As a concession to convention, these equations are not installed as default
+simplification rules but are merely used to remove nonzero-divisor
+hypotheses by case analysis. In \isa{div_mult_mult1} above, one of
+the two divisors (namely~\isa{c}) must be still be nonzero.
+
+The \textbf{divides} relation has the standard definition, which
+is overloaded over all numeric types:
+\begin{isabelle}
+m\ dvd\ n\ \isasymequiv\ {\isasymexists}k.\ n\ =\ m\ *\ k
+\rulename{dvd_def}
+\end{isabelle}
+%
+Section~\ref{sec:proving-euclid} discusses proofs involving this
+relation. Here are some of the facts proved about it:
+\begin{isabelle}
+\isasymlbrakk m\ dvd\ n;\ n\ dvd\ m\isasymrbrakk \ \isasymLongrightarrow \ m\ =\ n%
+\rulename{dvd_anti_sym}\isanewline
+\isasymlbrakk k\ dvd\ m;\ k\ dvd\ n\isasymrbrakk \ \isasymLongrightarrow \ k\ dvd\ (m\ +\ n)
+\rulename{dvd_add}
+\end{isabelle}
+
+\subsubsection{Simplifier tricks}
+The rule \isa{diff_mult_distrib} shown above is one of the few facts
+about \isa{m\ -\ n} that is not subject to
+the condition \isa{n\ \isasymle \ m}. Natural number subtraction has few
+nice properties; often it is best to remove it from a subgoal
+using this split rule:
+\begin{isabelle}
+P(a-b)\ =\ ((a<b\ \isasymlongrightarrow \ P\
+0)\ \isasymand \ (\isasymforall d.\ a\ =\ b+d\ \isasymlongrightarrow \ P\
+d))
+\rulename{nat_diff_split}
+\end{isabelle}
+For example, it proves the following fact, which lies outside the scope of
+linear arithmetic:
+\begin{isabelle}
+\isacommand{lemma}\ "(n-1)*(n+1)\ =\ n*n\ -\ 1"\isanewline
+\isacommand{apply}\ (simp\ split:\ nat_diff_split)\isanewline
+\isacommand{done}
+\end{isabelle}
+
+Suppose that two expressions are equal, differing only in
+associativity and commutativity of addition. Simplifying with the
+following equations sorts the terms and groups them to the right, making
+the two expressions identical:
+\begin{isabelle}
+m\ +\ n\ +\ k\ =\ m\ +\ (n\ +\ k)
+\rulename{add_assoc}\isanewline
+m\ +\ n\ =\ n\ +\ m%
+\rulename{add_commute}\isanewline
+x\ +\ (y\ +\ z)\ =\ y\ +\ (x\
++\ z)
+\rulename{add_left_commute}
+\end{isabelle}
+The name \isa{add_ac} refers to the list of all three theorems, similarly
+there is \isa{mult_ac}. Here is an example of the sorting effect. Start
+with this goal:
+\begin{isabelle}
+\ 1.\ Suc\ (i\ +\ j\ *\ l\ *\ k\ +\ m\ *\ n)\ =\
+f\ (n\ *\ m\ +\ i\ +\ k\ *\ j\ *\ l)
+\end{isabelle}
+%
+Simplify using \isa{add_ac} and \isa{mult_ac}:
+\begin{isabelle}
+\isacommand{apply}\ (simp\ add:\ add_ac\ mult_ac)
+\end{isabelle}
+%
+Here is the resulting subgoal:
+\begin{isabelle}
+\ 1.\ Suc\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))\
+=\ f\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))%
+\end{isabelle}
+
+
+\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.
+
+Concerning simplifier tricks, we have no need to eliminate subtraction (it
+is well-behaved), but the simplifier can sort the operands of integer
+operators. The name \isa{zadd_ac} refers to the associativity and
+commutativity theorems for integer addition, while \isa{zmult_ac} has the
+analogous theorems for multiplication. The prefix~\isa{z} in many theorem
+names recalls the use of $\Bbb{Z}$ to denote the set of integers.
+
+For division and remainder, the treatment of negative divisors follows
+traditional mathematical practice: the sign of the remainder follows that
+of the divisor:
+\begin{isabelle}
+\#0\ <\ b\ \isasymLongrightarrow \ \#0\ \isasymle \ a\ mod\ b%
+\rulename{pos_mod_sign}\isanewline
+\#0\ <\ b\ \isasymLongrightarrow \ a\ mod\ b\ <\ b%
+\rulename{pos_mod_bound}\isanewline
+b\ <\ \#0\ \isasymLongrightarrow \ a\ mod\ b\ \isasymle \ \#0
+\rulename{neg_mod_sign}\isanewline
+b\ <\ \#0\ \isasymLongrightarrow \ b\ <\ a\ mod\ b%
+\rulename{neg_mod_bound}
+\end{isabelle}
+ML treats negative divisors in the same way, but most computer hardware
+treats signed operands using the same rules as for multiplication.
+
+The library provides many lemmas for proving inequalities involving integer
+multiplication and division, similar to those shown above for
+type~\isa{nat}. The absolute value function \isa{abs} is
+defined for the integers; we have for example the obvious law
+\begin{isabelle}
+\isasymbar x\ *\ y\isasymbar \ =\ \isasymbar x\isasymbar \ *\ \isasymbar y\isasymbar
+\rulename{abs_mult}
+\end{isabelle}
+
+Again, many facts about quotients and remainders are provided:
+\begin{isabelle}
+(a\ +\ b)\ div\ c\ =\isanewline
+a\ div\ c\ +\ b\ div\ c\ +\ (a\ mod\ c\ +\ b\ mod\ c)\ div\ c%
+\rulename{zdiv_zadd1_eq}
+\par\smallskip
+(a\ +\ b)\ mod\ c\ =\ (a\ mod\ c\ +\ b\ mod\ c)\ mod\ c%
+\rulename{zmod_zadd1_eq}
+\end{isabelle}
+
+\begin{isabelle}
+(a\ *\ b)\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c%
+\rulename{zdiv_zmult1_eq}\isanewline
+(a\ *\ b)\ mod\ c\ =\ a\ *\ (b\ mod\ c)\ mod\ c%
+\rulename{zmod_zmult1_eq}
+\end{isabelle}
+
+\begin{isabelle}
+\#0\ <\ c\ \isasymLongrightarrow \ a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%
+\rulename{zdiv_zmult2_eq}\isanewline
+\#0\ <\ c\ \isasymLongrightarrow \ a\ mod\ (b*c)\ =\ b*(a\ div\ b\ mod\
+c)\ +\ a\ mod\ b%
+\rulename{zmod_zmult2_eq}
+\end{isabelle}
+The last two differ from their natural number analogues by requiring
+\isa{c} to be positive. Since division by zero yields zero, we could allow
+\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$.
+
+
+\subsection{The type of real numbers, {\tt\slshape real}}
+
+As with the other numeric types, the simplifier can sort the operands of
+addition and multiplication. The name \isa{real_add_ac} refers to the
+associativity and commutativity theorems for addition; similarly
+\isa{real_mult_ac} contains those properties for multiplication.
+
+\textbf{To be written. Inverse, abs, theorems about density, etc.?}