doc-src/TutorialI/Types/numerics.tex
 author paulson Thu Jan 04 10:22:33 2001 +0100 (2001-01-04) changeset 10777 a5a6255748c3 parent 10654 458068404143 child 10779 b0d961105f46 permissions -rw-r--r--
initial material on the Reals
     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

    34 Literals are available for the types of natural numbers, integers

    35 and reals and denote integer values of arbitrary size.

    36 They begin

    37 with a number sign (\isa{\#}), have an optional minus sign (\isa{-}) and

    38 then one or more decimal digits. Examples are \isa{\#0}, \isa{\#-3}

    39 and \isa{\#441223334678}.

    40

    41 Literals look like constants, but they abbreviate

    42 terms, representing the number in a two's complement binary notation.

    43 Isabelle performs arithmetic on literals by rewriting, rather

    44 than using the hardware arithmetic. In most cases arithmetic

    45 is fast enough, even for large numbers. The arithmetic operations

    46 provided for literals are addition, subtraction, multiplication,

    47 integer division and remainder.

    48

    49 \emph{Beware}: the arithmetic operators are

    50 overloaded, so you must be careful to ensure that each numeric

    51 expression refers to a specific type, if necessary by inserting

    52 type constraints.  Here is an example of what can go wrong:

    53 \begin{isabelle}

    54 \isacommand{lemma}\ "\#2\ *\ m\ =\ m\ +\ m"

    55 \end{isabelle}

    56 %

    57 Carefully observe how Isabelle displays the subgoal:

    58 \begin{isabelle}

    59 \ 1.\ (\#2::'a)\ *\ m\ =\ m\ +\ m

    60 \end{isabelle}

    61 The type \isa{'a} given for the literal \isa{\#2} warns us that no numeric

    62 type has been specified.  The problem is underspecified.  Given a type

    63 constraint such as \isa{nat}, \isa{int} or \isa{real}, it becomes trivial.

    64

    65

    66 \subsection{The type of natural numbers, {\tt\slshape nat}}

    67

    68 This type requires no introduction: we have been using it from the

    69 start.  Hundreds of useful lemmas about arithmetic on type \isa{nat} are

    70 proved in the theories \isa{Nat}, \isa{NatArith} and \isa{Divides}.  Only

    71 in exceptional circumstances should you resort to induction.

    72

    73 \subsubsection{Literals}

    74 The notational options for the natural numbers can be confusing. The

    75 constant \isa{0} is overloaded to serve as the neutral value

    76 in a variety of additive types. The symbols \isa{1} and \isa{2} are

    77 not constants but abbreviations for \isa{Suc 0} and \isa{Suc(Suc 0)},

    78 respectively. The literals \isa{\#0}, \isa{\#1} and \isa{\#2}  are

    79 entirely different from \isa{0}, \isa{1} and \isa{2}. You  will

    80 sometimes prefer one notation to the other. Literals are  obviously

    81 necessary to express large values, while \isa{0} and \isa{Suc}  are

    82 needed in order to match many theorems, including the rewrite  rules for

    83 primitive recursive functions. The following default  simplification rules

    84 replace small literals by zero and successor:

    85 \begin{isabelle}

    86 \#0\ =\ 0

    87 \rulename{numeral_0_eq_0}\isanewline

    88 \#1\ =\ 1

    89 \rulename{numeral_1_eq_1}\isanewline

    90 \#2\ +\ n\ =\ Suc\ (Suc\ n)

    91 \rulename{add_2_eq_Suc}\isanewline

    92 n\ +\ \#2\ =\ Suc\ (Suc\ n)

    93 \rulename{add_2_eq_Suc'}

    94 \end{isabelle}

    95 In special circumstances, you may wish to remove or reorient

    96 these rules.

    97

    98 \subsubsection{Typical lemmas}

    99 Inequalities involving addition and subtraction alone can be proved

   100 automatically.  Lemmas such as these can be used to prove inequalities

   101 involving multiplication and division:

   102 \begin{isabelle}

   103 \isasymlbrakk i\ \isasymle \ j;\ k\ \isasymle \ l\isasymrbrakk \ \isasymLongrightarrow \ i\ *\ k\ \isasymle \ j\ *\ l%

   104 \rulename{mult_le_mono}\isanewline

   105 \isasymlbrakk i\ <\ j;\ 0\ <\ k\isasymrbrakk \ \isasymLongrightarrow \ i\

   106 *\ k\ <\ j\ *\ k%

   107 \rulename{mult_less_mono1}\isanewline

   108 m\ \isasymle \ n\ \isasymLongrightarrow \ m\ div\ k\ \isasymle \ n\ div\ k%

   109 \rulename{div_le_mono}

   110 \end{isabelle}

   111 %

   112 Various distributive laws concerning multiplication are available:

   113 \begin{isabelle}

   114 (m\ +\ n)\ *\ k\ =\ m\ *\ k\ +\ n\ *\ k%

   115 \rulename{add_mult_distrib}\isanewline

   116 (m\ -\ n)\ *\ k\ =\ m\ *\ k\ -\ n\ *\ k%

   117 \rulename{diff_mult_distrib}\isanewline

   118 (m\ mod\ n)\ *\ k\ =\ (m\ *\ k)\ mod\ (n\ *\ k)

   119 \rulename{mod_mult_distrib}

   120 \end{isabelle}

   121

   122 \subsubsection{Division}

   123 The library contains the basic facts about quotient and remainder

   124 (including the analogous equation, \isa{div_if}):

   125 \begin{isabelle}

   126 m\ mod\ n\ =\ (if\ m\ <\ n\ then\ m\ else\ (m\ -\ n)\ mod\ n)

   127 \rulename{mod_if}\isanewline

   128 m\ div\ n\ *\ n\ +\ m\ mod\ n\ =\ m%

   129 \rulename{mod_div_equality}

   130 \end{isabelle}

   131

   132 Many less obvious facts about quotient and remainder are also provided.

   133 Here is a selection:

   134 \begin{isabelle}

   135 a\ *\ b\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c%

   136 \rulename{div_mult1_eq}\isanewline

   137 a\ *\ b\ mod\ c\ =\ a\ *\ (b\ mod\ c)\ mod\ c%

   138 \rulename{mod_mult1_eq}\isanewline

   139 a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%

   140 \rulename{div_mult2_eq}\isanewline

   141 a\ mod\ (b*c)\ =\ b * (a\ div\ b\ mod\ c)\ +\ a\ mod\ b%

   142 \rulename{mod_mult2_eq}\isanewline

   143 0\ <\ c\ \isasymLongrightarrow \ (c\ *\ a)\ div\ (c\ *\ b)\ =\ a\ div\ b%

   144 \rulename{div_mult_mult1}

   145 \end{isabelle}

   146

   147 Surprisingly few of these results depend upon the

   148 divisors' being nonzero.  Isabelle/HOL defines division by zero:

   149 \begin{isabelle}

   150 a\ div\ 0\ =\ 0

   151 \rulename{DIVISION_BY_ZERO_DIV}\isanewline

   152 a\ mod\ 0\ =\ a%

   153 \rulename{DIVISION_BY_ZERO_MOD}

   154 \end{isabelle}

   155 As a concession to convention, these equations are not installed as default

   156 simplification rules but are merely used to remove nonzero-divisor

   157 hypotheses by case analysis.  In \isa{div_mult_mult1} above, one of

   158 the two divisors (namely~\isa{c}) must be still be nonzero.

   159

   160 The \textbf{divides} relation has the standard definition, which

   161 is overloaded over all numeric types:

   162 \begin{isabelle}

   163 m\ dvd\ n\ \isasymequiv\ {\isasymexists}k.\ n\ =\ m\ *\ k

   164 \rulename{dvd_def}

   165 \end{isabelle}

   166 %

   167 Section~\ref{sec:proving-euclid} discusses proofs involving this

   168 relation.  Here are some of the facts proved about it:

   169 \begin{isabelle}

   170 \isasymlbrakk m\ dvd\ n;\ n\ dvd\ m\isasymrbrakk \ \isasymLongrightarrow \ m\ =\ n%

   171 \rulename{dvd_anti_sym}\isanewline

   172 \isasymlbrakk k\ dvd\ m;\ k\ dvd\ n\isasymrbrakk \ \isasymLongrightarrow \ k\ dvd\ (m\ +\ n)

   173 \rulename{dvd_add}

   174 \end{isabelle}

   175

   176 \subsubsection{Simplifier tricks}

   177 The rule \isa{diff_mult_distrib} shown above is one of the few facts

   178 about \isa{m\ -\ n} that is not subject to

   179 the condition \isa{n\ \isasymle \  m}.  Natural number subtraction has few

   180 nice properties; often it is best to remove it from a subgoal

   181 using this split rule:

   182 \begin{isabelle}

   183 P(a-b)\ =\ ((a<b\ \isasymlongrightarrow \ P\

   184 0)\ \isasymand \ (\isasymforall d.\ a\ =\ b+d\ \isasymlongrightarrow \ P\

   185 d))

   186 \rulename{nat_diff_split}

   187 \end{isabelle}

   188 For example, it proves the following fact, which lies outside the scope of

   189 linear arithmetic:

   190 \begin{isabelle}

   191 \isacommand{lemma}\ "(n-1)*(n+1)\ =\ n*n\ -\ 1"\isanewline

   192 \isacommand{apply}\ (simp\ split:\ nat_diff_split)\isanewline

   193 \isacommand{done}

   194 \end{isabelle}

   195

   196 Suppose that two expressions are equal, differing only in

   197 associativity and commutativity of addition.  Simplifying with the

   198 following equations sorts the terms and groups them to the right, making

   199 the two expressions identical:

   200 \begin{isabelle}

   201 m\ +\ n\ +\ k\ =\ m\ +\ (n\ +\ k)

   202 \rulename{add_assoc}\isanewline

   203 m\ +\ n\ =\ n\ +\ m%

   204 \rulename{add_commute}\isanewline

   205 x\ +\ (y\ +\ z)\ =\ y\ +\ (x\

   206 +\ z)

   207 \rulename{add_left_commute}

   208 \end{isabelle}

   209 The name \isa{add_ac} refers to the list of all three theorems, similarly

   210 there is \isa{mult_ac}.  Here is an example of the sorting effect.  Start

   211 with this goal:

   212 \begin{isabelle}

   213 \ 1.\ Suc\ (i\ +\ j\ *\ l\ *\ k\ +\ m\ *\ n)\ =\

   214 f\ (n\ *\ m\ +\ i\ +\ k\ *\ j\ *\ l)

   215 \end{isabelle}

   216 %

   217 Simplify using  \isa{add_ac} and \isa{mult_ac}:

   218 \begin{isabelle}

   219 \isacommand{apply}\ (simp\ add:\ add_ac\ mult_ac)

   220 \end{isabelle}

   221 %

   222 Here is the resulting subgoal:

   223 \begin{isabelle}

   224 \ 1.\ Suc\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))\

   225 =\ f\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))%

   226 \end{isabelle}

   227

   228

   229 \subsection{The type of integers, {\tt\slshape int}}

   230

   231 Reasoning methods resemble those for the natural numbers, but

   232 induction and the constant \isa{Suc} are not available.

   233

   234 Concerning simplifier tricks, we have no need to eliminate subtraction (it

   235 is well-behaved), but the simplifier can sort the operands of integer

   236 operators.  The name \isa{zadd_ac} refers to the associativity and

   237 commutativity theorems for integer addition, while \isa{zmult_ac} has the

   238 analogous theorems for multiplication.  The prefix~\isa{z} in many theorem

   239 names recalls the use of $\Bbb{Z}$ to denote the set of integers.

   240

   241 For division and remainder, the treatment of negative divisors follows

   242 traditional mathematical practice: the sign of the remainder follows that

   243 of the divisor:

   244 \begin{isabelle}

   245 \#0\ <\ b\ \isasymLongrightarrow \ \#0\ \isasymle \ a\ mod\ b%

   246 \rulename{pos_mod_sign}\isanewline

   247 \#0\ <\ b\ \isasymLongrightarrow \ a\ mod\ b\ <\ b%

   248 \rulename{pos_mod_bound}\isanewline

   249 b\ <\ \#0\ \isasymLongrightarrow \ a\ mod\ b\ \isasymle \ \#0

   250 \rulename{neg_mod_sign}\isanewline

   251 b\ <\ \#0\ \isasymLongrightarrow \ b\ <\ a\ mod\ b%

   252 \rulename{neg_mod_bound}

   253 \end{isabelle}

   254 ML treats negative divisors in the same way, but most computer hardware

   255 treats signed operands using the same rules as for multiplication.

   256

   257 The library provides many lemmas for proving inequalities involving integer

   258 multiplication and division, similar to those shown above for

   259 type~\isa{nat}.  The absolute value function \isa{abs} is

   260 defined for the integers; we have for example the obvious law

   261 \begin{isabelle}

   262 \isasymbar x\ *\ y\isasymbar \ =\ \isasymbar x\isasymbar \ *\ \isasymbar y\isasymbar

   263 \rulename{abs_mult}

   264 \end{isabelle}

   265

   266 Again, many facts about quotients and remainders are provided:

   267 \begin{isabelle}

   268 (a\ +\ b)\ div\ c\ =\isanewline

   269 a\ div\ c\ +\ b\ div\ c\ +\ (a\ mod\ c\ +\ b\ mod\ c)\ div\ c%

   270 \rulename{zdiv_zadd1_eq}

   271 \par\smallskip

   272 (a\ +\ b)\ mod\ c\ =\ (a\ mod\ c\ +\ b\ mod\ c)\ mod\ c%

   273 \rulename{zmod_zadd1_eq}

   274 \end{isabelle}

   275

   276 \begin{isabelle}

   277 (a\ *\ b)\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c%

   278 \rulename{zdiv_zmult1_eq}\isanewline

   279 (a\ *\ b)\ mod\ c\ =\ a\ *\ (b\ mod\ c)\ mod\ c%

   280 \rulename{zmod_zmult1_eq}

   281 \end{isabelle}

   282

   283 \begin{isabelle}

   284 \#0\ <\ c\ \isasymLongrightarrow \ a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%

   285 \rulename{zdiv_zmult2_eq}\isanewline

   286 \#0\ <\ c\ \isasymLongrightarrow \ a\ mod\ (b*c)\ =\ b*(a\ div\ b\ mod\

   287 c)\ +\ a\ mod\ b%

   288 \rulename{zmod_zmult2_eq}

   289 \end{isabelle}

   290 The last two differ from their natural number analogues by requiring

   291 \isa{c} to be positive.  Since division by zero yields zero, we could allow

   292 \isa{c} to be zero.  However, \isa{c} cannot be negative: a counterexample

   293 is

   294 $\isa{a} = 7$, $\isa{b} = 2$ and $\isa{c} = -3$, when the left-hand side of

   295 \isa{zdiv_zmult2_eq} is $-2$ while the right-hand side is $-1$.

   296

   297

   298 \subsection{The type of real numbers, {\tt\slshape real}}

   299

   300 The real numbers enjoy two significant properties that the integers lack.

   301 They are

   302 \textbf{dense}: between every two distinct real numbers there lies another.

   303 This property follows from the division laws, since if $x<y$ then between

   304 them lies $(x+y)/2$.  The second property is that they are

   305 \textbf{complete}: every set of reals that is bounded above has a least

   306 upper bound.  Completeness distinguishes the reals from the rationals, for

   307 which the set $\{x\mid x^2<2\}$ has no least upper bound.  (It could only be

   308 $\surd2$, which is irrational.)

   309

   310 The formalization of completeness is long and technical.  Rather than

   311 reproducing it here, we refer you to the theory \texttt{RComplete} in

   312 directory \texttt{Real}.

   313

   314 Density is trivial to express:

   315 \begin{isabelle}

   316 x\ <\ y\ \isasymLongrightarrow \ \isasymexists r.\ x\ <\ r\ \isasymand \ r\ <\ y%

   317 \rulename{real_dense}

   318 \end{isabelle}

   319

   320 Here is a selection of rules about the division operator.  The following

   321 are installed as default simplification rules in order to express

   322 combinations of products and quotients as rational expressions:

   323 \begin{isabelle}

   324 x\ *\ (y\ /\ z)\ =\ x\ *\ y\ /\ z%

   325 \rulename{real_times_divide1_eq}\isanewline

   326 y\ /\ z\ *\ x\ =\ y\ *\ x\ /\ z%

   327 \rulename{real_times_divide2_eq}\isanewline

   328 x\ /\ (y\ /\ z)\ =\ x\ *\ z\ /\ y%

   329 \rulename{real_divide_divide1_eq}\isanewline

   330 x\ /\ y\ /\ z\ =\ x\ /\ (y\ *\ z)

   331 \rulename{real_divide_divide2_eq}

   332 \end{isabelle}

   333

   334 Signs are extracted from quotients in the hope that complementary terms can

   335 then be cancelled:

   336 \begin{isabelle}

   337 -\ x\ /\ y\ =\ -\ (x\ /\ y)

   338 \rulename{real_minus_divide_eq}\isanewline

   339 x\ /\ -\ y\ =\ -\ (x\ /\ y)

   340 \rulename{real_divide_minus_eq}

   341 \end{isabelle}

   342

   343 The following distributive law is available, but it is not installed as a

   344 simplification rule.

   345 \begin{isabelle}

   346 (x\ +\ y)\ /\ z\ =\ x\ /\ z\ +\ y\ /\ z%

   347 \rulename{real_add_divide_distrib}

   348 \end{isabelle}

   349

   350 As with the other numeric types, the simplifier can sort the operands of

   351 addition and multiplication.  The name \isa{real_add_ac} refers to the

   352 associativity and commutativity theorems for addition, while similarly

   353 \isa{real_mult_ac} contains those properties for multiplication.

   354

   355 The absolute value function \isa{abs} is

   356 defined for the reals, along with many theorems such as this one about

   357 exponentiation:

   358 \begin{isabelle}

   359 \isasymbar r\isasymbar \ \isacharcircum \ n\ =\ \isasymbar r\ \isacharcircum \ n\isasymbar

   360 \rulename{realpow_abs}

   361 \end{isabelle}

   362

   363 \emph{Note}: Type \isa{real} is only available in the logic HOL-Real, which

   364 is  HOL extended with the rather substantial development of the real

   365 numbers.  Base your theory upon theory \isa{Real}, not the usual \isa{Main}.

   366

   367 Also distributed with Isabelle is HOL-Hyperreal,

   368 whose theory \isa{Hyperreal} defines the type \isa{hypreal} of non-standard

   369 reals.  These

   370 \textbf{hyperreals} include infinitesimals, which represent infinitely

   371 small and infinitely large quantities; they facilitate proofs

   372 about limits, differentiation and integration.  The development defines an

   373 infinitely large number, \isa{omega} and an infinitely small positive

   374 number, \isa{epsilon}.  Also available is the approximates relation,

   375 written $\approx$.