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-Complex also has the types
16 \isa{real} and \isa{complex}: the real and complex numbers. Isabelle has no
17 subtyping, so the numeric
18 types are distinct and there are functions to convert between them.
19 Fortunately most numeric operations are overloaded: the same symbol can be
20 used at all numeric types. Table~\ref{tab:overloading} in the appendix
21 shows the most important operations, together with the priorities of the
24 \index{linear arithmetic}%
25 Many theorems involving numeric types can be proved automatically by
26 Isabelle's arithmetic decision procedure, the method
27 \methdx{arith}. Linear arithmetic comprises addition, subtraction
28 and multiplication by constant factors; subterms involving other operators
29 are regarded as variables. The procedure can be slow, especially if the
30 subgoal to be proved involves subtraction over type \isa{nat}, which
31 causes case splits. On types \isa{nat} and \isa{int}, \methdx{arith}
32 can deal with quantifiers (this is known as ``Presburger Arithmetic''),
33 whereas on type \isa{real} it cannot.
35 The simplifier reduces arithmetic expressions in other
36 ways, such as dividing through by common factors. For problems that lie
37 outside the scope of automation, HOL provides hundreds of
38 theorems about multiplication, division, etc., that can be brought to
39 bear. You can locate them using Proof General's Find
40 button. A few lemmas are given below to show what
43 \subsection{Numeric Literals}
46 \index{numeric literals|(}%
47 The constants \cdx{0} and \cdx{1} are overloaded. They denote zero and one,
48 respectively, for all numeric types. Other values are expressed by numeric
49 literals, which consist of one or more decimal digits optionally preceeded by
50 a minus sign (\isa{-}). Examples are \isa{2}, \isa{-3} and
51 \isa{441223334678}. Literals are available for the types of natural numbers,
52 integers and reals; they denote integer values of arbitrary size.
54 Literals look like constants, but they abbreviate
55 terms representing the number in a two's complement binary notation.
56 Isabelle performs arithmetic on literals by rewriting rather
57 than using the hardware arithmetic. In most cases arithmetic
58 is fast enough, even for large numbers. The arithmetic operations
59 provided for literals include addition, subtraction, multiplication,
60 integer division and remainder. Fractions of literals (expressed using
61 division) are reduced to lowest terms.
63 \begin{warn}\index{overloading!and arithmetic}
64 The arithmetic operators are
65 overloaded, so you must be careful to ensure that each numeric
66 expression refers to a specific type, if necessary by inserting
67 type constraints. Here is an example of what can go wrong:
70 \isacommand{lemma}\ "2\ *\ m\ =\ m\ +\ m"
73 Carefully observe how Isabelle displays the subgoal:
75 \ 1.\ (2::'a)\ *\ m\ =\ m\ +\ m
77 The type \isa{'a} given for the literal \isa{2} warns us that no numeric
78 type has been specified. The problem is underspecified. Given a type
79 constraint such as \isa{nat}, \isa{int} or \isa{real}, it becomes trivial.
83 \index{recdef@\isacommand {recdef} (command)!and numeric literals}
84 Numeric literals are not constructors and therefore
85 must not be used in patterns. For example, this declaration is
88 \isacommand{recdef}\ h\ "\isacharbraceleft \isacharbraceright "\isanewline
89 "h\ 3\ =\ 2"\isanewline
93 You should use a conditional expression instead:
95 "h\ i\ =\ (if\ i\ =\ 3\ then\ 2\ else\ i)"
97 \index{numeric literals|)}
102 \subsection{The Type of Natural Numbers, {\tt\slshape nat}}
104 \index{natural numbers|(}\index{*nat (type)|(}%
105 This type requires no introduction: we have been using it from the
106 beginning. Hundreds of theorems about the natural numbers are
107 proved in the theories \isa{Nat}, \isa{NatArith} and \isa{Divides}. Only
108 in exceptional circumstances should you resort to induction.
110 \subsubsection{Literals}
111 \index{numeric literals!for type \protect\isa{nat}}%
112 The notational options for the natural numbers are confusing. Recall that an
113 overloaded constant can be defined independently for each type; the definition
114 of \cdx{1} for type \isa{nat} is
116 1\ \isasymequiv\ Suc\ 0
117 \rulename{One_nat_def}
119 This is installed as a simplification rule, so the simplifier will replace
120 every occurrence of \isa{1::nat} by \isa{Suc\ 0}. Literals are obviously
121 better than nested \isa{Suc}s at expressing large values. But many theorems,
122 including the rewrite rules for primitive recursive functions, can only be
123 applied to terms of the form \isa{Suc\ $n$}.
125 The following default simplification rules replace
126 small literals by zero and successor:
128 2\ +\ n\ =\ Suc\ (Suc\ n)
129 \rulename{add_2_eq_Suc}\isanewline
130 n\ +\ 2\ =\ Suc\ (Suc\ n)
131 \rulename{add_2_eq_Suc'}
133 It is less easy to transform \isa{100} into \isa{Suc\ 99} (for example), and
134 the simplifier will normally reverse this transformation. Novices should
135 express natural numbers using \isa{0} and \isa{Suc} only.
137 \subsubsection{Typical lemmas}
138 Inequalities involving addition and subtraction alone can be proved
139 automatically. Lemmas such as these can be used to prove inequalities
140 involving multiplication and division:
142 \isasymlbrakk i\ \isasymle \ j;\ k\ \isasymle \ l\isasymrbrakk \ \isasymLongrightarrow \ i\ *\ k\ \isasymle \ j\ *\ l%
143 \rulename{mult_le_mono}\isanewline
144 \isasymlbrakk i\ <\ j;\ 0\ <\ k\isasymrbrakk \ \isasymLongrightarrow \ i\
146 \rulename{mult_less_mono1}\isanewline
147 m\ \isasymle \ n\ \isasymLongrightarrow \ m\ div\ k\ \isasymle \ n\ div\ k%
148 \rulename{div_le_mono}
151 Various distributive laws concerning multiplication are available:
153 (m\ +\ n)\ *\ k\ =\ m\ *\ k\ +\ n\ *\ k%
154 \rulenamedx{add_mult_distrib}\isanewline
155 (m\ -\ n)\ *\ k\ =\ m\ *\ k\ -\ n\ *\ k%
156 \rulenamedx{diff_mult_distrib}\isanewline
157 (m\ mod\ n)\ *\ k\ =\ (m\ *\ k)\ mod\ (n\ *\ k)
158 \rulenamedx{mod_mult_distrib}
161 \subsubsection{Division}
162 \index{division!for type \protect\isa{nat}}%
163 The infix operators \isa{div} and \isa{mod} are overloaded.
164 Isabelle/HOL provides the basic facts about quotient and remainder
165 on the natural numbers:
167 m\ mod\ n\ =\ (if\ m\ <\ n\ then\ m\ else\ (m\ -\ n)\ mod\ n)
168 \rulename{mod_if}\isanewline
169 m\ div\ n\ *\ n\ +\ m\ mod\ n\ =\ m%
170 \rulenamedx{mod_div_equality}
173 Many less obvious facts about quotient and remainder are also provided.
176 a\ *\ b\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c%
177 \rulename{div_mult1_eq}\isanewline
178 a\ *\ b\ mod\ c\ =\ a\ *\ (b\ mod\ c)\ mod\ c%
179 \rulename{mod_mult1_eq}\isanewline
180 a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%
181 \rulename{div_mult2_eq}\isanewline
182 a\ mod\ (b*c)\ =\ b * (a\ div\ b\ mod\ c)\ +\ a\ mod\ b%
183 \rulename{mod_mult2_eq}\isanewline
184 0\ <\ c\ \isasymLongrightarrow \ (c\ *\ a)\ div\ (c\ *\ b)\ =\ a\ div\ b%
185 \rulename{div_mult_mult1}
188 Surprisingly few of these results depend upon the
189 divisors' being nonzero.
190 \index{division!by zero}%
191 That is because division by
195 \rulename{DIVISION_BY_ZERO_DIV}\isanewline
197 \rulename{DIVISION_BY_ZERO_MOD}
199 As a concession to convention, these equations are not installed as default
200 simplification rules. In \isa{div_mult_mult1} above, one of
201 the two divisors (namely~\isa{c}) must still be nonzero.
203 The \textbf{divides} relation\index{divides relation}
204 has the standard definition, which
205 is overloaded over all numeric types:
207 m\ dvd\ n\ \isasymequiv\ {\isasymexists}k.\ n\ =\ m\ *\ k
211 Section~\ref{sec:proving-euclid} discusses proofs involving this
212 relation. Here are some of the facts proved about it:
214 \isasymlbrakk m\ dvd\ n;\ n\ dvd\ m\isasymrbrakk \ \isasymLongrightarrow \ m\ =\ n%
215 \rulenamedx{dvd_anti_sym}\isanewline
216 \isasymlbrakk k\ dvd\ m;\ k\ dvd\ n\isasymrbrakk \ \isasymLongrightarrow \ k\ dvd\ (m\ +\ n)
220 \subsubsection{Simplifier Tricks}
221 The rule \isa{diff_mult_distrib} shown above is one of the few facts
222 about \isa{m\ -\ n} that is not subject to
223 the condition \isa{n\ \isasymle \ m}. Natural number subtraction has few
224 nice properties; often you should remove it by simplifying with this split
227 P(a-b)\ =\ ((a<b\ \isasymlongrightarrow \ P\
228 0)\ \isasymand \ (\isasymforall d.\ a\ =\ b+d\ \isasymlongrightarrow \ P\
230 \rulename{nat_diff_split}
232 For example, splitting helps to prove the following fact:
234 \isacommand{lemma}\ "(n\ -\ 2)\ *\ (n\ +\ 2)\ =\ n\ *\ n\ -\ (4::nat)"\isanewline
235 \isacommand{apply}\ (simp\ split:\ nat_diff_split,\ clarify)\isanewline
236 \ 1.\ \isasymAnd d.\ \isasymlbrakk n\ <\ 2;\ n\ *\ n\ =\ 4\ +\ d\isasymrbrakk \ \isasymLongrightarrow \ d\ =\ 0
238 The result lies outside the scope of linear arithmetic, but
240 if we explicitly split \isa{n<2} as \isa{n=0} or \isa{n=1}:
242 \isacommand{apply}\ (subgoal_tac\ "n=0\ |\ n=1",\ force,\ arith)\isanewline
246 Suppose that two expressions are equal, differing only in
247 associativity and commutativity of addition. Simplifying with the
248 following equations sorts the terms and groups them to the right, making
249 the two expressions identical:
251 m\ +\ n\ +\ k\ =\ m\ +\ (n\ +\ k)
252 \rulenamedx{add_assoc}\isanewline
254 \rulenamedx{add_commute}\isanewline
255 x\ +\ (y\ +\ z)\ =\ y\ +\ (x\
257 \rulename{add_left_commute}
259 The name \isa{add_ac}\index{*add_ac (theorems)}
260 refers to the list of all three theorems; similarly
261 there is \isa{mult_ac}.\index{*mult_ac (theorems)}
262 Here is an example of the sorting effect. Start
265 \ 1.\ Suc\ (i\ +\ j\ *\ l\ *\ k\ +\ m\ *\ n)\ =\
266 f\ (n\ *\ m\ +\ i\ +\ k\ *\ j\ *\ l)
269 Simplify using \isa{add_ac} and \isa{mult_ac}:
271 \isacommand{apply}\ (simp\ add:\ add_ac\ mult_ac)
274 Here is the resulting subgoal:
276 \ 1.\ Suc\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))\
277 =\ f\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))%
279 \index{natural numbers|)}\index{*nat (type)|)}
283 \subsection{The Type of Integers, {\tt\slshape int}}
285 \index{integers|(}\index{*int (type)|(}%
286 Reasoning methods resemble those for the natural numbers, but induction and
287 the constant \isa{Suc} are not available. HOL provides many lemmas
288 for proving inequalities involving integer multiplication and division,
289 similar to those shown above for type~\isa{nat}.
291 The \rmindex{absolute value} function \cdx{abs} is overloaded for the numeric types.
292 It is defined for the integers; we have for example the obvious law
294 \isasymbar x\ *\ y\isasymbar \ =\ \isasymbar x\isasymbar \ *\ \isasymbar y\isasymbar
299 The absolute value bars shown above cannot be typed on a keyboard. They
300 can be entered using the X-symbol package. In \textsc{ascii}, type \isa{abs x} to
301 get \isa{\isasymbar x\isasymbar}.
304 The \isa{arith} method can prove facts about \isa{abs} automatically,
305 though as it does so by case analysis, the cost can be exponential.
307 \isacommand{lemma}\ "abs\ (x+y)\ \isasymle \ abs\ x\ +\ abs\ (y\ ::\ int)"\isanewline
308 \isacommand{by}\ arith
311 Concerning simplifier tricks, we have no need to eliminate subtraction: it
312 is well-behaved. As with the natural numbers, the simplifier can sort the
313 operands of sums and products. The name \isa{zadd_ac}\index{*zadd_ac (theorems)}
315 associativity and commutativity theorems for integer addition, while
316 \isa{zmult_ac}\index{*zmult_ac (theorems)}
317 has the analogous theorems for multiplication. The
318 prefix~\isa{z} in many theorem names recalls the use of $\mathbb{Z}$ to
319 denote the set of integers.
321 For division and remainder,\index{division!by negative numbers}
322 the treatment of negative divisors follows
323 mathematical practice: the sign of the remainder follows that
326 0\ <\ b\ \isasymLongrightarrow \ 0\ \isasymle \ a\ mod\ b%
327 \rulename{pos_mod_sign}\isanewline
328 0\ <\ b\ \isasymLongrightarrow \ a\ mod\ b\ <\ b%
329 \rulename{pos_mod_bound}\isanewline
330 b\ <\ 0\ \isasymLongrightarrow \ a\ mod\ b\ \isasymle \ 0
331 \rulename{neg_mod_sign}\isanewline
332 b\ <\ 0\ \isasymLongrightarrow \ b\ <\ a\ mod\ b%
333 \rulename{neg_mod_bound}
335 ML treats negative divisors in the same way, but most computer hardware
336 treats signed operands using the same rules as for multiplication.
337 Many facts about quotients and remainders are provided:
339 (a\ +\ b)\ div\ c\ =\isanewline
340 a\ div\ c\ +\ b\ div\ c\ +\ (a\ mod\ c\ +\ b\ mod\ c)\ div\ c%
341 \rulename{zdiv_zadd1_eq}
343 (a\ +\ b)\ mod\ c\ =\ (a\ mod\ c\ +\ b\ mod\ c)\ mod\ c%
344 \rulename{zmod_zadd1_eq}
348 (a\ *\ b)\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c%
349 \rulename{zdiv_zmult1_eq}\isanewline
350 (a\ *\ b)\ mod\ c\ =\ a\ *\ (b\ mod\ c)\ mod\ c%
351 \rulename{zmod_zmult1_eq}
355 0\ <\ c\ \isasymLongrightarrow \ a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%
356 \rulename{zdiv_zmult2_eq}\isanewline
357 0\ <\ c\ \isasymLongrightarrow \ a\ mod\ (b*c)\ =\ b*(a\ div\ b\ mod\
359 \rulename{zmod_zmult2_eq}
361 The last two differ from their natural number analogues by requiring
362 \isa{c} to be positive. Since division by zero yields zero, we could allow
363 \isa{c} to be zero. However, \isa{c} cannot be negative: a counterexample
365 $\isa{a} = 7$, $\isa{b} = 2$ and $\isa{c} = -3$, when the left-hand side of
366 \isa{zdiv_zmult2_eq} is $-2$ while the right-hand side is~$-1$.%
367 \index{integers|)}\index{*int (type)|)}
369 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 $<$):
371 \isasymlbrakk k\ \isasymle \ i;\ P\ k;\ \isasymAnd i.\ \isasymlbrakk k\ \isasymle \ i;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i+1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%
372 \rulename{int_ge_induct}\isanewline
373 \isasymlbrakk k\ <\ i;\ P(k+1);\ \isasymAnd i.\ \isasymlbrakk k\ <\ i;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i+1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%
374 \rulename{int_gr_induct}\isanewline
375 \isasymlbrakk i\ \isasymle \ k;\ P\ k;\ \isasymAnd i.\ \isasymlbrakk i\ \isasymle \ k;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i-1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%
376 \rulename{int_le_induct}\isanewline
377 \isasymlbrakk i\ <\ k;\ P(k-1);\ \isasymAnd i.\ \isasymlbrakk i\ <\ k;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i-1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%
378 \rulename{int_less_induct}
382 \subsection{The Type of Real Numbers, {\tt\slshape real}}
384 \index{real numbers|(}\index{*real (type)|(}%
385 The real numbers enjoy two significant properties that the integers lack.
387 \textbf{dense}: between every two distinct real numbers there lies another.
388 This property follows from the division laws, since if $x<y$ then between
389 them lies $(x+y)/2$. The second property is that they are
390 \textbf{complete}: every set of reals that is bounded above has a least
391 upper bound. Completeness distinguishes the reals from the rationals, for
392 which the set $\{x\mid x^2<2\}$ has no least upper bound. (It could only be
393 $\surd2$, which is irrational.)
394 The formalization of completeness is complicated; rather than
395 reproducing it here, we refer you to the theory \texttt{RComplete} in
396 directory \texttt{Real}.
397 Density, however, is trivial to express:
399 x\ <\ y\ \isasymLongrightarrow \ \isasymexists r.\ x\ <\ r\ \isasymand \ r\ <\ y%
403 Here is a selection of rules about the division operator. The following
404 are installed as default simplification rules in order to express
405 combinations of products and quotients as rational expressions:
407 a\ *\ (b\ /\ c)\ =\ a\ *\ b\ /\ c
408 \rulename{times_divide_eq_right}\isanewline
409 b\ /\ c\ *\ a\ =\ b\ *\ a\ /\ c
410 \rulename{times_divide_eq_left}\isanewline
411 a\ /\ (b\ /\ c)\ =\ a\ *\ c\ /\ b
412 \rulename{divide_divide_eq_right}\isanewline
413 a\ /\ b\ /\ c\ =\ a\ /\ (b\ *\ c)
414 \rulename{divide_divide_eq_left}
417 Signs are extracted from quotients in the hope that complementary terms can
420 -\ (a\ /\ b)\ =\ -\ a\ /\ b
421 \rulename{minus_divide_left}\isanewline
422 -\ (a\ /\ b)\ =\ a\ /\ -\ b
423 \rulename{minus_divide_right}
426 The following distributive law is available, but it is not installed as a
429 (a\ +\ b)\ /\ c\ =\ a\ /\ c\ +\ b\ /\ c%
430 \rulename{add_divide_distrib}
433 As with the other numeric types, the simplifier can sort the operands of
434 addition and multiplication. The name \isa{real_add_ac} refers to the
435 associativity and commutativity theorems for addition, while similarly
436 \isa{real_mult_ac} contains those properties for multiplication.
438 The absolute value function \isa{abs} is
439 defined for the reals, along with many theorems such as this one about
442 \isasymbar a\ \isacharcircum \ n\isasymbar\ =\
443 \isasymbar a\isasymbar \ \isacharcircum \ n
447 Numeric literals\index{numeric literals!for type \protect\isa{real}}
448 for type \isa{real} have the same syntax as those for type
449 \isa{int} and only express integral values. Fractions expressed
450 using the division operator are automatically simplified to lowest terms:
452 \ 1.\ P\ ((3\ /\ 4)\ *\ (8\ /\ 15))\isanewline
453 \isacommand{apply} simp\isanewline
456 Exponentiation can express floating-point values such as
457 \isa{2 * 10\isacharcircum6}, but at present no special simplification
462 Type \isa{real} is only available in the logic HOL-Complex, which
463 is HOL extended with a definitional development of the real and complex
464 numbers. Base your theory upon theory
465 \thydx{Complex_Main}, not the usual \isa{Main}.%
466 \index{real numbers|)}\index{*real (type)|)}
467 Launch Isabelle using the command
469 Isabelle -l HOL-Complex
473 Also available in HOL-Complex is the
474 theory \isa{Hyperreal}, which define the type \tydx{hypreal} of
475 \rmindex{non-standard reals}. These
476 \textbf{hyperreals} include infinitesimals, which represent infinitely
477 small and infinitely large quantities; they facilitate proofs
478 about limits, differentiation and integration~\cite{fleuriot-jcm}. The
479 development defines an infinitely large number, \isa{omega} and an
480 infinitely small positive number, \isa{epsilon}. The
481 relation $x\approx y$ means ``$x$ is infinitely close to~$y$.''
482 Theory \isa{Hyperreal} also defines transcendental functions such as sine,
483 cosine, exponential and logarithm --- even the versions for type
484 \isa{real}, because they are defined using nonstandard limits.%