# HG changeset patch
# User nipkow
# Date 1273339752 -7200
# Node ID d1b498f2f50b648d846f5f8a1ef4d6240adcd3e9
# Parent  5ce217fc769af0cfab0d3adff40204b6b46dc926
added lemmas

diff -r 5ce217fc769a -r d1b498f2f50b src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Sat May 08 17:15:50 2010 +0200
+++ b/src/HOL/SetInterval.thy	Sat May 08 19:29:12 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)