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

src/HOL/Isar_Examples/Summation.thy

author | haftmann |

Wed Jun 30 16:46:44 2010 +0200 (2010-06-30) | |

changeset 37659 | 14cabf5fa710 |

parent 33026 | 8f35633c4922 |

child 37671 | fa53d267dab3 |

permissions | -rw-r--r-- |

more speaking names

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_raw {*

12 \footnote{This example is somewhat reminiscent of the

13 \url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, which is

14 discussed in \cite{isabelle-ref} in the context of permutative

15 rewrite rules and ordered rewriting.}

16 *}

18 text {*

19 Subsequently, we prove some summation laws of natural numbers

20 (including odds, squares, and cubes). These examples demonstrate how

21 plain natural deduction (including induction) may be combined with

22 calculational proof.

23 *}

26 subsection {* Summation laws *}

28 text {*

29 The sum of natural numbers $0 + \cdots + n$ equals $n \times (n +

30 1)/2$. Avoiding formal reasoning about division we prove this

31 equation multiplied by $2$.

32 *}

34 theorem sum_of_naturals:

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

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

37 proof (induct n)

38 show "?P 0" by simp

39 next

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

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

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

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

44 qed

46 text {*

47 The above proof is a typical instance of mathematical induction. The

48 main statement is viewed as some $\var{P} \ap n$ that is split by the

49 induction method into base case $\var{P} \ap 0$, and step case

50 $\var{P} \ap n \Impl \var{P} \ap (\idt{Suc} \ap n)$ for arbitrary $n$.

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

53 manner. Starting from the left-hand side $\var{S} \ap (n + 1)$ of

54 the thesis, the final result is achieved by transformations involving

55 basic arithmetic reasoning (using the Simplifier). The main point is

56 where the induction hypothesis $\var{S} \ap n = n \times (n + 1)$ is

57 introduced in order to replace a certain subterm. So the

58 ``transitivity'' rule involved here is actual \emph{substitution}.

59 Also note how the occurrence of ``\dots'' in the subsequent step

60 documents the position where the right-hand side of the hypothesis

61 got filled in.

63 \medskip A further notable point here is integration of calculations

64 with plain natural deduction. This works so well in Isar for two

65 reasons.

66 \begin{enumerate}

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

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

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

71 \isakeyword{assume} works just as well.

73 \item There are two \emph{separate} primitives for building natural

74 deduction contexts: \isakeyword{fix}~$x$ and \isakeyword{assume}~$A$.

75 Thus it is possible to start reasoning with some new ``arbitrary, but

76 fixed'' elements before bringing in the actual assumption. In

77 contrast, natural deduction is occasionally formalized with basic

78 context elements of the form $x:A$ instead.

80 \end{enumerate}

81 *}

83 text {*

84 \medskip We derive further summation laws for odds, squares, and

85 cubes as follows. The basic technique of induction plus calculation

86 is the same as before.

87 *}

89 theorem sum_of_odds:

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

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

92 proof (induct n)

93 show "?P 0" by simp

94 next

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

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

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

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

99 qed

101 text {*

102 Subsequently we require some additional tweaking of Isabelle built-in

103 arithmetic simplifications, such as bringing in distributivity by

104 hand.

105 *}

107 lemmas distrib = add_mult_distrib add_mult_distrib2

109 theorem sum_of_squares:

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

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

112 proof (induct n)

113 show "?P 0" by simp

114 next

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

116 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