indexing
authorpaulson
Fri Jul 13 17:55:35 2001 +0200 (2001-07-13)
changeset 1141691886738773a
parent 11415 34a76158cbb8
child 11417 499435b4084e
indexing
doc-src/TutorialI/Types/numerics.tex
     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.29 +\begin{warn}\index{overloading!and arithmetic}
    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.78 -\rulename{add_mult_distrib}\isanewline
    1.79 +\rulenamedx{add_mult_distrib}\isanewline
    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.134 -\rulename{dvd_add}
   1.135 +\rulenamedx{dvd_add}
   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.143 -\rulename{add_assoc}\isanewline
   1.144 +\rulenamedx{add_assoc}\isanewline
   1.145  m\ +\ n\ =\ n\ +\ m%
   1.146 -\rulename{add_commute}\isanewline
   1.147 +\rulenamedx{add_commute}\isanewline
   1.148  x\ +\ (y\ +\ z)\ =\ y\ +\ (x\
   1.149  +\ z)
   1.150  \rulename{add_left_commute}
   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