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
 paulson@10594  1 Our examples until now have used the type of \textbf{natural numbers},  paulson@10594  2 \isa{nat}. This is a recursive datatype generated by the constructors  paulson@10594  3 zero and successor, so it works well with inductive proofs and primitive  paulson@10594  4 recursive function definitions. Isabelle/HOL also has the type \isa{int}  paulson@10594  5 of \textbf{integers}, which gives up induction in exchange for proper subtraction.  paulson@10594  6 paulson@10594  7 The integers are preferable to the natural numbers for reasoning about  paulson@10594  8 complicated arithmetic expressions. For example, a termination proof  paulson@10594  9 typically involves an integer metric that is shown to decrease at each  paulson@10594  10 loop iteration. Even if the metric cannot become negative, proofs about it  paulson@10594  11 are usually easier if the integers are used rather than the natural  paulson@10594  12 numbers.  paulson@10594  13 paulson@10594  14 The logic Isabelle/HOL-Real also has the type \isa{real} of real numbers  paulson@10594  15 and even the type \isa{hypreal} of non-standard reals. These  paulson@10594  16 \textbf{hyperreals} include infinitesimals, which represent infinitely  paulson@10594  17 small and infinitely large quantities; they greatly facilitate proofs  paulson@10594  18 about limits, differentiation and integration. Isabelle has no subtyping,  paulson@10594  19 so the numeric types are distinct and there are  paulson@10594  20 functions to convert between them.  paulson@10594  21 paulson@10594  22 Many theorems involving numeric types can be proved automatically by  paulson@10594  23 Isabelle's arithmetic decision procedure, the method  paulson@10594  24 \isa{arith}. Linear arithmetic comprises addition, subtraction  paulson@10594  25 and multiplication by constant factors; subterms involving other operators  paulson@10594  26 are regarded as variables. The procedure can be slow, especially if the  paulson@10594  27 subgoal to be proved involves subtraction over type \isa{nat}, which  paulson@10594  28 causes case splits.  paulson@10594  29 paulson@10594  30 The simplifier reduces arithmetic expressions in other  paulson@10594  31 ways, such as dividing through by common factors. For problems that lie  paulson@10594  32 outside the scope of automation, the library has hundreds of  paulson@10594  33 theorems about multiplication, division, etc., that can be brought to  paulson@10594  34 bear. You can find find them by browsing the library. Some  paulson@10594  35 useful lemmas are shown below.  paulson@10594  36 paulson@10594  37 \subsection{Numeric Literals}  paulson@10594  38 paulson@10594  39 Literals are available for the types of natural numbers, integers  paulson@10594  40 and reals and denote integer values of arbitrary size.  paulson@10594  41 \REMARK{hypreal?}  paulson@10594  42 They begin  paulson@10594  43 with a number sign (\isa{\#}), have an optional minus sign (\isa{-}) and  paulson@10594  44 then one or more decimal digits. Examples are \isa{\#0}, \isa{\#-3}  paulson@10594  45 and \isa{\#441223334678}.  paulson@10594  46 paulson@10594  47 Literals look like constants, but they abbreviate  paulson@10594  48 terms, representing the number in a two's complement binary notation.  paulson@10594  49 Isabelle performs arithmetic on literals by rewriting, rather  paulson@10594  50 than using the hardware arithmetic. In most cases arithmetic  paulson@10594  51 is fast enough, even for large numbers. The arithmetic operations  paulson@10594  52 provided for literals are addition, subtraction, multiplication,  paulson@10594  53 integer division and remainder.  paulson@10594  54 paulson@10594  55 \emph{Beware}: the arithmetic operators are  paulson@10594  56 overloaded, so you must be careful to ensure that each numeric  paulson@10594  57 expression refers to a specific type, if necessary by inserting  paulson@10594  58 type constraints. Here is an example of what can go wrong:  paulson@10594  59 \begin{isabelle}  paulson@10594  60 \isacommand{lemma}\ "\#2\ *\ m\ =\ m\ +\ m"  paulson@10594  61 \end{isabelle}  paulson@10594  62 %  paulson@10594  63 Carefully observe how Isabelle displays the subgoal:  paulson@10594  64 \begin{isabelle}  paulson@10594  65 \ 1.\ (\#2::'a)\ *\ m\ =\ m\ +\ m  paulson@10594  66 \end{isabelle}  paulson@10594  67 The type \isa{'a} given for the literal \isa{\#2} warns us that no numeric  paulson@10594  68 type has been specified. The problem is underspecified. Given a type  paulson@10594  69 constraint such as \isa{nat}, \isa{int} or \isa{real}, it becomes trivial.  paulson@10594  70 paulson@10594  71 paulson@10594  72 \subsection{The type of natural numbers, {\tt\slshape nat}}  paulson@10594  73 paulson@10594  74 This type requires no introduction: we have been using it from the  paulson@10594  75 start. Hundreds of useful lemmas about arithmetic on type \isa{nat} are  paulson@10594  76 proved in the theories \isa{Nat}, \isa{NatArith} and \isa{Divides}. Only  paulson@10594  77 in exceptional circumstances should you resort to induction.  paulson@10594  78 paulson@10594  79 \subsubsection{Literals}  paulson@10594  80 The notational options for the natural numbers can be confusing. The  paulson@10594  81 constant \isa{0} is overloaded to serve as the neutral value  paulson@10594  82 in a variety of additive types. The symbols \isa{1} and \isa{2} are  paulson@10594  83 not constants but abbreviations for \isa{Suc 0} and \isa{Suc(Suc 0)},  paulson@10594  84 respectively. The literals \isa{\#0}, \isa{\#1} and \isa{\#2} are  paulson@10594  85 entirely different from \isa{0}, \isa{1} and \isa{2}. You will  paulson@10594  86 sometimes prefer one notation to the other. Literals are obviously  paulson@10594  87 necessary to express large values, while \isa{0} and \isa{Suc} are  paulson@10594  88 needed in order to match many theorems, including the rewrite rules for  paulson@10594  89 primitive recursive functions. The following default simplification rules  paulson@10594  90 replace small literals by zero and successor:  paulson@10594  91 \begin{isabelle}  paulson@10594  92 \#0\ =\ 0  paulson@10594  93 \rulename{numeral_0_eq_0}\isanewline  paulson@10594  94 \#1\ =\ 1  paulson@10594  95 \rulename{numeral_1_eq_1}\isanewline  paulson@10594  96 \#2\ +\ n\ =\ Suc\ (Suc\ n)  paulson@10594  97 \rulename{add_2_eq_Suc}\isanewline  paulson@10594  98 n\ +\ \#2\ =\ Suc\ (Suc\ n)  paulson@10594  99 \rulename{add_2_eq_Suc'}  paulson@10594  100 \end{isabelle}  paulson@10594  101 In special circumstances, you may wish to remove or reorient  paulson@10594  102 these rules.  paulson@10594  103 paulson@10594  104 \subsubsection{Typical lemmas}  paulson@10594  105 Inequalities involving addition and subtraction alone can be proved  paulson@10594  106 automatically. Lemmas such as these can be used to prove inequalities  paulson@10594  107 involving multiplication and division:  paulson@10594  108 \begin{isabelle}  paulson@10594  109 \isasymlbrakk i\ \isasymle \ j;\ k\ \isasymle \ l\isasymrbrakk \ \isasymLongrightarrow \ i\ *\ k\ \isasymle \ j\ *\ l%  paulson@10594  110 \rulename{mult_le_mono}\isanewline  paulson@10594  111 \isasymlbrakk i\ <\ j;\ 0\ <\ k\isasymrbrakk \ \isasymLongrightarrow \ i\  paulson@10594  112 *\ k\ <\ j\ *\ k%  paulson@10594  113 \rulename{mult_less_mono1}\isanewline  paulson@10594  114 m\ \isasymle \ n\ \isasymLongrightarrow \ m\ div\ k\ \isasymle \ n\ div\ k%  paulson@10594  115 \rulename{div_le_mono}  paulson@10594  116 \end{isabelle}  paulson@10594  117 %  paulson@10594  118 Various distributive laws concerning multiplication are available:  paulson@10594  119 \begin{isabelle}  paulson@10594  120 (m\ +\ n)\ *\ k\ =\ m\ *\ k\ +\ n\ *\ k%  paulson@10594  121 \rulename{add_mult_distrib}\isanewline  paulson@10594  122 (m\ -\ n)\ *\ k\ =\ m\ *\ k\ -\ n\ *\ k%  paulson@10594  123 \rulename{diff_mult_distrib}\isanewline  paulson@10594  124 (m\ mod\ n)\ *\ k\ =\ (m\ *\ k)\ mod\ (n\ *\ k)  paulson@10594  125 \rulename{mod_mult_distrib}  paulson@10594  126 \end{isabelle}  paulson@10594  127 paulson@10594  128 \subsubsection{Division}  paulson@10594  129 The library contains the basic facts about quotient and remainder  paulson@10594  130 (including the analogous equation, \isa{div_if}):  paulson@10594  131 \begin{isabelle}  paulson@10594  132 m\ mod\ n\ =\ (if\ m\ <\ n\ then\ m\ else\ (m\ -\ n)\ mod\ n)  paulson@10594  133 \rulename{mod_if}\isanewline  paulson@10594  134 m\ div\ n\ *\ n\ +\ m\ mod\ n\ =\ m%  paulson@10594  135 \rulename{mod_div_equality}  paulson@10594  136 \end{isabelle}  paulson@10594  137 paulson@10594  138 Many less obvious facts about quotient and remainder are also provided.  paulson@10594  139 Here is a selection:  paulson@10594  140 \begin{isabelle}  paulson@10594  141 a\ *\ b\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c%  paulson@10594  142 \rulename{div_mult1_eq}\isanewline  paulson@10594  143 a\ *\ b\ mod\ c\ =\ a\ *\ (b\ mod\ c)\ mod\ c%  paulson@10594  144 \rulename{mod_mult1_eq}\isanewline  paulson@10594  145 a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%  paulson@10594  146 \rulename{div_mult2_eq}\isanewline  paulson@10594  147 a\ mod\ (b*c)\ =\ b * (a\ div\ b\ mod\ c)\ +\ a\ mod\ b%  paulson@10594  148 \rulename{mod_mult2_eq}\isanewline  paulson@10594  149 0\ <\ c\ \isasymLongrightarrow \ (c\ *\ a)\ div\ (c\ *\ b)\ =\ a\ div\ b%  paulson@10594  150 \rulename{div_mult_mult1}  paulson@10594  151 \end{isabelle}  paulson@10594  152 paulson@10594  153 Surprisingly few of these results depend upon the  paulson@10594  154 divisors' being nonzero. Isabelle/HOL defines division by zero:  paulson@10594  155 \begin{isabelle}  paulson@10594  156 a\ div\ 0\ =\ 0  paulson@10594  157 \rulename{DIVISION_BY_ZERO_DIV}\isanewline  paulson@10594  158 a\ mod\ 0\ =\ a%  paulson@10594  159 \rulename{DIVISION_BY_ZERO_MOD}  paulson@10594  160 \end{isabelle}  paulson@10594  161 As a concession to convention, these equations are not installed as default  paulson@10594  162 simplification rules but are merely used to remove nonzero-divisor  paulson@10594  163 hypotheses by case analysis. In \isa{div_mult_mult1} above, one of  paulson@10594  164 the two divisors (namely~\isa{c}) must be still be nonzero.  paulson@10594  165 paulson@10594  166 The \textbf{divides} relation has the standard definition, which  paulson@10594  167 is overloaded over all numeric types:  paulson@10594  168 \begin{isabelle}  paulson@10594  169 m\ dvd\ n\ \isasymequiv\ {\isasymexists}k.\ n\ =\ m\ *\ k  paulson@10594  170 \rulename{dvd_def}  paulson@10594  171 \end{isabelle}  paulson@10594  172 %  paulson@10594  173 Section~\ref{sec:proving-euclid} discusses proofs involving this  paulson@10594  174 relation. Here are some of the facts proved about it:  paulson@10594  175 \begin{isabelle}  paulson@10594  176 \isasymlbrakk m\ dvd\ n;\ n\ dvd\ m\isasymrbrakk \ \isasymLongrightarrow \ m\ =\ n%  paulson@10594  177 \rulename{dvd_anti_sym}\isanewline  paulson@10594  178 \isasymlbrakk k\ dvd\ m;\ k\ dvd\ n\isasymrbrakk \ \isasymLongrightarrow \ k\ dvd\ (m\ +\ n)  paulson@10594  179 \rulename{dvd_add}  paulson@10594  180 \end{isabelle}  paulson@10594  181 paulson@10594  182 \subsubsection{Simplifier tricks}  paulson@10594  183 The rule \isa{diff_mult_distrib} shown above is one of the few facts  paulson@10594  184 about \isa{m\ -\ n} that is not subject to  paulson@10594  185 the condition \isa{n\ \isasymle \ m}. Natural number subtraction has few  paulson@10594  186 nice properties; often it is best to remove it from a subgoal  paulson@10594  187 using this split rule:  paulson@10594  188 \begin{isabelle}  paulson@10594  189 `P(a-b)\ =\ ((a