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

doc-src/TutorialI/Types/numerics.tex

author | nipkow |

Wed Jun 22 09:26:18 2005 +0200 (2005-06-22) | |

changeset 16523 | f8a734dc0fbc |

parent 16412 | 50eab0183aea |

child 21243 | afffe1f72143 |

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

*** empty log message ***

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. With subtraction, arithmetic reasoning is easier, which makes

14 the integers preferable to the natural numbers for

15 complicated arithmetic expressions, even if they are non-negative. The logic HOL-Complex also has the types

16 \isa{rat}, \isa{real} and \isa{complex}: the rational, real and complex numbers. Isabelle has no

17 subtyping, so the numeric

18 types are distinct and there are functions to convert between them.

19 Most numeric operations are overloaded: the same symbol can be

20 used at all numeric types. Table~\ref{tab:overloading} in the appendix

21 shows the most important operations, together with the priorities of the

22 infix symbols. Algebraic properties are organized using type classes

23 around algebraic concepts such as rings and fields;

24 a property such as the commutativity of addition is a single theorem

25 (\isa{add_commute}) that applies to all numeric types.

27 \index{linear arithmetic}%

28 Many theorems involving numeric types can be proved automatically by

29 Isabelle's arithmetic decision procedure, the method

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

31 and multiplication by constant factors; subterms involving other operators

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

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

34 causes case splits. On types \isa{nat} and \isa{int}, \methdx{arith}

35 can deal with quantifiers---this is known as Presburger arithmetic---whereas on type \isa{real} it cannot.

37 The simplifier reduces arithmetic expressions in other

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

39 outside the scope of automation, HOL provides hundreds of

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

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

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

43 is available.

45 \subsection{Numeric Literals}

46 \label{sec:numerals}

48 \index{numeric literals|(}%

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

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

51 literals, which consist of one or more decimal digits optionally preceeded by a minus sign (\isa{-}). Examples are \isa{2}, \isa{-3} and

52 \isa{441223334678}. Literals are available for the types of natural

53 numbers, integers, rationals, reals, etc.; they denote integer values of

54 arbitrary size.

56 Literals look like constants, but they abbreviate

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

58 Isabelle performs arithmetic on literals by rewriting rather

59 than using the hardware arithmetic. In most cases arithmetic

60 is fast enough, even for numbers in the millions. The arithmetic operations

61 provided for literals include addition, subtraction, multiplication,

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

63 division) are reduced to lowest terms.

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

66 The arithmetic operators are

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

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

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

70 \par

71 \begin{isabelle}

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

73 \end{isabelle}

74 %

75 Carefully observe how Isabelle displays the subgoal:

76 \begin{isabelle}

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

78 \end{isabelle}

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

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

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

82 \end{warn}

84 \begin{warn}

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

86 Numeric literals are not constructors and therefore

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

88 rejected:

89 \begin{isabelle}

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

91 "h\ 3\ =\ 2"\isanewline

92 "h\ i\ \ =\ i"

93 \end{isabelle}

95 You should use a conditional expression instead:

96 \begin{isabelle}

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

98 \end{isabelle}

99 \index{numeric literals|)}

100 \end{warn}

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

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

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

107 beginning. Hundreds of theorems about the natural numbers are

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

109 Basic properties of addition and multiplication are available through the

110 axiomatic type class for semirings (\S\ref{sec:numeric-axclasses}).

112 \subsubsection{Literals}

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

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

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

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

117 \begin{isabelle}

118 1\ \isasymequiv\ Suc\ 0

119 \rulename{One_nat_def}

120 \end{isabelle}

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

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

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

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

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

127 The following default simplification rules replace

128 small literals by zero and successor:

129 \begin{isabelle}

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

131 \rulename{add_2_eq_Suc}\isanewline

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

133 \rulename{add_2_eq_Suc'}

134 \end{isabelle}

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

136 the simplifier will normally reverse this transformation. Novices should

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

139 \subsubsection{Division}

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

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

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

143 on the natural numbers:

144 \begin{isabelle}

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

146 \rulename{mod_if}\isanewline

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

148 \rulenamedx{mod_div_equality}

149 \end{isabelle}

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

152 Here is a selection:

153 \begin{isabelle}

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

155 \rulename{div_mult1_eq}\isanewline

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

157 \rulename{mod_mult1_eq}\isanewline

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

159 \rulename{div_mult2_eq}\isanewline

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

161 \rulename{mod_mult2_eq}\isanewline

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

163 \rulename{div_mult_mult1}\isanewline

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

165 \rulenamedx{mod_mult_distrib}\isanewline

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

167 \rulename{div_le_mono}

168 \end{isabelle}

170 Surprisingly few of these results depend upon the

171 divisors' being nonzero.

172 \index{division!by zero}%

173 That is because division by

174 zero yields zero:

175 \begin{isabelle}

176 a\ div\ 0\ =\ 0

177 \rulename{DIVISION_BY_ZERO_DIV}\isanewline

178 a\ mod\ 0\ =\ a%

179 \rulename{DIVISION_BY_ZERO_MOD}

180 \end{isabelle}

181 In \isa{div_mult_mult1} above, one of

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

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

185 has the standard definition, which

186 is overloaded over all numeric types:

187 \begin{isabelle}

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

189 \rulenamedx{dvd_def}

190 \end{isabelle}

191 %

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

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

194 \begin{isabelle}

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

196 \rulenamedx{dvd_anti_sym}\isanewline

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

198 \rulenamedx{dvd_add}

199 \end{isabelle}

201 \subsubsection{Subtraction}

203 There are no negative natural numbers, so \isa{m\ -\ n} equals zero unless

204 \isa{m} exceeds~\isa{n}. The following is one of the few facts

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

206 the condition \isa{n\ \isasymle \ m}.

207 \begin{isabelle}

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

209 \rulenamedx{diff_mult_distrib}

210 \end{isabelle}

211 Natural number subtraction has few

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

213 rule.

214 \begin{isabelle}

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

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

217 d))

218 \rulename{nat_diff_split}

219 \end{isabelle}

220 For example, splitting helps to prove the following fact.

221 \begin{isabelle}

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

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

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

225 \end{isabelle}

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

227 it is easily found

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

229 \begin{isabelle}

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

231 \isacommand{done}

232 \end{isabelle}%%%%%%

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

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

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

239 Reasoning methods for the integers resemble those for the natural numbers,

240 but induction and

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

242 proving inequalities involving integer multiplication and division, similar

243 to those shown above for type~\isa{nat}. The laws of addition, subtraction

244 and multiplication are available through the axiomatic type class for rings

245 (\S\ref{sec:numeric-axclasses}).

247 The \rmindex{absolute value} function \cdx{abs} is overloaded, and is

248 defined for all types that involve negative numbers, including the integers.

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

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

251 \begin{isabelle}

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

253 \isacommand{by}\ arith

254 \end{isabelle}

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

257 the treatment of negative divisors follows

258 mathematical practice: the sign of the remainder follows that

259 of the divisor:

260 \begin{isabelle}

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

262 \rulename{pos_mod_sign}\isanewline

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

264 \rulename{pos_mod_bound}\isanewline

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

266 \rulename{neg_mod_sign}\isanewline

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

268 \rulename{neg_mod_bound}

269 \end{isabelle}

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

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

272 Many facts about quotients and remainders are provided:

273 \begin{isabelle}

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

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

276 \rulename{zdiv_zadd1_eq}

277 \par\smallskip

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

279 \rulename{zmod_zadd1_eq}

280 \end{isabelle}

282 \begin{isabelle}

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

284 \rulename{zdiv_zmult1_eq}\isanewline

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

286 \rulename{zmod_zmult1_eq}

287 \end{isabelle}

289 \begin{isabelle}

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

291 \rulename{zdiv_zmult2_eq}\isanewline

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

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

294 \rulename{zmod_zmult2_eq}

295 \end{isabelle}

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

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

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

299 is

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

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

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

303 denote the set of integers.%

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

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 $<$):

307 \begin{isabelle}

308 \isasymlbrakk k\ \isasymle \ i;\ P\ k;\ \isasymAnd i.\ \isasymlbrakk k\ \isasymle \ i;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i+1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%

309 \rulename{int_ge_induct}\isanewline

310 \isasymlbrakk k\ <\ i;\ P(k+1);\ \isasymAnd i.\ \isasymlbrakk k\ <\ i;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i+1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%

311 \rulename{int_gr_induct}\isanewline

312 \isasymlbrakk i\ \isasymle \ k;\ P\ k;\ \isasymAnd i.\ \isasymlbrakk i\ \isasymle \ k;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i-1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%

313 \rulename{int_le_induct}\isanewline

314 \isasymlbrakk i\ <\ k;\ P(k-1);\ \isasymAnd i.\ \isasymlbrakk i\ <\ k;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i-1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%

315 \rulename{int_less_induct}

316 \end{isabelle}

319 \subsection{The Types of Rational, Real and Complex Numbers}

320 \label{sec:real}

322 \index{rational numbers|(}\index{*rat (type)|(}%

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

324 \index{complex numbers|(}\index{*complex (type)|(}%

325 These types provide true division, the overloaded operator \isa{/},

326 which differs from the operator \isa{div} of the

327 natural numbers and integers. The rationals and reals are

328 \textbf{dense}: between every two distinct numbers lies another.

329 This property follows from the division laws, since if $x\not=y$ then $(x+y)/2$ lies between them:

330 \begin{isabelle}

331 a\ <\ b\ \isasymLongrightarrow \ \isasymexists r.\ a\ <\ r\ \isasymand \ r\ <\ b%

332 \rulename{dense}

333 \end{isabelle}

335 The real numbers are, moreover, \textbf{complete}: every set of reals that

336 is bounded above has a least upper bound. Completeness distinguishes the

337 reals from the rationals, for which the set $\{x\mid x^2<2\}$ has no least

338 upper bound. (It could only be $\surd2$, which is irrational. The

339 formalization of completeness, which is complicated,

340 can be found in theory \texttt{RComplete} of directory

341 \texttt{Real}.

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

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

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

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

347 \begin{isabelle}

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

349 \isacommand{apply} simp\isanewline

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

351 \end{isabelle}

352 Exponentiation can express floating-point values such as

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

354 is performed.

356 \begin{warn}

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

358 HOL extended with a definitional development of the real and complex

359 numbers. Base your theory upon theory \thydx{Complex_Main}, not the

360 usual \isa{Main}, and set the Proof General menu item \pgmenu{Isabelle} $>$

361 \pgmenu{Logics} $>$ \pgmenu{HOL-Complex}.%

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

363 \end{warn}

365 Also available in HOL-Complex is the

366 theory \isa{Hyperreal}, which define the type \tydx{hypreal} of

367 \rmindex{non-standard reals}. These

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

369 small and infinitely large quantities; they facilitate proofs

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

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

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

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

374 Theory \isa{Hyperreal} also defines transcendental functions such as sine,

375 cosine, exponential and logarithm --- even the versions for type

376 \isa{real}, because they are defined using nonstandard limits.%

377 \index{rational numbers|)}\index{*rat (type)|)}%

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

379 \index{complex numbers|)}\index{*complex (type)|)}

382 \subsection{The Numeric Type Classes}\label{sec:numeric-axclasses}

384 Isabelle/HOL organises its numeric theories using axiomatic type classes.

385 Hundreds of basic properties are proved in the theory \isa{Ring_and_Field}.

386 These lemmas are available (as simprules if they were declared as such)

387 for all numeric types satisfying the necessary axioms. The theory defines

388 the following type classes:

389 \begin{itemize}

390 \item

391 \tcdx{semiring} and \tcdx{ordered_semiring}: a \emph{semiring}

392 provides the operators \isa{+} and~\isa{*}, which are commutative and

393 associative, with the usual distributive law and with \isa{0} and~\isa{1}

394 as their respective identities. An \emph{ordered semiring} is also linearly

395 ordered, with addition and multiplication respecting the ordering. Type \isa{nat} is an ordered semiring.

396 \item

397 \tcdx{ring} and \tcdx{ordered_ring}: a \emph{ring} extends a semiring

398 with unary minus (the additive inverse) and subtraction (both

399 denoted~\isa{-}). An \emph{ordered ring} includes the absolute value

400 function, \cdx{abs}. Type \isa{int} is an ordered ring.

401 \item

402 \tcdx{field} and \tcdx{ordered_field}: a field extends a ring with the

403 multiplicative inverse (called simply \cdx{inverse} and division~(\isa{/}).

404 An ordered field is based on an ordered ring. Type \isa{complex} is a field, while type \isa{real} is an ordered field.

405 \item

406 \tcdx{division_by_zero} includes all types where \isa{inverse 0 = 0}

407 and \isa{a / 0 = 0}. These include all of Isabelle's standard numeric types.

408 However, the basic properties of fields are derived without assuming

409 division by zero.

410 \end{itemize}

412 Theory \thydx{Ring_and_Field} proves over 250 lemmas, each of which

413 holds for all types in the corresponding type class. In most

414 cases, it is obvious whether a property is valid for a particular type. All

415 abstract properties involving subtraction require a ring, and therefore do

416 not hold for type \isa{nat}, although we have theorems such as

417 \isa{diff_mult_distrib} proved specifically about subtraction on

418 type~\isa{nat}. All abstract properties involving division require a field.

419 Obviously, all properties involving orderings required an ordered

420 structure.

422 The following two theorems are less obvious. Although they

423 mention no ordering, they require an ordered ring. However, if we have a

424 field, then an ordering is no longer required.

425 \begin{isabelle}

426 (a\ *\ b\ =\ (0::'a))\ =\ (a\ =\ (0::'a)\ \isasymor \ b\ =\ (0::'a))

427 \rulename{mult_eq_0_iff}\isanewline

428 (a\ *\ c\ =\ b\ *\ c)\ =\ (c\ =\ (0::'a)\ \isasymor \ a\ =\ b)

429 \rulename{mult_cancel_right}

430 \end{isabelle}

431 Theorems \isa{field_mult_eq_0_iff} and \isa{field_mult_cancel_right}

432 express the same properties, only for fields.

433 \begin{pgnote}

434 Setting the flag \pgmenu{Isabelle} $>$ \pgmenu{Settings} $>$

435 \pgmenu{Show Sorts} will display the type classes of all type variables.

436 \end{pgnote}

437 \noindent

438 Here is how the theorem \isa{field_mult_cancel_right} appears with the flag set.

439 \begin{isabelle}

440 ((a::'a::field)\ *\ (c::'a::field)\ =\ (b::'a::field)\ *\ c)\ =\isanewline

441 (c\ =\ (0::'a::field)\ \isasymor \ a\ =\ b)

442 \end{isabelle}

445 \subsubsection{Simplifying with the AC-Laws}

446 Suppose that two expressions are equal, differing only in

447 associativity and commutativity of addition. Simplifying with the

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

449 the two expressions identical.

450 \begin{isabelle}

451 a\ +\ b\ +\ c\ =\ a\ +\ (b\ +\ c)

452 \rulenamedx{add_assoc}\isanewline

453 a\ +\ b\ =\ b\ +\ a%

454 \rulenamedx{add_commute}\isanewline

455 a\ +\ (b\ +\ c)\ =\ b\ +\ (a\ +\ c)

456 \rulename{add_left_commute}

457 \end{isabelle}

458 The name \isa{add_ac}\index{*add_ac (theorems)}

459 refers to the list of all three theorems; similarly

460 there is \isa{mult_ac}.\index{*mult_ac (theorems)}

461 They are all proved for semirings and therefore hold for all numeric types.

463 Here is an example of the sorting effect. Start

464 with this goal, which involves type \isa{nat}.

465 \begin{isabelle}

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

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

468 \end{isabelle}

469 %

470 Simplify using \isa{add_ac} and \isa{mult_ac}.

471 \begin{isabelle}

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

473 \end{isabelle}

474 %

475 Here is the resulting subgoal.

476 \begin{isabelle}

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

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

479 \end{isabelle}

482 \subsubsection{Division Laws for Fields}

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

485 are installed as default simplification rules in order to express

486 combinations of products and quotients as rational expressions:

487 \begin{isabelle}

488 a\ *\ (b\ /\ c)\ =\ a\ *\ b\ /\ c

489 \rulename{times_divide_eq_right}\isanewline

490 b\ /\ c\ *\ a\ =\ b\ *\ a\ /\ c

491 \rulename{times_divide_eq_left}\isanewline

492 a\ /\ (b\ /\ c)\ =\ a\ *\ c\ /\ b

493 \rulename{divide_divide_eq_right}\isanewline

494 a\ /\ b\ /\ c\ =\ a\ /\ (b\ *\ c)

495 \rulename{divide_divide_eq_left}

496 \end{isabelle}

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

499 then be cancelled:

500 \begin{isabelle}

501 -\ (a\ /\ b)\ =\ -\ a\ /\ b

502 \rulename{minus_divide_left}\isanewline

503 -\ (a\ /\ b)\ =\ a\ /\ -\ b

504 \rulename{minus_divide_right}

505 \end{isabelle}

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

508 simplification rule.

509 \begin{isabelle}

510 (a\ +\ b)\ /\ c\ =\ a\ /\ c\ +\ b\ /\ c%

511 \rulename{add_divide_distrib}

512 \end{isabelle}

515 \subsubsection{Absolute Value}

517 The \rmindex{absolute value} function \cdx{abs} is available for all

518 ordered rings, including types \isa{int}, \isa{rat} and \isa{real}.

519 It satisfies many properties,

520 such as the following:

521 \begin{isabelle}

522 \isasymbar x\ *\ y\isasymbar \ =\ \isasymbar x\isasymbar \ *\ \isasymbar y\isasymbar

523 \rulename{abs_mult}\isanewline

524 (\isasymbar a\isasymbar \ \isasymle \ b)\ =\ (a\ \isasymle \ b\ \isasymand \ -\ a\ \isasymle \ b)

525 \rulename{abs_le_iff}\isanewline

526 \isasymbar a\ +\ b\isasymbar \ \isasymle \ \isasymbar a\isasymbar \ +\ \isasymbar b\isasymbar

527 \rulename{abs_triangle_ineq}

528 \end{isabelle}

530 \begin{warn}

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

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

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

534 \end{warn}

537 \subsubsection{Raising to a Power}

539 Another type class, \tcdx{ringppower}, specifies rings that also have

540 exponentation to a natural number power, defined using the obvious primitive

541 recursion. Theory \thydx{Power} proves various theorems, such as the

542 following.

543 \begin{isabelle}

544 a\ \isacharcircum \ (m\ +\ n)\ =\ a\ \isacharcircum \ m\ *\ a\ \isacharcircum \ n%

545 \rulename{power_add}\isanewline

546 a\ \isacharcircum \ (m\ *\ n)\ =\ (a\ \isacharcircum \ m)\ \isacharcircum \ n%

547 \rulename{power_mult}\isanewline

548 \isasymbar a\ \isacharcircum \ n\isasymbar \ =\ \isasymbar a\isasymbar \ \isacharcircum \ n%

549 \rulename{power_abs}

550 \end{isabelle}%%%%%%%%%%%%%%%%%%%%%%%%%

551 \index{numbers|)}