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