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.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.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,