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