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)