--- a/doc-src/TutorialI/Types/numerics.tex Tue Aug 28 13:15:15 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,543 +0,0 @@
-\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|)}