diff -r cc038dc8f412 -r 8f35633c4922 src/HOL/Isar_Examples/Summation.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Isar_Examples/Summation.thy	Tue Oct 20 19:37:09 2009 +0200
@@ -0,0 +1,158 @@
+(*  Title:      HOL/Isar_Examples/Summation.thy
+    Author:     Markus Wenzel
+*)
+
+header {* Summing natural numbers *}
+
+theory Summation
+imports Main
+begin
+
+text_raw {*
+ \footnote{This example is somewhat reminiscent of the
+ \url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, which is
+ discussed in \cite{isabelle-ref} in the context of permutative
+ rewrite rules and ordered rewriting.}
+*}
+
+text {*
+ Subsequently, we prove some summation laws of natural numbers
+ (including odds, squares, and cubes).  These examples demonstrate how
+ plain natural deduction (including induction) may be combined with
+ calculational proof.
+*}
+
+
+subsection {* Summation laws *}
+
+text {*
+ The sum of natural numbers $0 + \cdots + n$ equals $n \times (n +
+ 1)/2$.  Avoiding formal reasoning about division we prove this
+ equation multiplied by $2$.
+*}
+
+theorem sum_of_naturals:
+  "2 * (\<Sum>i::nat=0..n. i) = n * (n + 1)"
+  (is "?P n" is "?S n = _")
+proof (induct n)
+  show "?P 0" by simp
+next
+  fix n have "?S (n + 1) = ?S n + 2 * (n + 1)" by simp
+  also assume "?S n = n * (n + 1)"
+  also have "... + 2 * (n + 1) = (n + 1) * (n + 2)" by simp
+  finally show "?P (Suc n)" by simp
+qed
+
+text {*
+ The above proof is a typical instance of mathematical induction.  The
+ main statement is viewed as some $\var{P} \ap n$ that is split by the
+ induction method into base case $\var{P} \ap 0$, and step case
+ $\var{P} \ap n \Impl \var{P} \ap (\idt{Suc} \ap n)$ for arbitrary $n$.
+
+ The step case is established by a short calculation in forward
+ manner.  Starting from the left-hand side $\var{S} \ap (n + 1)$ of
+ the thesis, the final result is achieved by transformations involving
+ basic arithmetic reasoning (using the Simplifier).  The main point is
+ where the induction hypothesis $\var{S} \ap n = n \times (n + 1)$ is
+ introduced in order to replace a certain subterm.  So the
+ ``transitivity'' rule involved here is actual \emph{substitution}.
+ Also note how the occurrence of ``\dots'' in the subsequent step
+ documents the position where the right-hand side of the hypothesis
+ got filled in.
+
+ \medskip A further notable point here is integration of calculations
+ with plain natural deduction.  This works so well in Isar for two
+ reasons.
+ \begin{enumerate}
+
+ \item Facts involved in \isakeyword{also}~/ \isakeyword{finally}
+ calculational chains may be just anything.  There is nothing special
+ about \isakeyword{have}, so the natural deduction element
+ \isakeyword{assume} works just as well.
+
+ \item There are two \emph{separate} primitives for building natural
+ deduction contexts: \isakeyword{fix}~$x$ and \isakeyword{assume}~$A$.
+ Thus it is possible to start reasoning with some new ``arbitrary, but
+ fixed'' elements before bringing in the actual assumption.  In
+ contrast, natural deduction is occasionally formalized with basic
+ context elements of the form $x:A$ instead.
+
+ \end{enumerate}
+*}
+
+text {*
+ \medskip We derive further summation laws for odds, squares, and
+ cubes as follows.  The basic technique of induction plus calculation
+ is the same as before.
+*}
+
+theorem sum_of_odds:
+  "(\<Sum>i::nat=0..<n. 2 * i + 1) = n^Suc (Suc 0)"
+  (is "?P n" is "?S n = _")
+proof (induct n)
+  show "?P 0" by simp
+next
+  fix n have "?S (n + 1) = ?S n + 2 * n + 1" by simp
+  also assume "?S n = n^Suc (Suc 0)"
+  also have "... + 2 * n + 1 = (n + 1)^Suc (Suc 0)" by simp
+  finally show "?P (Suc n)" by simp
+qed
+
+text {*
+ Subsequently we require some additional tweaking of Isabelle built-in
+ arithmetic simplifications, such as bringing in distributivity by
+ hand.
+*}
+
+lemmas distrib = add_mult_distrib add_mult_distrib2
+
+theorem sum_of_squares:
+  "6 * (\<Sum>i::nat=0..n. i^Suc (Suc 0)) = n * (n + 1) * (2 * n + 1)"
+  (is "?P n" is "?S n = _")
+proof (induct n)
+  show "?P 0" by simp
+next
+  fix n have "?S (n + 1) = ?S n + 6 * (n + 1)^Suc (Suc 0)"
+    by (simp add: distrib)
+  also assume "?S n = n * (n + 1) * (2 * n + 1)"
+  also have "... + 6 * (n + 1)^Suc (Suc 0) =
+    (n + 1) * (n + 2) * (2 * (n + 1) + 1)" by (simp add: distrib)
+  finally show "?P (Suc n)" by simp
+qed
+
+theorem sum_of_cubes:
+  "4 * (\<Sum>i::nat=0..n. i^3) = (n * (n + 1))^Suc (Suc 0)"
+  (is "?P n" is "?S n = _")
+proof (induct n)
+  show "?P 0" by (simp add: power_eq_if)
+next
+  fix n have "?S (n + 1) = ?S n + 4 * (n + 1)^3"
+    by (simp add: power_eq_if distrib)
+  also assume "?S n = (n * (n + 1))^Suc (Suc 0)"
+  also have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^Suc (Suc 0)"
+    by (simp add: power_eq_if distrib)
+  finally show "?P (Suc n)" by simp
+qed
+
+text {*
+ Comparing these examples with the tactic script version
+ \url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, we note
+ an important difference of how induction vs.\ simplification is
+ applied.  While \cite[\S10]{isabelle-ref} advises for these examples
+ that ``induction should not be applied until the goal is in the
+ simplest form'' this would be a very bad idea in our setting.
+
+ Simplification normalizes all arithmetic expressions involved,
+ producing huge intermediate goals.  With applying induction
+ afterwards, the Isar proof text would have to reflect the emerging
+ configuration by appropriate sub-proofs.  This would result in badly
+ structured, low-level technical reasoning, without any good idea of
+ the actual point.
+
+ \medskip As a general rule of good proof style, automatic methods
+ such as $\idt{simp}$ or $\idt{auto}$ should normally be never used as
+ initial proof methods, but only as terminal ones, solving certain
+ goals completely.
+*}
+
+end