doc-src/TutorialI/Misc/natsum.thy
 author nipkow Wed Dec 13 09:39:53 2000 +0100 (2000-12-13) changeset 10654 458068404143 parent 10608 620647438780 child 10788 ea48dd8b0232 permissions -rw-r--r--
*** empty log message ***
 nipkow@8745  1 (*<*)  nipkow@8745  2 theory natsum = Main:;  nipkow@8745  3 (*>*)  nipkow@8745  4 text{*\noindent  nipkow@9792  5 In particular, there are @{text"case"}-expressions, for example  nipkow@9541  6 @{term[display]"case n of 0 => 0 | Suc m => m"}  nipkow@8745  7 primitive recursion, for example  nipkow@8745  8 *}  nipkow@8745  9 nipkow@10538  10 consts sum :: "nat \ nat";  nipkow@8745  11 primrec "sum 0 = 0"  nipkow@8745  12  "sum (Suc n) = Suc n + sum n";  nipkow@8745  13 nipkow@8745  14 text{*\noindent  nipkow@8745  15 and induction, for example  nipkow@8745  16 *}  nipkow@8745  17 nipkow@8745  18 lemma "sum n + sum n = n*(Suc n)";  nipkow@8745  19 apply(induct_tac n);  nipkow@10171  20 apply(auto);  nipkow@10171  21 done  nipkow@8745  22 nipkow@10538  23 text{*\newcommand{\mystar}{*%  nipkow@10538  24 }  nipkow@10538  25 The usual arithmetic operations \ttindexboldpos{+}{$HOL2arithfun},  nipkow@10538  26 \ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{\mystar}{$HOL2arithfun},  nipkow@10538  27 \isaindexbold{div}, \isaindexbold{mod}, \isaindexbold{min} and  nipkow@10538  28 \isaindexbold{max} are predefined, as are the relations  nipkow@10538  29 \indexboldpos{\isasymle}{$HOL2arithrel} and  nipkow@10654  30 \ttindexboldpos{<}{$HOL2arithrel}. As usual, @{prop"m-n = 0"} if  nipkow@10654  31 @{prop"m \ m < n; m < n+1 \ \ m = n"  nipkow@10538  63 (*<*)by(auto)(*>*)  nipkow@10538  64 nipkow@10538  65 text{*\noindent  nipkow@10538  66 is proved automatically. The main restriction is that only addition is taken  nipkow@10538  67 into account; other arithmetic operations and quantified formulae are ignored.  nipkow@10538  68 nipkow@10538  69 For more complex goals, there is the special method \isaindexbold{arith}  nipkow@10538  70 (which attacks the first subgoal). It proves arithmetic goals involving the  nipkow@10538  71 usual logical connectives (@{text"\"}, @{text"\"}, @{text"\"},  nipkow@10538  72 @{text"\"}), the relations @{text"\"} and @{text"<"}, and the operations  nipkow@10654  73 @{text"+"}, @{text"-"}, @{term min} and @{term max}. Technically, this is  nipkow@10654  74 known as the class of (quantifier free) \bfindex{linear arithmetic} formulae.  nipkow@10654  75 For example,  nipkow@10538  76 *}  nipkow@10538  77 nipkow@10538  78 lemma "min i (max j (k*k)) = max (min (k*k) i) (min i (j::nat))";  nipkow@10538  79 apply(arith)  nipkow@10538  80 (*<*)done(*>*)  nipkow@10538  81 nipkow@10538  82 text{*\noindent  nipkow@10538  83 succeeds because @{term"k*k"} can be treated as atomic. In contrast,  nipkow@10538  84 *}  nipkow@10538  85 nipkow@10538  86 lemma "n*n = n \ n=0 \ n=1"  nipkow@10538  87 (*<*)oops(*>*)  nipkow@10538  88 nipkow@10538  89 text{*\noindent  nipkow@10538  90 is not even proved by @{text arith} because the proof relies essentially  nipkow@10538  91 on properties of multiplication.  nipkow@10538  92 nipkow@10538  93 \begin{warn}  nipkow@10538  94  The running time of @{text arith} is exponential in the number of occurrences  nipkow@10538  95  of \ttindexboldpos{-}{$HOL2arithfun}, \isaindexbold{min} and  nipkow@10538  96  \isaindexbold{max} because they are first eliminated by case distinctions.  nipkow@10538  97 nipkow@10654  98  \isa{arith} is incomplete even for the restricted class of  nipkow@10654  99  linear arithmetic formulae. If divisibility plays a  nipkow@10538  100  role, it may fail to prove a valid formula, for example  nipkow@10538  101  @{prop"m+m \ n+n+1"}. Fortunately, such examples are rare in practice.  nipkow@10538  102 \end{warn}  nipkow@10538  103 *}  nipkow@10538  104 nipkow@8745  105 (*<*)  nipkow@8745  106 end  nipkow@8745  107 (*>*)