doc-src/TutorialI/Types/numerics.tex

Moving some theorems from Real/RealArith0.ML

% $Id$

\section{Numbers}
\label{sec:numbers}

\index{numbers|(}%
Until now, our numerical examples 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.  HOL also provides the type
\isa{int} of \textbf{integers}, which lack induction but support true
subtraction.  The integers are preferable to the natural numbers for reasoning about
complicated arithmetic expressions, even for some expressions whose
value is non-negative.  The logic HOL-Complex also has the types
\isa{real} and \isa{complex}: the real and complex numbers.  Isabelle has no 
subtyping,  so the numeric
types are distinct and there are functions to convert between them.
Fortunately most numeric operations are overloaded: the same symbol can be
used at all numeric types. Table~\ref{tab:overloading} in the appendix
shows the most important operations, together with the priorities of the
infix symbols.

\index{linear arithmetic}%
Many theorems involving numeric types can be proved automatically by
Isabelle's arithmetic decision procedure, the method
\methdx{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.  On types \isa{nat} and \isa{int}, \methdx{arith}
can deal with quantifiers (this is known as ``Presburger Arithmetic''),
whereas on type \isa{real} it cannot.

The simplifier reduces arithmetic expressions in other
ways, such as dividing through by common factors.  For problems that lie
outside the scope of automation, HOL provides hundreds of
theorems about multiplication, division, etc., that can be brought to
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}
\label{sec:numerals}

\index{numeric literals|(}%
The constants \cdx{0} and \cdx{1} are overloaded.  They denote zero and one,
respectively, for all numeric types.  Other values are expressed by numeric
literals, which consist of one or more decimal digits optionally preceeded by
a minus sign (\isa{-}).  Examples are \isa{2}, \isa{-3} and
\isa{441223334678}.  Literals are available for the types of natural numbers,
integers and reals; they denote integer values of arbitrary size.

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 include addition, subtraction, multiplication, 
integer division and remainder.  Fractions of literals (expressed using
division) are reduced to lowest terms.

\begin{warn}\index{overloading!and arithmetic}
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:
\par
\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.
\end{warn}

\begin{warn}
\index{recdef@\isacommand {recdef} (command)!and numeric literals}  
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}
\index{numeric literals|)}
\end{warn}



\subsection{The Type of Natural Numbers, {\tt\slshape nat}}

\index{natural numbers|(}\index{*nat (type)|(}%
This type requires no introduction: we have been using it from the
beginning.  Hundreds of theorems about the natural numbers are
proved in the theories \isa{Nat}, \isa{NatArith} and \isa{Divides}.  Only
in exceptional circumstances should you resort to induction.

\subsubsection{Literals}
\index{numeric literals!for type \protect\isa{nat}}%
The notational options for the natural  numbers are confusing.  Recall that an
overloaded constant can be defined independently for each type; the definition
of \cdx{1} for type \isa{nat} is
\begin{isabelle}
1\ \isasymequiv\ Suc\ 0
\rulename{One_nat_def}
\end{isabelle}
This is installed as a simplification rule, so the simplifier will replace
every occurrence of \isa{1::nat} by \isa{Suc\ 0}.  Literals are obviously
better than nested \isa{Suc}s at expressing large values.  But many theorems,
including the rewrite rules for primitive recursive functions, can only be
applied to terms of the form \isa{Suc\ $n$}.

The following default  simplification rules replace
small literals by zero and successor: 
\begin{isabelle}
2\ +\ n\ =\ Suc\ (Suc\ n)
\rulename{add_2_eq_Suc}\isanewline
n\ +\ 2\ =\ Suc\ (Suc\ n)
\rulename{add_2_eq_Suc'}
\end{isabelle}
It is less easy to transform \isa{100} into \isa{Suc\ 99} (for example), and
the simplifier will normally reverse this transformation.  Novices should
express natural numbers using \isa{0} and \isa{Suc} only.

\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%
\rulenamedx{add_mult_distrib}\isanewline
(m\ -\ n)\ *\ k\ =\ m\ *\ k\ -\ n\ *\ k%
\rulenamedx{diff_mult_distrib}\isanewline
(m\ mod\ n)\ *\ k\ =\ (m\ *\ k)\ mod\ (n\ *\ k)
\rulenamedx{mod_mult_distrib}
\end{isabelle}

\subsubsection{Division}
\index{division!for type \protect\isa{nat}}%
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
m\ div\ n\ *\ n\ +\ m\ mod\ n\ =\ m%
\rulenamedx{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.
\index{division!by zero}%
That is because division by
zero yields 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.  In \isa{div_mult_mult1} above, one of
the two divisors (namely~\isa{c}) must still be nonzero.

The \textbf{divides} relation\index{divides relation}
has the standard definition, which
is overloaded over all numeric types: 
\begin{isabelle}
m\ dvd\ n\ \isasymequiv\ {\isasymexists}k.\ n\ =\ m\ *\ k
\rulenamedx{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%
\rulenamedx{dvd_anti_sym}\isanewline
\isasymlbrakk k\ dvd\ m;\ k\ dvd\ n\isasymrbrakk \ \isasymLongrightarrow \ k\ dvd\ (m\ +\ n)
\rulenamedx{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 you should remove it by simplifying with 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, splitting helps to prove the following fact:
\begin{isabelle}
\isacommand{lemma}\ "(n\ -\ 2)\ *\ (n\ +\ 2)\ =\ n\ *\ n\ -\ (4::nat)"\isanewline
\isacommand{apply}\ (simp\ split:\ nat_diff_split,\ clarify)\isanewline
\ 1.\ \isasymAnd d.\ \isasymlbrakk n\ <\ 2;\ n\ *\ n\ =\ 4\ +\ d\isasymrbrakk \ \isasymLongrightarrow \ d\ =\ 0
\end{isabelle}
The result lies outside the scope of linear arithmetic, but
 it is easily found
if we explicitly split \isa{n<2} as \isa{n=0} or \isa{n=1}:
\begin{isabelle}
\isacommand{apply}\ (subgoal_tac\ "n=0\ |\ n=1",\ force,\ arith)\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)
\rulenamedx{add_assoc}\isanewline
m\ +\ n\ =\ n\ +\ m%
\rulenamedx{add_commute}\isanewline
x\ +\ (y\ +\ z)\ =\ y\ +\ (x\
+\ z)
\rulename{add_left_commute}
\end{isabelle}
The name \isa{add_ac}\index{*add_ac (theorems)} 
refers to the list of all three theorems; similarly
there is \isa{mult_ac}.\index{*mult_ac (theorems)} 
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}%
\index{natural numbers|)}\index{*nat (type)|)}



\subsection{The Type of Integers, {\tt\slshape int}}

\index{integers|(}\index{*int (type)|(}%
Reasoning methods resemble those for the natural numbers, but induction and
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}.  

The \rmindex{absolute value} function \cdx{abs} is overloaded for the numeric types.
It 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}

\begin{warn}
The absolute value bars shown above cannot be typed on a keyboard.  They
can be entered using the X-symbol package.  In \textsc{ascii}, type \isa{abs x} to
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}\ "abs\ (x+y)\ \isasymle \ abs\ x\ +\ abs\ (y\ ::\ 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
operands of sums and products.  The name \isa{zadd_ac}\index{*zadd_ac (theorems)}
refers to the
associativity and commutativity theorems for integer addition, while
\isa{zmult_ac}\index{*zmult_ac (theorems)}
has the analogous theorems for multiplication.  The
prefix~\isa{z} in many theorem names recalls the use of $\mathbb{Z}$ to
denote the set of integers.

For division and remainder,\index{division!by negative numbers}
the treatment of negative divisors follows
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.
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$.%
\index{integers|)}\index{*int (type)|)}

Induction is less important for integers than it is for the natural numbers, but it can be valuable if the range of integers has a lower or upper bound.  There are four rules for integer induction, corresponding to the possible relations of the bound ($\geq$, $>$, $\leq$ and $<$):
\begin{isabelle}
\isasymlbrakk k\ \isasymle \ i;\ P\ k;\ \isasymAnd i.\ \isasymlbrakk k\ \isasymle \ i;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i+1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%
\rulename{int_ge_induct}\isanewline
\isasymlbrakk k\ <\ i;\ P(k+1);\ \isasymAnd i.\ \isasymlbrakk k\ <\ i;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i+1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%
\rulename{int_gr_induct}\isanewline
\isasymlbrakk i\ \isasymle \ k;\ P\ k;\ \isasymAnd i.\ \isasymlbrakk i\ \isasymle \ k;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i-1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%
\rulename{int_le_induct}\isanewline
\isasymlbrakk i\ <\ k;\ P(k-1);\ \isasymAnd i.\ \isasymlbrakk i\ <\ k;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i-1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%
\rulename{int_less_induct}
\end{isabelle}


\subsection{The Type of Real Numbers, {\tt\slshape real}}

\index{real numbers|(}\index{*real (type)|(}%
The real numbers enjoy two significant properties that the integers lack. 
They are
\textbf{dense}: between every two distinct real numbers there lies another.
This property follows from the division laws, since if $x<y$ then between
them lies $(x+y)/2$.  The second property is that they are
\textbf{complete}: every set of reals that is bounded above has a least
upper bound.  Completeness distinguishes the reals from the rationals, for
which the set $\{x\mid x^2<2\}$ has no least upper bound.  (It could only be
$\surd2$, which is irrational.)
The formalization of completeness is complicated; rather than
reproducing it here, we refer you to the theory \texttt{RComplete} in
directory \texttt{Real}.
Density, however, is trivial to express:
\begin{isabelle}
x\ <\ y\ \isasymLongrightarrow \ \isasymexists r.\ x\ <\ r\ \isasymand \ r\ <\ y%
\rulename{real_dense}
\end{isabelle}

Here is a selection of rules about the division operator.  The following
are installed as default simplification rules in order to express
combinations of products and quotients as rational expressions:
\begin{isabelle}
a\ *\ (b\ /\ c)\ =\ a\ *\ b\ /\ c
\rulename{times_divide_eq_right}\isanewline
b\ /\ c\ *\ a\ =\ b\ *\ a\ /\ c
\rulename{times_divide_eq_left}\isanewline
a\ /\ (b\ /\ c)\ =\ a\ *\ c\ /\ b
\rulename{divide_divide_eq_right}\isanewline
a\ /\ b\ /\ c\ =\ a\ /\ (b\ *\ c)
\rulename{divide_divide_eq_left}
\end{isabelle}

Signs are extracted from quotients in the hope that complementary terms can
then be cancelled:
\begin{isabelle}
-\ x\ /\ y\ =\ -\ (x\ /\ y)
\rulename{real_minus_divide_eq}\isanewline
x\ /\ -\ y\ =\ -\ (x\ /\ y)
\rulename{real_divide_minus_eq}
\end{isabelle}

The following distributive law is available, but it is not installed as a
simplification rule.
\begin{isabelle}
(x\ +\ y)\ /\ z\ =\ x\ /\ z\ +\ y\ /\ z%
\rulename{real_add_divide_distrib}
\end{isabelle}

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, while similarly
\isa{real_mult_ac} contains those properties for multiplication. 

The absolute value function \isa{abs} is
defined for the reals, along with many theorems such as this one about
exponentiation:
\begin{isabelle}
\isasymbar r\ \isacharcircum \ n\isasymbar\ =\ 
\isasymbar r\isasymbar \ \isacharcircum \ n
\rulename{realpow_abs}
\end{isabelle}

Numeric literals\index{numeric literals!for type \protect\isa{real}}
for type \isa{real} have the same syntax as those for type
\isa{int} and only express integral values.  Fractions expressed
using the division operator are automatically simplified to lowest terms:
\begin{isabelle}
\ 1.\ P\ ((3\ /\ 4)\ *\ (8\ /\ 15))\isanewline
\isacommand{apply} simp\isanewline
\ 1.\ P\ (2\ /\ 5)
\end{isabelle}
Exponentiation can express floating-point values such as
\isa{2 * 10\isacharcircum6}, but at present no special simplification
is performed.


\begin{warn}
Type \isa{real} is only available in the logic HOL-Complex, which
is  HOL extended with a definitional development of the real and complex
numbers.  Base your theory upon theory
\thydx{Complex_Main}, not the usual \isa{Main}.%
\index{real numbers|)}\index{*real (type)|)}
Launch Isabelle using the command 
\begin{verbatim}
Isabelle -l HOL-Complex
\end{verbatim}
\end{warn}

Also available in HOL-Complex is the
theory \isa{Hyperreal}, which define the type \tydx{hypreal} of 
\rmindex{non-standard reals}.  These
\textbf{hyperreals} include infinitesimals, which represent infinitely
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}.  The 
relation $x\approx y$ means ``$x$ is infinitely close to~$y$.''
Theory \isa{Hyperreal} also defines transcendental functions such as sine,
cosine, exponential and logarithm --- even the versions for type
\isa{real}, because they are defined using nonstandard limits.%
\index{numbers|)}