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

src/HOL/Isar_examples/Summation.thy

author | wenzelm |

Sat Oct 30 20:20:48 1999 +0200 (1999-10-30) | |

changeset 7982 | d534b897ce39 |

parent 7968 | 964b65b4e433 |

child 8584 | 016314c2fa0a |

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

improved presentation;

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

2 ID: $Id$

3 Author: Markus Wenzel

4 *)

6 header {* Summing natural numbers *};

8 theory Summation = Main:;

10 text_raw {*

11 \footnote{This example is somewhat reminiscent of the

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

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

14 rewrite rules and ordered rewriting.}

15 *};

17 text {*

18 Subsequently, we prove some summation laws of natural numbers

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

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

21 calculational proof.

22 *};

25 subsection {* A summation operator *};

27 text {*

28 The binder operator $\idt{sum} :: (\idt{nat} \To \idt{nat}) \To

29 \idt{nat} \To \idt{nat}$ formalizes summation of natural numbers

30 indexed from $0$ up to $k$ (excluding the bound):

31 \[

32 \sum\limits_{i < k} f(i) = \idt{sum} \ap (\lam i f \ap i) \ap k

33 \]

34 *};

36 consts

37 sum :: "[nat => nat, nat] => nat";

39 primrec

40 "sum f 0 = 0"

41 "sum f (Suc n) = f n + sum f n";

43 syntax

44 "_SUM" :: "[idt, nat, nat] => nat"

45 ("SUM _ < _. _" [0, 0, 10] 10);

46 translations

47 "SUM i < k. b" == "sum (\<lambda>i. b) k";

50 subsection {* Summation laws *};

52 text_raw {* \begin{comment} *};

54 (* FIXME binary arithmetic does not yet work here *)

56 syntax

57 "3" :: nat ("3")

58 "4" :: nat ("4")

59 "6" :: nat ("6");

61 translations

62 "3" == "Suc 2"

63 "4" == "Suc 3"

64 "6" == "Suc (Suc 4)";

66 theorems [simp] = add_mult_distrib add_mult_distrib2 mult_ac;

68 text_raw {* \end{comment} *};

70 text {*

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

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

73 equation multiplied by $2$.

74 *};

76 theorem sum_of_naturals:

77 "2 * (SUM i < n + 1. i) = n * (n + 1)"

78 (is "?P n" is "?S n = _");

79 proof (induct n);

80 show "?P 0"; by simp;

82 fix n;

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

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

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

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

87 qed;

89 text {*

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

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

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

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

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

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

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

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

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

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

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

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

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

104 got filled in.

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

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

108 reasons.

109 \begin{enumerate}

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

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

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

114 \isakeyword{assume} works just as well.

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

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

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

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

120 contrast, natural deduction is occasionally formalized with basic

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

123 \end{enumerate}

124 *};

126 text {*

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

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

129 is the same as before.

130 *};

132 theorem sum_of_odds:

133 "(SUM i < n. 2 * i + 1) = n^2"

134 (is "?P n" is "?S n = _");

135 proof (induct n);

136 show "?P 0"; by simp;

138 fix n;

139 have "?S (n + 1) = ?S n + 2 * n + 1"; by simp;

140 also; assume "?S n = n^2";

141 also; have "... + 2 * n + 1 = (n + 1)^2"; by simp;

142 finally; show "?P (Suc n)"; by simp;

143 qed;

145 theorem sum_of_squares:

146 "6 * (SUM i < n + 1. i^2) = n * (n + 1) * (2 * n + 1)"

147 (is "?P n" is "?S n = _");

148 proof (induct n);

149 show "?P 0"; by simp;

151 fix n;

152 have "?S (n + 1) = ?S n + 6 * (n + 1)^2"; by simp;

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

154 also; have "... + 6 * (n + 1)^2 =

155 (n + 1) * (n + 2) * (2 * (n + 1) + 1)"; by simp;

156 finally; show "?P (Suc n)"; by simp;

157 qed;

159 theorem sum_of_cubes:

160 "4 * (SUM i < n + 1. i^3) = (n * (n + 1))^2"

161 (is "?P n" is "?S n = _");

162 proof (induct n);

163 show "?P 0"; by simp;

165 fix n;

166 have "?S (n + 1) = ?S n + 4 * (n + 1)^3"; by simp;

167 also; assume "?S n = (n * (n + 1))^2";

168 also; have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^2";

169 by simp;

170 finally; show "?P (Suc n)"; by simp;

171 qed;

173 text {*

174 Comparing these examples with the tactic script version

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

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

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

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

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

181 Simplification normalizes all arithmetic expressions involved,

182 producing huge intermediate goals. With applying induction

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

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

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

186 the actual point.

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

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

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

191 goals completely.

192 *};

194 end;