another reorganization of setsums and intervals
authornipkow
Wed Mar 02 12:06:15 2005 +0100 (2005-03-02)
changeset 15561045a07ac35a7
parent 15560 c862d556fb18
child 15562 8455c9671494
another reorganization of setsums and intervals
src/HOL/HoareParallel/OG_Examples.thy
src/HOL/HoareParallel/RG_Examples.thy
src/HOL/Hyperreal/MacLaurin.thy
src/HOL/Hyperreal/Series.thy
src/HOL/Hyperreal/Transcendental.thy
src/HOL/Isar_examples/Summation.thy
src/HOL/SetInterval.thy
src/HOL/ex/NatSum.thy
     1.1 --- a/src/HOL/HoareParallel/OG_Examples.thy	Wed Mar 02 10:33:10 2005 +0100
     1.2 +++ b/src/HOL/HoareParallel/OG_Examples.thy	Wed Mar 02 12:06:15 2005 +0100
     1.3 @@ -484,17 +484,19 @@
     1.4  
     1.5  subsubsection {* Increment a Variable in Parallel *}
     1.6  
     1.7 -text {* First some lemmas about summation properties. Summation is
     1.8 -defined in PreList. *}
     1.9 +declare setsum_op_ivl_Suc [simp]
    1.10  
    1.11 +text {* First some lemmas about summation properties. *}
    1.12 +(*
    1.13  lemma Example2_lemma1: "!!b. j<n \<Longrightarrow> (\<Sum>i::nat<n. b i) = (0::nat) \<Longrightarrow> b j = 0 "
    1.14  apply(induct n)
    1.15   apply simp_all
    1.16  apply(force simp add: less_Suc_eq)
    1.17  done
    1.18 -
    1.19 +*)
    1.20  lemma Example2_lemma2_aux: "!!b. j<n \<Longrightarrow> 
    1.21 - (\<Sum>i<n. (b i::nat)) = (\<Sum>i<j. b i) + b j + (\<Sum>i<n-(Suc j) . b (Suc j + i))"
    1.22 + (\<Sum>i=0..<n. (b i::nat)) =
    1.23 + (\<Sum>i=0..<j. b i) + b j + (\<Sum>i=0..<n-(Suc j) . b (Suc j + i))"
    1.24  apply(induct n)
    1.25   apply simp_all
    1.26  apply(simp add:less_Suc_eq)
    1.27 @@ -505,18 +507,18 @@
    1.28  done
    1.29  
    1.30  lemma Example2_lemma2_aux2: 
    1.31 -  "!!b. j\<le> s \<Longrightarrow> (\<Sum>i::nat<j. (b (s:=t)) i) = (\<Sum>i<j. b i)"
    1.32 +  "!!b. j\<le> s \<Longrightarrow> (\<Sum>i::nat=0..<j. (b (s:=t)) i) = (\<Sum>i=0..<j. b i)"
    1.33  apply(induct j)
    1.34   apply (simp_all cong:setsum_cong)
    1.35  done
    1.36  
    1.37  lemma Example2_lemma2: 
    1.38 - "!!b. \<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> Suc (\<Sum>i::nat< n. b i)=(\<Sum>i< n. (b (j := Suc 0)) i)"
    1.39 + "!!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)"
    1.40  apply(frule_tac b="(b (j:=(Suc 0)))" in Example2_lemma2_aux)
    1.41 -apply(erule_tac  t="setsum (b(j := (Suc 0))) {..<n}" in ssubst)
    1.42 +apply(erule_tac  t="setsum (b(j := (Suc 0))) {0..<n}" in ssubst)
    1.43  apply(frule_tac b=b in Example2_lemma2_aux)
    1.44 -apply(erule_tac  t="setsum b {..<n}" in ssubst)
    1.45 -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)))")
    1.46 +apply(erule_tac  t="setsum b {0..<n}" in ssubst)
    1.47 +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)))")
    1.48  apply(rotate_tac -1)
    1.49  apply(erule ssubst)
    1.50  apply(subgoal_tac "j\<le>j")
    1.51 @@ -526,7 +528,7 @@
    1.52  apply simp_all
    1.53  done
    1.54  
    1.55 -lemma Example2_lemma3: "!!b. \<forall>i< n. b i = (Suc 0) \<Longrightarrow> (\<Sum>i<n. b i)= n"
    1.56 +lemma Example2_lemma3: "!!b. \<forall>i< n. b i = (Suc 0) \<Longrightarrow> (\<Sum>i=0..<n. b i)= n"
    1.57  apply (induct n)
    1.58  apply auto
    1.59  done
    1.60 @@ -536,12 +538,12 @@
    1.61   x :: nat
    1.62  
    1.63  lemma Example_2: "0<n \<Longrightarrow> 
    1.64 - \<parallel>- .{\<acute>x=0 \<and> (\<Sum>i< n. \<acute>c i)=0}.  
    1.65 + \<parallel>- .{\<acute>x=0 \<and> (\<Sum>i=0..<n. \<acute>c i)=0}.  
    1.66   COBEGIN 
    1.67     SCHEME [0\<le>i<n] 
    1.68 -  .{\<acute>x=(\<Sum>i< n. \<acute>c i) \<and> \<acute>c i=0}. 
    1.69 +  .{\<acute>x=(\<Sum>i=0..<n. \<acute>c i) \<and> \<acute>c i=0}. 
    1.70     \<langle> \<acute>x:=\<acute>x+(Suc 0),, \<acute>c:=\<acute>c (i:=(Suc 0)) \<rangle>
    1.71 -  .{\<acute>x=(\<Sum>i< n. \<acute>c i) \<and> \<acute>c i=(Suc 0)}.
    1.72 +  .{\<acute>x=(\<Sum>i=0..<n. \<acute>c i) \<and> \<acute>c i=(Suc 0)}.
    1.73   COEND 
    1.74   .{\<acute>x=n}."
    1.75  apply oghoare
     2.1 --- a/src/HOL/HoareParallel/RG_Examples.thy	Wed Mar 02 10:33:10 2005 +0100
     2.2 +++ b/src/HOL/HoareParallel/RG_Examples.thy	Wed Mar 02 12:06:15 2005 +0100
     2.3 @@ -154,14 +154,11 @@
     2.4  
     2.5  subsubsection {* Parameterized *}
     2.6  
     2.7 -lemma Example2_lemma1: "j<n \<Longrightarrow> (\<Sum>i::nat<n. b i) = (0::nat) \<Longrightarrow> b j = 0 "
     2.8 -apply(induct n)
     2.9 - apply simp_all
    2.10 -apply(force simp add: less_Suc_eq)
    2.11 -done
    2.12 +declare setsum_op_ivl_Suc [simp]
    2.13  
    2.14 -lemma Example2_lemma2_aux: 
    2.15 - "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))"
    2.16 +lemma Example2_lemma2_aux: "j<n \<Longrightarrow> 
    2.17 + (\<Sum>i=0..<n. (b i::nat)) =
    2.18 + (\<Sum>i=0..<j. b i) + b j + (\<Sum>i=0..<n-(Suc j) . b (Suc j + i))"
    2.19  apply(induct n)
    2.20   apply simp_all
    2.21  apply(simp add:less_Suc_eq)
    2.22 @@ -169,20 +166,21 @@
    2.23  apply(subgoal_tac "n - j = Suc(n- Suc j)")
    2.24    apply simp
    2.25  apply arith
    2.26 -done 
    2.27 +done
    2.28  
    2.29 -lemma Example2_lemma2_aux2: "j\<le> s \<Longrightarrow> (\<Sum>i::nat<j. (b (s:=t)) i) = (\<Sum>i<j. b i)"
    2.30 +lemma Example2_lemma2_aux2: 
    2.31 +  "j\<le> s \<Longrightarrow> (\<Sum>i::nat=0..<j. (b (s:=t)) i) = (\<Sum>i=0..<j. b i)"
    2.32  apply(induct j)
    2.33   apply (simp_all cong:setsum_cong)
    2.34  done
    2.35  
    2.36  lemma Example2_lemma2: 
    2.37 - "!!b. \<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> Suc (\<Sum>i::nat< n. b i)=(\<Sum>i< n. (b (j := Suc 0)) i)"
    2.38 + "\<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)"
    2.39  apply(frule_tac b="(b (j:=(Suc 0)))" in Example2_lemma2_aux)
    2.40 -apply(erule_tac  t="setsum (b(j := (Suc 0))) {..<n}" in ssubst)
    2.41 +apply(erule_tac  t="setsum (b(j := (Suc 0))) {0..<n}" in ssubst)
    2.42  apply(frule_tac b=b in Example2_lemma2_aux)
    2.43 -apply(erule_tac  t="setsum b {..<n}" in ssubst)
    2.44 -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)))")
    2.45 +apply(erule_tac  t="setsum b {0..<n}" in ssubst)
    2.46 +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)))")
    2.47  apply(rotate_tac -1)
    2.48  apply(erule ssubst)
    2.49  apply(subgoal_tac "j\<le>j")
    2.50 @@ -192,14 +190,10 @@
    2.51  apply simp_all
    2.52  done
    2.53  
    2.54 -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)"
    2.55 +lemma Example2_lemma2_Suc0: "\<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow>
    2.56 + Suc (\<Sum>i::nat=0..< n. b i)=(\<Sum>i=0..< n. (b (j:=Suc 0)) i)"
    2.57  by(simp add:Example2_lemma2)
    2.58  
    2.59 -lemma Example2_lemma3: "\<forall>i< n. b i = 1 \<Longrightarrow> (\<Sum>i::nat<n. b i)= n"
    2.60 -apply (induct n)
    2.61 -apply auto
    2.62 -done
    2.63 -
    2.64  record Example2_parameterized =   
    2.65    C :: "nat \<Rightarrow> nat"
    2.66    y  :: nat
    2.67 @@ -207,21 +201,21 @@
    2.68  lemma Example2_parameterized: "0<n \<Longrightarrow> 
    2.69    \<turnstile> COBEGIN SCHEME  [0\<le>i<n]
    2.70       (\<langle> \<acute>y:=\<acute>y+1;; \<acute>C:=\<acute>C (i:=1) \<rangle>, 
    2.71 -     \<lbrace>\<acute>y=(\<Sum>i<n. \<acute>C i) \<and> \<acute>C i=0\<rbrace>, 
    2.72 +     \<lbrace>\<acute>y=(\<Sum>i=0..<n. \<acute>C i) \<and> \<acute>C i=0\<rbrace>, 
    2.73       \<lbrace>\<ordmasculine>C i = \<ordfeminine>C i \<and> 
    2.74 -      (\<ordmasculine>y=(\<Sum>i<n. \<ordmasculine>C i) \<longrightarrow> \<ordfeminine>y =(\<Sum>i<n. \<ordfeminine>C i))\<rbrace>,  
    2.75 +      (\<ordmasculine>y=(\<Sum>i=0..<n. \<ordmasculine>C i) \<longrightarrow> \<ordfeminine>y =(\<Sum>i=0..<n. \<ordfeminine>C i))\<rbrace>,  
    2.76       \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordmasculine>C j = \<ordfeminine>C j) \<and> 
    2.77 -       (\<ordmasculine>y=(\<Sum>i<n. \<ordmasculine>C i) \<longrightarrow> \<ordfeminine>y =(\<Sum>i<n. \<ordfeminine>C i))\<rbrace>,
    2.78 -     \<lbrace>\<acute>y=(\<Sum>i<n. \<acute>C i) \<and> \<acute>C i=1\<rbrace>) 
    2.79 +       (\<ordmasculine>y=(\<Sum>i=0..<n. \<ordmasculine>C i) \<longrightarrow> \<ordfeminine>y =(\<Sum>i=0..<n. \<ordfeminine>C i))\<rbrace>,
    2.80 +     \<lbrace>\<acute>y=(\<Sum>i=0..<n. \<acute>C i) \<and> \<acute>C i=1\<rbrace>) 
    2.81      COEND
    2.82 - 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>]"
    2.83 + 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>]"
    2.84  apply(rule Parallel)
    2.85  apply force
    2.86  apply force
    2.87 -apply(force elim:Example2_lemma1)
    2.88 +apply(force)
    2.89  apply clarify
    2.90  apply simp
    2.91 -apply(force intro:Example2_lemma3)
    2.92 +apply(simp cong:setsum_ivl_cong)
    2.93  apply clarify
    2.94  apply simp
    2.95  apply(rule Await)
     3.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Wed Mar 02 10:33:10 2005 +0100
     3.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Wed Mar 02 12:06:15 2005 +0100
     3.3 @@ -99,9 +99,9 @@
     3.4    prefer 3 apply (simp add: fact_diff_Suc)
     3.5   prefer 2 apply simp
     3.6  apply (frule_tac m = m in less_add_one, clarify)
     3.7 -apply (simp del: setsum_Suc)
     3.8 +apply (simp del: setsum_op_ivl_Suc)
     3.9  apply (insert sumr_offset4 [of 1])
    3.10 -apply (simp del: setsum_Suc fact_Suc realpow_Suc)
    3.11 +apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc)
    3.12  apply (rule lemma_DERIV_subst)
    3.13  apply (rule DERIV_add)
    3.14  apply (rule_tac [2] DERIV_const)
    3.15 @@ -157,9 +157,9 @@
    3.16  apply (erule exE)
    3.17  apply (subgoal_tac "g 0 = 0 & g h =0")
    3.18   prefer 2
    3.19 - apply (simp del: setsum_Suc)
    3.20 + apply (simp del: setsum_op_ivl_Suc)
    3.21   apply (cut_tac n = m and k = 1 in sumr_offset2)
    3.22 - apply (simp add: eq_diff_eq' del: setsum_Suc)
    3.23 + apply (simp add: eq_diff_eq' del: setsum_op_ivl_Suc)
    3.24  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))))))")
    3.25   prefer 2 apply blast
    3.26  apply (erule exE)
    3.27 @@ -178,9 +178,9 @@
    3.28   apply clarify
    3.29   apply simp
    3.30   apply (frule_tac m = ma in less_add_one, clarify)
    3.31 - apply (simp del: setsum_Suc)
    3.32 + apply (simp del: setsum_op_ivl_Suc)
    3.33  apply (insert sumr_offset4 [of 1])
    3.34 -apply (simp del: setsum_Suc fact_Suc realpow_Suc)
    3.35 +apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc)
    3.36  apply (subgoal_tac "\<forall>m. m < n --> (\<exists>t. 0 < t & t < h & DERIV (difg m) t :> 0) ")
    3.37  apply (rule allI, rule impI)
    3.38  apply (drule_tac x = ma and P="%m. m<n --> (\<exists>t. ?QQ m t)" in spec)
    3.39 @@ -515,7 +515,7 @@
    3.40  apply (simp (no_asm))
    3.41  apply (simp (no_asm))
    3.42  apply (case_tac "n", simp)
    3.43 -apply (simp del: setsum_Suc)
    3.44 +apply (simp del: setsum_op_ivl_Suc)
    3.45  apply (rule ccontr, simp)
    3.46  apply (drule_tac x = x in spec, simp)
    3.47  apply (erule ssubst)
     4.1 --- a/src/HOL/Hyperreal/Series.thy	Wed Mar 02 10:33:10 2005 +0100
     4.2 +++ b/src/HOL/Hyperreal/Series.thy	Wed Mar 02 12:06:15 2005 +0100
     4.3 @@ -11,10 +11,9 @@
     4.4  theory Series
     4.5  imports SEQ Lim
     4.6  begin
     4.7 -thm atLeastLessThan_empty
     4.8 -(* FIXME why not globally? *)
     4.9 -declare atLeastLessThan_empty[simp];
    4.10 +
    4.11  declare atLeastLessThan_iff[iff]
    4.12 +declare setsum_op_ivl_Suc[simp]
    4.13  
    4.14  constdefs
    4.15     sums  :: "(nat => real) => real => bool"     (infixr "sums" 80)
    4.16 @@ -31,9 +30,6 @@
    4.17  translations
    4.18    "\<Sum>i. b" == "suminf (%i. b)"
    4.19  
    4.20 -lemma setsum_Suc[simp]:
    4.21 -  "setsum f {m..<Suc n} = (if n < m then 0 else setsum f {m..<n} + f(n))"
    4.22 -by (simp add: atLeastLessThanSuc add_commute)
    4.23  
    4.24  lemma sumr_diff_mult_const:
    4.25   "setsum f {0..<n} - (real n*r) = setsum (%i. f i - r) {0..<n::nat}"
     5.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Wed Mar 02 10:33:10 2005 +0100
     5.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Wed Mar 02 12:06:15 2005 +0100
     5.3 @@ -360,7 +360,7 @@
     5.4  lemma lemma_realpow_diff_sumr:
     5.5       "(\<Sum>p=0..<Suc n. (x ^ p) * y ^ ((Suc n) - p)) =  
     5.6        y * (\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))::real)"
     5.7 -apply (auto simp add: setsum_mult simp del: setsum_Suc)
     5.8 +apply (auto simp add: setsum_mult simp del: setsum_op_ivl_Suc)
     5.9  apply (rule setsum_cong[OF refl])
    5.10  apply (subst lemma_realpow_diff)
    5.11  apply (auto simp add: mult_ac)
    5.12 @@ -370,21 +370,21 @@
    5.13       "x ^ (Suc n) - y ^ (Suc n) =  
    5.14        (x - y) * (\<Sum>p=0..<Suc n. (x ^ p) * (y ^(n - p))::real)"
    5.15  apply (induct "n", simp)
    5.16 -apply (auto simp del: setsum_Suc)
    5.17 -apply (subst setsum_Suc)
    5.18 +apply (auto simp del: setsum_op_ivl_Suc)
    5.19 +apply (subst setsum_op_ivl_Suc)
    5.20  apply (drule sym)
    5.21 -apply (auto simp add: lemma_realpow_diff_sumr right_distrib diff_minus mult_ac simp del: setsum_Suc)
    5.22 +apply (auto simp add: lemma_realpow_diff_sumr right_distrib diff_minus mult_ac simp del: setsum_op_ivl_Suc)
    5.23  done
    5.24  
    5.25  lemma lemma_realpow_rev_sumr:
    5.26       "(\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))) =  
    5.27        (\<Sum>p=0..<Suc n. (x ^ (n - p)) * (y ^ p)::real)"
    5.28  apply (case_tac "x = y")
    5.29 -apply (auto simp add: mult_commute power_add [symmetric] simp del: setsum_Suc)
    5.30 +apply (auto simp add: mult_commute power_add [symmetric] simp del: setsum_op_ivl_Suc)
    5.31  apply (rule_tac c1 = "x - y" in real_mult_left_cancel [THEN iffD1])
    5.32  apply (rule_tac [2] minus_minus [THEN subst], simp)
    5.33  apply (subst minus_mult_left)
    5.34 -apply (simp add: lemma_realpow_diff_sumr2 [symmetric] del: setsum_Suc)
    5.35 +apply (simp add: lemma_realpow_diff_sumr2 [symmetric] del: setsum_op_ivl_Suc)
    5.36  done
    5.37  
    5.38  text{*Power series has a `circle` of convergence, i.e. if it sums for @{term
    5.39 @@ -490,14 +490,14 @@
    5.40  apply (case_tac "n")
    5.41  apply (auto simp add: lemma_realpow_diff_sumr2 
    5.42                        right_diff_distrib [symmetric] mult_assoc
    5.43 -            simp del: realpow_Suc setsum_Suc)
    5.44 -apply (auto simp add: lemma_realpow_rev_sumr simp del: setsum_Suc)
    5.45 +            simp del: realpow_Suc setsum_op_ivl_Suc)
    5.46 +apply (auto simp add: lemma_realpow_rev_sumr simp del: setsum_op_ivl_Suc)
    5.47  apply (auto simp add: real_of_nat_Suc sumr_diff_mult_const left_distrib 
    5.48                  sumdiff lemma_termdiff1 setsum_mult)
    5.49  apply (auto intro!: setsum_cong[OF refl] simp add: diff_minus real_add_assoc)
    5.50  apply (simp add: diff_minus [symmetric] less_iff_Suc_add)
    5.51  apply (auto simp add: setsum_mult lemma_realpow_diff_sumr2 mult_ac simp
    5.52 -                 del: setsum_Suc realpow_Suc)
    5.53 +                 del: setsum_op_ivl_Suc realpow_Suc)
    5.54  done
    5.55  
    5.56  lemma lemma_termdiff3:
    5.57 @@ -517,13 +517,13 @@
    5.58  apply clarify 
    5.59  apply (subgoal_tac "K ^ p * K ^ d * real (Suc (Suc (p + d))) =
    5.60                      K ^ p * (real (Suc (Suc (p + d))) * K ^ d)") 
    5.61 -apply (simp (no_asm_simp) add: power_add del: setsum_Suc)
    5.62 -apply (auto intro!: mult_mono simp del: setsum_Suc)
    5.63 -apply (auto intro!: power_mono simp add: power_abs simp del: setsum_Suc)
    5.64 +apply (simp (no_asm_simp) add: power_add del: setsum_op_ivl_Suc)
    5.65 +apply (auto intro!: mult_mono simp del: setsum_op_ivl_Suc)
    5.66 +apply (auto intro!: power_mono simp add: power_abs simp del: setsum_op_ivl_Suc)
    5.67  apply (rule_tac j = "real (Suc d) * (K ^ d)" in real_le_trans)
    5.68  apply (subgoal_tac [2] "0 \<le> K")
    5.69  apply (drule_tac [2] n = d in zero_le_power)
    5.70 -apply (auto simp del: setsum_Suc)
    5.71 +apply (auto simp del: setsum_op_ivl_Suc)
    5.72  apply (rule setsum_abs [THEN real_le_trans])
    5.73  apply (rule real_setsum_nat_ivl_bounded, auto dest!: less_add_one intro!: mult_mono simp add: power_add)
    5.74  apply (auto intro!: power_mono zero_le_power simp add: power_abs, arith+)
    5.75 @@ -1412,7 +1412,7 @@
    5.76   "\<Sum>n=0..< Suc(Suc(Suc 0)). - ((- 1) ^ n / (real(fact (2*n))) * 2 ^ (2*n))"
    5.77         in order_less_trans)
    5.78  apply (simp (no_asm) add: fact_num_eq_if realpow_num_eq_if del: fact_Suc realpow_Suc)
    5.79 -apply (simp (no_asm) add: mult_assoc del: setsum_Suc)
    5.80 +apply (simp (no_asm) add: mult_assoc del: setsum_op_ivl_Suc)
    5.81  apply (rule sumr_pos_lt_pair)
    5.82  apply (erule sums_summable, safe)
    5.83  apply (simp (no_asm) add: divide_inverse real_0_less_add_iff mult_assoc [symmetric] 
     6.1 --- a/src/HOL/Isar_examples/Summation.thy	Wed Mar 02 10:33:10 2005 +0100
     6.2 +++ b/src/HOL/Isar_examples/Summation.thy	Wed Mar 02 12:06:15 2005 +0100
     6.3 @@ -5,7 +5,11 @@
     6.4  
     6.5  header {* Summing natural numbers *}
     6.6  
     6.7 -theory Summation = Main:
     6.8 +theory Summation
     6.9 +imports Main
    6.10 +begin
    6.11 +
    6.12 +declare setsum_op_ivl_Suc [simp] setsum_cl_ivl_Suc [simp]
    6.13  
    6.14  text_raw {*
    6.15   \footnote{This example is somewhat reminiscent of the
    6.16 @@ -31,7 +35,7 @@
    6.17  *}
    6.18  
    6.19  theorem sum_of_naturals:
    6.20 -  "2 * (\<Sum>i::nat < n + 1. i) = n * (n + 1)"
    6.21 +  "2 * (\<Sum>i::nat=0..n. i) = n * (n + 1)"
    6.22    (is "?P n" is "?S n = _")
    6.23  proof (induct n)
    6.24    show "?P 0" by simp
    6.25 @@ -86,7 +90,7 @@
    6.26  *}
    6.27  
    6.28  theorem sum_of_odds:
    6.29 -  "(\<Sum>i::nat < n. 2 * i + 1) = n^Suc (Suc 0)"
    6.30 +  "(\<Sum>i::nat=0..<n. 2 * i + 1) = n^Suc (Suc 0)"
    6.31    (is "?P n" is "?S n = _")
    6.32  proof (induct n)
    6.33    show "?P 0" by simp
    6.34 @@ -106,7 +110,7 @@
    6.35  lemmas distrib = add_mult_distrib add_mult_distrib2
    6.36  
    6.37  theorem sum_of_squares:
    6.38 -  "6 * (\<Sum>i::nat < n + 1. i^Suc (Suc 0)) = n * (n + 1) * (2 * n + 1)"
    6.39 +  "6 * (\<Sum>i::nat=0..n. i^Suc (Suc 0)) = n * (n + 1) * (2 * n + 1)"
    6.40    (is "?P n" is "?S n = _")
    6.41  proof (induct n)
    6.42    show "?P 0" by simp
    6.43 @@ -119,7 +123,7 @@
    6.44  qed
    6.45  
    6.46  theorem sum_of_cubes:
    6.47 -  "4 * (\<Sum>i::nat < n + 1. i^3) = (n * (n + 1))^Suc (Suc 0)"
    6.48 +  "4 * (\<Sum>i::nat=0..n. i^3) = (n * (n + 1))^Suc (Suc 0)"
    6.49    (is "?P n" is "?S n = _")
    6.50  proof (induct n)
    6.51    show "?P 0" by (simp add: power_eq_if)
     7.1 --- a/src/HOL/SetInterval.thy	Wed Mar 02 10:33:10 2005 +0100
     7.2 +++ b/src/HOL/SetInterval.thy	Wed Mar 02 12:06:15 2005 +0100
     7.3 @@ -392,7 +392,7 @@
     7.4  
     7.5  lemma image_atLeastLessThan_int_shift:
     7.6      "(%x. x + (l::int)) ` {0..<u-l} = {l..<u}"
     7.7 -  apply (auto simp add: image_def atLeastLessThan_iff)
     7.8 +  apply (auto simp add: image_def)
     7.9    apply (rule_tac x = "x - l" in bexI)
    7.10    apply auto
    7.11    done
    7.12 @@ -612,15 +612,23 @@
    7.13   setsum f {a..<b} = setsum g {c..<d}"
    7.14  by(rule setsum_cong, simp_all)
    7.15  
    7.16 -lemma setsum_cl_ivl_add_one_nat: "(n::nat) <= m + 1 ==>
    7.17 -    (\<Sum>i=n..m+1. f i) = (\<Sum>i=n..m. f i) + f(m + 1)"
    7.18 -by (auto simp:add_ac atLeastAtMostSuc_conv)
    7.19 -
    7.20  (* FIXME delete
    7.21  lemma Summation_Suc[simp]: "(\<Sum>i < Suc n. b i) = b n + (\<Sum>i < n. b i)"
    7.22  by (simp add:lessThan_Suc)
    7.23  *)
    7.24  
    7.25 +lemma setsum_cl_ivl_Suc:
    7.26 +  "setsum f {m..Suc n} = (if Suc n < m then 0 else setsum f {m..n} + f(Suc n))"
    7.27 +by (auto simp:add_ac atLeastAtMostSuc_conv)
    7.28 +
    7.29 +lemma setsum_op_ivl_Suc:
    7.30 +  "setsum f {m..<Suc n} = (if n < m then 0 else setsum f {m..<n} + f(n))"
    7.31 +by (auto simp:add_ac atLeastLessThanSuc)
    7.32 +
    7.33 +lemma setsum_cl_ivl_add_one_nat: "(n::nat) <= m + 1 ==>
    7.34 +    (\<Sum>i=n..m+1. f i) = (\<Sum>i=n..m. f i) + f(m + 1)"
    7.35 +by (auto simp:add_ac atLeastAtMostSuc_conv)
    7.36 +
    7.37  lemma setsum_add_nat_ivl: "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
    7.38    setsum f {m..<n} + setsum f {n..<p} = setsum f {m..<p::nat}"
    7.39  by (simp add:setsum_Un_disjoint[symmetric] ivl_disj_int ivl_disj_un)
     8.1 --- a/src/HOL/ex/NatSum.thy	Wed Mar 02 10:33:10 2005 +0100
     8.2 +++ b/src/HOL/ex/NatSum.thy	Wed Mar 02 12:06:15 2005 +0100
     8.3 @@ -17,16 +17,18 @@
     8.4    \url{http://www.research.att.com/~njas/sequences/}.
     8.5  *}
     8.6  
     8.7 -lemmas [simp] = lessThan_Suc atMost_Suc  left_distrib right_distrib
     8.8 -                left_diff_distrib right_diff_distrib --{*for true subtraction*}
     8.9 -                diff_mult_distrib diff_mult_distrib2 --{*for type nat*}
    8.10 +lemmas [simp] =
    8.11 +  lessThan_Suc atMost_Suc setsum_op_ivl_Suc setsum_cl_ivl_Suc
    8.12 +  left_distrib right_distrib
    8.13 +  left_diff_distrib right_diff_distrib --{*for true subtraction*}
    8.14 +  diff_mult_distrib diff_mult_distrib2 --{*for type nat*}
    8.15  
    8.16  text {*
    8.17    \medskip The sum of the first @{text n} odd numbers equals @{text n}
    8.18    squared.
    8.19  *}
    8.20  
    8.21 -lemma sum_of_odds: "(\<Sum>i \<in> {..<n}. Suc (i + i)) = n * n"
    8.22 +lemma sum_of_odds: "(\<Sum>i \<in> {0..<n}. Suc (i + i)) = n * n"
    8.23    apply (induct n)
    8.24     apply auto
    8.25    done
    8.26 @@ -37,8 +39,7 @@
    8.27  *}
    8.28  
    8.29  lemma sum_of_odd_squares:
    8.30 -  "3 * (\<Sum>i \<in> {..<n}. Suc (2*i) * Suc (2*i)) =
    8.31 -    n * (4 * n * n - 1)"
    8.32 +  "3 * (\<Sum>i=0..<n. Suc(2*i) * Suc(2*i)) = n * (4 * n * n - 1)"
    8.33    apply (induct n)
    8.34     apply (auto split: nat_diff_split) (*eliminate the subtraction*)
    8.35    done
    8.36 @@ -48,10 +49,10 @@
    8.37    \medskip The sum of the first @{text n} odd cubes
    8.38  *}
    8.39  
    8.40 -lemma numeral_2_eq_2: "2 = Suc (Suc 0)" by (auto ); 
    8.41 +lemma numeral_2_eq_2: "2 = Suc (Suc 0)" by auto
    8.42  
    8.43  lemma sum_of_odd_cubes:
    8.44 -  "(\<Sum>i \<in> {..<n}. Suc (2*i) * Suc (2*i) * Suc (2*i)) =
    8.45 +  "(\<Sum>i=0..<n. Suc (2*i) * Suc (2*i) * Suc (2*i)) =
    8.46      n * n * (2 * n * n - 1)"
    8.47    apply (induct n)
    8.48     apply (auto split: nat_diff_split) (*eliminate the subtraction*)
    8.49 @@ -62,30 +63,30 @@
    8.50    @{text "n (n + 1) / 2"}.*}
    8.51  
    8.52  lemma sum_of_naturals:
    8.53 -    "2 * (\<Sum>i \<in> {..n}. i) = n * Suc n"
    8.54 +    "2 * (\<Sum>i=0..n. i) = n * Suc n"
    8.55    apply (induct n)
    8.56     apply auto
    8.57    done
    8.58  
    8.59  lemma sum_of_squares:
    8.60 -    "6 * (\<Sum>i \<in> {..n}. i * i) = n * Suc n * Suc (2 * n)"
    8.61 +    "6 * (\<Sum>i=0..n. i * i) = n * Suc n * Suc (2 * n)"
    8.62    apply (induct n)
    8.63     apply auto
    8.64    done
    8.65  
    8.66  lemma sum_of_cubes:
    8.67 -    "4 * (\<Sum>i \<in> {..n}. i * i * i) = n * n * Suc n * Suc n"
    8.68 +    "4 * (\<Sum>i=0..n. i * i * i) = n * n * Suc n * Suc n"
    8.69    apply (induct n)
    8.70     apply auto
    8.71    done
    8.72  
    8.73  
    8.74  text {*
    8.75 -  \medskip Sum of fourth powers: two versions.
    8.76 +  \medskip Sum of fourth powers: three versions.
    8.77  *}
    8.78  
    8.79  lemma sum_of_fourth_powers:
    8.80 -  "30 * (\<Sum>i \<in> {..n}. i * i * i * i) =
    8.81 +  "30 * (\<Sum>i=0..n. i * i * i * i) =
    8.82      n * Suc n * Suc (2 * n) * (3 * n * n + 3 * n - 1)"
    8.83    apply (induct n)
    8.84     apply simp_all
    8.85 @@ -94,11 +95,19 @@
    8.86    done
    8.87  
    8.88  text {*
    8.89 -  Alternative proof, with a change of variables and much more
    8.90 +  Tow alternative proofs, with a change of variables and much more
    8.91    subtraction, performed using the integers. *}
    8.92  
    8.93  lemma int_sum_of_fourth_powers:
    8.94 -  "30 * of_nat (\<Sum>i \<in> {..<m}. i * i * i * i) =
    8.95 +  "30 * int (\<Sum>i=0..<m. i * i * i * i) =
    8.96 +    int m * (int m - 1) * (int(2 * m) - 1) *
    8.97 +    (int(3 * m * m) - int(3 * m) - 1)"
    8.98 +  apply (induct m)
    8.99 +   apply (simp_all add:zmult_int[symmetric])
   8.100 +  done
   8.101 +
   8.102 +lemma of_nat_sum_of_fourth_powers:
   8.103 +  "30 * of_nat (\<Sum>i=0..<m. i * i * i * i) =
   8.104      of_nat m * (of_nat m - 1) * (of_nat (2 * m) - 1) *
   8.105      (of_nat (3 * m * m) - of_nat (3 * m) - (1::int))"
   8.106    apply (induct m)
   8.107 @@ -111,17 +120,17 @@
   8.108    general case.
   8.109  *}
   8.110  
   8.111 -lemma sum_of_2_powers: "(\<Sum>i \<in> {..<n}. 2^i) = 2^n - (1::nat)"
   8.112 +lemma sum_of_2_powers: "(\<Sum>i=0..<n. 2^i) = 2^n - (1::nat)"
   8.113    apply (induct n)
   8.114     apply (auto split: nat_diff_split)
   8.115    done
   8.116  
   8.117 -lemma sum_of_3_powers: "2 * (\<Sum>i \<in> {..<n}. 3^i) = 3^n - (1::nat)"
   8.118 +lemma sum_of_3_powers: "2 * (\<Sum>i=0..<n. 3^i) = 3^n - (1::nat)"
   8.119    apply (induct n)
   8.120     apply auto
   8.121    done
   8.122  
   8.123 -lemma sum_of_powers: "0 < k ==> (k - 1) * (\<Sum>i \<in> {..<n}. k^i) = k^n - (1::nat)"
   8.124 +lemma sum_of_powers: "0 < k ==> (k - 1) * (\<Sum>i=0..<n. k^i) = k^n - (1::nat)"
   8.125    apply (induct n)
   8.126     apply auto
   8.127    done