summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/TutorialI/Types/numerics.tex

author | nipkow |

Fri, 16 Feb 2001 08:10:28 +0100 | |

changeset 11148 | 79aa2932b2d7 |

parent 10983 | 59961d32b1ae |

child 11161 | 166f7d87b37f |

permissions | -rw-r--r-- |

*** empty log message ***

% $Id$ Until now, our numerical have used the type of \textbf{natural numbers}, \isa{nat}. This is a recursive datatype generated by the constructors zero and successor, so it works well with inductive proofs and primitive recursive function definitions. Isabelle/HOL also provides the type \isa{int} of \textbf{integers}, which lack induction but support true subtraction. The logic HOL-Real also has the type \isa{real} of real numbers. Isabelle has no subtyping, so the numeric types are distinct and there are functions to convert between them. Fortunately most numeric operations are overloaded: the same symbol can be used at all numeric types. Table~\ref{tab:overloading} in the appendix shows the most important operations, together with the priorities of the infix symbols. The integers are preferable to the natural numbers for reasoning about complicated arithmetic expressions. For example, a termination proof typically involves an integer metric that is shown to decrease at each loop iteration. Even if the metric cannot become negative, proofs may be easier if you use the integers instead of the natural numbers. Many theorems involving numeric types can be proved automatically by Isabelle's arithmetic decision procedure, the method \isa{arith}. Linear arithmetic comprises addition, subtraction and multiplication by constant factors; subterms involving other operators are regarded as variables. The procedure can be slow, especially if the subgoal to be proved involves subtraction over type \isa{nat}, which causes case splits. The simplifier reduces arithmetic expressions in other ways, such as dividing through by common factors. For problems that lie outside the scope of automation, HOL provides hundreds of theorems about multiplication, division, etc., that can be brought to bear. You can locate them using Proof General's Find button. A few lemmas are given below to show what is available. \subsection{Numeric Literals} \label{sec:numerals} Literals are available for the types of natural numbers, integers and reals and denote integer values of arbitrary size. They begin with a number sign (\isa{\#}), have an optional minus sign (\isa{-}) and then one or more decimal digits. Examples are \isa{\#0}, \isa{\#-3} and \isa{\#441223334678}. Literals look like constants, but they abbreviate terms, representing the number in a two's complement binary notation. Isabelle performs arithmetic on literals by rewriting rather than using the hardware arithmetic. In most cases arithmetic is fast enough, even for large numbers. The arithmetic operations provided for literals include addition, subtraction, multiplication, integer division and remainder. Fractions of literals (expressed using division) are reduced to lowest terms. \begin{warn} The arithmetic operators are overloaded, so you must be careful to ensure that each numeric expression refers to a specific type, if necessary by inserting type constraints. Here is an example of what can go wrong: \par \begin{isabelle} \isacommand{lemma}\ "\#2\ *\ m\ =\ m\ +\ m" \end{isabelle} % Carefully observe how Isabelle displays the subgoal: \begin{isabelle} \ 1.\ (\#2::'a)\ *\ m\ =\ m\ +\ m \end{isabelle} The type \isa{'a} given for the literal \isa{\#2} warns us that no numeric type has been specified. The problem is underspecified. Given a type constraint such as \isa{nat}, \isa{int} or \isa{real}, it becomes trivial. \end{warn} \begin{warn} Numeric literals are not constructors and therefore must not be used in patterns. For example, this declaration is rejected: \begin{isabelle} \isacommand{recdef}\ h\ "\isacharbraceleft \isacharbraceright "\isanewline "h\ \#3\ =\ \#2"\isanewline "h\ i\ \ =\ i" \end{isabelle} You should use a conditional expression instead: \begin{isabelle} "h\ i\ =\ (if\ i\ =\ \#3\ then\ \#2\ else\ i)" \end{isabelle} \end{warn} \subsection{The type of natural numbers, {\tt\slshape nat}} This type requires no introduction: we have been using it from the beginning. Hundreds of theorems about the natural numbers are proved in the theories \isa{Nat}, \isa{NatArith} and \isa{Divides}. Only in exceptional circumstances should you resort to induction. \subsubsection{Literals} The notational options for the natural numbers can be confusing. The constant \isa{0} is overloaded to serve as the neutral value in a variety of additive types. The symbols \isa{1} and \isa{2} are not constants but abbreviations for \isa{Suc 0} and \isa{Suc(Suc 0)}, respectively. The literals \isa{\#0}, \isa{\#1} and \isa{\#2} are syntactically different from \isa{0}, \isa{1} and \isa{2}. You will sometimes prefer one notation to the other. Literals are obviously necessary to express large values, while \isa{0} and \isa{Suc} are needed in order to match many theorems, including the rewrite rules for primitive recursive functions. The following default simplification rules replace small literals by zero and successor: \begin{isabelle} \#0\ =\ 0 \rulename{numeral_0_eq_0}\isanewline \#1\ =\ 1 \rulename{numeral_1_eq_1}\isanewline \#2\ +\ n\ =\ Suc\ (Suc\ n) \rulename{add_2_eq_Suc}\isanewline n\ +\ \#2\ =\ Suc\ (Suc\ n) \rulename{add_2_eq_Suc'} \end{isabelle} In special circumstances, you may wish to remove or reorient these rules. \subsubsection{Typical lemmas} Inequalities involving addition and subtraction alone can be proved automatically. Lemmas such as these can be used to prove inequalities involving multiplication and division: \begin{isabelle} \isasymlbrakk i\ \isasymle \ j;\ k\ \isasymle \ l\isasymrbrakk \ \isasymLongrightarrow \ i\ *\ k\ \isasymle \ j\ *\ l% \rulename{mult_le_mono}\isanewline \isasymlbrakk i\ <\ j;\ 0\ <\ k\isasymrbrakk \ \isasymLongrightarrow \ i\ *\ k\ <\ j\ *\ k% \rulename{mult_less_mono1}\isanewline m\ \isasymle \ n\ \isasymLongrightarrow \ m\ div\ k\ \isasymle \ n\ div\ k% \rulename{div_le_mono} \end{isabelle} % Various distributive laws concerning multiplication are available: \begin{isabelle} (m\ +\ n)\ *\ k\ =\ m\ *\ k\ +\ n\ *\ k% \rulename{add_mult_distrib}\isanewline (m\ -\ n)\ *\ k\ =\ m\ *\ k\ -\ n\ *\ k% \rulename{diff_mult_distrib}\isanewline (m\ mod\ n)\ *\ k\ =\ (m\ *\ k)\ mod\ (n\ *\ k) \rulename{mod_mult_distrib} \end{isabelle} \subsubsection{Division} The infix operators \isa{div} and \isa{mod} are overloaded. Isabelle/HOL provides the basic facts about quotient and remainder on the natural numbers: \begin{isabelle} m\ mod\ n\ =\ (if\ m\ <\ n\ then\ m\ else\ (m\ -\ n)\ mod\ n) \rulename{mod_if}\isanewline m\ div\ n\ *\ n\ +\ m\ mod\ n\ =\ m% \rulename{mod_div_equality} \end{isabelle} Many less obvious facts about quotient and remainder are also provided. Here is a selection: \begin{isabelle} a\ *\ b\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c% \rulename{div_mult1_eq}\isanewline a\ *\ b\ mod\ c\ =\ a\ *\ (b\ mod\ c)\ mod\ c% \rulename{mod_mult1_eq}\isanewline a\ div\ (b*c)\ =\ a\ div\ b\ div\ c% \rulename{div_mult2_eq}\isanewline a\ mod\ (b*c)\ =\ b * (a\ div\ b\ mod\ c)\ +\ a\ mod\ b% \rulename{mod_mult2_eq}\isanewline 0\ <\ c\ \isasymLongrightarrow \ (c\ *\ a)\ div\ (c\ *\ b)\ =\ a\ div\ b% \rulename{div_mult_mult1} \end{isabelle} Surprisingly few of these results depend upon the divisors' being nonzero. That is because division by zero yields zero: \begin{isabelle} a\ div\ 0\ =\ 0 \rulename{DIVISION_BY_ZERO_DIV}\isanewline a\ mod\ 0\ =\ a% \rulename{DIVISION_BY_ZERO_MOD} \end{isabelle} As a concession to convention, these equations are not installed as default simplification rules but are merely used to remove nonzero-divisor hypotheses by case analysis. In \isa{div_mult_mult1} above, one of the two divisors (namely~\isa{c}) must be still be nonzero. The \textbf{divides} relation has the standard definition, which is overloaded over all numeric types: \begin{isabelle} m\ dvd\ n\ \isasymequiv\ {\isasymexists}k.\ n\ =\ m\ *\ k \rulename{dvd_def} \end{isabelle} % Section~\ref{sec:proving-euclid} discusses proofs involving this relation. Here are some of the facts proved about it: \begin{isabelle} \isasymlbrakk m\ dvd\ n;\ n\ dvd\ m\isasymrbrakk \ \isasymLongrightarrow \ m\ =\ n% \rulename{dvd_anti_sym}\isanewline \isasymlbrakk k\ dvd\ m;\ k\ dvd\ n\isasymrbrakk \ \isasymLongrightarrow \ k\ dvd\ (m\ +\ n) \rulename{dvd_add} \end{isabelle} \subsubsection{Simplifier tricks} The rule \isa{diff_mult_distrib} shown above is one of the few facts about \isa{m\ -\ n} that is not subject to the condition \isa{n\ \isasymle \ m}. Natural number subtraction has few nice properties; often you should remove it by simplifying with this split rule: \begin{isabelle} P(a-b)\ =\ ((a<b\ \isasymlongrightarrow \ P\ 0)\ \isasymand \ (\isasymforall d.\ a\ =\ b+d\ \isasymlongrightarrow \ P\ d)) \rulename{nat_diff_split} \end{isabelle} For example, it proves the following fact, which lies outside the scope of linear arithmetic: \begin{isabelle} \isacommand{lemma}\ "(n-1)*(n+1)\ =\ n*n\ -\ 1"\isanewline \isacommand{apply}\ (simp\ split:\ nat_diff_split)\isanewline \isacommand{done} \end{isabelle} Suppose that two expressions are equal, differing only in associativity and commutativity of addition. Simplifying with the following equations sorts the terms and groups them to the right, making the two expressions identical: \begin{isabelle} m\ +\ n\ +\ k\ =\ m\ +\ (n\ +\ k) \rulename{add_assoc}\isanewline m\ +\ n\ =\ n\ +\ m% \rulename{add_commute}\isanewline x\ +\ (y\ +\ z)\ =\ y\ +\ (x\ +\ z) \rulename{add_left_commute} \end{isabelle} The name \isa{add_ac} refers to the list of all three theorems, similarly there is \isa{mult_ac}. Here is an example of the sorting effect. Start with this goal: \begin{isabelle} \ 1.\ Suc\ (i\ +\ j\ *\ l\ *\ k\ +\ m\ *\ n)\ =\ f\ (n\ *\ m\ +\ i\ +\ k\ *\ j\ *\ l) \end{isabelle} % Simplify using \isa{add_ac} and \isa{mult_ac}: \begin{isabelle} \isacommand{apply}\ (simp\ add:\ add_ac\ mult_ac) \end{isabelle} % Here is the resulting subgoal: \begin{isabelle} \ 1.\ Suc\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))\ =\ f\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))% \end{isabelle} \subsection{The type of integers, {\tt\slshape int}} Reasoning methods resemble those for the natural numbers, but induction and the constant \isa{Suc} are not available. HOL provides many lemmas for proving inequalities involving integer multiplication and division, similar to those shown above for type~\isa{nat}. The absolute value function \isa{abs} is overloaded for the numeric types. It is defined for the integers; we have for example the obvious law \begin{isabelle} \isasymbar x\ *\ y\isasymbar \ =\ \isasymbar x\isasymbar \ *\ \isasymbar y\isasymbar \rulename{abs_mult} \end{isabelle} \begin{warn} The absolute value bars shown above cannot be typed on a keyboard. They can be entered using the X-symbol package. In \textsc{ascii}, type \isa{abs x} to get \isa{\isasymbar x\isasymbar}. \end{warn} The \isa{arith} method can prove facts about \isa{abs} automatically, though as it does so by case analysis, the cost can be exponential. \begin{isabelle} \isacommand{lemma}\ "\isasymlbrakk abs\ x\ <\ a;\ abs\ y\ <\ b\isasymrbrakk \ \isasymLongrightarrow \ abs\ x\ +\ abs\ y\ <\ (a\ +\ b\ ::\ int)"\isanewline \isacommand{by}\ arith \end{isabelle} Concerning simplifier tricks, we have no need to eliminate subtraction: it is well-behaved. As with the natural numbers, the simplifier can sort the operands of sums and products. The name \isa{zadd_ac} refers to the associativity and commutativity theorems for integer addition, while \isa{zmult_ac} has the analogous theorems for multiplication. The prefix~\isa{z} in many theorem names recalls the use of $\mathbb{Z}$ to denote the set of integers. For division and remainder, the treatment of negative divisors follows mathematical practice: the sign of the remainder follows that of the divisor: \begin{isabelle} \#0\ <\ b\ \isasymLongrightarrow \ \#0\ \isasymle \ a\ mod\ b% \rulename{pos_mod_sign}\isanewline \#0\ <\ b\ \isasymLongrightarrow \ a\ mod\ b\ <\ b% \rulename{pos_mod_bound}\isanewline b\ <\ \#0\ \isasymLongrightarrow \ a\ mod\ b\ \isasymle \ \#0 \rulename{neg_mod_sign}\isanewline b\ <\ \#0\ \isasymLongrightarrow \ b\ <\ a\ mod\ b% \rulename{neg_mod_bound} \end{isabelle} ML treats negative divisors in the same way, but most computer hardware treats signed operands using the same rules as for multiplication. Many facts about quotients and remainders are provided: \begin{isabelle} (a\ +\ b)\ div\ c\ =\isanewline a\ div\ c\ +\ b\ div\ c\ +\ (a\ mod\ c\ +\ b\ mod\ c)\ div\ c% \rulename{zdiv_zadd1_eq} \par\smallskip (a\ +\ b)\ mod\ c\ =\ (a\ mod\ c\ +\ b\ mod\ c)\ mod\ c% \rulename{zmod_zadd1_eq} \end{isabelle} \begin{isabelle} (a\ *\ b)\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c% \rulename{zdiv_zmult1_eq}\isanewline (a\ *\ b)\ mod\ c\ =\ a\ *\ (b\ mod\ c)\ mod\ c% \rulename{zmod_zmult1_eq} \end{isabelle} \begin{isabelle} \#0\ <\ c\ \isasymLongrightarrow \ a\ div\ (b*c)\ =\ a\ div\ b\ div\ c% \rulename{zdiv_zmult2_eq}\isanewline \#0\ <\ c\ \isasymLongrightarrow \ a\ mod\ (b*c)\ =\ b*(a\ div\ b\ mod\ c)\ +\ a\ mod\ b% \rulename{zmod_zmult2_eq} \end{isabelle} The last two differ from their natural number analogues by requiring \isa{c} to be positive. Since division by zero yields zero, we could allow \isa{c} to be zero. However, \isa{c} cannot be negative: a counterexample is $\isa{a} = 7$, $\isa{b} = 2$ and $\isa{c} = -3$, when the left-hand side of \isa{zdiv_zmult2_eq} is $-2$ while the right-hand side is~$-1$. \subsection{The type of real numbers, {\tt\slshape real}} The real numbers enjoy two significant properties that the integers lack. They are \textbf{dense}: between every two distinct real numbers there lies another. This property follows from the division laws, since if $x<y$ then between them lies $(x+y)/2$. The second property is that they are \textbf{complete}: every set of reals that is bounded above has a least upper bound. Completeness distinguishes the reals from the rationals, for which the set $\{x\mid x^2<2\}$ has no least upper bound. (It could only be $\surd2$, which is irrational.) The formalization of completeness is complicated; rather than reproducing it here, we refer you to the theory \texttt{RComplete} in directory \texttt{Real}. Density, however, is trivial to express: \begin{isabelle} x\ <\ y\ \isasymLongrightarrow \ \isasymexists r.\ x\ <\ r\ \isasymand \ r\ <\ y% \rulename{real_dense} \end{isabelle} Here is a selection of rules about the division operator. The following are installed as default simplification rules in order to express combinations of products and quotients as rational expressions: \begin{isabelle} x\ *\ (y\ /\ z)\ =\ x\ *\ y\ /\ z% \rulename{real_times_divide1_eq}\isanewline y\ /\ z\ *\ x\ =\ y\ *\ x\ /\ z% \rulename{real_times_divide2_eq}\isanewline x\ /\ (y\ /\ z)\ =\ x\ *\ z\ /\ y% \rulename{real_divide_divide1_eq}\isanewline x\ /\ y\ /\ z\ =\ x\ /\ (y\ *\ z) \rulename{real_divide_divide2_eq} \end{isabelle} Signs are extracted from quotients in the hope that complementary terms can then be cancelled: \begin{isabelle} -\ x\ /\ y\ =\ -\ (x\ /\ y) \rulename{real_minus_divide_eq}\isanewline x\ /\ -\ y\ =\ -\ (x\ /\ y) \rulename{real_divide_minus_eq} \end{isabelle} The following distributive law is available, but it is not installed as a simplification rule. \begin{isabelle} (x\ +\ y)\ /\ z\ =\ x\ /\ z\ +\ y\ /\ z% \rulename{real_add_divide_distrib} \end{isabelle} As with the other numeric types, the simplifier can sort the operands of addition and multiplication. The name \isa{real_add_ac} refers to the associativity and commutativity theorems for addition, while similarly \isa{real_mult_ac} contains those properties for multiplication. The absolute value function \isa{abs} is defined for the reals, along with many theorems such as this one about exponentiation: \begin{isabelle} \isasymbar r\isasymbar \ \isacharcircum \ n\ =\ \isasymbar r\ \isacharcircum \ n\isasymbar \rulename{realpow_abs} \end{isabelle} \begin{warn} Type \isa{real} is only available in the logic HOL-Real, which is HOL extended with the rather substantial development of the real numbers. Base your theory upon theory \isa{Real}, not the usual \isa{Main}. \end{warn} Also distributed with Isabelle is HOL-Hyperreal, whose theory \isa{Hyperreal} defines the type \isa{hypreal} of non-standard reals. These \textbf{hyperreals} include infinitesimals, which represent infinitely small and infinitely large quantities; they facilitate proofs about limits, differentiation and integration~\cite{fleuriot-jcm}. The development defines an infinitely large number, \isa{omega} and an infinitely small positive number, \isa{epsilon}. The relation $x\approx y$ means ``$x$ is infinitely close to~$y$''.