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$''.