--- a/src/HOL/Fun.thy Wed Oct 21 12:08:52 2009 +0200
+++ b/src/HOL/Fun.thy Wed Oct 21 11:19:11 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)
--- a/src/HOL/Set.thy Wed Oct 21 12:08:52 2009 +0200
+++ b/src/HOL/Set.thy Wed Oct 21 11:19:11 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 *}
--- a/src/HOL/SetInterval.thy Wed Oct 21 12:08:52 2009 +0200
+++ b/src/HOL/SetInterval.thy Wed Oct 21 11:19:11 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 *}