load Metis a little later
authortraytel
Fri Feb 28 17:54:52 2014 +0100 (2014-02-28)
changeset 55811aa1acc25126b
parent 55810 63d63d854fae
child 55815 557003a7cf78
load Metis a little later
src/HOL/BNF_Cardinal_Arithmetic.thy
src/HOL/BNF_Cardinal_Order_Relation.thy
src/HOL/BNF_Comp.thy
src/HOL/BNF_Constructions_on_Wellorders.thy
src/HOL/BNF_Def.thy
src/HOL/BNF_FP_Base.thy
src/HOL/BNF_LFP.thy
src/HOL/BNF_Wellorder_Embedding.thy
src/HOL/Basic_BNFs.thy
src/HOL/Cardinals/Wellorder_Extension.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Library/Multiset.thy
src/HOL/List.thy
src/HOL/Power.thy
src/HOL/Tools/BNF/bnf_fp_util.ML
src/HOL/Transfer.thy
src/HOL/Zorn.thy
     1.1 --- a/src/HOL/BNF_Cardinal_Arithmetic.thy	Fri Feb 28 22:00:13 2014 +0100
     1.2 +++ b/src/HOL/BNF_Cardinal_Arithmetic.thy	Fri Feb 28 17:54:52 2014 +0100
     1.3 @@ -57,15 +57,19 @@
     1.4                    \<lambda>x. if x \<in> A then snd (fg x) else undefined)"
     1.5    let ?G = "\<lambda>(f, g) x. if x \<in> A then (f x, g x) else undefined"
     1.6    have "bij_betw ?F ?LHS ?RHS" unfolding bij_betw_def inj_on_def
     1.7 -  apply safe
     1.8 -     apply (simp add: Func_def fun_eq_iff)
     1.9 -     apply (metis (no_types) pair_collapse)
    1.10 -    apply (auto simp: Func_def fun_eq_iff)[2]
    1.11 -  proof -
    1.12 -    fix f g assume "f \<in> Func A B" "g \<in> Func A C"
    1.13 -    thus "(f, g) \<in> ?F ` Func A (B \<times> C)"
    1.14 -      by (intro image_eqI[of _ _ "?G (f, g)"]) (auto simp: Func_def)
    1.15 -  qed
    1.16 +  proof (intro conjI impI ballI equalityI subsetI)
    1.17 +    fix f g assume *: "f \<in> Func A (B \<times> C)" "g \<in> Func A (B \<times> C)" "?F f = ?F g"
    1.18 +    show "f = g"
    1.19 +    proof
    1.20 +      fix x from * have "fst (f x) = fst (g x) \<and> snd (f x) = snd (g x)"
    1.21 +        by (case_tac "x \<in> A") (auto simp: Func_def fun_eq_iff split: if_splits)
    1.22 +      then show "f x = g x" by (subst (1 2) surjective_pairing) simp
    1.23 +    qed
    1.24 +  next
    1.25 +    fix fg assume "fg \<in> Func A B \<times> Func A C"
    1.26 +    thus "fg \<in> ?F ` Func A (B \<times> C)"
    1.27 +      by (intro image_eqI[of _ _ "?G fg"]) (auto simp: Func_def)
    1.28 +  qed (auto simp: Func_def fun_eq_iff)
    1.29    thus ?thesis using card_of_ordIso by blast
    1.30  qed
    1.31  
    1.32 @@ -89,7 +93,7 @@
    1.33  
    1.34  (*helper*)
    1.35  lemma Cnotzero_imp_not_empty: "Cnotzero r \<Longrightarrow> Field r \<noteq> {}"
    1.36 -by (metis Card_order_iff_ordIso_card_of czero_def)
    1.37 +  unfolding Card_order_iff_ordIso_card_of czero_def by force
    1.38  
    1.39  lemma czeroI:
    1.40    "\<lbrakk>Card_order r; Field r = {}\<rbrakk> \<Longrightarrow> r =o czero"
    1.41 @@ -127,33 +131,35 @@
    1.42  
    1.43  lemma Cfinite_ordLess_Cinfinite: "\<lbrakk>Cfinite r; Cinfinite s\<rbrakk> \<Longrightarrow> r <o s"
    1.44    unfolding cfinite_def cinfinite_def
    1.45 -  by (metis card_order_on_well_order_on finite_ordLess_infinite)
    1.46 +  by (blast intro: finite_ordLess_infinite card_order_on_well_order_on)
    1.47  
    1.48  lemmas natLeq_card_order = natLeq_Card_order[unfolded Field_natLeq]
    1.49  
    1.50  lemma natLeq_cinfinite: "cinfinite natLeq"
    1.51 -unfolding cinfinite_def Field_natLeq by (metis infinite_UNIV_nat)
    1.52 +unfolding cinfinite_def Field_natLeq by (rule infinite_UNIV_nat)
    1.53  
    1.54  lemma natLeq_ordLeq_cinfinite:
    1.55    assumes inf: "Cinfinite r"
    1.56    shows "natLeq \<le>o r"
    1.57  proof -
    1.58 -  from inf have "natLeq \<le>o |Field r|" by (metis cinfinite_def infinite_iff_natLeq_ordLeq)
    1.59 +  from inf have "natLeq \<le>o |Field r|" unfolding cinfinite_def
    1.60 +    using infinite_iff_natLeq_ordLeq by blast
    1.61    also from inf have "|Field r| =o r" by (simp add: card_of_unique ordIso_symmetric)
    1.62    finally show ?thesis .
    1.63  qed
    1.64  
    1.65  lemma cinfinite_not_czero: "cinfinite r \<Longrightarrow> \<not> (r =o (czero :: 'a rel))"
    1.66 -unfolding cinfinite_def by (metis czeroE finite.emptyI)
    1.67 +unfolding cinfinite_def by (cases "Field r = {}") (auto dest: czeroE)
    1.68  
    1.69  lemma Cinfinite_Cnotzero: "Cinfinite r \<Longrightarrow> Cnotzero r"
    1.70 -by (metis cinfinite_not_czero)
    1.71 +by (rule conjI[OF cinfinite_not_czero]) simp_all
    1.72  
    1.73  lemma Cinfinite_cong: "\<lbrakk>r1 =o r2; Cinfinite r1\<rbrakk> \<Longrightarrow> Cinfinite r2"
    1.74 -by (metis Card_order_ordIso2 card_of_mono2 card_of_ordLeq_infinite cinfinite_def ordIso_iff_ordLeq)
    1.75 +using Card_order_ordIso2[of r1 r2] unfolding cinfinite_def ordIso_iff_ordLeq
    1.76 +by (auto dest: card_of_ordLeq_infinite[OF card_of_mono2])
    1.77  
    1.78  lemma cinfinite_mono: "\<lbrakk>r1 \<le>o r2; cinfinite r1\<rbrakk> \<Longrightarrow> cinfinite r2"
    1.79 -by (metis card_of_mono2 card_of_ordLeq_infinite cinfinite_def)
    1.80 +unfolding cinfinite_def by (auto dest: card_of_ordLeq_infinite[OF card_of_mono2])
    1.81  
    1.82  
    1.83  subsection {* Binary sum *}
    1.84 @@ -170,8 +176,8 @@
    1.85  
    1.86  lemma csum_Cnotzero1:
    1.87    "Cnotzero r1 \<Longrightarrow> Cnotzero (r1 +c r2)"
    1.88 -unfolding csum_def
    1.89 -by (metis Cnotzero_imp_not_empty Plus_eq_empty_conv card_of_Card_order card_of_ordIso_czero_iff_empty)
    1.90 +unfolding csum_def using Cnotzero_imp_not_empty[of r1] Plus_eq_empty_conv[of "Field r1" "Field r2"]
    1.91 +   card_of_ordIso_czero_iff_empty[of "Field r1 <+> Field r2"] by (auto intro: card_of_Card_order)
    1.92  
    1.93  lemma card_order_csum:
    1.94    assumes "card_order r1" "card_order r2"
    1.95 @@ -187,15 +193,15 @@
    1.96  
    1.97  lemma Cinfinite_csum1:
    1.98    "Cinfinite r1 \<Longrightarrow> Cinfinite (r1 +c r2)"
    1.99 -unfolding cinfinite_def csum_def by (metis Field_card_of card_of_Card_order finite_Plus_iff)
   1.100 +unfolding cinfinite_def csum_def by (rule conjI[OF _ card_of_Card_order]) (auto simp: Field_card_of)
   1.101  
   1.102  lemma Cinfinite_csum:
   1.103    "Cinfinite r1 \<or> Cinfinite r2 \<Longrightarrow> Cinfinite (r1 +c r2)"
   1.104 -unfolding cinfinite_def csum_def by (metis Field_card_of card_of_Card_order finite_Plus_iff)
   1.105 +unfolding cinfinite_def csum_def by (rule conjI[OF _ card_of_Card_order]) (auto simp: Field_card_of)
   1.106  
   1.107  lemma Cinfinite_csum_strong:
   1.108    "\<lbrakk>Cinfinite r1; Cinfinite r2\<rbrakk> \<Longrightarrow> Cinfinite (r1 +c r2)"
   1.109 -by (metis Cinfinite_csum)
   1.110 +by (erule Cinfinite_csum1)
   1.111  
   1.112  lemma csum_cong: "\<lbrakk>p1 =o r1; p2 =o r2\<rbrakk> \<Longrightarrow> p1 +c p2 =o r1 +c r2"
   1.113  by (simp only: csum_def ordIso_Plus_cong)
   1.114 @@ -233,15 +239,15 @@
   1.115  lemma csum_csum: "(r1 +c r2) +c (r3 +c r4) =o (r1 +c r3) +c (r2 +c r4)"
   1.116  proof -
   1.117    have "(r1 +c r2) +c (r3 +c r4) =o r1 +c r2 +c (r3 +c r4)"
   1.118 -    by (metis csum_assoc)
   1.119 +    by (rule csum_assoc)
   1.120    also have "r1 +c r2 +c (r3 +c r4) =o r1 +c (r2 +c r3) +c r4"
   1.121 -    by (metis csum_assoc csum_cong2 ordIso_symmetric)
   1.122 +    by (intro csum_assoc csum_cong2 ordIso_symmetric)
   1.123    also have "r1 +c (r2 +c r3) +c r4 =o r1 +c (r3 +c r2) +c r4"
   1.124 -    by (metis csum_com csum_cong1 csum_cong2)
   1.125 +    by (intro csum_com csum_cong1 csum_cong2)
   1.126    also have "r1 +c (r3 +c r2) +c r4 =o r1 +c r3 +c r2 +c r4"
   1.127 -    by (metis csum_assoc csum_cong2 ordIso_symmetric)
   1.128 +    by (intro csum_assoc csum_cong2 ordIso_symmetric)
   1.129    also have "r1 +c r3 +c r2 +c r4 =o (r1 +c r3) +c (r2 +c r4)"
   1.130 -    by (metis csum_assoc ordIso_symmetric)
   1.131 +    by (intro csum_assoc ordIso_symmetric)
   1.132    finally show ?thesis .
   1.133  qed
   1.134  
   1.135 @@ -264,10 +270,10 @@
   1.136    unfolding cfinite_def by (simp add: Card_order_cone)
   1.137  
   1.138  lemma cone_not_czero: "\<not> (cone =o czero)"
   1.139 -unfolding czero_def cone_def by (metis empty_not_insert card_of_empty3[of "{()}"] ordIso_iff_ordLeq)
   1.140 +unfolding czero_def cone_def ordIso_iff_ordLeq using card_of_empty3 empty_not_insert by blast
   1.141  
   1.142  lemma cone_ordLeq_Cnotzero: "Cnotzero r \<Longrightarrow> cone \<le>o r"
   1.143 -unfolding cone_def by (metis Card_order_singl_ordLeq czeroI)
   1.144 +unfolding cone_def by (rule Card_order_singl_ordLeq) (auto intro: czeroI)
   1.145  
   1.146  
   1.147  subsection {* Two *}
   1.148 @@ -280,7 +286,7 @@
   1.149  
   1.150  lemma ctwo_not_czero: "\<not> (ctwo =o czero)"
   1.151  using card_of_empty3[of "UNIV :: bool set"] ordIso_iff_ordLeq
   1.152 -unfolding czero_def ctwo_def by (metis UNIV_not_empty)
   1.153 +unfolding czero_def ctwo_def using UNIV_not_empty by auto
   1.154  
   1.155  lemma ctwo_Cnotzero: "Cnotzero ctwo"
   1.156  by (simp add: ctwo_not_czero Card_order_ctwo)
   1.157 @@ -330,13 +336,13 @@
   1.158  by (simp only: cprod_def ordLeq_Times_mono2)
   1.159  
   1.160  lemma ordLeq_cprod2: "\<lbrakk>Cnotzero p1; Card_order p2\<rbrakk> \<Longrightarrow> p2 \<le>o p1 *c p2"
   1.161 -unfolding cprod_def by (metis Card_order_Times2 czeroI)
   1.162 +unfolding cprod_def by (rule Card_order_Times2) (auto intro: czeroI)
   1.163  
   1.164  lemma cinfinite_cprod: "\<lbrakk>cinfinite r1; cinfinite r2\<rbrakk> \<Longrightarrow> cinfinite (r1 *c r2)"
   1.165  by (simp add: cinfinite_def cprod_def Field_card_of infinite_cartesian_product)
   1.166  
   1.167  lemma cinfinite_cprod2: "\<lbrakk>Cnotzero r1; Cinfinite r2\<rbrakk> \<Longrightarrow> cinfinite (r1 *c r2)"
   1.168 -by (metis cinfinite_mono ordLeq_cprod2)
   1.169 +by (rule cinfinite_mono) (auto intro: ordLeq_cprod2)
   1.170  
   1.171  lemma Cinfinite_cprod2: "\<lbrakk>Cnotzero r1; Cinfinite r2\<rbrakk> \<Longrightarrow> Cinfinite (r1 *c r2)"
   1.172  by (blast intro: cinfinite_cprod2 Card_order_cprod)
   1.173 @@ -364,7 +370,8 @@
   1.174  unfolding csum_def cprod_def by (simp add: Field_card_of card_of_Times_Plus_distrib ordIso_symmetric)
   1.175  
   1.176  lemma csum_absorb2': "\<lbrakk>Card_order r2; r1 \<le>o r2; cinfinite r1 \<or> cinfinite r2\<rbrakk> \<Longrightarrow> r1 +c r2 =o r2"
   1.177 -unfolding csum_def by (metis Card_order_Plus_infinite cinfinite_def cinfinite_mono)
   1.178 +unfolding csum_def by (rule conjunct2[OF Card_order_Plus_infinite])
   1.179 +  (auto simp: cinfinite_def dest: cinfinite_mono)
   1.180  
   1.181  lemma csum_absorb1':
   1.182    assumes card: "Card_order r2"
   1.183 @@ -390,10 +397,10 @@
   1.184    shows "p1 ^c p2 \<le>o r1 ^c r2"
   1.185  proof(cases "Field p1 = {}")
   1.186    case True
   1.187 -  hence "|Field |Func (Field p2) (Field p1)|| \<le>o cone"
   1.188 +  hence "Field p2 \<noteq> {} \<Longrightarrow> Func (Field p2) {} = {}" unfolding Func_is_emp by simp
   1.189 +  with True have "|Field |Func (Field p2) (Field p1)|| \<le>o cone"
   1.190      unfolding cone_def Field_card_of
   1.191 -    by (cases "Field p2 = {}", auto intro: card_of_ordLeqI2 simp: Func_empty)
   1.192 -       (metis Func_is_emp card_of_empty ex_in_conv)
   1.193 +    by (cases "Field p2 = {}", auto intro: surj_imp_ordLeq simp: Func_empty)
   1.194    hence "|Func (Field p2) (Field p1)| \<le>o cone" by (simp add: Field_card_of cexp_def)
   1.195    hence "p1 ^c p2 \<le>o cone" unfolding cexp_def .
   1.196    thus ?thesis
   1.197 @@ -429,7 +436,7 @@
   1.198    assumes 1: "p1 \<le>o r1" and 2: "p2 \<le>o r2"
   1.199    and n: "p2 =o czero \<Longrightarrow> r2 =o czero" and card: "Card_order p2"
   1.200    shows "p1 ^c p2 \<le>o r1 ^c r2"
   1.201 -  by (metis (full_types) "1" "2" card cexp_mono' czeroE czeroI n)
   1.202 +  by (rule cexp_mono'[OF 1 2 czeroE[OF n[OF czeroI[OF card]]]])
   1.203  
   1.204  lemma cexp_mono1:
   1.205    assumes 1: "p1 \<le>o r1" and q: "Card_order q"
   1.206 @@ -451,7 +458,7 @@
   1.207  lemma cexp_mono2_Cnotzero:
   1.208    assumes "p2 \<le>o r2" "Card_order q" "Cnotzero p2"
   1.209    shows "q ^c p2 \<le>o q ^c r2"
   1.210 -by (metis assms cexp_mono2' czeroI)
   1.211 +using assms(3) czeroI by (blast intro: cexp_mono2'[OF assms(1,2)])
   1.212  
   1.213  lemma cexp_cong:
   1.214    assumes 1: "p1 =o r1" and 2: "p2 =o r2"
   1.215 @@ -466,7 +473,7 @@
   1.216      and p: "r2 =o czero \<Longrightarrow> p2 =o czero"
   1.217       using 0 Cr Cp czeroE czeroI by auto
   1.218    show ?thesis using 0 1 2 unfolding ordIso_iff_ordLeq
   1.219 -    using r p cexp_mono[OF _ _ _ Cp] cexp_mono[OF _ _ _ Cr] by metis
   1.220 +    using r p cexp_mono[OF _ _ _ Cp] cexp_mono[OF _ _ _ Cr] by blast
   1.221  qed
   1.222  
   1.223  lemma cexp_cong1:
   1.224 @@ -575,7 +582,7 @@
   1.225  qed
   1.226  
   1.227  lemma cinfinite_cexp: "\<lbrakk>ctwo \<le>o q; Cinfinite r\<rbrakk> \<Longrightarrow> cinfinite (q ^c r)"
   1.228 -by (metis assms cinfinite_mono ordLeq_cexp2)
   1.229 +by (rule cinfinite_mono[OF ordLeq_cexp2]) simp_all
   1.230  
   1.231  lemma Cinfinite_cexp:
   1.232    "\<lbrakk>ctwo \<le>o q; Cinfinite r\<rbrakk> \<Longrightarrow> Cinfinite (q ^c r)"
   1.233 @@ -586,7 +593,7 @@
   1.234  by (intro Cfinite_ordLess_Cinfinite) (auto simp: cfinite_def card_of_Card_order)
   1.235  
   1.236  lemma ctwo_ordLess_Cinfinite: "Cinfinite r \<Longrightarrow> ctwo <o r"
   1.237 -by (metis ctwo_ordLess_natLeq natLeq_ordLeq_cinfinite ordLess_ordLeq_trans)
   1.238 +by (rule ordLess_ordLeq_trans[OF ctwo_ordLess_natLeq natLeq_ordLeq_cinfinite])
   1.239  
   1.240  lemma ctwo_ordLeq_Cinfinite:
   1.241    assumes "Cinfinite r"
   1.242 @@ -663,9 +670,10 @@
   1.243    case True thus ?thesis using t by (blast intro: cexp_mono1)
   1.244  next
   1.245    case False
   1.246 -  hence "ctwo \<le>o s" by (metis card_order_on_well_order_on ctwo_Cnotzero ordLeq_total s)
   1.247 -  hence "Cnotzero s" by (metis Cnotzero_mono ctwo_Cnotzero s)
   1.248 -  hence st: "Cnotzero (s *c t)" by (metis Cinfinite_cprod2 cinfinite_not_czero t)
   1.249 +  hence "ctwo \<le>o s" using ordLeq_total[of s ctwo] Card_order_ctwo s
   1.250 +    by (auto intro: card_order_on_well_order_on)
   1.251 +  hence "Cnotzero s" using Cnotzero_mono[OF ctwo_Cnotzero] s by blast
   1.252 +  hence st: "Cnotzero (s *c t)" by (intro Cinfinite_Cnotzero[OF Cinfinite_cprod2]) (auto simp: t)
   1.253    have "s ^c t \<le>o (ctwo ^c s) ^c t"
   1.254      using assms by (blast intro: cexp_mono1 ordLess_imp_ordLeq[OF ordLess_ctwo_cexp])
   1.255    also have "(ctwo ^c s) ^c t =o ctwo ^c (s *c t)"
     2.1 --- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Fri Feb 28 22:00:13 2014 +0100
     2.2 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Fri Feb 28 17:54:52 2014 +0100
     2.3 @@ -394,18 +394,13 @@
     2.4  qed
     2.5  
     2.6  lemma surj_imp_ordLeq:
     2.7 -assumes "B <= f ` A"
     2.8 -shows "|B| <=o |A|"
     2.9 +assumes "B \<subseteq> f ` A"
    2.10 +shows "|B| \<le>o |A|"
    2.11  proof-
    2.12    have "|B| <=o |f ` A|" using assms card_of_mono1 by auto
    2.13    thus ?thesis using card_of_image ordLeq_transitive by blast
    2.14  qed
    2.15  
    2.16 -lemma card_of_ordLeqI2:
    2.17 -assumes "B \<subseteq> f ` A"
    2.18 -shows "|B| \<le>o |A|"
    2.19 -using assms by (metis surj_imp_ordLeq)
    2.20 -
    2.21  lemma card_of_singl_ordLeq:
    2.22  assumes "A \<noteq> {}"
    2.23  shows "|{b}| \<le>o |A|"
    2.24 @@ -529,7 +524,7 @@
    2.25      }
    2.26      ultimately show ?thesis unfolding inj_on_def by auto
    2.27    qed
    2.28 -  thus ?thesis using card_of_ordLeq by metis
    2.29 +  thus ?thesis using card_of_ordLeq by blast
    2.30  qed
    2.31  
    2.32  corollary ordLeq_Plus_mono1:
    2.33 @@ -678,7 +673,7 @@
    2.34    "g = (\<lambda>(a,c::'c). (f a,c))" by blast
    2.35    have "inj_on g (A \<times> C) \<and> g ` (A \<times> C) \<le> (B \<times> C)"
    2.36    using 1 unfolding inj_on_def using g_def by auto
    2.37 -  thus ?thesis using card_of_ordLeq by metis
    2.38 +  thus ?thesis using card_of_ordLeq by blast
    2.39  qed
    2.40  
    2.41  corollary ordLeq_Times_mono1:
    2.42 @@ -706,11 +701,12 @@
    2.43    have "\<forall>i. i \<in> I \<longrightarrow> (\<exists>f. inj_on f (A i) \<and> f ` (A i) \<le> B i)"
    2.44    using assms by (auto simp add: card_of_ordLeq)
    2.45    with choice[of "\<lambda> i f. i \<in> I \<longrightarrow> inj_on f (A i) \<and> f ` (A i) \<le> B i"]
    2.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
    2.47 +  obtain F where 1: "\<forall>i \<in> I. inj_on (F i) (A i) \<and> (F i) ` (A i) \<le> B i"
    2.48 +    by atomize_elim (auto intro: bchoice)
    2.49    obtain g where g_def: "g = (\<lambda>(i,a::'b). (i,F i a))" by blast
    2.50    have "inj_on g (Sigma I A) \<and> g ` (Sigma I A) \<le> (Sigma I B)"
    2.51    using 1 unfolding inj_on_def using g_def by force
    2.52 -  thus ?thesis using card_of_ordLeq by metis
    2.53 +  thus ?thesis using card_of_ordLeq by blast
    2.54  qed
    2.55  
    2.56  corollary card_of_Sigma_Times:
    2.57 @@ -719,7 +715,7 @@
    2.58  
    2.59  lemma card_of_UNION_Sigma:
    2.60  "|\<Union>i \<in> I. A i| \<le>o |SIGMA i : I. A i|"
    2.61 -using Ex_inj_on_UNION_Sigma[of I A] card_of_ordLeq by metis
    2.62 +using Ex_inj_on_UNION_Sigma[of I A] card_of_ordLeq by blast
    2.63  
    2.64  lemma card_of_bool:
    2.65  assumes "a1 \<noteq> a2"
    2.66 @@ -745,8 +741,7 @@
    2.67         hence "?f False = a" by auto  thus ?thesis by blast
    2.68       qed
    2.69      }
    2.70 -    ultimately show ?thesis unfolding bij_betw_def inj_on_def
    2.71 -    by (metis (no_types) image_subsetI order_eq_iff subsetI)
    2.72 +    ultimately show ?thesis unfolding bij_betw_def inj_on_def by blast
    2.73    qed
    2.74    thus ?thesis using card_of_ordIso by blast
    2.75  qed
    2.76 @@ -758,7 +753,7 @@
    2.77  proof-
    2.78    have 1: "|UNIV::bool set| \<le>o |A|"
    2.79    using A2 card_of_mono1[of "{a1,a2}"] card_of_bool[of a1 a2]
    2.80 -        ordIso_ordLeq_trans[of "|UNIV::bool set|"] by metis
    2.81 +        ordIso_ordLeq_trans[of "|UNIV::bool set|"] by blast
    2.82    (*  *)
    2.83    have "|A <+> B| \<le>o |B <+> B|"
    2.84    using LEQ card_of_Plus_mono1 by blast
    2.85 @@ -789,11 +784,11 @@
    2.86     using assms by (auto simp add: card_of_Plus_Times_aux)
    2.87     hence ?thesis
    2.88     using card_of_Plus_commute card_of_Times_commute
    2.89 -         ordIso_ordLeq_trans ordLeq_ordIso_trans by metis
    2.90 +         ordIso_ordLeq_trans ordLeq_ordIso_trans by blast
    2.91    }
    2.92    ultimately show ?thesis
    2.93    using card_of_Well_order[of A] card_of_Well_order[of B]
    2.94 -        ordLeq_total[of "|A|"] by metis
    2.95 +        ordLeq_total[of "|A|"] by blast
    2.96  qed
    2.97  
    2.98  lemma card_of_ordLeq_finite:
    2.99 @@ -852,7 +847,7 @@
   2.100      let ?r' = "Restr r (underS r a)"
   2.101      assume Case2: "a \<in> Field r"
   2.102      hence 1: "under r a = underS r a \<union> {a} \<and> a \<notin> underS r a"
   2.103 -    using 0 Refl_under_underS underS_notIn by metis
   2.104 +    using 0 Refl_under_underS[of r a] underS_notIn[of a r] by blast
   2.105      have 2: "wo_rel.ofilter r (underS r a) \<and> underS r a < Field r"
   2.106      using 0 wo_rel.underS_ofilter * 1 Case2 by fast
   2.107      hence "?r' <o r" using 0 using ofilter_ordLess by blast
   2.108 @@ -951,7 +946,7 @@
   2.109      (*  *)
   2.110      have "\<not> finite (Field r)" using 1 unfolding phi_def by simp
   2.111      hence "\<not> finite ?B" using 8 3 card_of_ordIso_finite_Field[of r ?B] by blast
   2.112 -    hence "\<not> finite A1" using 9 finite_cartesian_product finite_subset by metis
   2.113 +    hence "\<not> finite A1" using 9 finite_cartesian_product finite_subset by blast
   2.114      moreover have temp4: "Field |A1| = A1 \<and> Well_order |A1| \<and> Card_order |A1|"
   2.115      using card_of_Card_order[of A1] card_of_Well_order[of A1]
   2.116      by (simp add: Field_card_of)
   2.117 @@ -1110,7 +1105,7 @@
   2.118      by (auto simp add: card_of_Plus_Times)
   2.119      moreover have "|A \<times> B| =o |A|"
   2.120      using assms * by (simp add: card_of_Times_infinite_simps)
   2.121 -    ultimately have "|A <+> B| \<le>o |A|" using ordLeq_ordIso_trans by metis
   2.122 +    ultimately have "|A <+> B| \<le>o |A|" using ordLeq_ordIso_trans by blast
   2.123      thus ?thesis using card_of_Plus1 ordIso_iff_ordLeq by blast
   2.124    qed
   2.125  qed
   2.126 @@ -1256,7 +1251,7 @@
   2.127  corollary finite_iff_ordLess_natLeq:
   2.128  "finite A = ( |A| <o natLeq)"
   2.129  using infinite_iff_natLeq_ordLeq not_ordLeq_iff_ordLess
   2.130 -      card_of_Well_order natLeq_Well_order by metis
   2.131 +      card_of_Well_order natLeq_Well_order by blast
   2.132  
   2.133  
   2.134  subsection {* The successor of a cardinal *}
   2.135 @@ -1394,7 +1389,7 @@
   2.136    then show "finite (Field (cardSuc |A| ))"
   2.137    proof (rule card_of_ordLeq_finite[OF card_of_mono2, rotated])
   2.138      show "cardSuc |A| \<le>o |Pow A|"
   2.139 -      by (metis cardSuc_ordLess_ordLeq card_of_Card_order card_of_Pow)
   2.140 +      by (rule iffD1[OF cardSuc_ordLess_ordLeq card_of_Pow]) (simp_all add: card_of_Card_order)
   2.141    qed
   2.142  qed
   2.143  
   2.144 @@ -1655,7 +1650,7 @@
   2.145    unfolding bij_betw_def inj_on_def proof safe
   2.146      fix h :: "'a \<Rightarrow> 'b" assume h: "h \<in> Func UNIV B"
   2.147      hence "\<forall> a. \<exists> b. h a = b" unfolding Func_def by auto
   2.148 -    then obtain f where f: "\<forall> a. h a = f a" by metis
   2.149 +    then obtain f where f: "\<forall> a. h a = f a" by blast
   2.150      hence "range f \<subseteq> B" using h unfolding Func_def by auto
   2.151      thus "h \<in> (\<lambda>f a. f a) ` {f. range f \<subseteq> B}" using f unfolding image_def by auto
   2.152    qed(unfold Func_def fun_eq_iff, auto)
     3.1 --- a/src/HOL/BNF_Comp.thy	Fri Feb 28 22:00:13 2014 +0100
     3.2 +++ b/src/HOL/BNF_Comp.thy	Fri Feb 28 17:54:52 2014 +0100
     3.3 @@ -90,26 +90,41 @@
     3.4  
     3.5  lemma type_copy_map_id0: "M = id \<Longrightarrow> Abs o M o Rep = id"
     3.6    using type_definition.Rep_inverse[OF type_copy] by auto
     3.7 +
     3.8  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)"
     3.9    using type_definition.Abs_inverse[OF type_copy UNIV_I] by auto
    3.10 +
    3.11  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)"
    3.12    using type_definition.Abs_inverse[OF type_copy UNIV_I] by (auto simp: o_def fun_eq_iff)
    3.13 +
    3.14  lemma type_copy_wit: "x \<in> (S o Rep) (Abs y) \<Longrightarrow> x \<in> S y"
    3.15    using type_definition.Abs_inverse[OF type_copy UNIV_I] by auto
    3.16 +
    3.17  lemma type_copy_vimage2p_Grp_Rep: "vimage2p f Rep (Grp (Collect P) h) =
    3.18      Grp (Collect (\<lambda>x. P (f x))) (Abs o h o f)"
    3.19    unfolding vimage2p_def Grp_def fun_eq_iff
    3.20    by (auto simp: type_definition.Abs_inverse[OF type_copy UNIV_I]
    3.21     type_definition.Rep_inverse[OF type_copy] dest: sym)
    3.22 +
    3.23  lemma type_copy_vimage2p_Grp_Abs:
    3.24    "\<And>h. vimage2p g Abs (Grp (Collect P) h) = Grp (Collect (\<lambda>x. P (g x))) (Rep o h o g)"
    3.25    unfolding vimage2p_def Grp_def fun_eq_iff
    3.26    by (auto simp: type_definition.Abs_inverse[OF type_copy UNIV_I]
    3.27     type_definition.Rep_inverse[OF type_copy] dest: sym)
    3.28 +
    3.29 +lemma type_copy_ex_RepI: "(\<exists>b. F b) = (\<exists>b. F (Rep b))"
    3.30 +proof safe
    3.31 +  fix b assume "F b"
    3.32 +  show "\<exists>b'. F (Rep b')"
    3.33 +  proof (rule exI)
    3.34 +    from `F b` show "F (Rep (Abs b))" using type_definition.Abs_inverse[OF type_copy] by auto
    3.35 +  qed
    3.36 +qed blast
    3.37 +
    3.38  lemma vimage2p_relcompp_converse:
    3.39    "vimage2p f g (R^--1 OO S) = (vimage2p Rep f R)^--1 OO vimage2p Rep g S"
    3.40    unfolding vimage2p_def relcompp.simps conversep.simps fun_eq_iff image_def
    3.41 -  by (metis surjD[OF type_definition.Rep_range[OF type_copy]])
    3.42 +  by (auto simp: type_copy_ex_RepI)
    3.43  
    3.44  end
    3.45  
     4.1 --- a/src/HOL/BNF_Constructions_on_Wellorders.thy	Fri Feb 28 22:00:13 2014 +0100
     4.2 +++ b/src/HOL/BNF_Constructions_on_Wellorders.thy	Fri Feb 28 17:54:52 2014 +0100
     4.3 @@ -793,7 +793,7 @@
     4.4    {assume "r' \<le>o r"
     4.5     then obtain h where "inj_on h (Field r') \<and> h ` (Field r') \<le> Field r"
     4.6     unfolding ordLeq_def using assms embed_inj_on embed_Field by blast
     4.7 -   hence False using finite_imageD finite_subset FIN INF by metis
     4.8 +   hence False using finite_imageD finite_subset FIN INF by blast
     4.9    }
    4.10    thus ?thesis using WELL WELL' ordLess_or_ordLeq by blast
    4.11  qed
    4.12 @@ -819,7 +819,7 @@
    4.13      hence "bij_betw f A A" unfolding bij_betw_def using FIN endo_inj_surj by blast
    4.14      thus "r =o r'" unfolding ordIso_def iso_def[abs_def] using 1 2 by auto
    4.15    qed
    4.16 -  ultimately show ?thesis using assms ordLeq_total ordIso_symmetric by metis
    4.17 +  ultimately show ?thesis using assms ordLeq_total ordIso_symmetric by blast
    4.18  qed
    4.19  
    4.20  subsection{* @{text "<o"} is well-founded *}
    4.21 @@ -987,7 +987,7 @@
    4.22    have "A \<noteq> {} \<and> A \<le> Field r"
    4.23    using A_def dir_image_Field[of r f] SUB NE by blast
    4.24    then obtain a where 1: "a \<in> A \<and> (\<forall>b \<in> A. (b,a) \<notin> r)"
    4.25 -  using WF unfolding wf_eq_minimal2 by metis
    4.26 +  using WF unfolding wf_eq_minimal2 by blast
    4.27    have "\<forall>b' \<in> A'. (b',f a) \<notin> dir_image r f"
    4.28    proof(clarify)
    4.29      fix b' assume *: "b' \<in> A'" and **: "(b',f a) \<in> dir_image r f"
    4.30 @@ -1597,7 +1597,7 @@
    4.31  proof
    4.32    assume L: ?L
    4.33    moreover {assume "A = {}" hence False using L Func_empty by auto}
    4.34 -  moreover {assume "B \<noteq> {}" hence False using L Func_non_emp by metis}
    4.35 +  moreover {assume "B \<noteq> {}" hence False using L Func_non_emp[of B A] by simp }
    4.36    ultimately show ?R by blast
    4.37  next
    4.38    assume R: ?R
    4.39 @@ -1624,7 +1624,8 @@
    4.40      fix h assume h: "h \<in> Func B2 B1"
    4.41      def j1 \<equiv> "inv_into A1 f1"
    4.42      have "\<forall> a2 \<in> f2 ` B2. \<exists> b2. b2 \<in> B2 \<and> f2 b2 = a2" by blast
    4.43 -    then obtain k where k: "\<forall> a2 \<in> f2 ` B2. k a2 \<in> B2 \<and> f2 (k a2) = a2" by metis
    4.44 +    then obtain k where k: "\<forall> a2 \<in> f2 ` B2. k a2 \<in> B2 \<and> f2 (k a2) = a2"
    4.45 +      by atomize_elim (rule bchoice)
    4.46      {fix b2 assume b2: "b2 \<in> B2"
    4.47       hence "f2 (k (f2 b2)) = f2 b2" using k A2(2) by auto
    4.48       moreover have "k (f2 b2) \<in> B2" using b2 A2(2) k by auto
     5.1 --- a/src/HOL/BNF_Def.thy	Fri Feb 28 22:00:13 2014 +0100
     5.2 +++ b/src/HOL/BNF_Def.thy	Fri Feb 28 17:54:52 2014 +0100
     5.3 @@ -116,7 +116,7 @@
     5.4  
     5.5  
     5.6  lemma predicate2_eqD: "A = B \<Longrightarrow> A a b \<longleftrightarrow> B a b"
     5.7 -by metis
     5.8 +by simp
     5.9  
    5.10  lemma case_sum_o_inj:
    5.11  "case_sum f g \<circ> Inl = f"
     6.1 --- a/src/HOL/BNF_FP_Base.thy	Fri Feb 28 22:00:13 2014 +0100
     6.2 +++ b/src/HOL/BNF_FP_Base.thy	Fri Feb 28 17:54:52 2014 +0100
     6.3 @@ -65,13 +65,16 @@
     6.4  by blast
     6.5  
     6.6  lemma type_copy_obj_one_point_absE:
     6.7 -  assumes "type_definition Rep Abs UNIV"
     6.8 -  shows "\<forall>x. s = Abs x \<longrightarrow> P \<Longrightarrow> P"
     6.9 -  using type_definition.Rep_inverse[OF assms] by metis
    6.10 +  assumes "type_definition Rep Abs UNIV" "\<forall>x. s = Abs x \<longrightarrow> P" shows P
    6.11 +  using type_definition.Rep_inverse[OF assms(1)]
    6.12 +  by (intro mp[OF spec[OF assms(2), of "Rep s"]]) simp
    6.13  
    6.14  lemma obj_sumE_f:
    6.15 -"\<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"
    6.16 -by (rule allI) (metis sumE)
    6.17 +  assumes "\<forall>x. s = f (Inl x) \<longrightarrow> P" "\<forall>x. s = f (Inr x) \<longrightarrow> P"
    6.18 +  shows "\<forall>x. s = f x \<longrightarrow> P"
    6.19 +proof
    6.20 +  fix x from assms show "s = f x \<longrightarrow> P" by (cases x) auto
    6.21 +qed
    6.22  
    6.23  lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
    6.24  by (cases s) auto
     7.1 --- a/src/HOL/BNF_LFP.thy	Fri Feb 28 22:00:13 2014 +0100
     7.2 +++ b/src/HOL/BNF_LFP.thy	Fri Feb 28 17:54:52 2014 +0100
     7.3 @@ -50,8 +50,16 @@
     7.4  lemma convol_expand_snd: "fst o f = g \<Longrightarrow>  <g, snd o f> = f"
     7.5  unfolding convol_def by auto
     7.6  
     7.7 -lemma convol_expand_snd': "(fst o f = g) \<Longrightarrow> (h = snd o f) \<longleftrightarrow> (<g, h> = f)"
     7.8 -  by (metis convol_expand_snd snd_convol)
     7.9 +lemma convol_expand_snd':
    7.10 +  assumes "(fst o f = g)"
    7.11 +  shows "h = snd o f \<longleftrightarrow> <g, h> = f"
    7.12 +proof -
    7.13 +  from assms have *: "<g, snd o f> = f" by (rule convol_expand_snd)
    7.14 +  then have "h = snd o f \<longleftrightarrow> h = snd o <g, snd o f>" by simp
    7.15 +  moreover have "\<dots> \<longleftrightarrow> h = snd o f" by (simp add: snd_convol)
    7.16 +  moreover have "\<dots> \<longleftrightarrow> <g, h> = f" by (subst (2) *[symmetric]) (auto simp: convol_def fun_eq_iff)
    7.17 +  ultimately show ?thesis by simp
    7.18 +qed
    7.19  
    7.20  definition inver where
    7.21    "inver g f A = (ALL a : A. g (f a) = a)"
    7.22 @@ -67,7 +75,11 @@
    7.23      using bchoice[of B ?phi] by blast
    7.24    hence gg: "ALL b : f ` A. g b : A \<and> f (g b) = b" using f by blast
    7.25    have gf: "inver g f A" unfolding inver_def
    7.26 -    by (metis (no_types) gg imageI[of _ A f] the_inv_into_f_f[OF inj_f])
    7.27 +  proof
    7.28 +    fix a assume "a \<in> A"
    7.29 +    then show "g (f a) = a" using the_inv_into_f_f[OF inj_f, of "g (f a)"]
    7.30 +      the_inv_into_f_f[OF inj_f, of a] gg imageI[of a A f] by auto
    7.31 +  qed
    7.32    moreover have "g ` B \<le> A \<and> inver f g B" using g unfolding inver_def by blast
    7.33    moreover have "A \<le> g ` B"
    7.34    proof safe
    7.35 @@ -224,8 +236,13 @@
    7.36  by (rule assms)
    7.37  
    7.38  lemma nchotomy_relcomppE:
    7.39 -  "\<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"
    7.40 -  by (metis relcompp.cases)
    7.41 +  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"
    7.42 +  shows P
    7.43 +proof (rule relcompp.cases[OF assms(2)], hypsubst)
    7.44 +  fix b assume "r a b" "s b c"
    7.45 +  moreover from assms(1) obtain b' where "b = f b'" by blast
    7.46 +  ultimately show P by (blast intro: assms(3))
    7.47 +qed
    7.48  
    7.49  lemma vimage2p_fun_rel: "fun_rel (vimage2p f g R) R f g"
    7.50    unfolding fun_rel_def vimage2p_def by auto
     8.1 --- a/src/HOL/BNF_Wellorder_Embedding.thy	Fri Feb 28 22:00:13 2014 +0100
     8.2 +++ b/src/HOL/BNF_Wellorder_Embedding.thy	Fri Feb 28 17:54:52 2014 +0100
     8.3 @@ -305,8 +305,7 @@
     8.4    (* Main proof *)
     8.5    show "bij_betw f (under r a) (under r' (f a))"
     8.6    proof(unfold bij_betw_def, auto)
     8.7 -    show  "inj_on f (under r a)"
     8.8 -    using * by (metis (no_types) under_Field subset_inj_on)
     8.9 +    show  "inj_on f (under r a)" by (rule subset_inj_on[OF * under_Field])
    8.10    next
    8.11      fix b assume "b \<in> under r a"
    8.12      thus "f b \<in> under r' (f a)"
    8.13 @@ -1035,8 +1034,7 @@
    8.14    {fix a assume ***: "a \<in> Field r"
    8.15     have "bij_betw f (under r a) (under r' (f a))"
    8.16     proof(unfold bij_betw_def, auto)
    8.17 -     show "inj_on f (under r a)"
    8.18 -     using 1 2 by (metis subset_inj_on)
    8.19 +     show "inj_on f (under r a)" using 1 2 subset_inj_on by blast
    8.20     next
    8.21       fix b assume "b \<in> under r a"
    8.22       hence "a \<in> Field r \<and> b \<in> Field r \<and> (b,a) \<in> r"
     9.1 --- a/src/HOL/Basic_BNFs.thy	Fri Feb 28 22:00:13 2014 +0100
     9.2 +++ b/src/HOL/Basic_BNFs.thy	Fri Feb 28 17:54:52 2014 +0100
     9.3 @@ -158,11 +158,11 @@
     9.4  next
     9.5    fix x
     9.6    show "|{fst x}| \<le>o natLeq"
     9.7 -    by (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq finite.emptyI finite_insert)
     9.8 +    by (rule ordLess_imp_ordLeq) (simp add: finite_iff_ordLess_natLeq[symmetric])
     9.9  next
    9.10    fix x
    9.11    show "|{snd x}| \<le>o natLeq"
    9.12 -    by (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq finite.emptyI finite_insert)
    9.13 +    by (rule ordLess_imp_ordLeq) (simp add: finite_iff_ordLess_natLeq[symmetric])
    9.14  next
    9.15    fix R1 R2 S1 S2
    9.16    show "prod_rel R1 R2 OO prod_rel S1 S2 \<le> prod_rel (R1 OO S1) (R2 OO S2)" by auto
    9.17 @@ -215,8 +215,14 @@
    9.18    show "fun_rel op = R =
    9.19          (Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> fst))\<inverse>\<inverse> OO
    9.20           Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> snd)"
    9.21 -  unfolding fun_rel_def Grp_def fun_eq_iff relcompp.simps conversep.simps  subset_iff image_iff
    9.22 -  by auto (force, metis (no_types) pair_collapse)
    9.23 +  unfolding fun_rel_def Grp_def fun_eq_iff relcompp.simps conversep.simps subset_iff image_iff
    9.24 +    comp_apply mem_Collect_eq split_beta bex_UNIV
    9.25 +  proof (safe, unfold fun_eq_iff[symmetric])
    9.26 +    fix x xa a b c xb y aa ba
    9.27 +    assume *: "x = a" "xa = c" "a = ba" "b = aa" "c = (\<lambda>x. snd (b x))" "ba = (\<lambda>x. fst (aa x))" and
    9.28 +       **: "\<forall>t. (\<exists>x. t = aa x) \<longrightarrow> R (fst t) (snd t)"
    9.29 +    show "R (x y) (xa y)" unfolding * by (rule mp[OF spec[OF **]]) blast
    9.30 +  qed force
    9.31  qed
    9.32  
    9.33  end
    10.1 --- a/src/HOL/Cardinals/Wellorder_Extension.thy	Fri Feb 28 22:00:13 2014 +0100
    10.2 +++ b/src/HOL/Cardinals/Wellorder_Extension.thy	Fri Feb 28 17:54:52 2014 +0100
    10.3 @@ -5,7 +5,7 @@
    10.4  header {* Extending Well-founded Relations to Wellorders *}
    10.5  
    10.6  theory Wellorder_Extension
    10.7 -imports Zorn Order_Union
    10.8 +imports Main Order_Union
    10.9  begin
   10.10  
   10.11  subsection {* Extending Well-founded Relations to Wellorders *}
    11.1 --- a/src/HOL/Hilbert_Choice.thy	Fri Feb 28 22:00:13 2014 +0100
    11.2 +++ b/src/HOL/Hilbert_Choice.thy	Fri Feb 28 17:54:52 2014 +0100
    11.3 @@ -6,7 +6,7 @@
    11.4  header {* Hilbert's Epsilon-Operator and the Axiom of Choice *}
    11.5  
    11.6  theory Hilbert_Choice
    11.7 -imports Nat Wellfounded Metis
    11.8 +imports Nat Wellfounded
    11.9  keywords "specification" "ax_specification" :: thy_goal
   11.10  begin
   11.11  
   11.12 @@ -292,12 +292,13 @@
   11.13    def Sseq \<equiv> "rec_nat S (\<lambda>n T. T - {SOME e. e \<in> T})"
   11.14    def pick \<equiv> "\<lambda>n. (SOME e. e \<in> Sseq n)"
   11.15    { fix n have "Sseq n \<subseteq> S" "\<not> finite (Sseq n)" by (induct n) (auto simp add: Sseq_def inf) }
   11.16 -  moreover then have *: "\<And>n. pick n \<in> Sseq n" by (metis someI_ex pick_def ex_in_conv finite.simps)
   11.17 +  moreover then have *: "\<And>n. pick n \<in> Sseq n"
   11.18 +    unfolding pick_def by (subst (asm) finite.simps) (auto simp add: ex_in_conv intro: someI_ex)
   11.19    ultimately have "range pick \<subseteq> S" by auto
   11.20    moreover
   11.21    { fix n m                 
   11.22      have "pick n \<notin> Sseq (n + Suc m)" by (induct m) (auto simp add: Sseq_def pick_def)
   11.23 -    hence "pick n \<noteq> pick (n + Suc m)" by (metis *)
   11.24 +    with * have "pick n \<noteq> pick (n + Suc m)" by auto
   11.25    }
   11.26    then have "inj pick" by (intro linorder_injI) (auto simp add: less_iff_Suc_add)
   11.27    ultimately show ?thesis by blast
   11.28 @@ -305,7 +306,7 @@
   11.29  
   11.30  lemma infinite_iff_countable_subset: "\<not> finite S \<longleftrightarrow> (\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S)"
   11.31    -- {* Courtesy of Stephan Merz *}
   11.32 -  by (metis finite_imageD finite_subset infinite_UNIV_char_0 infinite_countable_subset)
   11.33 +  using finite_imageD finite_subset infinite_UNIV_char_0 infinite_countable_subset by auto
   11.34  
   11.35  lemma image_inv_into_cancel:
   11.36    assumes SURJ: "f`A=A'" and SUB: "B' \<le> A'"
   11.37 @@ -706,9 +707,13 @@
   11.38      then have "\<And>n. f n < f (Suc n)"
   11.39        using  `mono f` by (auto simp: le_less mono_iff_le_Suc)
   11.40      with lift_Suc_mono_less_iff[of f]
   11.41 -    have "\<And>n m. n < m \<Longrightarrow> f n < f m" by auto
   11.42 -    then have "inj f"
   11.43 -      by (auto simp: inj_on_def) (metis linorder_less_linear order_less_imp_not_eq)
   11.44 +    have *: "\<And>n m. n < m \<Longrightarrow> f n < f m" by auto
   11.45 +    have "inj f"
   11.46 +    proof (intro injI)
   11.47 +      fix x y
   11.48 +      assume "f x = f y"
   11.49 +      then show "x = y" by (cases x y rule: linorder_cases) (auto dest: *)
   11.50 +    qed
   11.51      with `finite (range f)` have "finite (UNIV::nat set)"
   11.52        by (rule finite_imageD)
   11.53      then show False by simp
    12.1 --- a/src/HOL/Library/Multiset.thy	Fri Feb 28 22:00:13 2014 +0100
    12.2 +++ b/src/HOL/Library/Multiset.thy	Fri Feb 28 17:54:52 2014 +0100
    12.3 @@ -2314,7 +2314,7 @@
    12.4  
    12.5  lemma card_of_set_of:
    12.6  "(card_of {M. set_of M \<subseteq> A}, card_of {as. set as \<subseteq> A}) \<in> ordLeq"
    12.7 -apply(rule card_of_ordLeqI2[of _ multiset_of]) using multiset_of_surj by auto
    12.8 +apply(rule surj_imp_ordLeq[of _ multiset_of]) using multiset_of_surj by auto
    12.9  
   12.10  lemma nat_sum_induct:
   12.11  assumes "\<And>n1 n2. (\<And> m1 m2. m1 + m2 < n1 + n2 \<Longrightarrow> phi m1 m2) \<Longrightarrow> phi n1 n2"
    13.1 --- a/src/HOL/List.thy	Fri Feb 28 22:00:13 2014 +0100
    13.2 +++ b/src/HOL/List.thy	Fri Feb 28 17:54:52 2014 +0100
    13.3 @@ -3117,7 +3117,7 @@
    13.4  proof(induct i j rule:upto.induct)
    13.5    case (1 i j)
    13.6    from this show ?case
    13.7 -    unfolding upto.simps[of i j] simp_from_to[of i j] by auto
    13.8 +    unfolding upto.simps[of i j] by auto
    13.9  qed
   13.10  
   13.11  text{* Tail recursive version for code generation: *}
    14.1 --- a/src/HOL/Power.thy	Fri Feb 28 22:00:13 2014 +0100
    14.2 +++ b/src/HOL/Power.thy	Fri Feb 28 17:54:52 2014 +0100
    14.3 @@ -613,7 +613,7 @@
    14.4  lemma self_le_power:
    14.5    fixes x::"'a::linordered_semidom" 
    14.6    shows "1 \<le> x \<Longrightarrow> 0 < n \<Longrightarrow> x \<le> x ^ n"
    14.7 -  by (metis gr_implies_not0 le_eq_less_or_eq less_one nat_le_linear power_increasing power_one_right)
    14.8 +  using power_increasing[of 1 n x] power_one_right[of x] by auto
    14.9  
   14.10  lemma power_eq_if: "p ^ m = (if m=0 then 1 else p * (p ^ (m - 1)))"
   14.11    unfolding One_nat_def by (cases m) simp_all
    15.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Feb 28 22:00:13 2014 +0100
    15.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Feb 28 17:54:52 2014 +0100
    15.3 @@ -232,7 +232,8 @@
    15.4  fun co_rec_of [_, r] = r;
    15.5  
    15.6  fun time ctxt timer msg = (if Config.get ctxt bnf_timing
    15.7 -  then warning (msg ^ ": " ^ ATP_Util.string_of_time (Timer.checkRealTimer timer))
    15.8 +  then warning (msg ^ ": " ^ string_of_int (Time.toMilliseconds (Timer.checkRealTimer timer)) ^
    15.9 +    "ms")
   15.10    else (); Timer.startRealTimer ());
   15.11  
   15.12  val preN = "pre_"
    16.1 --- a/src/HOL/Transfer.thy	Fri Feb 28 22:00:13 2014 +0100
    16.2 +++ b/src/HOL/Transfer.thy	Fri Feb 28 17:54:52 2014 +0100
    16.3 @@ -6,7 +6,7 @@
    16.4  header {* Generic theorem transfer using relations *}
    16.5  
    16.6  theory Transfer
    16.7 -imports Hilbert_Choice Basic_BNFs
    16.8 +imports Hilbert_Choice Basic_BNFs Metis
    16.9  begin
   16.10  
   16.11  subsection {* Relator for function space *}
    17.1 --- a/src/HOL/Zorn.thy	Fri Feb 28 22:00:13 2014 +0100
    17.2 +++ b/src/HOL/Zorn.thy	Fri Feb 28 17:54:52 2014 +0100
    17.3 @@ -70,7 +70,7 @@
    17.4  
    17.5  lemma suc_not_equals:
    17.6    "chain C \<Longrightarrow> \<not> maxchain C \<Longrightarrow> suc C \<noteq> C"
    17.7 -  by (auto simp: suc_def) (metis (no_types) less_irrefl not_maxchain_Some)
    17.8 +  using not_maxchain_Some by (auto simp: suc_def)
    17.9  
   17.10  lemma subset_suc:
   17.11    assumes "X \<subseteq> Y" shows "X \<subseteq> suc Y"
   17.12 @@ -257,7 +257,7 @@
   17.13    shows "chain X"
   17.14  using assms
   17.15  proof (induct)
   17.16 -  case (suc X) then show ?case by (simp add: suc_def) (metis (no_types) not_maxchain_Some)
   17.17 +  case (suc X) then show ?case using not_maxchain_Some by (simp add: suc_def)
   17.18  next
   17.19    case (Union X)
   17.20    then have "\<Union>X \<subseteq> A" by (auto dest: suc_Union_closed_in_carrier)
   17.21 @@ -377,7 +377,7 @@
   17.22          using `subset.maxchain A M` by (auto simp: subset.maxchain_def)
   17.23      qed
   17.24    qed
   17.25 -  ultimately show ?thesis by metis
   17.26 +  ultimately show ?thesis by blast
   17.27  qed
   17.28  
   17.29  text{*Alternative version of Zorn's lemma for the subset relation.*}
   17.30 @@ -440,8 +440,7 @@
   17.31  lemma Chains_alt_def:
   17.32    assumes "refl r"
   17.33    shows "Chains r = {C. pred_on.chain UNIV (\<lambda>x y. (x, y) \<in> r) C}"
   17.34 -  using assms
   17.35 -  by (metis Chains_subset Chains_subset' subset_antisym)
   17.36 +  using assms Chains_subset Chains_subset' by blast
   17.37  
   17.38  lemma Zorn_Lemma:
   17.39    "\<forall>C\<in>chains A. \<Union>C \<in> A \<Longrightarrow> \<exists>M\<in>A. \<forall>X\<in>A. M \<subseteq> X \<longrightarrow> X = M"
   17.40 @@ -534,16 +533,28 @@
   17.41    by (auto simp: init_seg_of_def Ball_def Chains_def) blast
   17.42  
   17.43  lemma chain_subset_trans_Union:
   17.44 -  "chain\<^sub>\<subseteq> R \<Longrightarrow> \<forall>r\<in>R. trans r \<Longrightarrow> trans (\<Union>R)"
   17.45 -apply (auto simp add: chain_subset_def)
   17.46 -apply (simp (no_asm_use) add: trans_def)
   17.47 -by (metis subsetD)
   17.48 +  assumes "chain\<^sub>\<subseteq> R" "\<forall>r\<in>R. trans r"
   17.49 +  shows "trans (\<Union>R)"
   17.50 +proof (intro transI, elim UnionE)
   17.51 +  fix  S1 S2 :: "'a rel" and x y z :: 'a
   17.52 +  assume "S1 \<in> R" "S2 \<in> R"
   17.53 +  with assms(1) have "S1 \<subseteq> S2 \<or> S2 \<subseteq> S1" unfolding chain_subset_def by blast
   17.54 +  moreover assume "(x, y) \<in> S1" "(y, z) \<in> S2"
   17.55 +  ultimately have "((x, y) \<in> S1 \<and> (y, z) \<in> S1) \<or> ((x, y) \<in> S2 \<and> (y, z) \<in> S2)" by blast
   17.56 +  with `S1 \<in> R` `S2 \<in> R` assms(2) show "(x, z) \<in> \<Union>R" by (auto elim: transE)
   17.57 +qed
   17.58  
   17.59  lemma chain_subset_antisym_Union:
   17.60 -  "chain\<^sub>\<subseteq> R \<Longrightarrow> \<forall>r\<in>R. antisym r \<Longrightarrow> antisym (\<Union>R)"
   17.61 -unfolding chain_subset_def antisym_def
   17.62 -apply simp
   17.63 -by (metis (no_types) subsetD)
   17.64 +  assumes "chain\<^sub>\<subseteq> R" "\<forall>r\<in>R. antisym r"
   17.65 +  shows "antisym (\<Union>R)"
   17.66 +proof (intro antisymI, elim UnionE)
   17.67 +  fix  S1 S2 :: "'a rel" and x y :: 'a
   17.68 +  assume "S1 \<in> R" "S2 \<in> R"
   17.69 +  with assms(1) have "S1 \<subseteq> S2 \<or> S2 \<subseteq> S1" unfolding chain_subset_def by blast
   17.70 +  moreover assume "(x, y) \<in> S1" "(y, x) \<in> S2"
   17.71 +  ultimately have "((x, y) \<in> S1 \<and> (y, x) \<in> S1) \<or> ((x, y) \<in> S2 \<and> (y, x) \<in> S2)" by blast
   17.72 +  with `S1 \<in> R` `S2 \<in> R` assms(2) show "x = y" unfolding antisym_def by auto
   17.73 +qed
   17.74  
   17.75  lemma chain_subset_Total_Union:
   17.76    assumes "chain\<^sub>\<subseteq> R" and "\<forall>r\<in>R. Total r"
   17.77 @@ -554,12 +565,12 @@
   17.78      by (auto simp add: chain_subset_def)
   17.79    thus "(\<exists>r\<in>R. (a, b) \<in> r) \<or> (\<exists>r\<in>R. (b, a) \<in> r)"
   17.80    proof
   17.81 -    assume "r \<subseteq> s" hence "(a, b) \<in> s \<or> (b, a) \<in> s" using assms(2) A
   17.82 -      by (simp add: total_on_def) (metis (no_types) mono_Field subsetD)
   17.83 +    assume "r \<subseteq> s" hence "(a, b) \<in> s \<or> (b, a) \<in> s" using assms(2) A mono_Field[of r s]
   17.84 +      by (auto simp add: total_on_def)
   17.85      thus ?thesis using `s \<in> R` by blast
   17.86    next
   17.87 -    assume "s \<subseteq> r" hence "(a, b) \<in> r \<or> (b, a) \<in> r" using assms(2) A
   17.88 -      by (simp add: total_on_def) (metis (no_types) mono_Field subsetD)
   17.89 +    assume "s \<subseteq> r" hence "(a, b) \<in> r \<or> (b, a) \<in> r" using assms(2) A mono_Field[of s r]
   17.90 +      by (fastforce simp add: total_on_def)
   17.91      thus ?thesis using `r \<in> R` by blast
   17.92    qed
   17.93  qed
   17.94 @@ -633,8 +644,8 @@
   17.95      moreover have "\<forall>r \<in> R. r initial_segment_of \<Union>R" using Ris
   17.96        by(simp add: Chains_init_seg_of_Union)
   17.97      ultimately have "\<Union>R \<in> ?WO \<and> (\<forall>r\<in>R. (r, \<Union>R) \<in> I)"
   17.98 -      using mono_Chains [OF I_init] and `R \<in> Chains I`
   17.99 -      by (simp (no_asm) add: I_def del: Field_Union) (metis Chains_wo)
  17.100 +      using mono_Chains [OF I_init] Chains_wo[of R] and `R \<in> Chains I`
  17.101 +      unfolding I_def by blast
  17.102    }
  17.103    hence 1: "\<forall>R \<in> Chains I. \<exists>u\<in>Field I. \<forall>r\<in>R. (r, u) \<in> I" by (subst FI) blast
  17.104  --{*Zorn's Lemma yields a maximal well-order m:*}
  17.105 @@ -671,8 +682,8 @@
  17.106      moreover have "Total ?m" using `Total m` and Fm by (auto simp: total_on_def)
  17.107      moreover have "wf (?m - Id)"
  17.108      proof -
  17.109 -      have "wf ?s" using `x \<notin> Field m`
  17.110 -        by (auto simp add: wf_eq_minimal Field_def) metis
  17.111 +      have "wf ?s" using `x \<notin> Field m` unfolding wf_eq_minimal Field_def
  17.112 +        by (auto simp: Bex_def)
  17.113        thus ?thesis using `wf (m - Id)` and `x \<notin> Field m`
  17.114          wf_subset [OF `wf ?s` Diff_subset]
  17.115          unfolding Un_Diff Field_def by (auto intro: wf_Un)