10794
|
1 |
% $Id$
|
11389
|
2 |
|
|
3 |
\section{Numbers}
|
|
4 |
\label{sec:numbers}
|
|
5 |
|
11174
|
6 |
Until now, our numerical examples have used the type of \textbf{natural
|
|
7 |
numbers},
|
10594
|
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
|
11174
|
10 |
recursive function definitions. HOL also provides the type
|
10794
|
11 |
\isa{int} of \textbf{integers}, which lack induction but support true
|
11174
|
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
|
|
20 |
infix symbols.
|
10594
|
21 |
|
11416
|
22 |
\index{linear arithmetic}%
|
10594
|
23 |
Many theorems involving numeric types can be proved automatically by
|
|
24 |
Isabelle's arithmetic decision procedure, the method
|
11416
|
25 |
\methdx{arith}. Linear arithmetic comprises addition, subtraction
|
10594
|
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
|
|
29 |
causes case splits.
|
|
30 |
|
|
31 |
The simplifier reduces arithmetic expressions in other
|
|
32 |
ways, such as dividing through by common factors. For problems that lie
|
10881
|
33 |
outside the scope of automation, HOL provides hundreds of
|
10594
|
34 |
theorems about multiplication, division, etc., that can be brought to
|
10881
|
35 |
bear. You can locate them using Proof General's Find
|
|
36 |
button. A few lemmas are given below to show what
|
10794
|
37 |
is available.
|
10594
|
38 |
|
|
39 |
\subsection{Numeric Literals}
|
10779
|
40 |
\label{sec:numerals}
|
10594
|
41 |
|
11416
|
42 |
\index{numeric literals|(}%
|
10594
|
43 |
Literals are available for the types of natural numbers, integers
|
|
44 |
and reals and denote integer values of arbitrary size.
|
|
45 |
They begin
|
|
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}.
|
|
49 |
|
|
50 |
Literals look like constants, but they abbreviate
|
|
51 |
terms, representing the number in a two's complement binary notation.
|
10794
|
52 |
Isabelle performs arithmetic on literals by rewriting rather
|
10594
|
53 |
than using the hardware arithmetic. In most cases arithmetic
|
|
54 |
is fast enough, even for large numbers. The arithmetic operations
|
10794
|
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.
|
10594
|
58 |
|
11416
|
59 |
\begin{warn}\index{overloading!and arithmetic}
|
10794
|
60 |
The arithmetic operators are
|
10594
|
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:
|
10794
|
64 |
\par
|
10594
|
65 |
\begin{isabelle}
|
|
66 |
\isacommand{lemma}\ "\#2\ *\ m\ =\ m\ +\ m"
|
|
67 |
\end{isabelle}
|
|
68 |
%
|
|
69 |
Carefully observe how Isabelle displays the subgoal:
|
|
70 |
\begin{isabelle}
|
|
71 |
\ 1.\ (\#2::'a)\ *\ m\ =\ m\ +\ m
|
|
72 |
\end{isabelle}
|
|
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.
|
10794
|
76 |
\end{warn}
|
|
77 |
|
10881
|
78 |
\begin{warn}
|
11416
|
79 |
\index{recdef@\protect\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
|
|
82 |
rejected:
|
10881
|
83 |
\begin{isabelle}
|
|
84 |
\isacommand{recdef}\ h\ "\isacharbraceleft \isacharbraceright "\isanewline
|
11148
|
85 |
"h\ \#3\ =\ \#2"\isanewline
|
|
86 |
"h\ i\ \ =\ i"
|
10881
|
87 |
\end{isabelle}
|
|
88 |
|
|
89 |
You should use a conditional expression instead:
|
|
90 |
\begin{isabelle}
|
|
91 |
"h\ i\ =\ (if\ i\ =\ \#3\ then\ \#2\ else\ i)"
|
|
92 |
\end{isabelle}
|
11416
|
93 |
\index{numeric literals|)}
|
10881
|
94 |
\end{warn}
|
|
95 |
|
10594
|
96 |
|
|
97 |
|
11216
|
98 |
\subsection{The Type of Natural Numbers, {\tt\slshape nat}}
|
10594
|
99 |
|
11416
|
100 |
\index{natural numbers|(}\index{*nat (type)|(}%
|
10594
|
101 |
This type requires no introduction: we have been using it from the
|
10794
|
102 |
beginning. Hundreds of theorems about the natural numbers are
|
10594
|
103 |
proved in the theories \isa{Nat}, \isa{NatArith} and \isa{Divides}. Only
|
|
104 |
in exceptional circumstances should you resort to induction.
|
|
105 |
|
|
106 |
\subsubsection{Literals}
|
11416
|
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
|
10594
|
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
|
10794
|
113 |
syntactically different from \isa{0}, \isa{1} and \isa{2}. You will
|
10594
|
114 |
sometimes prefer one notation to the other. Literals are obviously
|
10794
|
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:
|
10594
|
119 |
\begin{isabelle}
|
|
120 |
\#0\ =\ 0
|
|
121 |
\rulename{numeral_0_eq_0}\isanewline
|
|
122 |
\#1\ =\ 1
|
|
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'}
|
|
128 |
\end{isabelle}
|
|
129 |
In special circumstances, you may wish to remove or reorient
|
|
130 |
these rules.
|
|
131 |
|
|
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:
|
|
136 |
\begin{isabelle}
|
|
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\
|
|
140 |
*\ k\ <\ j\ *\ k%
|
|
141 |
\rulename{mult_less_mono1}\isanewline
|
|
142 |
m\ \isasymle \ n\ \isasymLongrightarrow \ m\ div\ k\ \isasymle \ n\ div\ k%
|
|
143 |
\rulename{div_le_mono}
|
|
144 |
\end{isabelle}
|
|
145 |
%
|
|
146 |
Various distributive laws concerning multiplication are available:
|
|
147 |
\begin{isabelle}
|
|
148 |
(m\ +\ n)\ *\ k\ =\ m\ *\ k\ +\ n\ *\ k%
|
11416
|
149 |
\rulenamedx{add_mult_distrib}\isanewline
|
10594
|
150 |
(m\ -\ n)\ *\ k\ =\ m\ *\ k\ -\ n\ *\ k%
|
11416
|
151 |
\rulenamedx{diff_mult_distrib}\isanewline
|
10594
|
152 |
(m\ mod\ n)\ *\ k\ =\ (m\ *\ k)\ mod\ (n\ *\ k)
|
11416
|
153 |
\rulenamedx{mod_mult_distrib}
|
10594
|
154 |
\end{isabelle}
|
|
155 |
|
|
156 |
\subsubsection{Division}
|
11416
|
157 |
\index{division!for type \protect\isa{nat}}%
|
10881
|
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:
|
10594
|
161 |
\begin{isabelle}
|
|
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%
|
11416
|
165 |
\rulenamedx{mod_div_equality}
|
10594
|
166 |
\end{isabelle}
|
|
167 |
|
|
168 |
Many less obvious facts about quotient and remainder are also provided.
|
|
169 |
Here is a selection:
|
|
170 |
\begin{isabelle}
|
|
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}
|
|
181 |
\end{isabelle}
|
|
182 |
|
|
183 |
Surprisingly few of these results depend upon the
|
11416
|
184 |
divisors' being nonzero.
|
|
185 |
\index{division!by zero}%
|
|
186 |
That is because division by
|
10794
|
187 |
zero yields zero:
|
10594
|
188 |
\begin{isabelle}
|
|
189 |
a\ div\ 0\ =\ 0
|
|
190 |
\rulename{DIVISION_BY_ZERO_DIV}\isanewline
|
|
191 |
a\ mod\ 0\ =\ a%
|
|
192 |
\rulename{DIVISION_BY_ZERO_MOD}
|
|
193 |
\end{isabelle}
|
|
194 |
As a concession to convention, these equations are not installed as default
|
11174
|
195 |
simplification rules. In \isa{div_mult_mult1} above, one of
|
11161
|
196 |
the two divisors (namely~\isa{c}) must still be nonzero.
|
10594
|
197 |
|
11416
|
198 |
The \textbf{divides} relation\index{divides relation}
|
|
199 |
has the standard definition, which
|
10594
|
200 |
is overloaded over all numeric types:
|
|
201 |
\begin{isabelle}
|
|
202 |
m\ dvd\ n\ \isasymequiv\ {\isasymexists}k.\ n\ =\ m\ *\ k
|
11416
|
203 |
\rulenamedx{dvd_def}
|
10594
|
204 |
\end{isabelle}
|
|
205 |
%
|
|
206 |
Section~\ref{sec:proving-euclid} discusses proofs involving this
|
|
207 |
relation. Here are some of the facts proved about it:
|
|
208 |
\begin{isabelle}
|
|
209 |
\isasymlbrakk m\ dvd\ n;\ n\ dvd\ m\isasymrbrakk \ \isasymLongrightarrow \ m\ =\ n%
|
11416
|
210 |
\rulenamedx{dvd_anti_sym}\isanewline
|
10594
|
211 |
\isasymlbrakk k\ dvd\ m;\ k\ dvd\ n\isasymrbrakk \ \isasymLongrightarrow \ k\ dvd\ (m\ +\ n)
|
11416
|
212 |
\rulenamedx{dvd_add}
|
10594
|
213 |
\end{isabelle}
|
|
214 |
|
11216
|
215 |
\subsubsection{Simplifier Tricks}
|
10594
|
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
|
10794
|
219 |
nice properties; often you should remove it by simplifying with this split
|
|
220 |
rule:
|
10594
|
221 |
\begin{isabelle}
|
|
222 |
P(a-b)\ =\ ((a<b\ \isasymlongrightarrow \ P\
|
|
223 |
0)\ \isasymand \ (\isasymforall d.\ a\ =\ b+d\ \isasymlongrightarrow \ P\
|
|
224 |
d))
|
|
225 |
\rulename{nat_diff_split}
|
|
226 |
\end{isabelle}
|
|
227 |
For example, it proves the following fact, which lies outside the scope of
|
|
228 |
linear arithmetic:
|
|
229 |
\begin{isabelle}
|
|
230 |
\isacommand{lemma}\ "(n-1)*(n+1)\ =\ n*n\ -\ 1"\isanewline
|
|
231 |
\isacommand{apply}\ (simp\ split:\ nat_diff_split)\isanewline
|
|
232 |
\isacommand{done}
|
|
233 |
\end{isabelle}
|
|
234 |
|
|
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:
|
|
239 |
\begin{isabelle}
|
|
240 |
m\ +\ n\ +\ k\ =\ m\ +\ (n\ +\ k)
|
11416
|
241 |
\rulenamedx{add_assoc}\isanewline
|
10594
|
242 |
m\ +\ n\ =\ n\ +\ m%
|
11416
|
243 |
\rulenamedx{add_commute}\isanewline
|
10594
|
244 |
x\ +\ (y\ +\ z)\ =\ y\ +\ (x\
|
|
245 |
+\ z)
|
|
246 |
\rulename{add_left_commute}
|
|
247 |
\end{isabelle}
|
|
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
|
|
250 |
with this goal:
|
|
251 |
\begin{isabelle}
|
|
252 |
\ 1.\ Suc\ (i\ +\ j\ *\ l\ *\ k\ +\ m\ *\ n)\ =\
|
|
253 |
f\ (n\ *\ m\ +\ i\ +\ k\ *\ j\ *\ l)
|
|
254 |
\end{isabelle}
|
|
255 |
%
|
|
256 |
Simplify using \isa{add_ac} and \isa{mult_ac}:
|
|
257 |
\begin{isabelle}
|
|
258 |
\isacommand{apply}\ (simp\ add:\ add_ac\ mult_ac)
|
|
259 |
\end{isabelle}
|
|
260 |
%
|
|
261 |
Here is the resulting subgoal:
|
|
262 |
\begin{isabelle}
|
|
263 |
\ 1.\ Suc\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))\
|
|
264 |
=\ f\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))%
|
11416
|
265 |
\end{isabelle}%
|
|
266 |
\index{natural numbers|)}\index{*nat (type)|)}
|
|
267 |
|
10594
|
268 |
|
|
269 |
|
11216
|
270 |
\subsection{The Type of Integers, {\tt\slshape int}}
|
10594
|
271 |
|
11416
|
272 |
\index{integers|(}\index{*int (type)|(}%
|
10794
|
273 |
Reasoning methods resemble those for the natural numbers, but induction and
|
10881
|
274 |
the constant \isa{Suc} are not available. HOL provides many lemmas
|
10794
|
275 |
for proving inequalities involving integer multiplication and division,
|
|
276 |
similar to those shown above for type~\isa{nat}.
|
|
277 |
|
11416
|
278 |
The \rmindex{absolute value} function \cdx{abs} is overloaded for the numeric types.
|
10794
|
279 |
It is defined for the integers; we have for example the obvious law
|
|
280 |
\begin{isabelle}
|
|
281 |
\isasymbar x\ *\ y\isasymbar \ =\ \isasymbar x\isasymbar \ *\ \isasymbar y\isasymbar
|
|
282 |
\rulename{abs_mult}
|
|
283 |
\end{isabelle}
|
10594
|
284 |
|
10794
|
285 |
\begin{warn}
|
|
286 |
The absolute value bars shown above cannot be typed on a keyboard. They
|
10983
|
287 |
can be entered using the X-symbol package. In \textsc{ascii}, type \isa{abs x} to
|
10794
|
288 |
get \isa{\isasymbar x\isasymbar}.
|
|
289 |
\end{warn}
|
|
290 |
|
10881
|
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.
|
|
293 |
\begin{isabelle}
|
11174
|
294 |
\isacommand{lemma}\ "abs\ (x+y)\ \isasymle \ abs\ x\ +\ abs\ (y\ ::\ int)"\isanewline
|
10881
|
295 |
\isacommand{by}\ arith
|
|
296 |
\end{isabelle}
|
10794
|
297 |
|
|
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.
|
10594
|
305 |
|
11416
|
306 |
For division and remainder,\index{division!by negative numbers}
|
|
307 |
the treatment of negative divisors follows
|
10794
|
308 |
mathematical practice: the sign of the remainder follows that
|
10594
|
309 |
of the divisor:
|
|
310 |
\begin{isabelle}
|
|
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}
|
|
319 |
\end{isabelle}
|
|
320 |
ML treats negative divisors in the same way, but most computer hardware
|
|
321 |
treats signed operands using the same rules as for multiplication.
|
10794
|
322 |
Many facts about quotients and remainders are provided:
|
10594
|
323 |
\begin{isabelle}
|
|
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}
|
|
327 |
\par\smallskip
|
|
328 |
(a\ +\ b)\ mod\ c\ =\ (a\ mod\ c\ +\ b\ mod\ c)\ mod\ c%
|
|
329 |
\rulename{zmod_zadd1_eq}
|
|
330 |
\end{isabelle}
|
|
331 |
|
|
332 |
\begin{isabelle}
|
|
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}
|
|
337 |
\end{isabelle}
|
|
338 |
|
|
339 |
\begin{isabelle}
|
|
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\
|
|
343 |
c)\ +\ a\ mod\ b%
|
|
344 |
\rulename{zmod_zmult2_eq}
|
|
345 |
\end{isabelle}
|
|
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
|
|
349 |
is
|
|
350 |
$\isa{a} = 7$, $\isa{b} = 2$ and $\isa{c} = -3$, when the left-hand side of
|
11416
|
351 |
\isa{zdiv_zmult2_eq} is $-2$ while the right-hand side is~$-1$.%
|
|
352 |
\index{integers|)}\index{*int (type)|)}
|
10594
|
353 |
|
|
354 |
|
11216
|
355 |
\subsection{The Type of Real Numbers, {\tt\slshape real}}
|
10594
|
356 |
|
11416
|
357 |
\index{real numbers|(}\index{*real (type)|(}%
|
10777
|
358 |
The real numbers enjoy two significant properties that the integers lack.
|
|
359 |
They are
|
|
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.)
|
10794
|
367 |
The formalization of completeness is complicated; rather than
|
10777
|
368 |
reproducing it here, we refer you to the theory \texttt{RComplete} in
|
|
369 |
directory \texttt{Real}.
|
10794
|
370 |
Density, however, is trivial to express:
|
10777
|
371 |
\begin{isabelle}
|
|
372 |
x\ <\ y\ \isasymLongrightarrow \ \isasymexists r.\ x\ <\ r\ \isasymand \ r\ <\ y%
|
|
373 |
\rulename{real_dense}
|
|
374 |
\end{isabelle}
|
|
375 |
|
|
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:
|
|
379 |
\begin{isabelle}
|
11174
|
380 |
x\ *\ (y\ /\ z)\ =\ x\ *\ y\ /\ z
|
10777
|
381 |
\rulename{real_times_divide1_eq}\isanewline
|
11174
|
382 |
y\ /\ z\ *\ x\ =\ y\ *\ x\ /\ z
|
10777
|
383 |
\rulename{real_times_divide2_eq}\isanewline
|
11174
|
384 |
x\ /\ (y\ /\ z)\ =\ x\ *\ z\ /\ y
|
10777
|
385 |
\rulename{real_divide_divide1_eq}\isanewline
|
|
386 |
x\ /\ y\ /\ z\ =\ x\ /\ (y\ *\ z)
|
|
387 |
\rulename{real_divide_divide2_eq}
|
|
388 |
\end{isabelle}
|
|
389 |
|
|
390 |
Signs are extracted from quotients in the hope that complementary terms can
|
|
391 |
then be cancelled:
|
|
392 |
\begin{isabelle}
|
|
393 |
-\ x\ /\ y\ =\ -\ (x\ /\ y)
|
|
394 |
\rulename{real_minus_divide_eq}\isanewline
|
|
395 |
x\ /\ -\ y\ =\ -\ (x\ /\ y)
|
|
396 |
\rulename{real_divide_minus_eq}
|
|
397 |
\end{isabelle}
|
|
398 |
|
|
399 |
The following distributive law is available, but it is not installed as a
|
|
400 |
simplification rule.
|
|
401 |
\begin{isabelle}
|
|
402 |
(x\ +\ y)\ /\ z\ =\ x\ /\ z\ +\ y\ /\ z%
|
|
403 |
\rulename{real_add_divide_distrib}
|
|
404 |
\end{isabelle}
|
|
405 |
|
10594
|
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
|
10777
|
408 |
associativity and commutativity theorems for addition, while similarly
|
10594
|
409 |
\isa{real_mult_ac} contains those properties for multiplication.
|
|
410 |
|
10777
|
411 |
The absolute value function \isa{abs} is
|
|
412 |
defined for the reals, along with many theorems such as this one about
|
|
413 |
exponentiation:
|
|
414 |
\begin{isabelle}
|
|
415 |
\isasymbar r\isasymbar \ \isacharcircum \ n\ =\ \isasymbar r\ \isacharcircum \ n\isasymbar
|
|
416 |
\rulename{realpow_abs}
|
|
417 |
\end{isabelle}
|
|
418 |
|
11416
|
419 |
Numeric literals\index{numeric literals!for type \protect\isa{real}}
|
|
420 |
for type \isa{real} have the same syntax as those for type
|
11174
|
421 |
\isa{int} and only express integral values. Fractions expressed
|
|
422 |
using the division operator are automatically simplified to lowest terms:
|
|
423 |
\begin{isabelle}
|
|
424 |
\ 1.\ P\ ((\#3\ /\ \#4)\ *\ (\#8\ /\ \#15))\isanewline
|
|
425 |
\isacommand{apply} simp\isanewline
|
|
426 |
\ 1.\ P\ (\#2\ /\ \#5)
|
|
427 |
\end{isabelle}
|
|
428 |
Exponentiation can express floating-point values such as
|
|
429 |
\isa{\#2 * \#10\isacharcircum\#6}, but at present no special simplification
|
|
430 |
is performed.
|
|
431 |
|
|
432 |
|
10881
|
433 |
\begin{warn}
|
|
434 |
Type \isa{real} is only available in the logic HOL-Real, which
|
10777
|
435 |
is HOL extended with the rather substantial development of the real
|
11174
|
436 |
numbers. Base your theory upon theory
|
11416
|
437 |
\isa{Real}, not the usual \isa{Main}.%
|
|
438 |
\index{real numbers|)}\index{*real (type)|)}
|
|
439 |
Launch Isabelle using the command
|
11174
|
440 |
\begin{verbatim}
|
|
441 |
Isabelle -l HOL-Real
|
|
442 |
\end{verbatim}
|
10881
|
443 |
\end{warn}
|
10777
|
444 |
|
|
445 |
Also distributed with Isabelle is HOL-Hyperreal,
|
11416
|
446 |
whose theory \isa{Hyperreal} defines the type \tydx{hypreal} of
|
|
447 |
\rmindex{non-standard reals}. These
|
10777
|
448 |
\textbf{hyperreals} include infinitesimals, which represent infinitely
|
|
449 |
small and infinitely large quantities; they facilitate proofs
|
10794
|
450 |
about limits, differentiation and integration~\cite{fleuriot-jcm}. The
|
|
451 |
development defines an infinitely large number, \isa{omega} and an
|
10881
|
452 |
infinitely small positive number, \isa{epsilon}. The
|
|
453 |
relation $x\approx y$ means ``$x$ is infinitely close to~$y$''.
|