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}
\label{sec:numerals}
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 $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.?}