10794

1 
% $Id$


2 
Until now, our numerical have used the type of \textbf{natural numbers},

10594

3 
\isa{nat}. This is a recursive datatype generated by the constructors


4 
zero and successor, so it works well with inductive proofs and primitive

10794

5 
recursive function definitions. Isabelle/HOL also provides the type


6 
\isa{int} of \textbf{integers}, which lack induction but support true

10881

7 
subtraction. The logic HOLReal also has the type \isa{real} of real

10777

8 
numbers. Isabelle has no subtyping, so the numeric types are distinct and

10978

9 
there are functions to convert between them. Fortunately most numeric


10 
operations are overloaded: the same symbol can be used at all numeric types.


11 
Table~\ref{tab:overloading} in the appendix shows the most important operations,


12 
together with the priorities of the infix symbols.

10594

13 


14 
The integers are preferable to the natural numbers for reasoning about


15 
complicated arithmetic expressions. For example, a termination proof


16 
typically involves an integer metric that is shown to decrease at each

10794

17 
loop iteration. Even if the metric cannot become negative, proofs


18 
may be easier if you use the integers instead of the natural

10594

19 
numbers.


20 


21 
Many theorems involving numeric types can be proved automatically by


22 
Isabelle's arithmetic decision procedure, the method


23 
\isa{arith}. Linear arithmetic comprises addition, subtraction


24 
and multiplication by constant factors; subterms involving other operators


25 
are regarded as variables. The procedure can be slow, especially if the


26 
subgoal to be proved involves subtraction over type \isa{nat}, which


27 
causes case splits.


28 


29 
The simplifier reduces arithmetic expressions in other


30 
ways, such as dividing through by common factors. For problems that lie

10881

31 
outside the scope of automation, HOL provides hundreds of

10594

32 
theorems about multiplication, division, etc., that can be brought to

10881

33 
bear. You can locate them using Proof General's Find


34 
button. A few lemmas are given below to show what

10794

35 
is available.

10594

36 


37 
\subsection{Numeric Literals}

10779

38 
\label{sec:numerals}

10594

39 


40 
Literals are available for the types of natural numbers, integers


41 
and reals and denote integer values of arbitrary size.


42 
They begin


43 
with a number sign (\isa{\#}), have an optional minus sign (\isa{}) and


44 
then one or more decimal digits. Examples are \isa{\#0}, \isa{\#3}


45 
and \isa{\#441223334678}.


46 


47 
Literals look like constants, but they abbreviate


48 
terms, representing the number in a two's complement binary notation.

10794

49 
Isabelle performs arithmetic on literals by rewriting rather

10594

50 
than using the hardware arithmetic. In most cases arithmetic


51 
is fast enough, even for large numbers. The arithmetic operations

10794

52 
provided for literals include addition, subtraction, multiplication,


53 
integer division and remainder. Fractions of literals (expressed using


54 
division) are reduced to lowest terms.

10594

55 

10794

56 
\begin{warn}


57 
The arithmetic operators are

10594

58 
overloaded, so you must be careful to ensure that each numeric


59 
expression refers to a specific type, if necessary by inserting


60 
type constraints. Here is an example of what can go wrong:

10794

61 
\par

10594

62 
\begin{isabelle}


63 
\isacommand{lemma}\ "\#2\ *\ m\ =\ m\ +\ m"


64 
\end{isabelle}


65 
%


66 
Carefully observe how Isabelle displays the subgoal:


67 
\begin{isabelle}


68 
\ 1.\ (\#2::'a)\ *\ m\ =\ m\ +\ m


69 
\end{isabelle}


70 
The type \isa{'a} given for the literal \isa{\#2} warns us that no numeric


71 
type has been specified. The problem is underspecified. Given a type


72 
constraint such as \isa{nat}, \isa{int} or \isa{real}, it becomes trivial.

10794

73 
\end{warn}


74 

10881

75 
\begin{warn}


76 
Numeric literals are not constructors and therefore must not be used in


77 
patterns. For example, this declaration is rejected:


78 
\begin{isabelle}


79 
\isacommand{recdef}\ h\ "\isacharbraceleft \isacharbraceright "\isanewline

11148

80 
"h\ \#3\ =\ \#2"\isanewline


81 
"h\ i\ \ =\ i"

10881

82 
\end{isabelle}


83 


84 
You should use a conditional expression instead:


85 
\begin{isabelle}


86 
"h\ i\ =\ (if\ i\ =\ \#3\ then\ \#2\ else\ i)"


87 
\end{isabelle}


88 
\end{warn}


89 

10594

90 


91 


92 
\subsection{The type of natural numbers, {\tt\slshape nat}}


93 


94 
This type requires no introduction: we have been using it from the

10794

95 
beginning. Hundreds of theorems about the natural numbers are

10594

96 
proved in the theories \isa{Nat}, \isa{NatArith} and \isa{Divides}. Only


97 
in exceptional circumstances should you resort to induction.


98 


99 
\subsubsection{Literals}


100 
The notational options for the natural numbers can be confusing. The


101 
constant \isa{0} is overloaded to serve as the neutral value


102 
in a variety of additive types. The symbols \isa{1} and \isa{2} are


103 
not constants but abbreviations for \isa{Suc 0} and \isa{Suc(Suc 0)},


104 
respectively. The literals \isa{\#0}, \isa{\#1} and \isa{\#2} are

10794

105 
syntactically different from \isa{0}, \isa{1} and \isa{2}. You will

10594

106 
sometimes prefer one notation to the other. Literals are obviously

10794

107 
necessary to express large values, while \isa{0} and \isa{Suc} are needed


108 
in order to match many theorems, including the rewrite rules for primitive


109 
recursive functions. The following default simplification rules replace


110 
small literals by zero and successor:

10594

111 
\begin{isabelle}


112 
\#0\ =\ 0


113 
\rulename{numeral_0_eq_0}\isanewline


114 
\#1\ =\ 1


115 
\rulename{numeral_1_eq_1}\isanewline


116 
\#2\ +\ n\ =\ Suc\ (Suc\ n)


117 
\rulename{add_2_eq_Suc}\isanewline


118 
n\ +\ \#2\ =\ Suc\ (Suc\ n)


119 
\rulename{add_2_eq_Suc'}


120 
\end{isabelle}


121 
In special circumstances, you may wish to remove or reorient


122 
these rules.


123 


124 
\subsubsection{Typical lemmas}


125 
Inequalities involving addition and subtraction alone can be proved


126 
automatically. Lemmas such as these can be used to prove inequalities


127 
involving multiplication and division:


128 
\begin{isabelle}


129 
\isasymlbrakk i\ \isasymle \ j;\ k\ \isasymle \ l\isasymrbrakk \ \isasymLongrightarrow \ i\ *\ k\ \isasymle \ j\ *\ l%


130 
\rulename{mult_le_mono}\isanewline


131 
\isasymlbrakk i\ <\ j;\ 0\ <\ k\isasymrbrakk \ \isasymLongrightarrow \ i\


132 
*\ k\ <\ j\ *\ k%


133 
\rulename{mult_less_mono1}\isanewline


134 
m\ \isasymle \ n\ \isasymLongrightarrow \ m\ div\ k\ \isasymle \ n\ div\ k%


135 
\rulename{div_le_mono}


136 
\end{isabelle}


137 
%


138 
Various distributive laws concerning multiplication are available:


139 
\begin{isabelle}


140 
(m\ +\ n)\ *\ k\ =\ m\ *\ k\ +\ n\ *\ k%


141 
\rulename{add_mult_distrib}\isanewline


142 
(m\ \ n)\ *\ k\ =\ m\ *\ k\ \ n\ *\ k%


143 
\rulename{diff_mult_distrib}\isanewline


144 
(m\ mod\ n)\ *\ k\ =\ (m\ *\ k)\ mod\ (n\ *\ k)


145 
\rulename{mod_mult_distrib}


146 
\end{isabelle}


147 


148 
\subsubsection{Division}

10881

149 
The infix operators \isa{div} and \isa{mod} are overloaded.


150 
Isabelle/HOL provides the basic facts about quotient and remainder


151 
on the natural numbers:

10594

152 
\begin{isabelle}


153 
m\ mod\ n\ =\ (if\ m\ <\ n\ then\ m\ else\ (m\ \ n)\ mod\ n)


154 
\rulename{mod_if}\isanewline


155 
m\ div\ n\ *\ n\ +\ m\ mod\ n\ =\ m%


156 
\rulename{mod_div_equality}


157 
\end{isabelle}


158 


159 
Many less obvious facts about quotient and remainder are also provided.


160 
Here is a selection:


161 
\begin{isabelle}


162 
a\ *\ b\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c%


163 
\rulename{div_mult1_eq}\isanewline


164 
a\ *\ b\ mod\ c\ =\ a\ *\ (b\ mod\ c)\ mod\ c%


165 
\rulename{mod_mult1_eq}\isanewline


166 
a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%


167 
\rulename{div_mult2_eq}\isanewline


168 
a\ mod\ (b*c)\ =\ b * (a\ div\ b\ mod\ c)\ +\ a\ mod\ b%


169 
\rulename{mod_mult2_eq}\isanewline


170 
0\ <\ c\ \isasymLongrightarrow \ (c\ *\ a)\ div\ (c\ *\ b)\ =\ a\ div\ b%


171 
\rulename{div_mult_mult1}


172 
\end{isabelle}


173 


174 
Surprisingly few of these results depend upon the

10794

175 
divisors' being nonzero. That is because division by


176 
zero yields zero:

10594

177 
\begin{isabelle}


178 
a\ div\ 0\ =\ 0


179 
\rulename{DIVISION_BY_ZERO_DIV}\isanewline


180 
a\ mod\ 0\ =\ a%


181 
\rulename{DIVISION_BY_ZERO_MOD}


182 
\end{isabelle}


183 
As a concession to convention, these equations are not installed as default


184 
simplification rules but are merely used to remove nonzerodivisor


185 
hypotheses by case analysis. In \isa{div_mult_mult1} above, one of


186 
the two divisors (namely~\isa{c}) must be still be nonzero.


187 


188 
The \textbf{divides} relation has the standard definition, which


189 
is overloaded over all numeric types:


190 
\begin{isabelle}


191 
m\ dvd\ n\ \isasymequiv\ {\isasymexists}k.\ n\ =\ m\ *\ k


192 
\rulename{dvd_def}


193 
\end{isabelle}


194 
%


195 
Section~\ref{sec:provingeuclid} discusses proofs involving this


196 
relation. Here are some of the facts proved about it:


197 
\begin{isabelle}


198 
\isasymlbrakk m\ dvd\ n;\ n\ dvd\ m\isasymrbrakk \ \isasymLongrightarrow \ m\ =\ n%


199 
\rulename{dvd_anti_sym}\isanewline


200 
\isasymlbrakk k\ dvd\ m;\ k\ dvd\ n\isasymrbrakk \ \isasymLongrightarrow \ k\ dvd\ (m\ +\ n)


201 
\rulename{dvd_add}


202 
\end{isabelle}


203 


204 
\subsubsection{Simplifier tricks}


205 
The rule \isa{diff_mult_distrib} shown above is one of the few facts


206 
about \isa{m\ \ n} that is not subject to


207 
the condition \isa{n\ \isasymle \ m}. Natural number subtraction has few

10794

208 
nice properties; often you should remove it by simplifying with this split


209 
rule:

10594

210 
\begin{isabelle}


211 
P(ab)\ =\ ((a<b\ \isasymlongrightarrow \ P\


212 
0)\ \isasymand \ (\isasymforall d.\ a\ =\ b+d\ \isasymlongrightarrow \ P\


213 
d))


214 
\rulename{nat_diff_split}


215 
\end{isabelle}


216 
For example, it proves the following fact, which lies outside the scope of


217 
linear arithmetic:


218 
\begin{isabelle}


219 
\isacommand{lemma}\ "(n1)*(n+1)\ =\ n*n\ \ 1"\isanewline


220 
\isacommand{apply}\ (simp\ split:\ nat_diff_split)\isanewline


221 
\isacommand{done}


222 
\end{isabelle}


223 


224 
Suppose that two expressions are equal, differing only in


225 
associativity and commutativity of addition. Simplifying with the


226 
following equations sorts the terms and groups them to the right, making


227 
the two expressions identical:


228 
\begin{isabelle}


229 
m\ +\ n\ +\ k\ =\ m\ +\ (n\ +\ k)


230 
\rulename{add_assoc}\isanewline


231 
m\ +\ n\ =\ n\ +\ m%


232 
\rulename{add_commute}\isanewline


233 
x\ +\ (y\ +\ z)\ =\ y\ +\ (x\


234 
+\ z)


235 
\rulename{add_left_commute}


236 
\end{isabelle}


237 
The name \isa{add_ac} refers to the list of all three theorems, similarly


238 
there is \isa{mult_ac}. Here is an example of the sorting effect. Start


239 
with this goal:


240 
\begin{isabelle}


241 
\ 1.\ Suc\ (i\ +\ j\ *\ l\ *\ k\ +\ m\ *\ n)\ =\


242 
f\ (n\ *\ m\ +\ i\ +\ k\ *\ j\ *\ l)


243 
\end{isabelle}


244 
%


245 
Simplify using \isa{add_ac} and \isa{mult_ac}:


246 
\begin{isabelle}


247 
\isacommand{apply}\ (simp\ add:\ add_ac\ mult_ac)


248 
\end{isabelle}


249 
%


250 
Here is the resulting subgoal:


251 
\begin{isabelle}


252 
\ 1.\ Suc\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))\


253 
=\ f\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))%


254 
\end{isabelle}


255 


256 


257 
\subsection{The type of integers, {\tt\slshape int}}


258 

10794

259 
Reasoning methods resemble those for the natural numbers, but induction and

10881

260 
the constant \isa{Suc} are not available. HOL provides many lemmas

10794

261 
for proving inequalities involving integer multiplication and division,


262 
similar to those shown above for type~\isa{nat}.


263 


264 
The absolute value function \isa{abs} is overloaded for the numeric types.


265 
It is defined for the integers; we have for example the obvious law


266 
\begin{isabelle}


267 
\isasymbar x\ *\ y\isasymbar \ =\ \isasymbar x\isasymbar \ *\ \isasymbar y\isasymbar


268 
\rulename{abs_mult}


269 
\end{isabelle}

10594

270 

10794

271 
\begin{warn}


272 
The absolute value bars shown above cannot be typed on a keyboard. They

10983

273 
can be entered using the Xsymbol package. In \textsc{ascii}, type \isa{abs x} to

10794

274 
get \isa{\isasymbar x\isasymbar}.


275 
\end{warn}


276 

10881

277 
The \isa{arith} method can prove facts about \isa{abs} automatically,


278 
though as it does so by case analysis, the cost can be exponential.


279 
\begin{isabelle}


280 
\isacommand{lemma}\ "\isasymlbrakk abs\ x\ <\ a;\ abs\ y\ <\ b\isasymrbrakk \ \isasymLongrightarrow \ abs\ x\ +\ abs\ y\ <\ (a\ +\ b\ ::\ int)"\isanewline


281 
\isacommand{by}\ arith


282 
\end{isabelle}

10794

283 


284 
Concerning simplifier tricks, we have no need to eliminate subtraction: it


285 
is wellbehaved. As with the natural numbers, the simplifier can sort the


286 
operands of sums and products. The name \isa{zadd_ac} refers to the


287 
associativity and commutativity theorems for integer addition, while


288 
\isa{zmult_ac} has the analogous theorems for multiplication. The


289 
prefix~\isa{z} in many theorem names recalls the use of $\mathbb{Z}$ to


290 
denote the set of integers.

10594

291 


292 
For division and remainder, the treatment of negative divisors follows

10794

293 
mathematical practice: the sign of the remainder follows that

10594

294 
of the divisor:


295 
\begin{isabelle}


296 
\#0\ <\ b\ \isasymLongrightarrow \ \#0\ \isasymle \ a\ mod\ b%


297 
\rulename{pos_mod_sign}\isanewline


298 
\#0\ <\ b\ \isasymLongrightarrow \ a\ mod\ b\ <\ b%


299 
\rulename{pos_mod_bound}\isanewline


300 
b\ <\ \#0\ \isasymLongrightarrow \ a\ mod\ b\ \isasymle \ \#0


301 
\rulename{neg_mod_sign}\isanewline


302 
b\ <\ \#0\ \isasymLongrightarrow \ b\ <\ a\ mod\ b%


303 
\rulename{neg_mod_bound}


304 
\end{isabelle}


305 
ML treats negative divisors in the same way, but most computer hardware


306 
treats signed operands using the same rules as for multiplication.

10794

307 
Many facts about quotients and remainders are provided:

10594

308 
\begin{isabelle}


309 
(a\ +\ b)\ div\ c\ =\isanewline


310 
a\ div\ c\ +\ b\ div\ c\ +\ (a\ mod\ c\ +\ b\ mod\ c)\ div\ c%


311 
\rulename{zdiv_zadd1_eq}


312 
\par\smallskip


313 
(a\ +\ b)\ mod\ c\ =\ (a\ mod\ c\ +\ b\ mod\ c)\ mod\ c%


314 
\rulename{zmod_zadd1_eq}


315 
\end{isabelle}


316 


317 
\begin{isabelle}


318 
(a\ *\ b)\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c%


319 
\rulename{zdiv_zmult1_eq}\isanewline


320 
(a\ *\ b)\ mod\ c\ =\ a\ *\ (b\ mod\ c)\ mod\ c%


321 
\rulename{zmod_zmult1_eq}


322 
\end{isabelle}


323 


324 
\begin{isabelle}


325 
\#0\ <\ c\ \isasymLongrightarrow \ a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%


326 
\rulename{zdiv_zmult2_eq}\isanewline


327 
\#0\ <\ c\ \isasymLongrightarrow \ a\ mod\ (b*c)\ =\ b*(a\ div\ b\ mod\


328 
c)\ +\ a\ mod\ b%


329 
\rulename{zmod_zmult2_eq}


330 
\end{isabelle}


331 
The last two differ from their natural number analogues by requiring


332 
\isa{c} to be positive. Since division by zero yields zero, we could allow


333 
\isa{c} to be zero. However, \isa{c} cannot be negative: a counterexample


334 
is


335 
$\isa{a} = 7$, $\isa{b} = 2$ and $\isa{c} = 3$, when the lefthand side of

10881

336 
\isa{zdiv_zmult2_eq} is $2$ while the righthand side is~$1$.

10594

337 


338 


339 
\subsection{The type of real numbers, {\tt\slshape real}}


340 

10777

341 
The real numbers enjoy two significant properties that the integers lack.


342 
They are


343 
\textbf{dense}: between every two distinct real numbers there lies another.


344 
This property follows from the division laws, since if $x<y$ then between


345 
them lies $(x+y)/2$. The second property is that they are


346 
\textbf{complete}: every set of reals that is bounded above has a least


347 
upper bound. Completeness distinguishes the reals from the rationals, for


348 
which the set $\{x\mid x^2<2\}$ has no least upper bound. (It could only be


349 
$\surd2$, which is irrational.)

10794

350 
The formalization of completeness is complicated; rather than

10777

351 
reproducing it here, we refer you to the theory \texttt{RComplete} in


352 
directory \texttt{Real}.

10794

353 
Density, however, is trivial to express:

10777

354 
\begin{isabelle}


355 
x\ <\ y\ \isasymLongrightarrow \ \isasymexists r.\ x\ <\ r\ \isasymand \ r\ <\ y%


356 
\rulename{real_dense}


357 
\end{isabelle}


358 


359 
Here is a selection of rules about the division operator. The following


360 
are installed as default simplification rules in order to express


361 
combinations of products and quotients as rational expressions:


362 
\begin{isabelle}


363 
x\ *\ (y\ /\ z)\ =\ x\ *\ y\ /\ z%


364 
\rulename{real_times_divide1_eq}\isanewline


365 
y\ /\ z\ *\ x\ =\ y\ *\ x\ /\ z%


366 
\rulename{real_times_divide2_eq}\isanewline


367 
x\ /\ (y\ /\ z)\ =\ x\ *\ z\ /\ y%


368 
\rulename{real_divide_divide1_eq}\isanewline


369 
x\ /\ y\ /\ z\ =\ x\ /\ (y\ *\ z)


370 
\rulename{real_divide_divide2_eq}


371 
\end{isabelle}


372 


373 
Signs are extracted from quotients in the hope that complementary terms can


374 
then be cancelled:


375 
\begin{isabelle}


376 
\ x\ /\ y\ =\ \ (x\ /\ y)


377 
\rulename{real_minus_divide_eq}\isanewline


378 
x\ /\ \ y\ =\ \ (x\ /\ y)


379 
\rulename{real_divide_minus_eq}


380 
\end{isabelle}


381 


382 
The following distributive law is available, but it is not installed as a


383 
simplification rule.


384 
\begin{isabelle}


385 
(x\ +\ y)\ /\ z\ =\ x\ /\ z\ +\ y\ /\ z%


386 
\rulename{real_add_divide_distrib}


387 
\end{isabelle}


388 

10594

389 
As with the other numeric types, the simplifier can sort the operands of


390 
addition and multiplication. The name \isa{real_add_ac} refers to the

10777

391 
associativity and commutativity theorems for addition, while similarly

10594

392 
\isa{real_mult_ac} contains those properties for multiplication.


393 

10777

394 
The absolute value function \isa{abs} is


395 
defined for the reals, along with many theorems such as this one about


396 
exponentiation:


397 
\begin{isabelle}


398 
\isasymbar r\isasymbar \ \isacharcircum \ n\ =\ \isasymbar r\ \isacharcircum \ n\isasymbar


399 
\rulename{realpow_abs}


400 
\end{isabelle}


401 

10881

402 
\begin{warn}


403 
Type \isa{real} is only available in the logic HOLReal, which

10777

404 
is HOL extended with the rather substantial development of the real


405 
numbers. Base your theory upon theory \isa{Real}, not the usual \isa{Main}.

10881

406 
\end{warn}

10777

407 


408 
Also distributed with Isabelle is HOLHyperreal,


409 
whose theory \isa{Hyperreal} defines the type \isa{hypreal} of nonstandard


410 
reals. These


411 
\textbf{hyperreals} include infinitesimals, which represent infinitely


412 
small and infinitely large quantities; they facilitate proofs

10794

413 
about limits, differentiation and integration~\cite{fleuriotjcm}. The


414 
development defines an infinitely large number, \isa{omega} and an

10881

415 
infinitely small positive number, \isa{epsilon}. The


416 
relation $x\approx y$ means ``$x$ is infinitely close to~$y$''.
