summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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