7 Until now, our numerical examples have used the type of \textbf{natural
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
45 \subsection{Numeric Literals}
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
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:
72 \isacommand{lemma}\ "2\ *\ m\ =\ m\ +\ m"
75 Carefully observe how Isabelle displays the subgoal:
77 \ 1.\ (2::'a)\ *\ m\ =\ m\ +\ m
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.
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
90 \isacommand{recdef}\ h\ "\isacharbraceleft \isacharbraceright "\isanewline
91 "h\ 3\ =\ 2"\isanewline
95 You should use a conditional expression instead:
97 "h\ i\ =\ (if\ i\ =\ 3\ then\ 2\ else\ i)"
99 \index{numeric literals|)}
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} 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
118 1\ \isasymequiv\ Suc\ 0
119 \rulename{One_nat_def}
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:
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'}
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:
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}
151 Many less obvious facts about quotient and remainder are also provided.
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}
170 Surprisingly few of these results depend upon the
171 divisors' being nonzero.
172 \index{division!by zero}%
173 That is because division by
177 \rulename{DIVISION_BY_ZERO_DIV}\isanewline
179 \rulename{DIVISION_BY_ZERO_MOD}
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:
188 m\ dvd\ n\ \isasymequiv\ {\isasymexists}k.\ n\ =\ m\ *\ k
192 Section~\ref{sec:proving-euclid} discusses proofs involving this
193 relation. Here are some of the facts proved about it:
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)
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}.
208 (m\ -\ n)\ *\ k\ =\ m\ *\ k\ -\ n\ *\ k%
209 \rulenamedx{diff_mult_distrib}
211 Natural number subtraction has few
212 nice properties; often you should remove it by simplifying with this split
215 P(a-b)\ =\ ((a<b\ \isasymlongrightarrow \ P\
216 0)\ \isasymand \ (\isasymforall d.\ a\ =\ b+d\ \isasymlongrightarrow \ P\
218 \rulename{nat_diff_split}
220 For example, splitting helps to prove the following fact.
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
226 The result lies outside the scope of linear arithmetic, but
228 if we explicitly split \isa{n<2} as \isa{n=0} or \isa{n=1}:
230 \isacommand{apply}\ (subgoal_tac\ "n=0\ |\ n=1",\ force,\ arith)\isanewline
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,
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.
252 \isacommand{lemma}\ "abs\ (x+y)\ \isasymle \ abs\ x\ +\ abs\ (y\ ::\ int)"\isanewline
253 \isacommand{by}\ arith
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
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}
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:
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}
278 (a\ +\ b)\ mod\ c\ =\ (a\ mod\ c\ +\ b\ mod\ c)\ mod\ c%
279 \rulename{zmod_zadd1_eq}
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}
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\
294 \rulename{zmod_zmult2_eq}
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
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 $<$):
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}
319 \subsection{The Types of Rational, Real and Complex Numbers}
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:
331 a\ <\ b\ \isasymLongrightarrow \ \isasymexists r.\ a\ <\ r\ \isasymand \ r\ <\ b%
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
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:
348 \ 1.\ P\ ((3\ /\ 4)\ *\ (8\ /\ 15))\isanewline
349 \isacommand{apply} simp\isanewline
352 Exponentiation can express floating-point values such as
353 \isa{2 * 10\isacharcircum6}, but at present no special simplification
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)|)}
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:
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.
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.
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.
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
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
422 The class \tcdx{ring_no_zero_divisors} of rings without zero divisors satisfies a number of natural cancellation laws, the first of which characterizes this class:
424 (a\ *\ b\ =\ (0::'a))\ =\ (a\ =\ (0::'a)\ \isasymor \ b\ =\ (0::'a))
425 \rulename{mult_eq_0_iff}\isanewline
426 (a\ *\ c\ =\ b\ *\ c)\ =\ (c\ =\ (0::'a)\ \isasymor \ a\ =\ b)
427 \rulename{mult_cancel_right}
430 Setting the flag \pgmenu{Isabelle} $>$ \pgmenu{Settings} $>$
431 \pgmenu{Show Sorts} will display the type classes of all type variables.
434 Here is how the theorem \isa{mult_cancel_left} appears with the flag set.
436 ((c::'a::ring_no_zero_divisors)\ *\ (a::'a::ring_no_zero_divisors) =\isanewline
437 \ c\ *\ (b::'a::ring_no_zero_divisors))\ =\isanewline
438 (c\ =\ (0::'a::ring_no_zero_divisors)\ \isasymor\ a\ =\ b)
442 \subsubsection{Simplifying with the AC-Laws}
443 Suppose that two expressions are equal, differing only in
444 associativity and commutativity of addition. Simplifying with the
445 following equations sorts the terms and groups them to the right, making
446 the two expressions identical.
448 a\ +\ b\ +\ c\ =\ a\ +\ (b\ +\ c)
449 \rulenamedx{add_assoc}\isanewline
451 \rulenamedx{add_commute}\isanewline
452 a\ +\ (b\ +\ c)\ =\ b\ +\ (a\ +\ c)
453 \rulename{add_left_commute}
455 The name \isa{add_ac}\index{*add_ac (theorems)}
456 refers to the list of all three theorems; similarly
457 there is \isa{mult_ac}.\index{*mult_ac (theorems)}
458 They are all proved for semirings and therefore hold for all numeric types.
460 Here is an example of the sorting effect. Start
461 with this goal, which involves type \isa{nat}.
463 \ 1.\ Suc\ (i\ +\ j\ *\ l\ *\ k\ +\ m\ *\ n)\ =\
464 f\ (n\ *\ m\ +\ i\ +\ k\ *\ j\ *\ l)
467 Simplify using \isa{add_ac} and \isa{mult_ac}.
469 \isacommand{apply}\ (simp\ add:\ add_ac\ mult_ac)
472 Here is the resulting subgoal.
474 \ 1.\ Suc\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))\
475 =\ f\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))%
479 \subsubsection{Division Laws for Fields}
481 Here is a selection of rules about the division operator. The following
482 are installed as default simplification rules in order to express
483 combinations of products and quotients as rational expressions:
485 a\ *\ (b\ /\ c)\ =\ a\ *\ b\ /\ c
486 \rulename{times_divide_eq_right}\isanewline
487 b\ /\ c\ *\ a\ =\ b\ *\ a\ /\ c
488 \rulename{times_divide_eq_left}\isanewline
489 a\ /\ (b\ /\ c)\ =\ a\ *\ c\ /\ b
490 \rulename{divide_divide_eq_right}\isanewline
491 a\ /\ b\ /\ c\ =\ a\ /\ (b\ *\ c)
492 \rulename{divide_divide_eq_left}
495 Signs are extracted from quotients in the hope that complementary terms can
498 -\ (a\ /\ b)\ =\ -\ a\ /\ b
499 \rulename{minus_divide_left}\isanewline
500 -\ (a\ /\ b)\ =\ a\ /\ -\ b
501 \rulename{minus_divide_right}
504 The following distributive law is available, but it is not installed as a
507 (a\ +\ b)\ /\ c\ =\ a\ /\ c\ +\ b\ /\ c%
508 \rulename{add_divide_distrib}
512 \subsubsection{Absolute Value}
514 The \rmindex{absolute value} function \cdx{abs} is available for all
515 ordered rings, including types \isa{int}, \isa{rat} and \isa{real}.
516 It satisfies many properties,
517 such as the following:
519 \isasymbar x\ *\ y\isasymbar \ =\ \isasymbar x\isasymbar \ *\ \isasymbar y\isasymbar
520 \rulename{abs_mult}\isanewline
521 (\isasymbar a\isasymbar \ \isasymle \ b)\ =\ (a\ \isasymle \ b\ \isasymand \ -\ a\ \isasymle \ b)
522 \rulename{abs_le_iff}\isanewline
523 \isasymbar a\ +\ b\isasymbar \ \isasymle \ \isasymbar a\isasymbar \ +\ \isasymbar b\isasymbar
524 \rulename{abs_triangle_ineq}
528 The absolute value bars shown above cannot be typed on a keyboard. They
529 can be entered using the X-symbol package. In \textsc{ascii}, type \isa{abs x} to
530 get \isa{\isasymbar x\isasymbar}.
534 \subsubsection{Raising to a Power}
536 Another type class, \tcdx{ringppower}, specifies rings that also have
537 exponentation to a natural number power, defined using the obvious primitive
538 recursion. Theory \thydx{Power} proves various theorems, such as the
541 a\ \isacharcircum \ (m\ +\ n)\ =\ a\ \isacharcircum \ m\ *\ a\ \isacharcircum \ n%
542 \rulename{power_add}\isanewline
543 a\ \isacharcircum \ (m\ *\ n)\ =\ (a\ \isacharcircum \ m)\ \isacharcircum \ n%
544 \rulename{power_mult}\isanewline
545 \isasymbar a\ \isacharcircum \ n\isasymbar \ =\ \isasymbar a\isasymbar \ \isacharcircum \ n%
547 \end{isabelle}%%%%%%%%%%%%%%%%%%%%%%%%%