author paulson Thu, 04 Jan 2001 10:22:33 +0100 changeset 10777 a5a6255748c3 parent 10776 985066e9495d child 10778 2c6605049646
initial material on the Reals
--- a/doc-src/TutorialI/Types/Numbers.thy	Wed Jan 03 21:27:15 2001 +0100
+++ b/doc-src/TutorialI/Types/Numbers.thy	Thu Jan 04 10:22:33 2001 +0100
@@ -2,7 +2,7 @@
theory Numbers = Real:

ML "Pretty.setmargin 64"
-
+ML "IsarOutput.indent := 0"  (*we don't want 5 for listing theorems*)

text{*

@@ -198,7 +198,8 @@

This last NOT a simprule

*}

end
--- a/doc-src/TutorialI/Types/document/Typedef.tex	Wed Jan 03 21:27:15 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Typedef.tex	Thu Jan 04 10:22:33 2001 +0100
@@ -104,7 +104,7 @@
\end{center}
Constant \isa{three} is just an abbreviation (\isa{three{\isacharunderscore}def}):
\begin{isabelle}%
-\ \ \ \ \ three\ {\isasymequiv}\ {\isacharbraceleft}n{\isachardot}\ n\ {\isasymle}\ {\isadigit{2}}{\isacharbraceright}%
+three\ {\isasymequiv}\ {\isacharbraceleft}n{\isachardot}\ n\ {\isasymle}\ {\isadigit{2}}{\isacharbraceright}%
\end{isabelle}
The situation is best summarized with the help of the following diagram,
where squares are types and circles are sets:
@@ -204,7 +204,7 @@
Expanding \isa{three{\isacharunderscore}def} yields the premise \isa{n\ {\isasymle}\ {\isadigit{2}}}. Repeated
elimination with \isa{le{\isacharunderscore}SucE}
\begin{isabelle}%
-\ \ \ \ \ {\isasymlbrakk}{\isacharquery}m\ {\isasymle}\ Suc\ {\isacharquery}n{\isacharsemicolon}\ {\isacharquery}m\ {\isasymle}\ {\isacharquery}n\ {\isasymLongrightarrow}\ {\isacharquery}R{\isacharsemicolon}\ {\isacharquery}m\ {\isacharequal}\ Suc\ {\isacharquery}n\ {\isasymLongrightarrow}\ {\isacharquery}R{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}R%
+{\isasymlbrakk}{\isacharquery}m\ {\isasymle}\ Suc\ {\isacharquery}n{\isacharsemicolon}\ {\isacharquery}m\ {\isasymle}\ {\isacharquery}n\ {\isasymLongrightarrow}\ {\isacharquery}R{\isacharsemicolon}\ {\isacharquery}m\ {\isacharequal}\ Suc\ {\isacharquery}n\ {\isasymLongrightarrow}\ {\isacharquery}R{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}R%
\end{isabelle}
\isa{n\ {\isacharequal}\ {\isadigit{2}}} which are trivial for simplification:%
--- a/doc-src/TutorialI/Types/numerics.tex	Wed Jan 03 21:27:15 2001 +0100
+++ b/doc-src/TutorialI/Types/numerics.tex	Thu Jan 04 10:22:33 2001 +0100
@@ -1,8 +1,11 @@
Our examples until now 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 has the type \isa{int}
-of \textbf{integers}, which gives up induction in exchange  for proper subtraction.
+recursive function definitions. Isabelle/HOL also has the type \isa{int} of
+\textbf{integers}, which gives up induction in exchange  for proper
+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.

The integers are preferable to the natural  numbers for reasoning about
complicated arithmetic expressions. For  example, a termination proof
@@ -11,14 +14,6 @@
are usually easier  if the integers are used rather than the natural
numbers.

-The logic Isabelle/HOL-Real also has the type \isa{real} of real numbers
-and even the type \isa{hypreal} of non-standard reals. These
-\textbf{hyperreals} include  infinitesimals, which represent infinitely
-small and infinitely  large quantities; they greatly facilitate proofs
-about limits,  differentiation and integration.  Isabelle has no subtyping,
-so the numeric types are distinct and there are
-functions to convert between them.
-
Many theorems involving numeric types can be proved automatically by
Isabelle's arithmetic decision procedure, the method
\isa{arith}.  Linear arithmetic comprises addition, subtraction
@@ -35,11 +30,9 @@
useful lemmas are shown below.

\subsection{Numeric Literals}
-\label{sec:numerals}

Literals are available for the types of natural numbers, integers
and reals and denote integer values of arbitrary size.
-\REMARK{hypreal?}
They begin
with a number sign (\isa{\#}), have an optional minus sign (\isa{-}) and
then one or more decimal digits. Examples are \isa{\#0}, \isa{\#-3}
@@ -243,7 +236,7 @@
operators.  The name \isa{zadd_ac} refers to the associativity and
commutativity theorems for integer addition, while \isa{zmult_ac} has the
analogous theorems for multiplication.  The prefix~\isa{z} in many theorem
-names recalls the use of $Z$ to denote the set of integers.
+names recalls the use of $\Bbb{Z}$ to denote the set of integers.

For division and remainder, the treatment of negative divisors follows
traditional mathematical practice: the sign of the remainder follows that
@@ -304,9 +297,79 @@

\subsection{The type of real numbers, {\tt\slshape real}}

+The real numbers enjoy two significant properties that the integers lack.
+They are
+\textbf{dense}: between every two distinct real numbers there lies another.
+This property follows from the division laws, since if $x<y$ then between
+them lies $(x+y)/2$.  The second property is that they are
+\textbf{complete}: every set of reals that is bounded above has a least
+upper bound.  Completeness distinguishes the reals from the rationals, for
+which the set $\{x\mid x^2<2\}$ has no least upper bound.  (It could only be
+$\surd2$, which is irrational.)
+
+The formalization of completeness is long and technical.  Rather than
+reproducing it here, we refer you to the theory \texttt{RComplete} in
+directory \texttt{Real}.
+
+Density is trivial to express:
+\begin{isabelle}
+x\ <\ y\ \isasymLongrightarrow \ \isasymexists r.\ x\ <\ r\ \isasymand \ r\ <\ y%
+\rulename{real_dense}
+\end{isabelle}
+
+Here is a selection of rules about the division operator.  The following
+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%
+\rulename{real_times_divide1_eq}\isanewline
+y\ /\ z\ *\ x\ =\ y\ *\ x\ /\ z%
+\rulename{real_times_divide2_eq}\isanewline
+x\ /\ (y\ /\ z)\ =\ x\ *\ z\ /\ y%
+\rulename{real_divide_divide1_eq}\isanewline
+x\ /\ y\ /\ z\ =\ x\ /\ (y\ *\ z)
+\rulename{real_divide_divide2_eq}
+\end{isabelle}
+
+Signs are extracted from quotients in the hope that complementary terms can
+then be cancelled:
+\begin{isabelle}
+-\ x\ /\ y\ =\ -\ (x\ /\ y)
+\rulename{real_minus_divide_eq}\isanewline
+x\ /\ -\ y\ =\ -\ (x\ /\ y)
+\rulename{real_divide_minus_eq}
+\end{isabelle}
+
+The following distributive law is available, but it is not installed as a
+simplification rule.
+\begin{isabelle}
+(x\ +\ y)\ /\ z\ =\ x\ /\ z\ +\ y\ /\ z%
+\end{isabelle}
+
As with the other numeric types, the simplifier can sort the operands of
-associativity and commutativity theorems for addition; similarly
+associativity and commutativity theorems for addition, while similarly
\isa{real_mult_ac} contains those properties for multiplication.

-\textbf{To be written.  Inverse, abs, theorems about density, etc.?}
+The absolute value function \isa{abs} is
+defined for the reals, along with many theorems such as this one about
+exponentiation:
+\begin{isabelle}
+\isasymbar r\isasymbar \ \isacharcircum \ n\ =\ \isasymbar r\ \isacharcircum \ n\isasymbar
+\rulename{realpow_abs}
+\end{isabelle}
+
+\emph{Note}: 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}.
+
+Also distributed with Isabelle is HOL-Hyperreal,
+whose theory \isa{Hyperreal} defines the type \isa{hypreal} of non-standard
+reals.  These
+\textbf{hyperreals} include infinitesimals, which represent infinitely
+small and infinitely large quantities; they facilitate proofs
+about limits, differentiation and integration.  The development defines an
+infinitely large number, \isa{omega} and an infinitely small positive
+number, \isa{epsilon}.  Also available is the approximates relation,
+written $\approx$.