src/HOL/SetInterval.thy
changeset 33044 fd0a9c794ec1
parent 32960 69916a850301
child 33318 ddd97d9dfbfb
     1.1 --- a/src/HOL/SetInterval.thy	Tue Oct 20 15:02:48 2009 +0100
     1.2 +++ b/src/HOL/SetInterval.thy	Tue Oct 20 16:32:51 2009 +0100
     1.3 @@ -395,6 +395,11 @@
     1.4  lemma atLeastAtMostSuc_conv: "m \<le> Suc n \<Longrightarrow> {m..Suc n} = insert (Suc n) {m..n}"
     1.5  by (auto simp add: atLeastAtMost_def)
     1.6  
     1.7 +lemma atLeastLessThan_add_Un: "i \<le> j \<Longrightarrow> {i..<j+k} = {i..<j} \<union> {j..<j+k::nat}"
     1.8 +  apply (induct k) 
     1.9 +  apply (simp_all add: atLeastLessThanSuc)   
    1.10 +  done
    1.11 +
    1.12  subsubsection {* Image *}
    1.13  
    1.14  lemma image_add_atLeastAtMost:
    1.15 @@ -522,20 +527,20 @@
    1.16  lemma UN_finite_subset: "(!!n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> C) \<Longrightarrow> (\<Union>n. A n) \<subseteq> C"
    1.17    by (subst UN_UN_finite_eq [symmetric]) blast
    1.18  
    1.19 -lemma UN_finite2_subset:
    1.20 -  assumes sb: "!!n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> (\<Union>i\<in>{0..<n}. B i)"
    1.21 -  shows "(\<Union>n. A n) \<subseteq> (\<Union>n. B n)"
    1.22 -proof (rule UN_finite_subset)
    1.23 -  fix n
    1.24 -  have "(\<Union>i\<in>{0..<n}. A i) \<subseteq> (\<Union>i\<in>{0..<n}. B i)" by (rule sb)
    1.25 -  also have "...  \<subseteq> (\<Union>n::nat. \<Union>i\<in>{0..<n}. B i)" by blast
    1.26 -  also have "... = (\<Union>n. B n)" by (simp add: UN_UN_finite_eq) 
    1.27 -  finally show "(\<Union>i\<in>{0..<n}. A i) \<subseteq> (\<Union>n. B n)" .
    1.28 -qed
    1.29 +lemma UN_finite2_subset: 
    1.30 +     "(!!n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> (\<Union>i\<in>{0..<n+k}. B i)) \<Longrightarrow> (\<Union>n. A n) \<subseteq> (\<Union>n. B n)"
    1.31 +  apply (rule UN_finite_subset)
    1.32 +  apply (subst UN_UN_finite_eq [symmetric, of B]) 
    1.33 +  apply blast
    1.34 +  done
    1.35  
    1.36  lemma UN_finite2_eq:
    1.37 -  "(!!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.38 -  by (iprover intro: subset_antisym UN_finite2_subset elim: equalityE)  
    1.39 +  "(!!n::nat. (\<Union>i\<in>{0..<n}. A i) = (\<Union>i\<in>{0..<n+k}. B i)) \<Longrightarrow> (\<Union>n. A n) = (\<Union>n. B n)"
    1.40 +  apply (rule subset_antisym)
    1.41 +   apply (rule UN_finite2_subset, blast)
    1.42 + apply (rule UN_finite2_subset [where k=k])
    1.43 + apply (force simp add: atLeastLessThan_add_Un [of 0] UN_Un) 
    1.44 + done
    1.45  
    1.46  
    1.47  subsubsection {* Cardinality *}