author paulson Fri Jul 13 17:55:35 2001 +0200 (2001-07-13) changeset 11416 91886738773a parent 11415 34a76158cbb8 child 11417 499435b4084e
indexing
     1.1 --- a/doc-src/TutorialI/Types/numerics.tex	Fri Jul 13 13:58:41 2001 +0200
1.2 +++ b/doc-src/TutorialI/Types/numerics.tex	Fri Jul 13 17:55:35 2001 +0200
1.3 @@ -19,10 +19,10 @@
1.4  shows the most important operations, together with the priorities of the
1.5  infix symbols.
1.6
1.7 -
1.8 +\index{linear arithmetic}%
1.9  Many theorems involving numeric types can be proved automatically by
1.10  Isabelle's arithmetic decision procedure, the method
1.11 -\isa{arith}.  Linear arithmetic comprises addition, subtraction
1.12 +\methdx{arith}.  Linear arithmetic comprises addition, subtraction
1.13  and multiplication by constant factors; subterms involving other operators
1.14  are regarded as variables.  The procedure can be slow, especially if the
1.15  subgoal to be proved involves subtraction over type \isa{nat}, which
1.16 @@ -39,6 +39,7 @@
1.17  \subsection{Numeric Literals}
1.18  \label{sec:numerals}
1.19
1.20 +\index{numeric literals|(}%
1.21  Literals are available for the types of natural numbers, integers
1.22  and reals and denote integer values of arbitrary size.
1.23  They begin
1.24 @@ -55,7 +56,7 @@
1.25  integer division and remainder.  Fractions of literals (expressed using
1.26  division) are reduced to lowest terms.
1.27
1.28 -\begin{warn}
1.30  The arithmetic operators are
1.31  overloaded, so you must be careful to ensure that each numeric
1.32  expression refers to a specific type, if necessary by inserting
1.33 @@ -75,8 +76,10 @@
1.34  \end{warn}
1.35
1.36  \begin{warn}
1.37 -Numeric literals are not constructors and therefore must not be used in
1.38 -patterns.  For example, this declaration is rejected:
1.39 +\index{recdef@\protect\isacommand{recdef} (command)!and numeric literals}
1.40 +Numeric literals are not constructors and therefore
1.41 +must not be used in patterns.  For example, this declaration is
1.42 +rejected:
1.43  \begin{isabelle}
1.44  \isacommand{recdef}\ h\ "\isacharbraceleft \isacharbraceright "\isanewline
1.45  "h\ \#3\ =\ \#2"\isanewline
1.46 @@ -87,21 +90,24 @@
1.47  \begin{isabelle}
1.48  "h\ i\ =\ (if\ i\ =\ \#3\ then\ \#2\ else\ i)"
1.49  \end{isabelle}
1.50 +\index{numeric literals|)}
1.51  \end{warn}
1.52
1.53
1.54
1.55  \subsection{The Type of Natural Numbers, {\tt\slshape nat}}
1.56
1.57 +\index{natural numbers|(}\index{*nat (type)|(}%
1.58  This type requires no introduction: we have been using it from the
1.59  beginning.  Hundreds of theorems about the natural numbers are
1.60  proved in the theories \isa{Nat}, \isa{NatArith} and \isa{Divides}.  Only
1.61  in exceptional circumstances should you resort to induction.
1.62
1.63  \subsubsection{Literals}
1.64 -The notational options for the natural numbers can be confusing. The
1.65 -constant \isa{0} is overloaded to serve as the neutral value
1.66 -in a variety of additive types. The symbols \isa{1} and \isa{2} are
1.67 +\index{numeric literals!for type \protect\isa{nat}}%
1.68 +The notational options for the natural numbers are confusing.  The
1.69 +constant \cdx{0} is overloaded to serve as the neutral value
1.70 +in a variety of additive types. The symbols \sdx{1} and \sdx{2} are
1.71  not constants but abbreviations for \isa{Suc 0} and \isa{Suc(Suc 0)},
1.72  respectively. The literals \isa{\#0}, \isa{\#1} and \isa{\#2}  are
1.73  syntactically different from \isa{0}, \isa{1} and \isa{2}. You  will
1.74 @@ -140,14 +146,15 @@
1.75  Various distributive laws concerning multiplication are available:
1.76  \begin{isabelle}
1.77  (m\ +\ n)\ *\ k\ =\ m\ *\ k\ +\ n\ *\ k%
1.80  (m\ -\ n)\ *\ k\ =\ m\ *\ k\ -\ n\ *\ k%
1.81 -\rulename{diff_mult_distrib}\isanewline
1.82 +\rulenamedx{diff_mult_distrib}\isanewline
1.83  (m\ mod\ n)\ *\ k\ =\ (m\ *\ k)\ mod\ (n\ *\ k)
1.84 -\rulename{mod_mult_distrib}
1.85 +\rulenamedx{mod_mult_distrib}
1.86  \end{isabelle}
1.87
1.88  \subsubsection{Division}
1.89 +\index{division!for type \protect\isa{nat}}%
1.90  The infix operators \isa{div} and \isa{mod} are overloaded.
1.91  Isabelle/HOL provides the basic facts about quotient and remainder
1.92  on the natural numbers:
1.93 @@ -155,7 +162,7 @@
1.94  m\ mod\ n\ =\ (if\ m\ <\ n\ then\ m\ else\ (m\ -\ n)\ mod\ n)
1.95  \rulename{mod_if}\isanewline
1.96  m\ div\ n\ *\ n\ +\ m\ mod\ n\ =\ m%
1.97 -\rulename{mod_div_equality}
1.98 +\rulenamedx{mod_div_equality}
1.99  \end{isabelle}
1.100
1.101  Many less obvious facts about quotient and remainder are also provided.
1.102 @@ -174,7 +181,9 @@
1.103  \end{isabelle}
1.104
1.105  Surprisingly few of these results depend upon the
1.106 -divisors' being nonzero.  That is because division by
1.107 +divisors' being nonzero.
1.108 +\index{division!by zero}%
1.109 +That is because division by
1.110  zero yields zero:
1.111  \begin{isabelle}
1.112  a\ div\ 0\ =\ 0
1.113 @@ -186,20 +195,21 @@
1.114  simplification rules.  In \isa{div_mult_mult1} above, one of
1.115  the two divisors (namely~\isa{c}) must still be nonzero.
1.116
1.117 -The \textbf{divides} relation has the standard definition, which
1.118 +The \textbf{divides} relation\index{divides relation}
1.119 +has the standard definition, which
1.120  is overloaded over all numeric types:
1.121  \begin{isabelle}
1.122  m\ dvd\ n\ \isasymequiv\ {\isasymexists}k.\ n\ =\ m\ *\ k
1.123 -\rulename{dvd_def}
1.124 +\rulenamedx{dvd_def}
1.125  \end{isabelle}
1.126  %
1.127  Section~\ref{sec:proving-euclid} discusses proofs involving this
1.128  relation.  Here are some of the facts proved about it:
1.129  \begin{isabelle}
1.130  \isasymlbrakk m\ dvd\ n;\ n\ dvd\ m\isasymrbrakk \ \isasymLongrightarrow \ m\ =\ n%
1.131 -\rulename{dvd_anti_sym}\isanewline
1.132 +\rulenamedx{dvd_anti_sym}\isanewline
1.133  \isasymlbrakk k\ dvd\ m;\ k\ dvd\ n\isasymrbrakk \ \isasymLongrightarrow \ k\ dvd\ (m\ +\ n)
1.136  \end{isabelle}
1.137
1.138  \subsubsection{Simplifier Tricks}
1.139 @@ -228,9 +238,9 @@
1.140  the two expressions identical:
1.141  \begin{isabelle}
1.142  m\ +\ n\ +\ k\ =\ m\ +\ (n\ +\ k)
1.145  m\ +\ n\ =\ n\ +\ m%
1.148  x\ +\ (y\ +\ z)\ =\ y\ +\ (x\
1.149  +\ z)
1.151 @@ -252,17 +262,20 @@
1.152  \begin{isabelle}
1.153  \ 1.\ Suc\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))\
1.154  =\ f\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))%
1.155 -\end{isabelle}
1.156 +\end{isabelle}%
1.157 +\index{natural numbers|)}\index{*nat (type)|)}
1.158 +
1.159
1.160
1.161  \subsection{The Type of Integers, {\tt\slshape int}}
1.162
1.163 +\index{integers|(}\index{*int (type)|(}%
1.164  Reasoning methods resemble those for the natural numbers, but induction and
1.165  the constant \isa{Suc} are not available.  HOL provides many lemmas
1.166  for proving inequalities involving integer multiplication and division,
1.167  similar to those shown above for type~\isa{nat}.
1.168
1.169 -The absolute value function \isa{abs} is overloaded for the numeric types.
1.170 +The \rmindex{absolute value} function \cdx{abs} is overloaded for the numeric types.
1.171  It is defined for the integers; we have for example the obvious law
1.172  \begin{isabelle}
1.173  \isasymbar x\ *\ y\isasymbar \ =\ \isasymbar x\isasymbar \ *\ \isasymbar y\isasymbar
1.174 @@ -290,7 +303,8 @@
1.175  prefix~\isa{z} in many theorem names recalls the use of $\mathbb{Z}$ to
1.176  denote the set of integers.
1.177
1.178 -For division and remainder, the treatment of negative divisors follows
1.179 +For division and remainder,\index{division!by negative numbers}
1.180 +the treatment of negative divisors follows
1.181  mathematical practice: the sign of the remainder follows that
1.182  of the divisor:
1.183  \begin{isabelle}
1.184 @@ -334,11 +348,13 @@
1.185  \isa{c} to be zero.  However, \isa{c} cannot be negative: a counterexample
1.186  is
1.187  $\isa{a} = 7$, $\isa{b} = 2$ and $\isa{c} = -3$, when the left-hand side of
1.188 -\isa{zdiv_zmult2_eq} is $-2$ while the right-hand side is~$-1$.
1.189 +\isa{zdiv_zmult2_eq} is $-2$ while the right-hand side is~$-1$.%
1.190 +\index{integers|)}\index{*int (type)|)}
1.191
1.192
1.193  \subsection{The Type of Real Numbers, {\tt\slshape real}}
1.194
1.195 +\index{real numbers|(}\index{*real (type)|(}%
1.196  The real numbers enjoy two significant properties that the integers lack.
1.197  They are
1.198  \textbf{dense}: between every two distinct real numbers there lies another.
1.199 @@ -400,7 +416,8 @@
1.200  \rulename{realpow_abs}
1.201  \end{isabelle}
1.202
1.203 -Numeric literals for type \isa{real} have the same syntax as those for type
1.204 +Numeric literals\index{numeric literals!for type \protect\isa{real}}
1.205 +for type \isa{real} have the same syntax as those for type
1.206  \isa{int} and only express integral values.  Fractions expressed
1.207  using the division operator are automatically simplified to lowest terms:
1.208  \begin{isabelle}
1.209 @@ -417,15 +434,17 @@
1.210  Type \isa{real} is only available in the logic HOL-Real, which
1.211  is  HOL extended with the rather substantial development of the real
1.212  numbers.  Base your theory upon theory
1.213 -\isa{Real}, not the usual \isa{Main}.  Launch Isabelle using the command
1.214 +\isa{Real}, not the usual \isa{Main}.%
1.215 +\index{real numbers|)}\index{*real (type)|)}
1.216 +Launch Isabelle using the command
1.217  \begin{verbatim}
1.218  Isabelle -l HOL-Real
1.219  \end{verbatim}
1.220  \end{warn}
1.221
1.222  Also distributed with Isabelle is HOL-Hyperreal,
1.223 -whose theory \isa{Hyperreal} defines the type \isa{hypreal} of non-standard
1.224 -reals.  These
1.225 +whose theory \isa{Hyperreal} defines the type \tydx{hypreal} of
1.226 +\rmindex{non-standard reals}.  These
1.227  \textbf{hyperreals} include infinitesimals, which represent infinitely
1.228  small and infinitely large quantities; they facilitate proofs
1.229  about limits, differentiation and integration~\cite{fleuriot-jcm}.  The