# HG changeset patch # User paulson # Date 1256120351 -3600 # Node ID 2b3694001c48ffd31cb7c724b267cb44d76387b1 # Parent ff71cadefb14894ee2c99297493693a14eabdcfd# Parent fd0a9c794ec14b0277e5acfdb5106b7817035964 merged diff -r ff71cadefb14 -r 2b3694001c48 src/HOL/Fun.thy --- 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 \ 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 ff71cadefb14 -r 2b3694001c48 src/HOL/Set.thy --- 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 \ A ==> A \ B ==> c \ B" +lemma rev_subsetD [noatp,intro?]: "c \ A ==> A \ B ==> c \ 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 \ B"} to @{prop "x \ A ==> x \ B"}. *} -lemma subsetCE [elim]: "A \ B ==> (c \ A ==> P) ==> (c \ B ==> P) ==> P" +lemma subsetCE [noatp,elim]: "A \ B ==> (c \ A ==> P) ==> (c \ B ==> P) ==> P" -- {* Classical elimination rule. *} unfolding mem_def by (blast dest: le_funE le_boolE) -lemma subset_eq: "A \ B = (\x\A. x \ B)" by blast +lemma subset_eq [noatp]: "A \ B = (\x\A. x \ B)" by blast -lemma contra_subsetD: "A \ B ==> c \ B ==> c \ A" +lemma contra_subsetD [noatp]: "A \ B ==> c \ B ==> c \ A" by blast lemma subset_refl [simp]: "A \ A" @@ -488,8 +488,11 @@ lemma set_mp: "A \ B ==> x:A ==> x:B" by (rule subsetD) +lemma eq_mem_trans: "a=b ==> b \ A ==> a \ 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 ff71cadefb14 -r 2b3694001c48 src/HOL/SetInterval.thy --- 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 \ Suc n \ {m..Suc n} = insert (Suc n) {m..n}" by (auto simp add: atLeastAtMost_def) +lemma atLeastLessThan_add_Un: "i \ j \ {i.. {j..i\{0.. C) \ (\n. A n) \ C" by (subst UN_UN_finite_eq [symmetric]) blast -lemma UN_finite2_subset: - assumes sb: "!!n::nat. (\i\{0.. (\i\{0..n. A n) \ (\n. B n)" -proof (rule UN_finite_subset) - fix n - have "(\i\{0.. (\i\{0.. (\n::nat. \i\{0..n. B n)" by (simp add: UN_UN_finite_eq) - finally show "(\i\{0.. (\n. B n)" . -qed +lemma UN_finite2_subset: + "(!!n::nat. (\i\{0.. (\i\{0.. (\n. A n) \ (\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. (\i\{0..i\{0.. (\n. A n) = (\n. B n)" - by (iprover intro: subset_antisym UN_finite2_subset elim: equalityE) + "(!!n::nat. (\i\{0..i\{0.. (\n. A n) = (\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 *}