src/HOL/Isar_Examples/Summation.thy
 author hoelzl Tue Mar 26 12:20:58 2013 +0100 (2013-03-26) changeset 51526 155263089e7b parent 50086 ecffea78d381 child 55640 abc140f21caa permissions -rw-r--r--
move SEQ.thy and Lim.thy to Limits.thy
 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@50086  123 text {* Note that in contrast to older traditions of tactical proof  wenzelm@50086  124  scripts, the structured proof applies induction on the original,  wenzelm@50086  125  unsimplified statement. This allows to state the induction cases  wenzelm@50086  126  robustly and conveniently. Simplification (or other automated)  wenzelm@50086  127  methods are then applied in terminal position to solve certain  wenzelm@50086  128  sub-problems completely.  wenzelm@7968  129 wenzelm@50086  130  As a general rule of good proof style, automatic methods such as  wenzelm@50086  131  $\idt{simp}$ or $\idt{auto}$ should normally be never used as  wenzelm@50086  132  initial proof methods with a nested sub-proof to address the  wenzelm@50086  133  automatically produced situation, but only as terminal ones to solve  wenzelm@50086  134  sub-problems. *}  wenzelm@7968  135 wenzelm@10007  136 end