doc-src/TutorialI/Types/numerics.tex
 changeset 13979 4c3a638828b9 parent 13750 b5cd10cb106b child 13983 afc0dadddaa4
     1.1 --- a/doc-src/TutorialI/Types/numerics.tex	Thu May 08 12:51:55 2003 +0200
1.2 +++ b/doc-src/TutorialI/Types/numerics.tex	Thu May 08 12:52:15 2003 +0200
1.3 @@ -12,9 +12,10 @@
1.4  \isa{int} of \textbf{integers}, which lack induction but support true
1.5  subtraction.  The integers are preferable to the natural numbers for reasoning about
1.6  complicated arithmetic expressions, even for some expressions whose
1.7 -value is non-negative.  The logic HOL-Real also has the type
1.8 -\isa{real} of real numbers.  Isabelle has no subtyping,  so the numeric
1.9 -types are distinct and there are  functions to convert between them.
1.10 +value is non-negative.  The logic HOL-Complex also has the types
1.11 +\isa{real} and \isa{complex}: the real and complex numbers.  Isabelle has no
1.12 +subtyping,  so the numeric
1.13 +types are distinct and there are functions to convert between them.
1.14  Fortunately most numeric operations are overloaded: the same symbol can be
1.15  used at all numeric types. Table~\ref{tab:overloading} in the appendix
1.16  shows the most important operations, together with the priorities of the
1.17 @@ -363,7 +364,7 @@
1.18  \isa{zdiv_zmult2_eq} is $-2$ while the right-hand side is~$-1$.%
1.19  \index{integers|)}\index{*int (type)|)}
1.20
1.21 -Induction is less important for integers than it is for the natural numbers, but it can be valuable if the range of integers has a lower or upper bound.  There are four rules for integer induction, corresponding to the possible relations of the bound ($\ge$, $>$, $\le$ and $<$):
1.22 +Induction is less important for integers than it is for the natural numbers, but it can be valuable if the range of integers has a lower or upper bound.  There are four rules for integer induction, corresponding to the possible relations of the bound ($\geq$, $>$, $\leq$ and $<$):
1.23  \begin{isabelle}
1.24  \isasymlbrakk k\ \isasymle \ i;\ P\ k;\ \isasymAnd i.\ \isasymlbrakk k\ \isasymle \ i;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i+1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%
1.25  \rulename{int_ge_induct}\isanewline