src/HOL/Isar_Examples/Summation.thy
 author nipkow Mon Jan 30 21:49:41 2012 +0100 (2012-01-30) changeset 46372 6fa9cdb8b850 parent 40880 be44a567ed28 child 50086 ecffea78d381 permissions -rw-r--r--
added "'a rel"
 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@37671  11 text {* Subsequently, we prove some summation laws of natural numbers  wenzelm@37671  12  (including odds, squares, and cubes). These examples demonstrate  wenzelm@37671  13  how plain natural deduction (including induction) may be combined  wenzelm@37671  14  with calculational proof. *}  wenzelm@7968  15 wenzelm@7761  16 wenzelm@10007  17 subsection {* Summation laws *}  wenzelm@7443  18 wenzelm@37671  19 text {* The sum of natural numbers $0 + \cdots + n$ equals $n \times  wenzelm@37671  20  (n + 1)/2$. Avoiding formal reasoning about division we prove this  wenzelm@37671  21  equation multiplied by $2$. *}  wenzelm@7800  22 wenzelm@7800  23 theorem sum_of_naturals:  nipkow@15561  24  "2 * (\i::nat=0..n. i) = n * (n + 1)"  wenzelm@10007  25  (is "?P n" is "?S n = _")  wenzelm@10007  26 proof (induct n)  wenzelm@10007  27  show "?P 0" by simp  wenzelm@10146  28 next  wenzelm@11704  29  fix n have "?S (n + 1) = ?S n + 2 * (n + 1)" by simp  wenzelm@10007  30  also assume "?S n = n * (n + 1)"  wenzelm@11704  31  also have "... + 2 * (n + 1) = (n + 1) * (n + 2)" by simp  wenzelm@10007  32  finally show "?P (Suc n)" by simp  wenzelm@10007  33 qed  wenzelm@7443  34 wenzelm@37671  35 text {* The above proof is a typical instance of mathematical  wenzelm@37671  36  induction. The main statement is viewed as some $\var{P} \ap n$  wenzelm@37671  37  that is split by the induction method into base case $\var{P} \ap  wenzelm@37671  38  0$, and step case $\var{P} \ap n \Impl \var{P} \ap (\idt{Suc} \ap  wenzelm@37671  39  n)$ for arbitrary $n$.  wenzelm@7968  40 wenzelm@37671  41  The step case is established by a short calculation in forward  wenzelm@37671  42  manner. Starting from the left-hand side $\var{S} \ap (n + 1)$ of  wenzelm@37671  43  the thesis, the final result is achieved by transformations  wenzelm@37671  44  involving basic arithmetic reasoning (using the Simplifier). The  wenzelm@37671  45  main point is where the induction hypothesis $\var{S} \ap n = n  wenzelm@37671  46  \times (n + 1)$ is introduced in order to replace a certain subterm.  wenzelm@37671  47  So the transitivity'' rule involved here is actual  wenzelm@37671  48  \emph{substitution}. Also note how the occurrence of \dots'' in  wenzelm@37671  49  the subsequent step documents the position where the right-hand side  wenzelm@37671  50  of the hypothesis got filled in.  wenzelm@7968  51 wenzelm@37671  52  \medskip A further notable point here is integration of calculations  wenzelm@37671  53  with plain natural deduction. This works so well in Isar for two  wenzelm@37671  54  reasons.  wenzelm@37671  55  \begin{enumerate}  wenzelm@37671  56 wenzelm@37671  57  \item Facts involved in \isakeyword{also}~/ \isakeyword{finally}  wenzelm@37671  58  calculational chains may be just anything. There is nothing special  wenzelm@37671  59  about \isakeyword{have}, so the natural deduction element  wenzelm@37671  60  \isakeyword{assume} works just as well.  wenzelm@7968  61 wenzelm@37671  62  \item There are two \emph{separate} primitives for building natural  wenzelm@37671  63  deduction contexts: \isakeyword{fix}~$x$ and  wenzelm@37671  64  \isakeyword{assume}~$A$. Thus it is possible to start reasoning  wenzelm@37671  65  with some new arbitrary, but fixed'' elements before bringing in  wenzelm@37671  66  the actual assumption. In contrast, natural deduction is  wenzelm@37671  67  occasionally formalized with basic context elements of the form  wenzelm@37671  68  $x:A$ instead.  wenzelm@7968  69 wenzelm@37671  70  \end{enumerate}  wenzelm@10007  71 *}  wenzelm@7968  72 wenzelm@37671  73 text {* \medskip We derive further summation laws for odds, squares,  wenzelm@37671  74  and cubes as follows. The basic technique of induction plus  wenzelm@37671  75  calculation is the same as before. *}  wenzelm@7968  76 wenzelm@7800  77 theorem sum_of_odds:  nipkow@15561  78  "(\i::nat=0..i::nat=0..n. i^Suc (Suc 0)) = n * (n + 1) * (2 * n + 1)"  wenzelm@10007  97  (is "?P n" is "?S n = _")  wenzelm@10007  98 proof (induct n)  wenzelm@10007  99  show "?P 0" by simp  wenzelm@10146  100 next  wenzelm@18193  101  fix n have "?S (n + 1) = ?S n + 6 * (n + 1)^Suc (Suc 0)"  wenzelm@18193  102  by (simp add: distrib)  wenzelm@11704  103  also assume "?S n = n * (n + 1) * (2 * n + 1)"  wenzelm@11704  104  also have "... + 6 * (n + 1)^Suc (Suc 0) =  wenzelm@37671  105  (n + 1) * (n + 2) * (2 * (n + 1) + 1)" by (simp add: distrib)  wenzelm@10007  106  finally show "?P (Suc n)" by simp  wenzelm@10007  107 qed  wenzelm@7443  108 wenzelm@7800  109 theorem sum_of_cubes:  nipkow@15561  110  "4 * (\i::nat=0..n. i^3) = (n * (n + 1))^Suc (Suc 0)"  wenzelm@10007  111  (is "?P n" is "?S n = _")  wenzelm@10007  112 proof (induct n)  wenzelm@10007  113  show "?P 0" by (simp add: power_eq_if)  wenzelm@10146  114 next  wenzelm@11704  115  fix n have "?S (n + 1) = ?S n + 4 * (n + 1)^3"  wenzelm@10007  116  by (simp add: power_eq_if distrib)  wenzelm@11701  117  also assume "?S n = (n * (n + 1))^Suc (Suc 0)"  wenzelm@11704  118  also have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^Suc (Suc 0)"  wenzelm@10007  119  by (simp add: power_eq_if distrib)  wenzelm@10007  120  finally show "?P (Suc n)" by simp  wenzelm@10007  121 qed  wenzelm@7443  122 wenzelm@37671  123 text {* Comparing these examples with the tactic script version  wenzelm@40880  124  @{file "~~/src/HOL/ex/NatSum.thy"}, we note an important difference  wenzelm@40880  125  of how induction vs.\ simplification is  wenzelm@37671  126  applied. While \cite[\S10]{isabelle-ref} advises for these examples  wenzelm@37671  127  that induction should not be applied until the goal is in the  wenzelm@37671  128  simplest form'' this would be a very bad idea in our setting.  wenzelm@7968  129 wenzelm@37671  130  Simplification normalizes all arithmetic expressions involved,  wenzelm@37671  131  producing huge intermediate goals. With applying induction  wenzelm@37671  132  afterwards, the Isar proof text would have to reflect the emerging  wenzelm@37671  133  configuration by appropriate sub-proofs. This would result in badly  wenzelm@37671  134  structured, low-level technical reasoning, without any good idea of  wenzelm@37671  135  the actual point.  wenzelm@7968  136 wenzelm@37671  137  \medskip As a general rule of good proof style, automatic methods  wenzelm@37671  138  such as $\idt{simp}$ or $\idt{auto}$ should normally be never used  wenzelm@37671  139  as initial proof methods, but only as terminal ones, solving certain  wenzelm@37671  140  goals completely. *}  wenzelm@7968  141 wenzelm@10007  142 end