--- a/src/HOL/Set_Interval.thy Tue Apr 28 16:23:05 2015 +0100
+++ b/src/HOL/Set_Interval.thy Tue Apr 28 16:23:38 2015 +0100
@@ -1298,7 +1298,14 @@
"[| (l::'a::linorder) <= m; m <= u |] ==> {l..m} Un {m<..u} = {l..u}"
by auto
-lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two
+lemma ivl_disj_un_two_touch:
+ "[| (l::'a::linorder) < m; m < u |] ==> {l<..m} Un {m..<u} = {l<..<u}"
+ "[| (l::'a::linorder) <= m; m < u |] ==> {l..m} Un {m..<u} = {l..<u}"
+ "[| (l::'a::linorder) < m; m <= u |] ==> {l<..m} Un {m..u} = {l<..u}"
+ "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m} Un {m..u} = {l..u}"
+by auto
+
+lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two ivl_disj_un_two_touch
subsubsection {* Disjoint Intersections *}
@@ -1498,6 +1505,20 @@
apply (simp_all add: setsum_add_nat_ivl add.commute atLeast0LessThan[symmetric])
done
+lemma setsum_triangle_reindex:
+ fixes n :: nat
+ shows "(\<Sum>(i,j)\<in>{(i,j). i+j < n}. f i j) = (\<Sum>k<n. \<Sum>i\<le>k. f i (k - i))"
+ apply (simp add: setsum.Sigma)
+ apply (rule setsum.reindex_bij_witness[where j="\<lambda>(i, j). (i+j, i)" and i="\<lambda>(k, i). (i, k - i)"])
+ apply auto
+ done
+
+lemma setsum_triangle_reindex_eq:
+ fixes n :: nat
+ shows "(\<Sum>(i,j)\<in>{(i,j). i+j \<le> n}. f i j) = (\<Sum>k\<le>n. \<Sum>i\<le>k. f i (k - i))"
+using setsum_triangle_reindex [of f "Suc n"]
+by (simp only: Nat.less_Suc_eq_le lessThan_Suc_atMost)
+
subsection{* Shifting bounds *}
lemma setsum_shift_bounds_nat_ivl: