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