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