wenzelm@7443

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

wenzelm@7443

2 
ID: $Id$

wenzelm@7443

3 
Author: Markus Wenzel

wenzelm@7443

4 
*)

wenzelm@7443

5 

wenzelm@10007

6 
header {* Summing natural numbers *}

wenzelm@7443

7 

wenzelm@10007

8 
theory Summation = Main:

wenzelm@7443

9 

wenzelm@7968

10 
text_raw {*

wenzelm@7968

11 
\footnote{This example is somewhat reminiscent of the

wenzelm@7968

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

wenzelm@7968

13 
discussed in \cite{isabelleref} in the context of permutative

wenzelm@7968

14 
rewrite rules and ordered rewriting.}

wenzelm@10007

15 
*}

wenzelm@7968

16 

wenzelm@7968

17 
text {*

wenzelm@7968

18 
Subsequently, we prove some summation laws of natural numbers

wenzelm@7982

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

wenzelm@7968

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

wenzelm@7968

21 
calculational proof.

wenzelm@10007

22 
*}

wenzelm@7968

23 

wenzelm@7761

24 

wenzelm@10007

25 
subsection {* Summation laws *}

wenzelm@7443

26 

wenzelm@7968

27 
text {*

wenzelm@7968

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

wenzelm@7982

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

wenzelm@7982

30 
equation multiplied by $2$.

wenzelm@10007

31 
*}

wenzelm@7800

32 

wenzelm@7800

33 
theorem sum_of_naturals:

wenzelm@10672

34 
"2 * (\<Sum>i < n + 1. i) = n * (n + 1)"

wenzelm@10007

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

wenzelm@10007

36 
proof (induct n)

wenzelm@10007

37 
show "?P 0" by simp

wenzelm@10146

38 
next

wenzelm@10146

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

wenzelm@10007

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

wenzelm@10007

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

wenzelm@10007

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

wenzelm@10007

43 
qed

wenzelm@7443

44 

wenzelm@7968

45 
text {*

wenzelm@7968

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

wenzelm@7968

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

wenzelm@7968

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

wenzelm@7982

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

wenzelm@7968

50 

wenzelm@7968

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

wenzelm@7968

52 
manner. Starting from the lefthand side $\var{S} \ap (n + 1)$ of

wenzelm@7982

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

wenzelm@7982

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

wenzelm@7982

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

wenzelm@7982

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

wenzelm@7968

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

wenzelm@7968

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

wenzelm@7982

59 
documents the position where the righthand side of the hypothesis

wenzelm@7968

60 
got filled in.

wenzelm@7968

61 

wenzelm@7968

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

wenzelm@7982

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

wenzelm@7982

64 
reasons.

wenzelm@7968

65 
\begin{enumerate}

wenzelm@7968

66 

wenzelm@7968

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

wenzelm@7968

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

wenzelm@7968

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

wenzelm@7968

70 
\isakeyword{assume} works just as well.

wenzelm@7968

71 

wenzelm@7968

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

wenzelm@7968

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

wenzelm@7982

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

wenzelm@7982

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

wenzelm@7982

76 
contrast, natural deduction is occasionally formalized with basic

wenzelm@7982

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

wenzelm@7968

78 

wenzelm@7968

79 
\end{enumerate}

wenzelm@10007

80 
*}

wenzelm@7968

81 

wenzelm@7968

82 
text {*

wenzelm@7982

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

wenzelm@7982

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

wenzelm@7982

85 
is the same as before.

wenzelm@10007

86 
*}

wenzelm@7968

87 

wenzelm@7800

88 
theorem sum_of_odds:

wenzelm@10672

89 
"(\<Sum>i < n. 2 * i + 1) = n^2"

wenzelm@10007

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

wenzelm@10007

91 
proof (induct n)

wenzelm@10007

92 
show "?P 0" by simp

wenzelm@10146

93 
next

wenzelm@10146

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

wenzelm@10007

95 
also assume "?S n = n^2"

wenzelm@10007

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

wenzelm@10007

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

wenzelm@10007

98 
qed

wenzelm@7443

99 

wenzelm@8814

100 
text {*

wenzelm@8814

101 
Subsequently we require some additional tweaking of Isabelle builtin

wenzelm@8814

102 
arithmetic simplifications, such as bringing in distributivity by

wenzelm@8814

103 
hand.

wenzelm@10007

104 
*}

wenzelm@8814

105 

wenzelm@10007

106 
lemmas distrib = add_mult_distrib add_mult_distrib2

wenzelm@8814

107 

wenzelm@7761

108 
theorem sum_of_squares:

wenzelm@10672

109 
"#6 * (\<Sum>i < n + 1. i^2) = n * (n + 1) * (2 * n + 1)"

wenzelm@10007

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

wenzelm@10007

111 
proof (induct n)

wenzelm@10007

112 
show "?P 0" by simp

wenzelm@10146

113 
next

wenzelm@10146

114 
fix n have "?S (n + 1) = ?S n + #6 * (n + 1)^2" by (simp add: distrib)

wenzelm@10007

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

wenzelm@10007

116 
also have "... + #6 * (n + 1)^2 =

wenzelm@10007

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

wenzelm@10007

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

wenzelm@10007

119 
qed

wenzelm@7443

120 

wenzelm@7800

121 
theorem sum_of_cubes:

wenzelm@10672

122 
"#4 * (\<Sum>i < n + 1. i^#3) = (n * (n + 1))^2"

wenzelm@10007

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

wenzelm@10007

124 
proof (induct n)

wenzelm@10007

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

wenzelm@10146

126 
next

wenzelm@10146

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

wenzelm@10007

128 
by (simp add: power_eq_if distrib)

wenzelm@10007

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

wenzelm@10007

130 
also have "... + #4 * (n + 1)^#3 = ((n + 1) * ((n + 1) + 1))^2"

wenzelm@10007

131 
by (simp add: power_eq_if distrib)

wenzelm@10007

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

wenzelm@10007

133 
qed

wenzelm@7443

134 

wenzelm@7968

135 
text {*

wenzelm@7968

136 
Comparing these examples with the tactic script version

wenzelm@7968

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

wenzelm@7982

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

wenzelm@7968

139 
applied. While \cite[\S10]{isabelleref} advises for these examples

wenzelm@7968

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

wenzelm@7968

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

wenzelm@7968

142 

wenzelm@7968

143 
Simplification normalizes all arithmetic expressions involved,

wenzelm@7982

144 
producing huge intermediate goals. With applying induction

wenzelm@7982

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

wenzelm@7982

146 
configuration by appropriate subproofs. This would result in badly

wenzelm@7982

147 
structured, lowlevel technical reasoning, without any good idea of

wenzelm@7982

148 
the actual point.

wenzelm@7968

149 

wenzelm@7968

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

wenzelm@7982

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

wenzelm@7968

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

wenzelm@7968

153 
goals completely.

wenzelm@10007

154 
*}

wenzelm@7968

155 

wenzelm@10007

156 
end
