# HG changeset patch
# User nipkow
# Date 1162470909 -3600
# Node ID 17b0b4c6491bfb0b6ddf314f290f8bde8987f4d0
# Parent  56695d1f45cf5060bdb86950d96f9ef070c38ec7
added sum_squared

diff -r 56695d1f45cf -r 17b0b4c6491b src/HOL/ex/NatSum.thy
--- a/src/HOL/ex/NatSum.thy	Wed Nov 01 19:07:37 2006 +0100
+++ b/src/HOL/ex/NatSum.thy	Thu Nov 02 13:35:09 2006 +0100
@@ -62,6 +62,22 @@
     "4 * (\<Sum>i=0..n. i * i * i) = n * n * Suc n * Suc n"
   by (induct n) auto
 
+text{* \medskip A cute identity: *}
+
+lemma sum_squared: "(\<Sum>i=0..n. i)^2 = (\<Sum>i=0..n::nat. i^3)"
+proof(induct n)
+  case 0 show ?case by simp
+next
+  case (Suc n)
+  have "(\<Sum>i = 0..Suc n. i)^2 =
+        (\<Sum>i = 0..n. i^3) + (2*(\<Sum>i = 0..n. i)*(n+1) + (n+1)^2)"
+    (is "_ = ?A + ?B")
+    using Suc by(simp add:nat_number)
+  also have "?B = (n+1)^3"
+    using sum_of_naturals by(simp add:nat_number)
+  also have "?A + (n+1)^3 = (\<Sum>i=0..Suc n. i^3)" by simp
+  finally show ?case .
+qed
 
 text {*
   \medskip Sum of fourth powers: three versions.