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
     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_mult_right_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_add_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|)}