author | haftmann |
Fri, 04 Jul 2014 20:18:47 +0200 | |
changeset 57512 | cc97b347b301 |
parent 48985 | 5386df44a037 |
child 57514 | bdc2c6b40bf2 |
permissions | -rw-r--r-- |
11389 | 1 |
\section{Numbers} |
2 |
\label{sec:numbers} |
|
3 |
||
11494 | 4 |
\index{numbers|(}% |
11174 | 5 |
Until now, our numerical examples have used the type of \textbf{natural |
6 |
numbers}, |
|
10594 | 7 |
\isa{nat}. This is a recursive datatype generated by the constructors |
8 |
zero and successor, so it works well with inductive proofs and primitive |
|
11174 | 9 |
recursive function definitions. HOL also provides the type |
10794 | 10 |
\isa{int} of \textbf{integers}, which lack induction but support true |
14400 | 11 |
subtraction. With subtraction, arithmetic reasoning is easier, which makes |
12 |
the integers preferable to the natural numbers for |
|
31678 | 13 |
complicated arithmetic expressions, even if they are non-negative. There are also the types |
14400 | 14 |
\isa{rat}, \isa{real} and \isa{complex}: the rational, real and complex numbers. Isabelle has no |
13979 | 15 |
subtyping, so the numeric |
16 |
types are distinct and there are functions to convert between them. |
|
14400 | 17 |
Most numeric operations are overloaded: the same symbol can be |
11174 | 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 |
|
14400 | 20 |
infix symbols. Algebraic properties are organized using type classes |
21 |
around algebraic concepts such as rings and fields; |
|
22 |
a property such as the commutativity of addition is a single theorem |
|
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
48985
diff
changeset
|
23 |
(\isa{add.commute}) that applies to all numeric types. |
10594 | 24 |
|
11416 | 25 |
\index{linear arithmetic}% |
10594 | 26 |
Many theorems involving numeric types can be proved automatically by |
27 |
Isabelle's arithmetic decision procedure, the method |
|
11416 | 28 |
\methdx{arith}. Linear arithmetic comprises addition, subtraction |
10594 | 29 |
and multiplication by constant factors; subterms involving other operators |
30 |
are regarded as variables. The procedure can be slow, especially if the |
|
31 |
subgoal to be proved involves subtraction over type \isa{nat}, which |
|
13996 | 32 |
causes case splits. On types \isa{nat} and \isa{int}, \methdx{arith} |
14400 | 33 |
can deal with quantifiers---this is known as Presburger arithmetic---whereas on type \isa{real} it cannot. |
10594 | 34 |
|
35 |
The simplifier reduces arithmetic expressions in other |
|
36 |
ways, such as dividing through by common factors. For problems that lie |
|
10881 | 37 |
outside the scope of automation, HOL provides hundreds of |
10594 | 38 |
theorems about multiplication, division, etc., that can be brought to |
10881 | 39 |
bear. You can locate them using Proof General's Find |
40 |
button. A few lemmas are given below to show what |
|
10794 | 41 |
is available. |
10594 | 42 |
|
43 |
\subsection{Numeric Literals} |
|
10779 | 44 |
\label{sec:numerals} |
10594 | 45 |
|
11416 | 46 |
\index{numeric literals|(}% |
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
47 |
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
|
48 |
respectively, for all numeric types. Other values are expressed by numeric |
21243 | 49 |
literals, which consist of one or more decimal digits optionally preceeded by a minus sign (\isa{-}). Examples are \isa{2}, \isa{-3} and |
50 |
\isa{441223334678}. Literals are available for the types of natural |
|
51 |
numbers, integers, rationals, reals, etc.; they denote integer values of |
|
52 |
arbitrary size. |
|
10594 | 53 |
|
54 |
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
|
55 |
terms representing the number in a two's complement binary notation. |
10794 | 56 |
Isabelle performs arithmetic on literals by rewriting rather |
10594 | 57 |
than using the hardware arithmetic. In most cases arithmetic |
14400 | 58 |
is fast enough, even for numbers in the millions. The arithmetic operations |
10794 | 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. |
|
10594 | 62 |
|
11416 | 63 |
\begin{warn}\index{overloading!and arithmetic} |
10794 | 64 |
The arithmetic operators are |
10594 | 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: |
|
10794 | 68 |
\par |
10594 | 69 |
\begin{isabelle} |
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
70 |
\isacommand{lemma}\ "2\ *\ m\ =\ m\ +\ m" |
10594 | 71 |
\end{isabelle} |
72 |
% |
|
73 |
Carefully observe how Isabelle displays the subgoal: |
|
74 |
\begin{isabelle} |
|
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
75 |
\ 1.\ (2::'a)\ *\ m\ =\ m\ +\ m |
10594 | 76 |
\end{isabelle} |
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
77 |
The type \isa{'a} given for the literal \isa{2} warns us that no numeric |
10594 | 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. |
|
10794 | 80 |
\end{warn} |
81 |
||
10881 | 82 |
\begin{warn} |
31682 | 83 |
\index{function@\isacommand {function} (command)!and numeric literals} |
11416 | 84 |
Numeric literals are not constructors and therefore |
85 |
must not be used in patterns. For example, this declaration is |
|
86 |
rejected: |
|
10881 | 87 |
\begin{isabelle} |
31682 | 88 |
\isacommand{function}\ h\ \isakeyword{where}\isanewline |
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
89 |
"h\ 3\ =\ 2"\isanewline |
31682 | 90 |
\isacharbar "h\ i\ \ =\ i" |
10881 | 91 |
\end{isabelle} |
92 |
||
93 |
You should use a conditional expression instead: |
|
94 |
\begin{isabelle} |
|
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
95 |
"h\ i\ =\ (if\ i\ =\ 3\ then\ 2\ else\ i)" |
10881 | 96 |
\end{isabelle} |
11416 | 97 |
\index{numeric literals|)} |
10881 | 98 |
\end{warn} |
99 |
||
10594 | 100 |
|
11216 | 101 |
\subsection{The Type of Natural Numbers, {\tt\slshape nat}} |
10594 | 102 |
|
11416 | 103 |
\index{natural numbers|(}\index{*nat (type)|(}% |
10594 | 104 |
This type requires no introduction: we have been using it from the |
10794 | 105 |
beginning. Hundreds of theorems about the natural numbers are |
21243 | 106 |
proved in the theories \isa{Nat} and \isa{Divides}. |
14400 | 107 |
Basic properties of addition and multiplication are available through the |
31678 | 108 |
axiomatic type class for semirings (\S\ref{sec:numeric-classes}). |
10594 | 109 |
|
110 |
\subsubsection{Literals} |
|
11416 | 111 |
\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
|
112 |
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
|
113 |
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
|
114 |
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
|
115 |
\begin{isabelle} |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
116 |
1\ \isasymequiv\ Suc\ 0 |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
117 |
\rulename{One_nat_def} |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
118 |
\end{isabelle} |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
119 |
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
|
120 |
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
|
121 |
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
|
122 |
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
|
123 |
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
|
124 |
|
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
125 |
The following default simplification rules replace |
10794 | 126 |
small literals by zero and successor: |
10594 | 127 |
\begin{isabelle} |
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
128 |
2\ +\ n\ =\ Suc\ (Suc\ n) |
10594 | 129 |
\rulename{add_2_eq_Suc}\isanewline |
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
130 |
n\ +\ 2\ =\ Suc\ (Suc\ n) |
10594 | 131 |
\rulename{add_2_eq_Suc'} |
132 |
\end{isabelle} |
|
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
133 |
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
|
134 |
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
|
135 |
express natural numbers using \isa{0} and \isa{Suc} only. |
10594 | 136 |
|
137 |
\subsubsection{Division} |
|
11416 | 138 |
\index{division!for type \protect\isa{nat}}% |
10881 | 139 |
The infix operators \isa{div} and \isa{mod} are overloaded. |
140 |
Isabelle/HOL provides the basic facts about quotient and remainder |
|
141 |
on the natural numbers: |
|
10594 | 142 |
\begin{isabelle} |
143 |
m\ mod\ n\ =\ (if\ m\ <\ n\ then\ m\ else\ (m\ -\ n)\ mod\ n) |
|
144 |
\rulename{mod_if}\isanewline |
|
145 |
m\ div\ n\ *\ n\ +\ m\ mod\ n\ =\ m% |
|
11416 | 146 |
\rulenamedx{mod_div_equality} |
10594 | 147 |
\end{isabelle} |
148 |
||
149 |
Many less obvious facts about quotient and remainder are also provided. |
|
150 |
Here is a selection: |
|
151 |
\begin{isabelle} |
|
152 |
a\ *\ b\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c% |
|
153 |
\rulename{div_mult1_eq}\isanewline |
|
154 |
a\ *\ b\ mod\ c\ =\ a\ *\ (b\ mod\ c)\ mod\ c% |
|
30224 | 155 |
\rulename{mod_mult_right_eq}\isanewline |
10594 | 156 |
a\ div\ (b*c)\ =\ a\ div\ b\ div\ c% |
157 |
\rulename{div_mult2_eq}\isanewline |
|
158 |
a\ mod\ (b*c)\ =\ b * (a\ div\ b\ mod\ c)\ +\ a\ mod\ b% |
|
159 |
\rulename{mod_mult2_eq}\isanewline |
|
160 |
0\ <\ c\ \isasymLongrightarrow \ (c\ *\ a)\ div\ (c\ *\ b)\ =\ a\ div\ b% |
|
14400 | 161 |
\rulename{div_mult_mult1}\isanewline |
162 |
(m\ mod\ n)\ *\ k\ =\ (m\ *\ k)\ mod\ (n\ *\ k) |
|
163 |
\rulenamedx{mod_mult_distrib}\isanewline |
|
164 |
m\ \isasymle \ n\ \isasymLongrightarrow \ m\ div\ k\ \isasymle \ n\ div\ k% |
|
165 |
\rulename{div_le_mono} |
|
10594 | 166 |
\end{isabelle} |
167 |
||
168 |
Surprisingly few of these results depend upon the |
|
11416 | 169 |
divisors' being nonzero. |
170 |
\index{division!by zero}% |
|
171 |
That is because division by |
|
10794 | 172 |
zero yields zero: |
10594 | 173 |
\begin{isabelle} |
174 |
a\ div\ 0\ =\ 0 |
|
175 |
\rulename{DIVISION_BY_ZERO_DIV}\isanewline |
|
176 |
a\ mod\ 0\ =\ a% |
|
177 |
\rulename{DIVISION_BY_ZERO_MOD} |
|
178 |
\end{isabelle} |
|
14400 | 179 |
In \isa{div_mult_mult1} above, one of |
11161 | 180 |
the two divisors (namely~\isa{c}) must still be nonzero. |
10594 | 181 |
|
11416 | 182 |
The \textbf{divides} relation\index{divides relation} |
183 |
has the standard definition, which |
|
10594 | 184 |
is overloaded over all numeric types: |
185 |
\begin{isabelle} |
|
186 |
m\ dvd\ n\ \isasymequiv\ {\isasymexists}k.\ n\ =\ m\ *\ k |
|
11416 | 187 |
\rulenamedx{dvd_def} |
10594 | 188 |
\end{isabelle} |
189 |
% |
|
190 |
Section~\ref{sec:proving-euclid} discusses proofs involving this |
|
191 |
relation. Here are some of the facts proved about it: |
|
192 |
\begin{isabelle} |
|
193 |
\isasymlbrakk m\ dvd\ n;\ n\ dvd\ m\isasymrbrakk \ \isasymLongrightarrow \ m\ =\ n% |
|
33750 | 194 |
\rulenamedx{dvd_antisym}\isanewline |
10594 | 195 |
\isasymlbrakk k\ dvd\ m;\ k\ dvd\ n\isasymrbrakk \ \isasymLongrightarrow \ k\ dvd\ (m\ +\ n) |
11416 | 196 |
\rulenamedx{dvd_add} |
10594 | 197 |
\end{isabelle} |
198 |
||
14400 | 199 |
\subsubsection{Subtraction} |
200 |
||
201 |
There are no negative natural numbers, so \isa{m\ -\ n} equals zero unless |
|
202 |
\isa{m} exceeds~\isa{n}. The following is one of the few facts |
|
10594 | 203 |
about \isa{m\ -\ n} that is not subject to |
14400 | 204 |
the condition \isa{n\ \isasymle \ m}. |
205 |
\begin{isabelle} |
|
206 |
(m\ -\ n)\ *\ k\ =\ m\ *\ k\ -\ n\ *\ k% |
|
207 |
\rulenamedx{diff_mult_distrib} |
|
208 |
\end{isabelle} |
|
209 |
Natural number subtraction has few |
|
10794 | 210 |
nice properties; often you should remove it by simplifying with this split |
14400 | 211 |
rule. |
10594 | 212 |
\begin{isabelle} |
213 |
P(a-b)\ =\ ((a<b\ \isasymlongrightarrow \ P\ |
|
214 |
0)\ \isasymand \ (\isasymforall d.\ a\ =\ b+d\ \isasymlongrightarrow \ P\ |
|
215 |
d)) |
|
216 |
\rulename{nat_diff_split} |
|
217 |
\end{isabelle} |
|
14400 | 218 |
For example, splitting helps to prove the following fact. |
10594 | 219 |
\begin{isabelle} |
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
220 |
\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
|
221 |
\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
|
222 |
\ 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
|
223 |
\end{isabelle} |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
224 |
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
|
225 |
it is easily found |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
226 |
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
|
227 |
\begin{isabelle} |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
228 |
\isacommand{apply}\ (subgoal_tac\ "n=0\ |\ n=1",\ force,\ arith)\isanewline |
10594 | 229 |
\isacommand{done} |
14400 | 230 |
\end{isabelle}%%%%%% |
11416 | 231 |
\index{natural numbers|)}\index{*nat (type)|)} |
232 |
||
10594 | 233 |
|
11216 | 234 |
\subsection{The Type of Integers, {\tt\slshape int}} |
10594 | 235 |
|
11416 | 236 |
\index{integers|(}\index{*int (type)|(}% |
14400 | 237 |
Reasoning methods for the integers resemble those for the natural numbers, |
21243 | 238 |
but induction and |
239 |
the constant \isa{Suc} are not available. HOL provides many lemmas for |
|
240 |
proving inequalities involving integer multiplication and division, similar |
|
241 |
to those shown above for type~\isa{nat}. The laws of addition, subtraction |
|
242 |
and multiplication are available through the axiomatic type class for rings |
|
31678 | 243 |
(\S\ref{sec:numeric-classes}). |
10794 | 244 |
|
14400 | 245 |
The \rmindex{absolute value} function \cdx{abs} is overloaded, and is |
246 |
defined for all types that involve negative numbers, including the integers. |
|
10881 | 247 |
The \isa{arith} method can prove facts about \isa{abs} automatically, |
248 |
though as it does so by case analysis, the cost can be exponential. |
|
249 |
\begin{isabelle} |
|
11174 | 250 |
\isacommand{lemma}\ "abs\ (x+y)\ \isasymle \ abs\ x\ +\ abs\ (y\ ::\ int)"\isanewline |
10881 | 251 |
\isacommand{by}\ arith |
252 |
\end{isabelle} |
|
10794 | 253 |
|
11416 | 254 |
For division and remainder,\index{division!by negative numbers} |
255 |
the treatment of negative divisors follows |
|
10794 | 256 |
mathematical practice: the sign of the remainder follows that |
10594 | 257 |
of the divisor: |
258 |
\begin{isabelle} |
|
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
259 |
0\ <\ b\ \isasymLongrightarrow \ 0\ \isasymle \ a\ mod\ b% |
10594 | 260 |
\rulename{pos_mod_sign}\isanewline |
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
261 |
0\ <\ b\ \isasymLongrightarrow \ a\ mod\ b\ <\ b% |
10594 | 262 |
\rulename{pos_mod_bound}\isanewline |
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
263 |
b\ <\ 0\ \isasymLongrightarrow \ a\ mod\ b\ \isasymle \ 0 |
10594 | 264 |
\rulename{neg_mod_sign}\isanewline |
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
265 |
b\ <\ 0\ \isasymLongrightarrow \ b\ <\ a\ mod\ b% |
10594 | 266 |
\rulename{neg_mod_bound} |
267 |
\end{isabelle} |
|
268 |
ML treats negative divisors in the same way, but most computer hardware |
|
269 |
treats signed operands using the same rules as for multiplication. |
|
10794 | 270 |
Many facts about quotients and remainders are provided: |
10594 | 271 |
\begin{isabelle} |
272 |
(a\ +\ b)\ div\ c\ =\isanewline |
|
273 |
a\ div\ c\ +\ b\ div\ c\ +\ (a\ mod\ c\ +\ b\ mod\ c)\ div\ c% |
|
274 |
\rulename{zdiv_zadd1_eq} |
|
275 |
\par\smallskip |
|
276 |
(a\ +\ b)\ mod\ c\ =\ (a\ mod\ c\ +\ b\ mod\ c)\ mod\ c% |
|
30224 | 277 |
\rulename{mod_add_eq} |
10594 | 278 |
\end{isabelle} |
279 |
||
280 |
\begin{isabelle} |
|
281 |
(a\ *\ b)\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c% |
|
282 |
\rulename{zdiv_zmult1_eq}\isanewline |
|
283 |
(a\ *\ b)\ mod\ c\ =\ a\ *\ (b\ mod\ c)\ mod\ c% |
|
284 |
\rulename{zmod_zmult1_eq} |
|
285 |
\end{isabelle} |
|
286 |
||
287 |
\begin{isabelle} |
|
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
288 |
0\ <\ c\ \isasymLongrightarrow \ a\ div\ (b*c)\ =\ a\ div\ b\ div\ c% |
10594 | 289 |
\rulename{zdiv_zmult2_eq}\isanewline |
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11494
diff
changeset
|
290 |
0\ <\ c\ \isasymLongrightarrow \ a\ mod\ (b*c)\ =\ b*(a\ div\ b\ mod\ |
10594 | 291 |
c)\ +\ a\ mod\ b% |
292 |
\rulename{zmod_zmult2_eq} |
|
293 |
\end{isabelle} |
|
294 |
The last two differ from their natural number analogues by requiring |
|
295 |
\isa{c} to be positive. Since division by zero yields zero, we could allow |
|
296 |
\isa{c} to be zero. However, \isa{c} cannot be negative: a counterexample |
|
297 |
is |
|
298 |
$\isa{a} = 7$, $\isa{b} = 2$ and $\isa{c} = -3$, when the left-hand side of |
|
14400 | 299 |
\isa{zdiv_zmult2_eq} is $-2$ while the right-hand side is~$-1$. |
300 |
The prefix~\isa{z} in many theorem names recalls the use of $\mathbb{Z}$ to |
|
301 |
denote the set of integers.% |
|
11416 | 302 |
\index{integers|)}\index{*int (type)|)} |
10594 | 303 |
|
13979 | 304 |
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 $<$): |
13750 | 305 |
\begin{isabelle} |
306 |
\isasymlbrakk k\ \isasymle \ i;\ P\ k;\ \isasymAnd i.\ \isasymlbrakk k\ \isasymle \ i;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i+1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i% |
|
307 |
\rulename{int_ge_induct}\isanewline |
|
308 |
\isasymlbrakk k\ <\ i;\ P(k+1);\ \isasymAnd i.\ \isasymlbrakk k\ <\ i;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i+1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i% |
|
309 |
\rulename{int_gr_induct}\isanewline |
|
310 |
\isasymlbrakk i\ \isasymle \ k;\ P\ k;\ \isasymAnd i.\ \isasymlbrakk i\ \isasymle \ k;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i-1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i% |
|
311 |
\rulename{int_le_induct}\isanewline |
|
312 |
\isasymlbrakk i\ <\ k;\ P(k-1);\ \isasymAnd i.\ \isasymlbrakk i\ <\ k;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i-1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i% |
|
313 |
\rulename{int_less_induct} |
|
314 |
\end{isabelle} |
|
315 |
||
10594 | 316 |
|
14400 | 317 |
\subsection{The Types of Rational, Real and Complex Numbers} |
16359 | 318 |
\label{sec:real} |
10594 | 319 |
|
14400 | 320 |
\index{rational numbers|(}\index{*rat (type)|(}% |
11416 | 321 |
\index{real numbers|(}\index{*real (type)|(}% |
14400 | 322 |
\index{complex numbers|(}\index{*complex (type)|(}% |
323 |
These types provide true division, the overloaded operator \isa{/}, |
|
324 |
which differs from the operator \isa{div} of the |
|
325 |
natural numbers and integers. The rationals and reals are |
|
326 |
\textbf{dense}: between every two distinct numbers lies another. |
|
327 |
This property follows from the division laws, since if $x\not=y$ then $(x+y)/2$ lies between them: |
|
10777 | 328 |
\begin{isabelle} |
14400 | 329 |
a\ <\ b\ \isasymLongrightarrow \ \isasymexists r.\ a\ <\ r\ \isasymand \ r\ <\ b% |
14295 | 330 |
\rulename{dense} |
10777 | 331 |
\end{isabelle} |
332 |
||
21243 | 333 |
The real numbers are, moreover, \textbf{complete}: every set of reals that |
334 |
is bounded above has a least upper bound. Completeness distinguishes the |
|
335 |
reals from the rationals, for which the set $\{x\mid x^2<2\}$ has no least |
|
27093 | 336 |
upper bound. (It could only be $\surd2$, which is irrational.) The |
21243 | 337 |
formalization of completeness, which is complicated, |
31678 | 338 |
can be found in theory \texttt{RComplete}. |
14400 | 339 |
|
340 |
Numeric literals\index{numeric literals!for type \protect\isa{real}} |
|
341 |
for type \isa{real} have the same syntax as those for type |
|
342 |
\isa{int} and only express integral values. Fractions expressed |
|
343 |
using the division operator are automatically simplified to lowest terms: |
|
344 |
\begin{isabelle} |
|
345 |
\ 1.\ P\ ((3\ /\ 4)\ *\ (8\ /\ 15))\isanewline |
|
346 |
\isacommand{apply} simp\isanewline |
|
347 |
\ 1.\ P\ (2\ /\ 5) |
|
348 |
\end{isabelle} |
|
349 |
Exponentiation can express floating-point values such as |
|
33761 | 350 |
\isa{2 * 10\isacharcircum6}, which will be simplified to integers. |
14400 | 351 |
|
352 |
\begin{warn} |
|
31678 | 353 |
Types \isa{rat}, \isa{real} and \isa{complex} are provided by theory HOL-Complex, which is |
354 |
Main extended with a definitional development of the rational, real and complex |
|
16359 | 355 |
numbers. Base your theory upon theory \thydx{Complex_Main}, not the |
31678 | 356 |
usual \isa{Main}.% |
14400 | 357 |
\end{warn} |
358 |
||
31678 | 359 |
Available in the logic HOL-NSA is the |
14400 | 360 |
theory \isa{Hyperreal}, which define the type \tydx{hypreal} of |
361 |
\rmindex{non-standard reals}. These |
|
362 |
\textbf{hyperreals} include infinitesimals, which represent infinitely |
|
363 |
small and infinitely large quantities; they facilitate proofs |
|
364 |
about limits, differentiation and integration~\cite{fleuriot-jcm}. The |
|
365 |
development defines an infinitely large number, \isa{omega} and an |
|
366 |
infinitely small positive number, \isa{epsilon}. The |
|
367 |
relation $x\approx y$ means ``$x$ is infinitely close to~$y$.'' |
|
368 |
Theory \isa{Hyperreal} also defines transcendental functions such as sine, |
|
369 |
cosine, exponential and logarithm --- even the versions for type |
|
370 |
\isa{real}, because they are defined using nonstandard limits.% |
|
371 |
\index{rational numbers|)}\index{*rat (type)|)}% |
|
372 |
\index{real numbers|)}\index{*real (type)|)}% |
|
373 |
\index{complex numbers|)}\index{*complex (type)|)} |
|
374 |
||
375 |
||
31678 | 376 |
\subsection{The Numeric Type Classes}\label{sec:numeric-classes} |
14400 | 377 |
|
378 |
Isabelle/HOL organises its numeric theories using axiomatic type classes. |
|
379 |
Hundreds of basic properties are proved in the theory \isa{Ring_and_Field}. |
|
380 |
These lemmas are available (as simprules if they were declared as such) |
|
381 |
for all numeric types satisfying the necessary axioms. The theory defines |
|
23525 | 382 |
dozens of type classes, such as the following: |
14400 | 383 |
\begin{itemize} |
384 |
\item |
|
21243 | 385 |
\tcdx{semiring} and \tcdx{ordered_semiring}: a \emph{semiring} |
23525 | 386 |
provides the associative operators \isa{+} and~\isa{*}, with \isa{0} and~\isa{1} |
387 |
as their respective identities. The operators enjoy the usual distributive law, |
|
388 |
and addition (\isa{+}) is also commutative. |
|
389 |
An \emph{ordered semiring} is also linearly |
|
21243 | 390 |
ordered, with addition and multiplication respecting the ordering. Type \isa{nat} is an ordered semiring. |
14400 | 391 |
\item |
21243 | 392 |
\tcdx{ring} and \tcdx{ordered_ring}: a \emph{ring} extends a semiring |
393 |
with unary minus (the additive inverse) and subtraction (both |
|
394 |
denoted~\isa{-}). An \emph{ordered ring} includes the absolute value |
|
395 |
function, \cdx{abs}. Type \isa{int} is an ordered ring. |
|
14400 | 396 |
\item |
21243 | 397 |
\tcdx{field} and \tcdx{ordered_field}: a field extends a ring with the |
27093 | 398 |
multiplicative inverse (called simply \cdx{inverse} and division~(\isa{/})). |
21243 | 399 |
An ordered field is based on an ordered ring. Type \isa{complex} is a field, while type \isa{real} is an ordered field. |
14400 | 400 |
\item |
401 |
\tcdx{division_by_zero} includes all types where \isa{inverse 0 = 0} |
|
402 |
and \isa{a / 0 = 0}. These include all of Isabelle's standard numeric types. |
|
403 |
However, the basic properties of fields are derived without assuming |
|
21243 | 404 |
division by zero. |
405 |
\end{itemize} |
|
14400 | 406 |
|
23525 | 407 |
Hundreds of basic lemmas are proved, each of which |
21243 | 408 |
holds for all types in the corresponding type class. In most |
23525 | 409 |
cases, it is obvious whether a property is valid for a particular type. No |
410 |
abstract properties involving subtraction hold for type \isa{nat}; |
|
411 |
instead, theorems such as |
|
412 |
\isa{diff_mult_distrib} are proved specifically about subtraction on |
|
21243 | 413 |
type~\isa{nat}. All abstract properties involving division require a field. |
414 |
Obviously, all properties involving orderings required an ordered |
|
415 |
structure. |
|
14400 | 416 |
|
23504 | 417 |
The class \tcdx{ring_no_zero_divisors} of rings without zero divisors satisfies a number of natural cancellation laws, the first of which characterizes this class: |
14400 | 418 |
\begin{isabelle} |
419 |
(a\ *\ b\ =\ (0::'a))\ =\ (a\ =\ (0::'a)\ \isasymor \ b\ =\ (0::'a)) |
|
420 |
\rulename{mult_eq_0_iff}\isanewline |
|
421 |
(a\ *\ c\ =\ b\ *\ c)\ =\ (c\ =\ (0::'a)\ \isasymor \ a\ =\ b) |
|
422 |
\rulename{mult_cancel_right} |
|
423 |
\end{isabelle} |
|
16412 | 424 |
\begin{pgnote} |
16523 | 425 |
Setting the flag \pgmenu{Isabelle} $>$ \pgmenu{Settings} $>$ |
426 |
\pgmenu{Show Sorts} will display the type classes of all type variables. |
|
16412 | 427 |
\end{pgnote} |
428 |
\noindent |
|
23504 | 429 |
Here is how the theorem \isa{mult_cancel_left} appears with the flag set. |
14400 | 430 |
\begin{isabelle} |
23504 | 431 |
((c::'a::ring_no_zero_divisors)\ *\ (a::'a::ring_no_zero_divisors) =\isanewline |
432 |
\ c\ *\ (b::'a::ring_no_zero_divisors))\ =\isanewline |
|
433 |
(c\ =\ (0::'a::ring_no_zero_divisors)\ \isasymor\ a\ =\ b) |
|
14400 | 434 |
\end{isabelle} |
435 |
||
436 |
||
437 |
\subsubsection{Simplifying with the AC-Laws} |
|
438 |
Suppose that two expressions are equal, differing only in |
|
439 |
associativity and commutativity of addition. Simplifying with the |
|
440 |
following equations sorts the terms and groups them to the right, making |
|
441 |
the two expressions identical. |
|
442 |
\begin{isabelle} |
|
443 |
a\ +\ b\ +\ c\ =\ a\ +\ (b\ +\ c) |
|
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
48985
diff
changeset
|
444 |
\rulenamedx{add.assoc}\isanewline |
14400 | 445 |
a\ +\ b\ =\ b\ +\ a% |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
48985
diff
changeset
|
446 |
\rulenamedx{add.commute}\isanewline |
14400 | 447 |
a\ +\ (b\ +\ c)\ =\ b\ +\ (a\ +\ c) |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
48985
diff
changeset
|
448 |
\rulename{add.left_commute} |
14400 | 449 |
\end{isabelle} |
450 |
The name \isa{add_ac}\index{*add_ac (theorems)} |
|
451 |
refers to the list of all three theorems; similarly |
|
452 |
there is \isa{mult_ac}.\index{*mult_ac (theorems)} |
|
453 |
They are all proved for semirings and therefore hold for all numeric types. |
|
454 |
||
455 |
Here is an example of the sorting effect. Start |
|
456 |
with this goal, which involves type \isa{nat}. |
|
457 |
\begin{isabelle} |
|
458 |
\ 1.\ Suc\ (i\ +\ j\ *\ l\ *\ k\ +\ m\ *\ n)\ =\ |
|
459 |
f\ (n\ *\ m\ +\ i\ +\ k\ *\ j\ *\ l) |
|
460 |
\end{isabelle} |
|
461 |
% |
|
462 |
Simplify using \isa{add_ac} and \isa{mult_ac}. |
|
463 |
\begin{isabelle} |
|
464 |
\isacommand{apply}\ (simp\ add:\ add_ac\ mult_ac) |
|
465 |
\end{isabelle} |
|
466 |
% |
|
467 |
Here is the resulting subgoal. |
|
468 |
\begin{isabelle} |
|
469 |
\ 1.\ Suc\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))\ |
|
470 |
=\ f\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))% |
|
471 |
\end{isabelle} |
|
472 |
||
473 |
||
474 |
\subsubsection{Division Laws for Fields} |
|
475 |
||
10777 | 476 |
Here is a selection of rules about the division operator. The following |
477 |
are installed as default simplification rules in order to express |
|
478 |
combinations of products and quotients as rational expressions: |
|
479 |
\begin{isabelle} |
|
14288 | 480 |
a\ *\ (b\ /\ c)\ =\ a\ *\ b\ /\ c |
481 |
\rulename{times_divide_eq_right}\isanewline |
|
482 |
b\ /\ c\ *\ a\ =\ b\ *\ a\ /\ c |
|
483 |
\rulename{times_divide_eq_left}\isanewline |
|
484 |
a\ /\ (b\ /\ c)\ =\ a\ *\ c\ /\ b |
|
485 |
\rulename{divide_divide_eq_right}\isanewline |
|
486 |
a\ /\ b\ /\ c\ =\ a\ /\ (b\ *\ c) |
|
487 |
\rulename{divide_divide_eq_left} |
|
10777 | 488 |
\end{isabelle} |
489 |
||
490 |
Signs are extracted from quotients in the hope that complementary terms can |
|
491 |
then be cancelled: |
|
492 |
\begin{isabelle} |
|
14295 | 493 |
-\ (a\ /\ b)\ =\ -\ a\ /\ b |
494 |
\rulename{minus_divide_left}\isanewline |
|
495 |
-\ (a\ /\ b)\ =\ a\ /\ -\ b |
|
496 |
\rulename{minus_divide_right} |
|
10777 | 497 |
\end{isabelle} |
498 |
||
499 |
The following distributive law is available, but it is not installed as a |
|
500 |
simplification rule. |
|
501 |
\begin{isabelle} |
|
14295 | 502 |
(a\ +\ b)\ /\ c\ =\ a\ /\ c\ +\ b\ /\ c% |
503 |
\rulename{add_divide_distrib} |
|
10777 | 504 |
\end{isabelle} |
505 |
||
14400 | 506 |
|
507 |
\subsubsection{Absolute Value} |
|
10594 | 508 |
|
14400 | 509 |
The \rmindex{absolute value} function \cdx{abs} is available for all |
510 |
ordered rings, including types \isa{int}, \isa{rat} and \isa{real}. |
|
511 |
It satisfies many properties, |
|
512 |
such as the following: |
|
10777 | 513 |
\begin{isabelle} |
14400 | 514 |
\isasymbar x\ *\ y\isasymbar \ =\ \isasymbar x\isasymbar \ *\ \isasymbar y\isasymbar |
515 |
\rulename{abs_mult}\isanewline |
|
516 |
(\isasymbar a\isasymbar \ \isasymle \ b)\ =\ (a\ \isasymle \ b\ \isasymand \ -\ a\ \isasymle \ b) |
|
517 |
\rulename{abs_le_iff}\isanewline |
|
518 |
\isasymbar a\ +\ b\isasymbar \ \isasymle \ \isasymbar a\isasymbar \ +\ \isasymbar b\isasymbar |
|
519 |
\rulename{abs_triangle_ineq} |
|
10777 | 520 |
\end{isabelle} |
521 |
||
14400 | 522 |
\begin{warn} |
523 |
The absolute value bars shown above cannot be typed on a keyboard. They |
|
524 |
can be entered using the X-symbol package. In \textsc{ascii}, type \isa{abs x} to |
|
525 |
get \isa{\isasymbar x\isasymbar}. |
|
526 |
\end{warn} |
|
11174 | 527 |
|
528 |
||
14400 | 529 |
\subsubsection{Raising to a Power} |
10777 | 530 |
|
31682 | 531 |
Another type class, \tcdx{ordered\_idom}, specifies rings that also have |
14400 | 532 |
exponentation to a natural number power, defined using the obvious primitive |
533 |
recursion. Theory \thydx{Power} proves various theorems, such as the |
|
534 |
following. |
|
535 |
\begin{isabelle} |
|
536 |
a\ \isacharcircum \ (m\ +\ n)\ =\ a\ \isacharcircum \ m\ *\ a\ \isacharcircum \ n% |
|
537 |
\rulename{power_add}\isanewline |
|
538 |
a\ \isacharcircum \ (m\ *\ n)\ =\ (a\ \isacharcircum \ m)\ \isacharcircum \ n% |
|
539 |
\rulename{power_mult}\isanewline |
|
540 |
\isasymbar a\ \isacharcircum \ n\isasymbar \ =\ \isasymbar a\isasymbar \ \isacharcircum \ n% |
|
541 |
\rulename{power_abs} |
|
542 |
\end{isabelle}%%%%%%%%%%%%%%%%%%%%%%%%% |
|
13996 | 543 |
\index{numbers|)} |