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

src/HOL/Isar_Examples/Summation.thy

author | blanchet |

Thu Sep 11 18:54:36 2014 +0200 (2014-09-11) | |

changeset 58306 | 117ba6cbe414 |

parent 55640 | abc140f21caa |

child 58614 | 7338eb25226c |

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

renamed 'rep_datatype' to 'old_rep_datatype' (HOL)

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)"

30 by simp

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

32 also have "\<dots> + 2 * (n + 1) = (n + 1) * (n + 2)"

33 by simp

34 finally show "?P (Suc n)"

35 by simp

36 qed

38 text {* The above proof is a typical instance of mathematical

39 induction. The main statement is viewed as some $\var{P} \ap n$

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

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

42 n)$ for arbitrary $n$.

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

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

46 the thesis, the final result is achieved by transformations

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

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

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

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

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

52 the subsequent step documents the position where the right-hand side

53 of the hypothesis got filled in.

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

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

57 reasons.

58 \begin{enumerate}

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

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

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

63 \isakeyword{assume} works just as well.

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

66 deduction contexts: \isakeyword{fix}~$x$ and

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

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

69 the actual assumption. In contrast, natural deduction is

70 occasionally formalized with basic context elements of the form

71 $x:A$ instead.

73 \end{enumerate}

74 *}

76 text {* \medskip We derive further summation laws for odds, squares,

77 and cubes as follows. The basic technique of induction plus

78 calculation is the same as before. *}

80 theorem sum_of_odds:

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

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

83 proof (induct n)

84 show "?P 0" by simp

85 next

86 fix n

87 have "?S (n + 1) = ?S n + 2 * n + 1"

88 by simp

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

90 also have "\<dots> + 2 * n + 1 = (n + 1)^Suc (Suc 0)"

91 by simp

92 finally show "?P (Suc n)"

93 by simp

94 qed

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

97 built-in arithmetic simplifications, such as bringing in

98 distributivity by hand. *}

100 lemmas distrib = add_mult_distrib add_mult_distrib2

102 theorem sum_of_squares:

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

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

105 proof (induct n)

106 show "?P 0" by simp

107 next

108 fix n

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

110 by (simp add: distrib)

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

112 also have "\<dots> + 6 * (n + 1)^Suc (Suc 0) =

113 (n + 1) * (n + 2) * (2 * (n + 1) + 1)"

114 by (simp add: distrib)

115 finally show "?P (Suc n)"

116 by simp

117 qed

119 theorem sum_of_cubes:

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

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

122 proof (induct n)

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

124 next

125 fix n

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

127 by (simp add: power_eq_if distrib)

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

129 also have "\<dots> + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^Suc (Suc 0)"

130 by (simp add: power_eq_if distrib)

131 finally show "?P (Suc n)"

132 by simp

133 qed

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

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

137 unsimplified statement. This allows to state the induction cases

138 robustly and conveniently. Simplification (or other automated)

139 methods are then applied in terminal position to solve certain

140 sub-problems completely.

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

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

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

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

146 sub-problems. *}

148 end