6 Until now, our numerical examples have used the type of \textbf{natural
8 \isa{nat}. This is a recursive datatype generated by the constructors
9 zero and successor, so it works well with inductive proofs and primitive
10 recursive function definitions. HOL also provides the type
11 \isa{int} of \textbf{integers}, which lack induction but support true
12 subtraction. The integers are preferable to the natural numbers for reasoning about
13 complicated arithmetic expressions, even for some expressions whose
14 value is non-negative. The logic HOL-Real also has the type
15 \isa{real} of real numbers. Isabelle has no subtyping, so the numeric
16 types are distinct and there are functions to convert between them.
17 Fortunately most numeric operations are overloaded: the same symbol can be
18 used at all numeric types. Table~\ref{tab:overloading} in the appendix
19 shows the most important operations, together with the priorities of the
22 \index{linear arithmetic}%
23 Many theorems involving numeric types can be proved automatically by
24 Isabelle's arithmetic decision procedure, the method
25 \methdx{arith}. Linear arithmetic comprises addition, subtraction
26 and multiplication by constant factors; subterms involving other operators
27 are regarded as variables. The procedure can be slow, especially if the
28 subgoal to be proved involves subtraction over type \isa{nat}, which
31 The simplifier reduces arithmetic expressions in other
32 ways, such as dividing through by common factors. For problems that lie
33 outside the scope of automation, HOL provides hundreds of
34 theorems about multiplication, division, etc., that can be brought to
35 bear. You can locate them using Proof General's Find
36 button. A few lemmas are given below to show what
39 \subsection{Numeric Literals}
42 \index{numeric literals|(}%
43 Literals are available for the types of natural numbers, integers
44 and reals and denote integer values of arbitrary size.
46 with a number sign (\isa{\#}), have an optional minus sign (\isa{-}) and
47 then one or more decimal digits. Examples are \isa{\#0}, \isa{\#-3}
48 and \isa{\#441223334678}.
50 Literals look like constants, but they abbreviate
51 terms, representing the number in a two's complement binary notation.
52 Isabelle performs arithmetic on literals by rewriting rather
53 than using the hardware arithmetic. In most cases arithmetic
54 is fast enough, even for large numbers. The arithmetic operations
55 provided for literals include addition, subtraction, multiplication,
56 integer division and remainder. Fractions of literals (expressed using
57 division) are reduced to lowest terms.
59 \begin{warn}\index{overloading!and arithmetic}
60 The arithmetic operators are
61 overloaded, so you must be careful to ensure that each numeric
62 expression refers to a specific type, if necessary by inserting
63 type constraints. Here is an example of what can go wrong:
66 \isacommand{lemma}\ "\#2\ *\ m\ =\ m\ +\ m"
69 Carefully observe how Isabelle displays the subgoal:
71 \ 1.\ (\#2::'a)\ *\ m\ =\ m\ +\ m
73 The type \isa{'a} given for the literal \isa{\#2} warns us that no numeric
74 type has been specified. The problem is underspecified. Given a type
75 constraint such as \isa{nat}, \isa{int} or \isa{real}, it becomes trivial.
79 \index{recdef@\isacommand {recdef} (command)!and numeric literals}
80 Numeric literals are not constructors and therefore
81 must not be used in patterns. For example, this declaration is
84 \isacommand{recdef}\ h\ "\isacharbraceleft \isacharbraceright "\isanewline
85 "h\ \#3\ =\ \#2"\isanewline
89 You should use a conditional expression instead:
91 "h\ i\ =\ (if\ i\ =\ \#3\ then\ \#2\ else\ i)"
93 \index{numeric literals|)}
98 \subsection{The Type of Natural Numbers, {\tt\slshape nat}}
100 \index{natural numbers|(}\index{*nat (type)|(}%
101 This type requires no introduction: we have been using it from the
102 beginning. Hundreds of theorems about the natural numbers are
103 proved in the theories \isa{Nat}, \isa{NatArith} and \isa{Divides}. Only
104 in exceptional circumstances should you resort to induction.
106 \subsubsection{Literals}
107 \index{numeric literals!for type \protect\isa{nat}}%
108 The notational options for the natural numbers are confusing. The
109 constant \cdx{0} is overloaded to serve as the neutral value
110 in a variety of additive types. The symbols \sdx{1} and \sdx{2} are
111 not constants but abbreviations for \isa{Suc 0} and \isa{Suc(Suc 0)},
112 respectively. The literals \isa{\#0}, \isa{\#1} and \isa{\#2} are
113 syntactically different from \isa{0}, \isa{1} and \isa{2}. You will
114 sometimes prefer one notation to the other. Literals are obviously
115 necessary to express large values, while \isa{0} and \isa{Suc} are needed
116 in order to match many theorems, including the rewrite rules for primitive
117 recursive functions. The following default simplification rules replace
118 small literals by zero and successor:
121 \rulename{numeral_0_eq_0}\isanewline
123 \rulename{numeral_1_eq_1}\isanewline
124 \#2\ +\ n\ =\ Suc\ (Suc\ n)
125 \rulename{add_2_eq_Suc}\isanewline
126 n\ +\ \#2\ =\ Suc\ (Suc\ n)
127 \rulename{add_2_eq_Suc'}
129 In special circumstances, you may wish to remove or reorient
132 \subsubsection{Typical lemmas}
133 Inequalities involving addition and subtraction alone can be proved
134 automatically. Lemmas such as these can be used to prove inequalities
135 involving multiplication and division:
137 \isasymlbrakk i\ \isasymle \ j;\ k\ \isasymle \ l\isasymrbrakk \ \isasymLongrightarrow \ i\ *\ k\ \isasymle \ j\ *\ l%
138 \rulename{mult_le_mono}\isanewline
139 \isasymlbrakk i\ <\ j;\ 0\ <\ k\isasymrbrakk \ \isasymLongrightarrow \ i\
141 \rulename{mult_less_mono1}\isanewline
142 m\ \isasymle \ n\ \isasymLongrightarrow \ m\ div\ k\ \isasymle \ n\ div\ k%
143 \rulename{div_le_mono}
146 Various distributive laws concerning multiplication are available:
148 (m\ +\ n)\ *\ k\ =\ m\ *\ k\ +\ n\ *\ k%
149 \rulenamedx{add_mult_distrib}\isanewline
150 (m\ -\ n)\ *\ k\ =\ m\ *\ k\ -\ n\ *\ k%
151 \rulenamedx{diff_mult_distrib}\isanewline
152 (m\ mod\ n)\ *\ k\ =\ (m\ *\ k)\ mod\ (n\ *\ k)
153 \rulenamedx{mod_mult_distrib}
156 \subsubsection{Division}
157 \index{division!for type \protect\isa{nat}}%
158 The infix operators \isa{div} and \isa{mod} are overloaded.
159 Isabelle/HOL provides the basic facts about quotient and remainder
160 on the natural numbers:
162 m\ mod\ n\ =\ (if\ m\ <\ n\ then\ m\ else\ (m\ -\ n)\ mod\ n)
163 \rulename{mod_if}\isanewline
164 m\ div\ n\ *\ n\ +\ m\ mod\ n\ =\ m%
165 \rulenamedx{mod_div_equality}
168 Many less obvious facts about quotient and remainder are also provided.
171 a\ *\ b\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c%
172 \rulename{div_mult1_eq}\isanewline
173 a\ *\ b\ mod\ c\ =\ a\ *\ (b\ mod\ c)\ mod\ c%
174 \rulename{mod_mult1_eq}\isanewline
175 a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%
176 \rulename{div_mult2_eq}\isanewline
177 a\ mod\ (b*c)\ =\ b * (a\ div\ b\ mod\ c)\ +\ a\ mod\ b%
178 \rulename{mod_mult2_eq}\isanewline
179 0\ <\ c\ \isasymLongrightarrow \ (c\ *\ a)\ div\ (c\ *\ b)\ =\ a\ div\ b%
180 \rulename{div_mult_mult1}
183 Surprisingly few of these results depend upon the
184 divisors' being nonzero.
185 \index{division!by zero}%
186 That is because division by
190 \rulename{DIVISION_BY_ZERO_DIV}\isanewline
192 \rulename{DIVISION_BY_ZERO_MOD}
194 As a concession to convention, these equations are not installed as default
195 simplification rules. In \isa{div_mult_mult1} above, one of
196 the two divisors (namely~\isa{c}) must still be nonzero.
198 The \textbf{divides} relation\index{divides relation}
199 has the standard definition, which
200 is overloaded over all numeric types:
202 m\ dvd\ n\ \isasymequiv\ {\isasymexists}k.\ n\ =\ m\ *\ k
206 Section~\ref{sec:proving-euclid} discusses proofs involving this
207 relation. Here are some of the facts proved about it:
209 \isasymlbrakk m\ dvd\ n;\ n\ dvd\ m\isasymrbrakk \ \isasymLongrightarrow \ m\ =\ n%
210 \rulenamedx{dvd_anti_sym}\isanewline
211 \isasymlbrakk k\ dvd\ m;\ k\ dvd\ n\isasymrbrakk \ \isasymLongrightarrow \ k\ dvd\ (m\ +\ n)
215 \subsubsection{Simplifier Tricks}
216 The rule \isa{diff_mult_distrib} shown above is one of the few facts
217 about \isa{m\ -\ n} that is not subject to
218 the condition \isa{n\ \isasymle \ m}. Natural number subtraction has few
219 nice properties; often you should remove it by simplifying with this split
222 P(a-b)\ =\ ((a<b\ \isasymlongrightarrow \ P\
223 0)\ \isasymand \ (\isasymforall d.\ a\ =\ b+d\ \isasymlongrightarrow \ P\
225 \rulename{nat_diff_split}
227 For example, it proves the following fact, which lies outside the scope of
230 \isacommand{lemma}\ "(n-1)*(n+1)\ =\ n*n\ -\ 1"\isanewline
231 \isacommand{apply}\ (simp\ split:\ nat_diff_split)\isanewline
235 Suppose that two expressions are equal, differing only in
236 associativity and commutativity of addition. Simplifying with the
237 following equations sorts the terms and groups them to the right, making
238 the two expressions identical:
240 m\ +\ n\ +\ k\ =\ m\ +\ (n\ +\ k)
241 \rulenamedx{add_assoc}\isanewline
243 \rulenamedx{add_commute}\isanewline
244 x\ +\ (y\ +\ z)\ =\ y\ +\ (x\
246 \rulename{add_left_commute}
248 The name \isa{add_ac} refers to the list of all three theorems, similarly
249 there is \isa{mult_ac}. Here is an example of the sorting effect. Start
252 \ 1.\ Suc\ (i\ +\ j\ *\ l\ *\ k\ +\ m\ *\ n)\ =\
253 f\ (n\ *\ m\ +\ i\ +\ k\ *\ j\ *\ l)
256 Simplify using \isa{add_ac} and \isa{mult_ac}:
258 \isacommand{apply}\ (simp\ add:\ add_ac\ mult_ac)
261 Here is the resulting subgoal:
263 \ 1.\ Suc\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))\
264 =\ f\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))%
266 \index{natural numbers|)}\index{*nat (type)|)}
270 \subsection{The Type of Integers, {\tt\slshape int}}
272 \index{integers|(}\index{*int (type)|(}%
273 Reasoning methods resemble those for the natural numbers, but induction and
274 the constant \isa{Suc} are not available. HOL provides many lemmas
275 for proving inequalities involving integer multiplication and division,
276 similar to those shown above for type~\isa{nat}.
278 The \rmindex{absolute value} function \cdx{abs} is overloaded for the numeric types.
279 It is defined for the integers; we have for example the obvious law
281 \isasymbar x\ *\ y\isasymbar \ =\ \isasymbar x\isasymbar \ *\ \isasymbar y\isasymbar
286 The absolute value bars shown above cannot be typed on a keyboard. They
287 can be entered using the X-symbol package. In \textsc{ascii}, type \isa{abs x} to
288 get \isa{\isasymbar x\isasymbar}.
291 The \isa{arith} method can prove facts about \isa{abs} automatically,
292 though as it does so by case analysis, the cost can be exponential.
294 \isacommand{lemma}\ "abs\ (x+y)\ \isasymle \ abs\ x\ +\ abs\ (y\ ::\ int)"\isanewline
295 \isacommand{by}\ arith
298 Concerning simplifier tricks, we have no need to eliminate subtraction: it
299 is well-behaved. As with the natural numbers, the simplifier can sort the
300 operands of sums and products. The name \isa{zadd_ac} refers to the
301 associativity and commutativity theorems for integer addition, while
302 \isa{zmult_ac} has the analogous theorems for multiplication. The
303 prefix~\isa{z} in many theorem names recalls the use of $\mathbb{Z}$ to
304 denote the set of integers.
306 For division and remainder,\index{division!by negative numbers}
307 the treatment of negative divisors follows
308 mathematical practice: the sign of the remainder follows that
311 \#0\ <\ b\ \isasymLongrightarrow \ \#0\ \isasymle \ a\ mod\ b%
312 \rulename{pos_mod_sign}\isanewline
313 \#0\ <\ b\ \isasymLongrightarrow \ a\ mod\ b\ <\ b%
314 \rulename{pos_mod_bound}\isanewline
315 b\ <\ \#0\ \isasymLongrightarrow \ a\ mod\ b\ \isasymle \ \#0
316 \rulename{neg_mod_sign}\isanewline
317 b\ <\ \#0\ \isasymLongrightarrow \ b\ <\ a\ mod\ b%
318 \rulename{neg_mod_bound}
320 ML treats negative divisors in the same way, but most computer hardware
321 treats signed operands using the same rules as for multiplication.
322 Many facts about quotients and remainders are provided:
324 (a\ +\ b)\ div\ c\ =\isanewline
325 a\ div\ c\ +\ b\ div\ c\ +\ (a\ mod\ c\ +\ b\ mod\ c)\ div\ c%
326 \rulename{zdiv_zadd1_eq}
328 (a\ +\ b)\ mod\ c\ =\ (a\ mod\ c\ +\ b\ mod\ c)\ mod\ c%
329 \rulename{zmod_zadd1_eq}
333 (a\ *\ b)\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c%
334 \rulename{zdiv_zmult1_eq}\isanewline
335 (a\ *\ b)\ mod\ c\ =\ a\ *\ (b\ mod\ c)\ mod\ c%
336 \rulename{zmod_zmult1_eq}
340 \#0\ <\ c\ \isasymLongrightarrow \ a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%
341 \rulename{zdiv_zmult2_eq}\isanewline
342 \#0\ <\ c\ \isasymLongrightarrow \ a\ mod\ (b*c)\ =\ b*(a\ div\ b\ mod\
344 \rulename{zmod_zmult2_eq}
346 The last two differ from their natural number analogues by requiring
347 \isa{c} to be positive. Since division by zero yields zero, we could allow
348 \isa{c} to be zero. However, \isa{c} cannot be negative: a counterexample
350 $\isa{a} = 7$, $\isa{b} = 2$ and $\isa{c} = -3$, when the left-hand side of
351 \isa{zdiv_zmult2_eq} is $-2$ while the right-hand side is~$-1$.%
352 \index{integers|)}\index{*int (type)|)}
355 \subsection{The Type of Real Numbers, {\tt\slshape real}}
357 \index{real numbers|(}\index{*real (type)|(}%
358 The real numbers enjoy two significant properties that the integers lack.
360 \textbf{dense}: between every two distinct real numbers there lies another.
361 This property follows from the division laws, since if $x<y$ then between
362 them lies $(x+y)/2$. The second property is that they are
363 \textbf{complete}: every set of reals that is bounded above has a least
364 upper bound. Completeness distinguishes the reals from the rationals, for
365 which the set $\{x\mid x^2<2\}$ has no least upper bound. (It could only be
366 $\surd2$, which is irrational.)
367 The formalization of completeness is complicated; rather than
368 reproducing it here, we refer you to the theory \texttt{RComplete} in
369 directory \texttt{Real}.
370 Density, however, is trivial to express:
372 x\ <\ y\ \isasymLongrightarrow \ \isasymexists r.\ x\ <\ r\ \isasymand \ r\ <\ y%
373 \rulename{real_dense}
376 Here is a selection of rules about the division operator. The following
377 are installed as default simplification rules in order to express
378 combinations of products and quotients as rational expressions:
380 x\ *\ (y\ /\ z)\ =\ x\ *\ y\ /\ z
381 \rulename{real_times_divide1_eq}\isanewline
382 y\ /\ z\ *\ x\ =\ y\ *\ x\ /\ z
383 \rulename{real_times_divide2_eq}\isanewline
384 x\ /\ (y\ /\ z)\ =\ x\ *\ z\ /\ y
385 \rulename{real_divide_divide1_eq}\isanewline
386 x\ /\ y\ /\ z\ =\ x\ /\ (y\ *\ z)
387 \rulename{real_divide_divide2_eq}
390 Signs are extracted from quotients in the hope that complementary terms can
393 -\ x\ /\ y\ =\ -\ (x\ /\ y)
394 \rulename{real_minus_divide_eq}\isanewline
395 x\ /\ -\ y\ =\ -\ (x\ /\ y)
396 \rulename{real_divide_minus_eq}
399 The following distributive law is available, but it is not installed as a
402 (x\ +\ y)\ /\ z\ =\ x\ /\ z\ +\ y\ /\ z%
403 \rulename{real_add_divide_distrib}
406 As with the other numeric types, the simplifier can sort the operands of
407 addition and multiplication. The name \isa{real_add_ac} refers to the
408 associativity and commutativity theorems for addition, while similarly
409 \isa{real_mult_ac} contains those properties for multiplication.
411 The absolute value function \isa{abs} is
412 defined for the reals, along with many theorems such as this one about
415 \isasymbar r\isasymbar \ \isacharcircum \ n\ =\ \isasymbar r\ \isacharcircum \ n\isasymbar
416 \rulename{realpow_abs}
419 Numeric literals\index{numeric literals!for type \protect\isa{real}}
420 for type \isa{real} have the same syntax as those for type
421 \isa{int} and only express integral values. Fractions expressed
422 using the division operator are automatically simplified to lowest terms:
424 \ 1.\ P\ ((\#3\ /\ \#4)\ *\ (\#8\ /\ \#15))\isanewline
425 \isacommand{apply} simp\isanewline
426 \ 1.\ P\ (\#2\ /\ \#5)
428 Exponentiation can express floating-point values such as
429 \isa{\#2 * \#10\isacharcircum\#6}, but at present no special simplification
434 Type \isa{real} is only available in the logic HOL-Real, which
435 is HOL extended with the rather substantial development of the real
436 numbers. Base your theory upon theory
437 \thydx{Real}, not the usual \isa{Main}.%
438 \index{real numbers|)}\index{*real (type)|)}
439 Launch Isabelle using the command
445 Also distributed with Isabelle is HOL-Hyperreal,
446 whose theory \isa{Hyperreal} defines the type \tydx{hypreal} of
447 \rmindex{non-standard reals}. These
448 \textbf{hyperreals} include infinitesimals, which represent infinitely
449 small and infinitely large quantities; they facilitate proofs
450 about limits, differentiation and integration~\cite{fleuriot-jcm}. The
451 development defines an infinitely large number, \isa{omega} and an
452 infinitely small positive number, \isa{epsilon}. The
453 relation $x\approx y$ means ``$x$ is infinitely close to~$y$''.