doc-src/TutorialI/Types/numerics.tex
author paulson
Thu May 08 12:52:15 2003 +0200 (2003-05-08)
changeset 13979 4c3a638828b9
parent 13750 b5cd10cb106b
child 13983 afc0dadddaa4
permissions -rw-r--r--
HOL-Complex
     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.  
    32 
    33 The simplifier reduces arithmetic expressions in other
    34 ways, such as dividing through by common factors.  For problems that lie
    35 outside the scope of automation, HOL provides hundreds of
    36 theorems about multiplication, division, etc., that can be brought to
    37 bear.  You can locate them using Proof General's Find
    38 button.  A few lemmas are given below to show what
    39 is available.
    40 
    41 \subsection{Numeric Literals}
    42 \label{sec:numerals}
    43 
    44 \index{numeric literals|(}%
    45 The constants \cdx{0} and \cdx{1} are overloaded.  They denote zero and one,
    46 respectively, for all numeric types.  Other values are expressed by numeric
    47 literals, which consist of one or more decimal digits optionally preceeded by
    48 a minus sign (\isa{-}).  Examples are \isa{2}, \isa{-3} and
    49 \isa{441223334678}.  Literals are available for the types of natural numbers,
    50 integers and reals; they denote integer values of arbitrary size.
    51 
    52 Literals look like constants, but they abbreviate 
    53 terms representing the number in a two's complement binary notation. 
    54 Isabelle performs arithmetic on literals by rewriting rather 
    55 than using the hardware arithmetic. In most cases arithmetic 
    56 is fast enough, even for large numbers. The arithmetic operations 
    57 provided for literals include addition, subtraction, multiplication, 
    58 integer division and remainder.  Fractions of literals (expressed using
    59 division) are reduced to lowest terms.
    60 
    61 \begin{warn}\index{overloading!and arithmetic}
    62 The arithmetic operators are 
    63 overloaded, so you must be careful to ensure that each numeric 
    64 expression refers to a specific type, if necessary by inserting 
    65 type constraints.  Here is an example of what can go wrong:
    66 \par
    67 \begin{isabelle}
    68 \isacommand{lemma}\ "2\ *\ m\ =\ m\ +\ m"
    69 \end{isabelle}
    70 %
    71 Carefully observe how Isabelle displays the subgoal:
    72 \begin{isabelle}
    73 \ 1.\ (2::'a)\ *\ m\ =\ m\ +\ m
    74 \end{isabelle}
    75 The type \isa{'a} given for the literal \isa{2} warns us that no numeric
    76 type has been specified.  The problem is underspecified.  Given a type
    77 constraint such as \isa{nat}, \isa{int} or \isa{real}, it becomes trivial.
    78 \end{warn}
    79 
    80 \begin{warn}
    81 \index{recdef@\isacommand {recdef} (command)!and numeric literals}  
    82 Numeric literals are not constructors and therefore
    83 must not be used in patterns.  For example, this declaration is
    84 rejected:
    85 \begin{isabelle}
    86 \isacommand{recdef}\ h\ "\isacharbraceleft \isacharbraceright "\isanewline
    87 "h\ 3\ =\ 2"\isanewline
    88 "h\ i\ \ =\ i"
    89 \end{isabelle}
    90 
    91 You should use a conditional expression instead:
    92 \begin{isabelle}
    93 "h\ i\ =\ (if\ i\ =\ 3\ then\ 2\ else\ i)"
    94 \end{isabelle}
    95 \index{numeric literals|)}
    96 \end{warn}
    97 
    98 
    99 
   100 \subsection{The Type of Natural Numbers, {\tt\slshape nat}}
   101 
   102 \index{natural numbers|(}\index{*nat (type)|(}%
   103 This type requires no introduction: we have been using it from the
   104 beginning.  Hundreds of theorems about the natural numbers are
   105 proved in the theories \isa{Nat}, \isa{NatArith} and \isa{Divides}.  Only
   106 in exceptional circumstances should you resort to induction.
   107 
   108 \subsubsection{Literals}
   109 \index{numeric literals!for type \protect\isa{nat}}%
   110 The notational options for the natural  numbers are confusing.  Recall that an
   111 overloaded constant can be defined independently for each type; the definition
   112 of \cdx{1} for type \isa{nat} is
   113 \begin{isabelle}
   114 1\ \isasymequiv\ Suc\ 0
   115 \rulename{One_nat_def}
   116 \end{isabelle}
   117 This is installed as a simplification rule, so the simplifier will replace
   118 every occurrence of \isa{1::nat} by \isa{Suc\ 0}.  Literals are obviously
   119 better than nested \isa{Suc}s at expressing large values.  But many theorems,
   120 including the rewrite rules for primitive recursive functions, can only be
   121 applied to terms of the form \isa{Suc\ $n$}.
   122 
   123 The following default  simplification rules replace
   124 small literals by zero and successor: 
   125 \begin{isabelle}
   126 2\ +\ n\ =\ Suc\ (Suc\ n)
   127 \rulename{add_2_eq_Suc}\isanewline
   128 n\ +\ 2\ =\ Suc\ (Suc\ n)
   129 \rulename{add_2_eq_Suc'}
   130 \end{isabelle}
   131 It is less easy to transform \isa{100} into \isa{Suc\ 99} (for example), and
   132 the simplifier will normally reverse this transformation.  Novices should
   133 express natural numbers using \isa{0} and \isa{Suc} only.
   134 
   135 \subsubsection{Typical lemmas}
   136 Inequalities involving addition and subtraction alone can be proved
   137 automatically.  Lemmas such as these can be used to prove inequalities
   138 involving multiplication and division:
   139 \begin{isabelle}
   140 \isasymlbrakk i\ \isasymle \ j;\ k\ \isasymle \ l\isasymrbrakk \ \isasymLongrightarrow \ i\ *\ k\ \isasymle \ j\ *\ l%
   141 \rulename{mult_le_mono}\isanewline
   142 \isasymlbrakk i\ <\ j;\ 0\ <\ k\isasymrbrakk \ \isasymLongrightarrow \ i\
   143 *\ k\ <\ j\ *\ k%
   144 \rulename{mult_less_mono1}\isanewline
   145 m\ \isasymle \ n\ \isasymLongrightarrow \ m\ div\ k\ \isasymle \ n\ div\ k%
   146 \rulename{div_le_mono}
   147 \end{isabelle}
   148 %
   149 Various distributive laws concerning multiplication are available:
   150 \begin{isabelle}
   151 (m\ +\ n)\ *\ k\ =\ m\ *\ k\ +\ n\ *\ k%
   152 \rulenamedx{add_mult_distrib}\isanewline
   153 (m\ -\ n)\ *\ k\ =\ m\ *\ k\ -\ n\ *\ k%
   154 \rulenamedx{diff_mult_distrib}\isanewline
   155 (m\ mod\ n)\ *\ k\ =\ (m\ *\ k)\ mod\ (n\ *\ k)
   156 \rulenamedx{mod_mult_distrib}
   157 \end{isabelle}
   158 
   159 \subsubsection{Division}
   160 \index{division!for type \protect\isa{nat}}%
   161 The infix operators \isa{div} and \isa{mod} are overloaded.
   162 Isabelle/HOL provides the basic facts about quotient and remainder
   163 on the natural numbers:
   164 \begin{isabelle}
   165 m\ mod\ n\ =\ (if\ m\ <\ n\ then\ m\ else\ (m\ -\ n)\ mod\ n)
   166 \rulename{mod_if}\isanewline
   167 m\ div\ n\ *\ n\ +\ m\ mod\ n\ =\ m%
   168 \rulenamedx{mod_div_equality}
   169 \end{isabelle}
   170 
   171 Many less obvious facts about quotient and remainder are also provided. 
   172 Here is a selection:
   173 \begin{isabelle}
   174 a\ *\ b\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c%
   175 \rulename{div_mult1_eq}\isanewline
   176 a\ *\ b\ mod\ c\ =\ a\ *\ (b\ mod\ c)\ mod\ c%
   177 \rulename{mod_mult1_eq}\isanewline
   178 a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%
   179 \rulename{div_mult2_eq}\isanewline
   180 a\ mod\ (b*c)\ =\ b * (a\ div\ b\ mod\ c)\ +\ a\ mod\ b%
   181 \rulename{mod_mult2_eq}\isanewline
   182 0\ <\ c\ \isasymLongrightarrow \ (c\ *\ a)\ div\ (c\ *\ b)\ =\ a\ div\ b%
   183 \rulename{div_mult_mult1}
   184 \end{isabelle}
   185 
   186 Surprisingly few of these results depend upon the
   187 divisors' being nonzero.
   188 \index{division!by zero}%
   189 That is because division by
   190 zero yields zero:
   191 \begin{isabelle}
   192 a\ div\ 0\ =\ 0
   193 \rulename{DIVISION_BY_ZERO_DIV}\isanewline
   194 a\ mod\ 0\ =\ a%
   195 \rulename{DIVISION_BY_ZERO_MOD}
   196 \end{isabelle}
   197 As a concession to convention, these equations are not installed as default
   198 simplification rules.  In \isa{div_mult_mult1} above, one of
   199 the two divisors (namely~\isa{c}) must still be nonzero.
   200 
   201 The \textbf{divides} relation\index{divides relation}
   202 has the standard definition, which
   203 is overloaded over all numeric types: 
   204 \begin{isabelle}
   205 m\ dvd\ n\ \isasymequiv\ {\isasymexists}k.\ n\ =\ m\ *\ k
   206 \rulenamedx{dvd_def}
   207 \end{isabelle}
   208 %
   209 Section~\ref{sec:proving-euclid} discusses proofs involving this
   210 relation.  Here are some of the facts proved about it:
   211 \begin{isabelle}
   212 \isasymlbrakk m\ dvd\ n;\ n\ dvd\ m\isasymrbrakk \ \isasymLongrightarrow \ m\ =\ n%
   213 \rulenamedx{dvd_anti_sym}\isanewline
   214 \isasymlbrakk k\ dvd\ m;\ k\ dvd\ n\isasymrbrakk \ \isasymLongrightarrow \ k\ dvd\ (m\ +\ n)
   215 \rulenamedx{dvd_add}
   216 \end{isabelle}
   217 
   218 \subsubsection{Simplifier Tricks}
   219 The rule \isa{diff_mult_distrib} shown above is one of the few facts
   220 about \isa{m\ -\ n} that is not subject to
   221 the condition \isa{n\ \isasymle \  m}.  Natural number subtraction has few
   222 nice properties; often you should remove it by simplifying with this split
   223 rule:
   224 \begin{isabelle}
   225 P(a-b)\ =\ ((a<b\ \isasymlongrightarrow \ P\
   226 0)\ \isasymand \ (\isasymforall d.\ a\ =\ b+d\ \isasymlongrightarrow \ P\
   227 d))
   228 \rulename{nat_diff_split}
   229 \end{isabelle}
   230 For example, splitting helps to prove the following fact:
   231 \begin{isabelle}
   232 \isacommand{lemma}\ "(n\ -\ 2)\ *\ (n\ +\ 2)\ =\ n\ *\ n\ -\ (4::nat)"\isanewline
   233 \isacommand{apply}\ (simp\ split:\ nat_diff_split,\ clarify)\isanewline
   234 \ 1.\ \isasymAnd d.\ \isasymlbrakk n\ <\ 2;\ n\ *\ n\ =\ 4\ +\ d\isasymrbrakk \ \isasymLongrightarrow \ d\ =\ 0
   235 \end{isabelle}
   236 The result lies outside the scope of linear arithmetic, but
   237  it is easily found
   238 if we explicitly split \isa{n<2} as \isa{n=0} or \isa{n=1}:
   239 \begin{isabelle}
   240 \isacommand{apply}\ (subgoal_tac\ "n=0\ |\ n=1",\ force,\ arith)\isanewline
   241 \isacommand{done}
   242 \end{isabelle}
   243 
   244 Suppose that two expressions are equal, differing only in 
   245 associativity and commutativity of addition.  Simplifying with the
   246 following equations sorts the terms and groups them to the right, making
   247 the two expressions identical:
   248 \begin{isabelle}
   249 m\ +\ n\ +\ k\ =\ m\ +\ (n\ +\ k)
   250 \rulenamedx{add_assoc}\isanewline
   251 m\ +\ n\ =\ n\ +\ m%
   252 \rulenamedx{add_commute}\isanewline
   253 x\ +\ (y\ +\ z)\ =\ y\ +\ (x\
   254 +\ z)
   255 \rulename{add_left_commute}
   256 \end{isabelle}
   257 The name \isa{add_ac}\index{*add_ac (theorems)} 
   258 refers to the list of all three theorems; similarly
   259 there is \isa{mult_ac}.\index{*mult_ac (theorems)} 
   260 Here is an example of the sorting effect.  Start
   261 with this goal:
   262 \begin{isabelle}
   263 \ 1.\ Suc\ (i\ +\ j\ *\ l\ *\ k\ +\ m\ *\ n)\ =\
   264 f\ (n\ *\ m\ +\ i\ +\ k\ *\ j\ *\ l)
   265 \end{isabelle}
   266 %
   267 Simplify using  \isa{add_ac} and \isa{mult_ac}:
   268 \begin{isabelle}
   269 \isacommand{apply}\ (simp\ add:\ add_ac\ mult_ac)
   270 \end{isabelle}
   271 %
   272 Here is the resulting subgoal:
   273 \begin{isabelle}
   274 \ 1.\ Suc\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))\
   275 =\ f\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))%
   276 \end{isabelle}%
   277 \index{natural numbers|)}\index{*nat (type)|)}
   278 
   279 
   280 
   281 \subsection{The Type of Integers, {\tt\slshape int}}
   282 
   283 \index{integers|(}\index{*int (type)|(}%
   284 Reasoning methods resemble those for the natural numbers, but induction and
   285 the constant \isa{Suc} are not available.  HOL provides many lemmas
   286 for proving inequalities involving integer multiplication and division,
   287 similar to those shown above for type~\isa{nat}.  
   288 
   289 The \rmindex{absolute value} function \cdx{abs} is overloaded for the numeric types.
   290 It is defined for the integers; we have for example the obvious law
   291 \begin{isabelle}
   292 \isasymbar x\ *\ y\isasymbar \ =\ \isasymbar x\isasymbar \ *\ \isasymbar y\isasymbar 
   293 \rulename{abs_mult}
   294 \end{isabelle}
   295 
   296 \begin{warn}
   297 The absolute value bars shown above cannot be typed on a keyboard.  They
   298 can be entered using the X-symbol package.  In \textsc{ascii}, type \isa{abs x} to
   299 get \isa{\isasymbar x\isasymbar}.
   300 \end{warn}
   301 
   302 The \isa{arith} method can prove facts about \isa{abs} automatically, 
   303 though as it does so by case analysis, the cost can be exponential.
   304 \begin{isabelle}
   305 \isacommand{lemma}\ "abs\ (x+y)\ \isasymle \ abs\ x\ +\ abs\ (y\ ::\ int)"\isanewline
   306 \isacommand{by}\ arith
   307 \end{isabelle}
   308 
   309 Concerning simplifier tricks, we have no need to eliminate subtraction: it
   310 is well-behaved.  As with the natural numbers, the simplifier can sort the
   311 operands of sums and products.  The name \isa{zadd_ac}\index{*zadd_ac (theorems)}
   312 refers to the
   313 associativity and commutativity theorems for integer addition, while
   314 \isa{zmult_ac}\index{*zmult_ac (theorems)}
   315 has the analogous theorems for multiplication.  The
   316 prefix~\isa{z} in many theorem names recalls the use of $\mathbb{Z}$ to
   317 denote the set of integers.
   318 
   319 For division and remainder,\index{division!by negative numbers}
   320 the treatment of negative divisors follows
   321 mathematical practice: the sign of the remainder follows that
   322 of the divisor:
   323 \begin{isabelle}
   324 0\ <\ b\ \isasymLongrightarrow \ 0\ \isasymle \ a\ mod\ b%
   325 \rulename{pos_mod_sign}\isanewline
   326 0\ <\ b\ \isasymLongrightarrow \ a\ mod\ b\ <\ b%
   327 \rulename{pos_mod_bound}\isanewline
   328 b\ <\ 0\ \isasymLongrightarrow \ a\ mod\ b\ \isasymle \ 0
   329 \rulename{neg_mod_sign}\isanewline
   330 b\ <\ 0\ \isasymLongrightarrow \ b\ <\ a\ mod\ b%
   331 \rulename{neg_mod_bound}
   332 \end{isabelle}
   333 ML treats negative divisors in the same way, but most computer hardware
   334 treats signed operands using the same rules as for multiplication.
   335 Many facts about quotients and remainders are provided:
   336 \begin{isabelle}
   337 (a\ +\ b)\ div\ c\ =\isanewline
   338 a\ div\ c\ +\ b\ div\ c\ +\ (a\ mod\ c\ +\ b\ mod\ c)\ div\ c%
   339 \rulename{zdiv_zadd1_eq}
   340 \par\smallskip
   341 (a\ +\ b)\ mod\ c\ =\ (a\ mod\ c\ +\ b\ mod\ c)\ mod\ c%
   342 \rulename{zmod_zadd1_eq}
   343 \end{isabelle}
   344 
   345 \begin{isabelle}
   346 (a\ *\ b)\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c%
   347 \rulename{zdiv_zmult1_eq}\isanewline
   348 (a\ *\ b)\ mod\ c\ =\ a\ *\ (b\ mod\ c)\ mod\ c%
   349 \rulename{zmod_zmult1_eq}
   350 \end{isabelle}
   351 
   352 \begin{isabelle}
   353 0\ <\ c\ \isasymLongrightarrow \ a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%
   354 \rulename{zdiv_zmult2_eq}\isanewline
   355 0\ <\ c\ \isasymLongrightarrow \ a\ mod\ (b*c)\ =\ b*(a\ div\ b\ mod\
   356 c)\ +\ a\ mod\ b%
   357 \rulename{zmod_zmult2_eq}
   358 \end{isabelle}
   359 The last two differ from their natural number analogues by requiring
   360 \isa{c} to be positive.  Since division by zero yields zero, we could allow
   361 \isa{c} to be zero.  However, \isa{c} cannot be negative: a counterexample
   362 is
   363 $\isa{a} = 7$, $\isa{b} = 2$ and $\isa{c} = -3$, when the left-hand side of
   364 \isa{zdiv_zmult2_eq} is $-2$ while the right-hand side is~$-1$.%
   365 \index{integers|)}\index{*int (type)|)}
   366 
   367 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 $<$):
   368 \begin{isabelle}
   369 \isasymlbrakk k\ \isasymle \ i;\ P\ k;\ \isasymAnd i.\ \isasymlbrakk k\ \isasymle \ i;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i+1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%
   370 \rulename{int_ge_induct}\isanewline
   371 \isasymlbrakk k\ <\ i;\ P(k+1);\ \isasymAnd i.\ \isasymlbrakk k\ <\ i;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i+1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%
   372 \rulename{int_gr_induct}\isanewline
   373 \isasymlbrakk i\ \isasymle \ k;\ P\ k;\ \isasymAnd i.\ \isasymlbrakk i\ \isasymle \ k;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i-1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%
   374 \rulename{int_le_induct}\isanewline
   375 \isasymlbrakk i\ <\ k;\ P(k-1);\ \isasymAnd i.\ \isasymlbrakk i\ <\ k;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i-1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%
   376 \rulename{int_less_induct}
   377 \end{isabelle}
   378 
   379 
   380 \subsection{The Type of Real Numbers, {\tt\slshape real}}
   381 
   382 \index{real numbers|(}\index{*real (type)|(}%
   383 The real numbers enjoy two significant properties that the integers lack. 
   384 They are
   385 \textbf{dense}: between every two distinct real numbers there lies another.
   386 This property follows from the division laws, since if $x<y$ then between
   387 them lies $(x+y)/2$.  The second property is that they are
   388 \textbf{complete}: every set of reals that is bounded above has a least
   389 upper bound.  Completeness distinguishes the reals from the rationals, for
   390 which the set $\{x\mid x^2<2\}$ has no least upper bound.  (It could only be
   391 $\surd2$, which is irrational.)
   392 The formalization of completeness is complicated; rather than
   393 reproducing it here, we refer you to the theory \texttt{RComplete} in
   394 directory \texttt{Real}.
   395 Density, however, is trivial to express:
   396 \begin{isabelle}
   397 x\ <\ y\ \isasymLongrightarrow \ \isasymexists r.\ x\ <\ r\ \isasymand \ r\ <\ y%
   398 \rulename{real_dense}
   399 \end{isabelle}
   400 
   401 Here is a selection of rules about the division operator.  The following
   402 are installed as default simplification rules in order to express
   403 combinations of products and quotients as rational expressions:
   404 \begin{isabelle}
   405 x\ *\ (y\ /\ z)\ =\ x\ *\ y\ /\ z
   406 \rulename{real_times_divide1_eq}\isanewline
   407 y\ /\ z\ *\ x\ =\ y\ *\ x\ /\ z
   408 \rulename{real_times_divide2_eq}\isanewline
   409 x\ /\ (y\ /\ z)\ =\ x\ *\ z\ /\ y
   410 \rulename{real_divide_divide1_eq}\isanewline
   411 x\ /\ y\ /\ z\ =\ x\ /\ (y\ *\ z)
   412 \rulename{real_divide_divide2_eq}
   413 \end{isabelle}
   414 
   415 Signs are extracted from quotients in the hope that complementary terms can
   416 then be cancelled:
   417 \begin{isabelle}
   418 -\ x\ /\ y\ =\ -\ (x\ /\ y)
   419 \rulename{real_minus_divide_eq}\isanewline
   420 x\ /\ -\ y\ =\ -\ (x\ /\ y)
   421 \rulename{real_divide_minus_eq}
   422 \end{isabelle}
   423 
   424 The following distributive law is available, but it is not installed as a
   425 simplification rule.
   426 \begin{isabelle}
   427 (x\ +\ y)\ /\ z\ =\ x\ /\ z\ +\ y\ /\ z%
   428 \rulename{real_add_divide_distrib}
   429 \end{isabelle}
   430 
   431 As with the other numeric types, the simplifier can sort the operands of
   432 addition and multiplication.  The name \isa{real_add_ac} refers to the
   433 associativity and commutativity theorems for addition, while similarly
   434 \isa{real_mult_ac} contains those properties for multiplication. 
   435 
   436 The absolute value function \isa{abs} is
   437 defined for the reals, along with many theorems such as this one about
   438 exponentiation:
   439 \begin{isabelle}
   440 \isasymbar r\ \isacharcircum \ n\isasymbar\ =\ 
   441 \isasymbar r\isasymbar \ \isacharcircum \ n
   442 \rulename{realpow_abs}
   443 \end{isabelle}
   444 
   445 Numeric literals\index{numeric literals!for type \protect\isa{real}}
   446 for type \isa{real} have the same syntax as those for type
   447 \isa{int} and only express integral values.  Fractions expressed
   448 using the division operator are automatically simplified to lowest terms:
   449 \begin{isabelle}
   450 \ 1.\ P\ ((3\ /\ 4)\ *\ (8\ /\ 15))\isanewline
   451 \isacommand{apply} simp\isanewline
   452 \ 1.\ P\ (2\ /\ 5)
   453 \end{isabelle}
   454 Exponentiation can express floating-point values such as
   455 \isa{2 * 10\isacharcircum6}, but at present no special simplification
   456 is performed.
   457 
   458 
   459 \begin{warn}
   460 Type \isa{real} is only available in the logic HOL-Real, which
   461 is  HOL extended with a definitional development of the real
   462 numbers.  Base your theory upon theory
   463 \thydx{Real}, not the usual \isa{Main}.%
   464 \index{real numbers|)}\index{*real (type)|)}
   465 Launch Isabelle using the command 
   466 \begin{verbatim}
   467 Isabelle -l HOL-Real
   468 \end{verbatim}
   469 \end{warn}
   470 
   471 Also distributed with Isabelle is HOL-Hyperreal,
   472 whose theory \isa{Hyperreal} defines the type \tydx{hypreal} of 
   473 \rmindex{non-standard reals}.  These
   474 \textbf{hyperreals} include infinitesimals, which represent infinitely
   475 small and infinitely large quantities; they facilitate proofs
   476 about limits, differentiation and integration~\cite{fleuriot-jcm}.  The
   477 development defines an infinitely large number, \isa{omega} and an
   478 infinitely small positive number, \isa{epsilon}.  The 
   479 relation $x\approx y$ means ``$x$ is infinitely close to~$y$.''
   480 Theory \isa{Hyperreal} also defines transcendental functions such as sine,
   481 cosine, exponential and logarithm --- even the versions for type
   482 \isa{real}, because they are defined using nonstandard limits.%
   483 \index{numbers|)}