doc-src/TutorialI/Types/numerics.tex
 author paulson Fri Dec 13 16:48:20 2002 +0100 (2002-12-13) changeset 13750 b5cd10cb106b parent 12333 ef43a3d6e962 child 13979 4c3a638828b9 permissions -rw-r--r--
integer induction rules
 paulson@10794 1 % $Id$ paulson@11389 2 paulson@11389 3 \section{Numbers} paulson@11389 4 \label{sec:numbers} paulson@11389 5 paulson@11494 6 \index{numbers|(}% paulson@11174 7 Until now, our numerical examples have used the type of \textbf{natural paulson@11174 8 numbers}, paulson@10594 9 \isa{nat}. This is a recursive datatype generated by the constructors paulson@10594 10 zero and successor, so it works well with inductive proofs and primitive paulson@11174 11 recursive function definitions. HOL also provides the type paulson@10794 12 \isa{int} of \textbf{integers}, which lack induction but support true paulson@11174 13 subtraction. The integers are preferable to the natural numbers for reasoning about paulson@11174 14 complicated arithmetic expressions, even for some expressions whose paulson@11174 15 value is non-negative. The logic HOL-Real also has the type paulson@11174 16 \isa{real} of real numbers. Isabelle has no subtyping, so the numeric paulson@11174 17 types are distinct and there are functions to convert between them. paulson@11174 18 Fortunately most numeric operations are overloaded: the same symbol can be paulson@11174 19 used at all numeric types. Table~\ref{tab:overloading} in the appendix paulson@11174 20 shows the most important operations, together with the priorities of the paulson@11174 21 infix symbols. paulson@10594 22 paulson@11416 23 \index{linear arithmetic}% paulson@10594 24 Many theorems involving numeric types can be proved automatically by paulson@10594 25 Isabelle's arithmetic decision procedure, the method paulson@11416 26 \methdx{arith}. Linear arithmetic comprises addition, subtraction paulson@10594 27 and multiplication by constant factors; subterms involving other operators paulson@10594 28 are regarded as variables. The procedure can be slow, especially if the paulson@10594 29 subgoal to be proved involves subtraction over type \isa{nat}, which paulson@10594 30 causes case splits. paulson@10594 31 paulson@10594 32 The simplifier reduces arithmetic expressions in other paulson@10594 33 ways, such as dividing through by common factors. For problems that lie paulson@10881 34 outside the scope of automation, HOL provides hundreds of paulson@10594 35 theorems about multiplication, division, etc., that can be brought to paulson@10881 36 bear. You can locate them using Proof General's Find paulson@10881 37 button. A few lemmas are given below to show what paulson@10794 38 is available. paulson@10594 39 paulson@10594 40 \subsection{Numeric Literals} nipkow@10779 41 \label{sec:numerals} paulson@10594 42 paulson@11416 43 \index{numeric literals|(}% paulson@12156 44 The constants \cdx{0} and \cdx{1} are overloaded. They denote zero and one, paulson@12156 45 respectively, for all numeric types. Other values are expressed by numeric paulson@12156 46 literals, which consist of one or more decimal digits optionally preceeded by paulson@12156 47 a minus sign (\isa{-}). Examples are \isa{2}, \isa{-3} and paulson@12156 48 \isa{441223334678}. Literals are available for the types of natural numbers, paulson@12156 49 integers and reals; they denote integer values of arbitrary size. paulson@10594 50 paulson@10594 51 Literals look like constants, but they abbreviate paulson@12156 52 terms representing the number in a two's complement binary notation. paulson@10794 53 Isabelle performs arithmetic on literals by rewriting rather paulson@10594 54 than using the hardware arithmetic. In most cases arithmetic paulson@10594 55 is fast enough, even for large numbers. The arithmetic operations paulson@10794 56 provided for literals include addition, subtraction, multiplication, paulson@10794 57 integer division and remainder. Fractions of literals (expressed using paulson@10794 58 division) are reduced to lowest terms. paulson@10594 59 paulson@11416 60 \begin{warn}\index{overloading!and arithmetic} paulson@10794 61 The arithmetic operators are paulson@10594 62 overloaded, so you must be careful to ensure that each numeric paulson@10594 63 expression refers to a specific type, if necessary by inserting paulson@10594 64 type constraints. Here is an example of what can go wrong: paulson@10794 65 \par paulson@10594 66 \begin{isabelle} paulson@12156 67 \isacommand{lemma}\ "2\ *\ m\ =\ m\ +\ m" paulson@10594 68 \end{isabelle} paulson@10594 69 % paulson@10594 70 Carefully observe how Isabelle displays the subgoal: paulson@10594 71 \begin{isabelle} paulson@12156 72 \ 1.\ (2::'a)\ *\ m\ =\ m\ +\ m paulson@10594 73 \end{isabelle} paulson@12156 74 The type \isa{'a} given for the literal \isa{2} warns us that no numeric paulson@10594 75 type has been specified. The problem is underspecified. Given a type paulson@10594 76 constraint such as \isa{nat}, \isa{int} or \isa{real}, it becomes trivial. paulson@10794 77 \end{warn} paulson@10794 78 paulson@10881 79 \begin{warn} paulson@11428 80 \index{recdef@\isacommand {recdef} (command)!and numeric literals} paulson@11416 81 Numeric literals are not constructors and therefore paulson@11416 82 must not be used in patterns. For example, this declaration is paulson@11416 83 rejected: paulson@10881 84 \begin{isabelle} paulson@10881 85 \isacommand{recdef}\ h\ "\isacharbraceleft \isacharbraceright "\isanewline paulson@12156 86 "h\ 3\ =\ 2"\isanewline nipkow@11148 87 "h\ i\ \ =\ i" paulson@10881 88 \end{isabelle} paulson@10881 89 paulson@10881 90 You should use a conditional expression instead: paulson@10881 91 \begin{isabelle} paulson@12156 92 "h\ i\ =\ (if\ i\ =\ 3\ then\ 2\ else\ i)" paulson@10881 93 \end{isabelle} paulson@11416 94 \index{numeric literals|)} paulson@10881 95 \end{warn} paulson@10881 96 paulson@10594 97 paulson@10594 98 nipkow@11216 99 \subsection{The Type of Natural Numbers, {\tt\slshape nat}} paulson@10594 100 paulson@11416 101 \index{natural numbers|(}\index{*nat (type)|(}% paulson@10594 102 This type requires no introduction: we have been using it from the paulson@10794 103 beginning. Hundreds of theorems about the natural numbers are paulson@10594 104 proved in the theories \isa{Nat}, \isa{NatArith} and \isa{Divides}. Only paulson@10594 105 in exceptional circumstances should you resort to induction. paulson@10594 106 paulson@10594 107 \subsubsection{Literals} paulson@11416 108 \index{numeric literals!for type \protect\isa{nat}}% paulson@12156 109 The notational options for the natural numbers are confusing. Recall that an paulson@12156 110 overloaded constant can be defined independently for each type; the definition paulson@12156 111 of \cdx{1} for type \isa{nat} is paulson@12156 112 \begin{isabelle} paulson@12156 113 1\ \isasymequiv\ Suc\ 0 paulson@12156 114 \rulename{One_nat_def} paulson@12156 115 \end{isabelle} paulson@12156 116 This is installed as a simplification rule, so the simplifier will replace paulson@12156 117 every occurrence of \isa{1::nat} by \isa{Suc\ 0}. Literals are obviously paulson@12156 118 better than nested \isa{Suc}s at expressing large values. But many theorems, paulson@12156 119 including the rewrite rules for primitive recursive functions, can only be paulson@12156 120 applied to terms of the form \isa{Suc\ $n$}. paulson@12156 121 paulson@12156 122 The following default simplification rules replace paulson@10794 123 small literals by zero and successor: paulson@10594 124 \begin{isabelle} paulson@12156 125 2\ +\ n\ =\ Suc\ (Suc\ n) paulson@10594 126 \rulename{add_2_eq_Suc}\isanewline paulson@12156 127 n\ +\ 2\ =\ Suc\ (Suc\ n) paulson@10594 128 \rulename{add_2_eq_Suc'} paulson@10594 129 \end{isabelle} paulson@12156 130 It is less easy to transform \isa{100} into \isa{Suc\ 99} (for example), and paulson@12156 131 the simplifier will normally reverse this transformation. Novices should paulson@12156 132 express natural numbers using \isa{0} and \isa{Suc} only. paulson@10594 133 paulson@10594 134 \subsubsection{Typical lemmas} paulson@10594 135 Inequalities involving addition and subtraction alone can be proved paulson@10594 136 automatically. Lemmas such as these can be used to prove inequalities paulson@10594 137 involving multiplication and division: paulson@10594 138 \begin{isabelle} paulson@10594 139 \isasymlbrakk i\ \isasymle \ j;\ k\ \isasymle \ l\isasymrbrakk \ \isasymLongrightarrow \ i\ *\ k\ \isasymle \ j\ *\ l% paulson@10594 140 \rulename{mult_le_mono}\isanewline paulson@10594 141 \isasymlbrakk i\ <\ j;\ 0\ <\ k\isasymrbrakk \ \isasymLongrightarrow \ i\ paulson@10594 142 *\ k\ <\ j\ *\ k% paulson@10594 143 \rulename{mult_less_mono1}\isanewline paulson@10594 144 m\ \isasymle \ n\ \isasymLongrightarrow \ m\ div\ k\ \isasymle \ n\ div\ k% paulson@10594 145 \rulename{div_le_mono} paulson@10594 146 \end{isabelle} paulson@10594 147 % paulson@10594 148 Various distributive laws concerning multiplication are available: paulson@10594 149 \begin{isabelle} paulson@10594 150 (m\ +\ n)\ *\ k\ =\ m\ *\ k\ +\ n\ *\ k% paulson@11416 151 \rulenamedx{add_mult_distrib}\isanewline paulson@10594 152 (m\ -\ n)\ *\ k\ =\ m\ *\ k\ -\ n\ *\ k% paulson@11416 153 \rulenamedx{diff_mult_distrib}\isanewline paulson@10594 154 (m\ mod\ n)\ *\ k\ =\ (m\ *\ k)\ mod\ (n\ *\ k) paulson@11416 155 \rulenamedx{mod_mult_distrib} paulson@10594 156 \end{isabelle} paulson@10594 157 paulson@10594 158 \subsubsection{Division} paulson@11416 159 \index{division!for type \protect\isa{nat}}% paulson@10881 160 The infix operators \isa{div} and \isa{mod} are overloaded. paulson@10881 161 Isabelle/HOL provides the basic facts about quotient and remainder paulson@10881 162 on the natural numbers: paulson@10594 163 \begin{isabelle} paulson@10594 164 m\ mod\ n\ =\ (if\ m\ <\ n\ then\ m\ else\ (m\ -\ n)\ mod\ n) paulson@10594 165 \rulename{mod_if}\isanewline paulson@10594 166 m\ div\ n\ *\ n\ +\ m\ mod\ n\ =\ m% paulson@11416 167 \rulenamedx{mod_div_equality} paulson@10594 168 \end{isabelle} paulson@10594 169 paulson@10594 170 Many less obvious facts about quotient and remainder are also provided. paulson@10594 171 Here is a selection: paulson@10594 172 \begin{isabelle} paulson@10594 173 a\ *\ b\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c% paulson@10594 174 \rulename{div_mult1_eq}\isanewline paulson@10594 175 a\ *\ b\ mod\ c\ =\ a\ *\ (b\ mod\ c)\ mod\ c% paulson@10594 176 \rulename{mod_mult1_eq}\isanewline paulson@10594 177 a\ div\ (b*c)\ =\ a\ div\ b\ div\ c% paulson@10594 178 \rulename{div_mult2_eq}\isanewline paulson@10594 179 a\ mod\ (b*c)\ =\ b * (a\ div\ b\ mod\ c)\ +\ a\ mod\ b% paulson@10594 180 \rulename{mod_mult2_eq}\isanewline paulson@10594 181 0\ <\ c\ \isasymLongrightarrow \ (c\ *\ a)\ div\ (c\ *\ b)\ =\ a\ div\ b% paulson@10594 182 \rulename{div_mult_mult1} paulson@10594 183 \end{isabelle} paulson@10594 184 paulson@10594 185 Surprisingly few of these results depend upon the paulson@11416 186 divisors' being nonzero. paulson@11416 187 \index{division!by zero}% paulson@11416 188 That is because division by paulson@10794 189 zero yields zero: paulson@10594 190 \begin{isabelle} paulson@10594 191 a\ div\ 0\ =\ 0 paulson@10594 192 \rulename{DIVISION_BY_ZERO_DIV}\isanewline paulson@10594 193 a\ mod\ 0\ =\ a% paulson@10594 194 \rulename{DIVISION_BY_ZERO_MOD} paulson@10594 195 \end{isabelle} paulson@10594 196 As a concession to convention, these equations are not installed as default paulson@11174 197 simplification rules. In \isa{div_mult_mult1} above, one of nipkow@11161 198 the two divisors (namely~\isa{c}) must still be nonzero. paulson@10594 199 paulson@11416 200 The \textbf{divides} relation\index{divides relation} paulson@11416 201 has the standard definition, which paulson@10594 202 is overloaded over all numeric types: paulson@10594 203 \begin{isabelle} paulson@10594 204 m\ dvd\ n\ \isasymequiv\ {\isasymexists}k.\ n\ =\ m\ *\ k paulson@11416 205 \rulenamedx{dvd_def} paulson@10594 206 \end{isabelle} paulson@10594 207 % paulson@10594 208 Section~\ref{sec:proving-euclid} discusses proofs involving this paulson@10594 209 relation. Here are some of the facts proved about it: paulson@10594 210 \begin{isabelle} paulson@10594 211 \isasymlbrakk m\ dvd\ n;\ n\ dvd\ m\isasymrbrakk \ \isasymLongrightarrow \ m\ =\ n% paulson@11416 212 \rulenamedx{dvd_anti_sym}\isanewline paulson@10594 213 \isasymlbrakk k\ dvd\ m;\ k\ dvd\ n\isasymrbrakk \ \isasymLongrightarrow \ k\ dvd\ (m\ +\ n) paulson@11416 214 \rulenamedx{dvd_add} paulson@10594 215 \end{isabelle} paulson@10594 216 nipkow@11216 217 \subsubsection{Simplifier Tricks} paulson@10594 218 The rule \isa{diff_mult_distrib} shown above is one of the few facts paulson@10594 219 about \isa{m\ -\ n} that is not subject to paulson@10594 220 the condition \isa{n\ \isasymle \ m}. Natural number subtraction has few paulson@10794 221 nice properties; often you should remove it by simplifying with this split paulson@10794 222 rule: paulson@10594 223 \begin{isabelle} paulson@10594 224 P(a-b)\ =\ ((a$,$\le$and$<$): paulson@13750 367 \begin{isabelle} paulson@13750 368 \isasymlbrakk k\ \isasymle \ i;\ P\ k;\ \isasymAnd i.\ \isasymlbrakk k\ \isasymle \ i;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i+1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i% paulson@13750 369 \rulename{int_ge_induct}\isanewline paulson@13750 370 \isasymlbrakk k\ <\ i;\ P(k+1);\ \isasymAnd i.\ \isasymlbrakk k\ <\ i;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i+1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i% paulson@13750 371 \rulename{int_gr_induct}\isanewline paulson@13750 372 \isasymlbrakk i\ \isasymle \ k;\ P\ k;\ \isasymAnd i.\ \isasymlbrakk i\ \isasymle \ k;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i-1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i% paulson@13750 373 \rulename{int_le_induct}\isanewline paulson@13750 374 \isasymlbrakk i\ <\ k;\ P(k-1);\ \isasymAnd i.\ \isasymlbrakk i\ <\ k;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i-1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i% paulson@13750 375 \rulename{int_less_induct} paulson@13750 376 \end{isabelle} paulson@13750 377 paulson@10594 378 nipkow@11216 379 \subsection{The Type of Real Numbers, {\tt\slshape real}} paulson@10594 380 paulson@11416 381 \index{real numbers|(}\index{*real (type)|(}% paulson@10777 382 The real numbers enjoy two significant properties that the integers lack. paulson@10777 383 They are paulson@10777 384 \textbf{dense}: between every two distinct real numbers there lies another. paulson@10777 385 This property follows from the division laws, since if$x