doc-src/TutorialI/Types/numerics.tex
author nipkow
Mon Mar 02 17:26:23 2009 +0100 (2009-03-02)
changeset 30200 0db3a35eab01
parent 27093 66d6da816be7
child 30224 79136ce06bdb
permissions -rw-r--r--
name fix
     1 % $Id$
     2 
     3 \section{Numbers}
     4 \label{sec:numbers}
     5 
     6 \index{numbers|(}%
     7 Until now, our numerical examples have used the type of \textbf{natural
     8 numbers},
     9 \isa{nat}.  This is a recursive datatype generated by the constructors
    10 zero  and successor, so it works well with inductive proofs and primitive
    11 recursive function definitions.  HOL also provides the type
    12 \isa{int} of \textbf{integers}, which lack induction but support true
    13 subtraction.  With subtraction, arithmetic reasoning is easier, which makes
    14 the integers preferable to the natural numbers for
    15 complicated arithmetic expressions, even if they are non-negative.  The logic HOL-Complex also has the types
    16 \isa{rat}, \isa{real} and \isa{complex}: the rational, real and complex numbers.  Isabelle has no 
    17 subtyping,  so the numeric
    18 types are distinct and there are functions to convert between them.
    19 Most numeric operations are overloaded: the same symbol can be
    20 used at all numeric types. Table~\ref{tab:overloading} in the appendix
    21 shows the most important operations, together with the priorities of the
    22 infix symbols. Algebraic properties are organized using type classes
    23 around algebraic concepts such as rings and fields;
    24 a property such as the commutativity of addition is a single theorem 
    25 (\isa{add_commute}) that applies to all numeric types.
    26 
    27 \index{linear arithmetic}%
    28 Many theorems involving numeric types can be proved automatically by
    29 Isabelle's arithmetic decision procedure, the method
    30 \methdx{arith}.  Linear arithmetic comprises addition, subtraction
    31 and multiplication by constant factors; subterms involving other operators
    32 are regarded as variables.  The procedure can be slow, especially if the
    33 subgoal to be proved involves subtraction over type \isa{nat}, which 
    34 causes case splits.  On types \isa{nat} and \isa{int}, \methdx{arith}
    35 can deal with quantifiers---this is known as Presburger arithmetic---whereas on type \isa{real} it cannot.
    36 
    37 The simplifier reduces arithmetic expressions in other
    38 ways, such as dividing through by common factors.  For problems that lie
    39 outside the scope of automation, HOL provides hundreds of
    40 theorems about multiplication, division, etc., that can be brought to
    41 bear.  You can locate them using Proof General's Find
    42 button.  A few lemmas are given below to show what
    43 is available.
    44 
    45 \subsection{Numeric Literals}
    46 \label{sec:numerals}
    47 
    48 \index{numeric literals|(}%
    49 The constants \cdx{0} and \cdx{1} are overloaded.  They denote zero and one,
    50 respectively, for all numeric types.  Other values are expressed by numeric
    51 literals, which consist of one or more decimal digits optionally preceeded by a minus sign (\isa{-}).  Examples are \isa{2}, \isa{-3} and
    52 \isa{441223334678}.  Literals are available for the types of natural
    53 numbers, integers, rationals, reals, etc.; they denote integer values of
    54 arbitrary size.
    55 
    56 Literals look like constants, but they abbreviate 
    57 terms representing the number in a two's complement binary notation. 
    58 Isabelle performs arithmetic on literals by rewriting rather 
    59 than using the hardware arithmetic. In most cases arithmetic 
    60 is fast enough, even for numbers in the millions. The arithmetic operations 
    61 provided for literals include addition, subtraction, multiplication, 
    62 integer division and remainder.  Fractions of literals (expressed using
    63 division) are reduced to lowest terms.
    64 
    65 \begin{warn}\index{overloading!and arithmetic}
    66 The arithmetic operators are 
    67 overloaded, so you must be careful to ensure that each numeric 
    68 expression refers to a specific type, if necessary by inserting 
    69 type constraints.  Here is an example of what can go wrong:
    70 \par
    71 \begin{isabelle}
    72 \isacommand{lemma}\ "2\ *\ m\ =\ m\ +\ m"
    73 \end{isabelle}
    74 %
    75 Carefully observe how Isabelle displays the subgoal:
    76 \begin{isabelle}
    77 \ 1.\ (2::'a)\ *\ m\ =\ m\ +\ m
    78 \end{isabelle}
    79 The type \isa{'a} given for the literal \isa{2} warns us that no numeric
    80 type has been specified.  The problem is underspecified.  Given a type
    81 constraint such as \isa{nat}, \isa{int} or \isa{real}, it becomes trivial.
    82 \end{warn}
    83 
    84 \begin{warn}
    85 \index{recdef@\isacommand {recdef} (command)!and numeric literals}  
    86 Numeric literals are not constructors and therefore
    87 must not be used in patterns.  For example, this declaration is
    88 rejected:
    89 \begin{isabelle}
    90 \isacommand{recdef}\ h\ "\isacharbraceleft \isacharbraceright "\isanewline
    91 "h\ 3\ =\ 2"\isanewline
    92 "h\ i\ \ =\ i"
    93 \end{isabelle}
    94 
    95 You should use a conditional expression instead:
    96 \begin{isabelle}
    97 "h\ i\ =\ (if\ i\ =\ 3\ then\ 2\ else\ i)"
    98 \end{isabelle}
    99 \index{numeric literals|)}
   100 \end{warn}
   101 
   102 
   103 \subsection{The Type of Natural Numbers, {\tt\slshape nat}}
   104 
   105 \index{natural numbers|(}\index{*nat (type)|(}%
   106 This type requires no introduction: we have been using it from the
   107 beginning.  Hundreds of theorems about the natural numbers are
   108 proved in the theories \isa{Nat} and \isa{Divides}.  
   109 Basic properties of addition and multiplication are available through the
   110 axiomatic type class for semirings (\S\ref{sec:numeric-axclasses}).
   111 
   112 \subsubsection{Literals}
   113 \index{numeric literals!for type \protect\isa{nat}}%
   114 The notational options for the natural  numbers are confusing.  Recall that an
   115 overloaded constant can be defined independently for each type; the definition
   116 of \cdx{1} for type \isa{nat} is
   117 \begin{isabelle}
   118 1\ \isasymequiv\ Suc\ 0
   119 \rulename{One_nat_def}
   120 \end{isabelle}
   121 This is installed as a simplification rule, so the simplifier will replace
   122 every occurrence of \isa{1::nat} by \isa{Suc\ 0}.  Literals are obviously
   123 better than nested \isa{Suc}s at expressing large values.  But many theorems,
   124 including the rewrite rules for primitive recursive functions, can only be
   125 applied to terms of the form \isa{Suc\ $n$}.
   126 
   127 The following default  simplification rules replace
   128 small literals by zero and successor: 
   129 \begin{isabelle}
   130 2\ +\ n\ =\ Suc\ (Suc\ n)
   131 \rulename{add_2_eq_Suc}\isanewline
   132 n\ +\ 2\ =\ Suc\ (Suc\ n)
   133 \rulename{add_2_eq_Suc'}
   134 \end{isabelle}
   135 It is less easy to transform \isa{100} into \isa{Suc\ 99} (for example), and
   136 the simplifier will normally reverse this transformation.  Novices should
   137 express natural numbers using \isa{0} and \isa{Suc} only.
   138 
   139 \subsubsection{Division}
   140 \index{division!for type \protect\isa{nat}}%
   141 The infix operators \isa{div} and \isa{mod} are overloaded.
   142 Isabelle/HOL provides the basic facts about quotient and remainder
   143 on the natural numbers:
   144 \begin{isabelle}
   145 m\ mod\ n\ =\ (if\ m\ <\ n\ then\ m\ else\ (m\ -\ n)\ mod\ n)
   146 \rulename{mod_if}\isanewline
   147 m\ div\ n\ *\ n\ +\ m\ mod\ n\ =\ m%
   148 \rulenamedx{mod_div_equality}
   149 \end{isabelle}
   150 
   151 Many less obvious facts about quotient and remainder are also provided. 
   152 Here is a selection:
   153 \begin{isabelle}
   154 a\ *\ b\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c%
   155 \rulename{div_mult1_eq}\isanewline
   156 a\ *\ b\ mod\ c\ =\ a\ *\ (b\ mod\ c)\ mod\ c%
   157 \rulename{mod_mult1_eq}\isanewline
   158 a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%
   159 \rulename{div_mult2_eq}\isanewline
   160 a\ mod\ (b*c)\ =\ b * (a\ div\ b\ mod\ c)\ +\ a\ mod\ b%
   161 \rulename{mod_mult2_eq}\isanewline
   162 0\ <\ c\ \isasymLongrightarrow \ (c\ *\ a)\ div\ (c\ *\ b)\ =\ a\ div\ b%
   163 \rulename{div_mult_mult1}\isanewline
   164 (m\ mod\ n)\ *\ k\ =\ (m\ *\ k)\ mod\ (n\ *\ k)
   165 \rulenamedx{mod_mult_distrib}\isanewline
   166 m\ \isasymle \ n\ \isasymLongrightarrow \ m\ div\ k\ \isasymle \ n\ div\ k%
   167 \rulename{div_le_mono}
   168 \end{isabelle}
   169 
   170 Surprisingly few of these results depend upon the
   171 divisors' being nonzero.
   172 \index{division!by zero}%
   173 That is because division by
   174 zero yields zero:
   175 \begin{isabelle}
   176 a\ div\ 0\ =\ 0
   177 \rulename{DIVISION_BY_ZERO_DIV}\isanewline
   178 a\ mod\ 0\ =\ a%
   179 \rulename{DIVISION_BY_ZERO_MOD}
   180 \end{isabelle}
   181 In \isa{div_mult_mult1} above, one of
   182 the two divisors (namely~\isa{c}) must still be nonzero.
   183 
   184 The \textbf{divides} relation\index{divides relation}
   185 has the standard definition, which
   186 is overloaded over all numeric types: 
   187 \begin{isabelle}
   188 m\ dvd\ n\ \isasymequiv\ {\isasymexists}k.\ n\ =\ m\ *\ k
   189 \rulenamedx{dvd_def}
   190 \end{isabelle}
   191 %
   192 Section~\ref{sec:proving-euclid} discusses proofs involving this
   193 relation.  Here are some of the facts proved about it:
   194 \begin{isabelle}
   195 \isasymlbrakk m\ dvd\ n;\ n\ dvd\ m\isasymrbrakk \ \isasymLongrightarrow \ m\ =\ n%
   196 \rulenamedx{dvd_anti_sym}\isanewline
   197 \isasymlbrakk k\ dvd\ m;\ k\ dvd\ n\isasymrbrakk \ \isasymLongrightarrow \ k\ dvd\ (m\ +\ n)
   198 \rulenamedx{dvd_add}
   199 \end{isabelle}
   200 
   201 \subsubsection{Subtraction}
   202 
   203 There are no negative natural numbers, so \isa{m\ -\ n} equals zero unless 
   204 \isa{m} exceeds~\isa{n}. The following is one of the few facts
   205 about \isa{m\ -\ n} that is not subject to
   206 the condition \isa{n\ \isasymle \  m}. 
   207 \begin{isabelle}
   208 (m\ -\ n)\ *\ k\ =\ m\ *\ k\ -\ n\ *\ k%
   209 \rulenamedx{diff_mult_distrib}
   210 \end{isabelle}
   211 Natural number subtraction has few
   212 nice properties; often you should remove it by simplifying with this split
   213 rule.
   214 \begin{isabelle}
   215 P(a-b)\ =\ ((a<b\ \isasymlongrightarrow \ P\
   216 0)\ \isasymand \ (\isasymforall d.\ a\ =\ b+d\ \isasymlongrightarrow \ P\
   217 d))
   218 \rulename{nat_diff_split}
   219 \end{isabelle}
   220 For example, splitting helps to prove the following fact.
   221 \begin{isabelle}
   222 \isacommand{lemma}\ "(n\ -\ 2)\ *\ (n\ +\ 2)\ =\ n\ *\ n\ -\ (4::nat)"\isanewline
   223 \isacommand{apply}\ (simp\ split:\ nat_diff_split,\ clarify)\isanewline
   224 \ 1.\ \isasymAnd d.\ \isasymlbrakk n\ <\ 2;\ n\ *\ n\ =\ 4\ +\ d\isasymrbrakk \ \isasymLongrightarrow \ d\ =\ 0
   225 \end{isabelle}
   226 The result lies outside the scope of linear arithmetic, but
   227  it is easily found
   228 if we explicitly split \isa{n<2} as \isa{n=0} or \isa{n=1}:
   229 \begin{isabelle}
   230 \isacommand{apply}\ (subgoal_tac\ "n=0\ |\ n=1",\ force,\ arith)\isanewline
   231 \isacommand{done}
   232 \end{isabelle}%%%%%%
   233 \index{natural numbers|)}\index{*nat (type)|)}
   234 
   235 
   236 \subsection{The Type of Integers, {\tt\slshape int}}
   237 
   238 \index{integers|(}\index{*int (type)|(}%
   239 Reasoning methods for the integers resemble those for the natural numbers, 
   240 but induction and
   241 the constant \isa{Suc} are not available.  HOL provides many lemmas for
   242 proving inequalities involving integer multiplication and division, similar
   243 to those shown above for type~\isa{nat}. The laws of addition, subtraction
   244 and multiplication are available through the axiomatic type class for rings
   245 (\S\ref{sec:numeric-axclasses}).
   246 
   247 The \rmindex{absolute value} function \cdx{abs} is overloaded, and is 
   248 defined for all types that involve negative numbers, including the integers.
   249 The \isa{arith} method can prove facts about \isa{abs} automatically, 
   250 though as it does so by case analysis, the cost can be exponential.
   251 \begin{isabelle}
   252 \isacommand{lemma}\ "abs\ (x+y)\ \isasymle \ abs\ x\ +\ abs\ (y\ ::\ int)"\isanewline
   253 \isacommand{by}\ arith
   254 \end{isabelle}
   255 
   256 For division and remainder,\index{division!by negative numbers}
   257 the treatment of negative divisors follows
   258 mathematical practice: the sign of the remainder follows that
   259 of the divisor:
   260 \begin{isabelle}
   261 0\ <\ b\ \isasymLongrightarrow \ 0\ \isasymle \ a\ mod\ b%
   262 \rulename{pos_mod_sign}\isanewline
   263 0\ <\ b\ \isasymLongrightarrow \ a\ mod\ b\ <\ b%
   264 \rulename{pos_mod_bound}\isanewline
   265 b\ <\ 0\ \isasymLongrightarrow \ a\ mod\ b\ \isasymle \ 0
   266 \rulename{neg_mod_sign}\isanewline
   267 b\ <\ 0\ \isasymLongrightarrow \ b\ <\ a\ mod\ b%
   268 \rulename{neg_mod_bound}
   269 \end{isabelle}
   270 ML treats negative divisors in the same way, but most computer hardware
   271 treats signed operands using the same rules as for multiplication.
   272 Many facts about quotients and remainders are provided:
   273 \begin{isabelle}
   274 (a\ +\ b)\ div\ c\ =\isanewline
   275 a\ div\ c\ +\ b\ div\ c\ +\ (a\ mod\ c\ +\ b\ mod\ c)\ div\ c%
   276 \rulename{zdiv_zadd1_eq}
   277 \par\smallskip
   278 (a\ +\ b)\ mod\ c\ =\ (a\ mod\ c\ +\ b\ mod\ c)\ mod\ c%
   279 \rulename{mod_add1_eq}
   280 \end{isabelle}
   281 
   282 \begin{isabelle}
   283 (a\ *\ b)\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c%
   284 \rulename{zdiv_zmult1_eq}\isanewline
   285 (a\ *\ b)\ mod\ c\ =\ a\ *\ (b\ mod\ c)\ mod\ c%
   286 \rulename{zmod_zmult1_eq}
   287 \end{isabelle}
   288 
   289 \begin{isabelle}
   290 0\ <\ c\ \isasymLongrightarrow \ a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%
   291 \rulename{zdiv_zmult2_eq}\isanewline
   292 0\ <\ c\ \isasymLongrightarrow \ a\ mod\ (b*c)\ =\ b*(a\ div\ b\ mod\
   293 c)\ +\ a\ mod\ b%
   294 \rulename{zmod_zmult2_eq}
   295 \end{isabelle}
   296 The last two differ from their natural number analogues by requiring
   297 \isa{c} to be positive.  Since division by zero yields zero, we could allow
   298 \isa{c} to be zero.  However, \isa{c} cannot be negative: a counterexample
   299 is
   300 $\isa{a} = 7$, $\isa{b} = 2$ and $\isa{c} = -3$, when the left-hand side of
   301 \isa{zdiv_zmult2_eq} is $-2$ while the right-hand side is~$-1$.
   302 The prefix~\isa{z} in many theorem names recalls the use of $\mathbb{Z}$ to
   303 denote the set of integers.%
   304 \index{integers|)}\index{*int (type)|)}
   305 
   306 Induction is less important for integers than it is for the natural numbers, but it can be valuable if the range of integers has a lower or upper bound.  There are four rules for integer induction, corresponding to the possible relations of the bound ($\geq$, $>$, $\leq$ and $<$):
   307 \begin{isabelle}
   308 \isasymlbrakk k\ \isasymle \ i;\ P\ k;\ \isasymAnd i.\ \isasymlbrakk k\ \isasymle \ i;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i+1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%
   309 \rulename{int_ge_induct}\isanewline
   310 \isasymlbrakk k\ <\ i;\ P(k+1);\ \isasymAnd i.\ \isasymlbrakk k\ <\ i;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i+1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%
   311 \rulename{int_gr_induct}\isanewline
   312 \isasymlbrakk i\ \isasymle \ k;\ P\ k;\ \isasymAnd i.\ \isasymlbrakk i\ \isasymle \ k;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i-1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%
   313 \rulename{int_le_induct}\isanewline
   314 \isasymlbrakk i\ <\ k;\ P(k-1);\ \isasymAnd i.\ \isasymlbrakk i\ <\ k;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i-1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%
   315 \rulename{int_less_induct}
   316 \end{isabelle}
   317 
   318 
   319 \subsection{The Types of Rational, Real and Complex Numbers}
   320 \label{sec:real}
   321 
   322 \index{rational numbers|(}\index{*rat (type)|(}%
   323 \index{real numbers|(}\index{*real (type)|(}%
   324 \index{complex numbers|(}\index{*complex (type)|(}%
   325 These types provide true division, the overloaded operator \isa{/}, 
   326 which differs from the operator \isa{div} of the 
   327 natural numbers and integers. The rationals and reals are 
   328 \textbf{dense}: between every two distinct numbers lies another.
   329 This property follows from the division laws, since if $x\not=y$ then $(x+y)/2$ lies between them:
   330 \begin{isabelle}
   331 a\ <\ b\ \isasymLongrightarrow \ \isasymexists r.\ a\ <\ r\ \isasymand \ r\ <\ b%
   332 \rulename{dense}
   333 \end{isabelle}
   334 
   335 The real numbers are, moreover, \textbf{complete}: every set of reals that
   336 is bounded above has a least upper bound.  Completeness distinguishes the
   337 reals from the rationals, for which the set $\{x\mid x^2<2\}$ has no least
   338 upper bound.  (It could only be $\surd2$, which is irrational.) The
   339 formalization of completeness, which is complicated, 
   340 can be found in theory \texttt{RComplete} of directory
   341 \texttt{Real}.
   342 
   343 Numeric literals\index{numeric literals!for type \protect\isa{real}}
   344 for type \isa{real} have the same syntax as those for type
   345 \isa{int} and only express integral values.  Fractions expressed
   346 using the division operator are automatically simplified to lowest terms:
   347 \begin{isabelle}
   348 \ 1.\ P\ ((3\ /\ 4)\ *\ (8\ /\ 15))\isanewline
   349 \isacommand{apply} simp\isanewline
   350 \ 1.\ P\ (2\ /\ 5)
   351 \end{isabelle}
   352 Exponentiation can express floating-point values such as
   353 \isa{2 * 10\isacharcircum6}, but at present no special simplification
   354 is performed.
   355 
   356 \begin{warn}
   357 Type \isa{real} is only available in the logic HOL-Complex, which is
   358 HOL extended with a definitional development of the real and complex
   359 numbers.  Base your theory upon theory \thydx{Complex_Main}, not the
   360 usual \isa{Main}, and set the Proof General menu item \pgmenu{Isabelle} $>$
   361 \pgmenu{Logics} $>$ \pgmenu{HOL-Complex}.%
   362 \index{real numbers|)}\index{*real (type)|)}
   363 \end{warn}
   364 
   365 Also available in HOL-Complex is the
   366 theory \isa{Hyperreal}, which define the type \tydx{hypreal} of 
   367 \rmindex{non-standard reals}.  These
   368 \textbf{hyperreals} include infinitesimals, which represent infinitely
   369 small and infinitely large quantities; they facilitate proofs
   370 about limits, differentiation and integration~\cite{fleuriot-jcm}.  The
   371 development defines an infinitely large number, \isa{omega} and an
   372 infinitely small positive number, \isa{epsilon}.  The 
   373 relation $x\approx y$ means ``$x$ is infinitely close to~$y$.''
   374 Theory \isa{Hyperreal} also defines transcendental functions such as sine,
   375 cosine, exponential and logarithm --- even the versions for type
   376 \isa{real}, because they are defined using nonstandard limits.%
   377 \index{rational numbers|)}\index{*rat (type)|)}%
   378 \index{real numbers|)}\index{*real (type)|)}%
   379 \index{complex numbers|)}\index{*complex (type)|)}
   380 
   381 
   382 \subsection{The Numeric Type Classes}\label{sec:numeric-axclasses}
   383 
   384 Isabelle/HOL organises its numeric theories using axiomatic type classes.
   385 Hundreds of basic properties are proved in the theory \isa{Ring_and_Field}.
   386 These lemmas are available (as simprules if they were declared as such)
   387 for all numeric types satisfying the necessary axioms. The theory defines
   388 dozens of type classes, such as the following:
   389 \begin{itemize}
   390 \item 
   391 \tcdx{semiring} and \tcdx{ordered_semiring}: a \emph{semiring}
   392 provides the associative operators \isa{+} and~\isa{*}, with \isa{0} and~\isa{1}
   393 as their respective identities. The operators enjoy the usual distributive law,
   394 and addition (\isa{+}) is also commutative.
   395 An \emph{ordered semiring} is also linearly
   396 ordered, with addition and multiplication respecting the ordering. Type \isa{nat} is an ordered semiring.
   397 \item 
   398 \tcdx{ring} and \tcdx{ordered_ring}: a \emph{ring} extends a semiring
   399 with unary minus (the additive inverse) and subtraction (both
   400 denoted~\isa{-}). An \emph{ordered ring} includes the absolute value
   401 function, \cdx{abs}. Type \isa{int} is an ordered ring.
   402 \item 
   403 \tcdx{field} and \tcdx{ordered_field}: a field extends a ring with the
   404 multiplicative inverse (called simply \cdx{inverse} and division~(\isa{/})).
   405 An ordered field is based on an ordered ring. Type \isa{complex} is a field, while type \isa{real} is an ordered field.
   406 \item 
   407 \tcdx{division_by_zero} includes all types where \isa{inverse 0 = 0}
   408 and \isa{a / 0 = 0}. These include all of Isabelle's standard numeric types.
   409 However, the basic properties of fields are derived without assuming
   410 division by zero.
   411 \end{itemize}
   412 
   413 Hundreds of basic lemmas are proved, each of which
   414 holds for all types in the corresponding type class. In most
   415 cases, it is obvious whether a property is valid for a particular type. No
   416 abstract properties involving subtraction hold for type \isa{nat};
   417 instead, theorems such as
   418 \isa{diff_mult_distrib} are proved specifically about subtraction on
   419 type~\isa{nat}. All abstract properties involving division require a field.
   420 Obviously, all properties involving orderings required an ordered
   421 structure.
   422 
   423 The class \tcdx{ring_no_zero_divisors} of rings without zero divisors satisfies a number of natural cancellation laws, the first of which characterizes this class:
   424 \begin{isabelle}
   425 (a\ *\ b\ =\ (0::'a))\ =\ (a\ =\ (0::'a)\ \isasymor \ b\ =\ (0::'a))
   426 \rulename{mult_eq_0_iff}\isanewline
   427 (a\ *\ c\ =\ b\ *\ c)\ =\ (c\ =\ (0::'a)\ \isasymor \ a\ =\ b)
   428 \rulename{mult_cancel_right}
   429 \end{isabelle}
   430 \begin{pgnote}
   431 Setting the flag \pgmenu{Isabelle} $>$ \pgmenu{Settings} $>$
   432 \pgmenu{Show Sorts} will display the type classes of all type variables.
   433 \end{pgnote}
   434 \noindent
   435 Here is how the theorem \isa{mult_cancel_left} appears with the flag set.
   436 \begin{isabelle}
   437 ((c::'a::ring_no_zero_divisors)\ *\ (a::'a::ring_no_zero_divisors) =\isanewline
   438 \ c\ *\ (b::'a::ring_no_zero_divisors))\ =\isanewline
   439 (c\ =\ (0::'a::ring_no_zero_divisors)\ \isasymor\ a\ =\ b)
   440 \end{isabelle}
   441 
   442 
   443 \subsubsection{Simplifying with the AC-Laws}
   444 Suppose that two expressions are equal, differing only in 
   445 associativity and commutativity of addition.  Simplifying with the
   446 following equations sorts the terms and groups them to the right, making
   447 the two expressions identical.
   448 \begin{isabelle}
   449 a\ +\ b\ +\ c\ =\ a\ +\ (b\ +\ c)
   450 \rulenamedx{add_assoc}\isanewline
   451 a\ +\ b\ =\ b\ +\ a%
   452 \rulenamedx{add_commute}\isanewline
   453 a\ +\ (b\ +\ c)\ =\ b\ +\ (a\ +\ c)
   454 \rulename{add_left_commute}
   455 \end{isabelle}
   456 The name \isa{add_ac}\index{*add_ac (theorems)} 
   457 refers to the list of all three theorems; similarly
   458 there is \isa{mult_ac}.\index{*mult_ac (theorems)} 
   459 They are all proved for semirings and therefore hold for all numeric types.
   460 
   461 Here is an example of the sorting effect.  Start
   462 with this goal, which involves type \isa{nat}.
   463 \begin{isabelle}
   464 \ 1.\ Suc\ (i\ +\ j\ *\ l\ *\ k\ +\ m\ *\ n)\ =\
   465 f\ (n\ *\ m\ +\ i\ +\ k\ *\ j\ *\ l)
   466 \end{isabelle}
   467 %
   468 Simplify using  \isa{add_ac} and \isa{mult_ac}.
   469 \begin{isabelle}
   470 \isacommand{apply}\ (simp\ add:\ add_ac\ mult_ac)
   471 \end{isabelle}
   472 %
   473 Here is the resulting subgoal.
   474 \begin{isabelle}
   475 \ 1.\ Suc\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))\
   476 =\ f\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))%
   477 \end{isabelle}
   478 
   479 
   480 \subsubsection{Division Laws for Fields}
   481 
   482 Here is a selection of rules about the division operator.  The following
   483 are installed as default simplification rules in order to express
   484 combinations of products and quotients as rational expressions:
   485 \begin{isabelle}
   486 a\ *\ (b\ /\ c)\ =\ a\ *\ b\ /\ c
   487 \rulename{times_divide_eq_right}\isanewline
   488 b\ /\ c\ *\ a\ =\ b\ *\ a\ /\ c
   489 \rulename{times_divide_eq_left}\isanewline
   490 a\ /\ (b\ /\ c)\ =\ a\ *\ c\ /\ b
   491 \rulename{divide_divide_eq_right}\isanewline
   492 a\ /\ b\ /\ c\ =\ a\ /\ (b\ *\ c)
   493 \rulename{divide_divide_eq_left}
   494 \end{isabelle}
   495 
   496 Signs are extracted from quotients in the hope that complementary terms can
   497 then be cancelled:
   498 \begin{isabelle}
   499 -\ (a\ /\ b)\ =\ -\ a\ /\ b
   500 \rulename{minus_divide_left}\isanewline
   501 -\ (a\ /\ b)\ =\ a\ /\ -\ b
   502 \rulename{minus_divide_right}
   503 \end{isabelle}
   504 
   505 The following distributive law is available, but it is not installed as a
   506 simplification rule.
   507 \begin{isabelle}
   508 (a\ +\ b)\ /\ c\ =\ a\ /\ c\ +\ b\ /\ c%
   509 \rulename{add_divide_distrib}
   510 \end{isabelle}
   511 
   512 
   513 \subsubsection{Absolute Value}
   514 
   515 The \rmindex{absolute value} function \cdx{abs} is available for all 
   516 ordered rings, including types \isa{int}, \isa{rat} and \isa{real}.
   517 It satisfies many properties,
   518 such as the following:
   519 \begin{isabelle}
   520 \isasymbar x\ *\ y\isasymbar \ =\ \isasymbar x\isasymbar \ *\ \isasymbar y\isasymbar 
   521 \rulename{abs_mult}\isanewline
   522 (\isasymbar a\isasymbar \ \isasymle \ b)\ =\ (a\ \isasymle \ b\ \isasymand \ -\ a\ \isasymle \ b)
   523 \rulename{abs_le_iff}\isanewline
   524 \isasymbar a\ +\ b\isasymbar \ \isasymle \ \isasymbar a\isasymbar \ +\ \isasymbar b\isasymbar 
   525 \rulename{abs_triangle_ineq}
   526 \end{isabelle}
   527 
   528 \begin{warn}
   529 The absolute value bars shown above cannot be typed on a keyboard.  They
   530 can be entered using the X-symbol package.  In \textsc{ascii}, type \isa{abs x} to
   531 get \isa{\isasymbar x\isasymbar}.
   532 \end{warn}
   533 
   534 
   535 \subsubsection{Raising to a Power}
   536 
   537 Another type class, \tcdx{ringppower}, specifies rings that also have 
   538 exponentation to a natural number power, defined using the obvious primitive
   539 recursion. Theory \thydx{Power} proves various theorems, such as the 
   540 following.
   541 \begin{isabelle}
   542 a\ \isacharcircum \ (m\ +\ n)\ =\ a\ \isacharcircum \ m\ *\ a\ \isacharcircum \ n%
   543 \rulename{power_add}\isanewline
   544 a\ \isacharcircum \ (m\ *\ n)\ =\ (a\ \isacharcircum \ m)\ \isacharcircum \ n%
   545 \rulename{power_mult}\isanewline
   546 \isasymbar a\ \isacharcircum \ n\isasymbar \ =\ \isasymbar a\isasymbar \ \isacharcircum \ n%
   547 \rulename{power_abs}
   548 \end{isabelle}%%%%%%%%%%%%%%%%%%%%%%%%%
   549 \index{numbers|)}