diff -r 9ad1fccbba96 -r f2e51e704a96 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Tue Oct 27 23:18:32 2015 +0100
+++ b/src/HOL/Set_Interval.thy	Thu Oct 29 15:40:52 2015 +0100
@@ -409,6 +409,11 @@
   "{a .. b} \<subseteq> { c ..< d } \<longleftrightarrow> (a \<le> b \<longrightarrow> c \<le> a \<and> b < d)"
   using dense[of "max a d" "b"]
   by (force simp: subset_eq Ball_def not_less[symmetric])
+  
+lemma greaterThanLessThan_subseteq_greaterThanLessThan:
+  "{a <..< b} \<subseteq> {c <..< d} \<longleftrightarrow> (a < b \<longrightarrow> a \<ge> c \<and> b \<le> d)"
+  using dense[of "a" "min c b"] dense[of "max a d" "b"]
+  by (force simp: subset_eq Ball_def not_less[symmetric])
 
 lemma greaterThanAtMost_subseteq_atLeastLessThan_iff:
   "{a <.. b} \<subseteq> { c ..< d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b < d)"
@@ -1648,6 +1653,18 @@
   by auto
 
 
+subsection \<open>Telescoping\<close>
+
+lemma setsum_telescope:
+  fixes f::"nat \<Rightarrow> 'a::ab_group_add"
+  shows "setsum (\<lambda>i. f i - f (Suc i)) {.. i} = f 0 - f (Suc i)"
+  by (induct i) simp_all
+
+lemma setsum_telescope'':
+  assumes "m \<le> n"
+  shows   "(\<Sum>k\<in>{Suc m..n}. f k - f (k - 1)) = f n - (f m :: 'a :: ab_group_add)"
+  by (rule dec_induct[OF assms]) (simp_all add: algebra_simps)
+
 subsection \<open>The formula for geometric sums\<close>
 
 lemma geometric_sum:
@@ -1845,4 +1862,38 @@
     by auto
 qed
 
+
+subsection \<open>Shifting bounds\<close>
+
+lemma setprod_shift_bounds_nat_ivl:
+  "setprod f {m+k..<n+k} = setprod (%i. f(i + k)){m..<n::nat}"
+by (induct "n", auto simp:atLeastLessThanSuc)
+
+lemma setprod_shift_bounds_cl_nat_ivl:
+  "setprod f {m+k..n+k} = setprod (%i. f(i + k)){m..n::nat}"
+  by (rule setprod.reindex_bij_witness[where i="\<lambda>i. i + k" and j="\<lambda>i. i - k"]) auto
+
+corollary setprod_shift_bounds_cl_Suc_ivl:
+  "setprod f {Suc m..Suc n} = setprod (%i. f(Suc i)){m..n}"
+by (simp add:setprod_shift_bounds_cl_nat_ivl[where k="Suc 0", simplified])
+
+corollary setprod_shift_bounds_Suc_ivl:
+  "setprod f {Suc m..<Suc n} = setprod (%i. f(Suc i)){m..<n}"
+by (simp add:setprod_shift_bounds_nat_ivl[where k="Suc 0", simplified])
+
+lemma setprod_lessThan_Suc: "setprod f {..<Suc n} = setprod f {..<n} * f n"
+  by (simp add: lessThan_Suc mult.commute)
+
+lemma setprod_atLeastLessThan_Suc: "a \<le> b \<Longrightarrow> setprod f {a..<Suc b} = setprod f {a..<b} * f b"
+  by (simp add: atLeastLessThanSuc mult.commute)
+
+lemma setprod_nat_ivl_Suc':
+  assumes "m \<le> Suc n"
+  shows   "setprod f {m..Suc n} = f (Suc n) * setprod f {m..n}"
+proof -
+  from assms have "{m..Suc n} = insert (Suc n) {m..n}" by auto
+  also have "setprod f \<dots> = f (Suc n) * setprod f {m..n}" by simp
+  finally show ?thesis .
+qed
+
 end