src/HOL/SetInterval.thy

   apply auto
   done
 
 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
 
 lemma finite_atLeastLessThan_int [iff]: "finite {l..<u::int}"

 lemma setsum_ivl_cong:
  "\<lbrakk>a = c; b = d; !!x. \<lbrakk> c \<le> x; x < d \<rbrakk> \<Longrightarrow> f x = g x \<rbrakk> \<Longrightarrow>
  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)