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