src/HOL/Isar_Examples/Summation.thy
 author haftmann Wed Jun 30 16:46:44 2010 +0200 (2010-06-30) changeset 37659 14cabf5fa710 parent 33026 8f35633c4922 child 37671 fa53d267dab3 permissions -rw-r--r--
more speaking names
 wenzelm@33026  1 (* Title: HOL/Isar_Examples/Summation.thy  wenzelm@7443  2  Author: Markus Wenzel  wenzelm@7443  3 *)  wenzelm@7443  4 wenzelm@10007  5 header {* Summing natural numbers *}  wenzelm@7443  6 nipkow@15561  7 theory Summation  nipkow@15561  8 imports Main  nipkow@15561  9 begin  nipkow@15561  10 wenzelm@7968  11 text_raw {*  wenzelm@7968  12  \footnote{This example is somewhat reminiscent of the  wenzelm@7968  13  \url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, which is  wenzelm@7968  14  discussed in \cite{isabelle-ref} in the context of permutative  wenzelm@7968  15  rewrite rules and ordered rewriting.}  wenzelm@10007  16 *}  wenzelm@7968  17 wenzelm@7968  18 text {*  wenzelm@7968  19  Subsequently, we prove some summation laws of natural numbers  wenzelm@7982  20  (including odds, squares, and cubes). These examples demonstrate how  wenzelm@7968  21  plain natural deduction (including induction) may be combined with  wenzelm@7968  22  calculational proof.  wenzelm@10007  23 *}  wenzelm@7968  24 wenzelm@7761  25 wenzelm@10007  26 subsection {* Summation laws *}  wenzelm@7443  27 wenzelm@7968  28 text {*  wenzelm@7968  29  The sum of natural numbers $0 + \cdots + n$ equals $n \times (n +  wenzelm@7982  30  1)/2$. Avoiding formal reasoning about division we prove this  wenzelm@7982  31  equation multiplied by $2$.  wenzelm@10007  32 *}  wenzelm@7800  33 wenzelm@7800  34 theorem sum_of_naturals:  nipkow@15561  35  "2 * (\i::nat=0..n. i) = n * (n + 1)"  wenzelm@10007  36  (is "?P n" is "?S n = _")  wenzelm@10007  37 proof (induct n)  wenzelm@10007  38  show "?P 0" by simp  wenzelm@10146  39 next  wenzelm@11704  40  fix n have "?S (n + 1) = ?S n + 2 * (n + 1)" by simp  wenzelm@10007  41  also assume "?S n = n * (n + 1)"  wenzelm@11704  42  also have "... + 2 * (n + 1) = (n + 1) * (n + 2)" by simp  wenzelm@10007  43  finally show "?P (Suc n)" by simp  wenzelm@10007  44 qed  wenzelm@7443  45 wenzelm@7968  46 text {*  wenzelm@7968  47  The above proof is a typical instance of mathematical induction. The  wenzelm@7968  48  main statement is viewed as some $\var{P} \ap n$ that is split by the  wenzelm@7968  49  induction method into base case $\var{P} \ap 0$, and step case  wenzelm@7982  50  $\var{P} \ap n \Impl \var{P} \ap (\idt{Suc} \ap n)$ for arbitrary $n$.  wenzelm@7968  51 wenzelm@7968  52  The step case is established by a short calculation in forward  wenzelm@7968  53  manner. Starting from the left-hand side $\var{S} \ap (n + 1)$ of  wenzelm@7982  54  the thesis, the final result is achieved by transformations involving  wenzelm@7982  55  basic arithmetic reasoning (using the Simplifier). The main point is  wenzelm@7982  56  where the induction hypothesis $\var{S} \ap n = n \times (n + 1)$ is  wenzelm@7982  57  introduced in order to replace a certain subterm. So the  wenzelm@7968  58  transitivity'' rule involved here is actual \emph{substitution}.  wenzelm@7968  59  Also note how the occurrence of \dots'' in the subsequent step  wenzelm@7982  60  documents the position where the right-hand side of the hypothesis  wenzelm@7968  61  got filled in.  wenzelm@7968  62 wenzelm@7968  63  \medskip A further notable point here is integration of calculations  wenzelm@7982  64  with plain natural deduction. This works so well in Isar for two  wenzelm@7982  65  reasons.  wenzelm@7968  66  \begin{enumerate}  wenzelm@7968  67 wenzelm@7968  68  \item Facts involved in \isakeyword{also}~/ \isakeyword{finally}  wenzelm@7968  69  calculational chains may be just anything. There is nothing special  wenzelm@7968  70  about \isakeyword{have}, so the natural deduction element  wenzelm@7968  71  \isakeyword{assume} works just as well.  wenzelm@7968  72 wenzelm@7968  73  \item There are two \emph{separate} primitives for building natural  wenzelm@7968  74  deduction contexts: \isakeyword{fix}~$x$ and \isakeyword{assume}~$A$.  wenzelm@7982  75  Thus it is possible to start reasoning with some new arbitrary, but  wenzelm@7982  76  fixed'' elements before bringing in the actual assumption. In  wenzelm@7982  77  contrast, natural deduction is occasionally formalized with basic  wenzelm@7982  78  context elements of the form $x:A$ instead.  wenzelm@7968  79 wenzelm@7968  80  \end{enumerate}  wenzelm@10007  81 *}  wenzelm@7968  82 wenzelm@7968  83 text {*  wenzelm@7982  84  \medskip We derive further summation laws for odds, squares, and  wenzelm@7982  85  cubes as follows. The basic technique of induction plus calculation  wenzelm@7982  86  is the same as before.  wenzelm@10007  87 *}  wenzelm@7968  88 wenzelm@7800  89 theorem sum_of_odds:  nipkow@15561  90  "(\i::nat=0..i::nat=0..n. i^Suc (Suc 0)) = n * (n + 1) * (2 * n + 1)"  wenzelm@10007  111  (is "?P n" is "?S n = _")  wenzelm@10007  112 proof (induct n)  wenzelm@10007  113  show "?P 0" by simp  wenzelm@10146  114 next  wenzelm@18193  115  fix n have "?S (n + 1) = ?S n + 6 * (n + 1)^Suc (Suc 0)"  wenzelm@18193  116  by (simp add: distrib)  wenzelm@11704  117  also assume "?S n = n * (n + 1) * (2 * n + 1)"  wenzelm@11704  118  also have "... + 6 * (n + 1)^Suc (Suc 0) =  wenzelm@11704  119  (n + 1) * (n + 2) * (2 * (n + 1) + 1)" by (simp add: distrib)  wenzelm@10007  120  finally show "?P (Suc n)" by simp  wenzelm@10007  121 qed  wenzelm@7443  122 wenzelm@7800  123 theorem sum_of_cubes:  nipkow@15561  124  "4 * (\i::nat=0..n. i^3) = (n * (n + 1))^Suc (Suc 0)"  wenzelm@10007  125  (is "?P n" is "?S n = _")  wenzelm@10007  126 proof (induct n)  wenzelm@10007  127  show "?P 0" by (simp add: power_eq_if)  wenzelm@10146  128 next  wenzelm@11704  129  fix n have "?S (n + 1) = ?S n + 4 * (n + 1)^3"  wenzelm@10007  130  by (simp add: power_eq_if distrib)  wenzelm@11701  131  also assume "?S n = (n * (n + 1))^Suc (Suc 0)"  wenzelm@11704  132  also have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^Suc (Suc 0)"  wenzelm@10007  133  by (simp add: power_eq_if distrib)  wenzelm@10007  134  finally show "?P (Suc n)" by simp  wenzelm@10007  135 qed  wenzelm@7443  136 wenzelm@7968  137 text {*  wenzelm@7968  138  Comparing these examples with the tactic script version  wenzelm@7968  139  \url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, we note  wenzelm@7982  140  an important difference of how induction vs.\ simplification is  wenzelm@7968  141  applied. While \cite[\S10]{isabelle-ref} advises for these examples  wenzelm@7968  142  that induction should not be applied until the goal is in the  wenzelm@7968  143  simplest form'' this would be a very bad idea in our setting.  wenzelm@7968  144 wenzelm@7968  145  Simplification normalizes all arithmetic expressions involved,  wenzelm@7982  146  producing huge intermediate goals. With applying induction  wenzelm@7982  147  afterwards, the Isar proof text would have to reflect the emerging  wenzelm@7982  148  configuration by appropriate sub-proofs. This would result in badly  wenzelm@7982  149  structured, low-level technical reasoning, without any good idea of  wenzelm@7982  150  the actual point.  wenzelm@7968  151 wenzelm@7968  152  \medskip As a general rule of good proof style, automatic methods  wenzelm@7982  153  such as $\idt{simp}$ or $\idt{auto}$ should normally be never used as  wenzelm@7968  154  initial proof methods, but only as terminal ones, solving certain  wenzelm@7968  155  goals completely.  wenzelm@10007  156 *}  wenzelm@7968  157 wenzelm@10007  158 end