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

doc-src/TutorialI/Types/numerics.tex

author | nipkow |

Wed Dec 06 13:22:58 2000 +0100 (2000-12-06) | |

changeset 10608 | 620647438780 |

parent 10594 | 6330bc4b6fe4 |

child 10654 | 458068404143 |

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

*** empty log message ***

1 Our examples until now have used the type of \textbf{natural numbers},

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

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

4 recursive function definitions. Isabelle/HOL also has the type \isa{int}

5 of \textbf{integers}, which gives up induction in exchange for proper subtraction.

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

8 complicated arithmetic expressions. For example, a termination proof

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

10 loop iteration. Even if the metric cannot become negative, proofs about it

11 are usually easier if the integers are used rather than the natural

12 numbers.

14 The logic Isabelle/HOL-Real also has the type \isa{real} of real numbers

15 and even the type \isa{hypreal} of non-standard reals. These

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

17 small and infinitely large quantities; they greatly facilitate proofs

18 about limits, differentiation and integration. Isabelle has no subtyping,

19 so the numeric types are distinct and there are

20 functions to convert between them.

22 Many theorems involving numeric types can be proved automatically by

23 Isabelle's arithmetic decision procedure, the method

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

25 and multiplication by constant factors; subterms involving other operators

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

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

28 causes case splits.

30 The simplifier reduces arithmetic expressions in other

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

32 outside the scope of automation, the library has hundreds of

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

34 bear. You can find find them by browsing the library. Some

35 useful lemmas are shown below.

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 \REMARK{hypreal?}

43 They begin

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

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

46 and \isa{\#441223334678}.

48 Literals look like constants, but they abbreviate

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

50 Isabelle performs arithmetic on literals by rewriting, rather

51 than using the hardware arithmetic. In most cases arithmetic

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

53 provided for literals are addition, subtraction, multiplication,

54 integer division and remainder.

56 \emph{Beware}: the arithmetic operators are

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

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

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

60 \begin{isabelle}

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

62 \end{isabelle}

63 %

64 Carefully observe how Isabelle displays the subgoal:

65 \begin{isabelle}

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

67 \end{isabelle}

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

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

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

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

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

76 start. Hundreds of useful lemmas about arithmetic on type \isa{nat} are

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

78 in exceptional circumstances should you resort to induction.

80 \subsubsection{Literals}

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

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

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

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

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

86 entirely different from \isa{0}, \isa{1} and \isa{2}. You will

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

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

89 needed in order to match many theorems, including the rewrite rules for

90 primitive recursive functions. The following default simplification rules

91 replace small literals by zero and successor:

92 \begin{isabelle}

93 \#0\ =\ 0

94 \rulename{numeral_0_eq_0}\isanewline

95 \#1\ =\ 1

96 \rulename{numeral_1_eq_1}\isanewline

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

98 \rulename{add_2_eq_Suc}\isanewline

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

100 \rulename{add_2_eq_Suc'}

101 \end{isabelle}

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

103 these rules.

105 \subsubsection{Typical lemmas}

106 Inequalities involving addition and subtraction alone can be proved

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

108 involving multiplication and division:

109 \begin{isabelle}

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

111 \rulename{mult_le_mono}\isanewline

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

113 *\ k\ <\ j\ *\ k%

114 \rulename{mult_less_mono1}\isanewline

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

116 \rulename{div_le_mono}

117 \end{isabelle}

118 %

119 Various distributive laws concerning multiplication are available:

120 \begin{isabelle}

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

122 \rulename{add_mult_distrib}\isanewline

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

124 \rulename{diff_mult_distrib}\isanewline

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

126 \rulename{mod_mult_distrib}

127 \end{isabelle}

129 \subsubsection{Division}

130 The library contains the basic facts about quotient and remainder

131 (including the analogous equation, \isa{div_if}):

132 \begin{isabelle}

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

134 \rulename{mod_if}\isanewline

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

136 \rulename{mod_div_equality}

137 \end{isabelle}

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

140 Here is a selection:

141 \begin{isabelle}

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

143 \rulename{div_mult1_eq}\isanewline

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

145 \rulename{mod_mult1_eq}\isanewline

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

147 \rulename{div_mult2_eq}\isanewline

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

149 \rulename{mod_mult2_eq}\isanewline

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

151 \rulename{div_mult_mult1}

152 \end{isabelle}

154 Surprisingly few of these results depend upon the

155 divisors' being nonzero. Isabelle/HOL defines division by zero:

156 \begin{isabelle}

157 a\ div\ 0\ =\ 0

158 \rulename{DIVISION_BY_ZERO_DIV}\isanewline

159 a\ mod\ 0\ =\ a%

160 \rulename{DIVISION_BY_ZERO_MOD}

161 \end{isabelle}

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

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

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

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

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

168 is overloaded over all numeric types:

169 \begin{isabelle}

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

171 \rulename{dvd_def}

172 \end{isabelle}

173 %

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

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

176 \begin{isabelle}

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

178 \rulename{dvd_anti_sym}\isanewline

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

180 \rulename{dvd_add}

181 \end{isabelle}

183 \subsubsection{Simplifier tricks}

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

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

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

187 nice properties; often it is best to remove it from a subgoal

188 using this split rule:

189 \begin{isabelle}

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

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

192 d))

193 \rulename{nat_diff_split}

194 \end{isabelle}

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

196 linear arithmetic:

197 \begin{isabelle}

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

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

200 \isacommand{done}

201 \end{isabelle}

203 Suppose that two expressions are equal, differing only in

204 associativity and commutativity of addition. Simplifying with the

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

206 the two expressions identical:

207 \begin{isabelle}

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

209 \rulename{add_assoc}\isanewline

210 m\ +\ n\ =\ n\ +\ m%

211 \rulename{add_commute}\isanewline

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

213 +\ z)

214 \rulename{add_left_commute}

215 \end{isabelle}

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

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

218 with this goal:

219 \begin{isabelle}

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

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

222 \end{isabelle}

223 %

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

225 \begin{isabelle}

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

227 \end{isabelle}

228 %

229 Here is the resulting subgoal:

230 \begin{isabelle}

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

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

233 \end{isabelle}

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

238 Reasoning methods resemble those for the natural numbers, but

239 induction and the constant \isa{Suc} are not available.

241 Concerning simplifier tricks, we have no need to eliminate subtraction (it

242 is well-behaved), but the simplifier can sort the operands of integer

243 operators. The name \isa{zadd_ac} refers to the associativity and

244 commutativity theorems for integer addition, while \isa{zmult_ac} has the

245 analogous theorems for multiplication. The prefix~\isa{z} in many theorem

246 names recalls the use of $\Bbb{Z}$ to denote the set of integers.

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

249 traditional mathematical practice: the sign of the remainder follows that

250 of the divisor:

251 \begin{isabelle}

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

253 \rulename{pos_mod_sign}\isanewline

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

255 \rulename{pos_mod_bound}\isanewline

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

257 \rulename{neg_mod_sign}\isanewline

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

259 \rulename{neg_mod_bound}

260 \end{isabelle}

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

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

264 The library provides many lemmas for proving inequalities involving integer

265 multiplication and division, similar to those shown above for

266 type~\isa{nat}. The absolute value function \isa{abs} is

267 defined for the integers; we have for example the obvious law

268 \begin{isabelle}

269 \isasymbar x\ *\ y\isasymbar \ =\ \isasymbar x\isasymbar \ *\ \isasymbar y\isasymbar

270 \rulename{abs_mult}

271 \end{isabelle}

273 Again, many facts about quotients and remainders are provided:

274 \begin{isabelle}

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

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

277 \rulename{zdiv_zadd1_eq}

278 \par\smallskip

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

280 \rulename{zmod_zadd1_eq}

281 \end{isabelle}

283 \begin{isabelle}

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

285 \rulename{zdiv_zmult1_eq}\isanewline

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

287 \rulename{zmod_zmult1_eq}

288 \end{isabelle}

290 \begin{isabelle}

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

292 \rulename{zdiv_zmult2_eq}\isanewline

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

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

295 \rulename{zmod_zmult2_eq}

296 \end{isabelle}

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

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

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

300 is

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

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

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

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

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

309 associativity and commutativity theorems for addition; similarly

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

312 \textbf{To be written. Inverse, abs, theorems about density, etc.?}