author | paulson |
Fri, 30 Nov 2001 12:18:14 +0100 | |
changeset 12333 | ef43a3d6e962 |
parent 12156 | d2758965362e |
child 13750 | b5cd10cb106b |
permissions | -rw-r--r-- |
10794 | 1 |
% $Id$ |
11389 | 2 |
|
3 |
\section{Numbers} |
|
4 |
\label{sec:numbers} |
|
5 |
||
11494 | 6 |
\index{numbers|(}% |
11174 | 7 |
Until now, our numerical examples have used the type of \textbf{natural |
8 |
numbers}, |
|
10594 | 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 |
|
11174 | 11 |
recursive function definitions. HOL also provides the type |
10794 | 12 |
\isa{int} of \textbf{integers}, which lack induction but support true |
11174 | 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 |
|
21 |
infix symbols. |
|
10594 | 22 |
|
11416 | 23 |
\index{linear arithmetic}% |
10594 | 24 |
Many theorems involving numeric types can be proved automatically by |
25 |
Isabelle's arithmetic decision procedure, the method |
|
11416 | 26 |
\methdx{arith}. Linear arithmetic comprises addition, subtraction |
10594 | 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 |
|
30 |
causes case splits. |
|
31 |
||
32 |
The simplifier reduces arithmetic expressions in other |
|
33 |
ways, such as dividing through by common factors. For problems that lie |
|
10881 | 34 |
outside the scope of automation, HOL provides hundreds of |
10594 | 35 |
theorems about multiplication, division, etc., that can be brought to |
10881 | 36 |
bear. You can locate them using Proof General's Find |
37 |
button. A few lemmas are given below to show what |
|
10794 | 38 |
is available. |
10594 | 39 |
|
40 |
\subsection{Numeric Literals} |
|
10779 | 41 |
\label{sec:numerals} |
10594 | 42 |
|
11416 | 43 |
\index{numeric literals|(}% |
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
44 |
The constants \cdx{0} and \cdx{1} are overloaded. They denote zero and one, |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
45 |
respectively, for all numeric types. Other values are expressed by numeric |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
46 |
literals, which consist of one or more decimal digits optionally preceeded by |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
47 |
a minus sign (\isa{-}). Examples are \isa{2}, \isa{-3} and |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
48 |
\isa{441223334678}. Literals are available for the types of natural numbers, |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
49 |
integers and reals; they denote integer values of arbitrary size. |
10594 | 50 |
|
51 |
Literals look like constants, but they abbreviate |
|
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
52 |
terms representing the number in a two's complement binary notation. |
10794 | 53 |
Isabelle performs arithmetic on literals by rewriting rather |
10594 | 54 |
than using the hardware arithmetic. In most cases arithmetic |
55 |
is fast enough, even for large numbers. The arithmetic operations |
|
10794 | 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. |
|
10594 | 59 |
|
11416 | 60 |
\begin{warn}\index{overloading!and arithmetic} |
10794 | 61 |
The arithmetic operators are |
10594 | 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: |
|
10794 | 65 |
\par |
10594 | 66 |
\begin{isabelle} |
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
67 |
\isacommand{lemma}\ "2\ *\ m\ =\ m\ +\ m" |
10594 | 68 |
\end{isabelle} |
69 |
% |
|
70 |
Carefully observe how Isabelle displays the subgoal: |
|
71 |
\begin{isabelle} |
|
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
72 |
\ 1.\ (2::'a)\ *\ m\ =\ m\ +\ m |
10594 | 73 |
\end{isabelle} |
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
74 |
The type \isa{'a} given for the literal \isa{2} warns us that no numeric |
10594 | 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. |
|
10794 | 77 |
\end{warn} |
78 |
||
10881 | 79 |
\begin{warn} |
11428 | 80 |
\index{recdef@\isacommand {recdef} (command)!and numeric literals} |
11416 | 81 |
Numeric literals are not constructors and therefore |
82 |
must not be used in patterns. For example, this declaration is |
|
83 |
rejected: |
|
10881 | 84 |
\begin{isabelle} |
85 |
\isacommand{recdef}\ h\ "\isacharbraceleft \isacharbraceright "\isanewline |
|
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
86 |
"h\ 3\ =\ 2"\isanewline |
11148 | 87 |
"h\ i\ \ =\ i" |
10881 | 88 |
\end{isabelle} |
89 |
||
90 |
You should use a conditional expression instead: |
|
91 |
\begin{isabelle} |
|
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
92 |
"h\ i\ =\ (if\ i\ =\ 3\ then\ 2\ else\ i)" |
10881 | 93 |
\end{isabelle} |
11416 | 94 |
\index{numeric literals|)} |
10881 | 95 |
\end{warn} |
96 |
||
10594 | 97 |
|
98 |
||
11216 | 99 |
\subsection{The Type of Natural Numbers, {\tt\slshape nat}} |
10594 | 100 |
|
11416 | 101 |
\index{natural numbers|(}\index{*nat (type)|(}% |
10594 | 102 |
This type requires no introduction: we have been using it from the |
10794 | 103 |
beginning. Hundreds of theorems about the natural numbers are |
10594 | 104 |
proved in the theories \isa{Nat}, \isa{NatArith} and \isa{Divides}. Only |
105 |
in exceptional circumstances should you resort to induction. |
|
106 |
||
107 |
\subsubsection{Literals} |
|
11416 | 108 |
\index{numeric literals!for type \protect\isa{nat}}% |
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
109 |
The notational options for the natural numbers are confusing. Recall that an |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
110 |
overloaded constant can be defined independently for each type; the definition |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
111 |
of \cdx{1} for type \isa{nat} is |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
112 |
\begin{isabelle} |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
113 |
1\ \isasymequiv\ Suc\ 0 |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
114 |
\rulename{One_nat_def} |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
115 |
\end{isabelle} |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
116 |
This is installed as a simplification rule, so the simplifier will replace |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
117 |
every occurrence of \isa{1::nat} by \isa{Suc\ 0}. Literals are obviously |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
118 |
better than nested \isa{Suc}s at expressing large values. But many theorems, |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
119 |
including the rewrite rules for primitive recursive functions, can only be |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
120 |
applied to terms of the form \isa{Suc\ $n$}. |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
121 |
|
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
122 |
The following default simplification rules replace |
10794 | 123 |
small literals by zero and successor: |
10594 | 124 |
\begin{isabelle} |
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
125 |
2\ +\ n\ =\ Suc\ (Suc\ n) |
10594 | 126 |
\rulename{add_2_eq_Suc}\isanewline |
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
127 |
n\ +\ 2\ =\ Suc\ (Suc\ n) |
10594 | 128 |
\rulename{add_2_eq_Suc'} |
129 |
\end{isabelle} |
|
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
130 |
It is less easy to transform \isa{100} into \isa{Suc\ 99} (for example), and |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
131 |
the simplifier will normally reverse this transformation. Novices should |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
132 |
express natural numbers using \isa{0} and \isa{Suc} only. |
10594 | 133 |
|
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: |
|
138 |
\begin{isabelle} |
|
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\ |
|
142 |
*\ k\ <\ j\ *\ k% |
|
143 |
\rulename{mult_less_mono1}\isanewline |
|
144 |
m\ \isasymle \ n\ \isasymLongrightarrow \ m\ div\ k\ \isasymle \ n\ div\ k% |
|
145 |
\rulename{div_le_mono} |
|
146 |
\end{isabelle} |
|
147 |
% |
|
148 |
Various distributive laws concerning multiplication are available: |
|
149 |
\begin{isabelle} |
|
150 |
(m\ +\ n)\ *\ k\ =\ m\ *\ k\ +\ n\ *\ k% |
|
11416 | 151 |
\rulenamedx{add_mult_distrib}\isanewline |
10594 | 152 |
(m\ -\ n)\ *\ k\ =\ m\ *\ k\ -\ n\ *\ k% |
11416 | 153 |
\rulenamedx{diff_mult_distrib}\isanewline |
10594 | 154 |
(m\ mod\ n)\ *\ k\ =\ (m\ *\ k)\ mod\ (n\ *\ k) |
11416 | 155 |
\rulenamedx{mod_mult_distrib} |
10594 | 156 |
\end{isabelle} |
157 |
||
158 |
\subsubsection{Division} |
|
11416 | 159 |
\index{division!for type \protect\isa{nat}}% |
10881 | 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: |
|
10594 | 163 |
\begin{isabelle} |
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% |
|
11416 | 167 |
\rulenamedx{mod_div_equality} |
10594 | 168 |
\end{isabelle} |
169 |
||
170 |
Many less obvious facts about quotient and remainder are also provided. |
|
171 |
Here is a selection: |
|
172 |
\begin{isabelle} |
|
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} |
|
183 |
\end{isabelle} |
|
184 |
||
185 |
Surprisingly few of these results depend upon the |
|
11416 | 186 |
divisors' being nonzero. |
187 |
\index{division!by zero}% |
|
188 |
That is because division by |
|
10794 | 189 |
zero yields zero: |
10594 | 190 |
\begin{isabelle} |
191 |
a\ div\ 0\ =\ 0 |
|
192 |
\rulename{DIVISION_BY_ZERO_DIV}\isanewline |
|
193 |
a\ mod\ 0\ =\ a% |
|
194 |
\rulename{DIVISION_BY_ZERO_MOD} |
|
195 |
\end{isabelle} |
|
196 |
As a concession to convention, these equations are not installed as default |
|
11174 | 197 |
simplification rules. In \isa{div_mult_mult1} above, one of |
11161 | 198 |
the two divisors (namely~\isa{c}) must still be nonzero. |
10594 | 199 |
|
11416 | 200 |
The \textbf{divides} relation\index{divides relation} |
201 |
has the standard definition, which |
|
10594 | 202 |
is overloaded over all numeric types: |
203 |
\begin{isabelle} |
|
204 |
m\ dvd\ n\ \isasymequiv\ {\isasymexists}k.\ n\ =\ m\ *\ k |
|
11416 | 205 |
\rulenamedx{dvd_def} |
10594 | 206 |
\end{isabelle} |
207 |
% |
|
208 |
Section~\ref{sec:proving-euclid} discusses proofs involving this |
|
209 |
relation. Here are some of the facts proved about it: |
|
210 |
\begin{isabelle} |
|
211 |
\isasymlbrakk m\ dvd\ n;\ n\ dvd\ m\isasymrbrakk \ \isasymLongrightarrow \ m\ =\ n% |
|
11416 | 212 |
\rulenamedx{dvd_anti_sym}\isanewline |
10594 | 213 |
\isasymlbrakk k\ dvd\ m;\ k\ dvd\ n\isasymrbrakk \ \isasymLongrightarrow \ k\ dvd\ (m\ +\ n) |
11416 | 214 |
\rulenamedx{dvd_add} |
10594 | 215 |
\end{isabelle} |
216 |
||
11216 | 217 |
\subsubsection{Simplifier Tricks} |
10594 | 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 |
|
10794 | 221 |
nice properties; often you should remove it by simplifying with this split |
222 |
rule: |
|
10594 | 223 |
\begin{isabelle} |
224 |
P(a-b)\ =\ ((a<b\ \isasymlongrightarrow \ P\ |
|
225 |
0)\ \isasymand \ (\isasymforall d.\ a\ =\ b+d\ \isasymlongrightarrow \ P\ |
|
226 |
d)) |
|
227 |
\rulename{nat_diff_split} |
|
228 |
\end{isabelle} |
|
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
229 |
For example, splitting helps to prove the following fact: |
10594 | 230 |
\begin{isabelle} |
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
231 |
\isacommand{lemma}\ "(n\ -\ 2)\ *\ (n\ +\ 2)\ =\ n\ *\ n\ -\ (4::nat)"\isanewline |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
232 |
\isacommand{apply}\ (simp\ split:\ nat_diff_split,\ clarify)\isanewline |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
233 |
\ 1.\ \isasymAnd d.\ \isasymlbrakk n\ <\ 2;\ n\ *\ n\ =\ 4\ +\ d\isasymrbrakk \ \isasymLongrightarrow \ d\ =\ 0 |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
234 |
\end{isabelle} |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
235 |
The result lies outside the scope of linear arithmetic, but |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
236 |
it is easily found |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
237 |
if we explicitly split \isa{n<2} as \isa{n=0} or \isa{n=1}: |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
238 |
\begin{isabelle} |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
239 |
\isacommand{apply}\ (subgoal_tac\ "n=0\ |\ n=1",\ force,\ arith)\isanewline |
10594 | 240 |
\isacommand{done} |
241 |
\end{isabelle} |
|
242 |
||
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: |
|
247 |
\begin{isabelle} |
|
248 |
m\ +\ n\ +\ k\ =\ m\ +\ (n\ +\ k) |
|
11416 | 249 |
\rulenamedx{add_assoc}\isanewline |
10594 | 250 |
m\ +\ n\ =\ n\ +\ m% |
11416 | 251 |
\rulenamedx{add_commute}\isanewline |
10594 | 252 |
x\ +\ (y\ +\ z)\ =\ y\ +\ (x\ |
253 |
+\ z) |
|
254 |
\rulename{add_left_commute} |
|
255 |
\end{isabelle} |
|
11494 | 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 |
|
10594 | 260 |
with this goal: |
261 |
\begin{isabelle} |
|
262 |
\ 1.\ Suc\ (i\ +\ j\ *\ l\ *\ k\ +\ m\ *\ n)\ =\ |
|
263 |
f\ (n\ *\ m\ +\ i\ +\ k\ *\ j\ *\ l) |
|
264 |
\end{isabelle} |
|
265 |
% |
|
266 |
Simplify using \isa{add_ac} and \isa{mult_ac}: |
|
267 |
\begin{isabelle} |
|
268 |
\isacommand{apply}\ (simp\ add:\ add_ac\ mult_ac) |
|
269 |
\end{isabelle} |
|
270 |
% |
|
271 |
Here is the resulting subgoal: |
|
272 |
\begin{isabelle} |
|
273 |
\ 1.\ Suc\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))\ |
|
274 |
=\ f\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))% |
|
11416 | 275 |
\end{isabelle}% |
276 |
\index{natural numbers|)}\index{*nat (type)|)} |
|
277 |
||
10594 | 278 |
|
279 |
||
11216 | 280 |
\subsection{The Type of Integers, {\tt\slshape int}} |
10594 | 281 |
|
11416 | 282 |
\index{integers|(}\index{*int (type)|(}% |
10794 | 283 |
Reasoning methods resemble those for the natural numbers, but induction and |
10881 | 284 |
the constant \isa{Suc} are not available. HOL provides many lemmas |
10794 | 285 |
for proving inequalities involving integer multiplication and division, |
286 |
similar to those shown above for type~\isa{nat}. |
|
287 |
||
11416 | 288 |
The \rmindex{absolute value} function \cdx{abs} is overloaded for the numeric types. |
10794 | 289 |
It is defined for the integers; we have for example the obvious law |
290 |
\begin{isabelle} |
|
291 |
\isasymbar x\ *\ y\isasymbar \ =\ \isasymbar x\isasymbar \ *\ \isasymbar y\isasymbar |
|
292 |
\rulename{abs_mult} |
|
293 |
\end{isabelle} |
|
10594 | 294 |
|
10794 | 295 |
\begin{warn} |
296 |
The absolute value bars shown above cannot be typed on a keyboard. They |
|
10983 | 297 |
can be entered using the X-symbol package. In \textsc{ascii}, type \isa{abs x} to |
10794 | 298 |
get \isa{\isasymbar x\isasymbar}. |
299 |
\end{warn} |
|
300 |
||
10881 | 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. |
|
303 |
\begin{isabelle} |
|
11174 | 304 |
\isacommand{lemma}\ "abs\ (x+y)\ \isasymle \ abs\ x\ +\ abs\ (y\ ::\ int)"\isanewline |
10881 | 305 |
\isacommand{by}\ arith |
306 |
\end{isabelle} |
|
10794 | 307 |
|
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 |
|
11494 | 310 |
operands of sums and products. The name \isa{zadd_ac}\index{*zadd_ac (theorems)} |
311 |
refers to the |
|
10794 | 312 |
associativity and commutativity theorems for integer addition, while |
11494 | 313 |
\isa{zmult_ac}\index{*zmult_ac (theorems)} |
314 |
has the analogous theorems for multiplication. The |
|
10794 | 315 |
prefix~\isa{z} in many theorem names recalls the use of $\mathbb{Z}$ to |
316 |
denote the set of integers. |
|
10594 | 317 |
|
11416 | 318 |
For division and remainder,\index{division!by negative numbers} |
319 |
the treatment of negative divisors follows |
|
10794 | 320 |
mathematical practice: the sign of the remainder follows that |
10594 | 321 |
of the divisor: |
322 |
\begin{isabelle} |
|
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
323 |
0\ <\ b\ \isasymLongrightarrow \ 0\ \isasymle \ a\ mod\ b% |
10594 | 324 |
\rulename{pos_mod_sign}\isanewline |
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
325 |
0\ <\ b\ \isasymLongrightarrow \ a\ mod\ b\ <\ b% |
10594 | 326 |
\rulename{pos_mod_bound}\isanewline |
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
327 |
b\ <\ 0\ \isasymLongrightarrow \ a\ mod\ b\ \isasymle \ 0 |
10594 | 328 |
\rulename{neg_mod_sign}\isanewline |
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
329 |
b\ <\ 0\ \isasymLongrightarrow \ b\ <\ a\ mod\ b% |
10594 | 330 |
\rulename{neg_mod_bound} |
331 |
\end{isabelle} |
|
332 |
ML treats negative divisors in the same way, but most computer hardware |
|
333 |
treats signed operands using the same rules as for multiplication. |
|
10794 | 334 |
Many facts about quotients and remainders are provided: |
10594 | 335 |
\begin{isabelle} |
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} |
|
339 |
\par\smallskip |
|
340 |
(a\ +\ b)\ mod\ c\ =\ (a\ mod\ c\ +\ b\ mod\ c)\ mod\ c% |
|
341 |
\rulename{zmod_zadd1_eq} |
|
342 |
\end{isabelle} |
|
343 |
||
344 |
\begin{isabelle} |
|
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} |
|
349 |
\end{isabelle} |
|
350 |
||
351 |
\begin{isabelle} |
|
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
352 |
0\ <\ c\ \isasymLongrightarrow \ a\ div\ (b*c)\ =\ a\ div\ b\ div\ c% |
10594 | 353 |
\rulename{zdiv_zmult2_eq}\isanewline |
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
354 |
0\ <\ c\ \isasymLongrightarrow \ a\ mod\ (b*c)\ =\ b*(a\ div\ b\ mod\ |
10594 | 355 |
c)\ +\ a\ mod\ b% |
356 |
\rulename{zmod_zmult2_eq} |
|
357 |
\end{isabelle} |
|
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 |
|
361 |
is |
|
362 |
$\isa{a} = 7$, $\isa{b} = 2$ and $\isa{c} = -3$, when the left-hand side of |
|
11416 | 363 |
\isa{zdiv_zmult2_eq} is $-2$ while the right-hand side is~$-1$.% |
364 |
\index{integers|)}\index{*int (type)|)} |
|
10594 | 365 |
|
366 |
||
11216 | 367 |
\subsection{The Type of Real Numbers, {\tt\slshape real}} |
10594 | 368 |
|
11416 | 369 |
\index{real numbers|(}\index{*real (type)|(}% |
10777 | 370 |
The real numbers enjoy two significant properties that the integers lack. |
371 |
They are |
|
372 |
\textbf{dense}: between every two distinct real numbers there lies another. |
|
373 |
This property follows from the division laws, since if $x<y$ then between |
|
374 |
them lies $(x+y)/2$. The second property is that they are |
|
375 |
\textbf{complete}: every set of reals that is bounded above has a least |
|
376 |
upper bound. Completeness distinguishes the reals from the rationals, for |
|
377 |
which the set $\{x\mid x^2<2\}$ has no least upper bound. (It could only be |
|
378 |
$\surd2$, which is irrational.) |
|
10794 | 379 |
The formalization of completeness is complicated; rather than |
10777 | 380 |
reproducing it here, we refer you to the theory \texttt{RComplete} in |
381 |
directory \texttt{Real}. |
|
10794 | 382 |
Density, however, is trivial to express: |
10777 | 383 |
\begin{isabelle} |
384 |
x\ <\ y\ \isasymLongrightarrow \ \isasymexists r.\ x\ <\ r\ \isasymand \ r\ <\ y% |
|
385 |
\rulename{real_dense} |
|
386 |
\end{isabelle} |
|
387 |
||
388 |
Here is a selection of rules about the division operator. The following |
|
389 |
are installed as default simplification rules in order to express |
|
390 |
combinations of products and quotients as rational expressions: |
|
391 |
\begin{isabelle} |
|
11174 | 392 |
x\ *\ (y\ /\ z)\ =\ x\ *\ y\ /\ z |
10777 | 393 |
\rulename{real_times_divide1_eq}\isanewline |
11174 | 394 |
y\ /\ z\ *\ x\ =\ y\ *\ x\ /\ z |
10777 | 395 |
\rulename{real_times_divide2_eq}\isanewline |
11174 | 396 |
x\ /\ (y\ /\ z)\ =\ x\ *\ z\ /\ y |
10777 | 397 |
\rulename{real_divide_divide1_eq}\isanewline |
398 |
x\ /\ y\ /\ z\ =\ x\ /\ (y\ *\ z) |
|
399 |
\rulename{real_divide_divide2_eq} |
|
400 |
\end{isabelle} |
|
401 |
||
402 |
Signs are extracted from quotients in the hope that complementary terms can |
|
403 |
then be cancelled: |
|
404 |
\begin{isabelle} |
|
405 |
-\ x\ /\ y\ =\ -\ (x\ /\ y) |
|
406 |
\rulename{real_minus_divide_eq}\isanewline |
|
407 |
x\ /\ -\ y\ =\ -\ (x\ /\ y) |
|
408 |
\rulename{real_divide_minus_eq} |
|
409 |
\end{isabelle} |
|
410 |
||
411 |
The following distributive law is available, but it is not installed as a |
|
412 |
simplification rule. |
|
413 |
\begin{isabelle} |
|
414 |
(x\ +\ y)\ /\ z\ =\ x\ /\ z\ +\ y\ /\ z% |
|
415 |
\rulename{real_add_divide_distrib} |
|
416 |
\end{isabelle} |
|
417 |
||
10594 | 418 |
As with the other numeric types, the simplifier can sort the operands of |
419 |
addition and multiplication. The name \isa{real_add_ac} refers to the |
|
10777 | 420 |
associativity and commutativity theorems for addition, while similarly |
10594 | 421 |
\isa{real_mult_ac} contains those properties for multiplication. |
422 |
||
10777 | 423 |
The absolute value function \isa{abs} is |
424 |
defined for the reals, along with many theorems such as this one about |
|
425 |
exponentiation: |
|
426 |
\begin{isabelle} |
|
12333 | 427 |
\isasymbar r\ \isacharcircum \ n\isasymbar\ =\ |
428 |
\isasymbar r\isasymbar \ \isacharcircum \ n |
|
10777 | 429 |
\rulename{realpow_abs} |
430 |
\end{isabelle} |
|
431 |
||
11416 | 432 |
Numeric literals\index{numeric literals!for type \protect\isa{real}} |
433 |
for type \isa{real} have the same syntax as those for type |
|
11174 | 434 |
\isa{int} and only express integral values. Fractions expressed |
435 |
using the division operator are automatically simplified to lowest terms: |
|
436 |
\begin{isabelle} |
|
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
437 |
\ 1.\ P\ ((3\ /\ 4)\ *\ (8\ /\ 15))\isanewline |
11174 | 438 |
\isacommand{apply} simp\isanewline |
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
439 |
\ 1.\ P\ (2\ /\ 5) |
11174 | 440 |
\end{isabelle} |
441 |
Exponentiation can express floating-point values such as |
|
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
442 |
\isa{2 * 10\isacharcircum6}, but at present no special simplification |
11174 | 443 |
is performed. |
444 |
||
445 |
||
10881 | 446 |
\begin{warn} |
447 |
Type \isa{real} is only available in the logic HOL-Real, which |
|
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
448 |
is HOL extended with a definitional development of the real |
11174 | 449 |
numbers. Base your theory upon theory |
11428 | 450 |
\thydx{Real}, not the usual \isa{Main}.% |
11416 | 451 |
\index{real numbers|)}\index{*real (type)|)} |
452 |
Launch Isabelle using the command |
|
11174 | 453 |
\begin{verbatim} |
454 |
Isabelle -l HOL-Real |
|
455 |
\end{verbatim} |
|
10881 | 456 |
\end{warn} |
10777 | 457 |
|
458 |
Also distributed with Isabelle is HOL-Hyperreal, |
|
11416 | 459 |
whose theory \isa{Hyperreal} defines the type \tydx{hypreal} of |
460 |
\rmindex{non-standard reals}. These |
|
10777 | 461 |
\textbf{hyperreals} include infinitesimals, which represent infinitely |
462 |
small and infinitely large quantities; they facilitate proofs |
|
10794 | 463 |
about limits, differentiation and integration~\cite{fleuriot-jcm}. The |
464 |
development defines an infinitely large number, \isa{omega} and an |
|
10881 | 465 |
infinitely small positive number, \isa{epsilon}. The |
12333 | 466 |
relation $x\approx y$ means ``$x$ is infinitely close to~$y$.'' |
467 |
Theory \isa{Hyperreal} also defines transcendental functions such as sine, |
|
468 |
cosine, exponential and logarithm --- even the versions for type |
|
469 |
\isa{real}, because they are defined using nonstandard limits.% |
|
11494 | 470 |
\index{numbers|)} |