\section{Numbers}

 \label{sec:numbers}

 \index{numbers|(}%

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

 numbers},

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

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

 recursive function definitions.  HOL also provides the type

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

 subtraction.  With subtraction, arithmetic reasoning is easier, which makes

 the integers preferable to the natural numbers for

 complicated arithmetic expressions, even if they are non-negative.  There are also the types

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

 subtyping,  so the numeric

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

 Most numeric operations are overloaded: the same symbol can be

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

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

 infix symbols. Algebraic properties are organized using type classes

 around algebraic concepts such as rings and fields;

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

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

 \index{linear arithmetic}%

 Many theorems involving numeric types can be proved automatically by

 Isabelle's arithmetic decision procedure, the method

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

 and multiplication by constant factors; subterms involving other operators

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

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

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

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

 The simplifier reduces arithmetic expressions in other

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

 outside the scope of automation, HOL provides hundreds of

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

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

 button.  A few lemmas are given below to show what

 is available.

 \subsection{Numeric Literals}

 \label{sec:numerals}

 \index{numeric literals|(}%

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

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

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

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

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

 arbitrary size.

 Literals look like constants, but they abbreviate 

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

 Isabelle performs arithmetic on literals by rewriting rather 

 than using the hardware arithmetic. In most cases arithmetic 

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

 provided for literals include addition, subtraction, multiplication, 

 integer division and remainder.  Fractions of literals (expressed using

 division) are reduced to lowest terms.

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

 The arithmetic operators are 

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

 expression refers to a specific type, if necessary by inserting 

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

 \par

 \begin{isabelle}

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

 \end{isabelle}

 %

 Carefully observe how Isabelle displays the subgoal:

 \begin{isabelle}

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

 \end{isabelle}

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

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

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

 \end{warn}

 \begin{warn}

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

 Numeric literals are not constructors and therefore

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

 rejected:

 \begin{isabelle}

 \isacommand{function}\ h\ \isakeyword{where}\isanewline

 "h\ 3\ =\ 2"\isanewline

 \isacharbar "h\ i\ \ =\ i"

 \end{isabelle}

 You should use a conditional expression instead:

 \begin{isabelle}

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

 \end{isabelle}

 \index{numeric literals|)}

 \end{warn}

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

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

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

 beginning.  Hundreds of theorems about the natural numbers are

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

 Basic properties of addition and multiplication are available through the

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

 \subsubsection{Literals}

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

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

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

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

 \begin{isabelle}

 1\ \isasymequiv\ Suc\ 0

 \rulename{One_nat_def}

 \end{isabelle}

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

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

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

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

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

 The following default  simplification rules replace

 small literals by zero and successor: 

 \begin{isabelle}

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

 \rulename{add_2_eq_Suc}\isanewline

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

 \rulename{add_2_eq_Suc'}

 \end{isabelle}

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

 the simplifier will normally reverse this transformation.  Novices should

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

 \subsubsection{Division}

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

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

 Isabelle/HOL provides the basic facts about quotient and remainder

 on the natural numbers:

 \begin{isabelle}

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

 \rulename{mod_if}\isanewline

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

 \rulenamedx{mod_div_equality}

 \end{isabelle}

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

 Here is a selection:

 \begin{isabelle}

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

 \rulename{div_mult1_eq}\isanewline

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

 \rulename{mod_mult_right_eq}\isanewline

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

 \rulename{div_mult2_eq}\isanewline

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

 \rulename{mod_mult2_eq}\isanewline

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

 \rulename{div_mult_mult1}\isanewline

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

 \rulenamedx{mod_mult_distrib}\isanewline

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

 \rulename{div_le_mono}

 \end{isabelle}

 Surprisingly few of these results depend upon the

 divisors' being nonzero.

 \index{division!by zero}%

 That is because division by

 zero yields zero:

 \begin{isabelle}

 a\ div\ 0\ =\ 0

 \rulename{DIVISION_BY_ZERO_DIV}\isanewline

 a\ mod\ 0\ =\ a%

 \rulename{DIVISION_BY_ZERO_MOD}

 \end{isabelle}

 In \isa{div_mult_mult1} above, one of

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

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

 has the standard definition, which

 is overloaded over all numeric types: 

 \begin{isabelle}

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

 \rulenamedx{dvd_def}

 \end{isabelle}

 %

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

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

 \begin{isabelle}

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

 \rulenamedx{dvd_anti_sym}\isanewline

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

 \rulenamedx{dvd_add}

 \end{isabelle}

 \subsubsection{Subtraction}

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

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

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

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

 \begin{isabelle}

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

 \rulenamedx{diff_mult_distrib}

 \end{isabelle}

 Natural number subtraction has few

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

 rule.

 \begin{isabelle}

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

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

 d))

 \rulename{nat_diff_split}

 \end{isabelle}

 For example, splitting helps to prove the following fact.

 \begin{isabelle}

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

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

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

 \end{isabelle}

 The result lies outside the scope of linear arithmetic, but

  it is easily found

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

 \begin{isabelle}

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

 \isacommand{done}

 \end{isabelle}%%%%%%

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

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

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

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

 but induction and

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

 proving inequalities involving integer multiplication and division, similar

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

 and multiplication are available through the axiomatic type class for rings

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

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

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

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

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

 \begin{isabelle}

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

 \isacommand{by}\ arith

 \end{isabelle}

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

 the treatment of negative divisors follows

 mathematical practice: the sign of the remainder follows that

 of the divisor:

 \begin{isabelle}

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

 \rulename{pos_mod_sign}\isanewline

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

 \rulename{pos_mod_bound}\isanewline

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

 \rulename{neg_mod_sign}\isanewline

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

 \rulename{neg_mod_bound}

 \end{isabelle}

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

 treats signed operands using the same rules as for multiplication.

 Many facts about quotients and remainders are provided:

 \begin{isabelle}

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

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

 \rulename{zdiv_zadd1_eq}

 \par\smallskip

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

 \rulename{mod_add_eq}

 \end{isabelle}

 \begin{isabelle}

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

 \rulename{zdiv_zmult1_eq}\isanewline

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

 \rulename{zmod_zmult1_eq}

 \end{isabelle}

 \begin{isabelle}

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

 \rulename{zdiv_zmult2_eq}\isanewline

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

 c)\ +\ a\ mod\ b%

 \rulename{zmod_zmult2_eq}

 \end{isabelle}

 The last two differ from their natural number analogues by requiring

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

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

 is

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

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

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

 denote the set of integers.%

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

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

 \begin{isabelle}

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

 \rulename{int_ge_induct}\isanewline

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

 \rulename{int_gr_induct}\isanewline

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

 \rulename{int_le_induct}\isanewline

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

 \rulename{int_less_induct}

 \end{isabelle}

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

 \label{sec:real}

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

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

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

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

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

 natural numbers and integers. The rationals and reals are 

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

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

 \begin{isabelle}

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

 \rulename{dense}

 \end{isabelle}

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

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

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

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

 formalization of completeness, which is complicated, 

 can be found in theory \texttt{RComplete}.

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

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

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

 using the division operator are automatically simplified to lowest terms:

 \begin{isabelle}

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

 \isacommand{apply} simp\isanewline

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

 \end{isabelle}

 Exponentiation can express floating-point values such as

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

 is performed.

 \begin{warn}

 Types \isa{rat}, \isa{real} and \isa{complex} are provided by theory HOL-Complex, which is

 Main extended with a definitional development of the rational, real and complex

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

 usual \isa{Main}.%

 \end{warn}

 Available in the logic HOL-NSA is the

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

 \rmindex{non-standard reals}.  These

 \textbf{hyperreals} include infinitesimals, which represent infinitely

 small and infinitely large quantities; they facilitate proofs

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

 dozens of type classes, such as the following:

 \begin{itemize}

 \item 

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

 provides the associative operators \isa{+} and~\isa{*}, with \isa{0} and~\isa{1}

 as their respective identities. The operators enjoy the usual distributive law,

 and addition (\isa{+}) is also commutative.

 An \emph{ordered semiring} is also linearly

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

 \item 

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

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

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

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

 \item 

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

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

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

 \item 

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

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

 However, the basic properties of fields are derived without assuming

 division by zero.

 \end{itemize}

 Hundreds of basic lemmas are proved, each of which

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

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

 abstract properties involving subtraction hold for type \isa{nat};

 instead, theorems such as

 \isa{diff_mult_distrib} are proved specifically about subtraction on

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

 Obviously, all properties involving orderings required an ordered

 structure.

 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:

 \begin{isabelle}

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

 \rulename{mult_eq_0_iff}\isanewline

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

 \rulename{mult_cancel_right}

 \end{isabelle}

 \begin{pgnote}

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

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

 \end{pgnote}

 \noindent

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

 \begin{isabelle}

 ((c::'a::ring_no_zero_divisors)\ *\ (a::'a::ring_no_zero_divisors) =\isanewline

 \ c\ *\ (b::'a::ring_no_zero_divisors))\ =\isanewline

 (c\ =\ (0::'a::ring_no_zero_divisors)\ \isasymor\ a\ =\ b)

 \end{isabelle}

 \subsubsection{Simplifying with the AC-Laws}

 Suppose that two expressions are equal, differing only in 

 associativity and commutativity of addition.  Simplifying with the

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

 the two expressions identical.

 \begin{isabelle}

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

 \rulenamedx{add_assoc}\isanewline

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

 \rulenamedx{add_commute}\isanewline

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

 \rulename{add_left_commute}

 \end{isabelle}

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

 refers to the list of all three theorems; similarly

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

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

 Here is an example of the sorting effect.  Start

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

 \begin{isabelle}

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

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

 \end{isabelle}

 %

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

 \begin{isabelle}

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

 \end{isabelle}

 %

 Here is the resulting subgoal.

 \begin{isabelle}

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

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

 \end{isabelle}

 \subsubsection{Division Laws for Fields}

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

 are installed as default simplification rules in order to express

 combinations of products and quotients as rational expressions:

 \begin{isabelle}

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

 \rulename{times_divide_eq_right}\isanewline

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

 \rulename{times_divide_eq_left}\isanewline

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

 \rulename{divide_divide_eq_right}\isanewline

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

 \rulename{divide_divide_eq_left}

 \end{isabelle}

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

 then be cancelled:

 \begin{isabelle}

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

 \rulename{minus_divide_left}\isanewline

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

 \rulename{minus_divide_right}

 \end{isabelle}

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

 simplification rule.

 \begin{isabelle}

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

 \rulename{add_divide_distrib}

 \end{isabelle}

 \subsubsection{Absolute Value}

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

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

 It satisfies many properties,

 such as the following:

 \begin{isabelle}

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

 \rulename{abs_mult}\isanewline

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

 \rulename{abs_le_iff}\isanewline

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

 \rulename{abs_triangle_ineq}

 \end{isabelle}

 \begin{warn}

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

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

 get \isa{\isasymbar x\isasymbar}.

 \end{warn}

 \subsubsection{Raising to a Power}

 Another type class, \tcdx{ordered\_idom}, specifies rings that also have 

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

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

 following.

 \begin{isabelle}

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

 \rulename{power_add}\isanewline

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

 \rulename{power_mult}\isanewline

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

 \rulename{power_abs}

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

 \index{numbers|)}