summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

doc-src/TutorialI/Types/numerics.tex

author | nipkow |

Thu Jan 25 15:31:31 2001 +0100 (2001-01-25) | |

changeset 10978 | 5eebea8f359f |

parent 10881 | 03f06372230b |

child 10983 | 59961d32b1ae |

permissions | -rw-r--r-- |

*** empty log message ***

1 % $Id$

2 Until now, our numerical have used the type of \textbf{natural numbers},

3 \isa{nat}. This is a recursive datatype generated by the constructors

4 zero and successor, so it works well with inductive proofs and primitive

5 recursive function definitions. Isabelle/HOL also provides the type

6 \isa{int} of \textbf{integers}, which lack induction but support true

7 subtraction. The logic HOL-Real also has the type \isa{real} of real

8 numbers. Isabelle has no subtyping, so the numeric types are distinct and

9 there are functions to convert between them. Fortunately most numeric

10 operations are overloaded: the same symbol can be used at all numeric types.

11 Table~\ref{tab:overloading} in the appendix shows the most important operations,

12 together with the priorities of the infix symbols.

14 The integers are preferable to the natural numbers for reasoning about

15 complicated arithmetic expressions. For example, a termination proof

16 typically involves an integer metric that is shown to decrease at each

17 loop iteration. Even if the metric cannot become negative, proofs

18 may be easier if you use the integers instead of the natural

19 numbers.

21 Many theorems involving numeric types can be proved automatically by

22 Isabelle's arithmetic decision procedure, the method

23 \isa{arith}. Linear arithmetic comprises addition, subtraction

24 and multiplication by constant factors; subterms involving other operators

25 are regarded as variables. The procedure can be slow, especially if the

26 subgoal to be proved involves subtraction over type \isa{nat}, which

27 causes case splits.

29 The simplifier reduces arithmetic expressions in other

30 ways, such as dividing through by common factors. For problems that lie

31 outside the scope of automation, HOL provides hundreds of

32 theorems about multiplication, division, etc., that can be brought to

33 bear. You can locate them using Proof General's Find

34 button. A few lemmas are given below to show what

35 is available.

37 \subsection{Numeric Literals}

38 \label{sec:numerals}

40 Literals are available for the types of natural numbers, integers

41 and reals and denote integer values of arbitrary size.

42 They begin

43 with a number sign (\isa{\#}), have an optional minus sign (\isa{-}) and

44 then one or more decimal digits. Examples are \isa{\#0}, \isa{\#-3}

45 and \isa{\#441223334678}.

47 Literals look like constants, but they abbreviate

48 terms, representing the number in a two's complement binary notation.

49 Isabelle performs arithmetic on literals by rewriting rather

50 than using the hardware arithmetic. In most cases arithmetic

51 is fast enough, even for large numbers. The arithmetic operations

52 provided for literals include addition, subtraction, multiplication,

53 integer division and remainder. Fractions of literals (expressed using

54 division) are reduced to lowest terms.

56 \begin{warn}

57 The arithmetic operators are

58 overloaded, so you must be careful to ensure that each numeric

59 expression refers to a specific type, if necessary by inserting

60 type constraints. Here is an example of what can go wrong:

61 \par

62 \begin{isabelle}

63 \isacommand{lemma}\ "\#2\ *\ m\ =\ m\ +\ m"

64 \end{isabelle}

65 %

66 Carefully observe how Isabelle displays the subgoal:

67 \begin{isabelle}

68 \ 1.\ (\#2::'a)\ *\ m\ =\ m\ +\ m

69 \end{isabelle}

70 The type \isa{'a} given for the literal \isa{\#2} warns us that no numeric

71 type has been specified. The problem is underspecified. Given a type

72 constraint such as \isa{nat}, \isa{int} or \isa{real}, it becomes trivial.

73 \end{warn}

75 \begin{warn}

76 Numeric literals are not constructors and therefore must not be used in

77 patterns. For example, this declaration is rejected:

78 \begin{isabelle}

79 \isacommand{recdef}\ h\ "\isacharbraceleft \isacharbraceright "\isanewline

80 h\ \#3\ =\ \#2\isanewline

81 h\ i\ \ =\ i

82 \end{isabelle}

84 You should use a conditional expression instead:

85 \begin{isabelle}

86 "h\ i\ =\ (if\ i\ =\ \#3\ then\ \#2\ else\ i)"

87 \end{isabelle}

88 \end{warn}

92 \subsection{The type of natural numbers, {\tt\slshape nat}}

94 This type requires no introduction: we have been using it from the

95 beginning. Hundreds of theorems about the natural numbers are

96 proved in the theories \isa{Nat}, \isa{NatArith} and \isa{Divides}. Only

97 in exceptional circumstances should you resort to induction.

99 \subsubsection{Literals}

100 The notational options for the natural numbers can be confusing. The

101 constant \isa{0} is overloaded to serve as the neutral value

102 in a variety of additive types. The symbols \isa{1} and \isa{2} are

103 not constants but abbreviations for \isa{Suc 0} and \isa{Suc(Suc 0)},

104 respectively. The literals \isa{\#0}, \isa{\#1} and \isa{\#2} are

105 syntactically different from \isa{0}, \isa{1} and \isa{2}. You will

106 sometimes prefer one notation to the other. Literals are obviously

107 necessary to express large values, while \isa{0} and \isa{Suc} are needed

108 in order to match many theorems, including the rewrite rules for primitive

109 recursive functions. The following default simplification rules replace

110 small literals by zero and successor:

111 \begin{isabelle}

112 \#0\ =\ 0

113 \rulename{numeral_0_eq_0}\isanewline

114 \#1\ =\ 1

115 \rulename{numeral_1_eq_1}\isanewline

116 \#2\ +\ n\ =\ Suc\ (Suc\ n)

117 \rulename{add_2_eq_Suc}\isanewline

118 n\ +\ \#2\ =\ Suc\ (Suc\ n)

119 \rulename{add_2_eq_Suc'}

120 \end{isabelle}

121 In special circumstances, you may wish to remove or reorient

122 these rules.

124 \subsubsection{Typical lemmas}

125 Inequalities involving addition and subtraction alone can be proved

126 automatically. Lemmas such as these can be used to prove inequalities

127 involving multiplication and division:

128 \begin{isabelle}

129 \isasymlbrakk i\ \isasymle \ j;\ k\ \isasymle \ l\isasymrbrakk \ \isasymLongrightarrow \ i\ *\ k\ \isasymle \ j\ *\ l%

130 \rulename{mult_le_mono}\isanewline

131 \isasymlbrakk i\ <\ j;\ 0\ <\ k\isasymrbrakk \ \isasymLongrightarrow \ i\

132 *\ k\ <\ j\ *\ k%

133 \rulename{mult_less_mono1}\isanewline

134 m\ \isasymle \ n\ \isasymLongrightarrow \ m\ div\ k\ \isasymle \ n\ div\ k%

135 \rulename{div_le_mono}

136 \end{isabelle}

137 %

138 Various distributive laws concerning multiplication are available:

139 \begin{isabelle}

140 (m\ +\ n)\ *\ k\ =\ m\ *\ k\ +\ n\ *\ k%

141 \rulename{add_mult_distrib}\isanewline

142 (m\ -\ n)\ *\ k\ =\ m\ *\ k\ -\ n\ *\ k%

143 \rulename{diff_mult_distrib}\isanewline

144 (m\ mod\ n)\ *\ k\ =\ (m\ *\ k)\ mod\ (n\ *\ k)

145 \rulename{mod_mult_distrib}

146 \end{isabelle}

148 \subsubsection{Division}

149 The infix operators \isa{div} and \isa{mod} are overloaded.

150 Isabelle/HOL provides the basic facts about quotient and remainder

151 on the natural numbers:

152 \begin{isabelle}

153 m\ mod\ n\ =\ (if\ m\ <\ n\ then\ m\ else\ (m\ -\ n)\ mod\ n)

154 \rulename{mod_if}\isanewline

155 m\ div\ n\ *\ n\ +\ m\ mod\ n\ =\ m%

156 \rulename{mod_div_equality}

157 \end{isabelle}

159 Many less obvious facts about quotient and remainder are also provided.

160 Here is a selection:

161 \begin{isabelle}

162 a\ *\ b\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c%

163 \rulename{div_mult1_eq}\isanewline

164 a\ *\ b\ mod\ c\ =\ a\ *\ (b\ mod\ c)\ mod\ c%

165 \rulename{mod_mult1_eq}\isanewline

166 a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%

167 \rulename{div_mult2_eq}\isanewline

168 a\ mod\ (b*c)\ =\ b * (a\ div\ b\ mod\ c)\ +\ a\ mod\ b%

169 \rulename{mod_mult2_eq}\isanewline

170 0\ <\ c\ \isasymLongrightarrow \ (c\ *\ a)\ div\ (c\ *\ b)\ =\ a\ div\ b%

171 \rulename{div_mult_mult1}

172 \end{isabelle}

174 Surprisingly few of these results depend upon the

175 divisors' being nonzero. That is because division by

176 zero yields zero:

177 \begin{isabelle}

178 a\ div\ 0\ =\ 0

179 \rulename{DIVISION_BY_ZERO_DIV}\isanewline

180 a\ mod\ 0\ =\ a%

181 \rulename{DIVISION_BY_ZERO_MOD}

182 \end{isabelle}

183 As a concession to convention, these equations are not installed as default

184 simplification rules but are merely used to remove nonzero-divisor

185 hypotheses by case analysis. In \isa{div_mult_mult1} above, one of

186 the two divisors (namely~\isa{c}) must be still be nonzero.

188 The \textbf{divides} relation has the standard definition, which

189 is overloaded over all numeric types:

190 \begin{isabelle}

191 m\ dvd\ n\ \isasymequiv\ {\isasymexists}k.\ n\ =\ m\ *\ k

192 \rulename{dvd_def}

193 \end{isabelle}

194 %

195 Section~\ref{sec:proving-euclid} discusses proofs involving this

196 relation. Here are some of the facts proved about it:

197 \begin{isabelle}

198 \isasymlbrakk m\ dvd\ n;\ n\ dvd\ m\isasymrbrakk \ \isasymLongrightarrow \ m\ =\ n%

199 \rulename{dvd_anti_sym}\isanewline

200 \isasymlbrakk k\ dvd\ m;\ k\ dvd\ n\isasymrbrakk \ \isasymLongrightarrow \ k\ dvd\ (m\ +\ n)

201 \rulename{dvd_add}

202 \end{isabelle}

204 \subsubsection{Simplifier tricks}

205 The rule \isa{diff_mult_distrib} shown above is one of the few facts

206 about \isa{m\ -\ n} that is not subject to

207 the condition \isa{n\ \isasymle \ m}. Natural number subtraction has few

208 nice properties; often you should remove it by simplifying with this split

209 rule:

210 \begin{isabelle}

211 P(a-b)\ =\ ((a<b\ \isasymlongrightarrow \ P\

212 0)\ \isasymand \ (\isasymforall d.\ a\ =\ b+d\ \isasymlongrightarrow \ P\

213 d))

214 \rulename{nat_diff_split}

215 \end{isabelle}

216 For example, it proves the following fact, which lies outside the scope of

217 linear arithmetic:

218 \begin{isabelle}

219 \isacommand{lemma}\ "(n-1)*(n+1)\ =\ n*n\ -\ 1"\isanewline

220 \isacommand{apply}\ (simp\ split:\ nat_diff_split)\isanewline

221 \isacommand{done}

222 \end{isabelle}

224 Suppose that two expressions are equal, differing only in

225 associativity and commutativity of addition. Simplifying with the

226 following equations sorts the terms and groups them to the right, making

227 the two expressions identical:

228 \begin{isabelle}

229 m\ +\ n\ +\ k\ =\ m\ +\ (n\ +\ k)

230 \rulename{add_assoc}\isanewline

231 m\ +\ n\ =\ n\ +\ m%

232 \rulename{add_commute}\isanewline

233 x\ +\ (y\ +\ z)\ =\ y\ +\ (x\

234 +\ z)

235 \rulename{add_left_commute}

236 \end{isabelle}

237 The name \isa{add_ac} refers to the list of all three theorems, similarly

238 there is \isa{mult_ac}. Here is an example of the sorting effect. Start

239 with this goal:

240 \begin{isabelle}

241 \ 1.\ Suc\ (i\ +\ j\ *\ l\ *\ k\ +\ m\ *\ n)\ =\

242 f\ (n\ *\ m\ +\ i\ +\ k\ *\ j\ *\ l)

243 \end{isabelle}

244 %

245 Simplify using \isa{add_ac} and \isa{mult_ac}:

246 \begin{isabelle}

247 \isacommand{apply}\ (simp\ add:\ add_ac\ mult_ac)

248 \end{isabelle}

249 %

250 Here is the resulting subgoal:

251 \begin{isabelle}

252 \ 1.\ Suc\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))\

253 =\ f\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))%

254 \end{isabelle}

257 \subsection{The type of integers, {\tt\slshape int}}

259 Reasoning methods resemble those for the natural numbers, but induction and

260 the constant \isa{Suc} are not available. HOL provides many lemmas

261 for proving inequalities involving integer multiplication and division,

262 similar to those shown above for type~\isa{nat}.

264 The absolute value function \isa{abs} is overloaded for the numeric types.

265 It is defined for the integers; we have for example the obvious law

266 \begin{isabelle}

267 \isasymbar x\ *\ y\isasymbar \ =\ \isasymbar x\isasymbar \ *\ \isasymbar y\isasymbar

268 \rulename{abs_mult}

269 \end{isabelle}

271 \begin{warn}

272 The absolute value bars shown above cannot be typed on a keyboard. They

273 can be entered using the X-symbol package. In ASCII, type \isa{abs x} to

274 get \isa{\isasymbar x\isasymbar}.

275 \end{warn}

277 The \isa{arith} method can prove facts about \isa{abs} automatically,

278 though as it does so by case analysis, the cost can be exponential.

279 \begin{isabelle}

280 \isacommand{lemma}\ "\isasymlbrakk abs\ x\ <\ a;\ abs\ y\ <\ b\isasymrbrakk \ \isasymLongrightarrow \ abs\ x\ +\ abs\ y\ <\ (a\ +\ b\ ::\ int)"\isanewline

281 \isacommand{by}\ arith

282 \end{isabelle}

284 Concerning simplifier tricks, we have no need to eliminate subtraction: it

285 is well-behaved. As with the natural numbers, the simplifier can sort the

286 operands of sums and products. The name \isa{zadd_ac} refers to the

287 associativity and commutativity theorems for integer addition, while

288 \isa{zmult_ac} has the analogous theorems for multiplication. The

289 prefix~\isa{z} in many theorem names recalls the use of $\mathbb{Z}$ to

290 denote the set of integers.

292 For division and remainder, the treatment of negative divisors follows

293 mathematical practice: the sign of the remainder follows that

294 of the divisor:

295 \begin{isabelle}

296 \#0\ <\ b\ \isasymLongrightarrow \ \#0\ \isasymle \ a\ mod\ b%

297 \rulename{pos_mod_sign}\isanewline

298 \#0\ <\ b\ \isasymLongrightarrow \ a\ mod\ b\ <\ b%

299 \rulename{pos_mod_bound}\isanewline

300 b\ <\ \#0\ \isasymLongrightarrow \ a\ mod\ b\ \isasymle \ \#0

301 \rulename{neg_mod_sign}\isanewline

302 b\ <\ \#0\ \isasymLongrightarrow \ b\ <\ a\ mod\ b%

303 \rulename{neg_mod_bound}

304 \end{isabelle}

305 ML treats negative divisors in the same way, but most computer hardware

306 treats signed operands using the same rules as for multiplication.

307 Many facts about quotients and remainders are provided:

308 \begin{isabelle}

309 (a\ +\ b)\ div\ c\ =\isanewline

310 a\ div\ c\ +\ b\ div\ c\ +\ (a\ mod\ c\ +\ b\ mod\ c)\ div\ c%

311 \rulename{zdiv_zadd1_eq}

312 \par\smallskip

313 (a\ +\ b)\ mod\ c\ =\ (a\ mod\ c\ +\ b\ mod\ c)\ mod\ c%

314 \rulename{zmod_zadd1_eq}

315 \end{isabelle}

317 \begin{isabelle}

318 (a\ *\ b)\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c%

319 \rulename{zdiv_zmult1_eq}\isanewline

320 (a\ *\ b)\ mod\ c\ =\ a\ *\ (b\ mod\ c)\ mod\ c%

321 \rulename{zmod_zmult1_eq}

322 \end{isabelle}

324 \begin{isabelle}

325 \#0\ <\ c\ \isasymLongrightarrow \ a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%

326 \rulename{zdiv_zmult2_eq}\isanewline

327 \#0\ <\ c\ \isasymLongrightarrow \ a\ mod\ (b*c)\ =\ b*(a\ div\ b\ mod\

328 c)\ +\ a\ mod\ b%

329 \rulename{zmod_zmult2_eq}

330 \end{isabelle}

331 The last two differ from their natural number analogues by requiring

332 \isa{c} to be positive. Since division by zero yields zero, we could allow

333 \isa{c} to be zero. However, \isa{c} cannot be negative: a counterexample

334 is

335 $\isa{a} = 7$, $\isa{b} = 2$ and $\isa{c} = -3$, when the left-hand side of

336 \isa{zdiv_zmult2_eq} is $-2$ while the right-hand side is~$-1$.

339 \subsection{The type of real numbers, {\tt\slshape real}}

341 The real numbers enjoy two significant properties that the integers lack.

342 They are

343 \textbf{dense}: between every two distinct real numbers there lies another.

344 This property follows from the division laws, since if $x<y$ then between

345 them lies $(x+y)/2$. The second property is that they are

346 \textbf{complete}: every set of reals that is bounded above has a least

347 upper bound. Completeness distinguishes the reals from the rationals, for

348 which the set $\{x\mid x^2<2\}$ has no least upper bound. (It could only be

349 $\surd2$, which is irrational.)

350 The formalization of completeness is complicated; rather than

351 reproducing it here, we refer you to the theory \texttt{RComplete} in

352 directory \texttt{Real}.

353 Density, however, is trivial to express:

354 \begin{isabelle}

355 x\ <\ y\ \isasymLongrightarrow \ \isasymexists r.\ x\ <\ r\ \isasymand \ r\ <\ y%

356 \rulename{real_dense}

357 \end{isabelle}

359 Here is a selection of rules about the division operator. The following

360 are installed as default simplification rules in order to express

361 combinations of products and quotients as rational expressions:

362 \begin{isabelle}

363 x\ *\ (y\ /\ z)\ =\ x\ *\ y\ /\ z%

364 \rulename{real_times_divide1_eq}\isanewline

365 y\ /\ z\ *\ x\ =\ y\ *\ x\ /\ z%

366 \rulename{real_times_divide2_eq}\isanewline

367 x\ /\ (y\ /\ z)\ =\ x\ *\ z\ /\ y%

368 \rulename{real_divide_divide1_eq}\isanewline

369 x\ /\ y\ /\ z\ =\ x\ /\ (y\ *\ z)

370 \rulename{real_divide_divide2_eq}

371 \end{isabelle}

373 Signs are extracted from quotients in the hope that complementary terms can

374 then be cancelled:

375 \begin{isabelle}

376 -\ x\ /\ y\ =\ -\ (x\ /\ y)

377 \rulename{real_minus_divide_eq}\isanewline

378 x\ /\ -\ y\ =\ -\ (x\ /\ y)

379 \rulename{real_divide_minus_eq}

380 \end{isabelle}

382 The following distributive law is available, but it is not installed as a

383 simplification rule.

384 \begin{isabelle}

385 (x\ +\ y)\ /\ z\ =\ x\ /\ z\ +\ y\ /\ z%

386 \rulename{real_add_divide_distrib}

387 \end{isabelle}

389 As with the other numeric types, the simplifier can sort the operands of

390 addition and multiplication. The name \isa{real_add_ac} refers to the

391 associativity and commutativity theorems for addition, while similarly

392 \isa{real_mult_ac} contains those properties for multiplication.

394 The absolute value function \isa{abs} is

395 defined for the reals, along with many theorems such as this one about

396 exponentiation:

397 \begin{isabelle}

398 \isasymbar r\isasymbar \ \isacharcircum \ n\ =\ \isasymbar r\ \isacharcircum \ n\isasymbar

399 \rulename{realpow_abs}

400 \end{isabelle}

402 \begin{warn}

403 Type \isa{real} is only available in the logic HOL-Real, which

404 is HOL extended with the rather substantial development of the real

405 numbers. Base your theory upon theory \isa{Real}, not the usual \isa{Main}.

406 \end{warn}

408 Also distributed with Isabelle is HOL-Hyperreal,

409 whose theory \isa{Hyperreal} defines the type \isa{hypreal} of non-standard

410 reals. These

411 \textbf{hyperreals} include infinitesimals, which represent infinitely

412 small and infinitely large quantities; they facilitate proofs

413 about limits, differentiation and integration~\cite{fleuriot-jcm}. The

414 development defines an infinitely large number, \isa{omega} and an

415 infinitely small positive number, \isa{epsilon}. The

416 relation $x\approx y$ means ``$x$ is infinitely close to~$y$''.