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 Literals are available for the types of natural numbers, integers
45 and reals and denote integer values of arbitrary size.
47 with a number sign (\isa{\#}), have an optional minus sign (\isa{-}) and
48 then one or more decimal digits. Examples are \isa{\#0}, \isa{\#-3}
49 and \isa{\#441223334678}.\REMARK{will need updating?}
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. The
110 constant \cdx{0} is overloaded to serve as the neutral value
111 in a variety of additive types. The symbols \sdx{1} and \sdx{2} are
112 not constants but abbreviations for \isa{Suc 0} and \isa{Suc(Suc 0)},
113 respectively. The literals \isa{\#0}, \isa{\#1} and \isa{\#2} are
114 syntactically different from \isa{0}, \isa{1} and \isa{2}. You will\REMARK{will need updating?}
115 sometimes prefer one notation to the other. Literals are obviously
116 necessary to express large values, while \isa{0} and \isa{Suc} are needed
117 in order to match many theorems, including the rewrite rules for primitive
118 recursive functions. The following default simplification rules replace
119 small literals by zero and successor:
122 \rulename{numeral_0_eq_0}\isanewline
124 \rulename{numeral_1_eq_1}\isanewline
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 In special circumstances, you may wish to remove or reorient
133 \subsubsection{Typical lemmas}
134 Inequalities involving addition and subtraction alone can be proved
135 automatically. Lemmas such as these can be used to prove inequalities
136 involving multiplication and division:
138 \isasymlbrakk i\ \isasymle \ j;\ k\ \isasymle \ l\isasymrbrakk \ \isasymLongrightarrow \ i\ *\ k\ \isasymle \ j\ *\ l%
139 \rulename{mult_le_mono}\isanewline
140 \isasymlbrakk i\ <\ j;\ 0\ <\ k\isasymrbrakk \ \isasymLongrightarrow \ i\
142 \rulename{mult_less_mono1}\isanewline
143 m\ \isasymle \ n\ \isasymLongrightarrow \ m\ div\ k\ \isasymle \ n\ div\ k%
144 \rulename{div_le_mono}
147 Various distributive laws concerning multiplication are available:
149 (m\ +\ n)\ *\ k\ =\ m\ *\ k\ +\ n\ *\ k%
150 \rulenamedx{add_mult_distrib}\isanewline
151 (m\ -\ n)\ *\ k\ =\ m\ *\ k\ -\ n\ *\ k%
152 \rulenamedx{diff_mult_distrib}\isanewline
153 (m\ mod\ n)\ *\ k\ =\ (m\ *\ k)\ mod\ (n\ *\ k)
154 \rulenamedx{mod_mult_distrib}
157 \subsubsection{Division}
158 \index{division!for type \protect\isa{nat}}%
159 The infix operators \isa{div} and \isa{mod} are overloaded.
160 Isabelle/HOL provides the basic facts about quotient and remainder
161 on the natural numbers:
163 m\ mod\ n\ =\ (if\ m\ <\ n\ then\ m\ else\ (m\ -\ n)\ mod\ n)
164 \rulename{mod_if}\isanewline
165 m\ div\ n\ *\ n\ +\ m\ mod\ n\ =\ m%
166 \rulenamedx{mod_div_equality}
169 Many less obvious facts about quotient and remainder are also provided.
172 a\ *\ b\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c%
173 \rulename{div_mult1_eq}\isanewline
174 a\ *\ b\ mod\ c\ =\ a\ *\ (b\ mod\ c)\ mod\ c%
175 \rulename{mod_mult1_eq}\isanewline
176 a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%
177 \rulename{div_mult2_eq}\isanewline
178 a\ mod\ (b*c)\ =\ b * (a\ div\ b\ mod\ c)\ +\ a\ mod\ b%
179 \rulename{mod_mult2_eq}\isanewline
180 0\ <\ c\ \isasymLongrightarrow \ (c\ *\ a)\ div\ (c\ *\ b)\ =\ a\ div\ b%
181 \rulename{div_mult_mult1}
184 Surprisingly few of these results depend upon the
185 divisors' being nonzero.
186 \index{division!by zero}%
187 That is because division by
191 \rulename{DIVISION_BY_ZERO_DIV}\isanewline
193 \rulename{DIVISION_BY_ZERO_MOD}
195 As a concession to convention, these equations are not installed as default
196 simplification rules. In \isa{div_mult_mult1} above, one of
197 the two divisors (namely~\isa{c}) must still be nonzero.
199 The \textbf{divides} relation\index{divides relation}
200 has the standard definition, which
201 is overloaded over all numeric types:
203 m\ dvd\ n\ \isasymequiv\ {\isasymexists}k.\ n\ =\ m\ *\ k
207 Section~\ref{sec:proving-euclid} discusses proofs involving this
208 relation. Here are some of the facts proved about it:
210 \isasymlbrakk m\ dvd\ n;\ n\ dvd\ m\isasymrbrakk \ \isasymLongrightarrow \ m\ =\ n%
211 \rulenamedx{dvd_anti_sym}\isanewline
212 \isasymlbrakk k\ dvd\ m;\ k\ dvd\ n\isasymrbrakk \ \isasymLongrightarrow \ k\ dvd\ (m\ +\ n)
216 \subsubsection{Simplifier Tricks}
217 The rule \isa{diff_mult_distrib} shown above is one of the few facts
218 about \isa{m\ -\ n} that is not subject to
219 the condition \isa{n\ \isasymle \ m}. Natural number subtraction has few
220 nice properties; often you should remove it by simplifying with this split
223 P(a-b)\ =\ ((a<b\ \isasymlongrightarrow \ P\
224 0)\ \isasymand \ (\isasymforall d.\ a\ =\ b+d\ \isasymlongrightarrow \ P\
226 \rulename{nat_diff_split}
228 For example, this splitting proves the following fact, which lies outside the scope of
229 linear arithmetic:\REMARK{replace by new example!}
231 \isacommand{lemma}\ "(n-1)*(n+1)\ =\ n*n\ -\ 1"\isanewline
232 \isacommand{apply}\ (simp\ split:\ nat_diff_split)\isanewline
236 Suppose that two expressions are equal, differing only in
237 associativity and commutativity of addition. Simplifying with the
238 following equations sorts the terms and groups them to the right, making
239 the two expressions identical:
241 m\ +\ n\ +\ k\ =\ m\ +\ (n\ +\ k)
242 \rulenamedx{add_assoc}\isanewline
244 \rulenamedx{add_commute}\isanewline
245 x\ +\ (y\ +\ z)\ =\ y\ +\ (x\
247 \rulename{add_left_commute}
249 The name \isa{add_ac}\index{*add_ac (theorems)}
250 refers to the list of all three theorems; similarly
251 there is \isa{mult_ac}.\index{*mult_ac (theorems)}
252 Here is an example of the sorting effect. Start
255 \ 1.\ Suc\ (i\ +\ j\ *\ l\ *\ k\ +\ m\ *\ n)\ =\
256 f\ (n\ *\ m\ +\ i\ +\ k\ *\ j\ *\ l)
259 Simplify using \isa{add_ac} and \isa{mult_ac}:
261 \isacommand{apply}\ (simp\ add:\ add_ac\ mult_ac)
264 Here is the resulting subgoal:
266 \ 1.\ Suc\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))\
267 =\ f\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))%
269 \index{natural numbers|)}\index{*nat (type)|)}
273 \subsection{The Type of Integers, {\tt\slshape int}}
275 \index{integers|(}\index{*int (type)|(}%
276 Reasoning methods resemble those for the natural numbers, but induction and
277 the constant \isa{Suc} are not available. HOL provides many lemmas
278 for proving inequalities involving integer multiplication and division,
279 similar to those shown above for type~\isa{nat}.
281 The \rmindex{absolute value} function \cdx{abs} is overloaded for the numeric types.
282 It is defined for the integers; we have for example the obvious law
284 \isasymbar x\ *\ y\isasymbar \ =\ \isasymbar x\isasymbar \ *\ \isasymbar y\isasymbar
289 The absolute value bars shown above cannot be typed on a keyboard. They
290 can be entered using the X-symbol package. In \textsc{ascii}, type \isa{abs x} to
291 get \isa{\isasymbar x\isasymbar}.
294 The \isa{arith} method can prove facts about \isa{abs} automatically,
295 though as it does so by case analysis, the cost can be exponential.
297 \isacommand{lemma}\ "abs\ (x+y)\ \isasymle \ abs\ x\ +\ abs\ (y\ ::\ int)"\isanewline
298 \isacommand{by}\ arith
301 Concerning simplifier tricks, we have no need to eliminate subtraction: it
302 is well-behaved. As with the natural numbers, the simplifier can sort the
303 operands of sums and products. The name \isa{zadd_ac}\index{*zadd_ac (theorems)}
305 associativity and commutativity theorems for integer addition, while
306 \isa{zmult_ac}\index{*zmult_ac (theorems)}
307 has the analogous theorems for multiplication. The
308 prefix~\isa{z} in many theorem names recalls the use of $\mathbb{Z}$ to
309 denote the set of integers.
311 For division and remainder,\index{division!by negative numbers}
312 the treatment of negative divisors follows
313 mathematical practice: the sign of the remainder follows that
316 \#0\ <\ b\ \isasymLongrightarrow \ \#0\ \isasymle \ a\ mod\ b%
317 \rulename{pos_mod_sign}\isanewline
318 \#0\ <\ b\ \isasymLongrightarrow \ a\ mod\ b\ <\ b%
319 \rulename{pos_mod_bound}\isanewline
320 b\ <\ \#0\ \isasymLongrightarrow \ a\ mod\ b\ \isasymle \ \#0
321 \rulename{neg_mod_sign}\isanewline
322 b\ <\ \#0\ \isasymLongrightarrow \ b\ <\ a\ mod\ b%
323 \rulename{neg_mod_bound}
325 ML treats negative divisors in the same way, but most computer hardware
326 treats signed operands using the same rules as for multiplication.
327 Many facts about quotients and remainders are provided:
329 (a\ +\ b)\ div\ c\ =\isanewline
330 a\ div\ c\ +\ b\ div\ c\ +\ (a\ mod\ c\ +\ b\ mod\ c)\ div\ c%
331 \rulename{zdiv_zadd1_eq}
333 (a\ +\ b)\ mod\ c\ =\ (a\ mod\ c\ +\ b\ mod\ c)\ mod\ c%
334 \rulename{zmod_zadd1_eq}
338 (a\ *\ b)\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c%
339 \rulename{zdiv_zmult1_eq}\isanewline
340 (a\ *\ b)\ mod\ c\ =\ a\ *\ (b\ mod\ c)\ mod\ c%
341 \rulename{zmod_zmult1_eq}
345 \#0\ <\ c\ \isasymLongrightarrow \ a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%
346 \rulename{zdiv_zmult2_eq}\isanewline
347 \#0\ <\ c\ \isasymLongrightarrow \ a\ mod\ (b*c)\ =\ b*(a\ div\ b\ mod\
349 \rulename{zmod_zmult2_eq}
351 The last two differ from their natural number analogues by requiring
352 \isa{c} to be positive. Since division by zero yields zero, we could allow
353 \isa{c} to be zero. However, \isa{c} cannot be negative: a counterexample
355 $\isa{a} = 7$, $\isa{b} = 2$ and $\isa{c} = -3$, when the left-hand side of
356 \isa{zdiv_zmult2_eq} is $-2$ while the right-hand side is~$-1$.%
357 \index{integers|)}\index{*int (type)|)}
360 \subsection{The Type of Real Numbers, {\tt\slshape real}}
362 \index{real numbers|(}\index{*real (type)|(}%
363 The real numbers enjoy two significant properties that the integers lack.
365 \textbf{dense}: between every two distinct real numbers there lies another.
366 This property follows from the division laws, since if $x<y$ then between
367 them lies $(x+y)/2$. The second property is that they are
368 \textbf{complete}: every set of reals that is bounded above has a least
369 upper bound. Completeness distinguishes the reals from the rationals, for
370 which the set $\{x\mid x^2<2\}$ has no least upper bound. (It could only be
371 $\surd2$, which is irrational.)
372 The formalization of completeness is complicated; rather than
373 reproducing it here, we refer you to the theory \texttt{RComplete} in
374 directory \texttt{Real}.
375 Density, however, is trivial to express:
377 x\ <\ y\ \isasymLongrightarrow \ \isasymexists r.\ x\ <\ r\ \isasymand \ r\ <\ y%
378 \rulename{real_dense}
381 Here is a selection of rules about the division operator. The following
382 are installed as default simplification rules in order to express
383 combinations of products and quotients as rational expressions:
385 x\ *\ (y\ /\ z)\ =\ x\ *\ y\ /\ z
386 \rulename{real_times_divide1_eq}\isanewline
387 y\ /\ z\ *\ x\ =\ y\ *\ x\ /\ z
388 \rulename{real_times_divide2_eq}\isanewline
389 x\ /\ (y\ /\ z)\ =\ x\ *\ z\ /\ y
390 \rulename{real_divide_divide1_eq}\isanewline
391 x\ /\ y\ /\ z\ =\ x\ /\ (y\ *\ z)
392 \rulename{real_divide_divide2_eq}
395 Signs are extracted from quotients in the hope that complementary terms can
398 -\ x\ /\ y\ =\ -\ (x\ /\ y)
399 \rulename{real_minus_divide_eq}\isanewline
400 x\ /\ -\ y\ =\ -\ (x\ /\ y)
401 \rulename{real_divide_minus_eq}
404 The following distributive law is available, but it is not installed as a
407 (x\ +\ y)\ /\ z\ =\ x\ /\ z\ +\ y\ /\ z%
408 \rulename{real_add_divide_distrib}
411 As with the other numeric types, the simplifier can sort the operands of
412 addition and multiplication. The name \isa{real_add_ac} refers to the
413 associativity and commutativity theorems for addition, while similarly
414 \isa{real_mult_ac} contains those properties for multiplication.
416 The absolute value function \isa{abs} is
417 defined for the reals, along with many theorems such as this one about
420 \isasymbar r\isasymbar \ \isacharcircum \ n\ =\ \isasymbar r\ \isacharcircum \ n\isasymbar
421 \rulename{realpow_abs}
424 Numeric literals\index{numeric literals!for type \protect\isa{real}}
425 for type \isa{real} have the same syntax as those for type
426 \isa{int} and only express integral values. Fractions expressed
427 using the division operator are automatically simplified to lowest terms:
429 \ 1.\ P\ ((\#3\ /\ \#4)\ *\ (\#8\ /\ \#15))\isanewline
430 \isacommand{apply} simp\isanewline
431 \ 1.\ P\ (\#2\ /\ \#5)
433 Exponentiation can express floating-point values such as
434 \isa{\#2 * \#10\isacharcircum\#6}, but at present no special simplification
439 Type \isa{real} is only available in the logic HOL-Real, which
440 is HOL extended with the rather substantial development of the real
441 numbers. Base your theory upon theory
442 \thydx{Real}, not the usual \isa{Main}.%
443 \index{real numbers|)}\index{*real (type)|)}
444 Launch Isabelle using the command
450 Also distributed with Isabelle is HOL-Hyperreal,
451 whose theory \isa{Hyperreal} defines the type \tydx{hypreal} of
452 \rmindex{non-standard reals}. These
453 \textbf{hyperreals} include infinitesimals, which represent infinitely
454 small and infinitely large quantities; they facilitate proofs
455 about limits, differentiation and integration~\cite{fleuriot-jcm}. The
456 development defines an infinitely large number, \isa{omega} and an
457 infinitely small positive number, \isa{epsilon}. The
458 relation $x\approx y$ means ``$x$ is infinitely close to~$y$''.%