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