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,