src/Doc/Tutorial/document/numerics.tex

 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 
+\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 
+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 
+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

 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, 
+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 
+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}

 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}  
+\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

 \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}.  
+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}}%

 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: 
+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'}

 \rulename{mod_if}\isanewline
 m\ div\ n\ *\ n\ +\ m\ mod\ n\ =\ m%
 \rulenamedx{div_mult_mod_eq}
 \end{isabelle}
 
-Many less obvious facts about quotient and remainder are also provided. 
+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%

 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: 
+is overloaded over all numeric types:
 \begin{isabelle}
 m\ dvd\ n\ \isasymequiv\ {\isasymexists}k.\ n\ =\ m\ *\ k
 \rulenamedx{dvd_def}
 \end{isabelle}
 %

 \rulenamedx{dvd_add}
 \end{isabelle}
 
 \subsubsection{Subtraction}
 
-There are no negative natural numbers, so \isa{m\ -\ n} equals zero unless 
+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}. 
+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

 
 
 \subsection{The Type of Integers, {\tt\slshape int}}
 
 \index{integers|(}\index{*int (type)|(}%
-Reasoning methods for the integers resemble those for the natural numbers, 
+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 
+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, 
+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}

 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}
+\rulename{div_add1_eq}
 \par\smallskip
 (a\ +\ b)\ mod\ c\ =\ (a\ mod\ c\ +\ b\ mod\ c)\ mod\ c%
 \rulename{mod_add_eq}
 \end{isabelle}
 

 \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 
+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}

 
 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, 
+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

 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 
+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 
+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)|)}%

 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 
+\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 
+\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 
+\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 
+\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}

 (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 
+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)

 a\ +\ b\ =\ b\ +\ a%
 \rulenamedx{add.commute}\isanewline
 a\ +\ (b\ +\ c)\ =\ b\ +\ (a\ +\ c)
 \rulename{add.left_commute}
 \end{isabelle}
-The name \isa{ac_simps}\index{*ac_simps (theorems)} 
+The name \isa{ac_simps}\index{*ac_simps (theorems)}
 refers to the list of all three theorems; similarly
-there is \isa{ac_simps}.\index{*ac_simps (theorems)} 
+there is \isa{ac_simps}.\index{*ac_simps (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}

 \end{isabelle}
 
 
 \subsubsection{Absolute Value}
 
-The \rmindex{absolute value} function \cdx{abs} is available for all 
+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 
+\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 
+\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

 \end{warn}
 
 
 \subsubsection{Raising to a Power}
 
-Another type class, \tcdx{ordered\_idom}, specifies rings that also have 
+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 
+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%