# HG changeset patch
# User traytel
# Date 1393606492 -3600
# Node ID aa1acc25126b03b104a5c5d2096eb031c047e29e
# Parent  63d63d854fae399d27ec9df41bdf6f4b7d4ae13b
load Metis a little later

diff -r 63d63d854fae -r aa1acc25126b src/HOL/BNF_Cardinal_Arithmetic.thy
--- a/src/HOL/BNF_Cardinal_Arithmetic.thy	Fri Feb 28 22:00:13 2014 +0100
+++ b/src/HOL/BNF_Cardinal_Arithmetic.thy	Fri Feb 28 17:54:52 2014 +0100
@@ -57,15 +57,19 @@
                   \<lambda>x. if x \<in> A then snd (fg x) else undefined)"
   let ?G = "\<lambda>(f, g) x. if x \<in> A then (f x, g x) else undefined"
   have "bij_betw ?F ?LHS ?RHS" unfolding bij_betw_def inj_on_def
-  apply safe
-     apply (simp add: Func_def fun_eq_iff)
-     apply (metis (no_types) pair_collapse)
-    apply (auto simp: Func_def fun_eq_iff)[2]
-  proof -
-    fix f g assume "f \<in> Func A B" "g \<in> Func A C"
-    thus "(f, g) \<in> ?F ` Func A (B \<times> C)"
-      by (intro image_eqI[of _ _ "?G (f, g)"]) (auto simp: Func_def)
-  qed
+  proof (intro conjI impI ballI equalityI subsetI)
+    fix f g assume *: "f \<in> Func A (B \<times> C)" "g \<in> Func A (B \<times> C)" "?F f = ?F g"
+    show "f = g"
+    proof
+      fix x from * have "fst (f x) = fst (g x) \<and> snd (f x) = snd (g x)"
+        by (case_tac "x \<in> A") (auto simp: Func_def fun_eq_iff split: if_splits)
+      then show "f x = g x" by (subst (1 2) surjective_pairing) simp
+    qed
+  next
+    fix fg assume "fg \<in> Func A B \<times> Func A C"
+    thus "fg \<in> ?F ` Func A (B \<times> C)"
+      by (intro image_eqI[of _ _ "?G fg"]) (auto simp: Func_def)
+  qed (auto simp: Func_def fun_eq_iff)
   thus ?thesis using card_of_ordIso by blast
 qed
 
@@ -89,7 +93,7 @@
 
 (*helper*)
 lemma Cnotzero_imp_not_empty: "Cnotzero r \<Longrightarrow> Field r \<noteq> {}"
-by (metis Card_order_iff_ordIso_card_of czero_def)
+  unfolding Card_order_iff_ordIso_card_of czero_def by force
 
 lemma czeroI:
   "\<lbrakk>Card_order r; Field r = {}\<rbrakk> \<Longrightarrow> r =o czero"
@@ -127,33 +131,35 @@
 
 lemma Cfinite_ordLess_Cinfinite: "\<lbrakk>Cfinite r; Cinfinite s\<rbrakk> \<Longrightarrow> r <o s"
   unfolding cfinite_def cinfinite_def
-  by (metis card_order_on_well_order_on finite_ordLess_infinite)
+  by (blast intro: finite_ordLess_infinite card_order_on_well_order_on)
 
 lemmas natLeq_card_order = natLeq_Card_order[unfolded Field_natLeq]
 
 lemma natLeq_cinfinite: "cinfinite natLeq"
-unfolding cinfinite_def Field_natLeq by (metis infinite_UNIV_nat)
+unfolding cinfinite_def Field_natLeq by (rule infinite_UNIV_nat)
 
 lemma natLeq_ordLeq_cinfinite:
   assumes inf: "Cinfinite r"
   shows "natLeq \<le>o r"
 proof -
-  from inf have "natLeq \<le>o |Field r|" by (metis cinfinite_def infinite_iff_natLeq_ordLeq)
+  from inf have "natLeq \<le>o |Field r|" unfolding cinfinite_def
+    using infinite_iff_natLeq_ordLeq by blast
   also from inf have "|Field r| =o r" by (simp add: card_of_unique ordIso_symmetric)
   finally show ?thesis .
 qed
 
 lemma cinfinite_not_czero: "cinfinite r \<Longrightarrow> \<not> (r =o (czero :: 'a rel))"
-unfolding cinfinite_def by (metis czeroE finite.emptyI)
+unfolding cinfinite_def by (cases "Field r = {}") (auto dest: czeroE)
 
 lemma Cinfinite_Cnotzero: "Cinfinite r \<Longrightarrow> Cnotzero r"
-by (metis cinfinite_not_czero)
+by (rule conjI[OF cinfinite_not_czero]) simp_all
 
 lemma Cinfinite_cong: "\<lbrakk>r1 =o r2; Cinfinite r1\<rbrakk> \<Longrightarrow> Cinfinite r2"
-by (metis Card_order_ordIso2 card_of_mono2 card_of_ordLeq_infinite cinfinite_def ordIso_iff_ordLeq)
+using Card_order_ordIso2[of r1 r2] unfolding cinfinite_def ordIso_iff_ordLeq
+by (auto dest: card_of_ordLeq_infinite[OF card_of_mono2])
 
 lemma cinfinite_mono: "\<lbrakk>r1 \<le>o r2; cinfinite r1\<rbrakk> \<Longrightarrow> cinfinite r2"
-by (metis card_of_mono2 card_of_ordLeq_infinite cinfinite_def)
+unfolding cinfinite_def by (auto dest: card_of_ordLeq_infinite[OF card_of_mono2])
 
 
 subsection {* Binary sum *}
@@ -170,8 +176,8 @@
 
 lemma csum_Cnotzero1:
   "Cnotzero r1 \<Longrightarrow> Cnotzero (r1 +c r2)"
-unfolding csum_def
-by (metis Cnotzero_imp_not_empty Plus_eq_empty_conv card_of_Card_order card_of_ordIso_czero_iff_empty)
+unfolding csum_def using Cnotzero_imp_not_empty[of r1] Plus_eq_empty_conv[of "Field r1" "Field r2"]
+   card_of_ordIso_czero_iff_empty[of "Field r1 <+> Field r2"] by (auto intro: card_of_Card_order)
 
 lemma card_order_csum:
   assumes "card_order r1" "card_order r2"
@@ -187,15 +193,15 @@
 
 lemma Cinfinite_csum1:
   "Cinfinite r1 \<Longrightarrow> Cinfinite (r1 +c r2)"
-unfolding cinfinite_def csum_def by (metis Field_card_of card_of_Card_order finite_Plus_iff)
+unfolding cinfinite_def csum_def by (rule conjI[OF _ card_of_Card_order]) (auto simp: Field_card_of)
 
 lemma Cinfinite_csum:
   "Cinfinite r1 \<or> Cinfinite r2 \<Longrightarrow> Cinfinite (r1 +c r2)"
-unfolding cinfinite_def csum_def by (metis Field_card_of card_of_Card_order finite_Plus_iff)
+unfolding cinfinite_def csum_def by (rule conjI[OF _ card_of_Card_order]) (auto simp: Field_card_of)
 
 lemma Cinfinite_csum_strong:
   "\<lbrakk>Cinfinite r1; Cinfinite r2\<rbrakk> \<Longrightarrow> Cinfinite (r1 +c r2)"
-by (metis Cinfinite_csum)
+by (erule Cinfinite_csum1)
 
 lemma csum_cong: "\<lbrakk>p1 =o r1; p2 =o r2\<rbrakk> \<Longrightarrow> p1 +c p2 =o r1 +c r2"
 by (simp only: csum_def ordIso_Plus_cong)
@@ -233,15 +239,15 @@
 lemma csum_csum: "(r1 +c r2) +c (r3 +c r4) =o (r1 +c r3) +c (r2 +c r4)"
 proof -
   have "(r1 +c r2) +c (r3 +c r4) =o r1 +c r2 +c (r3 +c r4)"
-    by (metis csum_assoc)
+    by (rule csum_assoc)
   also have "r1 +c r2 +c (r3 +c r4) =o r1 +c (r2 +c r3) +c r4"
-    by (metis csum_assoc csum_cong2 ordIso_symmetric)
+    by (intro csum_assoc csum_cong2 ordIso_symmetric)
   also have "r1 +c (r2 +c r3) +c r4 =o r1 +c (r3 +c r2) +c r4"
-    by (metis csum_com csum_cong1 csum_cong2)
+    by (intro csum_com csum_cong1 csum_cong2)
   also have "r1 +c (r3 +c r2) +c r4 =o r1 +c r3 +c r2 +c r4"
-    by (metis csum_assoc csum_cong2 ordIso_symmetric)
+    by (intro csum_assoc csum_cong2 ordIso_symmetric)
   also have "r1 +c r3 +c r2 +c r4 =o (r1 +c r3) +c (r2 +c r4)"
-    by (metis csum_assoc ordIso_symmetric)
+    by (intro csum_assoc ordIso_symmetric)
   finally show ?thesis .
 qed
 
@@ -264,10 +270,10 @@
   unfolding cfinite_def by (simp add: Card_order_cone)
 
 lemma cone_not_czero: "\<not> (cone =o czero)"
-unfolding czero_def cone_def by (metis empty_not_insert card_of_empty3[of "{()}"] ordIso_iff_ordLeq)
+unfolding czero_def cone_def ordIso_iff_ordLeq using card_of_empty3 empty_not_insert by blast
 
 lemma cone_ordLeq_Cnotzero: "Cnotzero r \<Longrightarrow> cone \<le>o r"
-unfolding cone_def by (metis Card_order_singl_ordLeq czeroI)
+unfolding cone_def by (rule Card_order_singl_ordLeq) (auto intro: czeroI)
 
 
 subsection {* Two *}
@@ -280,7 +286,7 @@
 
 lemma ctwo_not_czero: "\<not> (ctwo =o czero)"
 using card_of_empty3[of "UNIV :: bool set"] ordIso_iff_ordLeq
-unfolding czero_def ctwo_def by (metis UNIV_not_empty)
+unfolding czero_def ctwo_def using UNIV_not_empty by auto
 
 lemma ctwo_Cnotzero: "Cnotzero ctwo"
 by (simp add: ctwo_not_czero Card_order_ctwo)
@@ -330,13 +336,13 @@
 by (simp only: cprod_def ordLeq_Times_mono2)
 
 lemma ordLeq_cprod2: "\<lbrakk>Cnotzero p1; Card_order p2\<rbrakk> \<Longrightarrow> p2 \<le>o p1 *c p2"
-unfolding cprod_def by (metis Card_order_Times2 czeroI)
+unfolding cprod_def by (rule Card_order_Times2) (auto intro: czeroI)
 
 lemma cinfinite_cprod: "\<lbrakk>cinfinite r1; cinfinite r2\<rbrakk> \<Longrightarrow> cinfinite (r1 *c r2)"
 by (simp add: cinfinite_def cprod_def Field_card_of infinite_cartesian_product)
 
 lemma cinfinite_cprod2: "\<lbrakk>Cnotzero r1; Cinfinite r2\<rbrakk> \<Longrightarrow> cinfinite (r1 *c r2)"
-by (metis cinfinite_mono ordLeq_cprod2)
+by (rule cinfinite_mono) (auto intro: ordLeq_cprod2)
 
 lemma Cinfinite_cprod2: "\<lbrakk>Cnotzero r1; Cinfinite r2\<rbrakk> \<Longrightarrow> Cinfinite (r1 *c r2)"
 by (blast intro: cinfinite_cprod2 Card_order_cprod)
@@ -364,7 +370,8 @@
 unfolding csum_def cprod_def by (simp add: Field_card_of card_of_Times_Plus_distrib ordIso_symmetric)
 
 lemma csum_absorb2': "\<lbrakk>Card_order r2; r1 \<le>o r2; cinfinite r1 \<or> cinfinite r2\<rbrakk> \<Longrightarrow> r1 +c r2 =o r2"
-unfolding csum_def by (metis Card_order_Plus_infinite cinfinite_def cinfinite_mono)
+unfolding csum_def by (rule conjunct2[OF Card_order_Plus_infinite])
+  (auto simp: cinfinite_def dest: cinfinite_mono)
 
 lemma csum_absorb1':
   assumes card: "Card_order r2"
@@ -390,10 +397,10 @@
   shows "p1 ^c p2 \<le>o r1 ^c r2"
 proof(cases "Field p1 = {}")
   case True
-  hence "|Field |Func (Field p2) (Field p1)|| \<le>o cone"
+  hence "Field p2 \<noteq> {} \<Longrightarrow> Func (Field p2) {} = {}" unfolding Func_is_emp by simp
+  with True have "|Field |Func (Field p2) (Field p1)|| \<le>o cone"
     unfolding cone_def Field_card_of
-    by (cases "Field p2 = {}", auto intro: card_of_ordLeqI2 simp: Func_empty)
-       (metis Func_is_emp card_of_empty ex_in_conv)
+    by (cases "Field p2 = {}", auto intro: surj_imp_ordLeq simp: Func_empty)
   hence "|Func (Field p2) (Field p1)| \<le>o cone" by (simp add: Field_card_of cexp_def)
   hence "p1 ^c p2 \<le>o cone" unfolding cexp_def .
   thus ?thesis
@@ -429,7 +436,7 @@
   assumes 1: "p1 \<le>o r1" and 2: "p2 \<le>o r2"
   and n: "p2 =o czero \<Longrightarrow> r2 =o czero" and card: "Card_order p2"
   shows "p1 ^c p2 \<le>o r1 ^c r2"
-  by (metis (full_types) "1" "2" card cexp_mono' czeroE czeroI n)
+  by (rule cexp_mono'[OF 1 2 czeroE[OF n[OF czeroI[OF card]]]])
 
 lemma cexp_mono1:
   assumes 1: "p1 \<le>o r1" and q: "Card_order q"
@@ -451,7 +458,7 @@
 lemma cexp_mono2_Cnotzero:
   assumes "p2 \<le>o r2" "Card_order q" "Cnotzero p2"
   shows "q ^c p2 \<le>o q ^c r2"
-by (metis assms cexp_mono2' czeroI)
+using assms(3) czeroI by (blast intro: cexp_mono2'[OF assms(1,2)])
 
 lemma cexp_cong:
   assumes 1: "p1 =o r1" and 2: "p2 =o r2"
@@ -466,7 +473,7 @@
     and p: "r2 =o czero \<Longrightarrow> p2 =o czero"
      using 0 Cr Cp czeroE czeroI by auto
   show ?thesis using 0 1 2 unfolding ordIso_iff_ordLeq
-    using r p cexp_mono[OF _ _ _ Cp] cexp_mono[OF _ _ _ Cr] by metis
+    using r p cexp_mono[OF _ _ _ Cp] cexp_mono[OF _ _ _ Cr] by blast
 qed
 
 lemma cexp_cong1:
@@ -575,7 +582,7 @@
 qed
 
 lemma cinfinite_cexp: "\<lbrakk>ctwo \<le>o q; Cinfinite r\<rbrakk> \<Longrightarrow> cinfinite (q ^c r)"
-by (metis assms cinfinite_mono ordLeq_cexp2)
+by (rule cinfinite_mono[OF ordLeq_cexp2]) simp_all
 
 lemma Cinfinite_cexp:
   "\<lbrakk>ctwo \<le>o q; Cinfinite r\<rbrakk> \<Longrightarrow> Cinfinite (q ^c r)"
@@ -586,7 +593,7 @@
 by (intro Cfinite_ordLess_Cinfinite) (auto simp: cfinite_def card_of_Card_order)
 
 lemma ctwo_ordLess_Cinfinite: "Cinfinite r \<Longrightarrow> ctwo <o r"
-by (metis ctwo_ordLess_natLeq natLeq_ordLeq_cinfinite ordLess_ordLeq_trans)
+by (rule ordLess_ordLeq_trans[OF ctwo_ordLess_natLeq natLeq_ordLeq_cinfinite])
 
 lemma ctwo_ordLeq_Cinfinite:
   assumes "Cinfinite r"
@@ -663,9 +670,10 @@
   case True thus ?thesis using t by (blast intro: cexp_mono1)
 next
   case False
-  hence "ctwo \<le>o s" by (metis card_order_on_well_order_on ctwo_Cnotzero ordLeq_total s)
-  hence "Cnotzero s" by (metis Cnotzero_mono ctwo_Cnotzero s)
-  hence st: "Cnotzero (s *c t)" by (metis Cinfinite_cprod2 cinfinite_not_czero t)
+  hence "ctwo \<le>o s" using ordLeq_total[of s ctwo] Card_order_ctwo s
+    by (auto intro: card_order_on_well_order_on)
+  hence "Cnotzero s" using Cnotzero_mono[OF ctwo_Cnotzero] s by blast
+  hence st: "Cnotzero (s *c t)" by (intro Cinfinite_Cnotzero[OF Cinfinite_cprod2]) (auto simp: t)
   have "s ^c t \<le>o (ctwo ^c s) ^c t"
     using assms by (blast intro: cexp_mono1 ordLess_imp_ordLeq[OF ordLess_ctwo_cexp])
   also have "(ctwo ^c s) ^c t =o ctwo ^c (s *c t)"
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 \<subseteq> f ` A"
+shows "|B| \<le>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 \<subseteq> f ` A"
-shows "|B| \<le>o |A|"
-using assms by (metis surj_imp_ordLeq)
-
 lemma card_of_singl_ordLeq:
 assumes "A \<noteq> {}"
 shows "|{b}| \<le>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 = (\<lambda>(a,c::'c). (f a,c))" by blast
   have "inj_on g (A \<times> C) \<and> g ` (A \<times> C) \<le> (B \<times> 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 "\<forall>i. i \<in> I \<longrightarrow> (\<exists>f. inj_on f (A i) \<and> f ` (A i) \<le> B i)"
   using assms by (auto simp add: card_of_ordLeq)
   with choice[of "\<lambda> i f. i \<in> I \<longrightarrow> inj_on f (A i) \<and> f ` (A i) \<le> B i"]
-  obtain F where 1: "\<forall>i \<in> I. inj_on (F i) (A i) \<and> (F i) ` (A i) \<le> B i" by metis
+  obtain F where 1: "\<forall>i \<in> I. inj_on (F i) (A i) \<and> (F i) ` (A i) \<le> B i"
+    by atomize_elim (auto intro: bchoice)
   obtain g where g_def: "g = (\<lambda>(i,a::'b). (i,F i a))" by blast
   have "inj_on g (Sigma I A) \<and> g ` (Sigma I A) \<le> (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:
 "|\<Union>i \<in> I. A i| \<le>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 \<noteq> 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| \<le>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| \<le>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 \<in> Field r"
     hence 1: "under r a = underS r a \<union> {a} \<and> a \<notin> 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) \<and> underS r a < Field r"
     using 0 wo_rel.underS_ofilter * 1 Case2 by fast
     hence "?r' <o r" using 0 using ofilter_ordLess by blast
@@ -951,7 +946,7 @@
     (*  *)
     have "\<not> finite (Field r)" using 1 unfolding phi_def by simp
     hence "\<not> finite ?B" using 8 3 card_of_ordIso_finite_Field[of r ?B] by blast
-    hence "\<not> finite A1" using 9 finite_cartesian_product finite_subset by metis
+    hence "\<not> finite A1" using 9 finite_cartesian_product finite_subset by blast
     moreover have temp4: "Field |A1| = A1 \<and> Well_order |A1| \<and> 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 \<times> B| =o |A|"
     using assms * by (simp add: card_of_Times_infinite_simps)
-    ultimately have "|A <+> B| \<le>o |A|" using ordLeq_ordIso_trans by metis
+    ultimately have "|A <+> B| \<le>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 natLeq)"
 using infinite_iff_natLeq_ordLeq not_ordLeq_iff_ordLess
-      card_of_Well_order natLeq_Well_order by metis
+      card_of_Well_order natLeq_Well_order by blast
 
 
 subsection {* The successor of a cardinal *}
@@ -1394,7 +1389,7 @@
   then show "finite (Field (cardSuc |A| ))"
   proof (rule card_of_ordLeq_finite[OF card_of_mono2, rotated])
     show "cardSuc |A| \<le>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 \<Rightarrow> 'b" assume h: "h \<in> Func UNIV B"
     hence "\<forall> a. \<exists> b. h a = b" unfolding Func_def by auto
-    then obtain f where f: "\<forall> a. h a = f a" by metis
+    then obtain f where f: "\<forall> a. h a = f a" by blast
     hence "range f \<subseteq> B" using h unfolding Func_def by auto
     thus "h \<in> (\<lambda>f a. f a) ` {f. range f \<subseteq> B}" using f unfolding image_def by auto
   qed(unfold Func_def fun_eq_iff, auto)
diff -r 63d63d854fae -r aa1acc25126b src/HOL/BNF_Comp.thy
--- a/src/HOL/BNF_Comp.thy	Fri Feb 28 22:00:13 2014 +0100
+++ b/src/HOL/BNF_Comp.thy	Fri Feb 28 17:54:52 2014 +0100
@@ -90,26 +90,41 @@
 
 lemma type_copy_map_id0: "M = id \<Longrightarrow> Abs o M o Rep = id"
   using type_definition.Rep_inverse[OF type_copy] by auto
+
 lemma type_copy_map_comp0: "M = M1 o M2 \<Longrightarrow> f o M o g = (f o M1 o Rep) o (Abs o M2 o g)"
   using type_definition.Abs_inverse[OF type_copy UNIV_I] by auto
+
 lemma type_copy_set_map0: "S o M = image f o S' \<Longrightarrow> (S o Rep) o (Abs o M o g) = image f o (S' o g)"
   using type_definition.Abs_inverse[OF type_copy UNIV_I] by (auto simp: o_def fun_eq_iff)
+
 lemma type_copy_wit: "x \<in> (S o Rep) (Abs y) \<Longrightarrow> x \<in> S y"
   using type_definition.Abs_inverse[OF type_copy UNIV_I] by auto
+
 lemma type_copy_vimage2p_Grp_Rep: "vimage2p f Rep (Grp (Collect P) h) =
     Grp (Collect (\<lambda>x. P (f x))) (Abs o h o f)"
   unfolding vimage2p_def Grp_def fun_eq_iff
   by (auto simp: type_definition.Abs_inverse[OF type_copy UNIV_I]
    type_definition.Rep_inverse[OF type_copy] dest: sym)
+
 lemma type_copy_vimage2p_Grp_Abs:
   "\<And>h. vimage2p g Abs (Grp (Collect P) h) = Grp (Collect (\<lambda>x. P (g x))) (Rep o h o g)"
   unfolding vimage2p_def Grp_def fun_eq_iff
   by (auto simp: type_definition.Abs_inverse[OF type_copy UNIV_I]
    type_definition.Rep_inverse[OF type_copy] dest: sym)
+
+lemma type_copy_ex_RepI: "(\<exists>b. F b) = (\<exists>b. F (Rep b))"
+proof safe
+  fix b assume "F b"
+  show "\<exists>b'. F (Rep b')"
+  proof (rule exI)
+    from `F b` show "F (Rep (Abs b))" using type_definition.Abs_inverse[OF type_copy] by auto
+  qed
+qed blast
+
 lemma vimage2p_relcompp_converse:
   "vimage2p f g (R^--1 OO S) = (vimage2p Rep f R)^--1 OO vimage2p Rep g S"
   unfolding vimage2p_def relcompp.simps conversep.simps fun_eq_iff image_def
-  by (metis surjD[OF type_definition.Rep_range[OF type_copy]])
+  by (auto simp: type_copy_ex_RepI)
 
 end
 
diff -r 63d63d854fae -r aa1acc25126b src/HOL/BNF_Constructions_on_Wellorders.thy
--- a/src/HOL/BNF_Constructions_on_Wellorders.thy	Fri Feb 28 22:00:13 2014 +0100
+++ b/src/HOL/BNF_Constructions_on_Wellorders.thy	Fri Feb 28 17:54:52 2014 +0100
@@ -793,7 +793,7 @@
   {assume "r' \<le>o r"
    then obtain h where "inj_on h (Field r') \<and> h ` (Field r') \<le> Field r"
    unfolding ordLeq_def using assms embed_inj_on embed_Field by blast
-   hence False using finite_imageD finite_subset FIN INF by metis
+   hence False using finite_imageD finite_subset FIN INF by blast
   }
   thus ?thesis using WELL WELL' ordLess_or_ordLeq by blast
 qed
@@ -819,7 +819,7 @@
     hence "bij_betw f A A" unfolding bij_betw_def using FIN endo_inj_surj by blast
     thus "r =o r'" unfolding ordIso_def iso_def[abs_def] using 1 2 by auto
   qed
-  ultimately show ?thesis using assms ordLeq_total ordIso_symmetric by metis
+  ultimately show ?thesis using assms ordLeq_total ordIso_symmetric by blast
 qed
 
 subsection{* @{text "<o"} is well-founded *}
@@ -987,7 +987,7 @@
   have "A \<noteq> {} \<and> A \<le> Field r"
   using A_def dir_image_Field[of r f] SUB NE by blast
   then obtain a where 1: "a \<in> A \<and> (\<forall>b \<in> A. (b,a) \<notin> r)"
-  using WF unfolding wf_eq_minimal2 by metis
+  using WF unfolding wf_eq_minimal2 by blast
   have "\<forall>b' \<in> A'. (b',f a) \<notin> dir_image r f"
   proof(clarify)
     fix b' assume *: "b' \<in> A'" and **: "(b',f a) \<in> dir_image r f"
@@ -1597,7 +1597,7 @@
 proof
   assume L: ?L
   moreover {assume "A = {}" hence False using L Func_empty by auto}
-  moreover {assume "B \<noteq> {}" hence False using L Func_non_emp by metis}
+  moreover {assume "B \<noteq> {}" hence False using L Func_non_emp[of B A] by simp }
   ultimately show ?R by blast
 next
   assume R: ?R
@@ -1624,7 +1624,8 @@
     fix h assume h: "h \<in> Func B2 B1"
     def j1 \<equiv> "inv_into A1 f1"
     have "\<forall> a2 \<in> f2 ` B2. \<exists> b2. b2 \<in> B2 \<and> f2 b2 = a2" by blast
-    then obtain k where k: "\<forall> a2 \<in> f2 ` B2. k a2 \<in> B2 \<and> f2 (k a2) = a2" by metis
+    then obtain k where k: "\<forall> a2 \<in> f2 ` B2. k a2 \<in> B2 \<and> f2 (k a2) = a2"
+      by atomize_elim (rule bchoice)
     {fix b2 assume b2: "b2 \<in> B2"
      hence "f2 (k (f2 b2)) = f2 b2" using k A2(2) by auto
      moreover have "k (f2 b2) \<in> B2" using b2 A2(2) k by auto
diff -r 63d63d854fae -r aa1acc25126b src/HOL/BNF_Def.thy
--- a/src/HOL/BNF_Def.thy	Fri Feb 28 22:00:13 2014 +0100
+++ b/src/HOL/BNF_Def.thy	Fri Feb 28 17:54:52 2014 +0100
@@ -116,7 +116,7 @@
 
 
 lemma predicate2_eqD: "A = B \<Longrightarrow> A a b \<longleftrightarrow> B a b"
-by metis
+by simp
 
 lemma case_sum_o_inj:
 "case_sum f g \<circ> Inl = f"
diff -r 63d63d854fae -r aa1acc25126b src/HOL/BNF_FP_Base.thy
--- a/src/HOL/BNF_FP_Base.thy	Fri Feb 28 22:00:13 2014 +0100
+++ b/src/HOL/BNF_FP_Base.thy	Fri Feb 28 17:54:52 2014 +0100
@@ -65,13 +65,16 @@
 by blast
 
 lemma type_copy_obj_one_point_absE:
-  assumes "type_definition Rep Abs UNIV"
-  shows "\<forall>x. s = Abs x \<longrightarrow> P \<Longrightarrow> P"
-  using type_definition.Rep_inverse[OF assms] by metis
+  assumes "type_definition Rep Abs UNIV" "\<forall>x. s = Abs x \<longrightarrow> P" shows P
+  using type_definition.Rep_inverse[OF assms(1)]
+  by (intro mp[OF spec[OF assms(2), of "Rep s"]]) simp
 
 lemma obj_sumE_f:
-"\<lbrakk>\<forall>x. s = f (Inl x) \<longrightarrow> P; \<forall>x. s = f (Inr x) \<longrightarrow> P\<rbrakk> \<Longrightarrow> \<forall>x. s = f x \<longrightarrow> P"
-by (rule allI) (metis sumE)
+  assumes "\<forall>x. s = f (Inl x) \<longrightarrow> P" "\<forall>x. s = f (Inr x) \<longrightarrow> P"
+  shows "\<forall>x. s = f x \<longrightarrow> P"
+proof
+  fix x from assms show "s = f x \<longrightarrow> P" by (cases x) auto
+qed
 
 lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
 by (cases s) auto
diff -r 63d63d854fae -r aa1acc25126b src/HOL/BNF_LFP.thy
--- a/src/HOL/BNF_LFP.thy	Fri Feb 28 22:00:13 2014 +0100
+++ b/src/HOL/BNF_LFP.thy	Fri Feb 28 17:54:52 2014 +0100
@@ -50,8 +50,16 @@
 lemma convol_expand_snd: "fst o f = g \<Longrightarrow>  <g, snd o f> = f"
 unfolding convol_def by auto
 
-lemma convol_expand_snd': "(fst o f = g) \<Longrightarrow> (h = snd o f) \<longleftrightarrow> (<g, h> = f)"
-  by (metis convol_expand_snd snd_convol)
+lemma convol_expand_snd':
+  assumes "(fst o f = g)"
+  shows "h = snd o f \<longleftrightarrow> <g, h> = f"
+proof -
+  from assms have *: "<g, snd o f> = f" by (rule convol_expand_snd)
+  then have "h = snd o f \<longleftrightarrow> h = snd o <g, snd o f>" by simp
+  moreover have "\<dots> \<longleftrightarrow> h = snd o f" by (simp add: snd_convol)
+  moreover have "\<dots> \<longleftrightarrow> <g, h> = f" by (subst (2) *[symmetric]) (auto simp: convol_def fun_eq_iff)
+  ultimately show ?thesis by simp
+qed
 
 definition inver where
   "inver g f A = (ALL a : A. g (f a) = a)"
@@ -67,7 +75,11 @@
     using bchoice[of B ?phi] by blast
   hence gg: "ALL b : f ` A. g b : A \<and> f (g b) = b" using f by blast
   have gf: "inver g f A" unfolding inver_def
-    by (metis (no_types) gg imageI[of _ A f] the_inv_into_f_f[OF inj_f])
+  proof
+    fix a assume "a \<in> A"
+    then show "g (f a) = a" using the_inv_into_f_f[OF inj_f, of "g (f a)"]
+      the_inv_into_f_f[OF inj_f, of a] gg imageI[of a A f] by auto
+  qed
   moreover have "g ` B \<le> A \<and> inver f g B" using g unfolding inver_def by blast
   moreover have "A \<le> g ` B"
   proof safe
@@ -224,8 +236,13 @@
 by (rule assms)
 
 lemma nchotomy_relcomppE:
-  "\<lbrakk>\<And>y. \<exists>x. y = f x; (r OO s) a c; \<And>b. r a (f b) \<Longrightarrow> s (f b) c \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
-  by (metis relcompp.cases)
+  assumes "\<And>y. \<exists>x. y = f x" "(r OO s) a c" "\<And>b. r a (f b) \<Longrightarrow> s (f b) c \<Longrightarrow> P"
+  shows P
+proof (rule relcompp.cases[OF assms(2)], hypsubst)
+  fix b assume "r a b" "s b c"
+  moreover from assms(1) obtain b' where "b = f b'" by blast
+  ultimately show P by (blast intro: assms(3))
+qed
 
 lemma vimage2p_fun_rel: "fun_rel (vimage2p f g R) R f g"
   unfolding fun_rel_def vimage2p_def by auto
diff -r 63d63d854fae -r aa1acc25126b src/HOL/BNF_Wellorder_Embedding.thy
--- a/src/HOL/BNF_Wellorder_Embedding.thy	Fri Feb 28 22:00:13 2014 +0100
+++ b/src/HOL/BNF_Wellorder_Embedding.thy	Fri Feb 28 17:54:52 2014 +0100
@@ -305,8 +305,7 @@
   (* Main proof *)
   show "bij_betw f (under r a) (under r' (f a))"
   proof(unfold bij_betw_def, auto)
-    show  "inj_on f (under r a)"
-    using * by (metis (no_types) under_Field subset_inj_on)
+    show  "inj_on f (under r a)" by (rule subset_inj_on[OF * under_Field])
   next
     fix b assume "b \<in> under r a"
     thus "f b \<in> under r' (f a)"
@@ -1035,8 +1034,7 @@
   {fix a assume ***: "a \<in> Field r"
    have "bij_betw f (under r a) (under r' (f a))"
    proof(unfold bij_betw_def, auto)
-     show "inj_on f (under r a)"
-     using 1 2 by (metis subset_inj_on)
+     show "inj_on f (under r a)" using 1 2 subset_inj_on by blast
    next
      fix b assume "b \<in> under r a"
      hence "a \<in> Field r \<and> b \<in> Field r \<and> (b,a) \<in> r"
diff -r 63d63d854fae -r aa1acc25126b src/HOL/Basic_BNFs.thy
--- a/src/HOL/Basic_BNFs.thy	Fri Feb 28 22:00:13 2014 +0100
+++ b/src/HOL/Basic_BNFs.thy	Fri Feb 28 17:54:52 2014 +0100
@@ -158,11 +158,11 @@
 next
   fix x
   show "|{fst x}| \<le>o natLeq"
-    by (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq finite.emptyI finite_insert)
+    by (rule ordLess_imp_ordLeq) (simp add: finite_iff_ordLess_natLeq[symmetric])
 next
   fix x
   show "|{snd x}| \<le>o natLeq"
-    by (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq finite.emptyI finite_insert)
+    by (rule ordLess_imp_ordLeq) (simp add: finite_iff_ordLess_natLeq[symmetric])
 next
   fix R1 R2 S1 S2
   show "prod_rel R1 R2 OO prod_rel S1 S2 \<le> prod_rel (R1 OO S1) (R2 OO S2)" by auto
@@ -215,8 +215,14 @@
   show "fun_rel op = R =
         (Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> fst))\<inverse>\<inverse> OO
          Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> snd)"
-  unfolding fun_rel_def Grp_def fun_eq_iff relcompp.simps conversep.simps  subset_iff image_iff
-  by auto (force, metis (no_types) pair_collapse)
+  unfolding fun_rel_def Grp_def fun_eq_iff relcompp.simps conversep.simps subset_iff image_iff
+    comp_apply mem_Collect_eq split_beta bex_UNIV
+  proof (safe, unfold fun_eq_iff[symmetric])
+    fix x xa a b c xb y aa ba
+    assume *: "x = a" "xa = c" "a = ba" "b = aa" "c = (\<lambda>x. snd (b x))" "ba = (\<lambda>x. fst (aa x))" and
+       **: "\<forall>t. (\<exists>x. t = aa x) \<longrightarrow> R (fst t) (snd t)"
+    show "R (x y) (xa y)" unfolding * by (rule mp[OF spec[OF **]]) blast
+  qed force
 qed
 
 end
diff -r 63d63d854fae -r aa1acc25126b src/HOL/Cardinals/Wellorder_Extension.thy
--- a/src/HOL/Cardinals/Wellorder_Extension.thy	Fri Feb 28 22:00:13 2014 +0100
+++ b/src/HOL/Cardinals/Wellorder_Extension.thy	Fri Feb 28 17:54:52 2014 +0100
@@ -5,7 +5,7 @@
 header {* Extending Well-founded Relations to Wellorders *}
 
 theory Wellorder_Extension
-imports Zorn Order_Union
+imports Main Order_Union
 begin
 
 subsection {* Extending Well-founded Relations to Wellorders *}
diff -r 63d63d854fae -r aa1acc25126b src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Fri Feb 28 22:00:13 2014 +0100
+++ b/src/HOL/Hilbert_Choice.thy	Fri Feb 28 17:54:52 2014 +0100
@@ -6,7 +6,7 @@
 header {* Hilbert's Epsilon-Operator and the Axiom of Choice *}
 
 theory Hilbert_Choice
-imports Nat Wellfounded Metis
+imports Nat Wellfounded
 keywords "specification" "ax_specification" :: thy_goal
 begin
 
@@ -292,12 +292,13 @@
   def Sseq \<equiv> "rec_nat S (\<lambda>n T. T - {SOME e. e \<in> T})"
   def pick \<equiv> "\<lambda>n. (SOME e. e \<in> Sseq n)"
   { fix n have "Sseq n \<subseteq> S" "\<not> finite (Sseq n)" by (induct n) (auto simp add: Sseq_def inf) }
-  moreover then have *: "\<And>n. pick n \<in> Sseq n" by (metis someI_ex pick_def ex_in_conv finite.simps)
+  moreover then have *: "\<And>n. pick n \<in> Sseq n"
+    unfolding pick_def by (subst (asm) finite.simps) (auto simp add: ex_in_conv intro: someI_ex)
   ultimately have "range pick \<subseteq> S" by auto
   moreover
   { fix n m                 
     have "pick n \<notin> Sseq (n + Suc m)" by (induct m) (auto simp add: Sseq_def pick_def)
-    hence "pick n \<noteq> pick (n + Suc m)" by (metis *)
+    with * have "pick n \<noteq> pick (n + Suc m)" by auto
   }
   then have "inj pick" by (intro linorder_injI) (auto simp add: less_iff_Suc_add)
   ultimately show ?thesis by blast
@@ -305,7 +306,7 @@
 
 lemma infinite_iff_countable_subset: "\<not> finite S \<longleftrightarrow> (\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S)"
   -- {* Courtesy of Stephan Merz *}
-  by (metis finite_imageD finite_subset infinite_UNIV_char_0 infinite_countable_subset)
+  using finite_imageD finite_subset infinite_UNIV_char_0 infinite_countable_subset by auto
 
 lemma image_inv_into_cancel:
   assumes SURJ: "f`A=A'" and SUB: "B' \<le> A'"
@@ -706,9 +707,13 @@
     then have "\<And>n. f n < f (Suc n)"
       using  `mono f` by (auto simp: le_less mono_iff_le_Suc)
     with lift_Suc_mono_less_iff[of f]
-    have "\<And>n m. n < m \<Longrightarrow> f n < f m" by auto
-    then have "inj f"
-      by (auto simp: inj_on_def) (metis linorder_less_linear order_less_imp_not_eq)
+    have *: "\<And>n m. n < m \<Longrightarrow> f n < f m" by auto
+    have "inj f"
+    proof (intro injI)
+      fix x y
+      assume "f x = f y"
+      then show "x = y" by (cases x y rule: linorder_cases) (auto dest: *)
+    qed
     with `finite (range f)` have "finite (UNIV::nat set)"
       by (rule finite_imageD)
     then show False by simp
diff -r 63d63d854fae -r aa1acc25126b src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Feb 28 22:00:13 2014 +0100
+++ b/src/HOL/Library/Multiset.thy	Fri Feb 28 17:54:52 2014 +0100
@@ -2314,7 +2314,7 @@
 
 lemma card_of_set_of:
 "(card_of {M. set_of M \<subseteq> A}, card_of {as. set as \<subseteq> A}) \<in> ordLeq"
-apply(rule card_of_ordLeqI2[of _ multiset_of]) using multiset_of_surj by auto
+apply(rule surj_imp_ordLeq[of _ multiset_of]) using multiset_of_surj by auto
 
 lemma nat_sum_induct:
 assumes "\<And>n1 n2. (\<And> m1 m2. m1 + m2 < n1 + n2 \<Longrightarrow> phi m1 m2) \<Longrightarrow> phi n1 n2"
diff -r 63d63d854fae -r aa1acc25126b src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Feb 28 22:00:13 2014 +0100
+++ b/src/HOL/List.thy	Fri Feb 28 17:54:52 2014 +0100
@@ -3117,7 +3117,7 @@
 proof(induct i j rule:upto.induct)
   case (1 i j)
   from this show ?case
-    unfolding upto.simps[of i j] simp_from_to[of i j] by auto
+    unfolding upto.simps[of i j] by auto
 qed
 
 text{* Tail recursive version for code generation: *}
diff -r 63d63d854fae -r aa1acc25126b src/HOL/Power.thy
--- a/src/HOL/Power.thy	Fri Feb 28 22:00:13 2014 +0100
+++ b/src/HOL/Power.thy	Fri Feb 28 17:54:52 2014 +0100
@@ -613,7 +613,7 @@
 lemma self_le_power:
   fixes x::"'a::linordered_semidom" 
   shows "1 \<le> x \<Longrightarrow> 0 < n \<Longrightarrow> x \<le> x ^ n"
-  by (metis gr_implies_not0 le_eq_less_or_eq less_one nat_le_linear power_increasing power_one_right)
+  using power_increasing[of 1 n x] power_one_right[of x] by auto
 
 lemma power_eq_if: "p ^ m = (if m=0 then 1 else p * (p ^ (m - 1)))"
   unfolding One_nat_def by (cases m) simp_all
diff -r 63d63d854fae -r aa1acc25126b src/HOL/Tools/BNF/bnf_fp_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Feb 28 22:00:13 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Feb 28 17:54:52 2014 +0100
@@ -232,7 +232,8 @@
 fun co_rec_of [_, r] = r;
 
 fun time ctxt timer msg = (if Config.get ctxt bnf_timing
-  then warning (msg ^ ": " ^ ATP_Util.string_of_time (Timer.checkRealTimer timer))
+  then warning (msg ^ ": " ^ string_of_int (Time.toMilliseconds (Timer.checkRealTimer timer)) ^
+    "ms")
   else (); Timer.startRealTimer ());
 
 val preN = "pre_"
diff -r 63d63d854fae -r aa1acc25126b src/HOL/Transfer.thy
--- a/src/HOL/Transfer.thy	Fri Feb 28 22:00:13 2014 +0100
+++ b/src/HOL/Transfer.thy	Fri Feb 28 17:54:52 2014 +0100
@@ -6,7 +6,7 @@
 header {* Generic theorem transfer using relations *}
 
 theory Transfer
-imports Hilbert_Choice Basic_BNFs
+imports Hilbert_Choice Basic_BNFs Metis
 begin
 
 subsection {* Relator for function space *}
diff -r 63d63d854fae -r aa1acc25126b src/HOL/Zorn.thy
--- a/src/HOL/Zorn.thy	Fri Feb 28 22:00:13 2014 +0100
+++ b/src/HOL/Zorn.thy	Fri Feb 28 17:54:52 2014 +0100
@@ -70,7 +70,7 @@
 
 lemma suc_not_equals:
   "chain C \<Longrightarrow> \<not> maxchain C \<Longrightarrow> suc C \<noteq> C"
-  by (auto simp: suc_def) (metis (no_types) less_irrefl not_maxchain_Some)
+  using not_maxchain_Some by (auto simp: suc_def)
 
 lemma subset_suc:
   assumes "X \<subseteq> Y" shows "X \<subseteq> suc Y"
@@ -257,7 +257,7 @@
   shows "chain X"
 using assms
 proof (induct)
-  case (suc X) then show ?case by (simp add: suc_def) (metis (no_types) not_maxchain_Some)
+  case (suc X) then show ?case using not_maxchain_Some by (simp add: suc_def)
 next
   case (Union X)
   then have "\<Union>X \<subseteq> A" by (auto dest: suc_Union_closed_in_carrier)
@@ -377,7 +377,7 @@
         using `subset.maxchain A M` by (auto simp: subset.maxchain_def)
     qed
   qed
-  ultimately show ?thesis by metis
+  ultimately show ?thesis by blast
 qed
 
 text{*Alternative version of Zorn's lemma for the subset relation.*}
@@ -440,8 +440,7 @@
 lemma Chains_alt_def:
   assumes "refl r"
   shows "Chains r = {C. pred_on.chain UNIV (\<lambda>x y. (x, y) \<in> r) C}"
-  using assms
-  by (metis Chains_subset Chains_subset' subset_antisym)
+  using assms Chains_subset Chains_subset' by blast
 
 lemma Zorn_Lemma:
   "\<forall>C\<in>chains A. \<Union>C \<in> A \<Longrightarrow> \<exists>M\<in>A. \<forall>X\<in>A. M \<subseteq> X \<longrightarrow> X = M"
@@ -534,16 +533,28 @@
   by (auto simp: init_seg_of_def Ball_def Chains_def) blast
 
 lemma chain_subset_trans_Union:
-  "chain\<^sub>\<subseteq> R \<Longrightarrow> \<forall>r\<in>R. trans r \<Longrightarrow> trans (\<Union>R)"
-apply (auto simp add: chain_subset_def)
-apply (simp (no_asm_use) add: trans_def)
-by (metis subsetD)
+  assumes "chain\<^sub>\<subseteq> R" "\<forall>r\<in>R. trans r"
+  shows "trans (\<Union>R)"
+proof (intro transI, elim UnionE)
+  fix  S1 S2 :: "'a rel" and x y z :: 'a
+  assume "S1 \<in> R" "S2 \<in> R"
+  with assms(1) have "S1 \<subseteq> S2 \<or> S2 \<subseteq> S1" unfolding chain_subset_def by blast
+  moreover assume "(x, y) \<in> S1" "(y, z) \<in> S2"
+  ultimately have "((x, y) \<in> S1 \<and> (y, z) \<in> S1) \<or> ((x, y) \<in> S2 \<and> (y, z) \<in> S2)" by blast
+  with `S1 \<in> R` `S2 \<in> R` assms(2) show "(x, z) \<in> \<Union>R" by (auto elim: transE)
+qed
 
 lemma chain_subset_antisym_Union:
-  "chain\<^sub>\<subseteq> R \<Longrightarrow> \<forall>r\<in>R. antisym r \<Longrightarrow> antisym (\<Union>R)"
-unfolding chain_subset_def antisym_def
-apply simp
-by (metis (no_types) subsetD)
+  assumes "chain\<^sub>\<subseteq> R" "\<forall>r\<in>R. antisym r"
+  shows "antisym (\<Union>R)"
+proof (intro antisymI, elim UnionE)
+  fix  S1 S2 :: "'a rel" and x y :: 'a
+  assume "S1 \<in> R" "S2 \<in> R"
+  with assms(1) have "S1 \<subseteq> S2 \<or> S2 \<subseteq> S1" unfolding chain_subset_def by blast
+  moreover assume "(x, y) \<in> S1" "(y, x) \<in> S2"
+  ultimately have "((x, y) \<in> S1 \<and> (y, x) \<in> S1) \<or> ((x, y) \<in> S2 \<and> (y, x) \<in> S2)" by blast
+  with `S1 \<in> R` `S2 \<in> R` assms(2) show "x = y" unfolding antisym_def by auto
+qed
 
 lemma chain_subset_Total_Union:
   assumes "chain\<^sub>\<subseteq> R" and "\<forall>r\<in>R. Total r"
@@ -554,12 +565,12 @@
     by (auto simp add: chain_subset_def)
   thus "(\<exists>r\<in>R. (a, b) \<in> r) \<or> (\<exists>r\<in>R. (b, a) \<in> r)"
   proof
-    assume "r \<subseteq> s" hence "(a, b) \<in> s \<or> (b, a) \<in> s" using assms(2) A
-      by (simp add: total_on_def) (metis (no_types) mono_Field subsetD)
+    assume "r \<subseteq> s" hence "(a, b) \<in> s \<or> (b, a) \<in> s" using assms(2) A mono_Field[of r s]
+      by (auto simp add: total_on_def)
     thus ?thesis using `s \<in> R` by blast
   next
-    assume "s \<subseteq> r" hence "(a, b) \<in> r \<or> (b, a) \<in> r" using assms(2) A
-      by (simp add: total_on_def) (metis (no_types) mono_Field subsetD)
+    assume "s \<subseteq> r" hence "(a, b) \<in> r \<or> (b, a) \<in> r" using assms(2) A mono_Field[of s r]
+      by (fastforce simp add: total_on_def)
     thus ?thesis using `r \<in> R` by blast
   qed
 qed
@@ -633,8 +644,8 @@
     moreover have "\<forall>r \<in> R. r initial_segment_of \<Union>R" using Ris
       by(simp add: Chains_init_seg_of_Union)
     ultimately have "\<Union>R \<in> ?WO \<and> (\<forall>r\<in>R. (r, \<Union>R) \<in> I)"
-      using mono_Chains [OF I_init] and `R \<in> Chains I`
-      by (simp (no_asm) add: I_def del: Field_Union) (metis Chains_wo)
+      using mono_Chains [OF I_init] Chains_wo[of R] and `R \<in> Chains I`
+      unfolding I_def by blast
   }
   hence 1: "\<forall>R \<in> Chains I. \<exists>u\<in>Field I. \<forall>r\<in>R. (r, u) \<in> I" by (subst FI) blast
 --{*Zorn's Lemma yields a maximal well-order m:*}
@@ -671,8 +682,8 @@
     moreover have "Total ?m" using `Total m` and Fm by (auto simp: total_on_def)
     moreover have "wf (?m - Id)"
     proof -
-      have "wf ?s" using `x \<notin> Field m`
-        by (auto simp add: wf_eq_minimal Field_def) metis
+      have "wf ?s" using `x \<notin> Field m` unfolding wf_eq_minimal Field_def
+        by (auto simp: Bex_def)
       thus ?thesis using `wf (m - Id)` and `x \<notin> Field m`
         wf_subset [OF `wf ?s` Diff_subset]
         unfolding Un_Diff Field_def by (auto intro: wf_Un)