diff -r 63d63d854fae -r aa1acc25126b src/HOL/BNF_Cardinal_Order_Relation.thy --- a/src/HOL/BNF_Cardinal_Order_Relation.thy Fri Feb 28 22:00:13 2014 +0100 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy Fri Feb 28 17:54:52 2014 +0100 @@ -394,18 +394,13 @@ qed lemma surj_imp_ordLeq: -assumes "B <= f ` A" -shows "|B| <=o |A|" +assumes "B \ f ` A" +shows "|B| \o |A|" proof- have "|B| <=o |f ` A|" using assms card_of_mono1 by auto thus ?thesis using card_of_image ordLeq_transitive by blast qed -lemma card_of_ordLeqI2: -assumes "B \ f ` A" -shows "|B| \o |A|" -using assms by (metis surj_imp_ordLeq) - lemma card_of_singl_ordLeq: assumes "A \ {}" shows "|{b}| \o |A|" @@ -529,7 +524,7 @@ } ultimately show ?thesis unfolding inj_on_def by auto qed - thus ?thesis using card_of_ordLeq by metis + thus ?thesis using card_of_ordLeq by blast qed corollary ordLeq_Plus_mono1: @@ -678,7 +673,7 @@ "g = (\(a,c::'c). (f a,c))" by blast have "inj_on g (A \ C) \ g ` (A \ C) \ (B \ C)" using 1 unfolding inj_on_def using g_def by auto - thus ?thesis using card_of_ordLeq by metis + thus ?thesis using card_of_ordLeq by blast qed corollary ordLeq_Times_mono1: @@ -706,11 +701,12 @@ have "\i. i \ I \ (\f. inj_on f (A i) \ f ` (A i) \ B i)" using assms by (auto simp add: card_of_ordLeq) with choice[of "\ i f. i \ I \ inj_on f (A i) \ f ` (A i) \ B i"] - obtain F where 1: "\i \ I. inj_on (F i) (A i) \ (F i) ` (A i) \ B i" by metis + obtain F where 1: "\i \ I. inj_on (F i) (A i) \ (F i) ` (A i) \ B i" + by atomize_elim (auto intro: bchoice) obtain g where g_def: "g = (\(i,a::'b). (i,F i a))" by blast have "inj_on g (Sigma I A) \ g ` (Sigma I A) \ (Sigma I B)" using 1 unfolding inj_on_def using g_def by force - thus ?thesis using card_of_ordLeq by metis + thus ?thesis using card_of_ordLeq by blast qed corollary card_of_Sigma_Times: @@ -719,7 +715,7 @@ lemma card_of_UNION_Sigma: "|\i \ I. A i| \o |SIGMA i : I. A i|" -using Ex_inj_on_UNION_Sigma[of I A] card_of_ordLeq by metis +using Ex_inj_on_UNION_Sigma[of I A] card_of_ordLeq by blast lemma card_of_bool: assumes "a1 \ a2" @@ -745,8 +741,7 @@ hence "?f False = a" by auto thus ?thesis by blast qed } - ultimately show ?thesis unfolding bij_betw_def inj_on_def - by (metis (no_types) image_subsetI order_eq_iff subsetI) + ultimately show ?thesis unfolding bij_betw_def inj_on_def by blast qed thus ?thesis using card_of_ordIso by blast qed @@ -758,7 +753,7 @@ proof- have 1: "|UNIV::bool set| \o |A|" using A2 card_of_mono1[of "{a1,a2}"] card_of_bool[of a1 a2] - ordIso_ordLeq_trans[of "|UNIV::bool set|"] by metis + ordIso_ordLeq_trans[of "|UNIV::bool set|"] by blast (* *) have "|A <+> B| \o |B <+> B|" using LEQ card_of_Plus_mono1 by blast @@ -789,11 +784,11 @@ using assms by (auto simp add: card_of_Plus_Times_aux) hence ?thesis using card_of_Plus_commute card_of_Times_commute - ordIso_ordLeq_trans ordLeq_ordIso_trans by metis + ordIso_ordLeq_trans ordLeq_ordIso_trans by blast } ultimately show ?thesis using card_of_Well_order[of A] card_of_Well_order[of B] - ordLeq_total[of "|A|"] by metis + ordLeq_total[of "|A|"] by blast qed lemma card_of_ordLeq_finite: @@ -852,7 +847,7 @@ let ?r' = "Restr r (underS r a)" assume Case2: "a \ Field r" hence 1: "under r a = underS r a \ {a} \ a \ underS r a" - using 0 Refl_under_underS underS_notIn by metis + using 0 Refl_under_underS[of r a] underS_notIn[of a r] by blast have 2: "wo_rel.ofilter r (underS r a) \ underS r a < Field r" using 0 wo_rel.underS_ofilter * 1 Case2 by fast hence "?r' finite (Field r)" using 1 unfolding phi_def by simp hence "\ finite ?B" using 8 3 card_of_ordIso_finite_Field[of r ?B] by blast - hence "\ finite A1" using 9 finite_cartesian_product finite_subset by metis + hence "\ finite A1" using 9 finite_cartesian_product finite_subset by blast moreover have temp4: "Field |A1| = A1 \ Well_order |A1| \ Card_order |A1|" using card_of_Card_order[of A1] card_of_Well_order[of A1] by (simp add: Field_card_of) @@ -1110,7 +1105,7 @@ by (auto simp add: card_of_Plus_Times) moreover have "|A \ B| =o |A|" using assms * by (simp add: card_of_Times_infinite_simps) - ultimately have "|A <+> B| \o |A|" using ordLeq_ordIso_trans by metis + ultimately have "|A <+> B| \o |A|" using ordLeq_ordIso_trans by blast thus ?thesis using card_of_Plus1 ordIso_iff_ordLeq by blast qed qed @@ -1256,7 +1251,7 @@ corollary finite_iff_ordLess_natLeq: "finite A = ( |A| o |Pow A|" - by (metis cardSuc_ordLess_ordLeq card_of_Card_order card_of_Pow) + by (rule iffD1[OF cardSuc_ordLess_ordLeq card_of_Pow]) (simp_all add: card_of_Card_order) qed qed @@ -1655,7 +1650,7 @@ unfolding bij_betw_def inj_on_def proof safe fix h :: "'a \ 'b" assume h: "h \ Func UNIV B" hence "\ a. \ b. h a = b" unfolding Func_def by auto - then obtain f where f: "\ a. h a = f a" by metis + then obtain f where f: "\ a. h a = f a" by blast hence "range f \ B" using h unfolding Func_def by auto thus "h \ (\f a. f a) ` {f. range f \ B}" using f unfolding image_def by auto qed(unfold Func_def fun_eq_iff, auto)