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