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