Our examples until now 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. Isabelle/HOL also has the type \isa{int} of

 \textbf{integers}, which gives up induction in exchange  for proper

 subtraction. The logic HOL-Real also has the type \isa{real} of real

 numbers.  Isabelle has no subtyping,  so the numeric types are distinct and

 there are  functions to convert between them. 

 The integers are preferable to the natural  numbers for reasoning about

 complicated arithmetic expressions. For  example, a termination proof

 typically involves an integer metric  that is shown to decrease at each

 loop iteration. Even if the  metric cannot become negative, proofs about it

 are usually easier  if the integers are used rather than the natural

 numbers. 

 Many theorems involving numeric types can be proved automatically by

 Isabelle's arithmetic decision procedure, the method

 \isa{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.  

 The simplifier reduces arithmetic expressions in other

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

 outside the scope of automation, the library has hundreds of

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

 bear.  You can find find them by browsing the library.  Some

 useful lemmas are shown below.

 \subsection{Numeric Literals}

 \label{sec:numerals}

 Literals are available for the types of natural numbers, integers 

 and reals and denote integer values of arbitrary size. 

 They begin 

 with a number sign (\isa{\#}), have an optional minus sign (\isa{-}) and 

 then one or more decimal digits. Examples are \isa{\#0}, \isa{\#-3} 

 and \isa{\#441223334678}.

 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 large numbers. The arithmetic operations 

 provided for literals are addition, subtraction, multiplication, 

 integer division and remainder. 

 \emph{Beware}: 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:

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

 \subsection{The type of natural numbers, {\tt\slshape nat}}

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

 start.  Hundreds of useful lemmas about arithmetic on type \isa{nat} are

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

 in exceptional circumstances should you resort to induction.

 \subsubsection{Literals}

 The notational options for the natural numbers can be confusing. The 

 constant \isa{0} is overloaded to serve as the neutral value 

 in a variety of additive types. The symbols \isa{1} and \isa{2} are 

 not constants but abbreviations for \isa{Suc 0} and \isa{Suc(Suc 0)},

 respectively. The literals \isa{\#0}, \isa{\#1} and \isa{\#2}  are

 entirely different from \isa{0}, \isa{1} and \isa{2}. You  will

 sometimes prefer one notation to the other. Literals are  obviously

 necessary to express large values, while \isa{0} and \isa{Suc}  are

 needed in order to match many theorems, including the rewrite  rules for

 primitive recursive functions. The following default  simplification rules

 replace small literals by zero and successor: 

 \begin{isabelle}

 \#0\ =\ 0

 \rulename{numeral_0_eq_0}\isanewline

 \#1\ =\ 1

 \rulename{numeral_1_eq_1}\isanewline

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

 \rulename{add_2_eq_Suc}\isanewline

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

 \rulename{add_2_eq_Suc'}

 \end{isabelle}

 In special circumstances, you may wish to remove or reorient 

 these rules. 

 \subsubsection{Typical lemmas}

 Inequalities involving addition and subtraction alone can be proved

 automatically.  Lemmas such as these can be used to prove inequalities

 involving multiplication and division:

 \begin{isabelle}

 \isasymlbrakk i\ \isasymle \ j;\ k\ \isasymle \ l\isasymrbrakk \ \isasymLongrightarrow \ i\ *\ k\ \isasymle \ j\ *\ l%

 \rulename{mult_le_mono}\isanewline

 \isasymlbrakk i\ <\ j;\ 0\ <\ k\isasymrbrakk \ \isasymLongrightarrow \ i\

 *\ k\ <\ j\ *\ k%

 \rulename{mult_less_mono1}\isanewline

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

 \rulename{div_le_mono}

 \end{isabelle}

 %

 Various distributive laws concerning multiplication are available:

 \begin{isabelle}

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

 \rulename{add_mult_distrib}\isanewline

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

 \rulename{diff_mult_distrib}\isanewline

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

 \rulename{mod_mult_distrib}

 \end{isabelle}

 \subsubsection{Division}

 The library contains the basic facts about quotient and remainder

 (including the analogous equation, \isa{div_if}):

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

 \rulename{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_mult1_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}

 \end{isabelle}

 Surprisingly few of these results depend upon the

 divisors' being nonzero.  Isabelle/HOL defines division by zero:

 \begin{isabelle}

 a\ div\ 0\ =\ 0

 \rulename{DIVISION_BY_ZERO_DIV}\isanewline

 a\ mod\ 0\ =\ a%

 \rulename{DIVISION_BY_ZERO_MOD}

 \end{isabelle}

 As a concession to convention, these equations are not installed as default

 simplification rules but are merely used to remove nonzero-divisor

 hypotheses by case analysis.  In \isa{div_mult_mult1} above, one of

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

 The \textbf{divides} relation has the standard definition, which

 is overloaded over all numeric types: 

 \begin{isabelle}

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

 \rulename{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%

 \rulename{dvd_anti_sym}\isanewline

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

 \rulename{dvd_add}

 \end{isabelle}

 \subsubsection{Simplifier tricks}

 The rule \isa{diff_mult_distrib} shown above is one of the few facts

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

 the condition \isa{n\ \isasymle \  m}.  Natural number subtraction has few

 nice properties; often it is best to remove it from a subgoal

 using 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, it proves the following fact, which lies outside the scope of

 linear arithmetic:

 \begin{isabelle}

 \isacommand{lemma}\ "(n-1)*(n+1)\ =\ n*n\ -\ 1"\isanewline

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

 \isacommand{done}

 \end{isabelle}

 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}

 m\ +\ n\ +\ k\ =\ m\ +\ (n\ +\ k)

 \rulename{add_assoc}\isanewline

 m\ +\ n\ =\ n\ +\ m%

 \rulename{add_commute}\isanewline

 x\ +\ (y\ +\ z)\ =\ y\ +\ (x\

 +\ z)

 \rulename{add_left_commute}

 \end{isabelle}

 The name \isa{add_ac} refers to the list of all three theorems, similarly

 there is \isa{mult_ac}.  Here is an example of the sorting effect.  Start

 with this goal:

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

 \subsection{The type of integers, {\tt\slshape int}}

 Reasoning methods resemble those for the natural numbers, but

 induction and the constant \isa{Suc} are not available.

 Concerning simplifier tricks, we have no need to eliminate subtraction (it

 is well-behaved), but the simplifier can sort the operands of integer

 operators.  The name \isa{zadd_ac} refers to the associativity and

 commutativity theorems for integer addition, while \isa{zmult_ac} has the

 analogous theorems for multiplication.  The prefix~\isa{z} in many theorem

 names recalls the use of $\Bbb{Z}$ to denote the set of integers.

 For division and remainder, the treatment of negative divisors follows

 traditional 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.

 The library provides many lemmas for proving inequalities involving integer

 multiplication and division, similar to those shown above for

 type~\isa{nat}.  The absolute value function \isa{abs} is

 defined for the integers; we have for example the obvious law

 \begin{isabelle}

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

 \rulename{abs_mult}

 \end{isabelle}

 Again, 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{zmod_zadd1_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$.

 \subsection{The type of real numbers, {\tt\slshape real}}

 The real numbers enjoy two significant properties that the integers lack. 

 They are

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

 This property follows from the division laws, since if $x<y$ then between

 them lies $(x+y)/2$.  The second property is that they are

 \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 is long and technical.  Rather than

 reproducing it here, we refer you to the theory \texttt{RComplete} in

 directory \texttt{Real}.

 Density is trivial to express:

 \begin{isabelle}

 x\ <\ y\ \isasymLongrightarrow \ \isasymexists r.\ x\ <\ r\ \isasymand \ r\ <\ y%

 \rulename{real_dense}

 \end{isabelle}

 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}

 x\ *\ (y\ /\ z)\ =\ x\ *\ y\ /\ z%

 \rulename{real_times_divide1_eq}\isanewline

 y\ /\ z\ *\ x\ =\ y\ *\ x\ /\ z%

 \rulename{real_times_divide2_eq}\isanewline

 x\ /\ (y\ /\ z)\ =\ x\ *\ z\ /\ y%

 \rulename{real_divide_divide1_eq}\isanewline

 x\ /\ y\ /\ z\ =\ x\ /\ (y\ *\ z)

 \rulename{real_divide_divide2_eq}

 \end{isabelle}

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

 then be cancelled:

 \begin{isabelle}

 -\ x\ /\ y\ =\ -\ (x\ /\ y)

 \rulename{real_minus_divide_eq}\isanewline

 x\ /\ -\ y\ =\ -\ (x\ /\ y)

 \rulename{real_divide_minus_eq}

 \end{isabelle}

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

 simplification rule.

 \begin{isabelle}

 (x\ +\ y)\ /\ z\ =\ x\ /\ z\ +\ y\ /\ z%

 \rulename{real_add_divide_distrib}

 \end{isabelle}

 As with the other numeric types, the simplifier can sort the operands of

 addition and multiplication.  The name \isa{real_add_ac} refers to the

 associativity and commutativity theorems for addition, while similarly

 \isa{real_mult_ac} contains those properties for multiplication. 

 The absolute value function \isa{abs} is

 defined for the reals, along with many theorems such as this one about

 exponentiation:

 \begin{isabelle}

 \isasymbar r\isasymbar \ \isacharcircum \ n\ =\ \isasymbar r\ \isacharcircum \ n\isasymbar 

 \rulename{realpow_abs}

 \end{isabelle}

 \emph{Note}: Type \isa{real} is only available in the logic HOL-Real, which

 is  HOL extended with the rather substantial development of the real

 numbers.  Base your theory upon theory \isa{Real}, not the usual \isa{Main}.

 Also distributed with Isabelle is HOL-Hyperreal,

 whose theory \isa{Hyperreal} defines the type \isa{hypreal} of non-standard

 reals.  These

 \textbf{hyperreals} include infinitesimals, which represent infinitely

 small and infinitely large quantities; they facilitate proofs

 about limits, differentiation and integration.  The development defines an

 infinitely large number, \isa{omega} and an infinitely small positive

 number, \isa{epsilon}.  Also available is the approximates relation,

 written $\approx$.