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

src/HOL/Isar_examples/Summation.thy

author | haftmann |

Mon Jan 30 08:20:56 2006 +0100 (2006-01-30) | |

changeset 18851 | 9502ce541f01 |

parent 18193 | 54419506df9e |

child 31758 | 3edd5f813f01 |

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

adaptions to codegen_package

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

108 lemmas distrib = add_mult_distrib add_mult_distrib2

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

117 by (simp add: distrib)

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

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

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

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

122 qed

124 theorem sum_of_cubes:

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

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

127 proof (induct n)

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

129 next

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

131 by (simp add: power_eq_if distrib)

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

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

134 by (simp add: power_eq_if distrib)

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

136 qed

138 text {*

139 Comparing these examples with the tactic script version

140 \url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, we note

141 an important difference of how induction vs.\ simplification is

142 applied. While \cite[\S10]{isabelle-ref} advises for these examples

143 that ``induction should not be applied until the goal is in the

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

146 Simplification normalizes all arithmetic expressions involved,

147 producing huge intermediate goals. With applying induction

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

149 configuration by appropriate sub-proofs. This would result in badly

150 structured, low-level technical reasoning, without any good idea of

151 the actual point.

153 \medskip As a general rule of good proof style, automatic methods

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

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

156 goals completely.

157 *}

159 end