--- 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:
--- 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
--- 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
--- 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
--- 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"
--- 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"
--- 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
--- 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)"
--- 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