Some new lemmas concerning sets
authorpaulson
Tue Oct 20 16:32:51 2009 +0100 (2009-10-20)
changeset 33044fd0a9c794ec1
parent 33022 c95102496490
child 33045 2b3694001c48
Some new lemmas concerning sets
src/HOL/Fun.thy
src/HOL/Set.thy
src/HOL/SetInterval.thy
     1.1 --- a/src/HOL/Fun.thy	Tue Oct 20 15:02:48 2009 +0100
     1.2 +++ b/src/HOL/Fun.thy	Tue Oct 20 16:32:51 2009 +0100
     1.3 @@ -78,6 +78,9 @@
     1.4  lemma image_compose: "(f o g) ` r = f`(g`r)"
     1.5  by (simp add: comp_def, blast)
     1.6  
     1.7 +lemma vimage_compose: "(g \<circ> f) -` x = f -` (g -` x)"
     1.8 +  by auto
     1.9 +
    1.10  lemma UN_o: "UNION A (g o f) = UNION (f`A) g"
    1.11  by (unfold comp_def, blast)
    1.12  
     2.1 --- a/src/HOL/Set.thy	Tue Oct 20 15:02:48 2009 +0100
     2.2 +++ b/src/HOL/Set.thy	Tue Oct 20 16:32:51 2009 +0100
     2.3 @@ -458,7 +458,7 @@
     2.4    unfolding mem_def by (erule le_funE, erule le_boolE)
     2.5    -- {* Rule in Modus Ponens style. *}
     2.6  
     2.7 -lemma rev_subsetD [intro?]: "c \<in> A ==> A \<subseteq> B ==> c \<in> B"
     2.8 +lemma rev_subsetD [noatp,intro?]: "c \<in> A ==> A \<subseteq> B ==> c \<in> B"
     2.9    -- {* The same, with reversed premises for use with @{text erule} --
    2.10        cf @{text rev_mp}. *}
    2.11    by (rule subsetD)
    2.12 @@ -467,13 +467,13 @@
    2.13    \medskip Converts @{prop "A \<subseteq> B"} to @{prop "x \<in> A ==> x \<in> B"}.
    2.14  *}
    2.15  
    2.16 -lemma subsetCE [elim]: "A \<subseteq> B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
    2.17 +lemma subsetCE [noatp,elim]: "A \<subseteq> B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
    2.18    -- {* Classical elimination rule. *}
    2.19    unfolding mem_def by (blast dest: le_funE le_boolE)
    2.20  
    2.21 -lemma subset_eq: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
    2.22 +lemma subset_eq [noatp]: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
    2.23  
    2.24 -lemma contra_subsetD: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
    2.25 +lemma contra_subsetD [noatp]: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
    2.26    by blast
    2.27  
    2.28  lemma subset_refl [simp]: "A \<subseteq> A"
    2.29 @@ -488,8 +488,11 @@
    2.30  lemma set_mp: "A \<subseteq> B ==> x:A ==> x:B"
    2.31    by (rule subsetD)
    2.32  
    2.33 +lemma eq_mem_trans: "a=b ==> b \<in> A ==> a \<in> A"
    2.34 +  by simp
    2.35 +
    2.36  lemmas basic_trans_rules [trans] =
    2.37 -  order_trans_rules set_rev_mp set_mp
    2.38 +  order_trans_rules set_rev_mp set_mp eq_mem_trans
    2.39  
    2.40  
    2.41  subsubsection {* Equality *}
     3.1 --- a/src/HOL/SetInterval.thy	Tue Oct 20 15:02:48 2009 +0100
     3.2 +++ b/src/HOL/SetInterval.thy	Tue Oct 20 16:32:51 2009 +0100
     3.3 @@ -395,6 +395,11 @@
     3.4  lemma atLeastAtMostSuc_conv: "m \<le> Suc n \<Longrightarrow> {m..Suc n} = insert (Suc n) {m..n}"
     3.5  by (auto simp add: atLeastAtMost_def)
     3.6  
     3.7 +lemma atLeastLessThan_add_Un: "i \<le> j \<Longrightarrow> {i..<j+k} = {i..<j} \<union> {j..<j+k::nat}"
     3.8 +  apply (induct k) 
     3.9 +  apply (simp_all add: atLeastLessThanSuc)   
    3.10 +  done
    3.11 +
    3.12  subsubsection {* Image *}
    3.13  
    3.14  lemma image_add_atLeastAtMost:
    3.15 @@ -522,20 +527,20 @@
    3.16  lemma UN_finite_subset: "(!!n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> C) \<Longrightarrow> (\<Union>n. A n) \<subseteq> C"
    3.17    by (subst UN_UN_finite_eq [symmetric]) blast
    3.18  
    3.19 -lemma UN_finite2_subset:
    3.20 -  assumes sb: "!!n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> (\<Union>i\<in>{0..<n}. B i)"
    3.21 -  shows "(\<Union>n. A n) \<subseteq> (\<Union>n. B n)"
    3.22 -proof (rule UN_finite_subset)
    3.23 -  fix n
    3.24 -  have "(\<Union>i\<in>{0..<n}. A i) \<subseteq> (\<Union>i\<in>{0..<n}. B i)" by (rule sb)
    3.25 -  also have "...  \<subseteq> (\<Union>n::nat. \<Union>i\<in>{0..<n}. B i)" by blast
    3.26 -  also have "... = (\<Union>n. B n)" by (simp add: UN_UN_finite_eq) 
    3.27 -  finally show "(\<Union>i\<in>{0..<n}. A i) \<subseteq> (\<Union>n. B n)" .
    3.28 -qed
    3.29 +lemma UN_finite2_subset: 
    3.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)"
    3.31 +  apply (rule UN_finite_subset)
    3.32 +  apply (subst UN_UN_finite_eq [symmetric, of B]) 
    3.33 +  apply blast
    3.34 +  done
    3.35  
    3.36  lemma UN_finite2_eq:
    3.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)"
    3.38 -  by (iprover intro: subset_antisym UN_finite2_subset elim: equalityE)  
    3.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)"
    3.40 +  apply (rule subset_antisym)
    3.41 +   apply (rule UN_finite2_subset, blast)
    3.42 + apply (rule UN_finite2_subset [where k=k])
    3.43 + apply (force simp add: atLeastLessThan_add_Un [of 0] UN_Un) 
    3.44 + done
    3.45  
    3.46  
    3.47  subsubsection {* Cardinality *}