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

src/HOL/Isar_examples/Summation.thy

author | paulson |

Tue Jun 28 15:27:45 2005 +0200 (2005-06-28) | |

changeset 16587 | b34c8aa657a5 |

parent 15912 | 47aa1a8fcdc9 |

child 18193 | 54419506df9e |

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

Constant "If" is now local

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