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