--- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy Wed Apr 24 16:21:23 2013 +0200
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy Wed Apr 24 16:43:19 2013 +0200
@@ -86,7 +86,7 @@
proof-
let ?Y = "{y. EX x. (x,y) : R}" let ?X = "{x. EX y. (x,y) : R}"
let ?f = "% y. SOME x. (x,y) : R"
- have "?f ` ?Y <= ?X" using someI by force (* FIXME: takes a bit long *)
+ have "?f ` ?Y <= ?X" by (auto dest: someI)
moreover have "inj_on ?f ?Y"
unfolding inj_on_def proof(auto)
fix y1 x1 y2 x2
@@ -603,7 +603,7 @@
shows "|{a} Un A| <o |B|"
proof-
have "|{a}| <o |B|" using assms by auto
- thus ?thesis using assms card_of_Un_ordLess_infinite[of B] by fastforce
+ thus ?thesis using assms card_of_Un_ordLess_infinite[of B] by blast
qed
lemma card_of_Un_singl_ordLess_infinite:
@@ -612,7 +612,7 @@
using assms card_of_Un_singl_ordLess_infinite1[of B A]
proof(auto)
assume "|insert a A| <o |B|"
- moreover have "|A| <=o |insert a A|" using card_of_mono1[of A] by blast
+ moreover have "|A| <=o |insert a A|" using card_of_mono1[of A "insert a A"] by blast
ultimately show "|A| <o |B|" using ordLeq_ordLess_trans by blast
qed
--- a/src/HOL/Cardinals/Cardinal_Order_Relation_Base.thy Wed Apr 24 16:21:23 2013 +0200
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation_Base.thy Wed Apr 24 16:43:19 2013 +0200
@@ -580,7 +580,7 @@
qed
qed
hence "bij_betw f ((A <+> B) <+> C) (A <+> B <+> C)"
- unfolding bij_betw_def inj_on_def f_def by auto
+ unfolding bij_betw_def inj_on_def f_def by force
thus ?thesis using card_of_ordIso by blast
qed
@@ -836,7 +836,7 @@
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 fastforce
+ 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 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
@@ -1766,9 +1766,9 @@
proof
assume "natLeq_on m \<le>o natLeq_on n"
then obtain f where "inj_on f {0..<m} \<and> f ` {0..<m} \<le> {0..<n}"
- using Field_natLeq_on[of m] Field_natLeq_on[of n]
- unfolding ordLeq_def using embed_inj_on[of "natLeq_on m" "natLeq_on n"]
- embed_Field[of "natLeq_on m" "natLeq_on n"] using natLeq_on_Well_order[of m] by fastforce
+ unfolding ordLeq_def using
+ embed_inj_on[OF natLeq_on_Well_order[of m], of "natLeq_on n", unfolded Field_natLeq_on]
+ embed_Field[OF natLeq_on_Well_order[of m], of "natLeq_on n", unfolded Field_natLeq_on] by blast
thus "m \<le> n" using atLeastLessThan_less_eq2 by blast
next
assume "m \<le> n"
@@ -2238,7 +2238,7 @@
proof (cases "(a,b) \<in> A <*> B")
case False
thus ?thesis using assms unfolding Func_def
- apply(cases "f1 (a,b)") apply(cases "f2 (a,b)", fastforce, fastforce)
+ apply(cases "f1 (a,b)") apply(cases "f2 (a,b)", simp, blast)
apply(cases "f2 (a,b)") by auto
next
case True hence a: "a \<in> A" and b: "b \<in> B" by auto
@@ -2406,7 +2406,7 @@
qed
moreover have "g \<in> Func A2 A1" unfolding g_def apply(rule Func_map[OF h])
using inv_into_into j2A2 B1 A2 inv_into_into
- unfolding j1_def image_def by(force, force)
+ unfolding j1_def image_def by fast+
ultimately show "h \<in> Func_map B2 f1 f2 ` Func A2 A1"
unfolding Func_map_def[abs_def] unfolding image_def by auto
qed(insert B1 Func_map[OF _ _ A2(2)], auto)
--- a/src/HOL/Cardinals/Constructions_on_Wellorders.thy Wed Apr 24 16:21:23 2013 +0200
+++ b/src/HOL/Cardinals/Constructions_on_Wellorders.thy Wed Apr 24 16:43:19 2013 +0200
@@ -44,7 +44,7 @@
lemma wf_Restr:
"wf r \<Longrightarrow> wf(Restr r A)"
-using wf_subset Restr_subset by blast
+using Restr_subset by (elim wf_subset) simp
lemma Restr_incr1:
"A \<le> B \<Longrightarrow> Restr r A \<le> Restr r B"
@@ -384,7 +384,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'"
@@ -412,7 +412,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'"
@@ -450,15 +450,14 @@
thus ?thesis by(auto simp add: Osum_def)
qed
-
lemma wf_Int_Times:
assumes "A Int B = {}"
shows "wf(A \<times> B)"
-proof(unfold wf_def, auto)
+proof(unfold wf_def mem_Sigma_iff, intro impI allI)
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)
+ ultimately show "P x" using * by (case_tac "x \<in> B") blast+
qed
lemma Osum_minus_Id1:
--- a/src/HOL/Cardinals/Constructions_on_Wellorders_Base.thy Wed Apr 24 16:21:23 2013 +0200
+++ b/src/HOL/Cardinals/Constructions_on_Wellorders_Base.thy Wed Apr 24 16:43:19 2013 +0200
@@ -879,7 +879,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 blast
+ hence False using finite_imageD finite_subset FIN INF by metis
}
thus ?thesis using WELL WELL' ordLess_or_ordLeq by blast
qed
@@ -1092,7 +1092,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 blast
+ using WF unfolding wf_eq_minimal2 by metis
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"
@@ -1290,7 +1290,7 @@
}
moreover
{assume Case42: "(wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \<in> r - Id"
- hence ?thesis using Case4 0 unfolding bsqr_def by auto
+ hence ?thesis using Case4 0 unfolding bsqr_def by force
}
moreover
{assume Case43: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> (b1,c1) \<in> r - Id"
--- a/src/HOL/Cardinals/Fun_More.thy Wed Apr 24 16:21:23 2013 +0200
+++ b/src/HOL/Cardinals/Fun_More.thy Wed Apr 24 16:43:19 2013 +0200
@@ -73,7 +73,7 @@
unfolding inj_on_def by auto
next
fix y assume ****: "y \<in> Y"
- with *** obtain x where "x \<in> X \<and> f x = f y" by force
+ with *** obtain x where "x \<in> X \<and> f x = f y" by atomize_elim force
with **** * ** assms show "y \<in> X"
unfolding inj_on_def by auto
qed
--- a/src/HOL/Cardinals/Fun_More_Base.thy Wed Apr 24 16:21:23 2013 +0200
+++ b/src/HOL/Cardinals/Fun_More_Base.thy Wed Apr 24 16:43:19 2013 +0200
@@ -32,7 +32,7 @@
IM1: "f ` A \<le> A'" and IM2: "f' ` A' \<le> A"
shows "bij_betw f A A'"
using assms
-proof(unfold bij_betw_def inj_on_def, auto)
+proof(unfold bij_betw_def inj_on_def, safe)
fix a b assume *: "a \<in> A" "b \<in> A" and **: "f a = f b"
have "a = f'(f a) \<and> b = f'(f b)" using * LEFT by simp
with ** show "a = b" by simp
--- a/src/HOL/Cardinals/Order_Relation_More.thy Wed Apr 24 16:21:23 2013 +0200
+++ b/src/HOL/Cardinals/Order_Relation_More.thy Wed Apr 24 16:43:19 2013 +0200
@@ -94,7 +94,7 @@
proof(unfold underS_def above_def, auto)
assume "a \<in> Field r" "(a, a) \<notin> r"
with LIN IN order_on_defs[of _ r] refl_on_def[of _ r]
- show False by auto
+ show False by metis
next
fix b assume "b \<in> Field r" "(a, b) \<notin> r"
with LIN IN order_on_defs[of "Field r" r] total_on_def[of "Field r" r]
--- a/src/HOL/Cardinals/Order_Relation_More_Base.thy Wed Apr 24 16:21:23 2013 +0200
+++ b/src/HOL/Cardinals/Order_Relation_More_Base.thy Wed Apr 24 16:43:19 2013 +0200
@@ -63,7 +63,7 @@
(* *)
fix a assume *: "a \<in> Field r"
obtain d where 2: "d \<in> Field r" and 3: "d \<noteq> a"
- using * 1 by blast
+ using * 1 by auto
hence "(a,d) \<in> r \<or> (d,a) \<in> r" using * TOT
by (simp add: total_on_def)
thus "a \<in> Field(r - Id)" using 3 unfolding Field_def by blast
--- a/src/HOL/Cardinals/Wellorder_Embedding_Base.thy Wed Apr 24 16:21:23 2013 +0200
+++ b/src/HOL/Cardinals/Wellorder_Embedding_Base.thy Wed Apr 24 16:43:19 2013 +0200
@@ -683,7 +683,7 @@
have "wo_rel.ofilter r (rel.underS r ?a)"
using Well by (auto simp add: wo_rel.underS_ofilter)
ultimately
- have "False \<notin> g`(rel.under r b)" using 3 Well by (auto simp add: wo_rel.ofilter_def)
+ have "False \<notin> g`(rel.under r b)" using 3 Well by (subst (asm) wo_rel.ofilter_def) fast+
moreover have "b \<in> Field r"
unfolding Field_def using as by (auto simp add: rel.underS_def)
ultimately
--- a/src/HOL/Cardinals/Wellorder_Relation.thy Wed Apr 24 16:21:23 2013 +0200
+++ b/src/HOL/Cardinals/Wellorder_Relation.thy Wed Apr 24 16:43:19 2013 +0200
@@ -11,16 +11,18 @@
imports Wellorder_Relation_Base Wellfounded_More
begin
+context wo_rel
+begin
subsection {* Auxiliaries *}
-lemma (in wo_rel) PREORD: "Preorder r"
+lemma PREORD: "Preorder r"
using WELL order_on_defs[of _ r] by auto
-lemma (in wo_rel) PARORD: "Partial_order r"
+lemma PARORD: "Partial_order r"
using WELL order_on_defs[of _ r] by auto
-lemma (in wo_rel) cases_Total2:
+lemma cases_Total2:
"\<And> phi a b. \<lbrakk>{a,b} \<le> Field r; ((a,b) \<in> r - Id \<Longrightarrow> phi a b);
((b,a) \<in> r - Id \<Longrightarrow> phi a b); (a = b \<Longrightarrow> phi a b)\<rbrakk>
\<Longrightarrow> phi a b"
@@ -29,7 +31,7 @@
subsection {* Well-founded induction and recursion adapted to non-strict well-order relations *}
-lemma (in wo_rel) worec_unique_fixpoint:
+lemma worec_unique_fixpoint:
assumes ADM: "adm_wo H" and fp: "f = H f"
shows "f = worec H"
proof-
@@ -44,7 +46,7 @@
subsubsection {* Properties of max2 *}
-lemma (in wo_rel) max2_iff:
+lemma max2_iff:
assumes "a \<in> Field r" and "b \<in> Field r"
shows "((max2 a b, c) \<in> r) = ((a,c) \<in> r \<and> (b,c) \<in> r)"
proof
@@ -60,7 +62,7 @@
subsubsection{* Properties of minim *}
-lemma (in wo_rel) minim_Under:
+lemma minim_Under:
"\<lbrakk>B \<le> Field r; B \<noteq> {}\<rbrakk> \<Longrightarrow> minim B \<in> Under B"
by(auto simp add: Under_def
minim_in
@@ -74,12 +76,12 @@
ofilter_Un
)
-lemma (in wo_rel) equals_minim_Under:
+lemma equals_minim_Under:
"\<lbrakk>B \<le> Field r; a \<in> B; a \<in> Under B\<rbrakk>
\<Longrightarrow> a = minim B"
by(auto simp add: Under_def equals_minim)
-lemma (in wo_rel) minim_iff_In_Under:
+lemma minim_iff_In_Under:
assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}"
shows "(a = minim B) = (a \<in> B \<and> a \<in> Under B)"
proof
@@ -92,7 +94,7 @@
using assms equals_minim_Under by simp
qed
-lemma (in wo_rel) minim_Under_under:
+lemma minim_Under_under:
assumes NE: "A \<noteq> {}" and SUB: "A \<le> Field r"
shows "Under A = under (minim A)"
proof-
@@ -128,7 +130,7 @@
ultimately show ?thesis by blast
qed
-lemma (in wo_rel) minim_UnderS_underS:
+lemma minim_UnderS_underS:
assumes NE: "A \<noteq> {}" and SUB: "A \<le> Field r"
shows "UnderS A = underS (minim A)"
proof-
@@ -176,7 +178,7 @@
subsubsection{* Properties of supr *}
-lemma (in wo_rel) supr_Above:
+lemma supr_Above:
assumes SUB: "B \<le> Field r" and ABOVE: "Above B \<noteq> {}"
shows "supr B \<in> Above B"
proof(unfold supr_def)
@@ -186,7 +188,7 @@
using assms by (simp add: minim_in)
qed
-lemma (in wo_rel) supr_greater:
+lemma supr_greater:
assumes SUB: "B \<le> Field r" and ABOVE: "Above B \<noteq> {}" and
IN: "b \<in> B"
shows "(b, supr B) \<in> r"
@@ -196,7 +198,7 @@
with IN Above_def show ?thesis by simp
qed
-lemma (in wo_rel) supr_least_Above:
+lemma supr_least_Above:
assumes SUB: "B \<le> Field r" and
ABOVE: "a \<in> Above B"
shows "(supr B, a) \<in> r"
@@ -208,12 +210,12 @@
by simp
qed
-lemma (in wo_rel) supr_least:
+lemma supr_least:
"\<lbrakk>B \<le> Field r; a \<in> Field r; (\<And> b. b \<in> B \<Longrightarrow> (b,a) \<in> r)\<rbrakk>
\<Longrightarrow> (supr B, a) \<in> r"
by(auto simp add: supr_least_Above Above_def)
-lemma (in wo_rel) equals_supr_Above:
+lemma equals_supr_Above:
assumes SUB: "B \<le> Field r" and ABV: "a \<in> Above B" and
MINIM: "\<And> a'. a' \<in> Above B \<Longrightarrow> (a,a') \<in> r"
shows "a = supr B"
@@ -224,7 +226,7 @@
using assms equals_minim by simp
qed
-lemma (in wo_rel) equals_supr:
+lemma equals_supr:
assumes SUB: "B \<le> Field r" and IN: "a \<in> Field r" and
ABV: "\<And> b. b \<in> B \<Longrightarrow> (b,a) \<in> r" and
MINIM: "\<And> a'. \<lbrakk> a' \<in> Field r; \<And> b. b \<in> B \<Longrightarrow> (b,a') \<in> r\<rbrakk> \<Longrightarrow> (a,a') \<in> r"
@@ -239,7 +241,7 @@
using equals_supr_Above SUB by auto
qed
-lemma (in wo_rel) supr_inField:
+lemma supr_inField:
assumes "B \<le> Field r" and "Above B \<noteq> {}"
shows "supr B \<in> Field r"
proof-
@@ -247,7 +249,7 @@
thus ?thesis using assms Above_Field by auto
qed
-lemma (in wo_rel) supr_above_Above:
+lemma supr_above_Above:
assumes SUB: "B \<le> Field r" and ABOVE: "Above B \<noteq> {}"
shows "Above B = above (supr B)"
proof(unfold Above_def above_def, auto)
@@ -267,7 +269,7 @@
using 1 TRANS trans_def[of r] by blast
qed
-lemma (in wo_rel) supr_under:
+lemma supr_under:
assumes IN: "a \<in> Field r"
shows "a = supr (under a)"
proof-
@@ -297,12 +299,12 @@
subsubsection{* Properties of successor *}
-lemma (in wo_rel) suc_least:
+lemma suc_least:
"\<lbrakk>B \<le> Field r; a \<in> Field r; (\<And> b. b \<in> B \<Longrightarrow> a \<noteq> b \<and> (b,a) \<in> r)\<rbrakk>
\<Longrightarrow> (suc B, a) \<in> r"
by(auto simp add: suc_least_AboveS AboveS_def)
-lemma (in wo_rel) equals_suc:
+lemma equals_suc:
assumes SUB: "B \<le> Field r" and IN: "a \<in> Field r" and
ABVS: "\<And> b. b \<in> B \<Longrightarrow> a \<noteq> b \<and> (b,a) \<in> r" and
MINIM: "\<And> a'. \<lbrakk>a' \<in> Field r; \<And> b. b \<in> B \<Longrightarrow> a' \<noteq> b \<and> (b,a') \<in> r\<rbrakk> \<Longrightarrow> (a,a') \<in> r"
@@ -317,7 +319,7 @@
using equals_suc_AboveS SUB by auto
qed
-lemma (in wo_rel) suc_above_AboveS:
+lemma suc_above_AboveS:
assumes SUB: "B \<le> Field r" and
ABOVE: "AboveS B \<noteq> {}"
shows "AboveS B = above (suc B)"
@@ -349,7 +351,7 @@
using assms suc_greater[of B a] 2 by auto
qed
-lemma (in wo_rel) suc_singl_pred:
+lemma suc_singl_pred:
assumes IN: "a \<in> Field r" and ABOVE_NE: "aboveS a \<noteq> {}" and
REL: "(a',suc {a}) \<in> r" and DIFF: "a' \<noteq> suc {a}"
shows "a' = a \<or> (a',a) \<in> r"
@@ -372,7 +374,7 @@
thus ?thesis by blast
qed
-lemma (in wo_rel) under_underS_suc:
+lemma under_underS_suc:
assumes IN: "a \<in> Field r" and ABV: "aboveS a \<noteq> {}"
shows "underS (suc {a}) = under a"
proof-
@@ -410,19 +412,19 @@
subsubsection {* Properties of order filters *}
-lemma (in wo_rel) ofilter_INTER:
+lemma ofilter_INTER:
"\<lbrakk>I \<noteq> {}; \<And> i. i \<in> I \<Longrightarrow> ofilter(A i)\<rbrakk> \<Longrightarrow> ofilter (\<Inter> i \<in> I. A i)"
unfolding ofilter_def by blast
-lemma (in wo_rel) ofilter_Inter:
+lemma ofilter_Inter:
"\<lbrakk>S \<noteq> {}; \<And> A. A \<in> S \<Longrightarrow> ofilter A\<rbrakk> \<Longrightarrow> ofilter (Inter S)"
unfolding ofilter_def by blast
-lemma (in wo_rel) ofilter_Union:
+lemma ofilter_Union:
"(\<And> A. A \<in> S \<Longrightarrow> ofilter A) \<Longrightarrow> ofilter (Union S)"
unfolding ofilter_def by blast
-lemma (in wo_rel) ofilter_under_Union:
+lemma ofilter_under_Union:
"ofilter A \<Longrightarrow> A = Union {under a| a. a \<in> A}"
using ofilter_under_UNION[of A]
by(unfold Union_eq, auto)
@@ -430,7 +432,7 @@
subsubsection{* Other properties *}
-lemma (in wo_rel) Trans_Under_regressive:
+lemma Trans_Under_regressive:
assumes NE: "A \<noteq> {}" and SUB: "A \<le> Field r"
shows "Under(Under A) \<le> Under A"
proof
@@ -455,7 +457,7 @@
show "x \<in> Under A" unfolding Under_def by auto
qed
-lemma (in wo_rel) ofilter_suc_Field:
+lemma ofilter_suc_Field:
assumes OF: "ofilter A" and NE: "A \<noteq> Field r"
shows "ofilter (A \<union> {suc A})"
proof-
@@ -487,7 +489,7 @@
qed
(* FIXME: needed? *)
-declare (in wo_rel)
+declare
minim_in[simp]
minim_inField[simp]
minim_least[simp]
@@ -499,6 +501,8 @@
ofilter_Int[simp]
ofilter_Un[simp]
+end
+
abbreviation "worec \<equiv> wo_rel.worec"
abbreviation "adm_wo \<equiv> wo_rel.adm_wo"
abbreviation "isMinim \<equiv> wo_rel.isMinim"
--- a/src/HOL/Cardinals/Wellorder_Relation_Base.thy Wed Apr 24 16:21:23 2013 +0200
+++ b/src/HOL/Cardinals/Wellorder_Relation_Base.thy Wed Apr 24 16:43:19 2013 +0200
@@ -234,8 +234,8 @@
assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}"
shows "\<exists>b. isMinim B b"
proof-
- from WF wf_eq_minimal[of "r - Id"] NE Id_def obtain b where
- *: "b \<in> B \<and> (\<forall>b'. b' \<noteq> b \<and> (b',b) \<in> r \<longrightarrow> b' \<notin> B)" by force
+ from spec[OF WF[unfolded wf_eq_minimal[of "r - Id"]], of B] NE obtain b where
+ *: "b \<in> B \<and> (\<forall>b'. b' \<noteq> b \<and> (b',b) \<in> r \<longrightarrow> b' \<notin> B)" by auto
show ?thesis
proof(simp add: isMinim_def, rule exI[of _ b], auto)
show "b \<in> B" using * by simp