# HG changeset patch
# User haftmann
# Date 1273341688 -7200
# Node ID 21443c2858a73deab4b494f2860a3da9d72fddee
# Parent  d1b498f2f50b648d846f5f8a1ef4d6240adcd3e9# Parent  c1ae8a0b426594306015420d6c0e6fce86374a2e
merged

diff -r c1ae8a0b4265 -r 21443c2858a7 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Sat May 08 18:52:38 2010 +0200
+++ b/src/HOL/SetInterval.thy	Sat May 08 20:01:28 2010 +0200
@@ -562,6 +562,38 @@
 
 subsubsection {* Proving Inclusions and Equalities between Unions *}
 
+lemma UN_le_eq_Un0:
+  "(\<Union>i\<le>n::nat. M i) = (\<Union>i\<in>{1..n}. M i) \<union> M 0" (is "?A = ?B")
+proof
+  show "?A <= ?B"
+  proof
+    fix x assume "x : ?A"
+    then obtain i where i: "i\<le>n" "x : M i" by auto
+    show "x : ?B"
+    proof(cases i)
+      case 0 with i show ?thesis by simp
+    next
+      case (Suc j) with i show ?thesis by auto
+    qed
+  qed
+next
+  show "?B <= ?A" by auto
+qed
+
+lemma UN_le_add_shift:
+  "(\<Union>i\<le>n::nat. M(i+k)) = (\<Union>i\<in>{k..n+k}. M i)" (is "?A = ?B")
+proof
+  show "?A <= ?B" by fastsimp
+next
+  show "?B <= ?A"
+  proof
+    fix x assume "x : ?B"
+    then obtain i where i: "i : {k..n+k}" "x : M(i)" by auto
+    hence "i-k\<le>n & x : M((i-k)+k)" by auto
+    thus "x : ?A" by blast
+  qed
+qed
+
 lemma UN_UN_finite_eq: "(\<Union>n::nat. \<Union>i\<in>{0..<n}. A i) = (\<Union>n. A n)"
   by (auto simp add: atLeast0LessThan)