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
 
-real_add_divide_distrib
+@{thm[display] real_add_divide_distrib[no_vars]}
+\rulename{real_add_divide_distrib}
 *}
 
 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}
 reduces \isa{n\ {\isasymle}\ {\isadigit{2}}} to the three cases \isa{n\ {\isasymle}\ {\isadigit{0}}}, \isa{n\ {\isacharequal}\ {\isadigit{1}}} and
 \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%
+\rulename{real_add_divide_distrib}
+\end{isabelle}
+
 As with the other numeric types, the simplifier can sort the operands of
 addition and multiplication.  The name \isa{real_add_ac} refers to the
-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$.