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