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