--- 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)"
--- 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)
--- 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
--- 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
--- 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"
--- 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
--- 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
--- 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"
--- 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
--- 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 *}
--- 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
--- 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"
--- 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: *}
--- 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
--- 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_"
--- 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 *}
--- 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)