--- a/src/HOL/Set_Interval.thy Wed Mar 15 21:52:04 2017 +0100
+++ b/src/HOL/Set_Interval.thy Thu Mar 16 13:55:29 2017 +0000
@@ -709,7 +709,7 @@
subsubsection \<open>The Constant @{term greaterThan}\<close>
-lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc"
+lemma greaterThan_0: "greaterThan 0 = range Suc"
apply (simp add: greaterThan_def)
apply (blast dest: gr0_conv_Suc [THEN iffD1])
done
@@ -1846,6 +1846,12 @@
shows "(\<Sum>i = m..n. f(Suc i) - f i) = f (Suc n) - f m"
using assms by (induct n) (auto simp: le_Suc_eq)
+lemma sum_Suc_diff':
+ fixes f :: "nat \<Rightarrow> 'a::ab_group_add"
+ assumes "m \<le> n"
+ shows "(\<Sum>i = m..<n. f (Suc i) - f i) = f n - f m"
+using assms by (induct n) (auto simp: le_Suc_eq)
+
lemma nested_sum_swap:
"(\<Sum>i = 0..n. (\<Sum>j = 0..<i. a i j)) = (\<Sum>j = 0..<n. \<Sum>i = Suc j..n. a i j)"
by (induction n) (auto simp: sum.distrib)