author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 40880  be44a567ed28 
child 50086  ecffea78d381 
permissions  rwrr 
33026  1 
(* Title: HOL/Isar_Examples/Summation.thy 
7443  2 
Author: Markus Wenzel 
3 
*) 

4 

10007  5 
header {* Summing natural numbers *} 
7443  6 

15561  7 
theory Summation 
8 
imports Main 

9 
begin 

10 

37671  11 
text {* Subsequently, we prove some summation laws of natural numbers 
12 
(including odds, squares, and cubes). These examples demonstrate 

13 
how plain natural deduction (including induction) may be combined 

14 
with calculational proof. *} 

7968  15 

7761  16 

10007  17 
subsection {* Summation laws *} 
7443  18 

37671  19 
text {* The sum of natural numbers $0 + \cdots + n$ equals $n \times 
20 
(n + 1)/2$. Avoiding formal reasoning about division we prove this 

21 
equation multiplied by $2$. *} 

7800  22 

23 
theorem sum_of_naturals: 

15561  24 
"2 * (\<Sum>i::nat=0..n. i) = n * (n + 1)" 
10007  25 
(is "?P n" is "?S n = _") 
26 
proof (induct n) 

27 
show "?P 0" by simp 

10146  28 
next 
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset

29 
fix n have "?S (n + 1) = ?S n + 2 * (n + 1)" by simp 
10007  30 
also assume "?S n = n * (n + 1)" 
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset

31 
also have "... + 2 * (n + 1) = (n + 1) * (n + 2)" by simp 
10007  32 
finally show "?P (Suc n)" by simp 
33 
qed 

7443  34 

37671  35 
text {* The above proof is a typical instance of mathematical 
36 
induction. The main statement is viewed as some $\var{P} \ap n$ 

37 
that is split by the induction method into base case $\var{P} \ap 

38 
0$, and step case $\var{P} \ap n \Impl \var{P} \ap (\idt{Suc} \ap 

39 
n)$ for arbitrary $n$. 

7968  40 

37671  41 
The step case is established by a short calculation in forward 
42 
manner. Starting from the lefthand side $\var{S} \ap (n + 1)$ of 

43 
the thesis, the final result is achieved by transformations 

44 
involving basic arithmetic reasoning (using the Simplifier). The 

45 
main point is where the induction hypothesis $\var{S} \ap n = n 

46 
\times (n + 1)$ is introduced in order to replace a certain subterm. 

47 
So the ``transitivity'' rule involved here is actual 

48 
\emph{substitution}. Also note how the occurrence of ``\dots'' in 

49 
the subsequent step documents the position where the righthand side 

50 
of the hypothesis got filled in. 

7968  51 

37671  52 
\medskip A further notable point here is integration of calculations 
53 
with plain natural deduction. This works so well in Isar for two 

54 
reasons. 

55 
\begin{enumerate} 

56 

57 
\item Facts involved in \isakeyword{also}~/ \isakeyword{finally} 

58 
calculational chains may be just anything. There is nothing special 

59 
about \isakeyword{have}, so the natural deduction element 

60 
\isakeyword{assume} works just as well. 

7968  61 

37671  62 
\item There are two \emph{separate} primitives for building natural 
63 
deduction contexts: \isakeyword{fix}~$x$ and 

64 
\isakeyword{assume}~$A$. Thus it is possible to start reasoning 

65 
with some new ``arbitrary, but fixed'' elements before bringing in 

66 
the actual assumption. In contrast, natural deduction is 

67 
occasionally formalized with basic context elements of the form 

68 
$x:A$ instead. 

7968  69 

37671  70 
\end{enumerate} 
10007  71 
*} 
7968  72 

37671  73 
text {* \medskip We derive further summation laws for odds, squares, 
74 
and cubes as follows. The basic technique of induction plus 

75 
calculation is the same as before. *} 

7968  76 

7800  77 
theorem sum_of_odds: 
15561  78 
"(\<Sum>i::nat=0..<n. 2 * i + 1) = n^Suc (Suc 0)" 
10007  79 
(is "?P n" is "?S n = _") 
80 
proof (induct n) 

81 
show "?P 0" by simp 

10146  82 
next 
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset

83 
fix n have "?S (n + 1) = ?S n + 2 * n + 1" by simp 
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10672
diff
changeset

84 
also assume "?S n = n^Suc (Suc 0)" 
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset

85 
also have "... + 2 * n + 1 = (n + 1)^Suc (Suc 0)" by simp 
10007  86 
finally show "?P (Suc n)" by simp 
87 
qed 

7443  88 

37671  89 
text {* Subsequently we require some additional tweaking of Isabelle 
90 
builtin arithmetic simplifications, such as bringing in 

91 
distributivity by hand. *} 

8814  92 

10007  93 
lemmas distrib = add_mult_distrib add_mult_distrib2 
8814  94 

7761  95 
theorem sum_of_squares: 
15561  96 
"6 * (\<Sum>i::nat=0..n. i^Suc (Suc 0)) = n * (n + 1) * (2 * n + 1)" 
10007  97 
(is "?P n" is "?S n = _") 
98 
proof (induct n) 

99 
show "?P 0" by simp 

10146  100 
next 
18193  101 
fix n have "?S (n + 1) = ?S n + 6 * (n + 1)^Suc (Suc 0)" 
102 
by (simp add: distrib) 

11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset

103 
also assume "?S n = n * (n + 1) * (2 * n + 1)" 
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset

104 
also have "... + 6 * (n + 1)^Suc (Suc 0) = 
37671  105 
(n + 1) * (n + 2) * (2 * (n + 1) + 1)" by (simp add: distrib) 
10007  106 
finally show "?P (Suc n)" by simp 
107 
qed 

7443  108 

7800  109 
theorem sum_of_cubes: 
15561  110 
"4 * (\<Sum>i::nat=0..n. i^3) = (n * (n + 1))^Suc (Suc 0)" 
10007  111 
(is "?P n" is "?S n = _") 
112 
proof (induct n) 

113 
show "?P 0" by (simp add: power_eq_if) 

10146  114 
next 
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset

115 
fix n have "?S (n + 1) = ?S n + 4 * (n + 1)^3" 
10007  116 
by (simp add: power_eq_if distrib) 
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10672
diff
changeset

117 
also assume "?S n = (n * (n + 1))^Suc (Suc 0)" 
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset

118 
also have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^Suc (Suc 0)" 
10007  119 
by (simp add: power_eq_if distrib) 
120 
finally show "?P (Suc n)" by simp 

121 
qed 

7443  122 

37671  123 
text {* Comparing these examples with the tactic script version 
40880  124 
@{file "~~/src/HOL/ex/NatSum.thy"}, we note an important difference 
125 
of how induction vs.\ simplification is 

37671  126 
applied. While \cite[\S10]{isabelleref} advises for these examples 
127 
that ``induction should not be applied until the goal is in the 

128 
simplest form'' this would be a very bad idea in our setting. 

7968  129 

37671  130 
Simplification normalizes all arithmetic expressions involved, 
131 
producing huge intermediate goals. With applying induction 

132 
afterwards, the Isar proof text would have to reflect the emerging 

133 
configuration by appropriate subproofs. This would result in badly 

134 
structured, lowlevel technical reasoning, without any good idea of 

135 
the actual point. 

7968  136 

37671  137 
\medskip As a general rule of good proof style, automatic methods 
138 
such as $\idt{simp}$ or $\idt{auto}$ should normally be never used 

139 
as initial proof methods, but only as terminal ones, solving certain 

140 
goals completely. *} 

7968  141 

10007  142 
end 