doc-src/TutorialI/Types/numerics.tex
 author nipkow Fri, 16 Feb 2001 08:10:28 +0100 changeset 11148 79aa2932b2d7 parent 10983 59961d32b1ae child 11161 166f7d87b37f permissions -rw-r--r--
*** empty log message ***
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
 10794 65d18005d802 revisions especially concerning the reals paulson parents: 10779 diff changeset  1 % $Id$  65d18005d802 revisions especially concerning the reals paulson parents: 10779 diff changeset  2 Until now, our numerical have used the type of \textbf{natural numbers},  10594 6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  3 \isa{nat}. This is a recursive datatype generated by the constructors  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  4 zero and successor, so it works well with inductive proofs and primitive  10794 65d18005d802 revisions especially concerning the reals paulson parents: 10779 diff changeset  5 recursive function definitions. Isabelle/HOL also provides the type  65d18005d802 revisions especially concerning the reals paulson parents: 10779 diff changeset  6 \isa{int} of \textbf{integers}, which lack induction but support true  10881 03f06372230b abs and other small changes paulson parents: 10794 diff changeset  7 subtraction. The logic HOL-Real also has the type \isa{real} of real  10777 a5a6255748c3 initial material on the Reals paulson parents: 10654 diff changeset  8 numbers. Isabelle has no subtyping, so the numeric types are distinct and  10978 5eebea8f359f *** empty log message *** nipkow parents: 10881 diff changeset  9 there are functions to convert between them. Fortunately most numeric  5eebea8f359f *** empty log message *** nipkow parents: 10881 diff changeset  10 operations are overloaded: the same symbol can be used at all numeric types.  5eebea8f359f *** empty log message *** nipkow parents: 10881 diff changeset  11 Table~\ref{tab:overloading} in the appendix shows the most important operations,  5eebea8f359f *** empty log message *** nipkow parents: 10881 diff changeset  12 together with the priorities of the infix symbols.  10594 6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  13 6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  14 The integers are preferable to the natural numbers for reasoning about  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  15 complicated arithmetic expressions. For example, a termination proof  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  16 typically involves an integer metric that is shown to decrease at each  10794 65d18005d802 revisions especially concerning the reals paulson parents: 10779 diff changeset  17 loop iteration. Even if the metric cannot become negative, proofs  65d18005d802 revisions especially concerning the reals paulson parents: 10779 diff changeset  18 may be easier if you use the integers instead of the natural  10594 6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  19 numbers.  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  20 6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  21 Many theorems involving numeric types can be proved automatically by  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  22 Isabelle's arithmetic decision procedure, the method  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  23 \isa{arith}. Linear arithmetic comprises addition, subtraction  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  24 and multiplication by constant factors; subterms involving other operators  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  25 are regarded as variables. The procedure can be slow, especially if the  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  26 subgoal to be proved involves subtraction over type \isa{nat}, which  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  27 causes case splits.  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  28 6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  29 The simplifier reduces arithmetic expressions in other  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  30 ways, such as dividing through by common factors. For problems that lie  10881 03f06372230b abs and other small changes paulson parents: 10794 diff changeset  31 outside the scope of automation, HOL provides hundreds of  10594 6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  32 theorems about multiplication, division, etc., that can be brought to  10881 03f06372230b abs and other small changes paulson parents: 10794 diff changeset  33 bear. You can locate them using Proof General's Find  03f06372230b abs and other small changes paulson parents: 10794 diff changeset  34 button. A few lemmas are given below to show what  10794 65d18005d802 revisions especially concerning the reals paulson parents: 10779 diff changeset  35 is available.  10594 6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  36 6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  37 \subsection{Numeric Literals}  10779 b0d961105f46 label! nipkow parents: 10777 diff changeset  38 \label{sec:numerals}  10594 6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  39 6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  40 Literals are available for the types of natural numbers, integers  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  41 and reals and denote integer values of arbitrary size.  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  42 They begin  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  43 with a number sign (\isa{\#}), have an optional minus sign (\isa{-}) and  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  44 then one or more decimal digits. Examples are \isa{\#0}, \isa{\#-3}  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  45 and \isa{\#441223334678}.  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  46 6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  47 Literals look like constants, but they abbreviate  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  48 terms, representing the number in a two's complement binary notation.  10794 65d18005d802 revisions especially concerning the reals paulson parents: 10779 diff changeset  49 Isabelle performs arithmetic on literals by rewriting rather  10594 6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  50 than using the hardware arithmetic. In most cases arithmetic  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  51 is fast enough, even for large numbers. The arithmetic operations  10794 65d18005d802 revisions especially concerning the reals paulson parents: 10779 diff changeset  52 provided for literals include addition, subtraction, multiplication,  65d18005d802 revisions especially concerning the reals paulson parents: 10779 diff changeset  53 integer division and remainder. Fractions of literals (expressed using  65d18005d802 revisions especially concerning the reals paulson parents: 10779 diff changeset  54 division) are reduced to lowest terms.  10594 6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  55 10794 65d18005d802 revisions especially concerning the reals paulson parents: 10779 diff changeset  56 \begin{warn}  65d18005d802 revisions especially concerning the reals paulson parents: 10779 diff changeset  57 The arithmetic operators are  10594 6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  58 overloaded, so you must be careful to ensure that each numeric  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  59 expression refers to a specific type, if necessary by inserting  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  60 type constraints. Here is an example of what can go wrong:  10794 65d18005d802 revisions especially concerning the reals paulson parents: 10779 diff changeset  61 \par  10594 6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  62 \begin{isabelle}  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  63 \isacommand{lemma}\ "\#2\ *\ m\ =\ m\ +\ m"  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  64 \end{isabelle}  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  65 %  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  66 Carefully observe how Isabelle displays the subgoal:  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  67 \begin{isabelle}  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  68 \ 1.\ (\#2::'a)\ *\ m\ =\ m\ +\ m  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  69 \end{isabelle}  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  70 The type \isa{'a} given for the literal \isa{\#2} warns us that no numeric  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  71 type has been specified. The problem is underspecified. Given a type  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  72 constraint such as \isa{nat}, \isa{int} or \isa{real}, it becomes trivial.  10794 65d18005d802 revisions especially concerning the reals paulson parents: 10779 diff changeset  73 \end{warn}  65d18005d802 revisions especially concerning the reals paulson parents: 10779 diff changeset  74 10881 03f06372230b abs and other small changes paulson parents: 10794 diff changeset  75 \begin{warn}  03f06372230b abs and other small changes paulson parents: 10794 diff changeset  76 Numeric literals are not constructors and therefore must not be used in  03f06372230b abs and other small changes paulson parents: 10794 diff changeset  77 patterns. For example, this declaration is rejected:  03f06372230b abs and other small changes paulson parents: 10794 diff changeset  78 \begin{isabelle}  03f06372230b abs and other small changes paulson parents: 10794 diff changeset  79 \isacommand{recdef}\ h\ "\isacharbraceleft \isacharbraceright "\isanewline  11148 79aa2932b2d7 *** empty log message *** nipkow parents: 10983 diff changeset  80 "h\ \#3\ =\ \#2"\isanewline  79aa2932b2d7 *** empty log message *** nipkow parents: 10983 diff changeset  81 "h\ i\ \ =\ i"  10881 03f06372230b abs and other small changes paulson parents: 10794 diff changeset  82 \end{isabelle}  03f06372230b abs and other small changes paulson parents: 10794 diff changeset  83 03f06372230b abs and other small changes paulson parents: 10794 diff changeset  84 You should use a conditional expression instead:  03f06372230b abs and other small changes paulson parents: 10794 diff changeset  85 \begin{isabelle}  03f06372230b abs and other small changes paulson parents: 10794 diff changeset  86 "h\ i\ =\ (if\ i\ =\ \#3\ then\ \#2\ else\ i)"  03f06372230b abs and other small changes paulson parents: 10794 diff changeset  87 \end{isabelle}  03f06372230b abs and other small changes paulson parents: 10794 diff changeset  88 \end{warn}  03f06372230b abs and other small changes paulson parents: 10794 diff changeset  89 10594 6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  90 6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  91 6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  92 \subsection{The type of natural numbers, {\tt\slshape nat}}  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  93 6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  94 This type requires no introduction: we have been using it from the  10794 65d18005d802 revisions especially concerning the reals paulson parents: 10779 diff changeset  95 beginning. Hundreds of theorems about the natural numbers are  10594 6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  96 proved in the theories \isa{Nat}, \isa{NatArith} and \isa{Divides}. Only  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  97 in exceptional circumstances should you resort to induction.  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  98 6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  99 \subsubsection{Literals}  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  100 The notational options for the natural numbers can be confusing. The  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  101 constant \isa{0} is overloaded to serve as the neutral value  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  102 in a variety of additive types. The symbols \isa{1} and \isa{2} are  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  103 not constants but abbreviations for \isa{Suc 0} and \isa{Suc(Suc 0)},  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  104 respectively. The literals \isa{\#0}, \isa{\#1} and \isa{\#2} are  10794 65d18005d802 revisions especially concerning the reals paulson parents: 10779 diff changeset  105 syntactically different from \isa{0}, \isa{1} and \isa{2}. You will  10594 6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  106 sometimes prefer one notation to the other. Literals are obviously  10794 65d18005d802 revisions especially concerning the reals paulson parents: 10779 diff changeset  107 necessary to express large values, while \isa{0} and \isa{Suc} are needed  65d18005d802 revisions especially concerning the reals paulson parents: 10779 diff changeset  108 in order to match many theorems, including the rewrite rules for primitive  65d18005d802 revisions especially concerning the reals paulson parents: 10779 diff changeset  109 recursive functions. The following default simplification rules replace  65d18005d802 revisions especially concerning the reals paulson parents: 10779 diff changeset  110 small literals by zero and successor:  10594 6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  111 \begin{isabelle}  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  112 \#0\ =\ 0  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  113 \rulename{numeral_0_eq_0}\isanewline  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  114 \#1\ =\ 1  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  115 \rulename{numeral_1_eq_1}\isanewline  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  116 \#2\ +\ n\ =\ Suc\ (Suc\ n)  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  117 \rulename{add_2_eq_Suc}\isanewline  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  118 n\ +\ \#2\ =\ Suc\ (Suc\ n)  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  119 \rulename{add_2_eq_Suc'}  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  120 \end{isabelle}  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  121 In special circumstances, you may wish to remove or reorient  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  122 these rules.  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  123 6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  124 \subsubsection{Typical lemmas}  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  125 Inequalities involving addition and subtraction alone can be proved  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  126 automatically. Lemmas such as these can be used to prove inequalities  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  127 involving multiplication and division:  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  128 \begin{isabelle}  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  129 \isasymlbrakk i\ \isasymle \ j;\ k\ \isasymle \ l\isasymrbrakk \ \isasymLongrightarrow \ i\ *\ k\ \isasymle \ j\ *\ l%  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  130 \rulename{mult_le_mono}\isanewline  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  131 \isasymlbrakk i\ <\ j;\ 0\ <\ k\isasymrbrakk \ \isasymLongrightarrow \ i\  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  132 *\ k\ <\ j\ *\ k%  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  133 \rulename{mult_less_mono1}\isanewline  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  134 m\ \isasymle \ n\ \isasymLongrightarrow \ m\ div\ k\ \isasymle \ n\ div\ k%  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  135 \rulename{div_le_mono}  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  136 \end{isabelle}  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  137 %  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  138 Various distributive laws concerning multiplication are available:  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  139 \begin{isabelle}  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  140 (m\ +\ n)\ *\ k\ =\ m\ *\ k\ +\ n\ *\ k%  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  141 \rulename{add_mult_distrib}\isanewline  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  142 (m\ -\ n)\ *\ k\ =\ m\ *\ k\ -\ n\ *\ k%  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  143 \rulename{diff_mult_distrib}\isanewline  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  144 (m\ mod\ n)\ *\ k\ =\ (m\ *\ k)\ mod\ (n\ *\ k)  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  145 \rulename{mod_mult_distrib}  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  146 \end{isabelle}  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  147 6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  148 \subsubsection{Division}  10881 03f06372230b abs and other small changes paulson parents: 10794 diff changeset  149 The infix operators \isa{div} and \isa{mod} are overloaded.  03f06372230b abs and other small changes paulson parents: 10794 diff changeset  150 Isabelle/HOL provides the basic facts about quotient and remainder  03f06372230b abs and other small changes paulson parents: 10794 diff changeset  151 on the natural numbers:  10594 6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  152 \begin{isabelle}  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  153 m\ mod\ n\ =\ (if\ m\ <\ n\ then\ m\ else\ (m\ -\ n)\ mod\ n)  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  154 \rulename{mod_if}\isanewline  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  155 m\ div\ n\ *\ n\ +\ m\ mod\ n\ =\ m%  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  156 \rulename{mod_div_equality}  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  157 \end{isabelle}  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  158 6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  159 Many less obvious facts about quotient and remainder are also provided.  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  160 Here is a selection:  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  161 \begin{isabelle}  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  162 a\ *\ b\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c%  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  163 \rulename{div_mult1_eq}\isanewline  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  164 a\ *\ b\ mod\ c\ =\ a\ *\ (b\ mod\ c)\ mod\ c%  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  165 \rulename{mod_mult1_eq}\isanewline  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  166 a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  167 \rulename{div_mult2_eq}\isanewline  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  168 a\ mod\ (b*c)\ =\ b * (a\ div\ b\ mod\ c)\ +\ a\ mod\ b%  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  169 \rulename{mod_mult2_eq}\isanewline  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  170 0\ <\ c\ \isasymLongrightarrow \ (c\ *\ a)\ div\ (c\ *\ b)\ =\ a\ div\ b%  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  171 \rulename{div_mult_mult1}  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  172 \end{isabelle}  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  173 6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  174 Surprisingly few of these results depend upon the  10794 65d18005d802 revisions especially concerning the reals paulson parents: 10779 diff changeset  175 divisors' being nonzero. That is because division by  65d18005d802 revisions especially concerning the reals paulson parents: 10779 diff changeset  176 zero yields zero:  10594 6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  177 \begin{isabelle}  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  178 a\ div\ 0\ =\ 0  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  179 \rulename{DIVISION_BY_ZERO_DIV}\isanewline  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  180 a\ mod\ 0\ =\ a%  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  181 \rulename{DIVISION_BY_ZERO_MOD}  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  182 \end{isabelle}  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  183 As a concession to convention, these equations are not installed as default  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  184 simplification rules but are merely used to remove nonzero-divisor  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  185 hypotheses by case analysis. In \isa{div_mult_mult1} above, one of  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  186 the two divisors (namely~\isa{c}) must be still be nonzero.  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  187 6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  188 The \textbf{divides} relation has the standard definition, which  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  189 is overloaded over all numeric types:  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  190 \begin{isabelle}  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  191 m\ dvd\ n\ \isasymequiv\ {\isasymexists}k.\ n\ =\ m\ *\ k  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  192 \rulename{dvd_def}  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  193 \end{isabelle}  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  194 %  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  195 Section~\ref{sec:proving-euclid} discusses proofs involving this  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  196 relation. Here are some of the facts proved about it:  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  197 \begin{isabelle}  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  198 \isasymlbrakk m\ dvd\ n;\ n\ dvd\ m\isasymrbrakk \ \isasymLongrightarrow \ m\ =\ n%  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  199 \rulename{dvd_anti_sym}\isanewline  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  200 \isasymlbrakk k\ dvd\ m;\ k\ dvd\ n\isasymrbrakk \ \isasymLongrightarrow \ k\ dvd\ (m\ +\ n)  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  201 \rulename{dvd_add}  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  202 \end{isabelle}  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  203 6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  204 \subsubsection{Simplifier tricks}  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  205 The rule \isa{diff_mult_distrib} shown above is one of the few facts  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  206 about \isa{m\ -\ n} that is not subject to  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  207 the condition \isa{n\ \isasymle \ m}. Natural number subtraction has few  10794 65d18005d802 revisions especially concerning the reals paulson parents: 10779 diff changeset  208 nice properties; often you should remove it by simplifying with this split  65d18005d802 revisions especially concerning the reals paulson parents: 10779 diff changeset  209 rule:  10594 6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  210 \begin{isabelle}  6330bc4b6fe4 nat and int sections but no real paulson parents: diff changeset  211 `P(a-b)\ =\ ((a