# HG changeset patch # User paulson # Date 978715953 -3600 # Node ID 65d18005d8020796c968e20427758deae900bebe # Parent 4d6cf7702e3c391be765a601a2e641f1a79517d2 revisions especially concerning the reals diff -r 4d6cf7702e3c -r 65d18005d802 doc-src/TutorialI/Types/numerics.tex --- a/doc-src/TutorialI/Types/numerics.tex Fri Jan 05 18:31:48 2001 +0100 +++ b/doc-src/TutorialI/Types/numerics.tex Fri Jan 05 18:32:33 2001 +0100 @@ -1,17 +1,18 @@ -Our examples until now have used the type of \textbf{natural numbers}, +% $Id$ +Until now, our numerical 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. The logic HOL-Real also has the type \isa{real} of real +recursive function definitions. Isabelle/HOL also provides the type +\isa{int} of \textbf{integers}, which lack induction but support true +subtraction. The logic HOL-Real\REMARK{now part of HOL?} 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 typically involves an integer metric that is shown to decrease at each -loop iteration. Even if the metric cannot become negative, proofs about it -are usually easier if the integers are used rather than the natural +loop iteration. Even if the metric cannot become negative, proofs +may be easier if you use the integers instead of the natural numbers. Many theorems involving numeric types can be proved automatically by @@ -26,8 +27,9 @@ ways, such as dividing through by common factors. For problems that lie outside the scope of automation, the library has hundreds of theorems about multiplication, division, etc., that can be brought to -bear. You can find find them by browsing the library. Some -useful lemmas are shown below. +bear. You can find find them by browsing the library or by using the Find +button in Proof General. A few lemmas are given below to show what +is available. \subsection{Numeric Literals} \label{sec:numerals} @@ -41,16 +43,19 @@ Literals look like constants, but they abbreviate terms, representing the number in a two's complement binary notation. -Isabelle performs arithmetic on literals by rewriting, rather +Isabelle performs arithmetic on literals by rewriting rather than using the hardware arithmetic. In most cases arithmetic is fast enough, even for large numbers. The arithmetic operations -provided for literals are addition, subtraction, multiplication, -integer division and remainder. +provided for literals include addition, subtraction, multiplication, +integer division and remainder. Fractions of literals (expressed using +division) are reduced to lowest terms. -\emph{Beware}: the arithmetic operators are +\begin{warn} +The arithmetic operators are overloaded, so you must be careful to ensure that each numeric expression refers to a specific type, if necessary by inserting type constraints. Here is an example of what can go wrong: +\par \begin{isabelle} \isacommand{lemma}\ "\#2\ *\ m\ =\ m\ +\ m" \end{isabelle} @@ -62,12 +67,14 @@ The type \isa{'a} given for the literal \isa{\#2} warns us that no numeric type has been specified. The problem is underspecified. Given a type constraint such as \isa{nat}, \isa{int} or \isa{real}, it becomes trivial. +\end{warn} + \subsection{The type of natural numbers, {\tt\slshape nat}} This type requires no introduction: we have been using it from the -start. Hundreds of useful lemmas about arithmetic on type \isa{nat} are +beginning. Hundreds of theorems about the natural numbers are proved in the theories \isa{Nat}, \isa{NatArith} and \isa{Divides}. Only in exceptional circumstances should you resort to induction. @@ -77,12 +84,12 @@ in a variety of additive types. The symbols \isa{1} and \isa{2} are not constants but abbreviations for \isa{Suc 0} and \isa{Suc(Suc 0)}, respectively. The literals \isa{\#0}, \isa{\#1} and \isa{\#2} are -entirely different from \isa{0}, \isa{1} and \isa{2}. You will +syntactically different from \isa{0}, \isa{1} and \isa{2}. You will sometimes prefer one notation to the other. Literals are obviously -necessary to express large values, while \isa{0} and \isa{Suc} are -needed in order to match many theorems, including the rewrite rules for -primitive recursive functions. The following default simplification rules -replace small literals by zero and successor: +necessary to express large values, while \isa{0} and \isa{Suc} are needed +in order to match many theorems, including the rewrite rules for primitive +recursive functions. The following default simplification rules replace +small literals by zero and successor: \begin{isabelle} \#0\ =\ 0 \rulename{numeral_0_eq_0}\isanewline @@ -146,7 +153,8 @@ \end{isabelle} Surprisingly few of these results depend upon the -divisors' being nonzero. Isabelle/HOL defines division by zero: +divisors' being nonzero. That is because division by +zero yields zero: \begin{isabelle} a\ div\ 0\ =\ 0 \rulename{DIVISION_BY_ZERO_DIV}\isanewline @@ -178,8 +186,8 @@ The rule \isa{diff_mult_distrib} shown above is one of the few facts about \isa{m\ -\ n} that is not subject to the condition \isa{n\ \isasymle \ m}. Natural number subtraction has few -nice properties; often it is best to remove it from a subgoal -using this split rule: +nice properties; often you should remove it by simplifying with this split +rule: \begin{isabelle} P(a-b)\ =\ ((a