--- a/doc-src/TutorialI/Types/numerics.tex Wed Feb 21 12:57:55 2001 +0100
+++ b/doc-src/TutorialI/Types/numerics.tex Wed Feb 21 15:21:15 2001 +0100
@@ -1,22 +1,20 @@
% $Id$
-Until now, our numerical have used the type of \textbf{natural numbers},
+Until now, our numerical examples have used the type of \textbf{natural
+numbers},
\isa{nat}. This is a recursive datatype generated by the constructors
zero and successor, so it works well with inductive proofs and primitive
-recursive function definitions. Isabelle/HOL also provides the type
+recursive function definitions. HOL also provides the type
\isa{int} of \textbf{integers}, which lack induction but support true
-subtraction. The logic HOL-Real also has the type \isa{real} of real
-numbers. Isabelle has no subtyping, so the numeric types are distinct and
-there are functions to convert between them. Fortunately most numeric
-operations are overloaded: the same symbol can be used at all numeric types.
-Table~\ref{tab:overloading} in the appendix shows the most important operations,
-together with the priorities of the infix symbols.
+subtraction. The integers are preferable to the natural numbers for reasoning about
+complicated arithmetic expressions, even for some expressions whose
+value is non-negative. The logic HOL-Real also has the type
+\isa{real} of real numbers. Isabelle has no subtyping, so the numeric
+types are distinct and there are functions to convert between them.
+Fortunately most numeric operations are overloaded: the same symbol can be
+used at all numeric types. Table~\ref{tab:overloading} in the appendix
+shows the most important operations, together with the priorities of the
+infix symbols.
-The integers are preferable to the natural numbers for reasoning about
-complicated arithmetic expressions. For example, a termination proof
-typically involves an integer metric that is shown to decrease at each
-loop iteration. Even if the metric cannot become negative, proofs
-may be easier if you use the integers instead of the natural
-numbers.
Many theorems involving numeric types can be proved automatically by
Isabelle's arithmetic decision procedure, the method
@@ -181,8 +179,7 @@
\rulename{DIVISION_BY_ZERO_MOD}
\end{isabelle}
As a concession to convention, these equations are not installed as default
-simplification rules but are merely used to remove nonzero-divisor
-hypotheses by case analysis. In \isa{div_mult_mult1} above, one of
+simplification rules. In \isa{div_mult_mult1} above, one of
the two divisors (namely~\isa{c}) must still be nonzero.
The \textbf{divides} relation has the standard definition, which
@@ -277,7 +274,7 @@
The \isa{arith} method can prove facts about \isa{abs} automatically,
though as it does so by case analysis, the cost can be exponential.
\begin{isabelle}
-\isacommand{lemma}\ "\isasymlbrakk abs\ x\ <\ a;\ abs\ y\ <\ b\isasymrbrakk \ \isasymLongrightarrow \ abs\ x\ +\ abs\ y\ <\ (a\ +\ b\ ::\ int)"\isanewline
+\isacommand{lemma}\ "abs\ (x+y)\ \isasymle \ abs\ x\ +\ abs\ (y\ ::\ int)"\isanewline
\isacommand{by}\ arith
\end{isabelle}
@@ -360,11 +357,11 @@
are installed as default simplification rules in order to express
combinations of products and quotients as rational expressions:
\begin{isabelle}
-x\ *\ (y\ /\ z)\ =\ x\ *\ y\ /\ z%
+x\ *\ (y\ /\ z)\ =\ x\ *\ y\ /\ z
\rulename{real_times_divide1_eq}\isanewline
-y\ /\ z\ *\ x\ =\ y\ *\ x\ /\ z%
+y\ /\ z\ *\ x\ =\ y\ *\ x\ /\ z
\rulename{real_times_divide2_eq}\isanewline
-x\ /\ (y\ /\ z)\ =\ x\ *\ z\ /\ y%
+x\ /\ (y\ /\ z)\ =\ x\ *\ z\ /\ y
\rulename{real_divide_divide1_eq}\isanewline
x\ /\ y\ /\ z\ =\ x\ /\ (y\ *\ z)
\rulename{real_divide_divide2_eq}
@@ -399,10 +396,27 @@
\rulename{realpow_abs}
\end{isabelle}
+Numeric literals for type \isa{real} have the same syntax as those for type
+\isa{int} and only express integral values. Fractions expressed
+using the division operator are automatically simplified to lowest terms:
+\begin{isabelle}
+\ 1.\ P\ ((\#3\ /\ \#4)\ *\ (\#8\ /\ \#15))\isanewline
+\isacommand{apply} simp\isanewline
+\ 1.\ P\ (\#2\ /\ \#5)
+\end{isabelle}
+Exponentiation can express floating-point values such as
+\isa{\#2 * \#10\isacharcircum\#6}, but at present no special simplification
+is performed.
+
+
\begin{warn}
Type \isa{real} is only available in the logic HOL-Real, which
is HOL extended with the rather substantial development of the real
-numbers. Base your theory upon theory \isa{Real}, not the usual \isa{Main}.
+numbers. Base your theory upon theory
+\isa{Real}, not the usual \isa{Main}. Launch Isabelle using the command
+\begin{verbatim}
+Isabelle -l HOL-Real
+\end{verbatim}
\end{warn}
Also distributed with Isabelle is HOL-Hyperreal,