src/HOL/BNF_Cardinal_Order_Relation.thy
changeset 55811 aa1acc25126b
parent 55603 48596c45bf7f
child 55936 f6591f8c629d
     1.1 --- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Fri Feb 28 22:00:13 2014 +0100
     1.2 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Fri Feb 28 17:54:52 2014 +0100
     1.3 @@ -394,18 +394,13 @@
     1.4  qed
     1.5  
     1.6  lemma surj_imp_ordLeq:
     1.7 -assumes "B <= f ` A"
     1.8 -shows "|B| <=o |A|"
     1.9 +assumes "B \<subseteq> f ` A"
    1.10 +shows "|B| \<le>o |A|"
    1.11  proof-
    1.12    have "|B| <=o |f ` A|" using assms card_of_mono1 by auto
    1.13    thus ?thesis using card_of_image ordLeq_transitive by blast
    1.14  qed
    1.15  
    1.16 -lemma card_of_ordLeqI2:
    1.17 -assumes "B \<subseteq> f ` A"
    1.18 -shows "|B| \<le>o |A|"
    1.19 -using assms by (metis surj_imp_ordLeq)
    1.20 -
    1.21  lemma card_of_singl_ordLeq:
    1.22  assumes "A \<noteq> {}"
    1.23  shows "|{b}| \<le>o |A|"
    1.24 @@ -529,7 +524,7 @@
    1.25      }
    1.26      ultimately show ?thesis unfolding inj_on_def by auto
    1.27    qed
    1.28 -  thus ?thesis using card_of_ordLeq by metis
    1.29 +  thus ?thesis using card_of_ordLeq by blast
    1.30  qed
    1.31  
    1.32  corollary ordLeq_Plus_mono1:
    1.33 @@ -678,7 +673,7 @@
    1.34    "g = (\<lambda>(a,c::'c). (f a,c))" by blast
    1.35    have "inj_on g (A \<times> C) \<and> g ` (A \<times> C) \<le> (B \<times> C)"
    1.36    using 1 unfolding inj_on_def using g_def by auto
    1.37 -  thus ?thesis using card_of_ordLeq by metis
    1.38 +  thus ?thesis using card_of_ordLeq by blast
    1.39  qed
    1.40  
    1.41  corollary ordLeq_Times_mono1:
    1.42 @@ -706,11 +701,12 @@
    1.43    have "\<forall>i. i \<in> I \<longrightarrow> (\<exists>f. inj_on f (A i) \<and> f ` (A i) \<le> B i)"
    1.44    using assms by (auto simp add: card_of_ordLeq)
    1.45    with choice[of "\<lambda> i f. i \<in> I \<longrightarrow> inj_on f (A i) \<and> f ` (A i) \<le> B i"]
    1.46 -  obtain F where 1: "\<forall>i \<in> I. inj_on (F i) (A i) \<and> (F i) ` (A i) \<le> B i" by metis
    1.47 +  obtain F where 1: "\<forall>i \<in> I. inj_on (F i) (A i) \<and> (F i) ` (A i) \<le> B i"
    1.48 +    by atomize_elim (auto intro: bchoice)
    1.49    obtain g where g_def: "g = (\<lambda>(i,a::'b). (i,F i a))" by blast
    1.50    have "inj_on g (Sigma I A) \<and> g ` (Sigma I A) \<le> (Sigma I B)"
    1.51    using 1 unfolding inj_on_def using g_def by force
    1.52 -  thus ?thesis using card_of_ordLeq by metis
    1.53 +  thus ?thesis using card_of_ordLeq by blast
    1.54  qed
    1.55  
    1.56  corollary card_of_Sigma_Times:
    1.57 @@ -719,7 +715,7 @@
    1.58  
    1.59  lemma card_of_UNION_Sigma:
    1.60  "|\<Union>i \<in> I. A i| \<le>o |SIGMA i : I. A i|"
    1.61 -using Ex_inj_on_UNION_Sigma[of I A] card_of_ordLeq by metis
    1.62 +using Ex_inj_on_UNION_Sigma[of I A] card_of_ordLeq by blast
    1.63  
    1.64  lemma card_of_bool:
    1.65  assumes "a1 \<noteq> a2"
    1.66 @@ -745,8 +741,7 @@
    1.67         hence "?f False = a" by auto  thus ?thesis by blast
    1.68       qed
    1.69      }
    1.70 -    ultimately show ?thesis unfolding bij_betw_def inj_on_def
    1.71 -    by (metis (no_types) image_subsetI order_eq_iff subsetI)
    1.72 +    ultimately show ?thesis unfolding bij_betw_def inj_on_def by blast
    1.73    qed
    1.74    thus ?thesis using card_of_ordIso by blast
    1.75  qed
    1.76 @@ -758,7 +753,7 @@
    1.77  proof-
    1.78    have 1: "|UNIV::bool set| \<le>o |A|"
    1.79    using A2 card_of_mono1[of "{a1,a2}"] card_of_bool[of a1 a2]
    1.80 -        ordIso_ordLeq_trans[of "|UNIV::bool set|"] by metis
    1.81 +        ordIso_ordLeq_trans[of "|UNIV::bool set|"] by blast
    1.82    (*  *)
    1.83    have "|A <+> B| \<le>o |B <+> B|"
    1.84    using LEQ card_of_Plus_mono1 by blast
    1.85 @@ -789,11 +784,11 @@
    1.86     using assms by (auto simp add: card_of_Plus_Times_aux)
    1.87     hence ?thesis
    1.88     using card_of_Plus_commute card_of_Times_commute
    1.89 -         ordIso_ordLeq_trans ordLeq_ordIso_trans by metis
    1.90 +         ordIso_ordLeq_trans ordLeq_ordIso_trans by blast
    1.91    }
    1.92    ultimately show ?thesis
    1.93    using card_of_Well_order[of A] card_of_Well_order[of B]
    1.94 -        ordLeq_total[of "|A|"] by metis
    1.95 +        ordLeq_total[of "|A|"] by blast
    1.96  qed
    1.97  
    1.98  lemma card_of_ordLeq_finite:
    1.99 @@ -852,7 +847,7 @@
   1.100      let ?r' = "Restr r (underS r a)"
   1.101      assume Case2: "a \<in> Field r"
   1.102      hence 1: "under r a = underS r a \<union> {a} \<and> a \<notin> underS r a"
   1.103 -    using 0 Refl_under_underS underS_notIn by metis
   1.104 +    using 0 Refl_under_underS[of r a] underS_notIn[of a r] by blast
   1.105      have 2: "wo_rel.ofilter r (underS r a) \<and> underS r a < Field r"
   1.106      using 0 wo_rel.underS_ofilter * 1 Case2 by fast
   1.107      hence "?r' <o r" using 0 using ofilter_ordLess by blast
   1.108 @@ -951,7 +946,7 @@
   1.109      (*  *)
   1.110      have "\<not> finite (Field r)" using 1 unfolding phi_def by simp
   1.111      hence "\<not> finite ?B" using 8 3 card_of_ordIso_finite_Field[of r ?B] by blast
   1.112 -    hence "\<not> finite A1" using 9 finite_cartesian_product finite_subset by metis
   1.113 +    hence "\<not> finite A1" using 9 finite_cartesian_product finite_subset by blast
   1.114      moreover have temp4: "Field |A1| = A1 \<and> Well_order |A1| \<and> Card_order |A1|"
   1.115      using card_of_Card_order[of A1] card_of_Well_order[of A1]
   1.116      by (simp add: Field_card_of)
   1.117 @@ -1110,7 +1105,7 @@
   1.118      by (auto simp add: card_of_Plus_Times)
   1.119      moreover have "|A \<times> B| =o |A|"
   1.120      using assms * by (simp add: card_of_Times_infinite_simps)
   1.121 -    ultimately have "|A <+> B| \<le>o |A|" using ordLeq_ordIso_trans by metis
   1.122 +    ultimately have "|A <+> B| \<le>o |A|" using ordLeq_ordIso_trans by blast
   1.123      thus ?thesis using card_of_Plus1 ordIso_iff_ordLeq by blast
   1.124    qed
   1.125  qed
   1.126 @@ -1256,7 +1251,7 @@
   1.127  corollary finite_iff_ordLess_natLeq:
   1.128  "finite A = ( |A| <o natLeq)"
   1.129  using infinite_iff_natLeq_ordLeq not_ordLeq_iff_ordLess
   1.130 -      card_of_Well_order natLeq_Well_order by metis
   1.131 +      card_of_Well_order natLeq_Well_order by blast
   1.132  
   1.133  
   1.134  subsection {* The successor of a cardinal *}
   1.135 @@ -1394,7 +1389,7 @@
   1.136    then show "finite (Field (cardSuc |A| ))"
   1.137    proof (rule card_of_ordLeq_finite[OF card_of_mono2, rotated])
   1.138      show "cardSuc |A| \<le>o |Pow A|"
   1.139 -      by (metis cardSuc_ordLess_ordLeq card_of_Card_order card_of_Pow)
   1.140 +      by (rule iffD1[OF cardSuc_ordLess_ordLeq card_of_Pow]) (simp_all add: card_of_Card_order)
   1.141    qed
   1.142  qed
   1.143  
   1.144 @@ -1655,7 +1650,7 @@
   1.145    unfolding bij_betw_def inj_on_def proof safe
   1.146      fix h :: "'a \<Rightarrow> 'b" assume h: "h \<in> Func UNIV B"
   1.147      hence "\<forall> a. \<exists> b. h a = b" unfolding Func_def by auto
   1.148 -    then obtain f where f: "\<forall> a. h a = f a" by metis
   1.149 +    then obtain f where f: "\<forall> a. h a = f a" by blast
   1.150      hence "range f \<subseteq> B" using h unfolding Func_def by auto
   1.151      thus "h \<in> (\<lambda>f a. f a) ` {f. range f \<subseteq> B}" using f unfolding image_def by auto
   1.152    qed(unfold Func_def fun_eq_iff, auto)