doc-src/TutorialI/Types/numerics.tex
author nipkow
Tue Mar 03 17:05:18 2009 +0100 (2009-03-03)
changeset 30224 79136ce06bdb
parent 30200 0db3a35eab01
child 30242 aea5d7fa7ef5
permissions -rw-r--r--
removed and renamed redundant lemmas
paulson@10794
     1
% $Id$
paulson@11389
     2
paulson@11389
     3
\section{Numbers}
paulson@11389
     4
\label{sec:numbers}
paulson@11389
     5
paulson@11494
     6
\index{numbers|(}%
paulson@11174
     7
Until now, our numerical examples have used the type of \textbf{natural
paulson@11174
     8
numbers},
paulson@10594
     9
\isa{nat}.  This is a recursive datatype generated by the constructors
paulson@10594
    10
zero  and successor, so it works well with inductive proofs and primitive
paulson@11174
    11
recursive function definitions.  HOL also provides the type
paulson@10794
    12
\isa{int} of \textbf{integers}, which lack induction but support true
paulson@14400
    13
subtraction.  With subtraction, arithmetic reasoning is easier, which makes
paulson@14400
    14
the integers preferable to the natural numbers for
paulson@14400
    15
complicated arithmetic expressions, even if they are non-negative.  The logic HOL-Complex also has the types
paulson@14400
    16
\isa{rat}, \isa{real} and \isa{complex}: the rational, real and complex numbers.  Isabelle has no 
paulson@13979
    17
subtyping,  so the numeric
paulson@13979
    18
types are distinct and there are functions to convert between them.
paulson@14400
    19
Most numeric operations are overloaded: the same symbol can be
paulson@11174
    20
used at all numeric types. Table~\ref{tab:overloading} in the appendix
paulson@11174
    21
shows the most important operations, together with the priorities of the
paulson@14400
    22
infix symbols. Algebraic properties are organized using type classes
paulson@14400
    23
around algebraic concepts such as rings and fields;
paulson@14400
    24
a property such as the commutativity of addition is a single theorem 
paulson@14400
    25
(\isa{add_commute}) that applies to all numeric types.
paulson@10594
    26
paulson@11416
    27
\index{linear arithmetic}%
paulson@10594
    28
Many theorems involving numeric types can be proved automatically by
paulson@10594
    29
Isabelle's arithmetic decision procedure, the method
paulson@11416
    30
\methdx{arith}.  Linear arithmetic comprises addition, subtraction
paulson@10594
    31
and multiplication by constant factors; subterms involving other operators
paulson@10594
    32
are regarded as variables.  The procedure can be slow, especially if the
paulson@10594
    33
subgoal to be proved involves subtraction over type \isa{nat}, which 
nipkow@13996
    34
causes case splits.  On types \isa{nat} and \isa{int}, \methdx{arith}
paulson@14400
    35
can deal with quantifiers---this is known as Presburger arithmetic---whereas on type \isa{real} it cannot.
paulson@10594
    36
paulson@10594
    37
The simplifier reduces arithmetic expressions in other
paulson@10594
    38
ways, such as dividing through by common factors.  For problems that lie
paulson@10881
    39
outside the scope of automation, HOL provides hundreds of
paulson@10594
    40
theorems about multiplication, division, etc., that can be brought to
paulson@10881
    41
bear.  You can locate them using Proof General's Find
paulson@10881
    42
button.  A few lemmas are given below to show what
paulson@10794
    43
is available.
paulson@10594
    44
paulson@10594
    45
\subsection{Numeric Literals}
nipkow@10779
    46
\label{sec:numerals}
paulson@10594
    47
paulson@11416
    48
\index{numeric literals|(}%
paulson@12156
    49
The constants \cdx{0} and \cdx{1} are overloaded.  They denote zero and one,
paulson@12156
    50
respectively, for all numeric types.  Other values are expressed by numeric
wenzelm@21243
    51
literals, which consist of one or more decimal digits optionally preceeded by a minus sign (\isa{-}).  Examples are \isa{2}, \isa{-3} and
wenzelm@21243
    52
\isa{441223334678}.  Literals are available for the types of natural
wenzelm@21243
    53
numbers, integers, rationals, reals, etc.; they denote integer values of
wenzelm@21243
    54
arbitrary size.
paulson@10594
    55
paulson@10594
    56
Literals look like constants, but they abbreviate 
paulson@12156
    57
terms representing the number in a two's complement binary notation. 
paulson@10794
    58
Isabelle performs arithmetic on literals by rewriting rather 
paulson@10594
    59
than using the hardware arithmetic. In most cases arithmetic 
paulson@14400
    60
is fast enough, even for numbers in the millions. The arithmetic operations 
paulson@10794
    61
provided for literals include addition, subtraction, multiplication, 
paulson@10794
    62
integer division and remainder.  Fractions of literals (expressed using
paulson@10794
    63
division) are reduced to lowest terms.
paulson@10594
    64
paulson@11416
    65
\begin{warn}\index{overloading!and arithmetic}
paulson@10794
    66
The arithmetic operators are 
paulson@10594
    67
overloaded, so you must be careful to ensure that each numeric 
paulson@10594
    68
expression refers to a specific type, if necessary by inserting 
paulson@10594
    69
type constraints.  Here is an example of what can go wrong:
paulson@10794
    70
\par
paulson@10594
    71
\begin{isabelle}
paulson@12156
    72
\isacommand{lemma}\ "2\ *\ m\ =\ m\ +\ m"
paulson@10594
    73
\end{isabelle}
paulson@10594
    74
%
paulson@10594
    75
Carefully observe how Isabelle displays the subgoal:
paulson@10594
    76
\begin{isabelle}
paulson@12156
    77
\ 1.\ (2::'a)\ *\ m\ =\ m\ +\ m
paulson@10594
    78
\end{isabelle}
paulson@12156
    79
The type \isa{'a} given for the literal \isa{2} warns us that no numeric
paulson@10594
    80
type has been specified.  The problem is underspecified.  Given a type
paulson@10594
    81
constraint such as \isa{nat}, \isa{int} or \isa{real}, it becomes trivial.
paulson@10794
    82
\end{warn}
paulson@10794
    83
paulson@10881
    84
\begin{warn}
paulson@11428
    85
\index{recdef@\isacommand {recdef} (command)!and numeric literals}  
paulson@11416
    86
Numeric literals are not constructors and therefore
paulson@11416
    87
must not be used in patterns.  For example, this declaration is
paulson@11416
    88
rejected:
paulson@10881
    89
\begin{isabelle}
paulson@10881
    90
\isacommand{recdef}\ h\ "\isacharbraceleft \isacharbraceright "\isanewline
paulson@12156
    91
"h\ 3\ =\ 2"\isanewline
nipkow@11148
    92
"h\ i\ \ =\ i"
paulson@10881
    93
\end{isabelle}
paulson@10881
    94
paulson@10881
    95
You should use a conditional expression instead:
paulson@10881
    96
\begin{isabelle}
paulson@12156
    97
"h\ i\ =\ (if\ i\ =\ 3\ then\ 2\ else\ i)"
paulson@10881
    98
\end{isabelle}
paulson@11416
    99
\index{numeric literals|)}
paulson@10881
   100
\end{warn}
paulson@10881
   101
paulson@10594
   102
nipkow@11216
   103
\subsection{The Type of Natural Numbers, {\tt\slshape nat}}
paulson@10594
   104
paulson@11416
   105
\index{natural numbers|(}\index{*nat (type)|(}%
paulson@10594
   106
This type requires no introduction: we have been using it from the
paulson@10794
   107
beginning.  Hundreds of theorems about the natural numbers are
wenzelm@21243
   108
proved in the theories \isa{Nat} and \isa{Divides}.  
paulson@14400
   109
Basic properties of addition and multiplication are available through the
paulson@14400
   110
axiomatic type class for semirings (\S\ref{sec:numeric-axclasses}).
paulson@10594
   111
paulson@10594
   112
\subsubsection{Literals}
paulson@11416
   113
\index{numeric literals!for type \protect\isa{nat}}%
paulson@12156
   114
The notational options for the natural  numbers are confusing.  Recall that an
paulson@12156
   115
overloaded constant can be defined independently for each type; the definition
paulson@12156
   116
of \cdx{1} for type \isa{nat} is
paulson@12156
   117
\begin{isabelle}
paulson@12156
   118
1\ \isasymequiv\ Suc\ 0
paulson@12156
   119
\rulename{One_nat_def}
paulson@12156
   120
\end{isabelle}
paulson@12156
   121
This is installed as a simplification rule, so the simplifier will replace
paulson@12156
   122
every occurrence of \isa{1::nat} by \isa{Suc\ 0}.  Literals are obviously
paulson@12156
   123
better than nested \isa{Suc}s at expressing large values.  But many theorems,
paulson@12156
   124
including the rewrite rules for primitive recursive functions, can only be
paulson@12156
   125
applied to terms of the form \isa{Suc\ $n$}.
paulson@12156
   126
paulson@12156
   127
The following default  simplification rules replace
paulson@10794
   128
small literals by zero and successor: 
paulson@10594
   129
\begin{isabelle}
paulson@12156
   130
2\ +\ n\ =\ Suc\ (Suc\ n)
paulson@10594
   131
\rulename{add_2_eq_Suc}\isanewline
paulson@12156
   132
n\ +\ 2\ =\ Suc\ (Suc\ n)
paulson@10594
   133
\rulename{add_2_eq_Suc'}
paulson@10594
   134
\end{isabelle}
paulson@12156
   135
It is less easy to transform \isa{100} into \isa{Suc\ 99} (for example), and
paulson@12156
   136
the simplifier will normally reverse this transformation.  Novices should
paulson@12156
   137
express natural numbers using \isa{0} and \isa{Suc} only.
paulson@10594
   138
paulson@10594
   139
\subsubsection{Division}
paulson@11416
   140
\index{division!for type \protect\isa{nat}}%
paulson@10881
   141
The infix operators \isa{div} and \isa{mod} are overloaded.
paulson@10881
   142
Isabelle/HOL provides the basic facts about quotient and remainder
paulson@10881
   143
on the natural numbers:
paulson@10594
   144
\begin{isabelle}
paulson@10594
   145
m\ mod\ n\ =\ (if\ m\ <\ n\ then\ m\ else\ (m\ -\ n)\ mod\ n)
paulson@10594
   146
\rulename{mod_if}\isanewline
paulson@10594
   147
m\ div\ n\ *\ n\ +\ m\ mod\ n\ =\ m%
paulson@11416
   148
\rulenamedx{mod_div_equality}
paulson@10594
   149
\end{isabelle}
paulson@10594
   150
paulson@10594
   151
Many less obvious facts about quotient and remainder are also provided. 
paulson@10594
   152
Here is a selection:
paulson@10594
   153
\begin{isabelle}
paulson@10594
   154
a\ *\ b\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c%
paulson@10594
   155
\rulename{div_mult1_eq}\isanewline
paulson@10594
   156
a\ *\ b\ mod\ c\ =\ a\ *\ (b\ mod\ c)\ mod\ c%
nipkow@30224
   157
\rulename{mod_mult_right_eq}\isanewline
paulson@10594
   158
a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%
paulson@10594
   159
\rulename{div_mult2_eq}\isanewline
paulson@10594
   160
a\ mod\ (b*c)\ =\ b * (a\ div\ b\ mod\ c)\ +\ a\ mod\ b%
paulson@10594
   161
\rulename{mod_mult2_eq}\isanewline
paulson@10594
   162
0\ <\ c\ \isasymLongrightarrow \ (c\ *\ a)\ div\ (c\ *\ b)\ =\ a\ div\ b%
paulson@14400
   163
\rulename{div_mult_mult1}\isanewline
paulson@14400
   164
(m\ mod\ n)\ *\ k\ =\ (m\ *\ k)\ mod\ (n\ *\ k)
paulson@14400
   165
\rulenamedx{mod_mult_distrib}\isanewline
paulson@14400
   166
m\ \isasymle \ n\ \isasymLongrightarrow \ m\ div\ k\ \isasymle \ n\ div\ k%
paulson@14400
   167
\rulename{div_le_mono}
paulson@10594
   168
\end{isabelle}
paulson@10594
   169
paulson@10594
   170
Surprisingly few of these results depend upon the
paulson@11416
   171
divisors' being nonzero.
paulson@11416
   172
\index{division!by zero}%
paulson@11416
   173
That is because division by
paulson@10794
   174
zero yields zero:
paulson@10594
   175
\begin{isabelle}
paulson@10594
   176
a\ div\ 0\ =\ 0
paulson@10594
   177
\rulename{DIVISION_BY_ZERO_DIV}\isanewline
paulson@10594
   178
a\ mod\ 0\ =\ a%
paulson@10594
   179
\rulename{DIVISION_BY_ZERO_MOD}
paulson@10594
   180
\end{isabelle}
paulson@14400
   181
In \isa{div_mult_mult1} above, one of
nipkow@11161
   182
the two divisors (namely~\isa{c}) must still be nonzero.
paulson@10594
   183
paulson@11416
   184
The \textbf{divides} relation\index{divides relation}
paulson@11416
   185
has the standard definition, which
paulson@10594
   186
is overloaded over all numeric types: 
paulson@10594
   187
\begin{isabelle}
paulson@10594
   188
m\ dvd\ n\ \isasymequiv\ {\isasymexists}k.\ n\ =\ m\ *\ k
paulson@11416
   189
\rulenamedx{dvd_def}
paulson@10594
   190
\end{isabelle}
paulson@10594
   191
%
paulson@10594
   192
Section~\ref{sec:proving-euclid} discusses proofs involving this
paulson@10594
   193
relation.  Here are some of the facts proved about it:
paulson@10594
   194
\begin{isabelle}
paulson@10594
   195
\isasymlbrakk m\ dvd\ n;\ n\ dvd\ m\isasymrbrakk \ \isasymLongrightarrow \ m\ =\ n%
paulson@11416
   196
\rulenamedx{dvd_anti_sym}\isanewline
paulson@10594
   197
\isasymlbrakk k\ dvd\ m;\ k\ dvd\ n\isasymrbrakk \ \isasymLongrightarrow \ k\ dvd\ (m\ +\ n)
paulson@11416
   198
\rulenamedx{dvd_add}
paulson@10594
   199
\end{isabelle}
paulson@10594
   200
paulson@14400
   201
\subsubsection{Subtraction}
paulson@14400
   202
paulson@14400
   203
There are no negative natural numbers, so \isa{m\ -\ n} equals zero unless 
paulson@14400
   204
\isa{m} exceeds~\isa{n}. The following is one of the few facts
paulson@10594
   205
about \isa{m\ -\ n} that is not subject to
paulson@14400
   206
the condition \isa{n\ \isasymle \  m}. 
paulson@14400
   207
\begin{isabelle}
paulson@14400
   208
(m\ -\ n)\ *\ k\ =\ m\ *\ k\ -\ n\ *\ k%
paulson@14400
   209
\rulenamedx{diff_mult_distrib}
paulson@14400
   210
\end{isabelle}
paulson@14400
   211
Natural number subtraction has few
paulson@10794
   212
nice properties; often you should remove it by simplifying with this split
paulson@14400
   213
rule.
paulson@10594
   214
\begin{isabelle}
paulson@10594
   215
P(a-b)\ =\ ((a<b\ \isasymlongrightarrow \ P\
paulson@10594
   216
0)\ \isasymand \ (\isasymforall d.\ a\ =\ b+d\ \isasymlongrightarrow \ P\
paulson@10594
   217
d))
paulson@10594
   218
\rulename{nat_diff_split}
paulson@10594
   219
\end{isabelle}
paulson@14400
   220
For example, splitting helps to prove the following fact.
paulson@10594
   221
\begin{isabelle}
paulson@12156
   222
\isacommand{lemma}\ "(n\ -\ 2)\ *\ (n\ +\ 2)\ =\ n\ *\ n\ -\ (4::nat)"\isanewline
paulson@12156
   223
\isacommand{apply}\ (simp\ split:\ nat_diff_split,\ clarify)\isanewline
paulson@12156
   224
\ 1.\ \isasymAnd d.\ \isasymlbrakk n\ <\ 2;\ n\ *\ n\ =\ 4\ +\ d\isasymrbrakk \ \isasymLongrightarrow \ d\ =\ 0
paulson@12156
   225
\end{isabelle}
paulson@12156
   226
The result lies outside the scope of linear arithmetic, but
paulson@12156
   227
 it is easily found
paulson@12156
   228
if we explicitly split \isa{n<2} as \isa{n=0} or \isa{n=1}:
paulson@12156
   229
\begin{isabelle}
paulson@12156
   230
\isacommand{apply}\ (subgoal_tac\ "n=0\ |\ n=1",\ force,\ arith)\isanewline
paulson@10594
   231
\isacommand{done}
paulson@14400
   232
\end{isabelle}%%%%%%
paulson@11416
   233
\index{natural numbers|)}\index{*nat (type)|)}
paulson@11416
   234
paulson@10594
   235
nipkow@11216
   236
\subsection{The Type of Integers, {\tt\slshape int}}
paulson@10594
   237
paulson@11416
   238
\index{integers|(}\index{*int (type)|(}%
paulson@14400
   239
Reasoning methods for the integers resemble those for the natural numbers, 
wenzelm@21243
   240
but induction and
wenzelm@21243
   241
the constant \isa{Suc} are not available.  HOL provides many lemmas for
wenzelm@21243
   242
proving inequalities involving integer multiplication and division, similar
wenzelm@21243
   243
to those shown above for type~\isa{nat}. The laws of addition, subtraction
wenzelm@21243
   244
and multiplication are available through the axiomatic type class for rings
wenzelm@21243
   245
(\S\ref{sec:numeric-axclasses}).
paulson@10794
   246
paulson@14400
   247
The \rmindex{absolute value} function \cdx{abs} is overloaded, and is 
paulson@14400
   248
defined for all types that involve negative numbers, including the integers.
paulson@10881
   249
The \isa{arith} method can prove facts about \isa{abs} automatically, 
paulson@10881
   250
though as it does so by case analysis, the cost can be exponential.
paulson@10881
   251
\begin{isabelle}
paulson@11174
   252
\isacommand{lemma}\ "abs\ (x+y)\ \isasymle \ abs\ x\ +\ abs\ (y\ ::\ int)"\isanewline
paulson@10881
   253
\isacommand{by}\ arith
paulson@10881
   254
\end{isabelle}
paulson@10794
   255
paulson@11416
   256
For division and remainder,\index{division!by negative numbers}
paulson@11416
   257
the treatment of negative divisors follows
paulson@10794
   258
mathematical practice: the sign of the remainder follows that
paulson@10594
   259
of the divisor:
paulson@10594
   260
\begin{isabelle}
paulson@12156
   261
0\ <\ b\ \isasymLongrightarrow \ 0\ \isasymle \ a\ mod\ b%
paulson@10594
   262
\rulename{pos_mod_sign}\isanewline
paulson@12156
   263
0\ <\ b\ \isasymLongrightarrow \ a\ mod\ b\ <\ b%
paulson@10594
   264
\rulename{pos_mod_bound}\isanewline
paulson@12156
   265
b\ <\ 0\ \isasymLongrightarrow \ a\ mod\ b\ \isasymle \ 0
paulson@10594
   266
\rulename{neg_mod_sign}\isanewline
paulson@12156
   267
b\ <\ 0\ \isasymLongrightarrow \ b\ <\ a\ mod\ b%
paulson@10594
   268
\rulename{neg_mod_bound}
paulson@10594
   269
\end{isabelle}
paulson@10594
   270
ML treats negative divisors in the same way, but most computer hardware
paulson@10594
   271
treats signed operands using the same rules as for multiplication.
paulson@10794
   272
Many facts about quotients and remainders are provided:
paulson@10594
   273
\begin{isabelle}
paulson@10594
   274
(a\ +\ b)\ div\ c\ =\isanewline
paulson@10594
   275
a\ div\ c\ +\ b\ div\ c\ +\ (a\ mod\ c\ +\ b\ mod\ c)\ div\ c%
paulson@10594
   276
\rulename{zdiv_zadd1_eq}
paulson@10594
   277
\par\smallskip
paulson@10594
   278
(a\ +\ b)\ mod\ c\ =\ (a\ mod\ c\ +\ b\ mod\ c)\ mod\ c%
nipkow@30224
   279
\rulename{mod_add_eq}
paulson@10594
   280
\end{isabelle}
paulson@10594
   281
paulson@10594
   282
\begin{isabelle}
paulson@10594
   283
(a\ *\ b)\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c%
paulson@10594
   284
\rulename{zdiv_zmult1_eq}\isanewline
paulson@10594
   285
(a\ *\ b)\ mod\ c\ =\ a\ *\ (b\ mod\ c)\ mod\ c%
paulson@10594
   286
\rulename{zmod_zmult1_eq}
paulson@10594
   287
\end{isabelle}
paulson@10594
   288
paulson@10594
   289
\begin{isabelle}
paulson@12156
   290
0\ <\ c\ \isasymLongrightarrow \ a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%
paulson@10594
   291
\rulename{zdiv_zmult2_eq}\isanewline
paulson@12156
   292
0\ <\ c\ \isasymLongrightarrow \ a\ mod\ (b*c)\ =\ b*(a\ div\ b\ mod\
paulson@10594
   293
c)\ +\ a\ mod\ b%
paulson@10594
   294
\rulename{zmod_zmult2_eq}
paulson@10594
   295
\end{isabelle}
paulson@10594
   296
The last two differ from their natural number analogues by requiring
paulson@10594
   297
\isa{c} to be positive.  Since division by zero yields zero, we could allow
paulson@10594
   298
\isa{c} to be zero.  However, \isa{c} cannot be negative: a counterexample
paulson@10594
   299
is
paulson@10594
   300
$\isa{a} = 7$, $\isa{b} = 2$ and $\isa{c} = -3$, when the left-hand side of
paulson@14400
   301
\isa{zdiv_zmult2_eq} is $-2$ while the right-hand side is~$-1$.
paulson@14400
   302
The prefix~\isa{z} in many theorem names recalls the use of $\mathbb{Z}$ to
paulson@14400
   303
denote the set of integers.%
paulson@11416
   304
\index{integers|)}\index{*int (type)|)}
paulson@10594
   305
paulson@13979
   306
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 $<$):
paulson@13750
   307
\begin{isabelle}
paulson@13750
   308
\isasymlbrakk k\ \isasymle \ i;\ P\ k;\ \isasymAnd i.\ \isasymlbrakk k\ \isasymle \ i;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i+1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%
paulson@13750
   309
\rulename{int_ge_induct}\isanewline
paulson@13750
   310
\isasymlbrakk k\ <\ i;\ P(k+1);\ \isasymAnd i.\ \isasymlbrakk k\ <\ i;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i+1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%
paulson@13750
   311
\rulename{int_gr_induct}\isanewline
paulson@13750
   312
\isasymlbrakk i\ \isasymle \ k;\ P\ k;\ \isasymAnd i.\ \isasymlbrakk i\ \isasymle \ k;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i-1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%
paulson@13750
   313
\rulename{int_le_induct}\isanewline
paulson@13750
   314
\isasymlbrakk i\ <\ k;\ P(k-1);\ \isasymAnd i.\ \isasymlbrakk i\ <\ k;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i-1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%
paulson@13750
   315
\rulename{int_less_induct}
paulson@13750
   316
\end{isabelle}
paulson@13750
   317
paulson@10594
   318
paulson@14400
   319
\subsection{The Types of Rational, Real and Complex Numbers}
nipkow@16359
   320
\label{sec:real}
paulson@10594
   321
paulson@14400
   322
\index{rational numbers|(}\index{*rat (type)|(}%
paulson@11416
   323
\index{real numbers|(}\index{*real (type)|(}%
paulson@14400
   324
\index{complex numbers|(}\index{*complex (type)|(}%
paulson@14400
   325
These types provide true division, the overloaded operator \isa{/}, 
paulson@14400
   326
which differs from the operator \isa{div} of the 
paulson@14400
   327
natural numbers and integers. The rationals and reals are 
paulson@14400
   328
\textbf{dense}: between every two distinct numbers lies another.
paulson@14400
   329
This property follows from the division laws, since if $x\not=y$ then $(x+y)/2$ lies between them:
paulson@10777
   330
\begin{isabelle}
paulson@14400
   331
a\ <\ b\ \isasymLongrightarrow \ \isasymexists r.\ a\ <\ r\ \isasymand \ r\ <\ b%
paulson@14295
   332
\rulename{dense}
paulson@10777
   333
\end{isabelle}
paulson@10777
   334
wenzelm@21243
   335
The real numbers are, moreover, \textbf{complete}: every set of reals that
wenzelm@21243
   336
is bounded above has a least upper bound.  Completeness distinguishes the
wenzelm@21243
   337
reals from the rationals, for which the set $\{x\mid x^2<2\}$ has no least
wenzelm@27093
   338
upper bound.  (It could only be $\surd2$, which is irrational.) The
wenzelm@21243
   339
formalization of completeness, which is complicated, 
wenzelm@21243
   340
can be found in theory \texttt{RComplete} of directory
wenzelm@21243
   341
\texttt{Real}.
paulson@14400
   342
paulson@14400
   343
Numeric literals\index{numeric literals!for type \protect\isa{real}}
paulson@14400
   344
for type \isa{real} have the same syntax as those for type
paulson@14400
   345
\isa{int} and only express integral values.  Fractions expressed
paulson@14400
   346
using the division operator are automatically simplified to lowest terms:
paulson@14400
   347
\begin{isabelle}
paulson@14400
   348
\ 1.\ P\ ((3\ /\ 4)\ *\ (8\ /\ 15))\isanewline
paulson@14400
   349
\isacommand{apply} simp\isanewline
paulson@14400
   350
\ 1.\ P\ (2\ /\ 5)
paulson@14400
   351
\end{isabelle}
paulson@14400
   352
Exponentiation can express floating-point values such as
paulson@14400
   353
\isa{2 * 10\isacharcircum6}, but at present no special simplification
paulson@14400
   354
is performed.
paulson@14400
   355
paulson@14400
   356
\begin{warn}
nipkow@16359
   357
Type \isa{real} is only available in the logic HOL-Complex, which is
nipkow@16359
   358
HOL extended with a definitional development of the real and complex
nipkow@16359
   359
numbers.  Base your theory upon theory \thydx{Complex_Main}, not the
nipkow@16523
   360
usual \isa{Main}, and set the Proof General menu item \pgmenu{Isabelle} $>$
nipkow@16523
   361
\pgmenu{Logics} $>$ \pgmenu{HOL-Complex}.%
paulson@14400
   362
\index{real numbers|)}\index{*real (type)|)}
paulson@14400
   363
\end{warn}
paulson@14400
   364
paulson@14400
   365
Also available in HOL-Complex is the
paulson@14400
   366
theory \isa{Hyperreal}, which define the type \tydx{hypreal} of 
paulson@14400
   367
\rmindex{non-standard reals}.  These
paulson@14400
   368
\textbf{hyperreals} include infinitesimals, which represent infinitely
paulson@14400
   369
small and infinitely large quantities; they facilitate proofs
paulson@14400
   370
about limits, differentiation and integration~\cite{fleuriot-jcm}.  The
paulson@14400
   371
development defines an infinitely large number, \isa{omega} and an
paulson@14400
   372
infinitely small positive number, \isa{epsilon}.  The 
paulson@14400
   373
relation $x\approx y$ means ``$x$ is infinitely close to~$y$.''
paulson@14400
   374
Theory \isa{Hyperreal} also defines transcendental functions such as sine,
paulson@14400
   375
cosine, exponential and logarithm --- even the versions for type
paulson@14400
   376
\isa{real}, because they are defined using nonstandard limits.%
paulson@14400
   377
\index{rational numbers|)}\index{*rat (type)|)}%
paulson@14400
   378
\index{real numbers|)}\index{*real (type)|)}%
paulson@14400
   379
\index{complex numbers|)}\index{*complex (type)|)}
paulson@14400
   380
paulson@14400
   381
paulson@14400
   382
\subsection{The Numeric Type Classes}\label{sec:numeric-axclasses}
paulson@14400
   383
paulson@14400
   384
Isabelle/HOL organises its numeric theories using axiomatic type classes.
paulson@14400
   385
Hundreds of basic properties are proved in the theory \isa{Ring_and_Field}.
paulson@14400
   386
These lemmas are available (as simprules if they were declared as such)
paulson@14400
   387
for all numeric types satisfying the necessary axioms. The theory defines
paulson@23525
   388
dozens of type classes, such as the following:
paulson@14400
   389
\begin{itemize}
paulson@14400
   390
\item 
wenzelm@21243
   391
\tcdx{semiring} and \tcdx{ordered_semiring}: a \emph{semiring}
paulson@23525
   392
provides the associative operators \isa{+} and~\isa{*}, with \isa{0} and~\isa{1}
paulson@23525
   393
as their respective identities. The operators enjoy the usual distributive law,
paulson@23525
   394
and addition (\isa{+}) is also commutative.
paulson@23525
   395
An \emph{ordered semiring} is also linearly
wenzelm@21243
   396
ordered, with addition and multiplication respecting the ordering. Type \isa{nat} is an ordered semiring.
paulson@14400
   397
\item 
wenzelm@21243
   398
\tcdx{ring} and \tcdx{ordered_ring}: a \emph{ring} extends a semiring
wenzelm@21243
   399
with unary minus (the additive inverse) and subtraction (both
wenzelm@21243
   400
denoted~\isa{-}). An \emph{ordered ring} includes the absolute value
wenzelm@21243
   401
function, \cdx{abs}. Type \isa{int} is an ordered ring.
paulson@14400
   402
\item 
wenzelm@21243
   403
\tcdx{field} and \tcdx{ordered_field}: a field extends a ring with the
wenzelm@27093
   404
multiplicative inverse (called simply \cdx{inverse} and division~(\isa{/})).
wenzelm@21243
   405
An ordered field is based on an ordered ring. Type \isa{complex} is a field, while type \isa{real} is an ordered field.
paulson@14400
   406
\item 
paulson@14400
   407
\tcdx{division_by_zero} includes all types where \isa{inverse 0 = 0}
paulson@14400
   408
and \isa{a / 0 = 0}. These include all of Isabelle's standard numeric types.
paulson@14400
   409
However, the basic properties of fields are derived without assuming
wenzelm@21243
   410
division by zero.
wenzelm@21243
   411
\end{itemize}
paulson@14400
   412
paulson@23525
   413
Hundreds of basic lemmas are proved, each of which
wenzelm@21243
   414
holds for all types in the corresponding type class. In most
paulson@23525
   415
cases, it is obvious whether a property is valid for a particular type. No
paulson@23525
   416
abstract properties involving subtraction hold for type \isa{nat};
paulson@23525
   417
instead, theorems such as
paulson@23525
   418
\isa{diff_mult_distrib} are proved specifically about subtraction on
wenzelm@21243
   419
type~\isa{nat}. All abstract properties involving division require a field.
wenzelm@21243
   420
Obviously, all properties involving orderings required an ordered
wenzelm@21243
   421
structure.
paulson@14400
   422
paulson@23504
   423
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:
paulson@14400
   424
\begin{isabelle}
paulson@14400
   425
(a\ *\ b\ =\ (0::'a))\ =\ (a\ =\ (0::'a)\ \isasymor \ b\ =\ (0::'a))
paulson@14400
   426
\rulename{mult_eq_0_iff}\isanewline
paulson@14400
   427
(a\ *\ c\ =\ b\ *\ c)\ =\ (c\ =\ (0::'a)\ \isasymor \ a\ =\ b)
paulson@14400
   428
\rulename{mult_cancel_right}
paulson@14400
   429
\end{isabelle}
nipkow@16412
   430
\begin{pgnote}
nipkow@16523
   431
Setting the flag \pgmenu{Isabelle} $>$ \pgmenu{Settings} $>$
nipkow@16523
   432
\pgmenu{Show Sorts} will display the type classes of all type variables.
nipkow@16412
   433
\end{pgnote}
nipkow@16412
   434
\noindent
paulson@23504
   435
Here is how the theorem \isa{mult_cancel_left} appears with the flag set.
paulson@14400
   436
\begin{isabelle}
paulson@23504
   437
((c::'a::ring_no_zero_divisors)\ *\ (a::'a::ring_no_zero_divisors) =\isanewline
paulson@23504
   438
\ c\ *\ (b::'a::ring_no_zero_divisors))\ =\isanewline
paulson@23504
   439
(c\ =\ (0::'a::ring_no_zero_divisors)\ \isasymor\ a\ =\ b)
paulson@14400
   440
\end{isabelle}
paulson@14400
   441
paulson@14400
   442
paulson@14400
   443
\subsubsection{Simplifying with the AC-Laws}
paulson@14400
   444
Suppose that two expressions are equal, differing only in 
paulson@14400
   445
associativity and commutativity of addition.  Simplifying with the
paulson@14400
   446
following equations sorts the terms and groups them to the right, making
paulson@14400
   447
the two expressions identical.
paulson@14400
   448
\begin{isabelle}
paulson@14400
   449
a\ +\ b\ +\ c\ =\ a\ +\ (b\ +\ c)
paulson@14400
   450
\rulenamedx{add_assoc}\isanewline
paulson@14400
   451
a\ +\ b\ =\ b\ +\ a%
paulson@14400
   452
\rulenamedx{add_commute}\isanewline
paulson@14400
   453
a\ +\ (b\ +\ c)\ =\ b\ +\ (a\ +\ c)
paulson@14400
   454
\rulename{add_left_commute}
paulson@14400
   455
\end{isabelle}
paulson@14400
   456
The name \isa{add_ac}\index{*add_ac (theorems)} 
paulson@14400
   457
refers to the list of all three theorems; similarly
paulson@14400
   458
there is \isa{mult_ac}.\index{*mult_ac (theorems)} 
paulson@14400
   459
They are all proved for semirings and therefore hold for all numeric types.
paulson@14400
   460
paulson@14400
   461
Here is an example of the sorting effect.  Start
paulson@14400
   462
with this goal, which involves type \isa{nat}.
paulson@14400
   463
\begin{isabelle}
paulson@14400
   464
\ 1.\ Suc\ (i\ +\ j\ *\ l\ *\ k\ +\ m\ *\ n)\ =\
paulson@14400
   465
f\ (n\ *\ m\ +\ i\ +\ k\ *\ j\ *\ l)
paulson@14400
   466
\end{isabelle}
paulson@14400
   467
%
paulson@14400
   468
Simplify using  \isa{add_ac} and \isa{mult_ac}.
paulson@14400
   469
\begin{isabelle}
paulson@14400
   470
\isacommand{apply}\ (simp\ add:\ add_ac\ mult_ac)
paulson@14400
   471
\end{isabelle}
paulson@14400
   472
%
paulson@14400
   473
Here is the resulting subgoal.
paulson@14400
   474
\begin{isabelle}
paulson@14400
   475
\ 1.\ Suc\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))\
paulson@14400
   476
=\ f\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))%
paulson@14400
   477
\end{isabelle}
paulson@14400
   478
paulson@14400
   479
paulson@14400
   480
\subsubsection{Division Laws for Fields}
paulson@14400
   481
paulson@10777
   482
Here is a selection of rules about the division operator.  The following
paulson@10777
   483
are installed as default simplification rules in order to express
paulson@10777
   484
combinations of products and quotients as rational expressions:
paulson@10777
   485
\begin{isabelle}
paulson@14288
   486
a\ *\ (b\ /\ c)\ =\ a\ *\ b\ /\ c
paulson@14288
   487
\rulename{times_divide_eq_right}\isanewline
paulson@14288
   488
b\ /\ c\ *\ a\ =\ b\ *\ a\ /\ c
paulson@14288
   489
\rulename{times_divide_eq_left}\isanewline
paulson@14288
   490
a\ /\ (b\ /\ c)\ =\ a\ *\ c\ /\ b
paulson@14288
   491
\rulename{divide_divide_eq_right}\isanewline
paulson@14288
   492
a\ /\ b\ /\ c\ =\ a\ /\ (b\ *\ c)
paulson@14288
   493
\rulename{divide_divide_eq_left}
paulson@10777
   494
\end{isabelle}
paulson@10777
   495
paulson@10777
   496
Signs are extracted from quotients in the hope that complementary terms can
paulson@10777
   497
then be cancelled:
paulson@10777
   498
\begin{isabelle}
paulson@14295
   499
-\ (a\ /\ b)\ =\ -\ a\ /\ b
paulson@14295
   500
\rulename{minus_divide_left}\isanewline
paulson@14295
   501
-\ (a\ /\ b)\ =\ a\ /\ -\ b
paulson@14295
   502
\rulename{minus_divide_right}
paulson@10777
   503
\end{isabelle}
paulson@10777
   504
paulson@10777
   505
The following distributive law is available, but it is not installed as a
paulson@10777
   506
simplification rule.
paulson@10777
   507
\begin{isabelle}
paulson@14295
   508
(a\ +\ b)\ /\ c\ =\ a\ /\ c\ +\ b\ /\ c%
paulson@14295
   509
\rulename{add_divide_distrib}
paulson@10777
   510
\end{isabelle}
paulson@10777
   511
paulson@14400
   512
paulson@14400
   513
\subsubsection{Absolute Value}
paulson@10594
   514
paulson@14400
   515
The \rmindex{absolute value} function \cdx{abs} is available for all 
paulson@14400
   516
ordered rings, including types \isa{int}, \isa{rat} and \isa{real}.
paulson@14400
   517
It satisfies many properties,
paulson@14400
   518
such as the following:
paulson@10777
   519
\begin{isabelle}
paulson@14400
   520
\isasymbar x\ *\ y\isasymbar \ =\ \isasymbar x\isasymbar \ *\ \isasymbar y\isasymbar 
paulson@14400
   521
\rulename{abs_mult}\isanewline
paulson@14400
   522
(\isasymbar a\isasymbar \ \isasymle \ b)\ =\ (a\ \isasymle \ b\ \isasymand \ -\ a\ \isasymle \ b)
paulson@14400
   523
\rulename{abs_le_iff}\isanewline
paulson@14400
   524
\isasymbar a\ +\ b\isasymbar \ \isasymle \ \isasymbar a\isasymbar \ +\ \isasymbar b\isasymbar 
paulson@14400
   525
\rulename{abs_triangle_ineq}
paulson@10777
   526
\end{isabelle}
paulson@10777
   527
paulson@14400
   528
\begin{warn}
paulson@14400
   529
The absolute value bars shown above cannot be typed on a keyboard.  They
paulson@14400
   530
can be entered using the X-symbol package.  In \textsc{ascii}, type \isa{abs x} to
paulson@14400
   531
get \isa{\isasymbar x\isasymbar}.
paulson@14400
   532
\end{warn}
paulson@11174
   533
paulson@11174
   534
paulson@14400
   535
\subsubsection{Raising to a Power}
paulson@10777
   536
paulson@14400
   537
Another type class, \tcdx{ringppower}, specifies rings that also have 
paulson@14400
   538
exponentation to a natural number power, defined using the obvious primitive
paulson@14400
   539
recursion. Theory \thydx{Power} proves various theorems, such as the 
paulson@14400
   540
following.
paulson@14400
   541
\begin{isabelle}
paulson@14400
   542
a\ \isacharcircum \ (m\ +\ n)\ =\ a\ \isacharcircum \ m\ *\ a\ \isacharcircum \ n%
paulson@14400
   543
\rulename{power_add}\isanewline
paulson@14400
   544
a\ \isacharcircum \ (m\ *\ n)\ =\ (a\ \isacharcircum \ m)\ \isacharcircum \ n%
paulson@14400
   545
\rulename{power_mult}\isanewline
paulson@14400
   546
\isasymbar a\ \isacharcircum \ n\isasymbar \ =\ \isasymbar a\isasymbar \ \isacharcircum \ n%
paulson@14400
   547
\rulename{power_abs}
paulson@14400
   548
\end{isabelle}%%%%%%%%%%%%%%%%%%%%%%%%%
nipkow@13996
   549
\index{numbers|)}