# HG changeset patch
# User blanchet
# Date 1384820990 -3600
# Node ID a2874c8b3558e9b67162318a583507fe39f809af
# Parent  5c9819d7713be2260ab2cfa538520786d70c7645
optimized 'bad apple' method calls

diff -r 5c9819d7713b -r a2874c8b3558 src/HOL/Cardinals/Cardinal_Arithmetic_FP.thy
--- a/src/HOL/Cardinals/Cardinal_Arithmetic_FP.thy	Mon Nov 18 18:04:45 2013 +0100
+++ b/src/HOL/Cardinals/Cardinal_Arithmetic_FP.thy	Tue Nov 19 01:29:50 2013 +0100
@@ -17,7 +17,7 @@
 
 (*should supersede a weaker lemma from the library*)
 lemma dir_image_Field: "Field (dir_image r f) = f ` Field r"
-unfolding dir_image_def Field_def Range_def Domain_def by fastforce
+unfolding dir_image_def Field_def Range_def Domain_def by fast
 
 lemma card_order_dir_image:
   assumes bij: "bij f" and co: "card_order r"
@@ -64,11 +64,15 @@
                   \<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
-  proof safe
+  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 (auto simp: Func_def fun_eq_iff, metis pair_collapse)
+  qed
   thus ?thesis using card_of_ordIso by blast
 qed
 
@@ -169,7 +173,7 @@
 lemma csum_Cnotzero1:
   "Cnotzero r1 \<Longrightarrow> Cnotzero (r1 +c r2)"
 unfolding csum_def
-by (metis Cnotzero_imp_not_empty Field_card_of Plus_eq_empty_conv card_of_card_order_on czeroE)
+by (metis Cnotzero_imp_not_empty Plus_eq_empty_conv card_of_Card_order card_of_ordIso_czero_iff_empty)
 
 lemma card_order_csum:
   assumes "card_order r1" "card_order r2"
@@ -463,7 +467,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 blast
+    using r p cexp_mono[OF _ _ _ Cp] cexp_mono[OF _ _ _ Cr] by metis
 qed
 
 lemma cexp_cong1:
diff -r 5c9819d7713b -r a2874c8b3558 src/HOL/Cardinals/Cardinal_Order_Relation_FP.thy
--- a/src/HOL/Cardinals/Cardinal_Order_Relation_FP.thy	Mon Nov 18 18:04:45 2013 +0100
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation_FP.thy	Tue Nov 19 01:29:50 2013 +0100
@@ -5,7 +5,7 @@
 Cardinal-order relations (FP).
 *)
 
-header {* Cardinal-Order Relations (FP)  *}
+header {* Cardinal-Order Relations (FP) *}
 
 theory Cardinal_Order_Relation_FP
 imports Constructions_on_Wellorders_FP
@@ -466,7 +466,7 @@
   let ?h = "\<lambda> b'::'b. if b' = b then a else undefined"
   have "inj_on ?h {b} \<and> ?h ` {b} \<le> A"
   using * unfolding inj_on_def by auto
-  thus ?thesis using card_of_ordLeq by blast
+  thus ?thesis using card_of_ordLeq by fast
 qed
 
 
@@ -576,7 +576,7 @@
     qed
   qed
   hence "bij_betw f ((A <+> B) <+> C) (A <+> B <+> C)"
-  unfolding bij_betw_def inj_on_def f_def by force
+  unfolding bij_betw_def inj_on_def f_def by fastforce
   thus ?thesis using card_of_ordIso by blast
 qed
 
@@ -593,8 +593,7 @@
   proof-
     {fix d1 and d2 assume "d1 \<in> A <+> C \<and> d2 \<in> A <+> C" and
                           "g d1 = g d2"
-     hence "d1 = d2" using 1 unfolding inj_on_def
-     by(case_tac d1, case_tac d2, auto simp add: g_def)
+     hence "d1 = d2" using 1 unfolding inj_on_def g_def by force
     }
     moreover
     {fix d assume "d \<in> A <+> C"
@@ -962,9 +961,9 @@
     let ?r' = "Restr r (rel.underS r a)"
     assume Case2: "a \<in> Field r"
     hence 1: "rel.under r a = rel.underS r a \<union> {a} \<and> a \<notin> rel.underS r a"
-    using 0 rel.Refl_under_underS rel.underS_notIn by fastforce
+    using 0 rel.Refl_under_underS rel.underS_notIn by metis
     have 2: "wo_rel.ofilter r (rel.underS r a) \<and> rel.underS r a < Field r"
-    using 0 wo_rel.underS_ofilter * 1 Case2 by auto
+    using 0 wo_rel.underS_ofilter * 1 Case2 by fast
     hence "?r' <o r" using 0 using ofilter_ordLess by blast
     moreover
     have "Field ?r' = rel.underS r a \<and> Well_order ?r'"
@@ -1370,7 +1369,7 @@
 
 
 lemma Restr_natLeq: "Restr natLeq {0 ..< n} = natLeq_on n"
-by auto
+by force
 
 
 lemma Restr_natLeq2:
@@ -1393,9 +1392,9 @@
 
 lemma natLeq_on_ofilter_less_eq:
 "n \<le> m \<Longrightarrow> wo_rel.ofilter (natLeq_on m) {0 ..< n}"
-by (auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def,
-    simp add: Field_natLeq_on, unfold rel.under_def, auto)
-
+apply (auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def)
+apply (simp add: Field_natLeq_on)
+by (auto simp add: rel.under_def)
 
 lemma natLeq_on_ofilter_iff:
 "wo_rel.ofilter (natLeq_on m) A = (\<exists>n \<le> m. A = {0 ..< n})"
@@ -1450,8 +1449,8 @@
 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 blast
-
+      card_of_Well_order natLeq_Well_order
+by auto
 
 lemma ordIso_natLeq_on_imp_finite:
 "|A| =o natLeq_on n \<Longrightarrow> finite A"
@@ -1502,7 +1501,8 @@
 lemma natLeq_on_ordLeq_less:
 "((natLeq_on m) <o (natLeq_on n)) = (m < n)"
 using not_ordLeq_iff_ordLess[of "natLeq_on m" "natLeq_on n"]
-natLeq_on_Well_order natLeq_on_ordLeq_less_eq by auto
+  natLeq_on_Well_order natLeq_on_ordLeq_less_eq
+by fastforce
 
 
 
@@ -1845,7 +1845,7 @@
 and "Card_order r"
 shows "|A Un B| \<le>o r"
 using assms card_of_Plus_ordLeq_infinite_Field card_of_Un_Plus_ordLeq
-ordLeq_transitive by blast
+ordLeq_transitive by fast
 
 
 
@@ -2039,7 +2039,11 @@
 lemma bij_betw_curr:
 "bij_betw (curr A) (Func (A <*> B) C) (Func A (Func B C))"
 unfolding bij_betw_def inj_on_def image_def
-using curr_in curr_inj curr_surj by blast
+apply (intro impI conjI ballI)
+apply (erule curr_inj[THEN iffD1], assumption+)
+apply auto
+apply (erule curr_in)
+using curr_surj by blast
 
 lemma card_of_Func_Times:
 "|Func (A <*> B) C| =o |Func A (Func B C)|"
@@ -2075,8 +2079,8 @@
   moreover
   {fix f assume "f \<in> Func A B"
    moreover obtain a where "a \<in> A" using R by blast
-   ultimately obtain b where "b \<in> B" unfolding Func_def by(cases "f a = undefined", force+)
-   with R have False by auto
+   ultimately obtain b where "b \<in> B" unfolding Func_def by blast
+   with R have False by blast
   }
   thus ?L by blast
 qed
diff -r 5c9819d7713b -r a2874c8b3558 src/HOL/Cardinals/Constructions_on_Wellorders_FP.thy
--- a/src/HOL/Cardinals/Constructions_on_Wellorders_FP.thy	Mon Nov 18 18:04:45 2013 +0100
+++ b/src/HOL/Cardinals/Constructions_on_Wellorders_FP.thy	Tue Nov 19 01:29:50 2013 +0100
@@ -90,7 +90,7 @@
 
 lemma Refl_Field_Restr:
 "Refl r \<Longrightarrow> Field(Restr r A) = (Field r) Int A"
-by (auto simp add: refl_on_def Field_def)
+unfolding refl_on_def Field_def by blast
 
 
 lemma Refl_Field_Restr2:
@@ -807,7 +807,7 @@
   have "wo_rel.ofilter r (rel.underS r a)" using 0
   by (simp add: wo_rel_def wo_rel.underS_ofilter)
   hence "Field ?p = rel.underS r a" using 0 Field_Restr_ofilter by blast
-  hence "Field ?p < Field r" using rel.underS_Field2 1 by fastforce
+  hence "Field ?p < Field r" using rel.underS_Field2 1 by fast
   moreover have "?p <o r" using underS_Restr_ordLess[of r a] 0 1 by blast
   ultimately
   show "\<exists>p. Field p < Field r \<and> r' =o p \<and> p <o r" using 2 by blast
@@ -894,7 +894,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 blast
+  ultimately show ?thesis using assms ordLeq_total ordIso_symmetric by metis
 qed
 
 
diff -r 5c9819d7713b -r a2874c8b3558 src/HOL/Cardinals/Fun_More_FP.thy
--- a/src/HOL/Cardinals/Fun_More_FP.thy	Mon Nov 18 18:04:45 2013 +0100
+++ b/src/HOL/Cardinals/Fun_More_FP.thy	Tue Nov 19 01:29:50 2013 +0100
@@ -232,7 +232,7 @@
 using assms
 using finite_atLeastLessThan[of m] finite_atLeastLessThan[of n]
       card_atLeastLessThan[of m] card_atLeastLessThan[of n]
-      card_inj_on_le[of f "{0 ..< m}" "{0 ..< n}"] by auto
+      card_inj_on_le[of f "{0 ..< m}" "{0 ..< n}"] by fastforce
 
 
 
diff -r 5c9819d7713b -r a2874c8b3558 src/HOL/Cardinals/Wellorder_Embedding_FP.thy
--- a/src/HOL/Cardinals/Wellorder_Embedding_FP.thy	Mon Nov 18 18:04:45 2013 +0100
+++ b/src/HOL/Cardinals/Wellorder_Embedding_FP.thy	Tue Nov 19 01:29:50 2013 +0100
@@ -331,8 +331,7 @@
   show "bij_betw f (rel.under r a) (rel.under r' (f a))"
   proof(unfold bij_betw_def, auto)
     show  "inj_on f (rel.under r a)"
-    using *
-    by (auto simp add: rel.under_Field subset_inj_on)
+    using * by (metis (no_types) rel.under_Field subset_inj_on)
   next
     fix b assume "b \<in> rel.under r a"
     thus "f b \<in> rel.under r' (f a)"
@@ -395,7 +394,7 @@
      unfolding rel.under_def using 11 Refl
      by (auto simp add: refl_on_def)
      hence "b1 = b2" using BIJ * ** ***
-     by (auto simp add: bij_betw_def inj_on_def)
+     by (simp add: bij_betw_def inj_on_def)
     }
     moreover
      {assume "(b2,b1) \<in> r"
@@ -403,7 +402,7 @@
      unfolding rel.under_def using 11 Refl
      by (auto simp add: refl_on_def)
      hence "b1 = b2" using BIJ * ** ***
-     by (auto simp add: bij_betw_def inj_on_def)
+     by (simp add: bij_betw_def inj_on_def)
     }
     ultimately
     show "b1 = b2"
@@ -578,7 +577,7 @@
     fix b assume *: "b \<in> rel.underS r a"
     have "f b \<noteq> f a \<and> (f b, f a) \<in> r'"
     using subField Well' SUC NE *
-          wo_rel.suc_greater[of r' "f`(rel.underS r a)" "f b"] by auto
+          wo_rel.suc_greater[of r' "f`(rel.underS r a)" "f b"] by force
     thus "f b \<in> rel.underS r' (f a)"
     unfolding rel.underS_def by simp
   qed
@@ -800,7 +799,7 @@
     then obtain a where "?chi a" by blast
     hence "\<exists>f'. embed r' r f'"
     using wellorders_totally_ordered_aux2[of r r' g f a]
-          WELL WELL' Main1 Main2 test_def by blast
+          WELL WELL' Main1 Main2 test_def by fast
     thus ?thesis by blast
   qed
 qed
@@ -1091,7 +1090,7 @@
    have "bij_betw f (rel.under r a) (rel.under r' (f a))"
    proof(unfold bij_betw_def, auto)
      show "inj_on f (rel.under r a)"
-     using 1 2 by (auto simp add: subset_inj_on)
+     using 1 2 by (metis subset_inj_on)
    next
      fix b assume "b \<in> rel.under r a"
      hence "a \<in> Field r \<and> b \<in> Field r \<and> (b,a) \<in> r"
diff -r 5c9819d7713b -r a2874c8b3558 src/HOL/Library/Order_Relation.thy
--- a/src/HOL/Library/Order_Relation.thy	Mon Nov 18 18:04:45 2013 +0100
+++ b/src/HOL/Library/Order_Relation.thy	Tue Nov 19 01:29:50 2013 +0100
@@ -93,7 +93,7 @@
 using mono_Field[of "r - Id" r] Diff_subset[of r Id]
 proof(auto)
   have "r \<noteq> {}" using NID by fast
-  then obtain b and c where "b \<noteq> c \<and> (b,c) \<in> r" using NID by fast
+  then obtain b and c where "b \<noteq> c \<and> (b,c) \<in> r" using NID by auto
   hence 1: "b \<noteq> c \<and> {b,c} \<le> Field r" by (auto simp: Field_def)
   (*  *)
   fix a assume *: "a \<in> Field r"
diff -r 5c9819d7713b -r a2874c8b3558 src/HOL/Library/Order_Union.thy
--- a/src/HOL/Library/Order_Union.thy	Mon Nov 18 18:04:45 2013 +0100
+++ b/src/HOL/Library/Order_Union.thy	Tue Nov 19 01:29:50 2013 +0100
@@ -31,7 +31,7 @@
     assume Case1: "B \<noteq> {}"
     hence "B \<noteq> {} \<and> B \<le> Field r" using B_def by auto
     then obtain a where 1: "a \<in> B" and 2: "\<forall>a1 \<in> B. (a1,a) \<notin> r"
-    using WF  unfolding wf_eq_minimal2 by blast
+    using WF unfolding wf_eq_minimal2 by metis
     hence 3: "a \<in> Field r \<and> a \<notin> Field r'" using B_def FLD by auto
     (*  *)
     have "\<forall>a1 \<in> A. (a1,a) \<notin> r Osum r'"
@@ -59,7 +59,7 @@
     assume Case2: "B = {}"
     hence 1: "A \<noteq> {} \<and> A \<le> Field r'" using * ** B_def by auto
     then obtain a' where 2: "a' \<in> A" and 3: "\<forall>a1' \<in> A. (a1',a') \<notin> r'"
-    using WF' unfolding wf_eq_minimal2 by blast
+    using WF' unfolding wf_eq_minimal2 by metis
     hence 4: "a' \<in> Field r' \<and> a' \<notin> Field r" using 1 FLD by blast
     (*  *)
     have "\<forall>a1' \<in> A. (a1',a') \<notin> r Osum r'"
@@ -299,7 +299,7 @@
       using assms Total_Id_Field by blast
       hence ?thesis unfolding Osum_def by auto
      }
-     ultimately show ?thesis using * unfolding Osum_def by blast
+     ultimately show ?thesis using * unfolding Osum_def by fast
    qed
   }
   thus ?thesis by(auto simp add: Osum_def)
@@ -308,12 +308,7 @@
 lemma wf_Int_Times:
 assumes "A Int B = {}"
 shows "wf(A \<times> B)"
-proof(unfold wf_def, auto)
-  fix P x
-  assume *: "\<forall>x. (\<forall>y. y \<in> A \<and> x \<in> B \<longrightarrow> P y) \<longrightarrow> P x"
-  moreover have "\<forall>y \<in> A. P y" using assms * by blast
-  ultimately show "P x" using * by (case_tac "x \<in> B", auto)
-qed
+unfolding wf_def using assms by blast
 
 lemma Osum_wf_Id:
 assumes TOT: "Total r" and TOT': "Total r'" and
@@ -343,7 +338,7 @@
     using 1 WF' wf_Un[of "Field r \<times> Field r'" "r' - Id"]
     by (auto simp add: Un_commute)
    }
-   ultimately have ?thesis by (auto simp add: wf_subset)
+   ultimately have ?thesis by (metis wf_subset)
   }
   moreover
   {assume Case22: "r' \<le> Id"
@@ -356,7 +351,7 @@
     using 1 WF wf_Un[of "r - Id" "Field r \<times> Field r'"]
     by (auto simp add: Un_commute)
    }
-   ultimately have ?thesis by (auto simp add: wf_subset)
+   ultimately have ?thesis by (metis wf_subset)
   }
   ultimately show ?thesis by blast
 qed
diff -r 5c9819d7713b -r a2874c8b3558 src/HOL/Library/Wfrec.thy
--- a/src/HOL/Library/Wfrec.thy	Mon Nov 18 18:04:45 2013 +0100
+++ b/src/HOL/Library/Wfrec.thy	Tue Nov 19 01:29:50 2013 +0100
@@ -48,7 +48,7 @@
 apply (fast dest!: theI')
 apply (erule wfrec_rel.cases, simp)
 apply (erule allE, erule allE, erule allE, erule mp)
-apply (fast intro: the_equality [symmetric])
+apply (blast intro: the_equality [symmetric])
 done
 
 lemma adm_lemma: "adm_wf R (%f x. F (cut f R x) x)"
diff -r 5c9819d7713b -r a2874c8b3558 src/HOL/Library/Zorn.thy
--- a/src/HOL/Library/Zorn.thy	Mon Nov 18 18:04:45 2013 +0100
+++ b/src/HOL/Library/Zorn.thy	Tue Nov 19 01:29:50 2013 +0100
@@ -71,7 +71,7 @@
 
 lemma suc_not_equals:
   "chain C \<Longrightarrow> \<not> maxchain C \<Longrightarrow> suc C \<noteq> C"
-  by (auto simp: suc_def) (metis less_irrefl not_maxchain_Some)
+  by (auto simp: suc_def) (metis (no_types) less_irrefl not_maxchain_Some)
 
 lemma subset_suc:
   assumes "X \<subseteq> Y" shows "X \<subseteq> suc Y"
@@ -258,7 +258,7 @@
   shows "chain X"
 using assms
 proof (induct)
-  case (suc X) then show ?case by (simp add: suc_def) (metis not_maxchain_Some)
+  case (suc X) then show ?case by (simp add: suc_def) (metis (no_types) not_maxchain_Some)
 next
   case (Union X)
   then have "\<Union>X \<subseteq> A" by (auto dest: suc_Union_closed_in_carrier)
@@ -378,7 +378,7 @@
         using `subset.maxchain A M` by (auto simp: subset.maxchain_def)
     qed
   qed
-  ultimately show ?thesis by blast
+  ultimately show ?thesis by metis
 qed
 
 text{*Alternative version of Zorn's lemma for the subset relation.*}
@@ -423,7 +423,7 @@
   unfolding Chains_def by blast
 
 lemma chain_subset_alt_def: "chain\<^sub>\<subseteq> C = subset.chain UNIV C"
-  by (auto simp add: chain_subset_def subset.chain_def)
+  unfolding chain_subset_def subset.chain_def by fast
 
 lemma chains_alt_def: "chains A = {C. subset.chain A C}"
   by (simp add: chains_def chain_subset_alt_def subset.chain_def)
@@ -487,7 +487,7 @@
       fix a B assume aB: "B \<in> C" "a \<in> B"
       with 1 obtain x where "x \<in> Field r" and "B = r\<inverse> `` {x}" by auto
       thus "(a, u) \<in> r" using uA and aB and `Preorder r`
-        by (auto simp add: preorder_on_def refl_on_def) (metis transD)
+        unfolding preorder_on_def refl_on_def by simp (fast dest: transD)
     qed
     then have "\<exists>u\<in>Field r. ?P u" using `u \<in> Field r` by blast
   }
@@ -524,8 +524,7 @@
 
 lemma trans_init_seg_of:
   "r initial_segment_of s \<Longrightarrow> s initial_segment_of t \<Longrightarrow> r initial_segment_of t"
-  by (simp (no_asm_use) add: init_seg_of_def)
-     (metis UnCI Un_absorb2 subset_trans)
+  by (simp (no_asm_use) add: init_seg_of_def) blast
 
 lemma antisym_init_seg_of:
   "r initial_segment_of s \<Longrightarrow> s initial_segment_of r \<Longrightarrow> r = s"
@@ -539,14 +538,13 @@
   "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)
-apply (metis subsetD)
-done
+by (metis subsetD)
 
 lemma chain_subset_antisym_Union:
   "chain\<^sub>\<subseteq> R \<Longrightarrow> \<forall>r\<in>R. antisym r \<Longrightarrow> antisym (\<Union>R)"
-apply (auto simp add: chain_subset_def antisym_def)
-apply (metis subsetD)
-done
+unfolding chain_subset_def antisym_def
+apply simp
+by (metis (no_types) subsetD)
 
 lemma chain_subset_Total_Union:
   assumes "chain\<^sub>\<subseteq> R" and "\<forall>r\<in>R. Total r"
@@ -558,11 +556,11 @@
   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 mono_Field subsetD)
+      by (simp add: total_on_def) (metis (no_types) mono_Field subsetD)
     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 mono_Field subsetD)
+      by (simp add: total_on_def) (metis (no_types) mono_Field subsetD)
     thus ?thesis using `r \<in> R` by blast
   qed
 qed
@@ -604,7 +602,7 @@
   def I \<equiv> "init_seg_of \<inter> ?WO \<times> ?WO"
   have I_init: "I \<subseteq> init_seg_of" by (auto simp: I_def)
   hence subch: "\<And>R. R \<in> Chains I \<Longrightarrow> chain\<^sub>\<subseteq> R"
-    by (auto simp: init_seg_of_def chain_subset_def Chains_def)
+    unfolding init_seg_of_def chain_subset_def Chains_def by blast
   have Chains_wo: "\<And>R r. R \<in> Chains I \<Longrightarrow> r \<in> R \<Longrightarrow> Well_order r"
     by (simp add: Chains_def I_def) blast
   have FI: "Field I = ?WO" by (auto simp add: I_def init_seg_of_def Field_def)
@@ -619,7 +617,7 @@
     have "\<forall>r\<in>R. Refl r" and "\<forall>r\<in>R. trans r" and "\<forall>r\<in>R. antisym r"
       and "\<forall>r\<in>R. Total r" and "\<forall>r\<in>R. wf (r - Id)"
       using Chains_wo [OF `R \<in> Chains I`] by (simp_all add: order_on_defs)
-    have "Refl (\<Union>R)" using `\<forall>r\<in>R. Refl r` by (auto simp: refl_on_def)
+    have "Refl (\<Union>R)" using `\<forall>r\<in>R. Refl r` unfolding refl_on_def by fastforce
     moreover have "trans (\<Union>R)"
       by (rule chain_subset_trans_Union [OF subch `\<forall>r\<in>R. trans r`])
     moreover have "antisym (\<Union>R)"
@@ -630,7 +628,7 @@
     proof -
       have "(\<Union>R) - Id = \<Union>{r - Id | r. r \<in> R}" by blast
       with `\<forall>r\<in>R. wf (r - Id)` and wf_Union_wf_init_segs [OF Chains_inits_DiffI [OF Ris]]
-      show ?thesis by (simp (no_asm_simp)) blast
+      show ?thesis by fastforce
     qed
     ultimately have "Well_order (\<Union>R)" by(simp add:order_on_defs)
     moreover have "\<forall>r \<in> R. r initial_segment_of \<Union>R" using Ris
@@ -643,7 +641,7 @@
 --{*Zorn's Lemma yields a maximal well-order m:*}
   then obtain m::"'a rel" where "Well_order m" and
     max: "\<forall>r. Well_order r \<and> (m, r) \<in> I \<longrightarrow> r = m"
-    using Zorns_po_lemma[OF 0 1] by (auto simp:FI)
+    using Zorns_po_lemma[OF 0 1] unfolding FI by fastforce
 --{*Now show by contradiction that m covers the whole type:*}
   { fix x::'a assume "x \<notin> Field m"
 --{*We assume that x is not covered and extend m at the top with x*}
@@ -666,7 +664,7 @@
     have "Refl m" and "trans m" and "antisym m" and "Total m" and "wf (m - Id)"
       using `Well_order m` by (simp_all add: order_on_defs)
 --{*We show that the extension is a well-order*}
-    have "Refl ?m" using `Refl m` Fm by (auto simp: refl_on_def)
+    have "Refl ?m" using `Refl m` Fm unfolding refl_on_def by blast
     moreover have "trans ?m" using `trans m` and `x \<notin> Field m`
       unfolding trans_def Field_def by blast
     moreover have "antisym ?m" using `antisym m` and `x \<notin> Field m`
@@ -678,7 +676,7 @@
         by (auto simp add: wf_eq_minimal Field_def) metis
       thus ?thesis using `wf (m - Id)` and `x \<notin> Field m`
         wf_subset [OF `wf ?s` Diff_subset]
-        by (fastforce intro!: wf_Un simp add: Un_Diff Field_def)
+        unfolding Un_Diff Field_def by (auto intro: wf_Un)
     qed
     ultimately have "Well_order ?m" by (simp add: order_on_defs)
 --{*We show that the extension is above m*}
@@ -709,7 +707,7 @@
   moreover have "Total ?r" using `Total r` by (simp add:total_on_def 1 univ)
   moreover have "wf (?r - Id)" by (rule wf_subset [OF `wf (r - Id)`]) blast
   ultimately have "Well_order ?r" by (simp add: order_on_defs)
-  with 1 show ?thesis by metis
+  with 1 show ?thesis by auto
 qed
 
 subsection {* Extending Well-founded Relations to Well-Orders *}
@@ -732,7 +730,7 @@
 
 lemma downset_onD:
   "downset_on A r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> y \<in> A \<Longrightarrow> x \<in> A"
-  by (auto simp: downset_on_def)
+  unfolding downset_on_def by blast
 
 text {*Extensions of relations w.r.t.\ a given set.*}
 definition extension_on where
@@ -755,7 +753,8 @@
   assumes "chain\<^sub>\<subseteq> R" and "\<And>r. r \<in> R \<Longrightarrow> extension_on (Field r) r p"
   shows "extension_on (Field (\<Union>R)) (\<Union>R) p"
   using assms
-  by (simp add: chain_subset_def extension_on_def) (metis mono_Field set_mp)
+  by (simp add: chain_subset_def extension_on_def)
+     (metis (no_types) mono_Field set_mp)
 
 lemma downset_on_empty [simp]: "downset_on {} p"
   by (auto simp: downset_on_def)
@@ -789,7 +788,7 @@
       "\<And>r. r \<in> R \<Longrightarrow> downset_on (Field r) p" and
       "\<And>r. r \<in> R \<Longrightarrow> extension_on (Field r) r p"
       using Chains_wo [OF `R \<in> Chains I`] by (simp_all add: order_on_defs)
-    have "Refl (\<Union>R)" using `\<forall>r\<in>R. Refl r` by (auto simp: refl_on_def)
+    have "Refl (\<Union>R)" using `\<forall>r\<in>R. Refl r`  unfolding refl_on_def by fastforce
     moreover have "trans (\<Union>R)"
       by (rule chain_subset_trans_Union [OF subch `\<forall>r\<in>R. trans r`])
     moreover have "antisym (\<Union>R)"
@@ -800,7 +799,7 @@
     proof -
       have "(\<Union>R) - Id = \<Union>{r - Id | r. r \<in> R}" by blast
       with `\<forall>r\<in>R. wf (r - Id)` wf_Union_wf_init_segs [OF Chains_inits_DiffI [OF Ris]]
-      show ?thesis by (simp (no_asm_simp)) blast
+      show ?thesis by fastforce
     qed
     ultimately have "Well_order (\<Union>R)" by (simp add: order_on_defs)
     moreover have "\<forall>r\<in>R. r initial_segment_of \<Union>R" using Ris
@@ -853,8 +852,9 @@
       using `extension_on (Field m) m p` `downset_on (Field m) p`
       by (subst Fm) (auto simp: extension_on_def dest: downset_onD)
     moreover have "downset_on (Field ?m) p"
+      apply (subst Fm)
       using `downset_on (Field m) p` and min
-      by (subst Fm, simp add: downset_on_def Field_def) (metis Domain_iff)
+      unfolding downset_on_def Field_def by blast
     moreover have "(m, ?m) \<in> I"
       using `Well_order m` and `Well_order ?m` and
       `downset_on (Field m) p` and `downset_on (Field ?m) p` and
@@ -867,7 +867,7 @@
   qed
   have "p \<subseteq> m"
     using `Field p \<subseteq> Field m` and `extension_on (Field m) m p`
-    by (force simp: Field_def extension_on_def)
+    unfolding Field_def extension_on_def by auto fast
   with `Well_order m` show ?thesis by blast
 qed