New theorems for proving equalities and inclusions involving unions
authorpaulson
Thu Sep 17 14:59:58 2009 +0100 (2009-09-17)
changeset 32596bd68c04dace1
parent 32595 2953c3917e21
child 32597 1e2872252f91
New theorems for proving equalities and inclusions involving unions
src/HOL/SetInterval.thy
     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"