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