doc-src/TutorialI/Types/numerics.tex
changeset 10594 6330bc4b6fe4
child 10608 620647438780
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/TutorialI/Types/numerics.tex	Tue Dec 05 18:55:18 2000 +0100
     1.3 @@ -0,0 +1,311 @@
     1.4 +Our examples until now have used the type of \textbf{natural numbers},
     1.5 +\isa{nat}.  This is a recursive datatype generated by the constructors
     1.6 +zero  and successor, so it works well with inductive proofs and primitive
     1.7 +recursive function definitions. Isabelle/HOL also has the type \isa{int}
     1.8 +of \textbf{integers}, which gives up induction in exchange  for proper subtraction.
     1.9 +
    1.10 +The integers are preferable to the natural  numbers for reasoning about
    1.11 +complicated arithmetic expressions. For  example, a termination proof
    1.12 +typically involves an integer metric  that is shown to decrease at each
    1.13 +loop iteration. Even if the  metric cannot become negative, proofs about it
    1.14 +are usually easier  if the integers are used rather than the natural
    1.15 +numbers. 
    1.16 +
    1.17 +The logic Isabelle/HOL-Real also has the type \isa{real} of real numbers
    1.18 +and even the type \isa{hypreal} of non-standard reals. These
    1.19 +\textbf{hyperreals} include  infinitesimals, which represent infinitely
    1.20 +small and infinitely  large quantities; they greatly facilitate proofs
    1.21 +about limits,  differentiation and integration.  Isabelle has no subtyping, 
    1.22 +so the numeric types are distinct and there are 
    1.23 +functions to convert between them. 
    1.24 +
    1.25 +Many theorems involving numeric types can be proved automatically by
    1.26 +Isabelle's arithmetic decision procedure, the method
    1.27 +\isa{arith}.  Linear arithmetic comprises addition, subtraction
    1.28 +and multiplication by constant factors; subterms involving other operators
    1.29 +are regarded as variables.  The procedure can be slow, especially if the
    1.30 +subgoal to be proved involves subtraction over type \isa{nat}, which 
    1.31 +causes case splits.  
    1.32 +
    1.33 +The simplifier reduces arithmetic expressions in other
    1.34 +ways, such as dividing through by common factors.  For problems that lie
    1.35 +outside the scope of automation, the library has hundreds of
    1.36 +theorems about multiplication, division, etc., that can be brought to
    1.37 +bear.  You can find find them by browsing the library.  Some
    1.38 +useful lemmas are shown below.
    1.39 +
    1.40 +\subsection{Numeric Literals}
    1.41 +
    1.42 +Literals are available for the types of natural numbers, integers 
    1.43 +and reals and denote integer values of arbitrary size. 
    1.44 +\REMARK{hypreal?}
    1.45 +They begin 
    1.46 +with a number sign (\isa{\#}), have an optional minus sign (\isa{-}) and 
    1.47 +then one or more decimal digits. Examples are \isa{\#0}, \isa{\#-3} 
    1.48 +and \isa{\#441223334678}.
    1.49 +
    1.50 +Literals look like constants, but they abbreviate 
    1.51 +terms, representing the number in a two's complement binary notation. 
    1.52 +Isabelle performs arithmetic on literals by rewriting, rather 
    1.53 +than using the hardware arithmetic. In most cases arithmetic 
    1.54 +is fast enough, even for large numbers. The arithmetic operations 
    1.55 +provided for literals are addition, subtraction, multiplication, 
    1.56 +integer division and remainder. 
    1.57 +
    1.58 +\emph{Beware}: the arithmetic operators are 
    1.59 +overloaded, so you must be careful to ensure that each numeric 
    1.60 +expression refers to a specific type, if necessary by inserting 
    1.61 +type constraints.  Here is an example of what can go wrong:
    1.62 +\begin{isabelle}
    1.63 +\isacommand{lemma}\ "\#2\ *\ m\ =\ m\ +\ m"
    1.64 +\end{isabelle}
    1.65 +%
    1.66 +Carefully observe how Isabelle displays the subgoal:
    1.67 +\begin{isabelle}
    1.68 +\ 1.\ (\#2::'a)\ *\ m\ =\ m\ +\ m
    1.69 +\end{isabelle}
    1.70 +The type \isa{'a} given for the literal \isa{\#2} warns us that no numeric
    1.71 +type has been specified.  The problem is underspecified.  Given a type
    1.72 +constraint such as \isa{nat}, \isa{int} or \isa{real}, it becomes trivial.
    1.73 +
    1.74 +
    1.75 +\subsection{The type of natural numbers, {\tt\slshape nat}}
    1.76 +
    1.77 +This type requires no introduction: we have been using it from the
    1.78 +start.  Hundreds of useful lemmas about arithmetic on type \isa{nat} are
    1.79 +proved in the theories \isa{Nat}, \isa{NatArith} and \isa{Divides}.  Only
    1.80 +in exceptional circumstances should you resort to induction.
    1.81 +
    1.82 +\subsubsection{Literals}
    1.83 +The notational options for the natural numbers can be confusing. The 
    1.84 +constant \isa{0} is overloaded to serve as the neutral value 
    1.85 +in a variety of additive types. The symbols \isa{1} and \isa{2} are 
    1.86 +not constants but abbreviations for \isa{Suc 0} and \isa{Suc(Suc 0)},
    1.87 +respectively. The literals \isa{\#0}, \isa{\#1} and \isa{\#2}  are
    1.88 +entirely different from \isa{0}, \isa{1} and \isa{2}. You  will
    1.89 +sometimes prefer one notation to the other. Literals are  obviously
    1.90 +necessary to express large values, while \isa{0} and \isa{Suc}  are
    1.91 +needed in order to match many theorems, including the rewrite  rules for
    1.92 +primitive recursive functions. The following default  simplification rules
    1.93 +replace small literals by zero and successor: 
    1.94 +\begin{isabelle}
    1.95 +\#0\ =\ 0
    1.96 +\rulename{numeral_0_eq_0}\isanewline
    1.97 +\#1\ =\ 1
    1.98 +\rulename{numeral_1_eq_1}\isanewline
    1.99 +\#2\ +\ n\ =\ Suc\ (Suc\ n)
   1.100 +\rulename{add_2_eq_Suc}\isanewline
   1.101 +n\ +\ \#2\ =\ Suc\ (Suc\ n)
   1.102 +\rulename{add_2_eq_Suc'}
   1.103 +\end{isabelle}
   1.104 +In special circumstances, you may wish to remove or reorient 
   1.105 +these rules. 
   1.106 +
   1.107 +\subsubsection{Typical lemmas}
   1.108 +Inequalities involving addition and subtraction alone can be proved
   1.109 +automatically.  Lemmas such as these can be used to prove inequalities
   1.110 +involving multiplication and division:
   1.111 +\begin{isabelle}
   1.112 +\isasymlbrakk i\ \isasymle \ j;\ k\ \isasymle \ l\isasymrbrakk \ \isasymLongrightarrow \ i\ *\ k\ \isasymle \ j\ *\ l%
   1.113 +\rulename{mult_le_mono}\isanewline
   1.114 +\isasymlbrakk i\ <\ j;\ 0\ <\ k\isasymrbrakk \ \isasymLongrightarrow \ i\
   1.115 +*\ k\ <\ j\ *\ k%
   1.116 +\rulename{mult_less_mono1}\isanewline
   1.117 +m\ \isasymle \ n\ \isasymLongrightarrow \ m\ div\ k\ \isasymle \ n\ div\ k%
   1.118 +\rulename{div_le_mono}
   1.119 +\end{isabelle}
   1.120 +%
   1.121 +Various distributive laws concerning multiplication are available:
   1.122 +\begin{isabelle}
   1.123 +(m\ +\ n)\ *\ k\ =\ m\ *\ k\ +\ n\ *\ k%
   1.124 +\rulename{add_mult_distrib}\isanewline
   1.125 +(m\ -\ n)\ *\ k\ =\ m\ *\ k\ -\ n\ *\ k%
   1.126 +\rulename{diff_mult_distrib}\isanewline
   1.127 +(m\ mod\ n)\ *\ k\ =\ (m\ *\ k)\ mod\ (n\ *\ k)
   1.128 +\rulename{mod_mult_distrib}
   1.129 +\end{isabelle}
   1.130 +
   1.131 +\subsubsection{Division}
   1.132 +The library contains the basic facts about quotient and remainder
   1.133 +(including the analogous equation, \isa{div_if}):
   1.134 +\begin{isabelle}
   1.135 +m\ mod\ n\ =\ (if\ m\ <\ n\ then\ m\ else\ (m\ -\ n)\ mod\ n)
   1.136 +\rulename{mod_if}\isanewline
   1.137 +m\ div\ n\ *\ n\ +\ m\ mod\ n\ =\ m%
   1.138 +\rulename{mod_div_equality}
   1.139 +\end{isabelle}
   1.140 +
   1.141 +Many less obvious facts about quotient and remainder are also provided. 
   1.142 +Here is a selection:
   1.143 +\begin{isabelle}
   1.144 +a\ *\ b\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c%
   1.145 +\rulename{div_mult1_eq}\isanewline
   1.146 +a\ *\ b\ mod\ c\ =\ a\ *\ (b\ mod\ c)\ mod\ c%
   1.147 +\rulename{mod_mult1_eq}\isanewline
   1.148 +a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%
   1.149 +\rulename{div_mult2_eq}\isanewline
   1.150 +a\ mod\ (b*c)\ =\ b * (a\ div\ b\ mod\ c)\ +\ a\ mod\ b%
   1.151 +\rulename{mod_mult2_eq}\isanewline
   1.152 +0\ <\ c\ \isasymLongrightarrow \ (c\ *\ a)\ div\ (c\ *\ b)\ =\ a\ div\ b%
   1.153 +\rulename{div_mult_mult1}
   1.154 +\end{isabelle}
   1.155 +
   1.156 +Surprisingly few of these results depend upon the
   1.157 +divisors' being nonzero.  Isabelle/HOL defines division by zero:
   1.158 +\begin{isabelle}
   1.159 +a\ div\ 0\ =\ 0
   1.160 +\rulename{DIVISION_BY_ZERO_DIV}\isanewline
   1.161 +a\ mod\ 0\ =\ a%
   1.162 +\rulename{DIVISION_BY_ZERO_MOD}
   1.163 +\end{isabelle}
   1.164 +As a concession to convention, these equations are not installed as default
   1.165 +simplification rules but are merely used to remove nonzero-divisor
   1.166 +hypotheses by case analysis.  In \isa{div_mult_mult1} above, one of
   1.167 +the two divisors (namely~\isa{c}) must be still be nonzero.
   1.168 +
   1.169 +The \textbf{divides} relation has the standard definition, which
   1.170 +is overloaded over all numeric types: 
   1.171 +\begin{isabelle}
   1.172 +m\ dvd\ n\ \isasymequiv\ {\isasymexists}k.\ n\ =\ m\ *\ k
   1.173 +\rulename{dvd_def}
   1.174 +\end{isabelle}
   1.175 +%
   1.176 +Section~\ref{sec:proving-euclid} discusses proofs involving this
   1.177 +relation.  Here are some of the facts proved about it:
   1.178 +\begin{isabelle}
   1.179 +\isasymlbrakk m\ dvd\ n;\ n\ dvd\ m\isasymrbrakk \ \isasymLongrightarrow \ m\ =\ n%
   1.180 +\rulename{dvd_anti_sym}\isanewline
   1.181 +\isasymlbrakk k\ dvd\ m;\ k\ dvd\ n\isasymrbrakk \ \isasymLongrightarrow \ k\ dvd\ (m\ +\ n)
   1.182 +\rulename{dvd_add}
   1.183 +\end{isabelle}
   1.184 +
   1.185 +\subsubsection{Simplifier tricks}
   1.186 +The rule \isa{diff_mult_distrib} shown above is one of the few facts
   1.187 +about \isa{m\ -\ n} that is not subject to
   1.188 +the condition \isa{n\ \isasymle \  m}.  Natural number subtraction has few
   1.189 +nice properties; often it is best to remove it from a subgoal
   1.190 +using this split rule:
   1.191 +\begin{isabelle}
   1.192 +P(a-b)\ =\ ((a<b\ \isasymlongrightarrow \ P\
   1.193 +0)\ \isasymand \ (\isasymforall d.\ a\ =\ b+d\ \isasymlongrightarrow \ P\
   1.194 +d))
   1.195 +\rulename{nat_diff_split}
   1.196 +\end{isabelle}
   1.197 +For example, it proves the following fact, which lies outside the scope of
   1.198 +linear arithmetic:
   1.199 +\begin{isabelle}
   1.200 +\isacommand{lemma}\ "(n-1)*(n+1)\ =\ n*n\ -\ 1"\isanewline
   1.201 +\isacommand{apply}\ (simp\ split:\ nat_diff_split)\isanewline
   1.202 +\isacommand{done}
   1.203 +\end{isabelle}
   1.204 +
   1.205 +Suppose that two expressions are equal, differing only in 
   1.206 +associativity and commutativity of addition.  Simplifying with the
   1.207 +following equations sorts the terms and groups them to the right, making
   1.208 +the two expressions identical:
   1.209 +\begin{isabelle}
   1.210 +m\ +\ n\ +\ k\ =\ m\ +\ (n\ +\ k)
   1.211 +\rulename{add_assoc}\isanewline
   1.212 +m\ +\ n\ =\ n\ +\ m%
   1.213 +\rulename{add_commute}\isanewline
   1.214 +x\ +\ (y\ +\ z)\ =\ y\ +\ (x\
   1.215 ++\ z)
   1.216 +\rulename{add_left_commute}
   1.217 +\end{isabelle}
   1.218 +The name \isa{add_ac} refers to the list of all three theorems, similarly
   1.219 +there is \isa{mult_ac}.  Here is an example of the sorting effect.  Start
   1.220 +with this goal:
   1.221 +\begin{isabelle}
   1.222 +\ 1.\ Suc\ (i\ +\ j\ *\ l\ *\ k\ +\ m\ *\ n)\ =\
   1.223 +f\ (n\ *\ m\ +\ i\ +\ k\ *\ j\ *\ l)
   1.224 +\end{isabelle}
   1.225 +%
   1.226 +Simplify using  \isa{add_ac} and \isa{mult_ac}:
   1.227 +\begin{isabelle}
   1.228 +\isacommand{apply}\ (simp\ add:\ add_ac\ mult_ac)
   1.229 +\end{isabelle}
   1.230 +%
   1.231 +Here is the resulting subgoal:
   1.232 +\begin{isabelle}
   1.233 +\ 1.\ Suc\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))\
   1.234 +=\ f\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))%
   1.235 +\end{isabelle}
   1.236 +
   1.237 +
   1.238 +\subsection{The type of integers, {\tt\slshape int}}
   1.239 +
   1.240 +Reasoning methods resemble those for the natural numbers, but
   1.241 +induction and the constant \isa{Suc} are not available.
   1.242 +
   1.243 +Concerning simplifier tricks, we have no need to eliminate subtraction (it
   1.244 +is well-behaved), but the simplifier can sort the operands of integer
   1.245 +operators.  The name \isa{zadd_ac} refers to the associativity and
   1.246 +commutativity theorems for integer addition, while \isa{zmult_ac} has the
   1.247 +analogous theorems for multiplication.  The prefix~\isa{z} in many theorem
   1.248 +names recalls the use of $\Bbb{Z}$ to denote the set of integers.
   1.249 +
   1.250 +For division and remainder, the treatment of negative divisors follows
   1.251 +traditional mathematical practice: the sign of the remainder follows that
   1.252 +of the divisor:
   1.253 +\begin{isabelle}
   1.254 +\#0\ <\ b\ \isasymLongrightarrow \ \#0\ \isasymle \ a\ mod\ b%
   1.255 +\rulename{pos_mod_sign}\isanewline
   1.256 +\#0\ <\ b\ \isasymLongrightarrow \ a\ mod\ b\ <\ b%
   1.257 +\rulename{pos_mod_bound}\isanewline
   1.258 +b\ <\ \#0\ \isasymLongrightarrow \ a\ mod\ b\ \isasymle \ \#0
   1.259 +\rulename{neg_mod_sign}\isanewline
   1.260 +b\ <\ \#0\ \isasymLongrightarrow \ b\ <\ a\ mod\ b%
   1.261 +\rulename{neg_mod_bound}
   1.262 +\end{isabelle}
   1.263 +ML treats negative divisors in the same way, but most computer hardware
   1.264 +treats signed operands using the same rules as for multiplication.
   1.265 +
   1.266 +The library provides many lemmas for proving inequalities involving integer
   1.267 +multiplication and division, similar to those shown above for
   1.268 +type~\isa{nat}.  The absolute value function \isa{abs} is
   1.269 +defined for the integers; we have for example the obvious law
   1.270 +\begin{isabelle}
   1.271 +\isasymbar x\ *\ y\isasymbar \ =\ \isasymbar x\isasymbar \ *\ \isasymbar y\isasymbar 
   1.272 +\rulename{abs_mult}
   1.273 +\end{isabelle}
   1.274 +
   1.275 +Again, many facts about quotients and remainders are provided:
   1.276 +\begin{isabelle}
   1.277 +(a\ +\ b)\ div\ c\ =\isanewline
   1.278 +a\ div\ c\ +\ b\ div\ c\ +\ (a\ mod\ c\ +\ b\ mod\ c)\ div\ c%
   1.279 +\rulename{zdiv_zadd1_eq}
   1.280 +\par\smallskip
   1.281 +(a\ +\ b)\ mod\ c\ =\ (a\ mod\ c\ +\ b\ mod\ c)\ mod\ c%
   1.282 +\rulename{zmod_zadd1_eq}
   1.283 +\end{isabelle}
   1.284 +
   1.285 +\begin{isabelle}
   1.286 +(a\ *\ b)\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c%
   1.287 +\rulename{zdiv_zmult1_eq}\isanewline
   1.288 +(a\ *\ b)\ mod\ c\ =\ a\ *\ (b\ mod\ c)\ mod\ c%
   1.289 +\rulename{zmod_zmult1_eq}
   1.290 +\end{isabelle}
   1.291 +
   1.292 +\begin{isabelle}
   1.293 +\#0\ <\ c\ \isasymLongrightarrow \ a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%
   1.294 +\rulename{zdiv_zmult2_eq}\isanewline
   1.295 +\#0\ <\ c\ \isasymLongrightarrow \ a\ mod\ (b*c)\ =\ b*(a\ div\ b\ mod\
   1.296 +c)\ +\ a\ mod\ b%
   1.297 +\rulename{zmod_zmult2_eq}
   1.298 +\end{isabelle}
   1.299 +The last two differ from their natural number analogues by requiring
   1.300 +\isa{c} to be positive.  Since division by zero yields zero, we could allow
   1.301 +\isa{c} to be zero.  However, \isa{c} cannot be negative: a counterexample
   1.302 +is
   1.303 +$\isa{a} = 7$, $\isa{b} = 2$ and $\isa{c} = -3$, when the left-hand side of
   1.304 +\isa{zdiv_zmult2_eq} is $-2$ while the right-hand side is $-1$.
   1.305 +
   1.306 +
   1.307 +\subsection{The type of real numbers, {\tt\slshape real}}
   1.308 +
   1.309 +As with the other numeric types, the simplifier can sort the operands of
   1.310 +addition and multiplication.  The name \isa{real_add_ac} refers to the
   1.311 +associativity and commutativity theorems for addition; similarly
   1.312 +\isa{real_mult_ac} contains those properties for multiplication. 
   1.313 +
   1.314 +\textbf{To be written.  Inverse, abs, theorems about density, etc.?}