doc-src/TutorialI/Types/numerics.tex
author paulson
Mon Jan 12 16:51:45 2004 +0100 (2004-01-12)
changeset 14353 79f9fbef9106
parent 14295 7f115e5c5de4
child 14400 6069098854b9
permissions -rw-r--r--
Added lemmas to Ring_and_Field with slightly modified simplification rules

Deleted some little-used integer theorems, replacing them by the generic ones
in Ring_and_Field

Consolidated integer powers
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@11174
    13
subtraction.  The integers are preferable to the natural numbers for reasoning about
paulson@11174
    14
complicated arithmetic expressions, even for some expressions whose
paulson@13979
    15
value is non-negative.  The logic HOL-Complex also has the types
paulson@13979
    16
\isa{real} and \isa{complex}: the 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@11174
    19
Fortunately 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@11174
    22
infix symbols.
paulson@10594
    23
paulson@11416
    24
\index{linear arithmetic}%
paulson@10594
    25
Many theorems involving numeric types can be proved automatically by
paulson@10594
    26
Isabelle's arithmetic decision procedure, the method
paulson@11416
    27
\methdx{arith}.  Linear arithmetic comprises addition, subtraction
paulson@10594
    28
and multiplication by constant factors; subterms involving other operators
paulson@10594
    29
are regarded as variables.  The procedure can be slow, especially if the
paulson@10594
    30
subgoal to be proved involves subtraction over type \isa{nat}, which 
nipkow@13996
    31
causes case splits.  On types \isa{nat} and \isa{int}, \methdx{arith}
nipkow@13996
    32
can deal with quantifiers (this is known as ``Presburger Arithmetic''),
nipkow@13996
    33
whereas on type \isa{real} it cannot.
paulson@10594
    34
paulson@10594
    35
The simplifier reduces arithmetic expressions in other
paulson@10594
    36
ways, such as dividing through by common factors.  For problems that lie
paulson@10881
    37
outside the scope of automation, HOL provides hundreds of
paulson@10594
    38
theorems about multiplication, division, etc., that can be brought to
paulson@10881
    39
bear.  You can locate them using Proof General's Find
paulson@10881
    40
button.  A few lemmas are given below to show what
paulson@10794
    41
is available.
paulson@10594
    42
paulson@10594
    43
\subsection{Numeric Literals}
nipkow@10779
    44
\label{sec:numerals}
paulson@10594
    45
paulson@11416
    46
\index{numeric literals|(}%
paulson@12156
    47
The constants \cdx{0} and \cdx{1} are overloaded.  They denote zero and one,
paulson@12156
    48
respectively, for all numeric types.  Other values are expressed by numeric
paulson@12156
    49
literals, which consist of one or more decimal digits optionally preceeded by
paulson@12156
    50
a minus sign (\isa{-}).  Examples are \isa{2}, \isa{-3} and
paulson@12156
    51
\isa{441223334678}.  Literals are available for the types of natural numbers,
paulson@12156
    52
integers and reals; they denote integer values of arbitrary size.
paulson@10594
    53
paulson@10594
    54
Literals look like constants, but they abbreviate 
paulson@12156
    55
terms representing the number in a two's complement binary notation. 
paulson@10794
    56
Isabelle performs arithmetic on literals by rewriting rather 
paulson@10594
    57
than using the hardware arithmetic. In most cases arithmetic 
paulson@10594
    58
is fast enough, even for large numbers. The arithmetic operations 
paulson@10794
    59
provided for literals include addition, subtraction, multiplication, 
paulson@10794
    60
integer division and remainder.  Fractions of literals (expressed using
paulson@10794
    61
division) are reduced to lowest terms.
paulson@10594
    62
paulson@11416
    63
\begin{warn}\index{overloading!and arithmetic}
paulson@10794
    64
The arithmetic operators are 
paulson@10594
    65
overloaded, so you must be careful to ensure that each numeric 
paulson@10594
    66
expression refers to a specific type, if necessary by inserting 
paulson@10594
    67
type constraints.  Here is an example of what can go wrong:
paulson@10794
    68
\par
paulson@10594
    69
\begin{isabelle}
paulson@12156
    70
\isacommand{lemma}\ "2\ *\ m\ =\ m\ +\ m"
paulson@10594
    71
\end{isabelle}
paulson@10594
    72
%
paulson@10594
    73
Carefully observe how Isabelle displays the subgoal:
paulson@10594
    74
\begin{isabelle}
paulson@12156
    75
\ 1.\ (2::'a)\ *\ m\ =\ m\ +\ m
paulson@10594
    76
\end{isabelle}
paulson@12156
    77
The type \isa{'a} given for the literal \isa{2} warns us that no numeric
paulson@10594
    78
type has been specified.  The problem is underspecified.  Given a type
paulson@10594
    79
constraint such as \isa{nat}, \isa{int} or \isa{real}, it becomes trivial.
paulson@10794
    80
\end{warn}
paulson@10794
    81
paulson@10881
    82
\begin{warn}
paulson@11428
    83
\index{recdef@\isacommand {recdef} (command)!and numeric literals}  
paulson@11416
    84
Numeric literals are not constructors and therefore
paulson@11416
    85
must not be used in patterns.  For example, this declaration is
paulson@11416
    86
rejected:
paulson@10881
    87
\begin{isabelle}
paulson@10881
    88
\isacommand{recdef}\ h\ "\isacharbraceleft \isacharbraceright "\isanewline
paulson@12156
    89
"h\ 3\ =\ 2"\isanewline
nipkow@11148
    90
"h\ i\ \ =\ i"
paulson@10881
    91
\end{isabelle}
paulson@10881
    92
paulson@10881
    93
You should use a conditional expression instead:
paulson@10881
    94
\begin{isabelle}
paulson@12156
    95
"h\ i\ =\ (if\ i\ =\ 3\ then\ 2\ else\ i)"
paulson@10881
    96
\end{isabelle}
paulson@11416
    97
\index{numeric literals|)}
paulson@10881
    98
\end{warn}
paulson@10881
    99
paulson@10594
   100
paulson@10594
   101
nipkow@11216
   102
\subsection{The Type of Natural Numbers, {\tt\slshape nat}}
paulson@10594
   103
paulson@11416
   104
\index{natural numbers|(}\index{*nat (type)|(}%
paulson@10594
   105
This type requires no introduction: we have been using it from the
paulson@10794
   106
beginning.  Hundreds of theorems about the natural numbers are
paulson@10594
   107
proved in the theories \isa{Nat}, \isa{NatArith} and \isa{Divides}.  Only
paulson@10594
   108
in exceptional circumstances should you resort to induction.
paulson@10594
   109
paulson@10594
   110
\subsubsection{Literals}
paulson@11416
   111
\index{numeric literals!for type \protect\isa{nat}}%
paulson@12156
   112
The notational options for the natural  numbers are confusing.  Recall that an
paulson@12156
   113
overloaded constant can be defined independently for each type; the definition
paulson@12156
   114
of \cdx{1} for type \isa{nat} is
paulson@12156
   115
\begin{isabelle}
paulson@12156
   116
1\ \isasymequiv\ Suc\ 0
paulson@12156
   117
\rulename{One_nat_def}
paulson@12156
   118
\end{isabelle}
paulson@12156
   119
This is installed as a simplification rule, so the simplifier will replace
paulson@12156
   120
every occurrence of \isa{1::nat} by \isa{Suc\ 0}.  Literals are obviously
paulson@12156
   121
better than nested \isa{Suc}s at expressing large values.  But many theorems,
paulson@12156
   122
including the rewrite rules for primitive recursive functions, can only be
paulson@12156
   123
applied to terms of the form \isa{Suc\ $n$}.
paulson@12156
   124
paulson@12156
   125
The following default  simplification rules replace
paulson@10794
   126
small literals by zero and successor: 
paulson@10594
   127
\begin{isabelle}
paulson@12156
   128
2\ +\ n\ =\ Suc\ (Suc\ n)
paulson@10594
   129
\rulename{add_2_eq_Suc}\isanewline
paulson@12156
   130
n\ +\ 2\ =\ Suc\ (Suc\ n)
paulson@10594
   131
\rulename{add_2_eq_Suc'}
paulson@10594
   132
\end{isabelle}
paulson@12156
   133
It is less easy to transform \isa{100} into \isa{Suc\ 99} (for example), and
paulson@12156
   134
the simplifier will normally reverse this transformation.  Novices should
paulson@12156
   135
express natural numbers using \isa{0} and \isa{Suc} only.
paulson@10594
   136
paulson@10594
   137
\subsubsection{Typical lemmas}
paulson@10594
   138
Inequalities involving addition and subtraction alone can be proved
paulson@10594
   139
automatically.  Lemmas such as these can be used to prove inequalities
paulson@10594
   140
involving multiplication and division:
paulson@10594
   141
\begin{isabelle}
paulson@10594
   142
\isasymlbrakk i\ \isasymle \ j;\ k\ \isasymle \ l\isasymrbrakk \ \isasymLongrightarrow \ i\ *\ k\ \isasymle \ j\ *\ l%
paulson@10594
   143
\rulename{mult_le_mono}\isanewline
paulson@10594
   144
\isasymlbrakk i\ <\ j;\ 0\ <\ k\isasymrbrakk \ \isasymLongrightarrow \ i\
paulson@10594
   145
*\ k\ <\ j\ *\ k%
paulson@10594
   146
\rulename{mult_less_mono1}\isanewline
paulson@10594
   147
m\ \isasymle \ n\ \isasymLongrightarrow \ m\ div\ k\ \isasymle \ n\ div\ k%
paulson@10594
   148
\rulename{div_le_mono}
paulson@10594
   149
\end{isabelle}
paulson@10594
   150
%
paulson@10594
   151
Various distributive laws concerning multiplication are available:
paulson@10594
   152
\begin{isabelle}
paulson@10594
   153
(m\ +\ n)\ *\ k\ =\ m\ *\ k\ +\ n\ *\ k%
paulson@11416
   154
\rulenamedx{add_mult_distrib}\isanewline
paulson@10594
   155
(m\ -\ n)\ *\ k\ =\ m\ *\ k\ -\ n\ *\ k%
paulson@11416
   156
\rulenamedx{diff_mult_distrib}\isanewline
paulson@10594
   157
(m\ mod\ n)\ *\ k\ =\ (m\ *\ k)\ mod\ (n\ *\ k)
paulson@11416
   158
\rulenamedx{mod_mult_distrib}
paulson@10594
   159
\end{isabelle}
paulson@10594
   160
paulson@10594
   161
\subsubsection{Division}
paulson@11416
   162
\index{division!for type \protect\isa{nat}}%
paulson@10881
   163
The infix operators \isa{div} and \isa{mod} are overloaded.
paulson@10881
   164
Isabelle/HOL provides the basic facts about quotient and remainder
paulson@10881
   165
on the natural numbers:
paulson@10594
   166
\begin{isabelle}
paulson@10594
   167
m\ mod\ n\ =\ (if\ m\ <\ n\ then\ m\ else\ (m\ -\ n)\ mod\ n)
paulson@10594
   168
\rulename{mod_if}\isanewline
paulson@10594
   169
m\ div\ n\ *\ n\ +\ m\ mod\ n\ =\ m%
paulson@11416
   170
\rulenamedx{mod_div_equality}
paulson@10594
   171
\end{isabelle}
paulson@10594
   172
paulson@10594
   173
Many less obvious facts about quotient and remainder are also provided. 
paulson@10594
   174
Here is a selection:
paulson@10594
   175
\begin{isabelle}
paulson@10594
   176
a\ *\ b\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c%
paulson@10594
   177
\rulename{div_mult1_eq}\isanewline
paulson@10594
   178
a\ *\ b\ mod\ c\ =\ a\ *\ (b\ mod\ c)\ mod\ c%
paulson@10594
   179
\rulename{mod_mult1_eq}\isanewline
paulson@10594
   180
a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%
paulson@10594
   181
\rulename{div_mult2_eq}\isanewline
paulson@10594
   182
a\ mod\ (b*c)\ =\ b * (a\ div\ b\ mod\ c)\ +\ a\ mod\ b%
paulson@10594
   183
\rulename{mod_mult2_eq}\isanewline
paulson@10594
   184
0\ <\ c\ \isasymLongrightarrow \ (c\ *\ a)\ div\ (c\ *\ b)\ =\ a\ div\ b%
paulson@10594
   185
\rulename{div_mult_mult1}
paulson@10594
   186
\end{isabelle}
paulson@10594
   187
paulson@10594
   188
Surprisingly few of these results depend upon the
paulson@11416
   189
divisors' being nonzero.
paulson@11416
   190
\index{division!by zero}%
paulson@11416
   191
That is because division by
paulson@10794
   192
zero yields zero:
paulson@10594
   193
\begin{isabelle}
paulson@10594
   194
a\ div\ 0\ =\ 0
paulson@10594
   195
\rulename{DIVISION_BY_ZERO_DIV}\isanewline
paulson@10594
   196
a\ mod\ 0\ =\ a%
paulson@10594
   197
\rulename{DIVISION_BY_ZERO_MOD}
paulson@10594
   198
\end{isabelle}
paulson@10594
   199
As a concession to convention, these equations are not installed as default
paulson@11174
   200
simplification rules.  In \isa{div_mult_mult1} above, one of
nipkow@11161
   201
the two divisors (namely~\isa{c}) must still be nonzero.
paulson@10594
   202
paulson@11416
   203
The \textbf{divides} relation\index{divides relation}
paulson@11416
   204
has the standard definition, which
paulson@10594
   205
is overloaded over all numeric types: 
paulson@10594
   206
\begin{isabelle}
paulson@10594
   207
m\ dvd\ n\ \isasymequiv\ {\isasymexists}k.\ n\ =\ m\ *\ k
paulson@11416
   208
\rulenamedx{dvd_def}
paulson@10594
   209
\end{isabelle}
paulson@10594
   210
%
paulson@10594
   211
Section~\ref{sec:proving-euclid} discusses proofs involving this
paulson@10594
   212
relation.  Here are some of the facts proved about it:
paulson@10594
   213
\begin{isabelle}
paulson@10594
   214
\isasymlbrakk m\ dvd\ n;\ n\ dvd\ m\isasymrbrakk \ \isasymLongrightarrow \ m\ =\ n%
paulson@11416
   215
\rulenamedx{dvd_anti_sym}\isanewline
paulson@10594
   216
\isasymlbrakk k\ dvd\ m;\ k\ dvd\ n\isasymrbrakk \ \isasymLongrightarrow \ k\ dvd\ (m\ +\ n)
paulson@11416
   217
\rulenamedx{dvd_add}
paulson@10594
   218
\end{isabelle}
paulson@10594
   219
nipkow@11216
   220
\subsubsection{Simplifier Tricks}
paulson@10594
   221
The rule \isa{diff_mult_distrib} shown above is one of the few facts
paulson@10594
   222
about \isa{m\ -\ n} that is not subject to
paulson@10594
   223
the condition \isa{n\ \isasymle \  m}.  Natural number subtraction has few
paulson@10794
   224
nice properties; often you should remove it by simplifying with this split
paulson@10794
   225
rule:
paulson@10594
   226
\begin{isabelle}
paulson@10594
   227
P(a-b)\ =\ ((a<b\ \isasymlongrightarrow \ P\
paulson@10594
   228
0)\ \isasymand \ (\isasymforall d.\ a\ =\ b+d\ \isasymlongrightarrow \ P\
paulson@10594
   229
d))
paulson@10594
   230
\rulename{nat_diff_split}
paulson@10594
   231
\end{isabelle}
paulson@12156
   232
For example, splitting helps to prove the following fact:
paulson@10594
   233
\begin{isabelle}
paulson@12156
   234
\isacommand{lemma}\ "(n\ -\ 2)\ *\ (n\ +\ 2)\ =\ n\ *\ n\ -\ (4::nat)"\isanewline
paulson@12156
   235
\isacommand{apply}\ (simp\ split:\ nat_diff_split,\ clarify)\isanewline
paulson@12156
   236
\ 1.\ \isasymAnd d.\ \isasymlbrakk n\ <\ 2;\ n\ *\ n\ =\ 4\ +\ d\isasymrbrakk \ \isasymLongrightarrow \ d\ =\ 0
paulson@12156
   237
\end{isabelle}
paulson@12156
   238
The result lies outside the scope of linear arithmetic, but
paulson@12156
   239
 it is easily found
paulson@12156
   240
if we explicitly split \isa{n<2} as \isa{n=0} or \isa{n=1}:
paulson@12156
   241
\begin{isabelle}
paulson@12156
   242
\isacommand{apply}\ (subgoal_tac\ "n=0\ |\ n=1",\ force,\ arith)\isanewline
paulson@10594
   243
\isacommand{done}
paulson@10594
   244
\end{isabelle}
paulson@10594
   245
paulson@10594
   246
Suppose that two expressions are equal, differing only in 
paulson@10594
   247
associativity and commutativity of addition.  Simplifying with the
paulson@10594
   248
following equations sorts the terms and groups them to the right, making
paulson@10594
   249
the two expressions identical:
paulson@10594
   250
\begin{isabelle}
paulson@10594
   251
m\ +\ n\ +\ k\ =\ m\ +\ (n\ +\ k)
paulson@11416
   252
\rulenamedx{add_assoc}\isanewline
paulson@10594
   253
m\ +\ n\ =\ n\ +\ m%
paulson@11416
   254
\rulenamedx{add_commute}\isanewline
paulson@10594
   255
x\ +\ (y\ +\ z)\ =\ y\ +\ (x\
paulson@10594
   256
+\ z)
paulson@10594
   257
\rulename{add_left_commute}
paulson@10594
   258
\end{isabelle}
paulson@11494
   259
The name \isa{add_ac}\index{*add_ac (theorems)} 
paulson@11494
   260
refers to the list of all three theorems; similarly
paulson@11494
   261
there is \isa{mult_ac}.\index{*mult_ac (theorems)} 
paulson@11494
   262
Here is an example of the sorting effect.  Start
paulson@10594
   263
with this goal:
paulson@10594
   264
\begin{isabelle}
paulson@10594
   265
\ 1.\ Suc\ (i\ +\ j\ *\ l\ *\ k\ +\ m\ *\ n)\ =\
paulson@10594
   266
f\ (n\ *\ m\ +\ i\ +\ k\ *\ j\ *\ l)
paulson@10594
   267
\end{isabelle}
paulson@10594
   268
%
paulson@10594
   269
Simplify using  \isa{add_ac} and \isa{mult_ac}:
paulson@10594
   270
\begin{isabelle}
paulson@10594
   271
\isacommand{apply}\ (simp\ add:\ add_ac\ mult_ac)
paulson@10594
   272
\end{isabelle}
paulson@10594
   273
%
paulson@10594
   274
Here is the resulting subgoal:
paulson@10594
   275
\begin{isabelle}
paulson@10594
   276
\ 1.\ Suc\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))\
paulson@10594
   277
=\ f\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))%
paulson@11416
   278
\end{isabelle}%
paulson@11416
   279
\index{natural numbers|)}\index{*nat (type)|)}
paulson@11416
   280
paulson@10594
   281
paulson@10594
   282
nipkow@11216
   283
\subsection{The Type of Integers, {\tt\slshape int}}
paulson@10594
   284
paulson@11416
   285
\index{integers|(}\index{*int (type)|(}%
paulson@10794
   286
Reasoning methods resemble those for the natural numbers, but induction and
paulson@10881
   287
the constant \isa{Suc} are not available.  HOL provides many lemmas
paulson@10794
   288
for proving inequalities involving integer multiplication and division,
paulson@10794
   289
similar to those shown above for type~\isa{nat}.  
paulson@10794
   290
paulson@11416
   291
The \rmindex{absolute value} function \cdx{abs} is overloaded for the numeric types.
paulson@10794
   292
It is defined for the integers; we have for example the obvious law
paulson@10794
   293
\begin{isabelle}
paulson@10794
   294
\isasymbar x\ *\ y\isasymbar \ =\ \isasymbar x\isasymbar \ *\ \isasymbar y\isasymbar 
paulson@10794
   295
\rulename{abs_mult}
paulson@10794
   296
\end{isabelle}
paulson@10594
   297
paulson@10794
   298
\begin{warn}
paulson@10794
   299
The absolute value bars shown above cannot be typed on a keyboard.  They
nipkow@10983
   300
can be entered using the X-symbol package.  In \textsc{ascii}, type \isa{abs x} to
paulson@10794
   301
get \isa{\isasymbar x\isasymbar}.
paulson@10794
   302
\end{warn}
paulson@10794
   303
paulson@10881
   304
The \isa{arith} method can prove facts about \isa{abs} automatically, 
paulson@10881
   305
though as it does so by case analysis, the cost can be exponential.
paulson@10881
   306
\begin{isabelle}
paulson@11174
   307
\isacommand{lemma}\ "abs\ (x+y)\ \isasymle \ abs\ x\ +\ abs\ (y\ ::\ int)"\isanewline
paulson@10881
   308
\isacommand{by}\ arith
paulson@10881
   309
\end{isabelle}
paulson@10794
   310
paulson@10794
   311
Concerning simplifier tricks, we have no need to eliminate subtraction: it
paulson@10794
   312
is well-behaved.  As with the natural numbers, the simplifier can sort the
paulson@11494
   313
operands of sums and products.  The name \isa{zadd_ac}\index{*zadd_ac (theorems)}
paulson@11494
   314
refers to the
paulson@10794
   315
associativity and commutativity theorems for integer addition, while
paulson@11494
   316
\isa{zmult_ac}\index{*zmult_ac (theorems)}
paulson@11494
   317
has the analogous theorems for multiplication.  The
paulson@10794
   318
prefix~\isa{z} in many theorem names recalls the use of $\mathbb{Z}$ to
paulson@10794
   319
denote the set of integers.
paulson@10594
   320
paulson@11416
   321
For division and remainder,\index{division!by negative numbers}
paulson@11416
   322
the treatment of negative divisors follows
paulson@10794
   323
mathematical practice: the sign of the remainder follows that
paulson@10594
   324
of the divisor:
paulson@10594
   325
\begin{isabelle}
paulson@12156
   326
0\ <\ b\ \isasymLongrightarrow \ 0\ \isasymle \ a\ mod\ b%
paulson@10594
   327
\rulename{pos_mod_sign}\isanewline
paulson@12156
   328
0\ <\ b\ \isasymLongrightarrow \ a\ mod\ b\ <\ b%
paulson@10594
   329
\rulename{pos_mod_bound}\isanewline
paulson@12156
   330
b\ <\ 0\ \isasymLongrightarrow \ a\ mod\ b\ \isasymle \ 0
paulson@10594
   331
\rulename{neg_mod_sign}\isanewline
paulson@12156
   332
b\ <\ 0\ \isasymLongrightarrow \ b\ <\ a\ mod\ b%
paulson@10594
   333
\rulename{neg_mod_bound}
paulson@10594
   334
\end{isabelle}
paulson@10594
   335
ML treats negative divisors in the same way, but most computer hardware
paulson@10594
   336
treats signed operands using the same rules as for multiplication.
paulson@10794
   337
Many facts about quotients and remainders are provided:
paulson@10594
   338
\begin{isabelle}
paulson@10594
   339
(a\ +\ b)\ div\ c\ =\isanewline
paulson@10594
   340
a\ div\ c\ +\ b\ div\ c\ +\ (a\ mod\ c\ +\ b\ mod\ c)\ div\ c%
paulson@10594
   341
\rulename{zdiv_zadd1_eq}
paulson@10594
   342
\par\smallskip
paulson@10594
   343
(a\ +\ b)\ mod\ c\ =\ (a\ mod\ c\ +\ b\ mod\ c)\ mod\ c%
paulson@10594
   344
\rulename{zmod_zadd1_eq}
paulson@10594
   345
\end{isabelle}
paulson@10594
   346
paulson@10594
   347
\begin{isabelle}
paulson@10594
   348
(a\ *\ b)\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c%
paulson@10594
   349
\rulename{zdiv_zmult1_eq}\isanewline
paulson@10594
   350
(a\ *\ b)\ mod\ c\ =\ a\ *\ (b\ mod\ c)\ mod\ c%
paulson@10594
   351
\rulename{zmod_zmult1_eq}
paulson@10594
   352
\end{isabelle}
paulson@10594
   353
paulson@10594
   354
\begin{isabelle}
paulson@12156
   355
0\ <\ c\ \isasymLongrightarrow \ a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%
paulson@10594
   356
\rulename{zdiv_zmult2_eq}\isanewline
paulson@12156
   357
0\ <\ c\ \isasymLongrightarrow \ a\ mod\ (b*c)\ =\ b*(a\ div\ b\ mod\
paulson@10594
   358
c)\ +\ a\ mod\ b%
paulson@10594
   359
\rulename{zmod_zmult2_eq}
paulson@10594
   360
\end{isabelle}
paulson@10594
   361
The last two differ from their natural number analogues by requiring
paulson@10594
   362
\isa{c} to be positive.  Since division by zero yields zero, we could allow
paulson@10594
   363
\isa{c} to be zero.  However, \isa{c} cannot be negative: a counterexample
paulson@10594
   364
is
paulson@10594
   365
$\isa{a} = 7$, $\isa{b} = 2$ and $\isa{c} = -3$, when the left-hand side of
paulson@11416
   366
\isa{zdiv_zmult2_eq} is $-2$ while the right-hand side is~$-1$.%
paulson@11416
   367
\index{integers|)}\index{*int (type)|)}
paulson@10594
   368
paulson@13979
   369
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
   370
\begin{isabelle}
paulson@13750
   371
\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
   372
\rulename{int_ge_induct}\isanewline
paulson@13750
   373
\isasymlbrakk k\ <\ i;\ P(k+1);\ \isasymAnd i.\ \isasymlbrakk k\ <\ i;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i+1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%
paulson@13750
   374
\rulename{int_gr_induct}\isanewline
paulson@13750
   375
\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
   376
\rulename{int_le_induct}\isanewline
paulson@13750
   377
\isasymlbrakk i\ <\ k;\ P(k-1);\ \isasymAnd i.\ \isasymlbrakk i\ <\ k;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i-1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%
paulson@13750
   378
\rulename{int_less_induct}
paulson@13750
   379
\end{isabelle}
paulson@13750
   380
paulson@10594
   381
nipkow@11216
   382
\subsection{The Type of Real Numbers, {\tt\slshape real}}
paulson@10594
   383
paulson@11416
   384
\index{real numbers|(}\index{*real (type)|(}%
paulson@10777
   385
The real numbers enjoy two significant properties that the integers lack. 
paulson@10777
   386
They are
paulson@10777
   387
\textbf{dense}: between every two distinct real numbers there lies another.
paulson@10777
   388
This property follows from the division laws, since if $x<y$ then between
paulson@10777
   389
them lies $(x+y)/2$.  The second property is that they are
paulson@10777
   390
\textbf{complete}: every set of reals that is bounded above has a least
paulson@10777
   391
upper bound.  Completeness distinguishes the reals from the rationals, for
paulson@10777
   392
which the set $\{x\mid x^2<2\}$ has no least upper bound.  (It could only be
paulson@10777
   393
$\surd2$, which is irrational.)
paulson@10794
   394
The formalization of completeness is complicated; rather than
paulson@10777
   395
reproducing it here, we refer you to the theory \texttt{RComplete} in
paulson@10777
   396
directory \texttt{Real}.
paulson@10794
   397
Density, however, is trivial to express:
paulson@10777
   398
\begin{isabelle}
paulson@10777
   399
x\ <\ y\ \isasymLongrightarrow \ \isasymexists r.\ x\ <\ r\ \isasymand \ r\ <\ y%
paulson@14295
   400
\rulename{dense}
paulson@10777
   401
\end{isabelle}
paulson@10777
   402
paulson@10777
   403
Here is a selection of rules about the division operator.  The following
paulson@10777
   404
are installed as default simplification rules in order to express
paulson@10777
   405
combinations of products and quotients as rational expressions:
paulson@10777
   406
\begin{isabelle}
paulson@14288
   407
a\ *\ (b\ /\ c)\ =\ a\ *\ b\ /\ c
paulson@14288
   408
\rulename{times_divide_eq_right}\isanewline
paulson@14288
   409
b\ /\ c\ *\ a\ =\ b\ *\ a\ /\ c
paulson@14288
   410
\rulename{times_divide_eq_left}\isanewline
paulson@14288
   411
a\ /\ (b\ /\ c)\ =\ a\ *\ c\ /\ b
paulson@14288
   412
\rulename{divide_divide_eq_right}\isanewline
paulson@14288
   413
a\ /\ b\ /\ c\ =\ a\ /\ (b\ *\ c)
paulson@14288
   414
\rulename{divide_divide_eq_left}
paulson@10777
   415
\end{isabelle}
paulson@10777
   416
paulson@10777
   417
Signs are extracted from quotients in the hope that complementary terms can
paulson@10777
   418
then be cancelled:
paulson@10777
   419
\begin{isabelle}
paulson@14295
   420
-\ (a\ /\ b)\ =\ -\ a\ /\ b
paulson@14295
   421
\rulename{minus_divide_left}\isanewline
paulson@14295
   422
-\ (a\ /\ b)\ =\ a\ /\ -\ b
paulson@14295
   423
\rulename{minus_divide_right}
paulson@10777
   424
\end{isabelle}
paulson@10777
   425
paulson@10777
   426
The following distributive law is available, but it is not installed as a
paulson@10777
   427
simplification rule.
paulson@10777
   428
\begin{isabelle}
paulson@14295
   429
(a\ +\ b)\ /\ c\ =\ a\ /\ c\ +\ b\ /\ c%
paulson@14295
   430
\rulename{add_divide_distrib}
paulson@10777
   431
\end{isabelle}
paulson@10777
   432
paulson@10594
   433
As with the other numeric types, the simplifier can sort the operands of
paulson@10594
   434
addition and multiplication.  The name \isa{real_add_ac} refers to the
paulson@10777
   435
associativity and commutativity theorems for addition, while similarly
paulson@10594
   436
\isa{real_mult_ac} contains those properties for multiplication. 
paulson@10594
   437
paulson@10777
   438
The absolute value function \isa{abs} is
paulson@10777
   439
defined for the reals, along with many theorems such as this one about
paulson@10777
   440
exponentiation:
paulson@10777
   441
\begin{isabelle}
paulson@14353
   442
\isasymbar a\ \isacharcircum \ n\isasymbar\ =\ 
paulson@14353
   443
\isasymbar a\isasymbar \ \isacharcircum \ n
paulson@14353
   444
\rulename{power_abs}
paulson@10777
   445
\end{isabelle}
paulson@10777
   446
paulson@11416
   447
Numeric literals\index{numeric literals!for type \protect\isa{real}}
paulson@11416
   448
for type \isa{real} have the same syntax as those for type
paulson@11174
   449
\isa{int} and only express integral values.  Fractions expressed
paulson@11174
   450
using the division operator are automatically simplified to lowest terms:
paulson@11174
   451
\begin{isabelle}
paulson@12156
   452
\ 1.\ P\ ((3\ /\ 4)\ *\ (8\ /\ 15))\isanewline
paulson@11174
   453
\isacommand{apply} simp\isanewline
paulson@12156
   454
\ 1.\ P\ (2\ /\ 5)
paulson@11174
   455
\end{isabelle}
paulson@11174
   456
Exponentiation can express floating-point values such as
paulson@12156
   457
\isa{2 * 10\isacharcircum6}, but at present no special simplification
paulson@11174
   458
is performed.
paulson@11174
   459
paulson@11174
   460
paulson@10881
   461
\begin{warn}
paulson@13983
   462
Type \isa{real} is only available in the logic HOL-Complex, which
paulson@13983
   463
is  HOL extended with a definitional development of the real and complex
paulson@11174
   464
numbers.  Base your theory upon theory
paulson@13983
   465
\thydx{Complex_Main}, not the usual \isa{Main}.%
paulson@11416
   466
\index{real numbers|)}\index{*real (type)|)}
paulson@11416
   467
Launch Isabelle using the command 
paulson@11174
   468
\begin{verbatim}
paulson@13983
   469
Isabelle -l HOL-Complex
paulson@11174
   470
\end{verbatim}
paulson@10881
   471
\end{warn}
paulson@10777
   472
paulson@13983
   473
Also available in HOL-Complex is the
paulson@13983
   474
theory \isa{Hyperreal}, which define the type \tydx{hypreal} of 
paulson@11416
   475
\rmindex{non-standard reals}.  These
paulson@10777
   476
\textbf{hyperreals} include infinitesimals, which represent infinitely
paulson@10777
   477
small and infinitely large quantities; they facilitate proofs
paulson@10794
   478
about limits, differentiation and integration~\cite{fleuriot-jcm}.  The
paulson@10794
   479
development defines an infinitely large number, \isa{omega} and an
paulson@10881
   480
infinitely small positive number, \isa{epsilon}.  The 
paulson@12333
   481
relation $x\approx y$ means ``$x$ is infinitely close to~$y$.''
paulson@12333
   482
Theory \isa{Hyperreal} also defines transcendental functions such as sine,
paulson@12333
   483
cosine, exponential and logarithm --- even the versions for type
paulson@12333
   484
\isa{real}, because they are defined using nonstandard limits.%
nipkow@13996
   485
\index{numbers|)}