author nipkow Sat May 08 19:29:12 2010 +0200 (2010-05-08) changeset 36755 d1b498f2f50b parent 36754 5ce217fc769a child 36757 21443c2858a7
 src/HOL/SetInterval.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/SetInterval.thy	Sat May 08 17:15:50 2010 +0200
1.2 +++ b/src/HOL/SetInterval.thy	Sat May 08 19:29:12 2010 +0200
1.3 @@ -562,6 +562,38 @@
1.4
1.5  subsubsection {* Proving Inclusions and Equalities between Unions *}
1.6
1.7 +lemma UN_le_eq_Un0:
1.8 +  "(\<Union>i\<le>n::nat. M i) = (\<Union>i\<in>{1..n}. M i) \<union> M 0" (is "?A = ?B")
1.9 +proof
1.10 +  show "?A <= ?B"
1.11 +  proof
1.12 +    fix x assume "x : ?A"
1.13 +    then obtain i where i: "i\<le>n" "x : M i" by auto
1.14 +    show "x : ?B"
1.15 +    proof(cases i)
1.16 +      case 0 with i show ?thesis by simp
1.17 +    next
1.18 +      case (Suc j) with i show ?thesis by auto
1.19 +    qed
1.20 +  qed
1.21 +next
1.22 +  show "?B <= ?A" by auto
1.23 +qed
1.24 +
1.26 +  "(\<Union>i\<le>n::nat. M(i+k)) = (\<Union>i\<in>{k..n+k}. M i)" (is "?A = ?B")
1.27 +proof
1.28 +  show "?A <= ?B" by fastsimp
1.29 +next
1.30 +  show "?B <= ?A"
1.31 +  proof
1.32 +    fix x assume "x : ?B"
1.33 +    then obtain i where i: "i : {k..n+k}" "x : M(i)" by auto
1.34 +    hence "i-k\<le>n & x : M((i-k)+k)" by auto
1.35 +    thus "x : ?A" by blast
1.36 +  qed
1.37 +qed
1.38 +
1.39  lemma UN_UN_finite_eq: "(\<Union>n::nat. \<Union>i\<in>{0..<n}. A i) = (\<Union>n. A n)"
1.40    by (auto simp add: atLeast0LessThan)
1.41
```