doc-src/TutorialI/Types/numerics.tex
 author paulson Mon Jan 12 16:51:45 2004 +0100 (2004-01-12) changeset 14353 79f9fbef9106 parent 14295 7f115e5c5de4 child 14400 6069098854b9 permissions -rw-r--r--
Added lemmas to Ring_and_Field with slightly modified simplification rules

Deleted some little-used integer theorems, replacing them by the generic ones
in Ring_and_Field

Consolidated integer powers
     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.  The integers are preferable to the natural numbers for reasoning about

    14 complicated arithmetic expressions, even for some expressions whose

    15 value is non-negative.  The logic HOL-Complex also has the types

    16 \isa{real} and \isa{complex}: the 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 Fortunately 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.

    23

    24 \index{linear arithmetic}%

    25 Many theorems involving numeric types can be proved automatically by

    26 Isabelle's arithmetic decision procedure, the method

    27 \methdx{arith}.  Linear arithmetic comprises addition, subtraction

    28 and multiplication by constant factors; subterms involving other operators

    29 are regarded as variables.  The procedure can be slow, especially if the

    30 subgoal to be proved involves subtraction over type \isa{nat}, which

    31 causes case splits.  On types \isa{nat} and \isa{int}, \methdx{arith}

    32 can deal with quantifiers (this is known as Presburger Arithmetic''),

    33 whereas on type \isa{real} it cannot.

    34

    35 The simplifier reduces arithmetic expressions in other

    36 ways, such as dividing through by common factors.  For problems that lie

    37 outside the scope of automation, HOL provides hundreds of

    38 theorems about multiplication, division, etc., that can be brought to

    39 bear.  You can locate them using Proof General's Find

    40 button.  A few lemmas are given below to show what

    41 is available.

    42

    43 \subsection{Numeric Literals}

    44 \label{sec:numerals}

    45

    46 \index{numeric literals|(}%

    47 The constants \cdx{0} and \cdx{1} are overloaded.  They denote zero and one,

    48 respectively, for all numeric types.  Other values are expressed by numeric

    49 literals, which consist of one or more decimal digits optionally preceeded by

    50 a minus sign (\isa{-}).  Examples are \isa{2}, \isa{-3} and

    51 \isa{441223334678}.  Literals are available for the types of natural numbers,

    52 integers and reals; they denote integer values of arbitrary size.

    53

    54 Literals look like constants, but they abbreviate

    55 terms representing the number in a two's complement binary notation.

    56 Isabelle performs arithmetic on literals by rewriting rather

    57 than using the hardware arithmetic. In most cases arithmetic

    58 is fast enough, even for large numbers. The arithmetic operations

    59 provided for literals include addition, subtraction, multiplication,

    60 integer division and remainder.  Fractions of literals (expressed using

    61 division) are reduced to lowest terms.

    62

    63 \begin{warn}\index{overloading!and arithmetic}

    64 The arithmetic operators are

    65 overloaded, so you must be careful to ensure that each numeric

    66 expression refers to a specific type, if necessary by inserting

    67 type 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 %

    73 Carefully observe how Isabelle displays the subgoal:

    74 \begin{isabelle}

    75 \ 1.\ (2::'a)\ *\ m\ =\ m\ +\ m

    76 \end{isabelle}

    77 The type \isa{'a} given for the literal \isa{2} warns us that no numeric

    78 type has been specified.  The problem is underspecified.  Given a type

    79 constraint such as \isa{nat}, \isa{int} or \isa{real}, it becomes trivial.

    80 \end{warn}

    81

    82 \begin{warn}

    83 \index{recdef@\isacommand {recdef} (command)!and numeric literals}

    84 Numeric literals are not constructors and therefore

    85 must not be used in patterns.  For example, this declaration is

    86 rejected:

    87 \begin{isabelle}

    88 \isacommand{recdef}\ h\ "\isacharbraceleft \isacharbraceright "\isanewline

    89 "h\ 3\ =\ 2"\isanewline

    90 "h\ i\ \ =\ i"

    91 \end{isabelle}

    92

    93 You 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

   102 \subsection{The Type of Natural Numbers, {\tt\slshape nat}}

   103

   104 \index{natural numbers|(}\index{*nat (type)|(}%

   105 This type requires no introduction: we have been using it from the

   106 beginning.  Hundreds of theorems about the natural numbers are

   107 proved in the theories \isa{Nat}, \isa{NatArith} and \isa{Divides}.  Only

   108 in exceptional circumstances should you resort to induction.

   109

   110 \subsubsection{Literals}

   111 \index{numeric literals!for type \protect\isa{nat}}%

   112 The notational options for the natural  numbers are confusing.  Recall that an

   113 overloaded constant can be defined independently for each type; the definition

   114 of \cdx{1} for type \isa{nat} is

   115 \begin{isabelle}

   116 1\ \isasymequiv\ Suc\ 0

   117 \rulename{One_nat_def}

   118 \end{isabelle}

   119 This is installed as a simplification rule, so the simplifier will replace

   120 every occurrence of \isa{1::nat} by \isa{Suc\ 0}.  Literals are obviously

   121 better than nested \isa{Suc}s at expressing large values.  But many theorems,

   122 including the rewrite rules for primitive recursive functions, can only be

   123 applied to terms of the form \isa{Suc\ $n$}.

   124

   125 The following default  simplification rules replace

   126 small literals by zero and successor:

   127 \begin{isabelle}

   128 2\ +\ n\ =\ Suc\ (Suc\ n)

   129 \rulename{add_2_eq_Suc}\isanewline

   130 n\ +\ 2\ =\ Suc\ (Suc\ n)

   131 \rulename{add_2_eq_Suc'}

   132 \end{isabelle}

   133 It is less easy to transform \isa{100} into \isa{Suc\ 99} (for example), and

   134 the simplifier will normally reverse this transformation.  Novices should

   135 express natural numbers using \isa{0} and \isa{Suc} only.

   136

   137 \subsubsection{Typical lemmas}

   138 Inequalities involving addition and subtraction alone can be proved

   139 automatically.  Lemmas such as these can be used to prove inequalities

   140 involving multiplication and division:

   141 \begin{isabelle}

   142 \isasymlbrakk i\ \isasymle \ j;\ k\ \isasymle \ l\isasymrbrakk \ \isasymLongrightarrow \ i\ *\ k\ \isasymle \ j\ *\ l%

   143 \rulename{mult_le_mono}\isanewline

   144 \isasymlbrakk i\ <\ j;\ 0\ <\ k\isasymrbrakk \ \isasymLongrightarrow \ i\

   145 *\ k\ <\ j\ *\ k%

   146 \rulename{mult_less_mono1}\isanewline

   147 m\ \isasymle \ n\ \isasymLongrightarrow \ m\ div\ k\ \isasymle \ n\ div\ k%

   148 \rulename{div_le_mono}

   149 \end{isabelle}

   150 %

   151 Various distributive laws concerning multiplication are available:

   152 \begin{isabelle}

   153 (m\ +\ n)\ *\ k\ =\ m\ *\ k\ +\ n\ *\ k%

   154 \rulenamedx{add_mult_distrib}\isanewline

   155 (m\ -\ n)\ *\ k\ =\ m\ *\ k\ -\ n\ *\ k%

   156 \rulenamedx{diff_mult_distrib}\isanewline

   157 (m\ mod\ n)\ *\ k\ =\ (m\ *\ k)\ mod\ (n\ *\ k)

   158 \rulenamedx{mod_mult_distrib}

   159 \end{isabelle}

   160

   161 \subsubsection{Division}

   162 \index{division!for type \protect\isa{nat}}%

   163 The infix operators \isa{div} and \isa{mod} are overloaded.

   164 Isabelle/HOL provides the basic facts about quotient and remainder

   165 on the natural numbers:

   166 \begin{isabelle}

   167 m\ mod\ n\ =\ (if\ m\ <\ n\ then\ m\ else\ (m\ -\ n)\ mod\ n)

   168 \rulename{mod_if}\isanewline

   169 m\ div\ n\ *\ n\ +\ m\ mod\ n\ =\ m%

   170 \rulenamedx{mod_div_equality}

   171 \end{isabelle}

   172

   173 Many less obvious facts about quotient and remainder are also provided.

   174 Here is a selection:

   175 \begin{isabelle}

   176 a\ *\ b\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c%

   177 \rulename{div_mult1_eq}\isanewline

   178 a\ *\ b\ mod\ c\ =\ a\ *\ (b\ mod\ c)\ mod\ c%

   179 \rulename{mod_mult1_eq}\isanewline

   180 a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%

   181 \rulename{div_mult2_eq}\isanewline

   182 a\ mod\ (b*c)\ =\ b * (a\ div\ b\ mod\ c)\ +\ a\ mod\ b%

   183 \rulename{mod_mult2_eq}\isanewline

   184 0\ <\ c\ \isasymLongrightarrow \ (c\ *\ a)\ div\ (c\ *\ b)\ =\ a\ div\ b%

   185 \rulename{div_mult_mult1}

   186 \end{isabelle}

   187

   188 Surprisingly few of these results depend upon the

   189 divisors' being nonzero.

   190 \index{division!by zero}%

   191 That is because division by

   192 zero yields zero:

   193 \begin{isabelle}

   194 a\ div\ 0\ =\ 0

   195 \rulename{DIVISION_BY_ZERO_DIV}\isanewline

   196 a\ mod\ 0\ =\ a%

   197 \rulename{DIVISION_BY_ZERO_MOD}

   198 \end{isabelle}

   199 As a concession to convention, these equations are not installed as default

   200 simplification rules.  In \isa{div_mult_mult1} above, one of

   201 the two divisors (namely~\isa{c}) must still be nonzero.

   202

   203 The \textbf{divides} relation\index{divides relation}

   204 has the standard definition, which

   205 is overloaded over all numeric types:

   206 \begin{isabelle}

   207 m\ dvd\ n\ \isasymequiv\ {\isasymexists}k.\ n\ =\ m\ *\ k

   208 \rulenamedx{dvd_def}

   209 \end{isabelle}

   210 %

   211 Section~\ref{sec:proving-euclid} discusses proofs involving this

   212 relation.  Here are some of the facts proved about it:

   213 \begin{isabelle}

   214 \isasymlbrakk m\ dvd\ n;\ n\ dvd\ m\isasymrbrakk \ \isasymLongrightarrow \ m\ =\ n%

   215 \rulenamedx{dvd_anti_sym}\isanewline

   216 \isasymlbrakk k\ dvd\ m;\ k\ dvd\ n\isasymrbrakk \ \isasymLongrightarrow \ k\ dvd\ (m\ +\ n)

   217 \rulenamedx{dvd_add}

   218 \end{isabelle}

   219

   220 \subsubsection{Simplifier Tricks}

   221 The rule \isa{diff_mult_distrib} shown above is one of the few facts

   222 about \isa{m\ -\ n} that is not subject to

   223 the condition \isa{n\ \isasymle \  m}.  Natural number subtraction has few

   224 nice properties; often you should remove it by simplifying with this split

   225 rule:

   226 \begin{isabelle}

   227 P(a-b)\ =\ ((a<b\ \isasymlongrightarrow \ P\

   228 0)\ \isasymand \ (\isasymforall d.\ a\ =\ b+d\ \isasymlongrightarrow \ P\

   229 d))

   230 \rulename{nat_diff_split}

   231 \end{isabelle}

   232 For example, splitting helps to prove the following fact:

   233 \begin{isabelle}

   234 \isacommand{lemma}\ "(n\ -\ 2)\ *\ (n\ +\ 2)\ =\ n\ *\ n\ -\ (4::nat)"\isanewline

   235 \isacommand{apply}\ (simp\ split:\ nat_diff_split,\ clarify)\isanewline

   236 \ 1.\ \isasymAnd d.\ \isasymlbrakk n\ <\ 2;\ n\ *\ n\ =\ 4\ +\ d\isasymrbrakk \ \isasymLongrightarrow \ d\ =\ 0

   237 \end{isabelle}

   238 The result lies outside the scope of linear arithmetic, but

   239  it is easily found

   240 if we explicitly split \isa{n<2} as \isa{n=0} or \isa{n=1}:

   241 \begin{isabelle}

   242 \isacommand{apply}\ (subgoal_tac\ "n=0\ |\ n=1",\ force,\ arith)\isanewline

   243 \isacommand{done}

   244 \end{isabelle}

   245

   246 Suppose that two expressions are equal, differing only in

   247 associativity and commutativity of addition.  Simplifying with the

   248 following equations sorts the terms and groups them to the right, making

   249 the two expressions identical:

   250 \begin{isabelle}

   251 m\ +\ n\ +\ k\ =\ m\ +\ (n\ +\ k)

   252 \rulenamedx{add_assoc}\isanewline

   253 m\ +\ n\ =\ n\ +\ m%

   254 \rulenamedx{add_commute}\isanewline

   255 x\ +\ (y\ +\ z)\ =\ y\ +\ (x\

   256 +\ z)

   257 \rulename{add_left_commute}

   258 \end{isabelle}

   259 The name \isa{add_ac}\index{*add_ac (theorems)}

   260 refers to the list of all three theorems; similarly

   261 there is \isa{mult_ac}.\index{*mult_ac (theorems)}

   262 Here is an example of the sorting effect.  Start

   263 with this goal:

   264 \begin{isabelle}

   265 \ 1.\ Suc\ (i\ +\ j\ *\ l\ *\ k\ +\ m\ *\ n)\ =\

   266 f\ (n\ *\ m\ +\ i\ +\ k\ *\ j\ *\ l)

   267 \end{isabelle}

   268 %

   269 Simplify using  \isa{add_ac} and \isa{mult_ac}:

   270 \begin{isabelle}

   271 \isacommand{apply}\ (simp\ add:\ add_ac\ mult_ac)

   272 \end{isabelle}

   273 %

   274 Here is the resulting subgoal:

   275 \begin{isabelle}

   276 \ 1.\ Suc\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))\

   277 =\ f\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))%

   278 \end{isabelle}%

   279 \index{natural numbers|)}\index{*nat (type)|)}

   280

   281

   282

   283 \subsection{The Type of Integers, {\tt\slshape int}}

   284

   285 \index{integers|(}\index{*int (type)|(}%

   286 Reasoning methods resemble those for the natural numbers, but induction and

   287 the constant \isa{Suc} are not available.  HOL provides many lemmas

   288 for proving inequalities involving integer multiplication and division,

   289 similar to those shown above for type~\isa{nat}.

   290

   291 The \rmindex{absolute value} function \cdx{abs} is overloaded for the numeric types.

   292 It is defined for the integers; we have for example the obvious law

   293 \begin{isabelle}

   294 \isasymbar x\ *\ y\isasymbar \ =\ \isasymbar x\isasymbar \ *\ \isasymbar y\isasymbar

   295 \rulename{abs_mult}

   296 \end{isabelle}

   297

   298 \begin{warn}

   299 The absolute value bars shown above cannot be typed on a keyboard.  They

   300 can be entered using the X-symbol package.  In \textsc{ascii}, type \isa{abs x} to

   301 get \isa{\isasymbar x\isasymbar}.

   302 \end{warn}

   303

   304 The \isa{arith} method can prove facts about \isa{abs} automatically,

   305 though as it does so by case analysis, the cost can be exponential.

   306 \begin{isabelle}

   307 \isacommand{lemma}\ "abs\ (x+y)\ \isasymle \ abs\ x\ +\ abs\ (y\ ::\ int)"\isanewline

   308 \isacommand{by}\ arith

   309 \end{isabelle}

   310

   311 Concerning simplifier tricks, we have no need to eliminate subtraction: it

   312 is well-behaved.  As with the natural numbers, the simplifier can sort the

   313 operands of sums and products.  The name \isa{zadd_ac}\index{*zadd_ac (theorems)}

   314 refers to the

   315 associativity and commutativity theorems for integer addition, while

   316 \isa{zmult_ac}\index{*zmult_ac (theorems)}

   317 has the analogous theorems for multiplication.  The

   318 prefix~\isa{z} in many theorem names recalls the use of $\mathbb{Z}$ to

   319 denote the set of integers.

   320

   321 For division and remainder,\index{division!by negative numbers}

   322 the treatment of negative divisors follows

   323 mathematical practice: the sign of the remainder follows that

   324 of the divisor:

   325 \begin{isabelle}

   326 0\ <\ b\ \isasymLongrightarrow \ 0\ \isasymle \ a\ mod\ b%

   327 \rulename{pos_mod_sign}\isanewline

   328 0\ <\ b\ \isasymLongrightarrow \ a\ mod\ b\ <\ b%

   329 \rulename{pos_mod_bound}\isanewline

   330 b\ <\ 0\ \isasymLongrightarrow \ a\ mod\ b\ \isasymle \ 0

   331 \rulename{neg_mod_sign}\isanewline

   332 b\ <\ 0\ \isasymLongrightarrow \ b\ <\ a\ mod\ b%

   333 \rulename{neg_mod_bound}

   334 \end{isabelle}

   335 ML treats negative divisors in the same way, but most computer hardware

   336 treats signed operands using the same rules as for multiplication.

   337 Many facts about quotients and remainders are provided:

   338 \begin{isabelle}

   339 (a\ +\ b)\ div\ c\ =\isanewline

   340 a\ div\ c\ +\ b\ div\ c\ +\ (a\ mod\ c\ +\ b\ mod\ c)\ div\ c%

   341 \rulename{zdiv_zadd1_eq}

   342 \par\smallskip

   343 (a\ +\ b)\ mod\ c\ =\ (a\ mod\ c\ +\ b\ mod\ c)\ mod\ c%

   344 \rulename{zmod_zadd1_eq}

   345 \end{isabelle}

   346

   347 \begin{isabelle}

   348 (a\ *\ b)\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c%

   349 \rulename{zdiv_zmult1_eq}\isanewline

   350 (a\ *\ b)\ mod\ c\ =\ a\ *\ (b\ mod\ c)\ mod\ c%

   351 \rulename{zmod_zmult1_eq}

   352 \end{isabelle}

   353

   354 \begin{isabelle}

   355 0\ <\ c\ \isasymLongrightarrow \ a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%

   356 \rulename{zdiv_zmult2_eq}\isanewline

   357 0\ <\ c\ \isasymLongrightarrow \ a\ mod\ (b*c)\ =\ b*(a\ div\ b\ mod\

   358 c)\ +\ a\ mod\ b%

   359 \rulename{zmod_zmult2_eq}

   360 \end{isabelle}

   361 The last two differ from their natural number analogues by requiring

   362 \isa{c} to be positive.  Since division by zero yields zero, we could allow

   363 \isa{c} to be zero.  However, \isa{c} cannot be negative: a counterexample

   364 is

   365 $\isa{a} = 7$, $\isa{b} = 2$ and $\isa{c} = -3$, when the left-hand side of

   366 \isa{zdiv_zmult2_eq} is $-2$ while the right-hand side is~$-1$.%

   367 \index{integers|)}\index{*int (type)|)}

   368

   369 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 $<$):

   370 \begin{isabelle}

   371 \isasymlbrakk k\ \isasymle \ i;\ P\ k;\ \isasymAnd i.\ \isasymlbrakk k\ \isasymle \ i;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i+1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%

   372 \rulename{int_ge_induct}\isanewline

   373 \isasymlbrakk k\ <\ i;\ P(k+1);\ \isasymAnd i.\ \isasymlbrakk k\ <\ i;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i+1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%

   374 \rulename{int_gr_induct}\isanewline

   375 \isasymlbrakk i\ \isasymle \ k;\ P\ k;\ \isasymAnd i.\ \isasymlbrakk i\ \isasymle \ k;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i-1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%

   376 \rulename{int_le_induct}\isanewline

   377 \isasymlbrakk i\ <\ k;\ P(k-1);\ \isasymAnd i.\ \isasymlbrakk i\ <\ k;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i-1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%

   378 \rulename{int_less_induct}

   379 \end{isabelle}

   380

   381

   382 \subsection{The Type of Real Numbers, {\tt\slshape real}}

   383

   384 \index{real numbers|(}\index{*real (type)|(}%

   385 The real numbers enjoy two significant properties that the integers lack.

   386 They are

   387 \textbf{dense}: between every two distinct real numbers there lies another.

   388 This property follows from the division laws, since if $x<y$ then between

   389 them lies $(x+y)/2$.  The second property is that they are

   390 \textbf{complete}: every set of reals that is bounded above has a least

   391 upper bound.  Completeness distinguishes the reals from the rationals, for

   392 which the set $\{x\mid x^2<2\}$ has no least upper bound.  (It could only be

   393 $\surd2$, which is irrational.)

   394 The formalization of completeness is complicated; rather than

   395 reproducing it here, we refer you to the theory \texttt{RComplete} in

   396 directory \texttt{Real}.

   397 Density, however, is trivial to express:

   398 \begin{isabelle}

   399 x\ <\ y\ \isasymLongrightarrow \ \isasymexists r.\ x\ <\ r\ \isasymand \ r\ <\ y%

   400 \rulename{dense}

   401 \end{isabelle}

   402

   403 Here is a selection of rules about the division operator.  The following

   404 are installed as default simplification rules in order to express

   405 combinations of products and quotients as rational expressions:

   406 \begin{isabelle}

   407 a\ *\ (b\ /\ c)\ =\ a\ *\ b\ /\ c

   408 \rulename{times_divide_eq_right}\isanewline

   409 b\ /\ c\ *\ a\ =\ b\ *\ a\ /\ c

   410 \rulename{times_divide_eq_left}\isanewline

   411 a\ /\ (b\ /\ c)\ =\ a\ *\ c\ /\ b

   412 \rulename{divide_divide_eq_right}\isanewline

   413 a\ /\ b\ /\ c\ =\ a\ /\ (b\ *\ c)

   414 \rulename{divide_divide_eq_left}

   415 \end{isabelle}

   416

   417 Signs are extracted from quotients in the hope that complementary terms can

   418 then be cancelled:

   419 \begin{isabelle}

   420 -\ (a\ /\ b)\ =\ -\ a\ /\ b

   421 \rulename{minus_divide_left}\isanewline

   422 -\ (a\ /\ b)\ =\ a\ /\ -\ b

   423 \rulename{minus_divide_right}

   424 \end{isabelle}

   425

   426 The following distributive law is available, but it is not installed as a

   427 simplification rule.

   428 \begin{isabelle}

   429 (a\ +\ b)\ /\ c\ =\ a\ /\ c\ +\ b\ /\ c%

   430 \rulename{add_divide_distrib}

   431 \end{isabelle}

   432

   433 As with the other numeric types, the simplifier can sort the operands of

   434 addition and multiplication.  The name \isa{real_add_ac} refers to the

   435 associativity and commutativity theorems for addition, while similarly

   436 \isa{real_mult_ac} contains those properties for multiplication.

   437

   438 The absolute value function \isa{abs} is

   439 defined for the reals, along with many theorems such as this one about

   440 exponentiation:

   441 \begin{isabelle}

   442 \isasymbar a\ \isacharcircum \ n\isasymbar\ =\

   443 \isasymbar a\isasymbar \ \isacharcircum \ n

   444 \rulename{power_abs}

   445 \end{isabelle}

   446

   447 Numeric literals\index{numeric literals!for type \protect\isa{real}}

   448 for type \isa{real} have the same syntax as those for type

   449 \isa{int} and only express integral values.  Fractions expressed

   450 using the division operator are automatically simplified to lowest terms:

   451 \begin{isabelle}

   452 \ 1.\ P\ ((3\ /\ 4)\ *\ (8\ /\ 15))\isanewline

   453 \isacommand{apply} simp\isanewline

   454 \ 1.\ P\ (2\ /\ 5)

   455 \end{isabelle}

   456 Exponentiation can express floating-point values such as

   457 \isa{2 * 10\isacharcircum6}, but at present no special simplification

   458 is performed.

   459

   460

   461 \begin{warn}

   462 Type \isa{real} is only available in the logic HOL-Complex, which

   463 is  HOL extended with a definitional development of the real and complex

   464 numbers.  Base your theory upon theory

   465 \thydx{Complex_Main}, not the usual \isa{Main}.%

   466 \index{real numbers|)}\index{*real (type)|)}

   467 Launch Isabelle using the command

   468 \begin{verbatim}

   469 Isabelle -l HOL-Complex

   470 \end{verbatim}

   471 \end{warn}

   472

   473 Also available in HOL-Complex is the

   474 theory \isa{Hyperreal}, which define the type \tydx{hypreal} of

   475 \rmindex{non-standard reals}.  These

   476 \textbf{hyperreals} include infinitesimals, which represent infinitely

   477 small and infinitely large quantities; they facilitate proofs

   478 about limits, differentiation and integration~\cite{fleuriot-jcm}.  The

   479 development defines an infinitely large number, \isa{omega} and an

   480 infinitely small positive number, \isa{epsilon}.  The

   481 relation $x\approx y$ means $x$ is infinitely close to~$y$.''

   482 Theory \isa{Hyperreal} also defines transcendental functions such as sine,

   483 cosine, exponential and logarithm --- even the versions for type

   484 \isa{real}, because they are defined using nonstandard limits.%

   485 \index{numbers|)}