doc-src/TutorialI/Types/numerics.tex
changeset 10794 65d18005d802
parent 10779 b0d961105f46
child 10881 03f06372230b
     1.1 --- a/doc-src/TutorialI/Types/numerics.tex	Fri Jan 05 18:31:48 2001 +0100
     1.2 +++ b/doc-src/TutorialI/Types/numerics.tex	Fri Jan 05 18:32:33 2001 +0100
     1.3 @@ -1,17 +1,18 @@
     1.4 -Our examples until now have used the type of \textbf{natural numbers},
     1.5 +% $Id$
     1.6 +Until now, our numerical have used the type of \textbf{natural numbers},
     1.7  \isa{nat}.  This is a recursive datatype generated by the constructors
     1.8  zero  and successor, so it works well with inductive proofs and primitive
     1.9 -recursive function definitions. Isabelle/HOL also has the type \isa{int} of
    1.10 -\textbf{integers}, which gives up induction in exchange  for proper
    1.11 -subtraction. The logic HOL-Real also has the type \isa{real} of real
    1.12 +recursive function definitions. Isabelle/HOL also provides the type
    1.13 +\isa{int} of \textbf{integers}, which lack induction but support true
    1.14 +subtraction. The logic HOL-Real\REMARK{now part of HOL?} also has the type \isa{real} of real
    1.15  numbers.  Isabelle has no subtyping,  so the numeric types are distinct and
    1.16  there are  functions to convert between them. 
    1.17  
    1.18  The integers are preferable to the natural  numbers for reasoning about
    1.19  complicated arithmetic expressions. For  example, a termination proof
    1.20  typically involves an integer metric  that is shown to decrease at each
    1.21 -loop iteration. Even if the  metric cannot become negative, proofs about it
    1.22 -are usually easier  if the integers are used rather than the natural
    1.23 +loop iteration. Even if the  metric cannot become negative, proofs 
    1.24 +may be easier if you use the integers instead of the natural
    1.25  numbers. 
    1.26  
    1.27  Many theorems involving numeric types can be proved automatically by
    1.28 @@ -26,8 +27,9 @@
    1.29  ways, such as dividing through by common factors.  For problems that lie
    1.30  outside the scope of automation, the library has hundreds of
    1.31  theorems about multiplication, division, etc., that can be brought to
    1.32 -bear.  You can find find them by browsing the library.  Some
    1.33 -useful lemmas are shown below.
    1.34 +bear.  You can find find them by browsing the library or by using the Find
    1.35 +button in Proof General.  A few lemmas are given below to show what
    1.36 +is available.
    1.37  
    1.38  \subsection{Numeric Literals}
    1.39  \label{sec:numerals}
    1.40 @@ -41,16 +43,19 @@
    1.41  
    1.42  Literals look like constants, but they abbreviate 
    1.43  terms, representing the number in a two's complement binary notation. 
    1.44 -Isabelle performs arithmetic on literals by rewriting, rather 
    1.45 +Isabelle performs arithmetic on literals by rewriting rather 
    1.46  than using the hardware arithmetic. In most cases arithmetic 
    1.47  is fast enough, even for large numbers. The arithmetic operations 
    1.48 -provided for literals are addition, subtraction, multiplication, 
    1.49 -integer division and remainder. 
    1.50 +provided for literals include addition, subtraction, multiplication, 
    1.51 +integer division and remainder.  Fractions of literals (expressed using
    1.52 +division) are reduced to lowest terms.
    1.53  
    1.54 -\emph{Beware}: the arithmetic operators are 
    1.55 +\begin{warn}
    1.56 +The arithmetic operators are 
    1.57  overloaded, so you must be careful to ensure that each numeric 
    1.58  expression refers to a specific type, if necessary by inserting 
    1.59  type constraints.  Here is an example of what can go wrong:
    1.60 +\par
    1.61  \begin{isabelle}
    1.62  \isacommand{lemma}\ "\#2\ *\ m\ =\ m\ +\ m"
    1.63  \end{isabelle}
    1.64 @@ -62,12 +67,14 @@
    1.65  The type \isa{'a} given for the literal \isa{\#2} warns us that no numeric
    1.66  type has been specified.  The problem is underspecified.  Given a type
    1.67  constraint such as \isa{nat}, \isa{int} or \isa{real}, it becomes trivial.
    1.68 +\end{warn}
    1.69 +
    1.70  
    1.71  
    1.72  \subsection{The type of natural numbers, {\tt\slshape nat}}
    1.73  
    1.74  This type requires no introduction: we have been using it from the
    1.75 -start.  Hundreds of useful lemmas about arithmetic on type \isa{nat} are
    1.76 +beginning.  Hundreds of theorems about the natural numbers are
    1.77  proved in the theories \isa{Nat}, \isa{NatArith} and \isa{Divides}.  Only
    1.78  in exceptional circumstances should you resort to induction.
    1.79  
    1.80 @@ -77,12 +84,12 @@
    1.81  in a variety of additive types. The symbols \isa{1} and \isa{2} are 
    1.82  not constants but abbreviations for \isa{Suc 0} and \isa{Suc(Suc 0)},
    1.83  respectively. The literals \isa{\#0}, \isa{\#1} and \isa{\#2}  are
    1.84 -entirely different from \isa{0}, \isa{1} and \isa{2}. You  will
    1.85 +syntactically different from \isa{0}, \isa{1} and \isa{2}. You  will
    1.86  sometimes prefer one notation to the other. Literals are  obviously
    1.87 -necessary to express large values, while \isa{0} and \isa{Suc}  are
    1.88 -needed in order to match many theorems, including the rewrite  rules for
    1.89 -primitive recursive functions. The following default  simplification rules
    1.90 -replace small literals by zero and successor: 
    1.91 +necessary to express large values, while \isa{0} and \isa{Suc}  are needed
    1.92 +in order to match many theorems, including the rewrite  rules for primitive
    1.93 +recursive functions. The following default  simplification rules replace
    1.94 +small literals by zero and successor: 
    1.95  \begin{isabelle}
    1.96  \#0\ =\ 0
    1.97  \rulename{numeral_0_eq_0}\isanewline
    1.98 @@ -146,7 +153,8 @@
    1.99  \end{isabelle}
   1.100  
   1.101  Surprisingly few of these results depend upon the
   1.102 -divisors' being nonzero.  Isabelle/HOL defines division by zero:
   1.103 +divisors' being nonzero.  That is because division by
   1.104 +zero yields zero:
   1.105  \begin{isabelle}
   1.106  a\ div\ 0\ =\ 0
   1.107  \rulename{DIVISION_BY_ZERO_DIV}\isanewline
   1.108 @@ -178,8 +186,8 @@
   1.109  The rule \isa{diff_mult_distrib} shown above is one of the few facts
   1.110  about \isa{m\ -\ n} that is not subject to
   1.111  the condition \isa{n\ \isasymle \  m}.  Natural number subtraction has few
   1.112 -nice properties; often it is best to remove it from a subgoal
   1.113 -using this split rule:
   1.114 +nice properties; often you should remove it by simplifying with this split
   1.115 +rule:
   1.116  \begin{isabelle}
   1.117  P(a-b)\ =\ ((a<b\ \isasymlongrightarrow \ P\
   1.118  0)\ \isasymand \ (\isasymforall d.\ a\ =\ b+d\ \isasymlongrightarrow \ P\
   1.119 @@ -229,18 +237,35 @@
   1.120  
   1.121  \subsection{The type of integers, {\tt\slshape int}}
   1.122  
   1.123 -Reasoning methods resemble those for the natural numbers, but
   1.124 -induction and the constant \isa{Suc} are not available.
   1.125 +Reasoning methods resemble those for the natural numbers, but induction and
   1.126 +the constant \isa{Suc} are not available.  The library provides many lemmas
   1.127 +for proving inequalities involving integer multiplication and division,
   1.128 +similar to those shown above for type~\isa{nat}.  
   1.129 +
   1.130 +The absolute value function \isa{abs} is overloaded for the numeric types.
   1.131 +It is defined for the integers; we have for example the obvious law
   1.132 +\begin{isabelle}
   1.133 +\isasymbar x\ *\ y\isasymbar \ =\ \isasymbar x\isasymbar \ *\ \isasymbar y\isasymbar 
   1.134 +\rulename{abs_mult}
   1.135 +\end{isabelle}
   1.136  
   1.137 -Concerning simplifier tricks, we have no need to eliminate subtraction (it
   1.138 -is well-behaved), but the simplifier can sort the operands of integer
   1.139 -operators.  The name \isa{zadd_ac} refers to the associativity and
   1.140 -commutativity theorems for integer addition, while \isa{zmult_ac} has the
   1.141 -analogous theorems for multiplication.  The prefix~\isa{z} in many theorem
   1.142 -names recalls the use of $\Bbb{Z}$ to denote the set of integers.
   1.143 +\begin{warn}
   1.144 +The absolute value bars shown above cannot be typed on a keyboard.  They
   1.145 +can be entered using the X-symbol package.  In ASCII, type \isa{abs x} to
   1.146 +get \isa{\isasymbar x\isasymbar}.
   1.147 +\end{warn}
   1.148 +
   1.149 +
   1.150 +Concerning simplifier tricks, we have no need to eliminate subtraction: it
   1.151 +is well-behaved.  As with the natural numbers, the simplifier can sort the
   1.152 +operands of sums and products.  The name \isa{zadd_ac} refers to the
   1.153 +associativity and commutativity theorems for integer addition, while
   1.154 +\isa{zmult_ac} has the analogous theorems for multiplication.  The
   1.155 +prefix~\isa{z} in many theorem names recalls the use of $\mathbb{Z}$ to
   1.156 +denote the set of integers.
   1.157  
   1.158  For division and remainder, the treatment of negative divisors follows
   1.159 -traditional mathematical practice: the sign of the remainder follows that
   1.160 +mathematical practice: the sign of the remainder follows that
   1.161  of the divisor:
   1.162  \begin{isabelle}
   1.163  \#0\ <\ b\ \isasymLongrightarrow \ \#0\ \isasymle \ a\ mod\ b%
   1.164 @@ -254,17 +279,7 @@
   1.165  \end{isabelle}
   1.166  ML treats negative divisors in the same way, but most computer hardware
   1.167  treats signed operands using the same rules as for multiplication.
   1.168 -
   1.169 -The library provides many lemmas for proving inequalities involving integer
   1.170 -multiplication and division, similar to those shown above for
   1.171 -type~\isa{nat}.  The absolute value function \isa{abs} is
   1.172 -defined for the integers; we have for example the obvious law
   1.173 -\begin{isabelle}
   1.174 -\isasymbar x\ *\ y\isasymbar \ =\ \isasymbar x\isasymbar \ *\ \isasymbar y\isasymbar 
   1.175 -\rulename{abs_mult}
   1.176 -\end{isabelle}
   1.177 -
   1.178 -Again, many facts about quotients and remainders are provided:
   1.179 +Many facts about quotients and remainders are provided:
   1.180  \begin{isabelle}
   1.181  (a\ +\ b)\ div\ c\ =\isanewline
   1.182  a\ div\ c\ +\ b\ div\ c\ +\ (a\ mod\ c\ +\ b\ mod\ c)\ div\ c%
   1.183 @@ -307,12 +322,10 @@
   1.184  upper bound.  Completeness distinguishes the reals from the rationals, for
   1.185  which the set $\{x\mid x^2<2\}$ has no least upper bound.  (It could only be
   1.186  $\surd2$, which is irrational.)
   1.187 -
   1.188 -The formalization of completeness is long and technical.  Rather than
   1.189 +The formalization of completeness is complicated; rather than
   1.190  reproducing it here, we refer you to the theory \texttt{RComplete} in
   1.191  directory \texttt{Real}.
   1.192 -
   1.193 -Density is trivial to express:
   1.194 +Density, however, is trivial to express:
   1.195  \begin{isabelle}
   1.196  x\ <\ y\ \isasymLongrightarrow \ \isasymexists r.\ x\ <\ r\ \isasymand \ r\ <\ y%
   1.197  \rulename{real_dense}
   1.198 @@ -361,7 +374,7 @@
   1.199  \rulename{realpow_abs}
   1.200  \end{isabelle}
   1.201  
   1.202 -\emph{Note}: Type \isa{real} is only available in the logic HOL-Real, which
   1.203 +\emph{Note}: Type \isa{real} is only available in the logic HOL-Real\REMARK{now part of HOL?}, which
   1.204  is  HOL extended with the rather substantial development of the real
   1.205  numbers.  Base your theory upon theory \isa{Real}, not the usual \isa{Main}.
   1.206  
   1.207 @@ -370,7 +383,7 @@
   1.208  reals.  These
   1.209  \textbf{hyperreals} include infinitesimals, which represent infinitely
   1.210  small and infinitely large quantities; they facilitate proofs
   1.211 -about limits, differentiation and integration.  The development defines an
   1.212 -infinitely large number, \isa{omega} and an infinitely small positive
   1.213 -number, \isa{epsilon}.  Also available is the approximates relation,
   1.214 -written $\approx$.
   1.215 +about limits, differentiation and integration~\cite{fleuriot-jcm}.  The
   1.216 +development defines an infinitely large number, \isa{omega} and an
   1.217 +infinitely small positive number, \isa{epsilon}.  Also available is the
   1.218 +approximates relation, written $\approx$.