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

doc-src/TutorialI/Types/numerics.tex

changeset 11174 | 96a533d300a6 |

parent 11161 | 166f7d87b37f |

child 11216 | 279004936bb0 |

1.1 --- a/doc-src/TutorialI/Types/numerics.tex Wed Feb 21 12:57:55 2001 +0100 1.2 +++ b/doc-src/TutorialI/Types/numerics.tex Wed Feb 21 15:21:15 2001 +0100 1.3 @@ -1,22 +1,20 @@ 1.4 % $Id$ 1.5 -Until now, our numerical have used the type of \textbf{natural numbers}, 1.6 +Until now, our numerical examples have used the type of \textbf{natural 1.7 +numbers}, 1.8 \isa{nat}. This is a recursive datatype generated by the constructors 1.9 zero and successor, so it works well with inductive proofs and primitive 1.10 -recursive function definitions. Isabelle/HOL also provides the type 1.11 +recursive function definitions. HOL also provides the type 1.12 \isa{int} of \textbf{integers}, which lack induction but support true 1.13 -subtraction. The logic HOL-Real also has the type \isa{real} of real 1.14 -numbers. Isabelle has no subtyping, so the numeric types are distinct and 1.15 -there are functions to convert between them. Fortunately most numeric 1.16 -operations are overloaded: the same symbol can be used at all numeric types. 1.17 -Table~\ref{tab:overloading} in the appendix shows the most important operations, 1.18 -together with the priorities of the infix symbols. 1.19 +subtraction. The integers are preferable to the natural numbers for reasoning about 1.20 +complicated arithmetic expressions, even for some expressions whose 1.21 +value is non-negative. The logic HOL-Real also has the type 1.22 +\isa{real} of real numbers. Isabelle has no subtyping, so the numeric 1.23 +types are distinct and there are functions to convert between them. 1.24 +Fortunately most numeric operations are overloaded: the same symbol can be 1.25 +used at all numeric types. Table~\ref{tab:overloading} in the appendix 1.26 +shows the most important operations, together with the priorities of the 1.27 +infix symbols. 1.28 1.29 -The integers are preferable to the natural numbers for reasoning about 1.30 -complicated arithmetic expressions. For example, a termination proof 1.31 -typically involves an integer metric that is shown to decrease at each 1.32 -loop iteration. Even if the metric cannot become negative, proofs 1.33 -may be easier if you use the integers instead of the natural 1.34 -numbers. 1.35 1.36 Many theorems involving numeric types can be proved automatically by 1.37 Isabelle's arithmetic decision procedure, the method 1.38 @@ -181,8 +179,7 @@ 1.39 \rulename{DIVISION_BY_ZERO_MOD} 1.40 \end{isabelle} 1.41 As a concession to convention, these equations are not installed as default 1.42 -simplification rules but are merely used to remove nonzero-divisor 1.43 -hypotheses by case analysis. In \isa{div_mult_mult1} above, one of 1.44 +simplification rules. In \isa{div_mult_mult1} above, one of 1.45 the two divisors (namely~\isa{c}) must still be nonzero. 1.46 1.47 The \textbf{divides} relation has the standard definition, which 1.48 @@ -277,7 +274,7 @@ 1.49 The \isa{arith} method can prove facts about \isa{abs} automatically, 1.50 though as it does so by case analysis, the cost can be exponential. 1.51 \begin{isabelle} 1.52 -\isacommand{lemma}\ "\isasymlbrakk abs\ x\ <\ a;\ abs\ y\ <\ b\isasymrbrakk \ \isasymLongrightarrow \ abs\ x\ +\ abs\ y\ <\ (a\ +\ b\ ::\ int)"\isanewline 1.53 +\isacommand{lemma}\ "abs\ (x+y)\ \isasymle \ abs\ x\ +\ abs\ (y\ ::\ int)"\isanewline 1.54 \isacommand{by}\ arith 1.55 \end{isabelle} 1.56 1.57 @@ -360,11 +357,11 @@ 1.58 are installed as default simplification rules in order to express 1.59 combinations of products and quotients as rational expressions: 1.60 \begin{isabelle} 1.61 -x\ *\ (y\ /\ z)\ =\ x\ *\ y\ /\ z% 1.62 +x\ *\ (y\ /\ z)\ =\ x\ *\ y\ /\ z 1.63 \rulename{real_times_divide1_eq}\isanewline 1.64 -y\ /\ z\ *\ x\ =\ y\ *\ x\ /\ z% 1.65 +y\ /\ z\ *\ x\ =\ y\ *\ x\ /\ z 1.66 \rulename{real_times_divide2_eq}\isanewline 1.67 -x\ /\ (y\ /\ z)\ =\ x\ *\ z\ /\ y% 1.68 +x\ /\ (y\ /\ z)\ =\ x\ *\ z\ /\ y 1.69 \rulename{real_divide_divide1_eq}\isanewline 1.70 x\ /\ y\ /\ z\ =\ x\ /\ (y\ *\ z) 1.71 \rulename{real_divide_divide2_eq} 1.72 @@ -399,10 +396,27 @@ 1.73 \rulename{realpow_abs} 1.74 \end{isabelle} 1.75 1.76 +Numeric literals for type \isa{real} have the same syntax as those for type 1.77 +\isa{int} and only express integral values. Fractions expressed 1.78 +using the division operator are automatically simplified to lowest terms: 1.79 +\begin{isabelle} 1.80 +\ 1.\ P\ ((\#3\ /\ \#4)\ *\ (\#8\ /\ \#15))\isanewline 1.81 +\isacommand{apply} simp\isanewline 1.82 +\ 1.\ P\ (\#2\ /\ \#5) 1.83 +\end{isabelle} 1.84 +Exponentiation can express floating-point values such as 1.85 +\isa{\#2 * \#10\isacharcircum\#6}, but at present no special simplification 1.86 +is performed. 1.87 + 1.88 + 1.89 \begin{warn} 1.90 Type \isa{real} is only available in the logic HOL-Real, which 1.91 is HOL extended with the rather substantial development of the real 1.92 -numbers. Base your theory upon theory \isa{Real}, not the usual \isa{Main}. 1.93 +numbers. Base your theory upon theory 1.94 +\isa{Real}, not the usual \isa{Main}. Launch Isabelle using the command 1.95 +\begin{verbatim} 1.96 +Isabelle -l HOL-Real 1.97 +\end{verbatim} 1.98 \end{warn} 1.99 1.100 Also distributed with Isabelle is HOL-Hyperreal,