doc-src/TutorialI/Types/numerics.tex
 author paulson Tue Dec 05 18:55:18 2000 +0100 (2000-12-05) changeset 10594 6330bc4b6fe4 child 10608 620647438780 permissions -rw-r--r--
nat and int sections but no real
     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

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

    40 and reals and denote integer values of arbitrary size.

    41 \REMARK{hypreal?}

    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 are addition, subtraction, multiplication,

    53 integer division and remainder.

    54

    55 \emph{Beware}: the arithmetic operators are

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

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

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

    59 \begin{isabelle}

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

    61 \end{isabelle}

    62 %

    63 Carefully observe how Isabelle displays the subgoal:

    64 \begin{isabelle}

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

    66 \end{isabelle}

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

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

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

    70

    71

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

    73

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

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

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

    77 in exceptional circumstances should you resort to induction.

    78

    79 \subsubsection{Literals}

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

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

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

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

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

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

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

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

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

    89 primitive recursive functions. The following default  simplification rules

    90 replace small literals by zero and successor:

    91 \begin{isabelle}

    92 \#0\ =\ 0

    93 \rulename{numeral_0_eq_0}\isanewline

    94 \#1\ =\ 1

    95 \rulename{numeral_1_eq_1}\isanewline

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

    97 \rulename{add_2_eq_Suc}\isanewline

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

    99 \rulename{add_2_eq_Suc'}

   100 \end{isabelle}

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

   102 these rules.

   103

   104 \subsubsection{Typical lemmas}

   105 Inequalities involving addition and subtraction alone can be proved

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

   107 involving multiplication and division:

   108 \begin{isabelle}

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

   110 \rulename{mult_le_mono}\isanewline

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

   112 *\ k\ <\ j\ *\ k%

   113 \rulename{mult_less_mono1}\isanewline

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

   115 \rulename{div_le_mono}

   116 \end{isabelle}

   117 %

   118 Various distributive laws concerning multiplication are available:

   119 \begin{isabelle}

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

   121 \rulename{add_mult_distrib}\isanewline

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

   123 \rulename{diff_mult_distrib}\isanewline

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

   125 \rulename{mod_mult_distrib}

   126 \end{isabelle}

   127

   128 \subsubsection{Division}

   129 The library contains the basic facts about quotient and remainder

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

   131 \begin{isabelle}

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

   133 \rulename{mod_if}\isanewline

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

   135 \rulename{mod_div_equality}

   136 \end{isabelle}

   137

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

   139 Here is a selection:

   140 \begin{isabelle}

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

   142 \rulename{div_mult1_eq}\isanewline

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

   144 \rulename{mod_mult1_eq}\isanewline

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

   146 \rulename{div_mult2_eq}\isanewline

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

   148 \rulename{mod_mult2_eq}\isanewline

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

   150 \rulename{div_mult_mult1}

   151 \end{isabelle}

   152

   153 Surprisingly few of these results depend upon the

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

   155 \begin{isabelle}

   156 a\ div\ 0\ =\ 0

   157 \rulename{DIVISION_BY_ZERO_DIV}\isanewline

   158 a\ mod\ 0\ =\ a%

   159 \rulename{DIVISION_BY_ZERO_MOD}

   160 \end{isabelle}

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

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

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

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

   165

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

   167 is overloaded over all numeric types:

   168 \begin{isabelle}

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

   170 \rulename{dvd_def}

   171 \end{isabelle}

   172 %

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

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

   175 \begin{isabelle}

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

   177 \rulename{dvd_anti_sym}\isanewline

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

   179 \rulename{dvd_add}

   180 \end{isabelle}

   181

   182 \subsubsection{Simplifier tricks}

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

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

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

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

   187 using this split rule:

   188 \begin{isabelle}

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

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

   191 d))

   192 \rulename{nat_diff_split}

   193 \end{isabelle}

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

   195 linear arithmetic:

   196 \begin{isabelle}

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

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

   199 \isacommand{done}

   200 \end{isabelle}

   201

   202 Suppose that two expressions are equal, differing only in

   203 associativity and commutativity of addition.  Simplifying with the

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

   205 the two expressions identical:

   206 \begin{isabelle}

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

   208 \rulename{add_assoc}\isanewline

   209 m\ +\ n\ =\ n\ +\ m%

   210 \rulename{add_commute}\isanewline

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

   212 +\ z)

   213 \rulename{add_left_commute}

   214 \end{isabelle}

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

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

   217 with this goal:

   218 \begin{isabelle}

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

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

   221 \end{isabelle}

   222 %

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

   224 \begin{isabelle}

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

   226 \end{isabelle}

   227 %

   228 Here is the resulting subgoal:

   229 \begin{isabelle}

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

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

   232 \end{isabelle}

   233

   234

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

   236

   237 Reasoning methods resemble those for the natural numbers, but

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

   239

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

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

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

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

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

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

   246

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

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

   249 of the divisor:

   250 \begin{isabelle}

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

   252 \rulename{pos_mod_sign}\isanewline

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

   254 \rulename{pos_mod_bound}\isanewline

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

   256 \rulename{neg_mod_sign}\isanewline

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

   258 \rulename{neg_mod_bound}

   259 \end{isabelle}

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

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

   262

   263 The library provides many lemmas for proving inequalities involving integer

   264 multiplication and division, similar to those shown above for

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

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

   267 \begin{isabelle}

   268 \isasymbar x\ *\ y\isasymbar \ =\ \isasymbar x\isasymbar \ *\ \isasymbar y\isasymbar

   269 \rulename{abs_mult}

   270 \end{isabelle}

   271

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

   273 \begin{isabelle}

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

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

   276 \rulename{zdiv_zadd1_eq}

   277 \par\smallskip

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

   279 \rulename{zmod_zadd1_eq}

   280 \end{isabelle}

   281

   282 \begin{isabelle}

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

   284 \rulename{zdiv_zmult1_eq}\isanewline

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

   286 \rulename{zmod_zmult1_eq}

   287 \end{isabelle}

   288

   289 \begin{isabelle}

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

   291 \rulename{zdiv_zmult2_eq}\isanewline

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

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

   294 \rulename{zmod_zmult2_eq}

   295 \end{isabelle}

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

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

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

   299 is

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

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

   302

   303

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

   305

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

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

   308 associativity and commutativity theorems for addition; similarly

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

   310

   311 \textbf{To be written.  Inverse, abs, theorems about density, etc.?}