# HG changeset patch
# User nipkow
# Date 1109761575 -3600
# Node ID 045a07ac35a73eefbd6130e0ccf1dace6f7f3587
# Parent  c862d556fb189d9e62df044e391201036dbf91ab
another reorganization of setsums and intervals

diff -r c862d556fb18 -r 045a07ac35a7 src/HOL/HoareParallel/OG_Examples.thy
--- a/src/HOL/HoareParallel/OG_Examples.thy	Wed Mar 02 10:33:10 2005 +0100
+++ b/src/HOL/HoareParallel/OG_Examples.thy	Wed Mar 02 12:06:15 2005 +0100
@@ -484,17 +484,19 @@
 
 subsubsection {* Increment a Variable in Parallel *}
 
-text {* First some lemmas about summation properties. Summation is
-defined in PreList. *}
+declare setsum_op_ivl_Suc [simp]
 
+text {* First some lemmas about summation properties. *}
+(*
 lemma Example2_lemma1: "!!b. j<n \<Longrightarrow> (\<Sum>i::nat<n. b i) = (0::nat) \<Longrightarrow> b j = 0 "
 apply(induct n)
  apply simp_all
 apply(force simp add: less_Suc_eq)
 done
-
+*)
 lemma Example2_lemma2_aux: "!!b. j<n \<Longrightarrow> 
- (\<Sum>i<n. (b i::nat)) = (\<Sum>i<j. b i) + b j + (\<Sum>i<n-(Suc j) . b (Suc j + i))"
+ (\<Sum>i=0..<n. (b i::nat)) =
+ (\<Sum>i=0..<j. b i) + b j + (\<Sum>i=0..<n-(Suc j) . b (Suc j + i))"
 apply(induct n)
  apply simp_all
 apply(simp add:less_Suc_eq)
@@ -505,18 +507,18 @@
 done
 
 lemma Example2_lemma2_aux2: 
-  "!!b. j\<le> s \<Longrightarrow> (\<Sum>i::nat<j. (b (s:=t)) i) = (\<Sum>i<j. b i)"
+  "!!b. j\<le> s \<Longrightarrow> (\<Sum>i::nat=0..<j. (b (s:=t)) i) = (\<Sum>i=0..<j. b i)"
 apply(induct j)
  apply (simp_all cong:setsum_cong)
 done
 
 lemma Example2_lemma2: 
- "!!b. \<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> Suc (\<Sum>i::nat< n. b i)=(\<Sum>i< n. (b (j := Suc 0)) i)"
+ "!!b. \<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> Suc (\<Sum>i::nat=0..<n. b i)=(\<Sum>i=0..<n. (b (j := Suc 0)) i)"
 apply(frule_tac b="(b (j:=(Suc 0)))" in Example2_lemma2_aux)
-apply(erule_tac  t="setsum (b(j := (Suc 0))) {..<n}" in ssubst)
+apply(erule_tac  t="setsum (b(j := (Suc 0))) {0..<n}" in ssubst)
 apply(frule_tac b=b in Example2_lemma2_aux)
-apply(erule_tac  t="setsum b {..<n}" in ssubst)
-apply(subgoal_tac "Suc (setsum b {..<j} + b j + (\<Sum>i<n - Suc j. b (Suc j + i)))=(setsum b {..<j} + Suc (b j) + (\<Sum>i<n - Suc j. b (Suc j + i)))")
+apply(erule_tac  t="setsum b {0..<n}" in ssubst)
+apply(subgoal_tac "Suc (setsum b {0..<j} + b j + (\<Sum>i=0..<n - Suc j. b (Suc j + i)))=(setsum b {0..<j} + Suc (b j) + (\<Sum>i=0..<n - Suc j. b (Suc j + i)))")
 apply(rotate_tac -1)
 apply(erule ssubst)
 apply(subgoal_tac "j\<le>j")
@@ -526,7 +528,7 @@
 apply simp_all
 done
 
-lemma Example2_lemma3: "!!b. \<forall>i< n. b i = (Suc 0) \<Longrightarrow> (\<Sum>i<n. b i)= n"
+lemma Example2_lemma3: "!!b. \<forall>i< n. b i = (Suc 0) \<Longrightarrow> (\<Sum>i=0..<n. b i)= n"
 apply (induct n)
 apply auto
 done
@@ -536,12 +538,12 @@
  x :: nat
 
 lemma Example_2: "0<n \<Longrightarrow> 
- \<parallel>- .{\<acute>x=0 \<and> (\<Sum>i< n. \<acute>c i)=0}.  
+ \<parallel>- .{\<acute>x=0 \<and> (\<Sum>i=0..<n. \<acute>c i)=0}.  
  COBEGIN 
    SCHEME [0\<le>i<n] 
-  .{\<acute>x=(\<Sum>i< n. \<acute>c i) \<and> \<acute>c i=0}. 
+  .{\<acute>x=(\<Sum>i=0..<n. \<acute>c i) \<and> \<acute>c i=0}. 
    \<langle> \<acute>x:=\<acute>x+(Suc 0),, \<acute>c:=\<acute>c (i:=(Suc 0)) \<rangle>
-  .{\<acute>x=(\<Sum>i< n. \<acute>c i) \<and> \<acute>c i=(Suc 0)}.
+  .{\<acute>x=(\<Sum>i=0..<n. \<acute>c i) \<and> \<acute>c i=(Suc 0)}.
  COEND 
  .{\<acute>x=n}."
 apply oghoare
diff -r c862d556fb18 -r 045a07ac35a7 src/HOL/HoareParallel/RG_Examples.thy
--- a/src/HOL/HoareParallel/RG_Examples.thy	Wed Mar 02 10:33:10 2005 +0100
+++ b/src/HOL/HoareParallel/RG_Examples.thy	Wed Mar 02 12:06:15 2005 +0100
@@ -154,14 +154,11 @@
 
 subsubsection {* Parameterized *}
 
-lemma Example2_lemma1: "j<n \<Longrightarrow> (\<Sum>i::nat<n. b i) = (0::nat) \<Longrightarrow> b j = 0 "
-apply(induct n)
- apply simp_all
-apply(force simp add: less_Suc_eq)
-done
+declare setsum_op_ivl_Suc [simp]
 
-lemma Example2_lemma2_aux: 
- "j<n \<Longrightarrow> (\<Sum>i<n. (b i::nat)) = (\<Sum>i<j. b i) + b j + (\<Sum>i<n-(Suc j) . b (Suc j + i))"
+lemma Example2_lemma2_aux: "j<n \<Longrightarrow> 
+ (\<Sum>i=0..<n. (b i::nat)) =
+ (\<Sum>i=0..<j. b i) + b j + (\<Sum>i=0..<n-(Suc j) . b (Suc j + i))"
 apply(induct n)
  apply simp_all
 apply(simp add:less_Suc_eq)
@@ -169,20 +166,21 @@
 apply(subgoal_tac "n - j = Suc(n- Suc j)")
   apply simp
 apply arith
-done 
+done
 
-lemma Example2_lemma2_aux2: "j\<le> s \<Longrightarrow> (\<Sum>i::nat<j. (b (s:=t)) i) = (\<Sum>i<j. b i)"
+lemma Example2_lemma2_aux2: 
+  "j\<le> s \<Longrightarrow> (\<Sum>i::nat=0..<j. (b (s:=t)) i) = (\<Sum>i=0..<j. b i)"
 apply(induct j)
  apply (simp_all cong:setsum_cong)
 done
 
 lemma Example2_lemma2: 
- "!!b. \<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> Suc (\<Sum>i::nat< n. b i)=(\<Sum>i< n. (b (j := Suc 0)) i)"
+ "\<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> Suc (\<Sum>i::nat=0..<n. b i)=(\<Sum>i=0..<n. (b (j := Suc 0)) i)"
 apply(frule_tac b="(b (j:=(Suc 0)))" in Example2_lemma2_aux)
-apply(erule_tac  t="setsum (b(j := (Suc 0))) {..<n}" in ssubst)
+apply(erule_tac  t="setsum (b(j := (Suc 0))) {0..<n}" in ssubst)
 apply(frule_tac b=b in Example2_lemma2_aux)
-apply(erule_tac  t="setsum b {..<n}" in ssubst)
-apply(subgoal_tac "Suc (setsum b {..<j} + b j + (\<Sum>i<n - Suc j. b (Suc j + i)))=(setsum b {..<j} + Suc (b j) + (\<Sum>i<n - Suc j. b (Suc j + i)))")
+apply(erule_tac  t="setsum b {0..<n}" in ssubst)
+apply(subgoal_tac "Suc (setsum b {0..<j} + b j + (\<Sum>i=0..<n - Suc j. b (Suc j + i)))=(setsum b {0..<j} + Suc (b j) + (\<Sum>i=0..<n - Suc j. b (Suc j + i)))")
 apply(rotate_tac -1)
 apply(erule ssubst)
 apply(subgoal_tac "j\<le>j")
@@ -192,14 +190,10 @@
 apply simp_all
 done
 
-lemma Example2_lemma2_Suc0: "\<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> Suc (\<Sum>i::nat< n. b i)=(\<Sum>i< n. (b (j:=Suc 0)) i)"
+lemma Example2_lemma2_Suc0: "\<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow>
+ Suc (\<Sum>i::nat=0..< n. b i)=(\<Sum>i=0..< n. (b (j:=Suc 0)) i)"
 by(simp add:Example2_lemma2)
 
-lemma Example2_lemma3: "\<forall>i< n. b i = 1 \<Longrightarrow> (\<Sum>i::nat<n. b i)= n"
-apply (induct n)
-apply auto
-done
-
 record Example2_parameterized =   
   C :: "nat \<Rightarrow> nat"
   y  :: nat
@@ -207,21 +201,21 @@
 lemma Example2_parameterized: "0<n \<Longrightarrow> 
   \<turnstile> COBEGIN SCHEME  [0\<le>i<n]
      (\<langle> \<acute>y:=\<acute>y+1;; \<acute>C:=\<acute>C (i:=1) \<rangle>, 
-     \<lbrace>\<acute>y=(\<Sum>i<n. \<acute>C i) \<and> \<acute>C i=0\<rbrace>, 
+     \<lbrace>\<acute>y=(\<Sum>i=0..<n. \<acute>C i) \<and> \<acute>C i=0\<rbrace>, 
      \<lbrace>\<ordmasculine>C i = \<ordfeminine>C i \<and> 
-      (\<ordmasculine>y=(\<Sum>i<n. \<ordmasculine>C i) \<longrightarrow> \<ordfeminine>y =(\<Sum>i<n. \<ordfeminine>C i))\<rbrace>,  
+      (\<ordmasculine>y=(\<Sum>i=0..<n. \<ordmasculine>C i) \<longrightarrow> \<ordfeminine>y =(\<Sum>i=0..<n. \<ordfeminine>C i))\<rbrace>,  
      \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordmasculine>C j = \<ordfeminine>C j) \<and> 
-       (\<ordmasculine>y=(\<Sum>i<n. \<ordmasculine>C i) \<longrightarrow> \<ordfeminine>y =(\<Sum>i<n. \<ordfeminine>C i))\<rbrace>,
-     \<lbrace>\<acute>y=(\<Sum>i<n. \<acute>C i) \<and> \<acute>C i=1\<rbrace>) 
+       (\<ordmasculine>y=(\<Sum>i=0..<n. \<ordmasculine>C i) \<longrightarrow> \<ordfeminine>y =(\<Sum>i=0..<n. \<ordfeminine>C i))\<rbrace>,
+     \<lbrace>\<acute>y=(\<Sum>i=0..<n. \<acute>C i) \<and> \<acute>C i=1\<rbrace>) 
     COEND
- SAT [\<lbrace>\<acute>y=0 \<and> (\<Sum>i<n. \<acute>C i)=0 \<rbrace>, \<lbrace>\<ordmasculine>C=\<ordfeminine>C \<and> \<ordmasculine>y=\<ordfeminine>y\<rbrace>, \<lbrace>True\<rbrace>, \<lbrace>\<acute>y=n\<rbrace>]"
+ SAT [\<lbrace>\<acute>y=0 \<and> (\<Sum>i=0..<n. \<acute>C i)=0 \<rbrace>, \<lbrace>\<ordmasculine>C=\<ordfeminine>C \<and> \<ordmasculine>y=\<ordfeminine>y\<rbrace>, \<lbrace>True\<rbrace>, \<lbrace>\<acute>y=n\<rbrace>]"
 apply(rule Parallel)
 apply force
 apply force
-apply(force elim:Example2_lemma1)
+apply(force)
 apply clarify
 apply simp
-apply(force intro:Example2_lemma3)
+apply(simp cong:setsum_ivl_cong)
 apply clarify
 apply simp
 apply(rule Await)
diff -r c862d556fb18 -r 045a07ac35a7 src/HOL/Hyperreal/MacLaurin.thy
--- a/src/HOL/Hyperreal/MacLaurin.thy	Wed Mar 02 10:33:10 2005 +0100
+++ b/src/HOL/Hyperreal/MacLaurin.thy	Wed Mar 02 12:06:15 2005 +0100
@@ -99,9 +99,9 @@
   prefer 3 apply (simp add: fact_diff_Suc)
  prefer 2 apply simp
 apply (frule_tac m = m in less_add_one, clarify)
-apply (simp del: setsum_Suc)
+apply (simp del: setsum_op_ivl_Suc)
 apply (insert sumr_offset4 [of 1])
-apply (simp del: setsum_Suc fact_Suc realpow_Suc)
+apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc)
 apply (rule lemma_DERIV_subst)
 apply (rule DERIV_add)
 apply (rule_tac [2] DERIV_const)
@@ -157,9 +157,9 @@
 apply (erule exE)
 apply (subgoal_tac "g 0 = 0 & g h =0")
  prefer 2
- apply (simp del: setsum_Suc)
+ apply (simp del: setsum_op_ivl_Suc)
  apply (cut_tac n = m and k = 1 in sumr_offset2)
- apply (simp add: eq_diff_eq' del: setsum_Suc)
+ apply (simp add: eq_diff_eq' del: setsum_op_ivl_Suc)
 apply (subgoal_tac "\<exists>difg. difg = (%m t. diff m t - (setsum (%p. (diff (m + p) 0 / real (fact p)) * (t ^ p)) {0..<n-m} + (B * ((t ^ (n - m)) / real (fact (n - m))))))")
  prefer 2 apply blast
 apply (erule exE)
@@ -178,9 +178,9 @@
  apply clarify
  apply simp
  apply (frule_tac m = ma in less_add_one, clarify)
- apply (simp del: setsum_Suc)
+ apply (simp del: setsum_op_ivl_Suc)
 apply (insert sumr_offset4 [of 1])
-apply (simp del: setsum_Suc fact_Suc realpow_Suc)
+apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc)
 apply (subgoal_tac "\<forall>m. m < n --> (\<exists>t. 0 < t & t < h & DERIV (difg m) t :> 0) ")
 apply (rule allI, rule impI)
 apply (drule_tac x = ma and P="%m. m<n --> (\<exists>t. ?QQ m t)" in spec)
@@ -515,7 +515,7 @@
 apply (simp (no_asm))
 apply (simp (no_asm))
 apply (case_tac "n", simp)
-apply (simp del: setsum_Suc)
+apply (simp del: setsum_op_ivl_Suc)
 apply (rule ccontr, simp)
 apply (drule_tac x = x in spec, simp)
 apply (erule ssubst)
diff -r c862d556fb18 -r 045a07ac35a7 src/HOL/Hyperreal/Series.thy
--- a/src/HOL/Hyperreal/Series.thy	Wed Mar 02 10:33:10 2005 +0100
+++ b/src/HOL/Hyperreal/Series.thy	Wed Mar 02 12:06:15 2005 +0100
@@ -11,10 +11,9 @@
 theory Series
 imports SEQ Lim
 begin
-thm atLeastLessThan_empty
-(* FIXME why not globally? *)
-declare atLeastLessThan_empty[simp];
+
 declare atLeastLessThan_iff[iff]
+declare setsum_op_ivl_Suc[simp]
 
 constdefs
    sums  :: "(nat => real) => real => bool"     (infixr "sums" 80)
@@ -31,9 +30,6 @@
 translations
   "\<Sum>i. b" == "suminf (%i. b)"
 
-lemma setsum_Suc[simp]:
-  "setsum f {m..<Suc n} = (if n < m then 0 else setsum f {m..<n} + f(n))"
-by (simp add: atLeastLessThanSuc add_commute)
 
 lemma sumr_diff_mult_const:
  "setsum f {0..<n} - (real n*r) = setsum (%i. f i - r) {0..<n::nat}"
diff -r c862d556fb18 -r 045a07ac35a7 src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Wed Mar 02 10:33:10 2005 +0100
+++ b/src/HOL/Hyperreal/Transcendental.thy	Wed Mar 02 12:06:15 2005 +0100
@@ -360,7 +360,7 @@
 lemma lemma_realpow_diff_sumr:
      "(\<Sum>p=0..<Suc n. (x ^ p) * y ^ ((Suc n) - p)) =  
       y * (\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))::real)"
-apply (auto simp add: setsum_mult simp del: setsum_Suc)
+apply (auto simp add: setsum_mult simp del: setsum_op_ivl_Suc)
 apply (rule setsum_cong[OF refl])
 apply (subst lemma_realpow_diff)
 apply (auto simp add: mult_ac)
@@ -370,21 +370,21 @@
      "x ^ (Suc n) - y ^ (Suc n) =  
       (x - y) * (\<Sum>p=0..<Suc n. (x ^ p) * (y ^(n - p))::real)"
 apply (induct "n", simp)
-apply (auto simp del: setsum_Suc)
-apply (subst setsum_Suc)
+apply (auto simp del: setsum_op_ivl_Suc)
+apply (subst setsum_op_ivl_Suc)
 apply (drule sym)
-apply (auto simp add: lemma_realpow_diff_sumr right_distrib diff_minus mult_ac simp del: setsum_Suc)
+apply (auto simp add: lemma_realpow_diff_sumr right_distrib diff_minus mult_ac simp del: setsum_op_ivl_Suc)
 done
 
 lemma lemma_realpow_rev_sumr:
      "(\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))) =  
       (\<Sum>p=0..<Suc n. (x ^ (n - p)) * (y ^ p)::real)"
 apply (case_tac "x = y")
-apply (auto simp add: mult_commute power_add [symmetric] simp del: setsum_Suc)
+apply (auto simp add: mult_commute power_add [symmetric] simp del: setsum_op_ivl_Suc)
 apply (rule_tac c1 = "x - y" in real_mult_left_cancel [THEN iffD1])
 apply (rule_tac [2] minus_minus [THEN subst], simp)
 apply (subst minus_mult_left)
-apply (simp add: lemma_realpow_diff_sumr2 [symmetric] del: setsum_Suc)
+apply (simp add: lemma_realpow_diff_sumr2 [symmetric] del: setsum_op_ivl_Suc)
 done
 
 text{*Power series has a `circle` of convergence, i.e. if it sums for @{term
@@ -490,14 +490,14 @@
 apply (case_tac "n")
 apply (auto simp add: lemma_realpow_diff_sumr2 
                       right_diff_distrib [symmetric] mult_assoc
-            simp del: realpow_Suc setsum_Suc)
-apply (auto simp add: lemma_realpow_rev_sumr simp del: setsum_Suc)
+            simp del: realpow_Suc setsum_op_ivl_Suc)
+apply (auto simp add: lemma_realpow_rev_sumr simp del: setsum_op_ivl_Suc)
 apply (auto simp add: real_of_nat_Suc sumr_diff_mult_const left_distrib 
                 sumdiff lemma_termdiff1 setsum_mult)
 apply (auto intro!: setsum_cong[OF refl] simp add: diff_minus real_add_assoc)
 apply (simp add: diff_minus [symmetric] less_iff_Suc_add)
 apply (auto simp add: setsum_mult lemma_realpow_diff_sumr2 mult_ac simp
-                 del: setsum_Suc realpow_Suc)
+                 del: setsum_op_ivl_Suc realpow_Suc)
 done
 
 lemma lemma_termdiff3:
@@ -517,13 +517,13 @@
 apply clarify 
 apply (subgoal_tac "K ^ p * K ^ d * real (Suc (Suc (p + d))) =
                     K ^ p * (real (Suc (Suc (p + d))) * K ^ d)") 
-apply (simp (no_asm_simp) add: power_add del: setsum_Suc)
-apply (auto intro!: mult_mono simp del: setsum_Suc)
-apply (auto intro!: power_mono simp add: power_abs simp del: setsum_Suc)
+apply (simp (no_asm_simp) add: power_add del: setsum_op_ivl_Suc)
+apply (auto intro!: mult_mono simp del: setsum_op_ivl_Suc)
+apply (auto intro!: power_mono simp add: power_abs simp del: setsum_op_ivl_Suc)
 apply (rule_tac j = "real (Suc d) * (K ^ d)" in real_le_trans)
 apply (subgoal_tac [2] "0 \<le> K")
 apply (drule_tac [2] n = d in zero_le_power)
-apply (auto simp del: setsum_Suc)
+apply (auto simp del: setsum_op_ivl_Suc)
 apply (rule setsum_abs [THEN real_le_trans])
 apply (rule real_setsum_nat_ivl_bounded, auto dest!: less_add_one intro!: mult_mono simp add: power_add)
 apply (auto intro!: power_mono zero_le_power simp add: power_abs, arith+)
@@ -1412,7 +1412,7 @@
  "\<Sum>n=0..< Suc(Suc(Suc 0)). - ((- 1) ^ n / (real(fact (2*n))) * 2 ^ (2*n))"
        in order_less_trans)
 apply (simp (no_asm) add: fact_num_eq_if realpow_num_eq_if del: fact_Suc realpow_Suc)
-apply (simp (no_asm) add: mult_assoc del: setsum_Suc)
+apply (simp (no_asm) add: mult_assoc del: setsum_op_ivl_Suc)
 apply (rule sumr_pos_lt_pair)
 apply (erule sums_summable, safe)
 apply (simp (no_asm) add: divide_inverse real_0_less_add_iff mult_assoc [symmetric] 
diff -r c862d556fb18 -r 045a07ac35a7 src/HOL/Isar_examples/Summation.thy
--- a/src/HOL/Isar_examples/Summation.thy	Wed Mar 02 10:33:10 2005 +0100
+++ b/src/HOL/Isar_examples/Summation.thy	Wed Mar 02 12:06:15 2005 +0100
@@ -5,7 +5,11 @@
 
 header {* Summing natural numbers *}
 
-theory Summation = Main:
+theory Summation
+imports Main
+begin
+
+declare setsum_op_ivl_Suc [simp] setsum_cl_ivl_Suc [simp]
 
 text_raw {*
  \footnote{This example is somewhat reminiscent of the
@@ -31,7 +35,7 @@
 *}
 
 theorem sum_of_naturals:
-  "2 * (\<Sum>i::nat < n + 1. i) = n * (n + 1)"
+  "2 * (\<Sum>i::nat=0..n. i) = n * (n + 1)"
   (is "?P n" is "?S n = _")
 proof (induct n)
   show "?P 0" by simp
@@ -86,7 +90,7 @@
 *}
 
 theorem sum_of_odds:
-  "(\<Sum>i::nat < n. 2 * i + 1) = n^Suc (Suc 0)"
+  "(\<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
@@ -106,7 +110,7 @@
 lemmas distrib = add_mult_distrib add_mult_distrib2
 
 theorem sum_of_squares:
-  "6 * (\<Sum>i::nat < n + 1. i^Suc (Suc 0)) = n * (n + 1) * (2 * n + 1)"
+  "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
@@ -119,7 +123,7 @@
 qed
 
 theorem sum_of_cubes:
-  "4 * (\<Sum>i::nat < n + 1. i^3) = (n * (n + 1))^Suc (Suc 0)"
+  "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)
diff -r c862d556fb18 -r 045a07ac35a7 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Wed Mar 02 10:33:10 2005 +0100
+++ b/src/HOL/SetInterval.thy	Wed Mar 02 12:06:15 2005 +0100
@@ -392,7 +392,7 @@
 
 lemma image_atLeastLessThan_int_shift:
     "(%x. x + (l::int)) ` {0..<u-l} = {l..<u}"
-  apply (auto simp add: image_def atLeastLessThan_iff)
+  apply (auto simp add: image_def)
   apply (rule_tac x = "x - l" in bexI)
   apply auto
   done
@@ -612,15 +612,23 @@
  setsum f {a..<b} = setsum g {c..<d}"
 by(rule setsum_cong, simp_all)
 
-lemma setsum_cl_ivl_add_one_nat: "(n::nat) <= m + 1 ==>
-    (\<Sum>i=n..m+1. f i) = (\<Sum>i=n..m. f i) + f(m + 1)"
-by (auto simp:add_ac atLeastAtMostSuc_conv)
-
 (* FIXME delete
 lemma Summation_Suc[simp]: "(\<Sum>i < Suc n. b i) = b n + (\<Sum>i < n. b i)"
 by (simp add:lessThan_Suc)
 *)
 
+lemma setsum_cl_ivl_Suc:
+  "setsum f {m..Suc n} = (if Suc n < m then 0 else setsum f {m..n} + f(Suc n))"
+by (auto simp:add_ac atLeastAtMostSuc_conv)
+
+lemma setsum_op_ivl_Suc:
+  "setsum f {m..<Suc n} = (if n < m then 0 else setsum f {m..<n} + f(n))"
+by (auto simp:add_ac atLeastLessThanSuc)
+
+lemma setsum_cl_ivl_add_one_nat: "(n::nat) <= m + 1 ==>
+    (\<Sum>i=n..m+1. f i) = (\<Sum>i=n..m. f i) + f(m + 1)"
+by (auto simp:add_ac atLeastAtMostSuc_conv)
+
 lemma setsum_add_nat_ivl: "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
   setsum f {m..<n} + setsum f {n..<p} = setsum f {m..<p::nat}"
 by (simp add:setsum_Un_disjoint[symmetric] ivl_disj_int ivl_disj_un)
diff -r c862d556fb18 -r 045a07ac35a7 src/HOL/ex/NatSum.thy
--- a/src/HOL/ex/NatSum.thy	Wed Mar 02 10:33:10 2005 +0100
+++ b/src/HOL/ex/NatSum.thy	Wed Mar 02 12:06:15 2005 +0100
@@ -17,16 +17,18 @@
   \url{http://www.research.att.com/~njas/sequences/}.
 *}
 
-lemmas [simp] = lessThan_Suc atMost_Suc  left_distrib right_distrib
-                left_diff_distrib right_diff_distrib --{*for true subtraction*}
-                diff_mult_distrib diff_mult_distrib2 --{*for type nat*}
+lemmas [simp] =
+  lessThan_Suc atMost_Suc setsum_op_ivl_Suc setsum_cl_ivl_Suc
+  left_distrib right_distrib
+  left_diff_distrib right_diff_distrib --{*for true subtraction*}
+  diff_mult_distrib diff_mult_distrib2 --{*for type nat*}
 
 text {*
   \medskip The sum of the first @{text n} odd numbers equals @{text n}
   squared.
 *}
 
-lemma sum_of_odds: "(\<Sum>i \<in> {..<n}. Suc (i + i)) = n * n"
+lemma sum_of_odds: "(\<Sum>i \<in> {0..<n}. Suc (i + i)) = n * n"
   apply (induct n)
    apply auto
   done
@@ -37,8 +39,7 @@
 *}
 
 lemma sum_of_odd_squares:
-  "3 * (\<Sum>i \<in> {..<n}. Suc (2*i) * Suc (2*i)) =
-    n * (4 * n * n - 1)"
+  "3 * (\<Sum>i=0..<n. Suc(2*i) * Suc(2*i)) = n * (4 * n * n - 1)"
   apply (induct n)
    apply (auto split: nat_diff_split) (*eliminate the subtraction*)
   done
@@ -48,10 +49,10 @@
   \medskip The sum of the first @{text n} odd cubes
 *}
 
-lemma numeral_2_eq_2: "2 = Suc (Suc 0)" by (auto ); 
+lemma numeral_2_eq_2: "2 = Suc (Suc 0)" by auto
 
 lemma sum_of_odd_cubes:
-  "(\<Sum>i \<in> {..<n}. Suc (2*i) * Suc (2*i) * Suc (2*i)) =
+  "(\<Sum>i=0..<n. Suc (2*i) * Suc (2*i) * Suc (2*i)) =
     n * n * (2 * n * n - 1)"
   apply (induct n)
    apply (auto split: nat_diff_split) (*eliminate the subtraction*)
@@ -62,30 +63,30 @@
   @{text "n (n + 1) / 2"}.*}
 
 lemma sum_of_naturals:
-    "2 * (\<Sum>i \<in> {..n}. i) = n * Suc n"
+    "2 * (\<Sum>i=0..n. i) = n * Suc n"
   apply (induct n)
    apply auto
   done
 
 lemma sum_of_squares:
-    "6 * (\<Sum>i \<in> {..n}. i * i) = n * Suc n * Suc (2 * n)"
+    "6 * (\<Sum>i=0..n. i * i) = n * Suc n * Suc (2 * n)"
   apply (induct n)
    apply auto
   done
 
 lemma sum_of_cubes:
-    "4 * (\<Sum>i \<in> {..n}. i * i * i) = n * n * Suc n * Suc n"
+    "4 * (\<Sum>i=0..n. i * i * i) = n * n * Suc n * Suc n"
   apply (induct n)
    apply auto
   done
 
 
 text {*
-  \medskip Sum of fourth powers: two versions.
+  \medskip Sum of fourth powers: three versions.
 *}
 
 lemma sum_of_fourth_powers:
-  "30 * (\<Sum>i \<in> {..n}. i * i * i * i) =
+  "30 * (\<Sum>i=0..n. i * i * i * i) =
     n * Suc n * Suc (2 * n) * (3 * n * n + 3 * n - 1)"
   apply (induct n)
    apply simp_all
@@ -94,11 +95,19 @@
   done
 
 text {*
-  Alternative proof, with a change of variables and much more
+  Tow alternative proofs, with a change of variables and much more
   subtraction, performed using the integers. *}
 
 lemma int_sum_of_fourth_powers:
-  "30 * of_nat (\<Sum>i \<in> {..<m}. i * i * i * i) =
+  "30 * int (\<Sum>i=0..<m. i * i * i * i) =
+    int m * (int m - 1) * (int(2 * m) - 1) *
+    (int(3 * m * m) - int(3 * m) - 1)"
+  apply (induct m)
+   apply (simp_all add:zmult_int[symmetric])
+  done
+
+lemma of_nat_sum_of_fourth_powers:
+  "30 * of_nat (\<Sum>i=0..<m. i * i * i * i) =
     of_nat m * (of_nat m - 1) * (of_nat (2 * m) - 1) *
     (of_nat (3 * m * m) - of_nat (3 * m) - (1::int))"
   apply (induct m)
@@ -111,17 +120,17 @@
   general case.
 *}
 
-lemma sum_of_2_powers: "(\<Sum>i \<in> {..<n}. 2^i) = 2^n - (1::nat)"
+lemma sum_of_2_powers: "(\<Sum>i=0..<n. 2^i) = 2^n - (1::nat)"
   apply (induct n)
    apply (auto split: nat_diff_split)
   done
 
-lemma sum_of_3_powers: "2 * (\<Sum>i \<in> {..<n}. 3^i) = 3^n - (1::nat)"
+lemma sum_of_3_powers: "2 * (\<Sum>i=0..<n. 3^i) = 3^n - (1::nat)"
   apply (induct n)
    apply auto
   done
 
-lemma sum_of_powers: "0 < k ==> (k - 1) * (\<Sum>i \<in> {..<n}. k^i) = k^n - (1::nat)"
+lemma sum_of_powers: "0 < k ==> (k - 1) * (\<Sum>i=0..<n. k^i) = k^n - (1::nat)"
   apply (induct n)
    apply auto
   done