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