diff -r f51d4a302962 -r 5386df44a037 src/Doc/Tutorial/document/numerics.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Tutorial/document/numerics.tex	Tue Aug 28 18:57:32 2012 +0200
@@ -0,0 +1,543 @@
+\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_antisym}\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}, which will be simplified to integers.
+
+\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|)}