summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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

1 (* Title: HOL/Isar_Examples/Summation.thy

2 Author: Markus Wenzel

3 *)

5 header {* Summing natural numbers *}

7 theory Summation

8 imports Main

9 begin

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. *}

17 subsection {* Summation laws *}

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$. *}

23 theorem sum_of_naturals:

24 "2 * (\<Sum>i::nat=0..n. i) = n * (n + 1)"

25 (is "?P n" is "?S n = _")

26 proof (induct n)

27 show "?P 0" by simp

28 next

29 fix n have "?S (n + 1) = ?S n + 2 * (n + 1)" by simp

30 also assume "?S n = n * (n + 1)"

31 also have "... + 2 * (n + 1) = (n + 1) * (n + 2)" by simp

32 finally show "?P (Suc n)" by simp

33 qed

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$.

41 The step case is established by a short calculation in forward

42 manner. Starting from the left-hand 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 right-hand side

50 of the hypothesis got filled in.

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}

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.

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.

70 \end{enumerate}

71 *}

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. *}

77 theorem sum_of_odds:

78 "(\<Sum>i::nat=0..<n. 2 * i + 1) = n^Suc (Suc 0)"

79 (is "?P n" is "?S n = _")

80 proof (induct n)

81 show "?P 0" by simp

82 next

83 fix n have "?S (n + 1) = ?S n + 2 * n + 1" by simp

84 also assume "?S n = n^Suc (Suc 0)"

85 also have "... + 2 * n + 1 = (n + 1)^Suc (Suc 0)" by simp

86 finally show "?P (Suc n)" by simp

87 qed

89 text {* Subsequently we require some additional tweaking of Isabelle

90 built-in arithmetic simplifications, such as bringing in

91 distributivity by hand. *}

93 lemmas distrib = add_mult_distrib add_mult_distrib2

95 theorem sum_of_squares:

96 "6 * (\<Sum>i::nat=0..n. i^Suc (Suc 0)) = n * (n + 1) * (2 * n + 1)"

97 (is "?P n" is "?S n = _")

98 proof (induct n)

99 show "?P 0" by simp

100 next

101 fix n have "?S (n + 1) = ?S n + 6 * (n + 1)^Suc (Suc 0)"

102 by (simp add: distrib)

103 also assume "?S n = n * (n + 1) * (2 * n + 1)"

104 also have "... + 6 * (n + 1)^Suc (Suc 0) =

105 (n + 1) * (n + 2) * (2 * (n + 1) + 1)" by (simp add: distrib)

106 finally show "?P (Suc n)" by simp

107 qed

109 theorem sum_of_cubes:

110 "4 * (\<Sum>i::nat=0..n. i^3) = (n * (n + 1))^Suc (Suc 0)"

111 (is "?P n" is "?S n = _")

112 proof (induct n)

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

114 next

115 fix n have "?S (n + 1) = ?S n + 4 * (n + 1)^3"

116 by (simp add: power_eq_if distrib)

117 also assume "?S n = (n * (n + 1))^Suc (Suc 0)"

118 also have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^Suc (Suc 0)"

119 by (simp add: power_eq_if distrib)

120 finally show "?P (Suc n)" by simp

121 qed

123 text {* Note that in contrast to older traditions of tactical proof

124 scripts, the structured proof applies induction on the original,

125 unsimplified statement. This allows to state the induction cases

126 robustly and conveniently. Simplification (or other automated)

127 methods are then applied in terminal position to solve certain

128 sub-problems completely.

130 As a general rule of good proof style, automatic methods such as

131 $\idt{simp}$ or $\idt{auto}$ should normally be never used as

132 initial proof methods with a nested sub-proof to address the

133 automatically produced situation, but only as terminal ones to solve

134 sub-problems. *}

136 end