# HG changeset patch
# User paulson
# Date 1256052771 -3600
# Node ID fd0a9c794ec14b0277e5acfdb5106b7817035964
# Parent  c95102496490a2176ae33aab986b47304f3e536c
Some new lemmas concerning sets

diff -r c95102496490 -r fd0a9c794ec1 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Tue Oct 20 15:02:48 2009 +0100
+++ b/src/HOL/Fun.thy	Tue Oct 20 16:32:51 2009 +0100
@@ -78,6 +78,9 @@
 lemma image_compose: "(f o g) ` r = f`(g`r)"
 by (simp add: comp_def, blast)
 
+lemma vimage_compose: "(g \<circ> f) -` x = f -` (g -` x)"
+  by auto
+
 lemma UN_o: "UNION A (g o f) = UNION (f`A) g"
 by (unfold comp_def, blast)
 
diff -r c95102496490 -r fd0a9c794ec1 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue Oct 20 15:02:48 2009 +0100
+++ b/src/HOL/Set.thy	Tue Oct 20 16:32:51 2009 +0100
@@ -458,7 +458,7 @@
   unfolding mem_def by (erule le_funE, erule le_boolE)
   -- {* Rule in Modus Ponens style. *}
 
-lemma rev_subsetD [intro?]: "c \<in> A ==> A \<subseteq> B ==> c \<in> B"
+lemma rev_subsetD [noatp,intro?]: "c \<in> A ==> A \<subseteq> B ==> c \<in> B"
   -- {* The same, with reversed premises for use with @{text erule} --
       cf @{text rev_mp}. *}
   by (rule subsetD)
@@ -467,13 +467,13 @@
   \medskip Converts @{prop "A \<subseteq> B"} to @{prop "x \<in> A ==> x \<in> B"}.
 *}
 
-lemma subsetCE [elim]: "A \<subseteq> B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
+lemma subsetCE [noatp,elim]: "A \<subseteq> B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
   -- {* Classical elimination rule. *}
   unfolding mem_def by (blast dest: le_funE le_boolE)
 
-lemma subset_eq: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
+lemma subset_eq [noatp]: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
 
-lemma contra_subsetD: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
+lemma contra_subsetD [noatp]: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
   by blast
 
 lemma subset_refl [simp]: "A \<subseteq> A"
@@ -488,8 +488,11 @@
 lemma set_mp: "A \<subseteq> B ==> x:A ==> x:B"
   by (rule subsetD)
 
+lemma eq_mem_trans: "a=b ==> b \<in> A ==> a \<in> A"
+  by simp
+
 lemmas basic_trans_rules [trans] =
-  order_trans_rules set_rev_mp set_mp
+  order_trans_rules set_rev_mp set_mp eq_mem_trans
 
 
 subsubsection {* Equality *}
diff -r c95102496490 -r fd0a9c794ec1 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Tue Oct 20 15:02:48 2009 +0100
+++ b/src/HOL/SetInterval.thy	Tue Oct 20 16:32:51 2009 +0100
@@ -395,6 +395,11 @@
 lemma atLeastAtMostSuc_conv: "m \<le> Suc n \<Longrightarrow> {m..Suc n} = insert (Suc n) {m..n}"
 by (auto simp add: atLeastAtMost_def)
 
+lemma atLeastLessThan_add_Un: "i \<le> j \<Longrightarrow> {i..<j+k} = {i..<j} \<union> {j..<j+k::nat}"
+  apply (induct k) 
+  apply (simp_all add: atLeastLessThanSuc)   
+  done
+
 subsubsection {* Image *}
 
 lemma image_add_atLeastAtMost:
@@ -522,20 +527,20 @@
 lemma UN_finite_subset: "(!!n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> C) \<Longrightarrow> (\<Union>n. A n) \<subseteq> C"
   by (subst UN_UN_finite_eq [symmetric]) blast
 
-lemma UN_finite2_subset:
-  assumes sb: "!!n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> (\<Union>i\<in>{0..<n}. B i)"
-  shows "(\<Union>n. A n) \<subseteq> (\<Union>n. B n)"
-proof (rule UN_finite_subset)
-  fix n
-  have "(\<Union>i\<in>{0..<n}. A i) \<subseteq> (\<Union>i\<in>{0..<n}. B i)" by (rule sb)
-  also have "...  \<subseteq> (\<Union>n::nat. \<Union>i\<in>{0..<n}. B i)" by blast
-  also have "... = (\<Union>n. B n)" by (simp add: UN_UN_finite_eq) 
-  finally show "(\<Union>i\<in>{0..<n}. A i) \<subseteq> (\<Union>n. B n)" .
-qed
+lemma UN_finite2_subset: 
+     "(!!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)"
+  apply (rule UN_finite_subset)
+  apply (subst UN_UN_finite_eq [symmetric, of B]) 
+  apply blast
+  done
 
 lemma UN_finite2_eq:
-  "(!!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)"
-  by (iprover intro: subset_antisym UN_finite2_subset elim: equalityE)  
+  "(!!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)"
+  apply (rule subset_antisym)
+   apply (rule UN_finite2_subset, blast)
+ apply (rule UN_finite2_subset [where k=k])
+ apply (force simp add: atLeastLessThan_add_Un [of 0] UN_Un) 
+ done
 
 
 subsubsection {* Cardinality *}