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

doc-src/TutorialI/Types/numerics.tex

author | paulson |

Mon Nov 12 10:56:38 2001 +0100 (2001-11-12) | |

changeset 12156 | d2758965362e |

parent 11494 | 23a118849801 |

child 12333 | ef43a3d6e962 |

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

new-style numerals without leading #, along with generic 0 and 1

1 % $Id$

3 \section{Numbers}

4 \label{sec:numbers}

6 \index{numbers|(}%

7 Until now, our numerical examples have used the type of \textbf{natural

8 numbers},

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

11 recursive function definitions. HOL also provides the type

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

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.

23 \index{linear arithmetic}%

24 Many theorems involving numeric types can be proved automatically by

25 Isabelle's arithmetic decision procedure, the method

26 \methdx{arith}. Linear arithmetic comprises addition, subtraction

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.

32 The simplifier reduces arithmetic expressions in other

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

34 outside the scope of automation, HOL provides hundreds of

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

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

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

38 is available.

40 \subsection{Numeric Literals}

41 \label{sec:numerals}

43 \index{numeric literals|(}%

44 The constants \cdx{0} and \cdx{1} are overloaded. They denote zero and one,

45 respectively, for all numeric types. Other values are expressed by numeric

46 literals, which consist of one or more decimal digits optionally preceeded by

47 a minus sign (\isa{-}). Examples are \isa{2}, \isa{-3} and

48 \isa{441223334678}. Literals are available for the types of natural numbers,

49 integers and reals; they denote integer values of arbitrary size.

51 Literals look like constants, but they abbreviate

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

53 Isabelle performs arithmetic on literals by rewriting rather

54 than using the hardware arithmetic. In most cases arithmetic

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

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.

60 \begin{warn}\index{overloading!and arithmetic}

61 The arithmetic operators are

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:

65 \par

66 \begin{isabelle}

67 \isacommand{lemma}\ "2\ *\ m\ =\ m\ +\ m"

68 \end{isabelle}

69 %

70 Carefully observe how Isabelle displays the subgoal:

71 \begin{isabelle}

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

73 \end{isabelle}

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

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.

77 \end{warn}

79 \begin{warn}

80 \index{recdef@\isacommand {recdef} (command)!and numeric literals}

81 Numeric literals are not constructors and therefore

82 must not be used in patterns. For example, this declaration is

83 rejected:

84 \begin{isabelle}

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

86 "h\ 3\ =\ 2"\isanewline

87 "h\ i\ \ =\ i"

88 \end{isabelle}

90 You should use a conditional expression instead:

91 \begin{isabelle}

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

93 \end{isabelle}

94 \index{numeric literals|)}

95 \end{warn}

99 \subsection{The Type of Natural Numbers, {\tt\slshape nat}}

101 \index{natural numbers|(}\index{*nat (type)|(}%

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

103 beginning. Hundreds of theorems about the natural numbers are

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

105 in exceptional circumstances should you resort to induction.

107 \subsubsection{Literals}

108 \index{numeric literals!for type \protect\isa{nat}}%

109 The notational options for the natural numbers are confusing. Recall that an

110 overloaded constant can be defined independently for each type; the definition

111 of \cdx{1} for type \isa{nat} is

112 \begin{isabelle}

113 1\ \isasymequiv\ Suc\ 0

114 \rulename{One_nat_def}

115 \end{isabelle}

116 This is installed as a simplification rule, so the simplifier will replace

117 every occurrence of \isa{1::nat} by \isa{Suc\ 0}. Literals are obviously

118 better than nested \isa{Suc}s at expressing large values. But many theorems,

119 including the rewrite rules for primitive recursive functions, can only be

120 applied to terms of the form \isa{Suc\ $n$}.

122 The following default simplification rules replace

123 small literals by zero and successor:

124 \begin{isabelle}

125 2\ +\ n\ =\ Suc\ (Suc\ n)

126 \rulename{add_2_eq_Suc}\isanewline

127 n\ +\ 2\ =\ Suc\ (Suc\ n)

128 \rulename{add_2_eq_Suc'}

129 \end{isabelle}

130 It is less easy to transform \isa{100} into \isa{Suc\ 99} (for example), and

131 the simplifier will normally reverse this transformation. Novices should

132 express natural numbers using \isa{0} and \isa{Suc} only.

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%

151 \rulenamedx{add_mult_distrib}\isanewline

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

153 \rulenamedx{diff_mult_distrib}\isanewline

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

155 \rulenamedx{mod_mult_distrib}

156 \end{isabelle}

158 \subsubsection{Division}

159 \index{division!for type \protect\isa{nat}}%

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:

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%

167 \rulenamedx{mod_div_equality}

168 \end{isabelle}

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}

185 Surprisingly few of these results depend upon the

186 divisors' being nonzero.

187 \index{division!by zero}%

188 That is because division by

189 zero yields zero:

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

197 simplification rules. In \isa{div_mult_mult1} above, one of

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

200 The \textbf{divides} relation\index{divides relation}

201 has the standard definition, which

202 is overloaded over all numeric types:

203 \begin{isabelle}

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

205 \rulenamedx{dvd_def}

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%

212 \rulenamedx{dvd_anti_sym}\isanewline

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

214 \rulenamedx{dvd_add}

215 \end{isabelle}

217 \subsubsection{Simplifier Tricks}

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

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

222 rule:

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}

229 For example, splitting helps to prove the following fact:

230 \begin{isabelle}

231 \isacommand{lemma}\ "(n\ -\ 2)\ *\ (n\ +\ 2)\ =\ n\ *\ n\ -\ (4::nat)"\isanewline

232 \isacommand{apply}\ (simp\ split:\ nat_diff_split,\ clarify)\isanewline

233 \ 1.\ \isasymAnd d.\ \isasymlbrakk n\ <\ 2;\ n\ *\ n\ =\ 4\ +\ d\isasymrbrakk \ \isasymLongrightarrow \ d\ =\ 0

234 \end{isabelle}

235 The result lies outside the scope of linear arithmetic, but

236 it is easily found

237 if we explicitly split \isa{n<2} as \isa{n=0} or \isa{n=1}:

238 \begin{isabelle}

239 \isacommand{apply}\ (subgoal_tac\ "n=0\ |\ n=1",\ force,\ arith)\isanewline

240 \isacommand{done}

241 \end{isabelle}

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)

249 \rulenamedx{add_assoc}\isanewline

250 m\ +\ n\ =\ n\ +\ m%

251 \rulenamedx{add_commute}\isanewline

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

253 +\ z)

254 \rulename{add_left_commute}

255 \end{isabelle}

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

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)))%

275 \end{isabelle}%

276 \index{natural numbers|)}\index{*nat (type)|)}

280 \subsection{The Type of Integers, {\tt\slshape int}}

282 \index{integers|(}\index{*int (type)|(}%

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

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

285 for proving inequalities involving integer multiplication and division,

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

288 The \rmindex{absolute value} function \cdx{abs} is overloaded for the numeric types.

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}

295 \begin{warn}

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

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

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

299 \end{warn}

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}

304 \isacommand{lemma}\ "abs\ (x+y)\ \isasymle \ abs\ x\ +\ abs\ (y\ ::\ int)"\isanewline

305 \isacommand{by}\ arith

306 \end{isabelle}

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

310 operands of sums and products. The name \isa{zadd_ac}\index{*zadd_ac (theorems)}

311 refers to the

312 associativity and commutativity theorems for integer addition, while

313 \isa{zmult_ac}\index{*zmult_ac (theorems)}

314 has the analogous theorems for multiplication. The

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

316 denote the set of integers.

318 For division and remainder,\index{division!by negative numbers}

319 the treatment of negative divisors follows

320 mathematical practice: the sign of the remainder follows that

321 of the divisor:

322 \begin{isabelle}

323 0\ <\ b\ \isasymLongrightarrow \ 0\ \isasymle \ a\ mod\ b%

324 \rulename{pos_mod_sign}\isanewline

325 0\ <\ b\ \isasymLongrightarrow \ a\ mod\ b\ <\ b%

326 \rulename{pos_mod_bound}\isanewline

327 b\ <\ 0\ \isasymLongrightarrow \ a\ mod\ b\ \isasymle \ 0

328 \rulename{neg_mod_sign}\isanewline

329 b\ <\ 0\ \isasymLongrightarrow \ b\ <\ a\ mod\ b%

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.

334 Many facts about quotients and remainders are provided:

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}

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}

351 \begin{isabelle}

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

353 \rulename{zdiv_zmult2_eq}\isanewline

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

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

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

364 \index{integers|)}\index{*int (type)|)}

367 \subsection{The Type of Real Numbers, {\tt\slshape real}}

369 \index{real numbers|(}\index{*real (type)|(}%

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.)

379 The formalization of completeness is complicated; rather than

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

381 directory \texttt{Real}.

382 Density, however, is trivial to express:

383 \begin{isabelle}

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

385 \rulename{real_dense}

386 \end{isabelle}

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}

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

393 \rulename{real_times_divide1_eq}\isanewline

394 y\ /\ z\ *\ x\ =\ y\ *\ x\ /\ z

395 \rulename{real_times_divide2_eq}\isanewline

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

397 \rulename{real_divide_divide1_eq}\isanewline

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

399 \rulename{real_divide_divide2_eq}

400 \end{isabelle}

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}

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}

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

420 associativity and commutativity theorems for addition, while similarly

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

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}

427 \isasymbar r\isasymbar \ \isacharcircum \ n\ =\ \isasymbar r\ \isacharcircum \ n\isasymbar

428 \rulename{realpow_abs}

429 \end{isabelle}

431 Numeric literals\index{numeric literals!for type \protect\isa{real}}

432 for type \isa{real} have the same syntax as those for type

433 \isa{int} and only express integral values. Fractions expressed

434 using the division operator are automatically simplified to lowest terms:

435 \begin{isabelle}

436 \ 1.\ P\ ((3\ /\ 4)\ *\ (8\ /\ 15))\isanewline

437 \isacommand{apply} simp\isanewline

438 \ 1.\ P\ (2\ /\ 5)

439 \end{isabelle}

440 Exponentiation can express floating-point values such as

441 \isa{2 * 10\isacharcircum6}, but at present no special simplification

442 is performed.

445 \begin{warn}

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

447 is HOL extended with a definitional development of the real

448 numbers. Base your theory upon theory

449 \thydx{Real}, not the usual \isa{Main}.%

450 \index{real numbers|)}\index{*real (type)|)}

451 Launch Isabelle using the command

452 \begin{verbatim}

453 Isabelle -l HOL-Real

454 \end{verbatim}

455 \end{warn}

457 Also distributed with Isabelle is HOL-Hyperreal,

458 whose theory \isa{Hyperreal} defines the type \tydx{hypreal} of

459 \rmindex{non-standard reals}. These

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

461 small and infinitely large quantities; they facilitate proofs

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

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

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

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

466 \index{numbers|)}