summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

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