7 Until now, our numerical examples have used the type of \textbf{natural
9 \isa{nat}. This is a recursive datatype generated by the constructors
10 zero and successor, so it works well with inductive proofs and primitive
11 recursive function definitions. HOL also provides the type
12 \isa{int} of \textbf{integers}, which lack induction but support true
13 subtraction. The integers are preferable to the natural numbers for reasoning about
14 complicated arithmetic expressions, even for some expressions whose
15 value is non-negative. The logic HOL-Real also has the type
16 \isa{real} of real numbers. Isabelle has no subtyping, so the numeric
17 types are distinct and there are functions to convert between them.
18 Fortunately most numeric operations are overloaded: the same symbol can be
19 used at all numeric types. Table~\ref{tab:overloading} in the appendix
20 shows the most important operations, together with the priorities of the
23 \index{linear arithmetic}%
24 Many theorems involving numeric types can be proved automatically by
25 Isabelle's arithmetic decision procedure, the method
26 \methdx{arith}. Linear arithmetic comprises addition, subtraction
27 and multiplication by constant factors; subterms involving other operators
28 are regarded as variables. The procedure can be slow, especially if the
29 subgoal to be proved involves subtraction over type \isa{nat}, which
32 The simplifier reduces arithmetic expressions in other
33 ways, such as dividing through by common factors. For problems that lie
34 outside the scope of automation, HOL provides hundreds of
35 theorems about multiplication, division, etc., that can be brought to
36 bear. You can locate them using Proof General's Find
37 button. A few lemmas are given below to show what
40 \subsection{Numeric Literals}
43 \index{numeric literals|(}%
44 The constants \cdx{0} and \cdx{1} are overloaded. They denote zero and one,
45 respectively, for all numeric types. Other values are expressed by numeric
46 literals, which consist of one or more decimal digits optionally preceeded by
47 a minus sign (\isa{-}). Examples are \isa{2}, \isa{-3} and
48 \isa{441223334678}. Literals are available for the types of natural numbers,
49 integers and reals; they denote integer values of arbitrary size.
51 Literals look like constants, but they abbreviate
52 terms representing the number in a two's complement binary notation.
53 Isabelle performs arithmetic on literals by rewriting rather
54 than using the hardware arithmetic. In most cases arithmetic
55 is fast enough, even for large numbers. The arithmetic operations
56 provided for literals include addition, subtraction, multiplication,
57 integer division and remainder. Fractions of literals (expressed using
58 division) are reduced to lowest terms.
60 \begin{warn}\index{overloading!and arithmetic}
61 The arithmetic operators are
62 overloaded, so you must be careful to ensure that each numeric
63 expression refers to a specific type, if necessary by inserting
64 type constraints. Here is an example of what can go wrong:
67 \isacommand{lemma}\ "2\ *\ m\ =\ m\ +\ m"
70 Carefully observe how Isabelle displays the subgoal:
72 \ 1.\ (2::'a)\ *\ m\ =\ m\ +\ m
74 The type \isa{'a} given for the literal \isa{2} warns us that no numeric
75 type has been specified. The problem is underspecified. Given a type
76 constraint such as \isa{nat}, \isa{int} or \isa{real}, it becomes trivial.
80 \index{recdef@\isacommand {recdef} (command)!and numeric literals}
81 Numeric literals are not constructors and therefore
82 must not be used in patterns. For example, this declaration is
85 \isacommand{recdef}\ h\ "\isacharbraceleft \isacharbraceright "\isanewline
86 "h\ 3\ =\ 2"\isanewline
90 You should use a conditional expression instead:
92 "h\ i\ =\ (if\ i\ =\ 3\ then\ 2\ else\ i)"
94 \index{numeric literals|)}
99 \subsection{The Type of Natural Numbers, {\tt\slshape nat}}
101 \index{natural numbers|(}\index{*nat (type)|(}%
102 This type requires no introduction: we have been using it from the
103 beginning. Hundreds of theorems about the natural numbers are
104 proved in the theories \isa{Nat}, \isa{NatArith} and \isa{Divides}. Only
105 in exceptional circumstances should you resort to induction.
107 \subsubsection{Literals}
108 \index{numeric literals!for type \protect\isa{nat}}%
109 The notational options for the natural numbers are confusing. Recall that an
110 overloaded constant can be defined independently for each type; the definition
111 of \cdx{1} for type \isa{nat} is
113 1\ \isasymequiv\ Suc\ 0
114 \rulename{One_nat_def}
116 This is installed as a simplification rule, so the simplifier will replace
117 every occurrence of \isa{1::nat} by \isa{Suc\ 0}. Literals are obviously
118 better than nested \isa{Suc}s at expressing large values. But many theorems,
119 including the rewrite rules for primitive recursive functions, can only be
120 applied to terms of the form \isa{Suc\ $n$}.
122 The following default simplification rules replace
123 small literals by zero and successor:
125 2\ +\ n\ =\ Suc\ (Suc\ n)
126 \rulename{add_2_eq_Suc}\isanewline
127 n\ +\ 2\ =\ Suc\ (Suc\ n)
128 \rulename{add_2_eq_Suc'}
130 It is less easy to transform \isa{100} into \isa{Suc\ 99} (for example), and
131 the simplifier will normally reverse this transformation. Novices should
132 express natural numbers using \isa{0} and \isa{Suc} only.
134 \subsubsection{Typical lemmas}
135 Inequalities involving addition and subtraction alone can be proved
136 automatically. Lemmas such as these can be used to prove inequalities
137 involving multiplication and division:
139 \isasymlbrakk i\ \isasymle \ j;\ k\ \isasymle \ l\isasymrbrakk \ \isasymLongrightarrow \ i\ *\ k\ \isasymle \ j\ *\ l%
140 \rulename{mult_le_mono}\isanewline
141 \isasymlbrakk i\ <\ j;\ 0\ <\ k\isasymrbrakk \ \isasymLongrightarrow \ i\
143 \rulename{mult_less_mono1}\isanewline
144 m\ \isasymle \ n\ \isasymLongrightarrow \ m\ div\ k\ \isasymle \ n\ div\ k%
145 \rulename{div_le_mono}
148 Various distributive laws concerning multiplication are available:
150 (m\ +\ n)\ *\ k\ =\ m\ *\ k\ +\ n\ *\ k%
151 \rulenamedx{add_mult_distrib}\isanewline
152 (m\ -\ n)\ *\ k\ =\ m\ *\ k\ -\ n\ *\ k%
153 \rulenamedx{diff_mult_distrib}\isanewline
154 (m\ mod\ n)\ *\ k\ =\ (m\ *\ k)\ mod\ (n\ *\ k)
155 \rulenamedx{mod_mult_distrib}
158 \subsubsection{Division}
159 \index{division!for type \protect\isa{nat}}%
160 The infix operators \isa{div} and \isa{mod} are overloaded.
161 Isabelle/HOL provides the basic facts about quotient and remainder
162 on the natural numbers:
164 m\ mod\ n\ =\ (if\ m\ <\ n\ then\ m\ else\ (m\ -\ n)\ mod\ n)
165 \rulename{mod_if}\isanewline
166 m\ div\ n\ *\ n\ +\ m\ mod\ n\ =\ m%
167 \rulenamedx{mod_div_equality}
170 Many less obvious facts about quotient and remainder are also provided.
173 a\ *\ b\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c%
174 \rulename{div_mult1_eq}\isanewline
175 a\ *\ b\ mod\ c\ =\ a\ *\ (b\ mod\ c)\ mod\ c%
176 \rulename{mod_mult1_eq}\isanewline
177 a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%
178 \rulename{div_mult2_eq}\isanewline
179 a\ mod\ (b*c)\ =\ b * (a\ div\ b\ mod\ c)\ +\ a\ mod\ b%
180 \rulename{mod_mult2_eq}\isanewline
181 0\ <\ c\ \isasymLongrightarrow \ (c\ *\ a)\ div\ (c\ *\ b)\ =\ a\ div\ b%
182 \rulename{div_mult_mult1}
185 Surprisingly few of these results depend upon the
186 divisors' being nonzero.
187 \index{division!by zero}%
188 That is because division by
192 \rulename{DIVISION_BY_ZERO_DIV}\isanewline
194 \rulename{DIVISION_BY_ZERO_MOD}
196 As a concession to convention, these equations are not installed as default
197 simplification rules. In \isa{div_mult_mult1} above, one of
198 the two divisors (namely~\isa{c}) must still be nonzero.
200 The \textbf{divides} relation\index{divides relation}
201 has the standard definition, which
202 is overloaded over all numeric types:
204 m\ dvd\ n\ \isasymequiv\ {\isasymexists}k.\ n\ =\ m\ *\ k
208 Section~\ref{sec:proving-euclid} discusses proofs involving this
209 relation. Here are some of the facts proved about it:
211 \isasymlbrakk m\ dvd\ n;\ n\ dvd\ m\isasymrbrakk \ \isasymLongrightarrow \ m\ =\ n%
212 \rulenamedx{dvd_anti_sym}\isanewline
213 \isasymlbrakk k\ dvd\ m;\ k\ dvd\ n\isasymrbrakk \ \isasymLongrightarrow \ k\ dvd\ (m\ +\ n)
217 \subsubsection{Simplifier Tricks}
218 The rule \isa{diff_mult_distrib} shown above is one of the few facts
219 about \isa{m\ -\ n} that is not subject to
220 the condition \isa{n\ \isasymle \ m}. Natural number subtraction has few
221 nice properties; often you should remove it by simplifying with this split
224 P(a-b)\ =\ ((a<b\ \isasymlongrightarrow \ P\
225 0)\ \isasymand \ (\isasymforall d.\ a\ =\ b+d\ \isasymlongrightarrow \ P\
227 \rulename{nat_diff_split}
229 For example, splitting helps to prove the following fact:
231 \isacommand{lemma}\ "(n\ -\ 2)\ *\ (n\ +\ 2)\ =\ n\ *\ n\ -\ (4::nat)"\isanewline
232 \isacommand{apply}\ (simp\ split:\ nat_diff_split,\ clarify)\isanewline
233 \ 1.\ \isasymAnd d.\ \isasymlbrakk n\ <\ 2;\ n\ *\ n\ =\ 4\ +\ d\isasymrbrakk \ \isasymLongrightarrow \ d\ =\ 0
235 The result lies outside the scope of linear arithmetic, but
237 if we explicitly split \isa{n<2} as \isa{n=0} or \isa{n=1}:
239 \isacommand{apply}\ (subgoal_tac\ "n=0\ |\ n=1",\ force,\ arith)\isanewline
243 Suppose that two expressions are equal, differing only in
244 associativity and commutativity of addition. Simplifying with the
245 following equations sorts the terms and groups them to the right, making
246 the two expressions identical:
248 m\ +\ n\ +\ k\ =\ m\ +\ (n\ +\ k)
249 \rulenamedx{add_assoc}\isanewline
251 \rulenamedx{add_commute}\isanewline
252 x\ +\ (y\ +\ z)\ =\ y\ +\ (x\
254 \rulename{add_left_commute}
256 The name \isa{add_ac}\index{*add_ac (theorems)}
257 refers to the list of all three theorems; similarly
258 there is \isa{mult_ac}.\index{*mult_ac (theorems)}
259 Here is an example of the sorting effect. Start
262 \ 1.\ Suc\ (i\ +\ j\ *\ l\ *\ k\ +\ m\ *\ n)\ =\
263 f\ (n\ *\ m\ +\ i\ +\ k\ *\ j\ *\ l)
266 Simplify using \isa{add_ac} and \isa{mult_ac}:
268 \isacommand{apply}\ (simp\ add:\ add_ac\ mult_ac)
271 Here is the resulting subgoal:
273 \ 1.\ Suc\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))\
274 =\ f\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))%
276 \index{natural numbers|)}\index{*nat (type)|)}
280 \subsection{The Type of Integers, {\tt\slshape int}}
282 \index{integers|(}\index{*int (type)|(}%
283 Reasoning methods resemble those for the natural numbers, but induction and
284 the constant \isa{Suc} are not available. HOL provides many lemmas
285 for proving inequalities involving integer multiplication and division,
286 similar to those shown above for type~\isa{nat}.
288 The \rmindex{absolute value} function \cdx{abs} is overloaded for the numeric types.
289 It is defined for the integers; we have for example the obvious law
291 \isasymbar x\ *\ y\isasymbar \ =\ \isasymbar x\isasymbar \ *\ \isasymbar y\isasymbar
296 The absolute value bars shown above cannot be typed on a keyboard. They
297 can be entered using the X-symbol package. In \textsc{ascii}, type \isa{abs x} to
298 get \isa{\isasymbar x\isasymbar}.
301 The \isa{arith} method can prove facts about \isa{abs} automatically,
302 though as it does so by case analysis, the cost can be exponential.
304 \isacommand{lemma}\ "abs\ (x+y)\ \isasymle \ abs\ x\ +\ abs\ (y\ ::\ int)"\isanewline
305 \isacommand{by}\ arith
308 Concerning simplifier tricks, we have no need to eliminate subtraction: it
309 is well-behaved. As with the natural numbers, the simplifier can sort the
310 operands of sums and products. The name \isa{zadd_ac}\index{*zadd_ac (theorems)}
312 associativity and commutativity theorems for integer addition, while
313 \isa{zmult_ac}\index{*zmult_ac (theorems)}
314 has the analogous theorems for multiplication. The
315 prefix~\isa{z} in many theorem names recalls the use of $\mathbb{Z}$ to
316 denote the set of integers.
318 For division and remainder,\index{division!by negative numbers}
319 the treatment of negative divisors follows
320 mathematical practice: the sign of the remainder follows that
323 0\ <\ b\ \isasymLongrightarrow \ 0\ \isasymle \ a\ mod\ b%
324 \rulename{pos_mod_sign}\isanewline
325 0\ <\ b\ \isasymLongrightarrow \ a\ mod\ b\ <\ b%
326 \rulename{pos_mod_bound}\isanewline
327 b\ <\ 0\ \isasymLongrightarrow \ a\ mod\ b\ \isasymle \ 0
328 \rulename{neg_mod_sign}\isanewline
329 b\ <\ 0\ \isasymLongrightarrow \ b\ <\ a\ mod\ b%
330 \rulename{neg_mod_bound}
332 ML treats negative divisors in the same way, but most computer hardware
333 treats signed operands using the same rules as for multiplication.
334 Many facts about quotients and remainders are provided:
336 (a\ +\ b)\ div\ c\ =\isanewline
337 a\ div\ c\ +\ b\ div\ c\ +\ (a\ mod\ c\ +\ b\ mod\ c)\ div\ c%
338 \rulename{zdiv_zadd1_eq}
340 (a\ +\ b)\ mod\ c\ =\ (a\ mod\ c\ +\ b\ mod\ c)\ mod\ c%
341 \rulename{zmod_zadd1_eq}
345 (a\ *\ b)\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c%
346 \rulename{zdiv_zmult1_eq}\isanewline
347 (a\ *\ b)\ mod\ c\ =\ a\ *\ (b\ mod\ c)\ mod\ c%
348 \rulename{zmod_zmult1_eq}
352 0\ <\ c\ \isasymLongrightarrow \ a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%
353 \rulename{zdiv_zmult2_eq}\isanewline
354 0\ <\ c\ \isasymLongrightarrow \ a\ mod\ (b*c)\ =\ b*(a\ div\ b\ mod\
356 \rulename{zmod_zmult2_eq}
358 The last two differ from their natural number analogues by requiring
359 \isa{c} to be positive. Since division by zero yields zero, we could allow
360 \isa{c} to be zero. However, \isa{c} cannot be negative: a counterexample
362 $\isa{a} = 7$, $\isa{b} = 2$ and $\isa{c} = -3$, when the left-hand side of
363 \isa{zdiv_zmult2_eq} is $-2$ while the right-hand side is~$-1$.%
364 \index{integers|)}\index{*int (type)|)}
366 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 ($\ge$, $>$, $\le$ and $<$):
368 \isasymlbrakk k\ \isasymle \ i;\ P\ k;\ \isasymAnd i.\ \isasymlbrakk k\ \isasymle \ i;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i+1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%
369 \rulename{int_ge_induct}\isanewline
370 \isasymlbrakk k\ <\ i;\ P(k+1);\ \isasymAnd i.\ \isasymlbrakk k\ <\ i;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i+1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%
371 \rulename{int_gr_induct}\isanewline
372 \isasymlbrakk i\ \isasymle \ k;\ P\ k;\ \isasymAnd i.\ \isasymlbrakk i\ \isasymle \ k;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i-1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%
373 \rulename{int_le_induct}\isanewline
374 \isasymlbrakk i\ <\ k;\ P(k-1);\ \isasymAnd i.\ \isasymlbrakk i\ <\ k;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i-1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%
375 \rulename{int_less_induct}
379 \subsection{The Type of Real Numbers, {\tt\slshape real}}
381 \index{real numbers|(}\index{*real (type)|(}%
382 The real numbers enjoy two significant properties that the integers lack.
384 \textbf{dense}: between every two distinct real numbers there lies another.
385 This property follows from the division laws, since if $x<y$ then between
386 them lies $(x+y)/2$. The second property is that they are
387 \textbf{complete}: every set of reals that is bounded above has a least
388 upper bound. Completeness distinguishes the reals from the rationals, for
389 which the set $\{x\mid x^2<2\}$ has no least upper bound. (It could only be
390 $\surd2$, which is irrational.)
391 The formalization of completeness is complicated; rather than
392 reproducing it here, we refer you to the theory \texttt{RComplete} in
393 directory \texttt{Real}.
394 Density, however, is trivial to express:
396 x\ <\ y\ \isasymLongrightarrow \ \isasymexists r.\ x\ <\ r\ \isasymand \ r\ <\ y%
397 \rulename{real_dense}
400 Here is a selection of rules about the division operator. The following
401 are installed as default simplification rules in order to express
402 combinations of products and quotients as rational expressions:
404 x\ *\ (y\ /\ z)\ =\ x\ *\ y\ /\ z
405 \rulename{real_times_divide1_eq}\isanewline
406 y\ /\ z\ *\ x\ =\ y\ *\ x\ /\ z
407 \rulename{real_times_divide2_eq}\isanewline
408 x\ /\ (y\ /\ z)\ =\ x\ *\ z\ /\ y
409 \rulename{real_divide_divide1_eq}\isanewline
410 x\ /\ y\ /\ z\ =\ x\ /\ (y\ *\ z)
411 \rulename{real_divide_divide2_eq}
414 Signs are extracted from quotients in the hope that complementary terms can
417 -\ x\ /\ y\ =\ -\ (x\ /\ y)
418 \rulename{real_minus_divide_eq}\isanewline
419 x\ /\ -\ y\ =\ -\ (x\ /\ y)
420 \rulename{real_divide_minus_eq}
423 The following distributive law is available, but it is not installed as a
426 (x\ +\ y)\ /\ z\ =\ x\ /\ z\ +\ y\ /\ z%
427 \rulename{real_add_divide_distrib}
430 As with the other numeric types, the simplifier can sort the operands of
431 addition and multiplication. The name \isa{real_add_ac} refers to the
432 associativity and commutativity theorems for addition, while similarly
433 \isa{real_mult_ac} contains those properties for multiplication.
435 The absolute value function \isa{abs} is
436 defined for the reals, along with many theorems such as this one about
439 \isasymbar r\ \isacharcircum \ n\isasymbar\ =\
440 \isasymbar r\isasymbar \ \isacharcircum \ n
441 \rulename{realpow_abs}
444 Numeric literals\index{numeric literals!for type \protect\isa{real}}
445 for type \isa{real} have the same syntax as those for type
446 \isa{int} and only express integral values. Fractions expressed
447 using the division operator are automatically simplified to lowest terms:
449 \ 1.\ P\ ((3\ /\ 4)\ *\ (8\ /\ 15))\isanewline
450 \isacommand{apply} simp\isanewline
453 Exponentiation can express floating-point values such as
454 \isa{2 * 10\isacharcircum6}, but at present no special simplification
459 Type \isa{real} is only available in the logic HOL-Real, which
460 is HOL extended with a definitional development of the real
461 numbers. Base your theory upon theory
462 \thydx{Real}, not the usual \isa{Main}.%
463 \index{real numbers|)}\index{*real (type)|)}
464 Launch Isabelle using the command
470 Also distributed with Isabelle is HOL-Hyperreal,
471 whose theory \isa{Hyperreal} defines the type \tydx{hypreal} of
472 \rmindex{non-standard reals}. These
473 \textbf{hyperreals} include infinitesimals, which represent infinitely
474 small and infinitely large quantities; they facilitate proofs
475 about limits, differentiation and integration~\cite{fleuriot-jcm}. The
476 development defines an infinitely large number, \isa{omega} and an
477 infinitely small positive number, \isa{epsilon}. The
478 relation $x\approx y$ means ``$x$ is infinitely close to~$y$.''
479 Theory \isa{Hyperreal} also defines transcendental functions such as sine,
480 cosine, exponential and logarithm --- even the versions for type
481 \isa{real}, because they are defined using nonstandard limits.%