doc-src/TutorialI/Types/numerics.tex
author paulson
Tue Dec 05 18:55:18 2000 +0100 (2000-12-05)
changeset 10594 6330bc4b6fe4
child 10608 620647438780
permissions -rw-r--r--
nat and int sections but no real
paulson@10594
     1
Our examples until now have used the type of \textbf{natural numbers},
paulson@10594
     2
\isa{nat}.  This is a recursive datatype generated by the constructors
paulson@10594
     3
zero  and successor, so it works well with inductive proofs and primitive
paulson@10594
     4
recursive function definitions. Isabelle/HOL also has the type \isa{int}
paulson@10594
     5
of \textbf{integers}, which gives up induction in exchange  for proper subtraction.
paulson@10594
     6
paulson@10594
     7
The integers are preferable to the natural  numbers for reasoning about
paulson@10594
     8
complicated arithmetic expressions. For  example, a termination proof
paulson@10594
     9
typically involves an integer metric  that is shown to decrease at each
paulson@10594
    10
loop iteration. Even if the  metric cannot become negative, proofs about it
paulson@10594
    11
are usually easier  if the integers are used rather than the natural
paulson@10594
    12
numbers. 
paulson@10594
    13
paulson@10594
    14
The logic Isabelle/HOL-Real also has the type \isa{real} of real numbers
paulson@10594
    15
and even the type \isa{hypreal} of non-standard reals. These
paulson@10594
    16
\textbf{hyperreals} include  infinitesimals, which represent infinitely
paulson@10594
    17
small and infinitely  large quantities; they greatly facilitate proofs
paulson@10594
    18
about limits,  differentiation and integration.  Isabelle has no subtyping, 
paulson@10594
    19
so the numeric types are distinct and there are 
paulson@10594
    20
functions to convert between them. 
paulson@10594
    21
paulson@10594
    22
Many theorems involving numeric types can be proved automatically by
paulson@10594
    23
Isabelle's arithmetic decision procedure, the method
paulson@10594
    24
\isa{arith}.  Linear arithmetic comprises addition, subtraction
paulson@10594
    25
and multiplication by constant factors; subterms involving other operators
paulson@10594
    26
are regarded as variables.  The procedure can be slow, especially if the
paulson@10594
    27
subgoal to be proved involves subtraction over type \isa{nat}, which 
paulson@10594
    28
causes case splits.  
paulson@10594
    29
paulson@10594
    30
The simplifier reduces arithmetic expressions in other
paulson@10594
    31
ways, such as dividing through by common factors.  For problems that lie
paulson@10594
    32
outside the scope of automation, the library has hundreds of
paulson@10594
    33
theorems about multiplication, division, etc., that can be brought to
paulson@10594
    34
bear.  You can find find them by browsing the library.  Some
paulson@10594
    35
useful lemmas are shown below.
paulson@10594
    36
paulson@10594
    37
\subsection{Numeric Literals}
paulson@10594
    38
paulson@10594
    39
Literals are available for the types of natural numbers, integers 
paulson@10594
    40
and reals and denote integer values of arbitrary size. 
paulson@10594
    41
\REMARK{hypreal?}
paulson@10594
    42
They begin 
paulson@10594
    43
with a number sign (\isa{\#}), have an optional minus sign (\isa{-}) and 
paulson@10594
    44
then one or more decimal digits. Examples are \isa{\#0}, \isa{\#-3} 
paulson@10594
    45
and \isa{\#441223334678}.
paulson@10594
    46
paulson@10594
    47
Literals look like constants, but they abbreviate 
paulson@10594
    48
terms, representing the number in a two's complement binary notation. 
paulson@10594
    49
Isabelle performs arithmetic on literals by rewriting, rather 
paulson@10594
    50
than using the hardware arithmetic. In most cases arithmetic 
paulson@10594
    51
is fast enough, even for large numbers. The arithmetic operations 
paulson@10594
    52
provided for literals are addition, subtraction, multiplication, 
paulson@10594
    53
integer division and remainder. 
paulson@10594
    54
paulson@10594
    55
\emph{Beware}: 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@10594
    59
\begin{isabelle}
paulson@10594
    60
\isacommand{lemma}\ "\#2\ *\ m\ =\ m\ +\ m"
paulson@10594
    61
\end{isabelle}
paulson@10594
    62
%
paulson@10594
    63
Carefully observe how Isabelle displays the subgoal:
paulson@10594
    64
\begin{isabelle}
paulson@10594
    65
\ 1.\ (\#2::'a)\ *\ m\ =\ m\ +\ m
paulson@10594
    66
\end{isabelle}
paulson@10594
    67
The type \isa{'a} given for the literal \isa{\#2} warns us that no numeric
paulson@10594
    68
type has been specified.  The problem is underspecified.  Given a type
paulson@10594
    69
constraint such as \isa{nat}, \isa{int} or \isa{real}, it becomes trivial.
paulson@10594
    70
paulson@10594
    71
paulson@10594
    72
\subsection{The type of natural numbers, {\tt\slshape nat}}
paulson@10594
    73
paulson@10594
    74
This type requires no introduction: we have been using it from the
paulson@10594
    75
start.  Hundreds of useful lemmas about arithmetic on type \isa{nat} are
paulson@10594
    76
proved in the theories \isa{Nat}, \isa{NatArith} and \isa{Divides}.  Only
paulson@10594
    77
in exceptional circumstances should you resort to induction.
paulson@10594
    78
paulson@10594
    79
\subsubsection{Literals}
paulson@10594
    80
The notational options for the natural numbers can be confusing. The 
paulson@10594
    81
constant \isa{0} is overloaded to serve as the neutral value 
paulson@10594
    82
in a variety of additive types. The symbols \isa{1} and \isa{2} are 
paulson@10594
    83
not constants but abbreviations for \isa{Suc 0} and \isa{Suc(Suc 0)},
paulson@10594
    84
respectively. The literals \isa{\#0}, \isa{\#1} and \isa{\#2}  are
paulson@10594
    85
entirely different from \isa{0}, \isa{1} and \isa{2}. You  will
paulson@10594
    86
sometimes prefer one notation to the other. Literals are  obviously
paulson@10594
    87
necessary to express large values, while \isa{0} and \isa{Suc}  are
paulson@10594
    88
needed in order to match many theorems, including the rewrite  rules for
paulson@10594
    89
primitive recursive functions. The following default  simplification rules
paulson@10594
    90
replace small literals by zero and successor: 
paulson@10594
    91
\begin{isabelle}
paulson@10594
    92
\#0\ =\ 0
paulson@10594
    93
\rulename{numeral_0_eq_0}\isanewline
paulson@10594
    94
\#1\ =\ 1
paulson@10594
    95
\rulename{numeral_1_eq_1}\isanewline
paulson@10594
    96
\#2\ +\ n\ =\ Suc\ (Suc\ n)
paulson@10594
    97
\rulename{add_2_eq_Suc}\isanewline
paulson@10594
    98
n\ +\ \#2\ =\ Suc\ (Suc\ n)
paulson@10594
    99
\rulename{add_2_eq_Suc'}
paulson@10594
   100
\end{isabelle}
paulson@10594
   101
In special circumstances, you may wish to remove or reorient 
paulson@10594
   102
these rules. 
paulson@10594
   103
paulson@10594
   104
\subsubsection{Typical lemmas}
paulson@10594
   105
Inequalities involving addition and subtraction alone can be proved
paulson@10594
   106
automatically.  Lemmas such as these can be used to prove inequalities
paulson@10594
   107
involving multiplication and division:
paulson@10594
   108
\begin{isabelle}
paulson@10594
   109
\isasymlbrakk i\ \isasymle \ j;\ k\ \isasymle \ l\isasymrbrakk \ \isasymLongrightarrow \ i\ *\ k\ \isasymle \ j\ *\ l%
paulson@10594
   110
\rulename{mult_le_mono}\isanewline
paulson@10594
   111
\isasymlbrakk i\ <\ j;\ 0\ <\ k\isasymrbrakk \ \isasymLongrightarrow \ i\
paulson@10594
   112
*\ k\ <\ j\ *\ k%
paulson@10594
   113
\rulename{mult_less_mono1}\isanewline
paulson@10594
   114
m\ \isasymle \ n\ \isasymLongrightarrow \ m\ div\ k\ \isasymle \ n\ div\ k%
paulson@10594
   115
\rulename{div_le_mono}
paulson@10594
   116
\end{isabelle}
paulson@10594
   117
%
paulson@10594
   118
Various distributive laws concerning multiplication are available:
paulson@10594
   119
\begin{isabelle}
paulson@10594
   120
(m\ +\ n)\ *\ k\ =\ m\ *\ k\ +\ n\ *\ k%
paulson@10594
   121
\rulename{add_mult_distrib}\isanewline
paulson@10594
   122
(m\ -\ n)\ *\ k\ =\ m\ *\ k\ -\ n\ *\ k%
paulson@10594
   123
\rulename{diff_mult_distrib}\isanewline
paulson@10594
   124
(m\ mod\ n)\ *\ k\ =\ (m\ *\ k)\ mod\ (n\ *\ k)
paulson@10594
   125
\rulename{mod_mult_distrib}
paulson@10594
   126
\end{isabelle}
paulson@10594
   127
paulson@10594
   128
\subsubsection{Division}
paulson@10594
   129
The library contains the basic facts about quotient and remainder
paulson@10594
   130
(including the analogous equation, \isa{div_if}):
paulson@10594
   131
\begin{isabelle}
paulson@10594
   132
m\ mod\ n\ =\ (if\ m\ <\ n\ then\ m\ else\ (m\ -\ n)\ mod\ n)
paulson@10594
   133
\rulename{mod_if}\isanewline
paulson@10594
   134
m\ div\ n\ *\ n\ +\ m\ mod\ n\ =\ m%
paulson@10594
   135
\rulename{mod_div_equality}
paulson@10594
   136
\end{isabelle}
paulson@10594
   137
paulson@10594
   138
Many less obvious facts about quotient and remainder are also provided. 
paulson@10594
   139
Here is a selection:
paulson@10594
   140
\begin{isabelle}
paulson@10594
   141
a\ *\ b\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c%
paulson@10594
   142
\rulename{div_mult1_eq}\isanewline
paulson@10594
   143
a\ *\ b\ mod\ c\ =\ a\ *\ (b\ mod\ c)\ mod\ c%
paulson@10594
   144
\rulename{mod_mult1_eq}\isanewline
paulson@10594
   145
a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%
paulson@10594
   146
\rulename{div_mult2_eq}\isanewline
paulson@10594
   147
a\ mod\ (b*c)\ =\ b * (a\ div\ b\ mod\ c)\ +\ a\ mod\ b%
paulson@10594
   148
\rulename{mod_mult2_eq}\isanewline
paulson@10594
   149
0\ <\ c\ \isasymLongrightarrow \ (c\ *\ a)\ div\ (c\ *\ b)\ =\ a\ div\ b%
paulson@10594
   150
\rulename{div_mult_mult1}
paulson@10594
   151
\end{isabelle}
paulson@10594
   152
paulson@10594
   153
Surprisingly few of these results depend upon the
paulson@10594
   154
divisors' being nonzero.  Isabelle/HOL defines division by zero:
paulson@10594
   155
\begin{isabelle}
paulson@10594
   156
a\ div\ 0\ =\ 0
paulson@10594
   157
\rulename{DIVISION_BY_ZERO_DIV}\isanewline
paulson@10594
   158
a\ mod\ 0\ =\ a%
paulson@10594
   159
\rulename{DIVISION_BY_ZERO_MOD}
paulson@10594
   160
\end{isabelle}
paulson@10594
   161
As a concession to convention, these equations are not installed as default
paulson@10594
   162
simplification rules but are merely used to remove nonzero-divisor
paulson@10594
   163
hypotheses by case analysis.  In \isa{div_mult_mult1} above, one of
paulson@10594
   164
the two divisors (namely~\isa{c}) must be still be nonzero.
paulson@10594
   165
paulson@10594
   166
The \textbf{divides} relation has the standard definition, which
paulson@10594
   167
is overloaded over all numeric types: 
paulson@10594
   168
\begin{isabelle}
paulson@10594
   169
m\ dvd\ n\ \isasymequiv\ {\isasymexists}k.\ n\ =\ m\ *\ k
paulson@10594
   170
\rulename{dvd_def}
paulson@10594
   171
\end{isabelle}
paulson@10594
   172
%
paulson@10594
   173
Section~\ref{sec:proving-euclid} discusses proofs involving this
paulson@10594
   174
relation.  Here are some of the facts proved about it:
paulson@10594
   175
\begin{isabelle}
paulson@10594
   176
\isasymlbrakk m\ dvd\ n;\ n\ dvd\ m\isasymrbrakk \ \isasymLongrightarrow \ m\ =\ n%
paulson@10594
   177
\rulename{dvd_anti_sym}\isanewline
paulson@10594
   178
\isasymlbrakk k\ dvd\ m;\ k\ dvd\ n\isasymrbrakk \ \isasymLongrightarrow \ k\ dvd\ (m\ +\ n)
paulson@10594
   179
\rulename{dvd_add}
paulson@10594
   180
\end{isabelle}
paulson@10594
   181
paulson@10594
   182
\subsubsection{Simplifier tricks}
paulson@10594
   183
The rule \isa{diff_mult_distrib} shown above is one of the few facts
paulson@10594
   184
about \isa{m\ -\ n} that is not subject to
paulson@10594
   185
the condition \isa{n\ \isasymle \  m}.  Natural number subtraction has few
paulson@10594
   186
nice properties; often it is best to remove it from a subgoal
paulson@10594
   187
using this split rule:
paulson@10594
   188
\begin{isabelle}
paulson@10594
   189
P(a-b)\ =\ ((a<b\ \isasymlongrightarrow \ P\
paulson@10594
   190
0)\ \isasymand \ (\isasymforall d.\ a\ =\ b+d\ \isasymlongrightarrow \ P\
paulson@10594
   191
d))
paulson@10594
   192
\rulename{nat_diff_split}
paulson@10594
   193
\end{isabelle}
paulson@10594
   194
For example, it proves the following fact, which lies outside the scope of
paulson@10594
   195
linear arithmetic:
paulson@10594
   196
\begin{isabelle}
paulson@10594
   197
\isacommand{lemma}\ "(n-1)*(n+1)\ =\ n*n\ -\ 1"\isanewline
paulson@10594
   198
\isacommand{apply}\ (simp\ split:\ nat_diff_split)\isanewline
paulson@10594
   199
\isacommand{done}
paulson@10594
   200
\end{isabelle}
paulson@10594
   201
paulson@10594
   202
Suppose that two expressions are equal, differing only in 
paulson@10594
   203
associativity and commutativity of addition.  Simplifying with the
paulson@10594
   204
following equations sorts the terms and groups them to the right, making
paulson@10594
   205
the two expressions identical:
paulson@10594
   206
\begin{isabelle}
paulson@10594
   207
m\ +\ n\ +\ k\ =\ m\ +\ (n\ +\ k)
paulson@10594
   208
\rulename{add_assoc}\isanewline
paulson@10594
   209
m\ +\ n\ =\ n\ +\ m%
paulson@10594
   210
\rulename{add_commute}\isanewline
paulson@10594
   211
x\ +\ (y\ +\ z)\ =\ y\ +\ (x\
paulson@10594
   212
+\ z)
paulson@10594
   213
\rulename{add_left_commute}
paulson@10594
   214
\end{isabelle}
paulson@10594
   215
The name \isa{add_ac} refers to the list of all three theorems, similarly
paulson@10594
   216
there is \isa{mult_ac}.  Here is an example of the sorting effect.  Start
paulson@10594
   217
with this goal:
paulson@10594
   218
\begin{isabelle}
paulson@10594
   219
\ 1.\ Suc\ (i\ +\ j\ *\ l\ *\ k\ +\ m\ *\ n)\ =\
paulson@10594
   220
f\ (n\ *\ m\ +\ i\ +\ k\ *\ j\ *\ l)
paulson@10594
   221
\end{isabelle}
paulson@10594
   222
%
paulson@10594
   223
Simplify using  \isa{add_ac} and \isa{mult_ac}:
paulson@10594
   224
\begin{isabelle}
paulson@10594
   225
\isacommand{apply}\ (simp\ add:\ add_ac\ mult_ac)
paulson@10594
   226
\end{isabelle}
paulson@10594
   227
%
paulson@10594
   228
Here is the resulting subgoal:
paulson@10594
   229
\begin{isabelle}
paulson@10594
   230
\ 1.\ Suc\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))\
paulson@10594
   231
=\ f\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))%
paulson@10594
   232
\end{isabelle}
paulson@10594
   233
paulson@10594
   234
paulson@10594
   235
\subsection{The type of integers, {\tt\slshape int}}
paulson@10594
   236
paulson@10594
   237
Reasoning methods resemble those for the natural numbers, but
paulson@10594
   238
induction and the constant \isa{Suc} are not available.
paulson@10594
   239
paulson@10594
   240
Concerning simplifier tricks, we have no need to eliminate subtraction (it
paulson@10594
   241
is well-behaved), but the simplifier can sort the operands of integer
paulson@10594
   242
operators.  The name \isa{zadd_ac} refers to the associativity and
paulson@10594
   243
commutativity theorems for integer addition, while \isa{zmult_ac} has the
paulson@10594
   244
analogous theorems for multiplication.  The prefix~\isa{z} in many theorem
paulson@10594
   245
names recalls the use of $\Bbb{Z}$ to denote the set of integers.
paulson@10594
   246
paulson@10594
   247
For division and remainder, the treatment of negative divisors follows
paulson@10594
   248
traditional mathematical practice: the sign of the remainder follows that
paulson@10594
   249
of the divisor:
paulson@10594
   250
\begin{isabelle}
paulson@10594
   251
\#0\ <\ b\ \isasymLongrightarrow \ \#0\ \isasymle \ a\ mod\ b%
paulson@10594
   252
\rulename{pos_mod_sign}\isanewline
paulson@10594
   253
\#0\ <\ b\ \isasymLongrightarrow \ a\ mod\ b\ <\ b%
paulson@10594
   254
\rulename{pos_mod_bound}\isanewline
paulson@10594
   255
b\ <\ \#0\ \isasymLongrightarrow \ a\ mod\ b\ \isasymle \ \#0
paulson@10594
   256
\rulename{neg_mod_sign}\isanewline
paulson@10594
   257
b\ <\ \#0\ \isasymLongrightarrow \ b\ <\ a\ mod\ b%
paulson@10594
   258
\rulename{neg_mod_bound}
paulson@10594
   259
\end{isabelle}
paulson@10594
   260
ML treats negative divisors in the same way, but most computer hardware
paulson@10594
   261
treats signed operands using the same rules as for multiplication.
paulson@10594
   262
paulson@10594
   263
The library provides many lemmas for proving inequalities involving integer
paulson@10594
   264
multiplication and division, similar to those shown above for
paulson@10594
   265
type~\isa{nat}.  The absolute value function \isa{abs} is
paulson@10594
   266
defined for the integers; we have for example the obvious law
paulson@10594
   267
\begin{isabelle}
paulson@10594
   268
\isasymbar x\ *\ y\isasymbar \ =\ \isasymbar x\isasymbar \ *\ \isasymbar y\isasymbar 
paulson@10594
   269
\rulename{abs_mult}
paulson@10594
   270
\end{isabelle}
paulson@10594
   271
paulson@10594
   272
Again, 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%
paulson@10594
   279
\rulename{zmod_zadd1_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@10594
   290
\#0\ <\ c\ \isasymLongrightarrow \ a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%
paulson@10594
   291
\rulename{zdiv_zmult2_eq}\isanewline
paulson@10594
   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@10594
   301
\isa{zdiv_zmult2_eq} is $-2$ while the right-hand side is $-1$.
paulson@10594
   302
paulson@10594
   303
paulson@10594
   304
\subsection{The type of real numbers, {\tt\slshape real}}
paulson@10594
   305
paulson@10594
   306
As with the other numeric types, the simplifier can sort the operands of
paulson@10594
   307
addition and multiplication.  The name \isa{real_add_ac} refers to the
paulson@10594
   308
associativity and commutativity theorems for addition; similarly
paulson@10594
   309
\isa{real_mult_ac} contains those properties for multiplication. 
paulson@10594
   310
paulson@10594
   311
\textbf{To be written.  Inverse, abs, theorems about density, etc.?}