# HG changeset patch # User paulson # Date 1077209874 -3600 # Node ID 6069098854b9e869ee4307d744d401797549085d # Parent dc677b35e54fc3dc6d5ead4da0be7c495fbd7848 new numerics section using type classes diff -r dc677b35e54f -r 6069098854b9 doc-src/TutorialI/Types/Numbers.thy --- a/doc-src/TutorialI/Types/Numbers.thy Thu Feb 19 16:44:21 2004 +0100 +++ b/doc-src/TutorialI/Types/Numbers.thy Thu Feb 19 17:57:54 2004 +0100 @@ -60,18 +60,10 @@ oops text{* -@{thm[display] mult_le_mono[no_vars]} -\rulename{mult_le_mono} - -@{thm[display] mult_less_mono1[no_vars]} -\rulename{mult_less_mono1} @{thm[display] div_le_mono[no_vars]} \rulename{div_le_mono} -@{thm[display] add_mult_distrib[no_vars]} -\rulename{add_mult_distrib} - @{thm[display] diff_mult_distrib[no_vars]} \rulename{diff_mult_distrib} @@ -168,9 +160,6 @@ @{thm[display] zmod_zmult2_eq[no_vars]} \rulename{zmod_zmult2_eq} - -@{thm[display] abs_mult[no_vars]} -\rulename{abs_mult} *} lemma "abs (x+y) \ abs x + abs (y :: int)" @@ -195,14 +184,11 @@ \rulename{int_less_induct} *} -text {*REALS +text {*FIELDS @{thm[display] dense[no_vars]} \rulename{dense} -@{thm[display] power_abs[no_vars]} -\rulename{power_abs} - @{thm[display] times_divide_eq_right[no_vars]} \rulename{times_divide_eq_right} @@ -254,6 +240,59 @@ apply simp oops +text{* +Ring and Field + +Requires a field, or else an ordered ring + +@{thm[display] mult_eq_0_iff[no_vars]} +\rulename{mult_eq_0_iff} + +@{thm[display] field_mult_eq_0_iff[no_vars]} +\rulename{field_mult_eq_0_iff} + +@{thm[display] mult_cancel_right[no_vars]} +\rulename{mult_cancel_right} + +@{thm[display] field_mult_cancel_right[no_vars]} +\rulename{field_mult_cancel_right} +*} + +ML{*set show_sorts*} + +text{* +effect of show sorts on the above + +@{thm[display] field_mult_cancel_right[no_vars]} +\rulename{field_mult_cancel_right} +*} + +ML{*reset show_sorts*} + + +text{* +absolute value + +@{thm[display] abs_mult[no_vars]} +\rulename{abs_mult} + +@{thm[display] abs_le_iff[no_vars]} +\rulename{abs_le_iff} + +@{thm[display] abs_triangle_ineq[no_vars]} +\rulename{abs_triangle_ineq} + +@{thm[display] power_add[no_vars]} +\rulename{power_add} + +@{thm[display] power_mult[no_vars]} +\rulename{power_mult} + +@{thm[display] power_abs[no_vars]} +\rulename{power_abs} + + +*} end diff -r dc677b35e54f -r 6069098854b9 doc-src/TutorialI/Types/document/Numbers.tex --- a/doc-src/TutorialI/Types/document/Numbers.tex Thu Feb 19 16:44:21 2004 +0100 +++ b/doc-src/TutorialI/Types/document/Numbers.tex Thu Feb 19 17:57:54 2004 +0100 @@ -95,26 +95,11 @@ % \begin{isamarkuptext}% \begin{isabelle}% -{\isasymlbrakk}i\ {\isasymle}\ j{\isacharsemicolon}\ k\ {\isasymle}\ l{\isasymrbrakk}\ {\isasymLongrightarrow}\ i\ {\isacharasterisk}\ k\ {\isasymle}\ j\ {\isacharasterisk}\ l% -\end{isabelle} -\rulename{mult_le_mono} - -\begin{isabelle}% -{\isasymlbrakk}i\ {\isacharless}\ j{\isacharsemicolon}\ {\isadigit{0}}\ {\isacharless}\ k{\isasymrbrakk}\ {\isasymLongrightarrow}\ i\ {\isacharasterisk}\ k\ {\isacharless}\ j\ {\isacharasterisk}\ k% -\end{isabelle} -\rulename{mult_less_mono1} - -\begin{isabelle}% m\ {\isasymle}\ n\ {\isasymLongrightarrow}\ m\ div\ k\ {\isasymle}\ n\ div\ k% \end{isabelle} \rulename{div_le_mono} \begin{isabelle}% -{\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}\ {\isacharasterisk}\ k\ {\isacharequal}\ m\ {\isacharasterisk}\ k\ {\isacharplus}\ n\ {\isacharasterisk}\ k% -\end{isabelle} -\rulename{add_mult_distrib} - -\begin{isabelle}% {\isacharparenleft}m\ {\isacharminus}\ n{\isacharparenright}\ {\isacharasterisk}\ k\ {\isacharequal}\ m\ {\isacharasterisk}\ k\ {\isacharminus}\ n\ {\isacharasterisk}\ k% \end{isabelle} \rulename{diff_mult_distrib} @@ -274,12 +259,7 @@ \begin{isabelle}% {\isadigit{0}}\ {\isacharless}\ c\ {\isasymLongrightarrow}\ a\ mod\ {\isacharparenleft}b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ b\ {\isacharasterisk}\ {\isacharparenleft}a\ div\ b\ mod\ c{\isacharparenright}\ {\isacharplus}\ a\ mod\ b% \end{isabelle} -\rulename{zmod_zmult2_eq} - -\begin{isabelle}% -{\isasymbar}a\ {\isacharasterisk}\ b{\isasymbar}\ {\isacharequal}\ {\isasymbar}a{\isasymbar}\ {\isacharasterisk}\ {\isasymbar}b{\isasymbar}% -\end{isabelle} -\rulename{abs_mult}% +\rulename{zmod_zmult2_eq}% \end{isamarkuptext}% \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}abs\ {\isacharparenleft}x{\isacharplus}y{\isacharparenright}\ {\isasymle}\ abs\ x\ {\isacharplus}\ abs\ {\isacharparenleft}y\ {\isacharcolon}{\isacharcolon}\ int{\isacharparenright}{\isachardoublequote}\isanewline @@ -317,7 +297,7 @@ \isamarkuptrue% % \begin{isamarkuptext}% -REALS +FIELDS \begin{isabelle}% a\ {\isacharless}\ b\ {\isasymLongrightarrow}\ {\isasymexists}r{\isachardot}\ a\ {\isacharless}\ r\ {\isasymand}\ r\ {\isacharless}\ b% @@ -325,11 +305,6 @@ \rulename{dense} \begin{isabelle}% -{\isasymbar}a\ {\isacharcircum}\ n{\isasymbar}\ {\isacharequal}\ {\isasymbar}a{\isasymbar}\ {\isacharcircum}\ n% -\end{isabelle} -\rulename{power_abs} - -\begin{isabelle}% a\ {\isacharasterisk}\ {\isacharparenleft}b\ {\isacharslash}\ c{\isacharparenright}\ {\isacharequal}\ a\ {\isacharasterisk}\ b\ {\isacharslash}\ c% \end{isabelle} \rulename{times_divide_eq_right} @@ -414,11 +389,82 @@ \isamarkupfalse% \isacommand{apply}\ simp\ \isanewline \isamarkupfalse% -\isacommand{oops}\isanewline -\isanewline -\isanewline -\isanewline -\isamarkupfalse% +\isacommand{oops}\isamarkupfalse% +% +\begin{isamarkuptext}% +Ring and Field + +Requires a field, or else an ordered ring + +\begin{isabelle}% +{\isacharparenleft}a\ {\isacharasterisk}\ b\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}a\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymor}\ b\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}{\isacharparenright}% +\end{isabelle} +\rulename{mult_eq_0_iff} + +\begin{isabelle}% +{\isacharparenleft}a\ {\isacharasterisk}\ b\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}a\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymor}\ b\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}{\isacharparenright}% +\end{isabelle} +\rulename{field_mult_eq_0_iff} + +\begin{isabelle}% +{\isacharparenleft}a\ {\isacharasterisk}\ c\ {\isacharequal}\ b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}c\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymor}\ a\ {\isacharequal}\ b{\isacharparenright}% +\end{isabelle} +\rulename{mult_cancel_right} + +\begin{isabelle}% +{\isacharparenleft}a\ {\isacharasterisk}\ c\ {\isacharequal}\ b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}c\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymor}\ a\ {\isacharequal}\ b{\isacharparenright}% +\end{isabelle} +\rulename{field_mult_cancel_right}% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{ML}{\isacharbraceleft}{\isacharasterisk}set\ show{\isacharunderscore}sorts{\isacharasterisk}{\isacharbraceright}\isamarkupfalse% +% +\begin{isamarkuptext}% +effect of show sorts on the above + +\begin{isabelle}% +{\isacharparenleft}{\isacharparenleft}a{\isasymColon}{\isacharprime}a{\isasymColon}field{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}c{\isasymColon}{\isacharprime}a{\isasymColon}field{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}b{\isasymColon}{\isacharprime}a{\isasymColon}field{\isacharparenright}\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\isanewline +{\isacharparenleft}c\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isasymColon}field{\isacharparenright}\ {\isasymor}\ a\ {\isacharequal}\ b{\isacharparenright}% +\end{isabelle} +\rulename{field_mult_cancel_right}% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{ML}{\isacharbraceleft}{\isacharasterisk}reset\ show{\isacharunderscore}sorts{\isacharasterisk}{\isacharbraceright}\isamarkupfalse% +% +\begin{isamarkuptext}% +absolute value + +\begin{isabelle}% +{\isasymbar}a\ {\isacharasterisk}\ b{\isasymbar}\ {\isacharequal}\ {\isasymbar}a{\isasymbar}\ {\isacharasterisk}\ {\isasymbar}b{\isasymbar}% +\end{isabelle} +\rulename{abs_mult} + +\begin{isabelle}% +{\isacharparenleft}{\isasymbar}a{\isasymbar}\ {\isasymle}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}a\ {\isasymle}\ b\ {\isasymand}\ {\isacharminus}\ a\ {\isasymle}\ b{\isacharparenright}% +\end{isabelle} +\rulename{abs_le_iff} + +\begin{isabelle}% +{\isasymbar}a\ {\isacharplus}\ b{\isasymbar}\ {\isasymle}\ {\isasymbar}a{\isasymbar}\ {\isacharplus}\ {\isasymbar}b{\isasymbar}% +\end{isabelle} +\rulename{abs_triangle_ineq} + +\begin{isabelle}% +a\ {\isacharcircum}\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}\ {\isacharequal}\ a\ {\isacharcircum}\ m\ {\isacharasterisk}\ a\ {\isacharcircum}\ n% +\end{isabelle} +\rulename{power_add} + +\begin{isabelle}% +a\ {\isacharcircum}\ {\isacharparenleft}m\ {\isacharasterisk}\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}a\ {\isacharcircum}\ m{\isacharparenright}\ {\isacharcircum}\ n% +\end{isabelle} +\rulename{power_mult} + +\begin{isabelle}% +{\isasymbar}a\ {\isacharcircum}\ n{\isasymbar}\ {\isacharequal}\ {\isasymbar}a{\isasymbar}\ {\isacharcircum}\ n% +\end{isabelle} +\rulename{power_abs}% +\end{isamarkuptext}% +\isamarkuptrue% \isacommand{end}\isanewline \isamarkupfalse% \end{isabellebody}% diff -r dc677b35e54f -r 6069098854b9 doc-src/TutorialI/Types/numerics.tex --- a/doc-src/TutorialI/Types/numerics.tex Thu Feb 19 16:44:21 2004 +0100 +++ b/doc-src/TutorialI/Types/numerics.tex Thu Feb 19 17:57:54 2004 +0100 @@ -10,16 +10,19 @@ zero and successor, so it works well with inductive proofs and primitive recursive function definitions. HOL also provides the type \isa{int} of \textbf{integers}, which lack induction but support true -subtraction. The integers are preferable to the natural numbers for reasoning about -complicated arithmetic expressions, even for some expressions whose -value is non-negative. The logic HOL-Complex also has the types -\isa{real} and \isa{complex}: the real and complex numbers. Isabelle has no +subtraction. With subtraction, arithmetic reasoning is easier, which makes +the integers preferable to the natural numbers for +complicated arithmetic expressions, even if they are non-negative. The logic HOL-Complex also has the types +\isa{rat}, \isa{real} and \isa{complex}: the rational, real and complex numbers. Isabelle has no subtyping, so the numeric types are distinct and there are functions to convert between them. -Fortunately most numeric operations are overloaded: the same symbol can be +Most numeric operations are overloaded: the same symbol can be used at all numeric types. Table~\ref{tab:overloading} in the appendix shows the most important operations, together with the priorities of the -infix symbols. +infix symbols. Algebraic properties are organized using type classes +around algebraic concepts such as rings and fields; +a property such as the commutativity of addition is a single theorem +(\isa{add_commute}) that applies to all numeric types. \index{linear arithmetic}% Many theorems involving numeric types can be proved automatically by @@ -29,8 +32,7 @@ are regarded as variables. The procedure can be slow, especially if the subgoal to be proved involves subtraction over type \isa{nat}, which causes case splits. On types \isa{nat} and \isa{int}, \methdx{arith} -can deal with quantifiers (this is known as ``Presburger Arithmetic''), -whereas on type \isa{real} it cannot. +can deal with quantifiers---this is known as Presburger arithmetic---whereas on type \isa{real} it cannot. The simplifier reduces arithmetic expressions in other ways, such as dividing through by common factors. For problems that lie @@ -46,16 +48,13 @@ \index{numeric literals|(}% The constants \cdx{0} and \cdx{1} are overloaded. They denote zero and one, respectively, for all numeric types. Other values are expressed by numeric -literals, which consist of one or more decimal digits optionally preceeded by -a minus sign (\isa{-}). Examples are \isa{2}, \isa{-3} and -\isa{441223334678}. Literals are available for the types of natural numbers, -integers and reals; they denote integer values of arbitrary size. +literals, which consist of one or more decimal digits optionally preceeded by a minus sign (\isa{-}). Examples are \isa{2}, \isa{-3} and \isa{441223334678}. Literals are available for the types of natural numbers, integers, rationals, reals, etc.; they denote integer values of arbitrary size. 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 than using the hardware arithmetic. In most cases arithmetic -is fast enough, even for large numbers. The arithmetic operations +is fast enough, even for numbers in the millions. The arithmetic operations provided for literals include addition, subtraction, multiplication, integer division and remainder. Fractions of literals (expressed using division) are reduced to lowest terms. @@ -98,14 +97,14 @@ \end{warn} - \subsection{The Type of Natural Numbers, {\tt\slshape nat}} \index{natural numbers|(}\index{*nat (type)|(}% This type requires no introduction: we have been using it from the 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. +proved in the theories \isa{Nat}, \isa{NatArith} and \isa{Divides}. +Basic properties of addition and multiplication are available through the +axiomatic type class for semirings (\S\ref{sec:numeric-axclasses}). \subsubsection{Literals} \index{numeric literals!for type \protect\isa{nat}}% @@ -134,30 +133,6 @@ the simplifier will normally reverse this transformation. Novices should express natural numbers using \isa{0} and \isa{Suc} only. -\subsubsection{Typical lemmas} -Inequalities involving addition and subtraction alone can be proved -automatically. Lemmas such as these can be used to prove inequalities -involving multiplication and division: -\begin{isabelle} -\isasymlbrakk i\ \isasymle \ j;\ k\ \isasymle \ l\isasymrbrakk \ \isasymLongrightarrow \ i\ *\ k\ \isasymle \ j\ *\ l% -\rulename{mult_le_mono}\isanewline -\isasymlbrakk i\ <\ j;\ 0\ <\ k\isasymrbrakk \ \isasymLongrightarrow \ i\ -*\ k\ <\ j\ *\ k% -\rulename{mult_less_mono1}\isanewline -m\ \isasymle \ n\ \isasymLongrightarrow \ m\ div\ k\ \isasymle \ n\ div\ k% -\rulename{div_le_mono} -\end{isabelle} -% -Various distributive laws concerning multiplication are available: -\begin{isabelle} -(m\ +\ n)\ *\ k\ =\ m\ *\ k\ +\ n\ *\ k% -\rulenamedx{add_mult_distrib}\isanewline -(m\ -\ n)\ *\ k\ =\ m\ *\ k\ -\ n\ *\ k% -\rulenamedx{diff_mult_distrib}\isanewline -(m\ mod\ n)\ *\ k\ =\ (m\ *\ k)\ mod\ (n\ *\ k) -\rulenamedx{mod_mult_distrib} -\end{isabelle} - \subsubsection{Division} \index{division!for type \protect\isa{nat}}% The infix operators \isa{div} and \isa{mod} are overloaded. @@ -182,7 +157,11 @@ a\ mod\ (b*c)\ =\ b * (a\ div\ b\ mod\ c)\ +\ a\ mod\ b% \rulename{mod_mult2_eq}\isanewline 0\ <\ c\ \isasymLongrightarrow \ (c\ *\ a)\ div\ (c\ *\ b)\ =\ a\ div\ b% -\rulename{div_mult_mult1} +\rulename{div_mult_mult1}\isanewline +(m\ mod\ n)\ *\ k\ =\ (m\ *\ k)\ mod\ (n\ *\ k) +\rulenamedx{mod_mult_distrib}\isanewline +m\ \isasymle \ n\ \isasymLongrightarrow \ m\ div\ k\ \isasymle \ n\ div\ k% +\rulename{div_le_mono} \end{isabelle} Surprisingly few of these results depend upon the @@ -196,8 +175,7 @@ a\ mod\ 0\ =\ a% \rulename{DIVISION_BY_ZERO_MOD} \end{isabelle} -As a concession to convention, these equations are not installed as default -simplification rules. In \isa{div_mult_mult1} above, one of +In \isa{div_mult_mult1} above, one of the two divisors (namely~\isa{c}) must still be nonzero. The \textbf{divides} relation\index{divides relation} @@ -217,19 +195,26 @@ \rulenamedx{dvd_add} \end{isabelle} -\subsubsection{Simplifier Tricks} -The rule \isa{diff_mult_distrib} shown above is one of the few facts +\subsubsection{Subtraction} + +There are no negative natural numbers, so \isa{m\ -\ n} equals zero unless +\isa{m} exceeds~\isa{n}. The following 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 +the condition \isa{n\ \isasymle \ m}. +\begin{isabelle} +(m\ -\ n)\ *\ k\ =\ m\ *\ k\ -\ n\ *\ k% +\rulenamedx{diff_mult_distrib} +\end{isabelle} +Natural number subtraction has few nice properties; often you should remove it by simplifying with this split -rule: +rule. \begin{isabelle} P(a-b)\ =\ ((a$, $\leq$ and $<$): @@ -379,27 +308,147 @@ \end{isabelle} -\subsection{The Type of Real Numbers, {\tt\slshape real}} +\subsection{The Types of Rational, Real and Complex Numbers} +\index{rational numbers|(}\index{*rat (type)|(}% \index{real numbers|(}\index{*real (type)|(}% -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