author paulson Thu Sep 17 14:59:58 2009 +0100 (2009-09-17) changeset 32596 bd68c04dace1 parent 32595 2953c3917e21 child 32597 1e2872252f91
New theorems for proving equalities and inclusions involving unions
 src/HOL/SetInterval.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/SetInterval.thy	Thu Sep 17 14:07:44 2009 +0200
1.2 +++ b/src/HOL/SetInterval.thy	Thu Sep 17 14:59:58 2009 +0100
1.3 @@ -514,6 +514,30 @@
1.4  qed
1.5
1.6
1.7 +subsubsection {* Proving Inclusions and Equalities between Unions *}
1.8 +
1.9 +lemma UN_UN_finite_eq: "(\<Union>n::nat. \<Union>i\<in>{0..<n}. A i) = (\<Union>n. A n)"
1.10 +  by (auto simp add: atLeast0LessThan)
1.11 +
1.12 +lemma UN_finite_subset: "(!!n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> C) \<Longrightarrow> (\<Union>n. A n) \<subseteq> C"
1.13 +  by (subst UN_UN_finite_eq [symmetric]) blast
1.14 +
1.15 +lemma UN_finite2_subset:
1.16 +  assumes sb: "!!n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> (\<Union>i\<in>{0..<n}. B i)"
1.17 +  shows "(\<Union>n. A n) \<subseteq> (\<Union>n. B n)"
1.18 +proof (rule UN_finite_subset)
1.19 +  fix n
1.20 +  have "(\<Union>i\<in>{0..<n}. A i) \<subseteq> (\<Union>i\<in>{0..<n}. B i)" by (rule sb)
1.21 +  also have "...  \<subseteq> (\<Union>n::nat. \<Union>i\<in>{0..<n}. B i)" by blast
1.22 +  also have "... = (\<Union>n. B n)" by (simp add: UN_UN_finite_eq)
1.23 +  finally show "(\<Union>i\<in>{0..<n}. A i) \<subseteq> (\<Union>n. B n)" .
1.24 +qed
1.25 +
1.26 +lemma UN_finite2_eq:
1.27 +  "(!!n::nat. (\<Union>i\<in>{0..<n}. A i) = (\<Union>i\<in>{0..<n}. B i)) \<Longrightarrow> (\<Union>n. A n) = (\<Union>n. B n)"
1.28 +  by (iprover intro: subset_antisym UN_finite2_subset elim: equalityE)
1.29 +
1.30 +
1.31  subsubsection {* Cardinality *}
1.32
1.33  lemma card_lessThan [simp]: "card {..<u} = u"
```