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