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

author | paulson |

Fri, 12 Jan 2001 16:11:55 +0100 | |

changeset 10881 | 03f06372230b |

parent 10880 | 729a36e469ec |

child 10882 | ca41ba5fb8e2 |

abs and other small changes

--- a/doc-src/TutorialI/Types/numerics.tex Fri Jan 12 16:10:56 2001 +0100 +++ b/doc-src/TutorialI/Types/numerics.tex Fri Jan 12 16:11:55 2001 +0100 @@ -4,7 +4,7 @@ zero and successor, so it works well with inductive proofs and primitive 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 +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. @@ -25,10 +25,10 @@ The simplifier reduces arithmetic expressions in other ways, such as dividing through by common factors. For problems that lie -outside the scope of automation, the library has hundreds of +outside the scope of automation, HOL provides hundreds of theorems about multiplication, division, etc., that can be brought to -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 +bear. You can locate them using Proof General's Find +button. A few lemmas are given below to show what is available. \subsection{Numeric Literals} @@ -69,6 +69,21 @@ constraint such as \isa{nat}, \isa{int} or \isa{real}, it becomes trivial. \end{warn} +\begin{warn} +Numeric literals are not constructors and therefore must not be used in +patterns. For example, this declaration is rejected: +\begin{isabelle} +\isacommand{recdef}\ h\ "\isacharbraceleft \isacharbraceright "\isanewline +h\ \#3\ =\ \#2\isanewline +h\ i\ \ =\ i +\end{isabelle} + +You should use a conditional expression instead: +\begin{isabelle} +"h\ i\ =\ (if\ i\ =\ \#3\ then\ \#2\ else\ i)" +\end{isabelle} +\end{warn} + \subsection{The type of natural numbers, {\tt\slshape nat}} @@ -128,8 +143,9 @@ \end{isabelle} \subsubsection{Division} -The library contains the basic facts about quotient and remainder -(including the analogous equation, \isa{div_if}): +The infix operators \isa{div} and \isa{mod} are overloaded. +Isabelle/HOL provides the basic facts about quotient and remainder +on the natural numbers: \begin{isabelle} m\ mod\ n\ =\ (if\ m\ <\ n\ then\ m\ else\ (m\ -\ n)\ mod\ n) \rulename{mod_if}\isanewline @@ -238,7 +254,7 @@ \subsection{The type of integers, {\tt\slshape int}} Reasoning methods resemble those for the natural numbers, but induction and -the constant \isa{Suc} are not available. The library provides many lemmas +the constant \isa{Suc} are not available. HOL provides many lemmas for proving inequalities involving integer multiplication and division, similar to those shown above for type~\isa{nat}. @@ -255,6 +271,12 @@ get \isa{\isasymbar x\isasymbar}. \end{warn} +The \isa{arith} method can prove facts about \isa{abs} automatically, +though as it does so by case analysis, the cost can be exponential. +\begin{isabelle} +\isacommand{lemma}\ "\isasymlbrakk abs\ x\ <\ a;\ abs\ y\ <\ b\isasymrbrakk \ \isasymLongrightarrow \ abs\ x\ +\ abs\ y\ <\ (a\ +\ b\ ::\ int)"\isanewline +\isacommand{by}\ arith +\end{isabelle} Concerning simplifier tricks, we have no need to eliminate subtraction: it is well-behaved. As with the natural numbers, the simplifier can sort the @@ -308,7 +330,7 @@ \isa{c} to be zero. However, \isa{c} cannot be negative: a counterexample is $\isa{a} = 7$, $\isa{b} = 2$ and $\isa{c} = -3$, when the left-hand side of -\isa{zdiv_zmult2_eq} is $-2$ while the right-hand side is $-1$. +\isa{zdiv_zmult2_eq} is $-2$ while the right-hand side is~$-1$. \subsection{The type of real numbers, {\tt\slshape real}} @@ -374,9 +396,11 @@ \rulename{realpow_abs} \end{isabelle} -\emph{Note}: Type \isa{real} is only available in the logic HOL-Real\REMARK{now part of HOL?}, which +\begin{warn} +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}. +\end{warn} Also distributed with Isabelle is HOL-Hyperreal, whose theory \isa{Hyperreal} defines the type \isa{hypreal} of non-standard @@ -385,5 +409,5 @@ small and infinitely large quantities; they facilitate proofs about limits, differentiation and integration~\cite{fleuriot-jcm}. 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$. +infinitely small positive number, \isa{epsilon}. The +relation $x\approx y$ means ``$x$ is infinitely close to~$y$''.