get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
--- a/src/HOL/BNF/BNF_LFP.thy Thu Jan 16 18:52:50 2014 +0100
+++ b/src/HOL/BNF/BNF_LFP.thy Thu Jan 16 20:52:54 2014 +0100
@@ -30,14 +30,14 @@
lemma prop_restrict: "\<lbrakk>x \<in> Z; Z \<subseteq> {x. x \<in> X \<and> P x}\<rbrakk> \<Longrightarrow> P x"
by auto
-lemma underS_I: "\<lbrakk>i \<noteq> j; (i, j) \<in> R\<rbrakk> \<Longrightarrow> i \<in> rel.underS R j"
-unfolding rel.underS_def by simp
+lemma underS_I: "\<lbrakk>i \<noteq> j; (i, j) \<in> R\<rbrakk> \<Longrightarrow> i \<in> underS R j"
+unfolding underS_def by simp
-lemma underS_E: "i \<in> rel.underS R j \<Longrightarrow> i \<noteq> j \<and> (i, j) \<in> R"
-unfolding rel.underS_def by simp
+lemma underS_E: "i \<in> underS R j \<Longrightarrow> i \<noteq> j \<and> (i, j) \<in> R"
+unfolding underS_def by simp
-lemma underS_Field: "i \<in> rel.underS R j \<Longrightarrow> i \<in> Field R"
-unfolding rel.underS_def Field_def by auto
+lemma underS_Field: "i \<in> underS R j \<Longrightarrow> i \<in> Field R"
+unfolding underS_def Field_def by auto
lemma FieldI2: "(i, j) \<in> R \<Longrightarrow> j \<in> Field R"
unfolding Field_def by auto
--- a/src/HOL/BNF/Tools/bnf_lfp_util.ML Thu Jan 16 18:52:50 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_lfp_util.ML Thu Jan 16 20:52:54 2014 +0100
@@ -34,7 +34,7 @@
fun mk_underS r =
let val T = fst (dest_relT (fastype_of r));
- in Const (@{const_name rel.underS}, mk_relT (T, T) --> T --> HOLogic.mk_setT T) $ r end;
+ in Const (@{const_name underS}, mk_relT (T, T) --> T --> HOLogic.mk_setT T) $ r end;
fun mk_worec r f =
let val (A, AB) = apfst domain_type (dest_funT (fastype_of f));
--- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy Thu Jan 16 18:52:50 2014 +0100
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy Thu Jan 16 20:52:54 2014 +0100
@@ -1012,11 +1012,11 @@
lemma natLeq_ofilter_less: "ofilter natLeq {0 ..< n}"
by(auto simp add: natLeq_wo_rel wo_rel.ofilter_def,
- simp add: Field_natLeq, unfold rel.under_def, auto)
+ simp add: Field_natLeq, unfold under_def, auto)
lemma natLeq_ofilter_leq: "ofilter natLeq {0 .. n}"
by(auto simp add: natLeq_wo_rel wo_rel.ofilter_def,
- simp add: Field_natLeq, unfold rel.under_def, auto)
+ simp add: Field_natLeq, unfold under_def, auto)
lemma natLeq_UNIV_ofilter: "wo_rel.ofilter natLeq UNIV"
using natLeq_wo_rel Field_natLeq wo_rel.Field_ofilter[of natLeq] by auto
@@ -1047,7 +1047,7 @@
proof(rule iffI)
assume "ofilter natLeq A"
hence "\<forall>m n. n \<in> A \<and> m \<le> n \<longrightarrow> m \<in> A"
- by(auto simp add: natLeq_wo_rel wo_rel.ofilter_def rel.under_def)
+ by(auto simp add: natLeq_wo_rel wo_rel.ofilter_def under_def)
thus "A = UNIV \<or> (\<exists>n. A = {0 ..< n})" using closed_nat_set_iff by blast
next
assume "A = UNIV \<or> (\<exists>n. A = {0 ..< n})"
@@ -1056,22 +1056,22 @@
qed
lemma natLeq_under_leq: "under natLeq n = {0 .. n}"
-unfolding rel.under_def by auto
+unfolding under_def by auto
lemma natLeq_on_ofilter_less_eq:
"n \<le> m \<Longrightarrow> wo_rel.ofilter (natLeq_on m) {0 ..< n}"
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)
+by (auto simp add: under_def)
lemma natLeq_on_ofilter_iff:
"wo_rel.ofilter (natLeq_on m) A = (\<exists>n \<le> m. A = {0 ..< n})"
proof(rule iffI)
assume *: "wo_rel.ofilter (natLeq_on m) A"
hence 1: "A \<le> {0..<m}"
- by (auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def rel.under_def Field_natLeq_on)
+ by (auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def under_def Field_natLeq_on)
hence "\<forall>n1 n2. n2 \<in> A \<and> n1 \<le> n2 \<longrightarrow> n1 \<in> A"
- using * by(fastforce simp add: natLeq_on_wo_rel wo_rel.ofilter_def rel.under_def)
+ using * by(fastforce simp add: natLeq_on_wo_rel wo_rel.ofilter_def under_def)
hence "A = UNIV \<or> (\<exists>n. A = {0 ..< n})" using closed_nat_set_iff by blast
thus "\<exists>n \<le> m. A = {0 ..< n}" using 1 atLeastLessThan_less_eq by blast
next
@@ -1086,7 +1086,7 @@
lemma natLeq_on_ofilter_less:
"n < m \<Longrightarrow> 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)
+ simp add: Field_natLeq_on, unfold under_def, auto)
lemma natLeq_on_ordLess_natLeq: "natLeq_on n <o natLeq"
using Field_natLeq Field_natLeq_on[of n]
@@ -1331,13 +1331,13 @@
lemma under_mono[simp]:
assumes "Well_order r" and "(i,j) \<in> r"
shows "under r i \<subseteq> under r j"
-using assms unfolding rel.under_def order_on_defs
+using assms unfolding under_def order_on_defs
trans_def by blast
lemma underS_under:
assumes "i \<in> Field r"
shows "underS r i = under r i - {i}"
-using assms unfolding rel.underS_def rel.under_def by auto
+using assms unfolding underS_def under_def by auto
lemma relChain_under:
assumes "Well_order r"
@@ -1593,7 +1593,7 @@
unfolding p_def apply(rule Refl_Field_Restr2[OF rr]) by auto
have of: "ofilter r (Field p)" unfolding wo_rel.ofilter_def[OF 0] proof safe
fix a x assume a: "a \<in> Field p" and "x \<in> under r a"
- hence x: "(x,a) \<in> r" "x \<in> Field r" unfolding rel.under_def Field_def by auto
+ hence x: "(x,a) \<in> r" "x \<in> Field r" unfolding under_def Field_def by auto
moreover have a: "a \<noteq> j" "a \<in> Field r" "(a,j) \<in> r" using a jm unfolding fp by auto
ultimately have "x \<noteq> j" using j jm by (metis 0 wo_rel.max2_def wo_rel.max2_equals1)
thus "x \<in> Field p" using x unfolding fp by auto
@@ -1654,7 +1654,7 @@
hence "As (succ r i) \<subseteq> As j" using rc unfolding relChain_def by auto
moreover
{have "(i,succ r i) \<in> r" apply(rule wo_rel.succ_in[OF 0])
- using 1 unfolding rel.aboveS_def by auto
+ using 1 unfolding aboveS_def by auto
hence "As i \<subset> As (succ r i)" using As_s rc rij unfolding relChain_def Field_def by auto
}
ultimately show False unfolding Asij by auto
@@ -1721,13 +1721,13 @@
def g \<equiv> "\<lambda> a. if F a \<noteq> {} then gg a else j0"
have g: "\<forall> a \<in> A. \<forall> u \<in> F a. (f (a,u),g a) \<in> r" using gg unfolding g_def by auto
hence 1: "Field r \<subseteq> (\<Union> a \<in> A. under r (g a))"
- using f[symmetric] unfolding rel.under_def image_def by auto
+ using f[symmetric] unfolding under_def image_def by auto
have gA: "g ` A \<subseteq> Field r" using gg j0 unfolding Field_def g_def by auto
moreover have "cofinal (g ` A) r" unfolding cofinal_def proof safe
fix i assume "i \<in> Field r"
then obtain j where ij: "(i,j) \<in> r" "i \<noteq> j" using cr ir by (metis infinite_Card_order_limit)
- hence "j \<in> Field r" by (metis card_order_on_def cr rel.well_order_on_domain)
- then obtain a where a: "a \<in> A" and j: "(j, g a) \<in> r" using 1 unfolding rel.under_def by auto
+ hence "j \<in> Field r" by (metis card_order_on_def cr well_order_on_domain)
+ then obtain a where a: "a \<in> A" and j: "(j, g a) \<in> r" using 1 unfolding under_def by auto
hence "(i, g a) \<in> r" using ij wo_rel.TRANS[OF r] unfolding trans_def by blast
moreover have "i \<noteq> g a"
using ij j r unfolding wo_rel_def unfolding well_order_on_def linear_order_on_def
@@ -1752,7 +1752,7 @@
{assume Kr: "|K| <o r"
then obtain f where "\<forall> a \<in> Field r. f a \<in> K \<and> a \<noteq> f a \<and> (a, f a) \<in> r"
using cof unfolding cofinal_def by metis
- hence "Field r \<subseteq> (\<Union> a \<in> K. underS r a)" unfolding rel.underS_def by auto
+ hence "Field r \<subseteq> (\<Union> a \<in> K. underS r a)" unfolding underS_def by auto
hence "r \<le>o |\<Union> a \<in> K. underS r a|" using cr
by (metis Card_order_iff_ordLeq_card_of card_of_mono1 ordLeq_transitive)
also have "|\<Union> a \<in> K. underS r a| \<le>o |SIGMA a: K. underS r a|" by (rule card_of_UNION_Sigma)
--- a/src/HOL/Cardinals/Cardinal_Order_Relation_FP.thy Thu Jan 16 18:52:50 2014 +0100
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation_FP.thy Thu Jan 16 20:52:54 2014 +0100
@@ -59,7 +59,7 @@
lemma card_order_on_Card_order:
"card_order_on A r \<Longrightarrow> A = Field r \<and> Card_order r"
-unfolding card_order_on_def using rel.well_order_on_Field by blast
+unfolding card_order_on_def using well_order_on_Field by blast
text{* The existence of a cardinal relation on any given set (which will mean
@@ -77,7 +77,7 @@
proof-
obtain R where R_def: "R = {r. well_order_on A r}" by blast
have 1: "R \<noteq> {} \<and> (\<forall>r \<in> R. Well_order r)"
- using well_order_on[of A] R_def rel.well_order_on_Well_order by blast
+ using well_order_on[of A] R_def well_order_on_Well_order by blast
hence "\<exists>r \<in> R. \<forall>r' \<in> R. r \<le>o r'"
using exists_minim_Well_order[of R] by auto
thus ?thesis using R_def unfolding card_order_on_def by auto
@@ -98,7 +98,7 @@
proof(unfold card_order_on_def, auto)
fix p' assume "well_order_on (Field r') p'"
hence 0: "Well_order p' \<and> Field p' = Field r'"
- using rel.well_order_on_Well_order by blast
+ using well_order_on_Well_order by blast
obtain f where 1: "iso r' r f" and 2: "Well_order r \<and> Well_order r'"
using ISO unfolding ordIso_def by auto
hence 3: "inj_on f (Field r') \<and> f ` (Field r') = Field r"
@@ -143,7 +143,7 @@
lemma Field_card_of: "Field |A| = A"
using card_of_card_order_on[of A] unfolding card_order_on_def
-using rel.well_order_on_Field by blast
+using well_order_on_Field by blast
lemma card_of_Card_order: "Card_order |A|"
@@ -273,7 +273,7 @@
obtain f where
1: "well_order_on (Field r) r \<and> well_order_on (Field r) r \<and> embed r r' f"
using assms unfolding ordLeq_def
- by (auto simp add: rel.well_order_on_Well_order)
+ by (auto simp add: well_order_on_Well_order)
hence "inj_on f (Field r) \<and> f ` (Field r) \<le> Field r'"
by (auto simp add: embed_inj_on embed_Field)
thus "|Field r| \<le>o |Field r'|" using card_of_ordLeq by blast
@@ -285,7 +285,7 @@
lemma card_of_Field_ordLess: "Well_order r \<Longrightarrow> |Field r| \<le>o r"
-using card_of_least card_of_well_order_on rel.well_order_on_Well_order by blast
+using card_of_least card_of_well_order_on well_order_on_Well_order by blast
lemma card_of_Field_ordIso:
@@ -321,16 +321,16 @@
lemma Card_order_iff_Restr_underS:
assumes "Well_order r"
-shows "Card_order r = (\<forall>a \<in> Field r. Restr r (rel.underS r a) <o |Field r| )"
+shows "Card_order r = (\<forall>a \<in> Field r. Restr r (underS r a) <o |Field r| )"
using assms unfolding Card_order_iff_ordLeq_card_of
using ordLeq_iff_ordLess_Restr card_of_Well_order by blast
lemma card_of_underS:
assumes r: "Card_order r" and a: "a : Field r"
-shows "|rel.underS r a| <o r"
+shows "|underS r a| <o r"
proof-
- let ?A = "rel.underS r a" let ?r' = "Restr r ?A"
+ let ?A = "underS r a" let ?r' = "Restr r ?A"
have 1: "Well_order r"
using r unfolding card_order_on_def by simp
have "Well_order ?r'" using 1 Well_order_Restr by auto
@@ -355,7 +355,7 @@
shows "|Field r| <o r'"
proof-
have "well_order_on (Field r) r" using assms unfolding ordLess_def
- by (auto simp add: rel.well_order_on_Well_order)
+ by (auto simp add: well_order_on_Well_order)
hence "|Field r| \<le>o r" using card_of_least by blast
thus ?thesis using assms ordLeq_ordLess_trans by blast
qed
@@ -937,35 +937,35 @@
lemma Card_order_infinite_not_under:
assumes CARD: "Card_order r" and INF: "\<not>finite (Field r)"
-shows "\<not> (\<exists>a. Field r = rel.under r a)"
+shows "\<not> (\<exists>a. Field r = under r a)"
proof(auto)
have 0: "Well_order r \<and> wo_rel r \<and> Refl r"
using CARD unfolding wo_rel_def card_order_on_def order_on_defs by auto
- fix a assume *: "Field r = rel.under r a"
+ fix a assume *: "Field r = under r a"
show False
proof(cases "a \<in> Field r")
assume Case1: "a \<notin> Field r"
- hence "rel.under r a = {}" unfolding Field_def rel.under_def by auto
+ hence "under r a = {}" unfolding Field_def under_def by auto
thus False using INF * by auto
next
- let ?r' = "Restr r (rel.underS r a)"
+ let ?r' = "Restr r (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 metis
- have 2: "wo_rel.ofilter r (rel.underS r a) \<and> rel.underS r a < 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
+ 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
moreover
- have "Field ?r' = rel.underS r a \<and> Well_order ?r'"
+ have "Field ?r' = underS r a \<and> Well_order ?r'"
using 2 0 Field_Restr_ofilter[of r] Well_order_Restr[of r] by blast
- ultimately have "|rel.underS r a| <o r" using ordLess_Field[of ?r'] by auto
- moreover have "|rel.under r a| =o r" using * CARD card_of_Field_ordIso[of r] by auto
- ultimately have "|rel.underS r a| <o |rel.under r a|"
+ ultimately have "|underS r a| <o r" using ordLess_Field[of ?r'] by auto
+ moreover have "|under r a| =o r" using * CARD card_of_Field_ordIso[of r] by auto
+ ultimately have "|underS r a| <o |under r a|"
using ordIso_symmetric ordLess_ordIso_trans by blast
moreover
- {have "\<exists>f. bij_betw f (rel.under r a) (rel.underS r a)"
+ {have "\<exists>f. bij_betw f (under r a) (underS r a)"
using infinite_imp_bij_betw[of "Field r" a] INF * 1 by auto
- hence "|rel.under r a| =o |rel.underS r a|" using card_of_ordIso by blast
+ hence "|under r a| =o |underS r a|" using card_of_ordIso by blast
}
ultimately show False using not_ordLess_ordIso ordIso_symmetric by blast
qed
@@ -977,13 +977,13 @@
and a: "a : Field r"
shows "EX b : Field r. a \<noteq> b \<and> (a,b) : r"
proof-
- have "Field r \<noteq> rel.under r a"
+ have "Field r \<noteq> under r a"
using assms Card_order_infinite_not_under by blast
- moreover have "rel.under r a \<le> Field r"
- using rel.under_Field .
- ultimately have "rel.under r a < Field r" by blast
+ moreover have "under r a \<le> Field r"
+ using under_Field .
+ ultimately have "under r a < Field r" by blast
then obtain b where 1: "b : Field r \<and> ~ (b,a) : r"
- unfolding rel.under_def by blast
+ unfolding under_def by blast
moreover have ba: "b \<noteq> a"
using 1 r unfolding card_order_on_def well_order_on_def
linear_order_on_def partial_order_on_def preorder_on_def refl_on_def by auto
@@ -1036,7 +1036,7 @@
using 7 unfolding bij_betw_def using 6 3 embed_inj_on 4 by auto
hence temp2: "wo_rel.ofilter ?r' ?B \<and> ?B < ?A \<times> ?A"
using 4 wo_rel_def[of ?r'] wo_rel.ofilter_def[of ?r' ?B] by blast
- have "\<not> (\<exists>a. Field r = rel.under r a)"
+ have "\<not> (\<exists>a. Field r = under r a)"
using 1 unfolding phi_def using Card_order_infinite_not_under[of r] by auto
then obtain A1 where temp3: "wo_rel.ofilter r A1 \<and> A1 < ?A" and 9: "?B \<le> A1 \<times> A1"
using temp2 3 bsqr_ofilter[of r ?B] by blast
@@ -1332,8 +1332,8 @@
unfolding Field_def by auto
-lemma natLeq_underS_less: "rel.underS natLeq n = {x. x < n}"
-unfolding rel.underS_def by auto
+lemma natLeq_underS_less: "underS natLeq n = {x. x < n}"
+unfolding underS_def by auto
lemma Restr_natLeq: "Restr natLeq {x. x < n} = natLeq_on n"
@@ -1341,7 +1341,7 @@
lemma Restr_natLeq2:
-"Restr natLeq (rel.underS natLeq n) = natLeq_on n"
+"Restr natLeq (underS natLeq n) = natLeq_on n"
by (auto simp add: Restr_natLeq natLeq_underS_less)
@@ -1728,7 +1728,7 @@
using r' by (simp add: card_of_Field_ordIso[of ?r'])
finally have "|K| \<le>o ?r'" .
moreover
- {let ?L = "UN j : K. rel.underS ?r' j"
+ {let ?L = "UN j : K. underS ?r' j"
let ?J = "Field r"
have rJ: "r =o |?J|"
using r_card card_of_Field_ordIso ordIso_symmetric by blast
@@ -1736,11 +1736,11 @@
hence "|K| <=o r" using r' card_of_Card_order[of K] by blast
hence "|K| \<le>o |?J|" using rJ ordLeq_ordIso_trans by blast
moreover
- {have "ALL j : K. |rel.underS ?r' j| <o ?r'"
+ {have "ALL j : K. |underS ?r' j| <o ?r'"
using r' 1 by (auto simp: card_of_underS)
- hence "ALL j : K. |rel.underS ?r' j| \<le>o r"
+ hence "ALL j : K. |underS ?r' j| \<le>o r"
using r' card_of_Card_order by blast
- hence "ALL j : K. |rel.underS ?r' j| \<le>o |?J|"
+ hence "ALL j : K. |underS ?r' j| \<le>o |?J|"
using rJ ordLeq_ordIso_trans by blast
}
ultimately have "|?L| \<le>o |?J|"
@@ -1750,7 +1750,7 @@
moreover
{
have "Field ?r' \<le> ?L"
- using 2 unfolding rel.underS_def cofinal_def by auto
+ using 2 unfolding underS_def cofinal_def by auto
hence "|Field ?r'| \<le>o |?L|" by (simp add: card_of_mono1)
hence "?r' \<le>o |?L|"
using 22 ordIso_ordLeq_trans ordIso_symmetric by blast
--- a/src/HOL/Cardinals/Constructions_on_Wellorders.thy Thu Jan 16 18:52:50 2014 +0100
+++ b/src/HOL/Cardinals/Constructions_on_Wellorders.thy Thu Jan 16 20:52:54 2014 +0100
@@ -216,7 +216,7 @@
moreover
have "ofilter (r Osum r') (Field r)"
using 1 proof(auto simp add: wo_rel_def wo_rel.ofilter_def
- Field_Osum rel.under_def)
+ Field_Osum under_def)
fix a b assume 2: "a \<in> Field r" and 3: "(b,a) \<in> r Osum r'"
moreover
{assume "(b,a) \<in> r'"
@@ -251,13 +251,13 @@
then obtain r'' where "well_order_on (f ` A) r''" and 1: "r =o r''"
using WELL Well_order_iso_copy by blast
hence 2: "Well_order r'' \<and> Field r'' = (f ` A)"
- using rel.well_order_on_Well_order by blast
+ using well_order_on_Well_order by blast
(* *)
let ?C = "B - (f ` A)"
obtain r''' where "well_order_on ?C r'''"
using well_order_on by blast
hence 3: "Well_order r''' \<and> Field r''' = ?C"
- using rel.well_order_on_Well_order by blast
+ using well_order_on_Well_order by blast
(* *)
let ?r' = "r'' Osum r'''"
have "Field r'' Int Field r''' = {}"
@@ -479,23 +479,18 @@
have bb: "b \<in> Field r" using bA unfolding underS_def Field_def by auto
assume "\<forall>a\<in>A. b \<notin> under a"
hence 0: "\<forall>a \<in> A. a \<in> underS b" using A bA unfolding underS_def
- by simp (metis (lifting) bb max2_def max2_greater mem_Collect_eq rel.under_def set_rev_mp)
- have "(suc A, b) \<in> r" apply(rule suc_least[OF A bb]) using 0 unfolding rel.underS_def by auto
+ by simp (metis (lifting) bb max2_def max2_greater mem_Collect_eq under_def set_rev_mp)
+ have "(suc A, b) \<in> r" apply(rule suc_least[OF A bb]) using 0 unfolding underS_def by auto
thus False using bA unfolding underS_def by simp (metis ANTISYM antisymD)
qed
-lemma (in rel) AboveS_underS:
-assumes "i \<in> Field r"
-shows "i \<in> AboveS (underS i)"
-using assms unfolding AboveS_def underS_def by auto
-
lemma (in wo_rel) in_underS_supr:
assumes j: "j \<in> underS i" and i: "i \<in> A" and A: "A \<subseteq> Field r" and AA: "Above A \<noteq> {}"
shows "j \<in> underS (supr A)"
proof-
have "(i,supr A) \<in> r" using supr_greater[OF A AA i] .
thus ?thesis using j unfolding underS_def
- by simp (metis REFL TRANS max2_def max2_equals1 rel.refl_on_domain transD)
+ by simp (metis REFL TRANS max2_def max2_equals1 refl_on_domain transD)
qed
lemma inj_on_Field:
@@ -530,7 +525,7 @@
and init: "(R ja, R j) \<notin> init_seg_of"
hence jja: "{j,ja} \<subseteq> Field r" and j: "j \<in> Field r" and ja: "ja \<in> Field r"
and jjai: "(j,i) \<in> r" "(ja,i) \<in> r"
- and i: "i \<notin> {j,ja}" unfolding Field_def rel.underS_def by auto
+ and i: "i \<notin> {j,ja}" unfolding Field_def underS_def by auto
have jj: "(j,j) \<in> r" and jaja: "(ja,ja) \<in> r" using j ja by (metis in_notinI)+
show "R j initial_segment_of R ja"
using jja init jjai i
@@ -544,7 +539,7 @@
fix j ja assume jS: "j \<in> Field r" and jaS: "ja \<in> Field r"
and init: "(R ja, R j) \<notin> init_seg_of"
hence jja: "{j,ja} \<subseteq> Field r" and j: "j \<in> Field r" and ja: "ja \<in> Field r"
- unfolding Field_def rel.underS_def by auto
+ unfolding Field_def underS_def by auto
have jj: "(j,j) \<in> r" and jaja: "(ja,ja) \<in> r" using j ja by (metis in_notinI)+
show "R j initial_segment_of R ja"
using jja init
@@ -700,8 +695,8 @@
assumes "aboveS i \<noteq> {}"
shows "(j, succ i) \<in> r \<longleftrightarrow> (j,i) \<in> r \<or> j = succ i"
apply safe
- apply (metis WELL assms in_notinI rel.well_order_on_domain suc_singl_pred succ_def succ_in_diff)
- apply (metis (hide_lams, full_types) REFL TRANS assms max2_def max2_equals1 rel.refl_on_domain succ_in_Field succ_not_in transD)
+ apply (metis WELL assms in_notinI well_order_on_domain suc_singl_pred succ_def succ_in_diff)
+ apply (metis (hide_lams, full_types) REFL TRANS assms max2_def max2_equals1 refl_on_domain succ_in_Field succ_not_in transD)
apply (metis assms in_notinI succ_in_Field)
done
@@ -926,7 +921,7 @@
lemma oproj_under:
assumes f: "oproj r s f" and a: "a \<in> under r a'"
shows "f a \<in> under s (f a')"
-using oproj_in[OF f] a unfolding rel.under_def by auto
+using oproj_in[OF f] a unfolding under_def by auto
(* An ordinal is embedded in another whenever it is embedded as an order
(not necessarily as initial segment):*)
@@ -950,55 +945,55 @@
and IH1a: "\<And> a1. a1 \<in> underS r a \<Longrightarrow> inj_on g (under r a1)"
and IH1b: "\<And> a1. a1 \<in> underS r a \<Longrightarrow> g ` under r a1 = under s (g a1)"
and IH2: "\<And> a1. a1 \<in> underS r a \<Longrightarrow> g a1 \<in> under s (f a1)"
- unfolding rel.underS_def Field_def bij_betw_def by auto
+ unfolding underS_def Field_def bij_betw_def by auto
have fa: "f a \<in> Field s" using f[OF a] by auto
have g: "g a = suc s (g ` underS r a)"
using r.worec_fixpoint[OF adm] unfolding g_def fun_eq_iff by simp
have A0: "g ` underS r a \<subseteq> Field s"
- using IH1b by (metis IH2 image_subsetI in_mono rel.under_Field)
+ using IH1b by (metis IH2 image_subsetI in_mono under_Field)
{fix a1 assume a1: "a1 \<in> underS r a"
from IH2[OF this] have "g a1 \<in> under s (f a1)" .
moreover have "f a1 \<in> underS s (f a)" using f[OF a] a1 by auto
- ultimately have "g a1 \<in> underS s (f a)" by (metis s.ANTISYM s.TRANS rel.under_underS_trans)
+ ultimately have "g a1 \<in> underS s (f a)" by (metis s.ANTISYM s.TRANS under_underS_trans)
}
- hence "f a \<in> AboveS s (g ` underS r a)" unfolding rel.AboveS_def
- using fa by simp (metis (lifting, full_types) mem_Collect_eq rel.underS_def)
+ hence "f a \<in> AboveS s (g ` underS r a)" unfolding AboveS_def
+ using fa by simp (metis (lifting, full_types) mem_Collect_eq underS_def)
hence A: "AboveS s (g ` underS r a) \<noteq> {}" by auto
have B: "\<And> a1. a1 \<in> underS r a \<Longrightarrow> g a1 \<in> underS s (g a)"
unfolding g apply(rule s.suc_underS[OF A0 A]) by auto
{fix a1 a2 assume a2: "a2 \<in> underS r a" and 1: "a1 \<in> underS r a2"
hence a12: "{a1,a2} \<subseteq> under r a2" and "a1 \<noteq> a2" using r.REFL a
- unfolding rel.underS_def rel.under_def refl_on_def Field_def by auto
+ unfolding underS_def under_def refl_on_def Field_def by auto
hence "g a1 \<noteq> g a2" using IH1a[OF a2] unfolding inj_on_def by auto
hence "g a1 \<in> underS s (g a2)" using IH1b[OF a2] a12
- unfolding rel.underS_def rel.under_def by auto
+ unfolding underS_def under_def by auto
} note C = this
have ga: "g a \<in> Field s" unfolding g using s.suc_inField[OF A0 A] .
have aa: "a \<in> under r a"
- using a r.REFL unfolding rel.under_def rel.underS_def refl_on_def by auto
+ using a r.REFL unfolding under_def underS_def refl_on_def by auto
show ?case proof safe
show "bij_betw g (under r a) (under s (g a))" unfolding bij_betw_def proof safe
show "inj_on g (under r a)" proof(rule r.inj_on_Field)
fix a1 a2 assume "a1 \<in> under r a" and a2: "a2 \<in> under r a" and a1: "a1 \<in> underS r a2"
hence a22: "a2 \<in> under r a2" and a12: "a1 \<in> under r a2" "a1 \<noteq> a2"
- using a r.REFL unfolding rel.under_def rel.underS_def refl_on_def by auto
+ using a r.REFL unfolding under_def underS_def refl_on_def by auto
show "g a1 \<noteq> g a2"
proof(cases "a2 = a")
case False hence "a2 \<in> underS r a"
- using a2 unfolding rel.underS_def rel.under_def by auto
+ using a2 unfolding underS_def under_def by auto
from IH1a[OF this] show ?thesis using a12 a22 unfolding inj_on_def by auto
- qed(insert B a1, unfold rel.underS_def, auto)
- qed(unfold rel.under_def Field_def, auto)
+ qed(insert B a1, unfold underS_def, auto)
+ qed(unfold under_def Field_def, auto)
next
fix a1 assume a1: "a1 \<in> under r a"
show "g a1 \<in> under s (g a)"
proof(cases "a1 = a")
case True thus ?thesis
- using ga s.REFL unfolding refl_on_def rel.under_def by auto
+ using ga s.REFL unfolding refl_on_def under_def by auto
next
case False
- hence a1: "a1 \<in> underS r a" using a1 unfolding rel.underS_def rel.under_def by auto
- thus ?thesis using B unfolding rel.underS_def rel.under_def by auto
+ hence a1: "a1 \<in> underS r a" using a1 unfolding underS_def under_def by auto
+ thus ?thesis using B unfolding underS_def under_def by auto
qed
next
fix b1 assume b1: "b1 \<in> under s (g a)"
@@ -1007,12 +1002,12 @@
case True thus ?thesis using aa by auto
next
case False
- hence "b1 \<in> underS s (g a)" using b1 unfolding rel.underS_def rel.under_def by auto
+ hence "b1 \<in> underS s (g a)" using b1 unfolding underS_def under_def by auto
from s.underS_suc[OF this[unfolded g] A0]
obtain a1 where a1: "a1 \<in> underS r a" and b1: "b1 \<in> under s (g a1)" by auto
obtain a2 where "a2 \<in> under r a1" and b1: "b1 = g a2" using IH1b[OF a1] b1 by auto
hence "a2 \<in> under r a" using a1
- by (metis r.ANTISYM r.TRANS in_mono rel.underS_subset_under rel.under_underS_trans)
+ by (metis r.ANTISYM r.TRANS in_mono underS_subset_under under_underS_trans)
thus ?thesis using b1 by auto
qed
qed
@@ -1022,9 +1017,9 @@
then obtain a1 where a1: "b1 = g a1" and a1: "a1 \<in> underS r a" by auto
hence "b1 \<in> underS s (f a)"
using a by (metis `\<And>a1. a1 \<in> underS r a \<Longrightarrow> g a1 \<in> underS s (f a)`)
- thus "f a \<noteq> b1 \<and> (b1, f a) \<in> s" unfolding rel.underS_def by auto
+ thus "f a \<noteq> b1 \<and> (b1, f a) \<in> s" unfolding underS_def by auto
qed(insert fa, auto)
- thus "g a \<in> under s (f a)" unfolding rel.under_def by auto
+ thus "g a \<in> under s (f a)" unfolding under_def by auto
qed
qed
}
@@ -1046,7 +1041,7 @@
theorem oproj_embed:
assumes r: "Well_order r" and s: "Well_order s" and f: "oproj r s f"
shows "\<exists> g. embed s r g"
-proof (rule embedI[OF s r, of "inv_into (Field r) f"], unfold rel.underS_def, safe)
+proof (rule embedI[OF s r, of "inv_into (Field r) f"], unfold underS_def, safe)
fix b assume "b \<in> Field s"
thus "inv_into (Field r) f b \<in> Field r" using oproj_Field2[OF f] by (metis imageI inv_into_into)
next
--- a/src/HOL/Cardinals/Constructions_on_Wellorders_FP.thy Thu Jan 16 18:52:50 2014 +0100
+++ b/src/HOL/Cardinals/Constructions_on_Wellorders_FP.thy Thu Jan 16 20:52:54 2014 +0100
@@ -116,12 +116,12 @@
lemma ofilter_Restr_under:
assumes WELL: "Well_order r" and OF: "wo_rel.ofilter r A" and IN: "a \<in> A"
-shows "rel.under (Restr r A) a = rel.under r a"
+shows "under (Restr r A) a = under r a"
using assms wo_rel_def
-proof(auto simp add: wo_rel.ofilter_def rel.under_def)
+proof(auto simp add: wo_rel.ofilter_def under_def)
fix b assume *: "a \<in> A" and "(b,a) \<in> r"
- hence "b \<in> rel.under r a \<and> a \<in> Field r"
- unfolding rel.under_def using Field_def by fastforce
+ hence "b \<in> under r a \<and> a \<in> Field r"
+ unfolding under_def using Field_def by fastforce
thus "b \<in> A" using * assms by (auto simp add: wo_rel_def wo_rel.ofilter_def)
qed
@@ -137,7 +137,7 @@
by (auto simp add: wo_rel_def wo_rel.ofilter_def)
next
fix a assume "a \<in> Field (Restr r A)"
- thus "bij_betw id (rel.under (Restr r A) a) (rel.under r a)" using assms *
+ thus "bij_betw id (under (Restr r A) a) (under r a)" using assms *
by (simp add: ofilter_Restr_under Field_Restr_ofilter)
qed
next
@@ -148,13 +148,13 @@
{fix a assume "a \<in> A"
hence "a \<in> Field(Restr r A)" using * assms
by (simp add: order_on_defs Refl_Field_Restr2)
- hence "bij_betw id (rel.under (Restr r A) a) (rel.under r a)"
+ hence "bij_betw id (under (Restr r A) a) (under r a)"
using * unfolding embed_def by auto
- hence "rel.under r a \<le> rel.under (Restr r A) a"
+ hence "under r a \<le> under (Restr r A) a"
unfolding bij_betw_def by auto
- also have "\<dots> \<le> Field(Restr r A)" by (simp add: rel.under_Field)
+ also have "\<dots> \<le> Field(Restr r A)" by (simp add: under_Field)
also have "\<dots> \<le> A" by (simp add: Field_Restr_subset)
- finally have "rel.under r a \<le> A" .
+ finally have "under r a \<le> A" .
}
thus "wo_rel.ofilter r A" using assms * by (simp add: wo_rel_def wo_rel.ofilter_def)
qed
@@ -173,13 +173,13 @@
by (simp add: Well_order_Restr wo_rel_def)
(* Main proof *)
show ?thesis using WellB assms
- proof(auto simp add: wo_rel.ofilter_def rel.under_def)
+ proof(auto simp add: wo_rel.ofilter_def under_def)
fix a assume "a \<in> A" and *: "a \<in> B"
hence "a \<in> Field r" using OFA Well by (auto simp add: wo_rel.ofilter_def)
with * show "a \<in> Field ?rB" using Field by auto
next
fix a b assume "a \<in> A" and "(b,a) \<in> r"
- thus "b \<in> A" using Well OFA by (auto simp add: wo_rel.ofilter_def rel.under_def)
+ thus "b \<in> A" using Well OFA by (auto simp add: wo_rel.ofilter_def under_def)
qed
qed
@@ -312,12 +312,12 @@
assume *: "wo_rel.ofilter r A" "A \<noteq> Field r" and
**: "wo_rel.ofilter r B" "B \<noteq> Field r" and ***: "A < B"
then obtain a and b where 0: "a \<in> Field r \<and> b \<in> Field r" and
- 1: "A = rel.underS r a \<and> B = rel.underS r b"
+ 1: "A = underS r a \<and> B = underS r b"
using Well by (auto simp add: wo_rel.ofilter_underS_Field)
hence "a \<noteq> b" using *** by auto
moreover
have "(a,b) \<in> r" using 0 1 Lo ***
- by (auto simp add: rel.underS_incl_iff)
+ by (auto simp add: underS_incl_iff)
moreover
have "a = wo_rel.suc r A \<and> b = wo_rel.suc r B"
using Well 0 1 by (simp add: wo_rel.suc_underS)
@@ -714,10 +714,10 @@
corollary underS_Restr_ordLess:
assumes "Well_order r" and "Field r \<noteq> {}"
-shows "Restr r (rel.underS r a) <o r"
+shows "Restr r (underS r a) <o r"
proof-
- have "rel.underS r a < Field r" using assms
- by (simp add: rel.underS_Field3)
+ have "underS r a < Field r" using assms
+ by (simp add: underS_Field3)
thus ?thesis using assms
by (simp add: ofilter_ordLess wo_rel.underS_ofilter wo_rel_def)
qed
@@ -772,10 +772,10 @@
lemma ordLess_iff_ordIso_Restr:
assumes WELL: "Well_order r" and WELL': "Well_order r'"
-shows "(r' <o r) = (\<exists>a \<in> Field r. r' =o Restr r (rel.underS r a))"
+shows "(r' <o r) = (\<exists>a \<in> Field r. r' =o Restr r (underS r a))"
proof(auto)
- fix a assume *: "a \<in> Field r" and **: "r' =o Restr r (rel.underS r a)"
- hence "Restr r (rel.underS r a) <o r" using WELL underS_Restr_ordLess[of r] by blast
+ fix a assume *: "a \<in> Field r" and **: "r' =o Restr r (underS r a)"
+ hence "Restr r (underS r a) <o r" using WELL underS_Restr_ordLess[of r] by blast
thus "r' <o r" using ** ordIso_ordLess_trans by blast
next
assume "r' <o r"
@@ -783,7 +783,7 @@
2: "embed r' r f \<and> f ` (Field r') \<noteq> Field r"
unfolding ordLess_def embedS_def[abs_def] bij_betw_def using embed_inj_on by blast
hence "wo_rel.ofilter r (f ` (Field r'))" using embed_Field_ofilter by blast
- then obtain a where 3: "a \<in> Field r" and 4: "rel.underS r a = f ` (Field r')"
+ then obtain a where 3: "a \<in> Field r" and 4: "underS r a = f ` (Field r')"
using 1 2 by (auto simp add: wo_rel.ofilter_underS_Field wo_rel_def)
have "iso r' (Restr r (f ` (Field r'))) f"
using embed_implies_iso_Restr 2 assms by blast
@@ -791,8 +791,8 @@
using WELL Well_order_Restr by blast
ultimately have "r' =o Restr r (f ` (Field r'))"
using WELL' unfolding ordIso_def by auto
- hence "r' =o Restr r (rel.underS r a)" using 4 by auto
- thus "\<exists>a \<in> Field r. r' =o Restr r (rel.underS r a)" using 3 by auto
+ hence "r' =o Restr r (underS r a)" using 4 by auto
+ thus "\<exists>a \<in> Field r. r' =o Restr r (underS r a)" using 3 by auto
qed
@@ -801,13 +801,13 @@
proof
assume *: "r' <o r"
hence 0: "Well_order r \<and> Well_order r'" unfolding ordLess_def by auto
- with * obtain a where 1: "a \<in> Field r" and 2: "r' =o Restr r (rel.underS r a)"
+ with * obtain a where 1: "a \<in> Field r" and 2: "r' =o Restr r (underS r a)"
using ordLess_iff_ordIso_Restr by blast
- let ?p = "Restr r (rel.underS r a)"
- have "wo_rel.ofilter r (rel.underS r a)" using 0
+ let ?p = "Restr r (underS r a)"
+ have "wo_rel.ofilter r (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 fast
+ hence "Field ?p = underS r a" using 0 Field_Restr_ofilter by blast
+ hence "Field ?p < Field r" using 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
@@ -840,18 +840,18 @@
lemma ordLeq_iff_ordLess_Restr:
assumes WELL: "Well_order r" and WELL': "Well_order r'"
-shows "(r \<le>o r') = (\<forall>a \<in> Field r. Restr r (rel.underS r a) <o r')"
+shows "(r \<le>o r') = (\<forall>a \<in> Field r. Restr r (underS r a) <o r')"
proof(auto)
assume *: "r \<le>o r'"
fix a assume "a \<in> Field r"
- hence "Restr r (rel.underS r a) <o r"
+ hence "Restr r (underS r a) <o r"
using WELL underS_Restr_ordLess[of r] by blast
- thus "Restr r (rel.underS r a) <o r'"
+ thus "Restr r (underS r a) <o r'"
using * ordLess_ordLeq_trans by blast
next
- assume *: "\<forall>a \<in> Field r. Restr r (rel.underS r a) <o r'"
+ assume *: "\<forall>a \<in> Field r. Restr r (underS r a) <o r'"
{assume "r' <o r"
- then obtain a where "a \<in> Field r \<and> r' =o Restr r (rel.underS r a)"
+ then obtain a where "a \<in> Field r \<and> r' =o Restr r (underS r a)"
using assms ordLess_iff_ordIso_Restr by blast
hence False using * not_ordLess_ordIso ordIso_symmetric by blast
}
@@ -879,14 +879,14 @@
shows "r =o r'"
proof-
have 0: "Well_order r \<and> Well_order r' \<and> Field r = A \<and> Field r' = A"
- using assms rel.well_order_on_Well_order by blast
+ using assms well_order_on_Well_order by blast
moreover
have "\<forall>r r'. well_order_on A r \<and> well_order_on A r' \<and> r \<le>o r'
\<longrightarrow> r =o r'"
proof(clarify)
fix r r' assume *: "well_order_on A r" and **: "well_order_on A r'"
have 2: "Well_order r \<and> Well_order r' \<and> Field r = A \<and> Field r' = A"
- using * ** rel.well_order_on_Well_order by blast
+ using * ** well_order_on_Well_order by blast
assume "r \<le>o r'"
then obtain f where 1: "embed r r' f" and
"inj_on f A \<and> f ` A \<le> A"
@@ -1137,7 +1137,7 @@
proof-
let ?r' = "dir_image r f"
have 1: "A = Field r \<and> Well_order r"
- using WELL rel.well_order_on_Well_order by blast
+ using WELL well_order_on_Well_order by blast
hence 2: "iso r ?r' f"
using dir_image_iso using BIJ unfolding bij_betw_def by auto
hence "f ` (Field r) = Field ?r'" using 1 iso_iff[of r ?r'] by blast
@@ -1576,7 +1576,7 @@
lemma bsqr_ofilter:
assumes WELL: "Well_order r" and
OF: "wo_rel.ofilter (bsqr r) D" and SUB: "D < Field r \<times> Field r" and
- NE: "\<not> (\<exists>a. Field r = rel.under r a)"
+ NE: "\<not> (\<exists>a. Field r = under r a)"
shows "\<exists>A. wo_rel.ofilter r A \<and> A < Field r \<and> D \<le> A \<times> A"
proof-
let ?r' = "bsqr r"
@@ -1587,17 +1587,17 @@
(* *)
have "D < Field ?r'" unfolding Field_bsqr using SUB .
with OF obtain a1 and a2 where
- "(a1,a2) \<in> Field ?r'" and 1: "D = rel.underS ?r' (a1,a2)"
+ "(a1,a2) \<in> Field ?r'" and 1: "D = underS ?r' (a1,a2)"
using Well' wo_rel.ofilter_underS_Field[of ?r' D] by auto
hence 2: "{a1,a2} \<le> Field r" unfolding Field_bsqr by auto
let ?m = "wo_rel.max2 r a1 a2"
- have "D \<le> (rel.under r ?m) \<times> (rel.under r ?m)"
+ have "D \<le> (under r ?m) \<times> (under r ?m)"
proof(unfold 1)
{fix b1 b2
let ?n = "wo_rel.max2 r b1 b2"
- assume "(b1,b2) \<in> rel.underS ?r' (a1,a2)"
+ assume "(b1,b2) \<in> underS ?r' (a1,a2)"
hence 3: "((b1,b2),(a1,a2)) \<in> ?r'"
- unfolding rel.underS_def by blast
+ unfolding underS_def by blast
hence "(?n,?m) \<in> r" using WELL by (simp add: bsqr_max2)
moreover
{have "(b1,b2) \<in> Field ?r'" using 3 unfolding Field_def by auto
@@ -1607,13 +1607,13 @@
}
ultimately have "(b1,?m) \<in> r \<and> (b2,?m) \<in> r"
using Trans trans_def[of r] by blast
- hence "(b1,b2) \<in> (rel.under r ?m) \<times> (rel.under r ?m)" unfolding rel.under_def by simp}
- thus "rel.underS ?r' (a1,a2) \<le> (rel.under r ?m) \<times> (rel.under r ?m)" by auto
+ hence "(b1,b2) \<in> (under r ?m) \<times> (under r ?m)" unfolding under_def by simp}
+ thus "underS ?r' (a1,a2) \<le> (under r ?m) \<times> (under r ?m)" by auto
qed
- moreover have "wo_rel.ofilter r (rel.under r ?m)"
+ moreover have "wo_rel.ofilter r (under r ?m)"
using Well by (simp add: wo_rel.under_ofilter)
- moreover have "rel.under r ?m < Field r"
- using NE rel.under_Field[of r ?m] by blast
+ moreover have "under r ?m < Field r"
+ using NE under_Field[of r ?m] by blast
ultimately show ?thesis by blast
qed
--- a/src/HOL/Cardinals/Order_Relation_More.thy Thu Jan 16 18:52:50 2014 +0100
+++ b/src/HOL/Cardinals/Order_Relation_More.thy Thu Jan 16 20:52:54 2014 +0100
@@ -14,66 +14,63 @@
subsection {* The upper and lower bounds operators *}
-context rel
-begin
-
-lemma aboveS_subset_above: "aboveS a \<le> above a"
+lemma aboveS_subset_above: "aboveS r a \<le> above r a"
by(auto simp add: aboveS_def above_def)
-lemma AboveS_subset_Above: "AboveS A \<le> Above A"
+lemma AboveS_subset_Above: "AboveS r A \<le> Above r A"
by(auto simp add: AboveS_def Above_def)
-lemma UnderS_disjoint: "A Int (UnderS A) = {}"
+lemma UnderS_disjoint: "A Int (UnderS r A) = {}"
by(auto simp add: UnderS_def)
-lemma aboveS_notIn: "a \<notin> aboveS a"
+lemma aboveS_notIn: "a \<notin> aboveS r a"
by(auto simp add: aboveS_def)
-lemma Refl_above_in: "\<lbrakk>Refl r; a \<in> Field r\<rbrakk> \<Longrightarrow> a \<in> above a"
+lemma Refl_above_in: "\<lbrakk>Refl r; a \<in> Field r\<rbrakk> \<Longrightarrow> a \<in> above r a"
by(auto simp add: refl_on_def above_def)
-lemma in_Above_under: "a \<in> Field r \<Longrightarrow> a \<in> Above (under a)"
+lemma in_Above_under: "a \<in> Field r \<Longrightarrow> a \<in> Above r (under r a)"
by(auto simp add: Above_def under_def)
-lemma in_Under_above: "a \<in> Field r \<Longrightarrow> a \<in> Under (above a)"
+lemma in_Under_above: "a \<in> Field r \<Longrightarrow> a \<in> Under r (above r a)"
by(auto simp add: Under_def above_def)
-lemma in_UnderS_aboveS: "a \<in> Field r \<Longrightarrow> a \<in> UnderS (aboveS a)"
+lemma in_UnderS_aboveS: "a \<in> Field r \<Longrightarrow> a \<in> UnderS r (aboveS r a)"
by(auto simp add: UnderS_def aboveS_def)
-lemma UnderS_subset_Under: "UnderS A \<le> Under A"
+lemma UnderS_subset_Under: "UnderS r A \<le> Under r A"
by(auto simp add: UnderS_def Under_def)
-lemma subset_Above_Under: "B \<le> Field r \<Longrightarrow> B \<le> Above (Under B)"
+lemma subset_Above_Under: "B \<le> Field r \<Longrightarrow> B \<le> Above r (Under r B)"
by(auto simp add: Above_def Under_def)
-lemma subset_Under_Above: "B \<le> Field r \<Longrightarrow> B \<le> Under (Above B)"
+lemma subset_Under_Above: "B \<le> Field r \<Longrightarrow> B \<le> Under r (Above r B)"
by(auto simp add: Under_def Above_def)
-lemma subset_AboveS_UnderS: "B \<le> Field r \<Longrightarrow> B \<le> AboveS (UnderS B)"
+lemma subset_AboveS_UnderS: "B \<le> Field r \<Longrightarrow> B \<le> AboveS r (UnderS r B)"
by(auto simp add: AboveS_def UnderS_def)
-lemma subset_UnderS_AboveS: "B \<le> Field r \<Longrightarrow> B \<le> UnderS (AboveS B)"
+lemma subset_UnderS_AboveS: "B \<le> Field r \<Longrightarrow> B \<le> UnderS r (AboveS r B)"
by(auto simp add: UnderS_def AboveS_def)
lemma Under_Above_Galois:
-"\<lbrakk>B \<le> Field r; C \<le> Field r\<rbrakk> \<Longrightarrow> (B \<le> Above C) = (C \<le> Under B)"
+"\<lbrakk>B \<le> Field r; C \<le> Field r\<rbrakk> \<Longrightarrow> (B \<le> Above r C) = (C \<le> Under r B)"
by(unfold Above_def Under_def, blast)
lemma UnderS_AboveS_Galois:
-"\<lbrakk>B \<le> Field r; C \<le> Field r\<rbrakk> \<Longrightarrow> (B \<le> AboveS C) = (C \<le> UnderS B)"
+"\<lbrakk>B \<le> Field r; C \<le> Field r\<rbrakk> \<Longrightarrow> (B \<le> AboveS r C) = (C \<le> UnderS r B)"
by(unfold AboveS_def UnderS_def, blast)
lemma Refl_above_aboveS:
-assumes REFL: "Refl r" and IN: "a \<in> Field r"
-shows "above a = aboveS a \<union> {a}"
+ assumes REFL: "Refl r" and IN: "a \<in> Field r"
+ shows "above r a = aboveS r a \<union> {a}"
proof(unfold above_def aboveS_def, auto)
show "(a,a) \<in> r" using REFL IN refl_on_def[of _ r] by blast
qed
lemma Linear_order_under_aboveS_Field:
-assumes LIN: "Linear_order r" and IN: "a \<in> Field r"
-shows "Field r = under a \<union> aboveS a"
+ assumes LIN: "Linear_order r" and IN: "a \<in> Field r"
+ shows "Field r = under r a \<union> aboveS r a"
proof(unfold under_def aboveS_def, auto)
assume "a \<in> Field r" "(a, a) \<notin> r"
with LIN IN order_on_defs[of _ r] refl_on_def[of _ r]
@@ -96,7 +93,7 @@
lemma Linear_order_underS_above_Field:
assumes LIN: "Linear_order r" and IN: "a \<in> Field r"
-shows "Field r = underS a \<union> above a"
+shows "Field r = underS r a \<union> above r a"
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]
@@ -117,155 +114,155 @@
using LIN order_on_defs[of "Field r" r] refl_on_def[of "Field r" r] by blast
qed
-lemma under_empty: "a \<notin> Field r \<Longrightarrow> under a = {}"
+lemma under_empty: "a \<notin> Field r \<Longrightarrow> under r a = {}"
unfolding Field_def under_def by auto
-lemma Under_Field: "Under A \<le> Field r"
+lemma Under_Field: "Under r A \<le> Field r"
by(unfold Under_def Field_def, auto)
-lemma UnderS_Field: "UnderS A \<le> Field r"
+lemma UnderS_Field: "UnderS r A \<le> Field r"
by(unfold UnderS_def Field_def, auto)
-lemma above_Field: "above a \<le> Field r"
+lemma above_Field: "above r a \<le> Field r"
by(unfold above_def Field_def, auto)
-lemma aboveS_Field: "aboveS a \<le> Field r"
+lemma aboveS_Field: "aboveS r a \<le> Field r"
by(unfold aboveS_def Field_def, auto)
-lemma Above_Field: "Above A \<le> Field r"
+lemma Above_Field: "Above r A \<le> Field r"
by(unfold Above_def Field_def, auto)
lemma Refl_under_Under:
assumes REFL: "Refl r" and NE: "A \<noteq> {}"
-shows "Under A = (\<Inter> a \<in> A. under a)"
+shows "Under r A = (\<Inter> a \<in> A. under r a)"
proof
- show "Under A \<subseteq> (\<Inter> a \<in> A. under a)"
+ show "Under r A \<subseteq> (\<Inter> a \<in> A. under r a)"
by(unfold Under_def under_def, auto)
next
- show "(\<Inter> a \<in> A. under a) \<subseteq> Under A"
+ show "(\<Inter> a \<in> A. under r a) \<subseteq> Under r A"
proof(auto)
fix x
- assume *: "\<forall>xa \<in> A. x \<in> under xa"
+ assume *: "\<forall>xa \<in> A. x \<in> under r xa"
hence "\<forall>xa \<in> A. (x,xa) \<in> r"
by (simp add: under_def)
moreover
{from NE obtain a where "a \<in> A" by blast
- with * have "x \<in> under a" by simp
+ with * have "x \<in> under r a" by simp
hence "x \<in> Field r"
- using under_Field[of a] by auto
+ using under_Field[of r a] by auto
}
- ultimately show "x \<in> Under A"
+ ultimately show "x \<in> Under r A"
unfolding Under_def by auto
qed
qed
lemma Refl_underS_UnderS:
assumes REFL: "Refl r" and NE: "A \<noteq> {}"
-shows "UnderS A = (\<Inter> a \<in> A. underS a)"
+shows "UnderS r A = (\<Inter> a \<in> A. underS r a)"
proof
- show "UnderS A \<subseteq> (\<Inter> a \<in> A. underS a)"
+ show "UnderS r A \<subseteq> (\<Inter> a \<in> A. underS r a)"
by(unfold UnderS_def underS_def, auto)
next
- show "(\<Inter> a \<in> A. underS a) \<subseteq> UnderS A"
+ show "(\<Inter> a \<in> A. underS r a) \<subseteq> UnderS r A"
proof(auto)
fix x
- assume *: "\<forall>xa \<in> A. x \<in> underS xa"
+ assume *: "\<forall>xa \<in> A. x \<in> underS r xa"
hence "\<forall>xa \<in> A. x \<noteq> xa \<and> (x,xa) \<in> r"
by (auto simp add: underS_def)
moreover
{from NE obtain a where "a \<in> A" by blast
- with * have "x \<in> underS a" by simp
+ with * have "x \<in> underS r a" by simp
hence "x \<in> Field r"
- using underS_Field[of a] by auto
+ using underS_Field[of r a] by auto
}
- ultimately show "x \<in> UnderS A"
+ ultimately show "x \<in> UnderS r A"
unfolding UnderS_def by auto
qed
qed
lemma Refl_above_Above:
assumes REFL: "Refl r" and NE: "A \<noteq> {}"
-shows "Above A = (\<Inter> a \<in> A. above a)"
+shows "Above r A = (\<Inter> a \<in> A. above r a)"
proof
- show "Above A \<subseteq> (\<Inter> a \<in> A. above a)"
+ show "Above r A \<subseteq> (\<Inter> a \<in> A. above r a)"
by(unfold Above_def above_def, auto)
next
- show "(\<Inter> a \<in> A. above a) \<subseteq> Above A"
+ show "(\<Inter> a \<in> A. above r a) \<subseteq> Above r A"
proof(auto)
fix x
- assume *: "\<forall>xa \<in> A. x \<in> above xa"
+ assume *: "\<forall>xa \<in> A. x \<in> above r xa"
hence "\<forall>xa \<in> A. (xa,x) \<in> r"
by (simp add: above_def)
moreover
{from NE obtain a where "a \<in> A" by blast
- with * have "x \<in> above a" by simp
+ with * have "x \<in> above r a" by simp
hence "x \<in> Field r"
- using above_Field[of a] by auto
+ using above_Field[of r a] by auto
}
- ultimately show "x \<in> Above A"
+ ultimately show "x \<in> Above r A"
unfolding Above_def by auto
qed
qed
lemma Refl_aboveS_AboveS:
assumes REFL: "Refl r" and NE: "A \<noteq> {}"
-shows "AboveS A = (\<Inter> a \<in> A. aboveS a)"
+shows "AboveS r A = (\<Inter> a \<in> A. aboveS r a)"
proof
- show "AboveS A \<subseteq> (\<Inter> a \<in> A. aboveS a)"
+ show "AboveS r A \<subseteq> (\<Inter> a \<in> A. aboveS r a)"
by(unfold AboveS_def aboveS_def, auto)
next
- show "(\<Inter> a \<in> A. aboveS a) \<subseteq> AboveS A"
+ show "(\<Inter> a \<in> A. aboveS r a) \<subseteq> AboveS r A"
proof(auto)
fix x
- assume *: "\<forall>xa \<in> A. x \<in> aboveS xa"
+ assume *: "\<forall>xa \<in> A. x \<in> aboveS r xa"
hence "\<forall>xa \<in> A. xa \<noteq> x \<and> (xa,x) \<in> r"
by (auto simp add: aboveS_def)
moreover
{from NE obtain a where "a \<in> A" by blast
- with * have "x \<in> aboveS a" by simp
+ with * have "x \<in> aboveS r a" by simp
hence "x \<in> Field r"
- using aboveS_Field[of a] by auto
+ using aboveS_Field[of r a] by auto
}
- ultimately show "x \<in> AboveS A"
+ ultimately show "x \<in> AboveS r A"
unfolding AboveS_def by auto
qed
qed
-lemma under_Under_singl: "under a = Under {a}"
+lemma under_Under_singl: "under r a = Under r {a}"
by(unfold Under_def under_def, auto simp add: Field_def)
-lemma underS_UnderS_singl: "underS a = UnderS {a}"
+lemma underS_UnderS_singl: "underS r a = UnderS r {a}"
by(unfold UnderS_def underS_def, auto simp add: Field_def)
-lemma above_Above_singl: "above a = Above {a}"
+lemma above_Above_singl: "above r a = Above r {a}"
by(unfold Above_def above_def, auto simp add: Field_def)
-lemma aboveS_AboveS_singl: "aboveS a = AboveS {a}"
+lemma aboveS_AboveS_singl: "aboveS r a = AboveS r {a}"
by(unfold AboveS_def aboveS_def, auto simp add: Field_def)
-lemma Under_decr: "A \<le> B \<Longrightarrow> Under B \<le> Under A"
+lemma Under_decr: "A \<le> B \<Longrightarrow> Under r B \<le> Under r A"
by(unfold Under_def, auto)
-lemma UnderS_decr: "A \<le> B \<Longrightarrow> UnderS B \<le> UnderS A"
+lemma UnderS_decr: "A \<le> B \<Longrightarrow> UnderS r B \<le> UnderS r A"
by(unfold UnderS_def, auto)
-lemma Above_decr: "A \<le> B \<Longrightarrow> Above B \<le> Above A"
+lemma Above_decr: "A \<le> B \<Longrightarrow> Above r B \<le> Above r A"
by(unfold Above_def, auto)
-lemma AboveS_decr: "A \<le> B \<Longrightarrow> AboveS B \<le> AboveS A"
+lemma AboveS_decr: "A \<le> B \<Longrightarrow> AboveS r B \<le> AboveS r A"
by(unfold AboveS_def, auto)
lemma under_incl_iff:
assumes TRANS: "trans r" and REFL: "Refl r" and IN: "a \<in> Field r"
-shows "(under a \<le> under b) = ((a,b) \<in> r)"
+shows "(under r a \<le> under r b) = ((a,b) \<in> r)"
proof
assume "(a,b) \<in> r"
- thus "under a \<le> under b" using TRANS
+ thus "under r a \<le> under r b" using TRANS
by (auto simp add: under_incr)
next
- assume "under a \<le> under b"
+ assume "under r a \<le> under r b"
moreover
- have "a \<in> under a" using REFL IN
+ have "a \<in> under r a" using REFL IN
by (auto simp add: Refl_under_in)
ultimately show "(a,b) \<in> r"
by (auto simp add: under_def)
@@ -273,7 +270,7 @@
lemma above_decr:
assumes TRANS: "trans r" and REL: "(a,b) \<in> r"
-shows "above b \<le> above a"
+shows "above r b \<le> above r a"
proof(unfold above_def, auto)
fix x assume "(b,x) \<in> r"
with REL TRANS trans_def[of r]
@@ -283,7 +280,7 @@
lemma aboveS_decr:
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
REL: "(a,b) \<in> r"
-shows "aboveS b \<le> aboveS a"
+shows "aboveS r b \<le> aboveS r a"
proof(unfold aboveS_def, auto)
assume *: "a \<noteq> b" and **: "(b,a) \<in> r"
with ANTISYM antisym_def[of r] REL
@@ -296,11 +293,11 @@
lemma under_trans:
assumes TRANS: "trans r" and
- IN1: "a \<in> under b" and IN2: "b \<in> under c"
-shows "a \<in> under c"
+ IN1: "a \<in> under r b" and IN2: "b \<in> under r c"
+shows "a \<in> under r c"
proof-
have "(a,b) \<in> r \<and> (b,c) \<in> r"
- using IN1 IN2 under_def by auto
+ using IN1 IN2 under_def by fastforce
hence "(a,c) \<in> r"
using TRANS trans_def[of r] by blast
thus ?thesis unfolding under_def by simp
@@ -308,14 +305,14 @@
lemma under_underS_trans:
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
- IN1: "a \<in> under b" and IN2: "b \<in> underS c"
-shows "a \<in> underS c"
+ IN1: "a \<in> under r b" and IN2: "b \<in> underS r c"
+shows "a \<in> underS r c"
proof-
have 0: "(a,b) \<in> r \<and> (b,c) \<in> r"
- using IN1 IN2 under_def underS_def by auto
+ using IN1 IN2 under_def underS_def by fastforce
hence 1: "(a,c) \<in> r"
using TRANS trans_def[of r] by blast
- have 2: "b \<noteq> c" using IN2 underS_def by auto
+ have 2: "b \<noteq> c" using IN2 underS_def by force
have 3: "a \<noteq> c"
proof
assume "a = c" with 0 2 ANTISYM antisym_def[of r]
@@ -326,14 +323,14 @@
lemma underS_under_trans:
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
- IN1: "a \<in> underS b" and IN2: "b \<in> under c"
-shows "a \<in> underS c"
+ IN1: "a \<in> underS r b" and IN2: "b \<in> under r c"
+shows "a \<in> underS r c"
proof-
have 0: "(a,b) \<in> r \<and> (b,c) \<in> r"
- using IN1 IN2 under_def underS_def by auto
+ using IN1 IN2 under_def underS_def by fast
hence 1: "(a,c) \<in> r"
- using TRANS trans_def[of r] by blast
- have 2: "a \<noteq> b" using IN1 underS_def by auto
+ using TRANS trans_def[of r] by fast
+ have 2: "a \<noteq> b" using IN1 underS_def by force
have 3: "a \<noteq> c"
proof
assume "a = c" with 0 2 ANTISYM antisym_def[of r]
@@ -344,21 +341,21 @@
lemma underS_underS_trans:
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
- IN1: "a \<in> underS b" and IN2: "b \<in> underS c"
-shows "a \<in> underS c"
+ IN1: "a \<in> underS r b" and IN2: "b \<in> underS r c"
+shows "a \<in> underS r c"
proof-
- have "a \<in> under b"
- using IN1 underS_subset_under by auto
- with assms under_underS_trans show ?thesis by auto
+ have "a \<in> under r b"
+ using IN1 underS_subset_under by fast
+ with assms under_underS_trans show ?thesis by fast
qed
lemma above_trans:
assumes TRANS: "trans r" and
- IN1: "b \<in> above a" and IN2: "c \<in> above b"
-shows "c \<in> above a"
+ IN1: "b \<in> above r a" and IN2: "c \<in> above r b"
+shows "c \<in> above r a"
proof-
have "(a,b) \<in> r \<and> (b,c) \<in> r"
- using IN1 IN2 above_def by auto
+ using IN1 IN2 above_def by fast
hence "(a,c) \<in> r"
using TRANS trans_def[of r] by blast
thus ?thesis unfolding above_def by simp
@@ -366,14 +363,14 @@
lemma above_aboveS_trans:
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
- IN1: "b \<in> above a" and IN2: "c \<in> aboveS b"
-shows "c \<in> aboveS a"
+ IN1: "b \<in> above r a" and IN2: "c \<in> aboveS r b"
+shows "c \<in> aboveS r a"
proof-
have 0: "(a,b) \<in> r \<and> (b,c) \<in> r"
- using IN1 IN2 above_def aboveS_def by auto
+ using IN1 IN2 above_def aboveS_def by fast
hence 1: "(a,c) \<in> r"
using TRANS trans_def[of r] by blast
- have 2: "b \<noteq> c" using IN2 aboveS_def by auto
+ have 2: "b \<noteq> c" using IN2 aboveS_def by force
have 3: "a \<noteq> c"
proof
assume "a = c" with 0 2 ANTISYM antisym_def[of r]
@@ -384,14 +381,14 @@
lemma aboveS_above_trans:
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
- IN1: "b \<in> aboveS a" and IN2: "c \<in> above b"
-shows "c \<in> aboveS a"
+ IN1: "b \<in> aboveS r a" and IN2: "c \<in> above r b"
+shows "c \<in> aboveS r a"
proof-
have 0: "(a,b) \<in> r \<and> (b,c) \<in> r"
- using IN1 IN2 above_def aboveS_def by auto
+ using IN1 IN2 above_def aboveS_def by fast
hence 1: "(a,c) \<in> r"
using TRANS trans_def[of r] by blast
- have 2: "a \<noteq> b" using IN1 aboveS_def by auto
+ have 2: "a \<noteq> b" using IN1 aboveS_def by force
have 3: "a \<noteq> c"
proof
assume "a = c" with 0 2 ANTISYM antisym_def[of r]
@@ -402,21 +399,23 @@
lemma aboveS_aboveS_trans:
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
- IN1: "b \<in> aboveS a" and IN2: "c \<in> aboveS b"
-shows "c \<in> aboveS a"
+ IN1: "b \<in> aboveS r a" and IN2: "c \<in> aboveS r b"
+shows "c \<in> aboveS r a"
proof-
- have "b \<in> above a"
- using IN1 aboveS_subset_above by auto
- with assms above_aboveS_trans show ?thesis by auto
+ have "b \<in> above r a"
+ using IN1 aboveS_subset_above by fast
+ with assms above_aboveS_trans show ?thesis by fast
qed
lemma under_Under_trans:
assumes TRANS: "trans r" and
- IN1: "a \<in> under b" and IN2: "b \<in> Under C"
-shows "a \<in> Under C"
+ IN1: "a \<in> under r b" and IN2: "b \<in> Under r C"
+shows "a \<in> Under r C"
proof-
- have "(a,b) \<in> r \<and> (\<forall>c \<in> C. (b,c) \<in> r)"
- using IN1 IN2 under_def Under_def by blast
+ have "b \<in> {u \<in> Field r. \<forall>x. x \<in> C \<longrightarrow> (u, x) \<in> r}"
+ using IN2 Under_def by force
+ hence "(a,b) \<in> r \<and> (\<forall>c \<in> C. (b,c) \<in> r)"
+ using IN1 under_def by fast
hence "\<forall>c \<in> C. (a,c) \<in> r"
using TRANS trans_def[of r] by blast
moreover
@@ -427,22 +426,22 @@
lemma underS_Under_trans:
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
- IN1: "a \<in> underS b" and IN2: "b \<in> Under C"
-shows "a \<in> UnderS C"
+ IN1: "a \<in> underS r b" and IN2: "b \<in> Under r C"
+shows "a \<in> UnderS r C"
proof-
- from IN1 have "a \<in> under b"
- using underS_subset_under[of b] by blast
+ from IN1 have "a \<in> under r b"
+ using underS_subset_under[of r b] by fast
with assms under_Under_trans
- have "a \<in> Under C" by auto
+ have "a \<in> Under r C" by fast
(* *)
moreover
have "a \<notin> C"
proof
assume *: "a \<in> C"
have 1: "b \<noteq> a \<and> (a,b) \<in> r"
- using IN1 underS_def[of b] by auto
+ using IN1 underS_def[of r b] by auto
have "\<forall>c \<in> C. (b,c) \<in> r"
- using IN2 Under_def[of C] by auto
+ using IN2 Under_def[of r C] by auto
with * have "(b,a) \<in> r" by simp
with 1 ANTISYM antisym_def[of r]
show False by blast
@@ -450,53 +449,53 @@
(* *)
ultimately
show ?thesis unfolding UnderS_def
- using Under_def by auto
+ using Under_def by force
qed
lemma underS_UnderS_trans:
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
- IN1: "a \<in> underS b" and IN2: "b \<in> UnderS C"
-shows "a \<in> UnderS C"
+ IN1: "a \<in> underS r b" and IN2: "b \<in> UnderS r C"
+shows "a \<in> UnderS r C"
proof-
- from IN2 have "b \<in> Under C"
- using UnderS_subset_Under[of C] by blast
+ from IN2 have "b \<in> Under r C"
+ using UnderS_subset_Under[of r C] by blast
with underS_Under_trans assms
- show ?thesis by auto
+ show ?thesis by force
qed
lemma above_Above_trans:
assumes TRANS: "trans r" and
- IN1: "a \<in> above b" and IN2: "b \<in> Above C"
-shows "a \<in> Above C"
+ IN1: "a \<in> above r b" and IN2: "b \<in> Above r C"
+shows "a \<in> Above r C"
proof-
have "(b,a) \<in> r \<and> (\<forall>c \<in> C. (c,b) \<in> r)"
- using IN1 IN2 above_def Above_def by auto
+ using IN1[unfolded above_def] IN2[unfolded Above_def] by simp
hence "\<forall>c \<in> C. (c,a) \<in> r"
using TRANS trans_def[of r] by blast
moreover
- have "a \<in> Field r" using IN1 Field_def above_def by force
+ have "a \<in> Field r" using IN1[unfolded above_def] Field_def by fast
ultimately
show ?thesis unfolding Above_def by auto
qed
lemma aboveS_Above_trans:
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
- IN1: "a \<in> aboveS b" and IN2: "b \<in> Above C"
-shows "a \<in> AboveS C"
+ IN1: "a \<in> aboveS r b" and IN2: "b \<in> Above r C"
+shows "a \<in> AboveS r C"
proof-
- from IN1 have "a \<in> above b"
- using aboveS_subset_above[of b] by blast
+ from IN1 have "a \<in> above r b"
+ using aboveS_subset_above[of r b] by blast
with assms above_Above_trans
- have "a \<in> Above C" by auto
+ have "a \<in> Above r C" by fast
(* *)
moreover
have "a \<notin> C"
proof
assume *: "a \<in> C"
have 1: "b \<noteq> a \<and> (b,a) \<in> r"
- using IN1 aboveS_def[of b] by auto
+ using IN1 aboveS_def[of r b] by auto
have "\<forall>c \<in> C. (c,b) \<in> r"
- using IN2 Above_def[of C] by auto
+ using IN2 Above_def[of r C] by auto
with * have "(a,b) \<in> r" by simp
with 1 ANTISYM antisym_def[of r]
show False by blast
@@ -504,27 +503,27 @@
(* *)
ultimately
show ?thesis unfolding AboveS_def
- using Above_def by auto
+ using Above_def by force
qed
lemma above_AboveS_trans:
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
- IN1: "a \<in> above b" and IN2: "b \<in> AboveS C"
-shows "a \<in> AboveS C"
+ IN1: "a \<in> above r b" and IN2: "b \<in> AboveS r C"
+shows "a \<in> AboveS r C"
proof-
- from IN2 have "b \<in> Above C"
- using AboveS_subset_Above[of C] by blast
+ from IN2 have "b \<in> Above r C"
+ using AboveS_subset_Above[of r C] by blast
with assms above_Above_trans
- have "a \<in> Above C" by auto
+ have "a \<in> Above r C" by force
(* *)
moreover
have "a \<notin> C"
proof
assume *: "a \<in> C"
have 1: "(b,a) \<in> r"
- using IN1 above_def[of b] by auto
+ using IN1 above_def[of r b] by auto
have "\<forall>c \<in> C. b \<noteq> c \<and> (c,b) \<in> r"
- using IN2 AboveS_def[of C] by auto
+ using IN2 AboveS_def[of r C] by auto
with * have "b \<noteq> a \<and> (a,b) \<in> r" by simp
with 1 ANTISYM antisym_def[of r]
show False by blast
@@ -532,38 +531,38 @@
(* *)
ultimately
show ?thesis unfolding AboveS_def
- using Above_def by auto
+ using Above_def by force
qed
lemma aboveS_AboveS_trans:
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
- IN1: "a \<in> aboveS b" and IN2: "b \<in> AboveS C"
-shows "a \<in> AboveS C"
+ IN1: "a \<in> aboveS r b" and IN2: "b \<in> AboveS r C"
+shows "a \<in> AboveS r C"
proof-
- from IN2 have "b \<in> Above C"
- using AboveS_subset_Above[of C] by blast
+ from IN2 have "b \<in> Above r C"
+ using AboveS_subset_Above[of r C] by blast
with aboveS_Above_trans assms
- show ?thesis by auto
+ show ?thesis by force
qed
lemma under_UnderS_trans:
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
- IN1: "a \<in> under b" and IN2: "b \<in> UnderS C"
-shows "a \<in> UnderS C"
+ IN1: "a \<in> under r b" and IN2: "b \<in> UnderS r C"
+shows "a \<in> UnderS r C"
proof-
- from IN2 have "b \<in> Under C"
- using UnderS_subset_Under[of C] by blast
+ from IN2 have "b \<in> Under r C"
+ using UnderS_subset_Under[of r C] by blast
with assms under_Under_trans
- have "a \<in> Under C" by blast
+ have "a \<in> Under r C" by force
(* *)
moreover
have "a \<notin> C"
proof
assume *: "a \<in> C"
have 1: "(a,b) \<in> r"
- using IN1 under_def[of b] by auto
+ using IN1 under_def[of r b] by auto
have "\<forall>c \<in> C. b \<noteq> c \<and> (b,c) \<in> r"
- using IN2 UnderS_def[of C] by blast
+ using IN2 UnderS_def[of r C] by blast
with * have "b \<noteq> a \<and> (b,a) \<in> r" by blast
with 1 ANTISYM antisym_def[of r]
show False by blast
@@ -573,66 +572,59 @@
show ?thesis unfolding UnderS_def Under_def by fast
qed
-end (* context rel *)
-
subsection {* Properties depending on more than one relation *}
-abbreviation "under \<equiv> rel.under"
-abbreviation "underS \<equiv> rel.underS"
-abbreviation "Under \<equiv> rel.Under"
-abbreviation "UnderS \<equiv> rel.UnderS"
-abbreviation "above \<equiv> rel.above"
-abbreviation "aboveS \<equiv> rel.aboveS"
-abbreviation "Above \<equiv> rel.Above"
-abbreviation "AboveS \<equiv> rel.AboveS"
-
lemma under_incr2:
"r \<le> r' \<Longrightarrow> under r a \<le> under r' a"
-unfolding rel.under_def by blast
+unfolding under_def by blast
lemma underS_incr2:
"r \<le> r' \<Longrightarrow> underS r a \<le> underS r' a"
-unfolding rel.underS_def by blast
+unfolding underS_def by blast
+(* FIXME: r \<leadsto> r'
lemma Under_incr:
"r \<le> r' \<Longrightarrow> Under r A \<le> Under r A"
-unfolding rel.Under_def by blast
+unfolding Under_def by blast
lemma UnderS_incr:
"r \<le> r' \<Longrightarrow> UnderS r A \<le> UnderS r A"
-unfolding rel.UnderS_def by blast
+unfolding UnderS_def by blast
lemma Under_incr_decr:
"\<lbrakk>r \<le> r'; A' \<le> A\<rbrakk> \<Longrightarrow> Under r A \<le> Under r A'"
-unfolding rel.Under_def by blast
+unfolding Under_def by blast
lemma UnderS_incr_decr:
"\<lbrakk>r \<le> r'; A' \<le> A\<rbrakk> \<Longrightarrow> UnderS r A \<le> UnderS r A'"
-unfolding rel.UnderS_def by blast
+unfolding UnderS_def by blast
+*)
lemma above_incr2:
"r \<le> r' \<Longrightarrow> above r a \<le> above r' a"
-unfolding rel.above_def by blast
+unfolding above_def by blast
lemma aboveS_incr2:
"r \<le> r' \<Longrightarrow> aboveS r a \<le> aboveS r' a"
-unfolding rel.aboveS_def by blast
+unfolding aboveS_def by blast
+(* FIXME
lemma Above_incr:
"r \<le> r' \<Longrightarrow> Above r A \<le> Above r A"
-unfolding rel.Above_def by blast
+unfolding Above_def by blast
lemma AboveS_incr:
"r \<le> r' \<Longrightarrow> AboveS r A \<le> AboveS r A"
-unfolding rel.AboveS_def by blast
+unfolding AboveS_def by blast
lemma Above_incr_decr:
-"\<lbrakk>r \<le> r'; A' \<le> A\<rbrakk> \<Longrightarrow> Above r A \<le> Above r A'"
-unfolding rel.Above_def by blast
+"\<lbrakk>r \<le> r'; A' \<le> A\<rbrakk> \<Longrightarrow> Above r A \<le> Above r A'"
+unfolding Above_def by blast
lemma AboveS_incr_decr:
-"\<lbrakk>r \<le> r'; A' \<le> A\<rbrakk> \<Longrightarrow> AboveS r A \<le> AboveS r A'"
-unfolding rel.AboveS_def by blast
+"\<lbrakk>r \<le> r'; A' \<le> A\<rbrakk> \<Longrightarrow> AboveS r A \<le> AboveS r A'"
+unfolding AboveS_def by blast
+*)
end
--- a/src/HOL/Cardinals/Order_Relation_More_FP.thy Thu Jan 16 18:52:50 2014 +0100
+++ b/src/HOL/Cardinals/Order_Relation_More_FP.thy Thu Jan 16 20:52:54 2014 +0100
@@ -19,16 +19,6 @@
further define upper and lower bounds operators. *}
-locale rel = fixes r :: "'a rel"
-
-text{* The following context encompasses all this section, except
-for its last subsection. In other words, for the rest of this section except its last
-subsection, we consider a fixed relation @{text "r"}. *}
-
-context rel
-begin
-
-
subsection {* Auxiliaries *}
@@ -39,7 +29,7 @@
corollary well_order_on_domain:
"\<lbrakk>well_order_on A r; (a,b) \<in> r\<rbrakk> \<Longrightarrow> a \<in> A \<and> b \<in> A"
-by(simp add: refl_on_domain order_on_defs)
+by (auto simp add: refl_on_domain order_on_defs)
lemma well_order_on_Field:
@@ -49,7 +39,7 @@
lemma well_order_on_Well_order:
"well_order_on A r \<Longrightarrow> A = Field r \<and> Well_order r"
-using well_order_on_Field by simp
+using well_order_on_Field by auto
lemma Total_subset_Id:
@@ -91,103 +81,91 @@
Capitalization of the first letter in the name reminds that the operator acts on sets, rather
than on individual elements. *}
-definition under::"'a \<Rightarrow> 'a set"
-where "under a \<equiv> {b. (b,a) \<in> r}"
+definition under::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
+where "under r a \<equiv> {b. (b,a) \<in> r}"
-definition underS::"'a \<Rightarrow> 'a set"
-where "underS a \<equiv> {b. b \<noteq> a \<and> (b,a) \<in> r}"
+definition underS::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
+where "underS r a \<equiv> {b. b \<noteq> a \<and> (b,a) \<in> r}"
-definition Under::"'a set \<Rightarrow> 'a set"
-where "Under A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (b,a) \<in> r}"
+definition Under::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
+where "Under r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (b,a) \<in> r}"
-definition UnderS::"'a set \<Rightarrow> 'a set"
-where "UnderS A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (b,a) \<in> r}"
+definition UnderS::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
+where "UnderS r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (b,a) \<in> r}"
-definition above::"'a \<Rightarrow> 'a set"
-where "above a \<equiv> {b. (a,b) \<in> r}"
+definition above::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
+where "above r a \<equiv> {b. (a,b) \<in> r}"
-definition aboveS::"'a \<Rightarrow> 'a set"
-where "aboveS a \<equiv> {b. b \<noteq> a \<and> (a,b) \<in> r}"
+definition aboveS::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
+where "aboveS r a \<equiv> {b. b \<noteq> a \<and> (a,b) \<in> r}"
-definition Above::"'a set \<Rightarrow> 'a set"
-where "Above A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (a,b) \<in> r}"
+definition Above::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
+where "Above r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (a,b) \<in> r}"
-definition AboveS::"'a set \<Rightarrow> 'a set"
-where "AboveS A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (a,b) \<in> r}"
-(* *)
+definition AboveS::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
+where "AboveS r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (a,b) \<in> r}"
text{* Note: In the definitions of @{text "Above[S]"} and @{text "Under[S]"},
we bounded comprehension by @{text "Field r"} in order to properly cover
the case of @{text "A"} being empty. *}
-
-lemma underS_subset_under: "underS a \<le> under a"
+lemma underS_subset_under: "underS r a \<le> under r a"
by(auto simp add: underS_def under_def)
-lemma underS_notIn: "a \<notin> underS a"
+lemma underS_notIn: "a \<notin> underS r a"
by(simp add: underS_def)
-lemma Refl_under_in: "\<lbrakk>Refl r; a \<in> Field r\<rbrakk> \<Longrightarrow> a \<in> under a"
+lemma Refl_under_in: "\<lbrakk>Refl r; a \<in> Field r\<rbrakk> \<Longrightarrow> a \<in> under r a"
by(simp add: refl_on_def under_def)
-lemma AboveS_disjoint: "A Int (AboveS A) = {}"
+lemma AboveS_disjoint: "A Int (AboveS r A) = {}"
by(auto simp add: AboveS_def)
-
-lemma in_AboveS_underS: "a \<in> Field r \<Longrightarrow> a \<in> AboveS (underS a)"
+lemma in_AboveS_underS: "a \<in> Field r \<Longrightarrow> a \<in> AboveS r (underS r a)"
by(auto simp add: AboveS_def underS_def)
-
lemma Refl_under_underS:
-assumes "Refl r" "a \<in> Field r"
-shows "under a = underS a \<union> {a}"
+ assumes "Refl r" "a \<in> Field r"
+ shows "under r a = underS r a \<union> {a}"
unfolding under_def underS_def
using assms refl_on_def[of _ r] by fastforce
-
-lemma underS_empty: "a \<notin> Field r \<Longrightarrow> underS a = {}"
+lemma underS_empty: "a \<notin> Field r \<Longrightarrow> underS r a = {}"
by (auto simp: Field_def underS_def)
-
-lemma under_Field: "under a \<le> Field r"
+lemma under_Field: "under r a \<le> Field r"
by(unfold under_def Field_def, auto)
-
-lemma underS_Field: "underS a \<le> Field r"
+lemma underS_Field: "underS r a \<le> Field r"
by(unfold underS_def Field_def, auto)
-
lemma underS_Field2:
-"a \<in> Field r \<Longrightarrow> underS a < Field r"
-using assms underS_notIn underS_Field by blast
-
+"a \<in> Field r \<Longrightarrow> underS r a < Field r"
+using underS_notIn underS_Field by fast
lemma underS_Field3:
-"Field r \<noteq> {} \<Longrightarrow> underS a < Field r"
+"Field r \<noteq> {} \<Longrightarrow> underS r a < Field r"
by(cases "a \<in> Field r", simp add: underS_Field2, auto simp add: underS_empty)
-
-lemma AboveS_Field: "AboveS A \<le> Field r"
+lemma AboveS_Field: "AboveS r A \<le> Field r"
by(unfold AboveS_def Field_def, auto)
-
lemma under_incr:
-assumes TRANS: "trans r" and REL: "(a,b) \<in> r"
-shows "under a \<le> under b"
+ assumes TRANS: "trans r" and REL: "(a,b) \<in> r"
+ shows "under r a \<le> under r b"
proof(unfold under_def, auto)
fix x assume "(x,a) \<in> r"
with REL TRANS trans_def[of r]
show "(x,b) \<in> r" by blast
qed
-
lemma underS_incr:
assumes TRANS: "trans r" and ANTISYM: "antisym r" and
REL: "(a,b) \<in> r"
-shows "underS a \<le> underS b"
+shows "underS r a \<le> underS r b"
proof(unfold underS_def, auto)
assume *: "b \<noteq> a" and **: "(b,a) \<in> r"
with ANTISYM antisym_def[of r] REL
@@ -198,25 +176,24 @@
show "(x,b) \<in> r" by blast
qed
-
lemma underS_incl_iff:
assumes LO: "Linear_order r" and
INa: "a \<in> Field r" and INb: "b \<in> Field r"
-shows "(underS a \<le> underS b) = ((a,b) \<in> r)"
+shows "(underS r a \<le> underS r b) = ((a,b) \<in> r)"
proof
assume "(a,b) \<in> r"
- thus "underS a \<le> underS b" using LO
+ thus "underS r a \<le> underS r b" using LO
by (simp add: order_on_defs underS_incr)
next
- assume *: "underS a \<le> underS b"
+ assume *: "underS r a \<le> underS r b"
{assume "a = b"
hence "(a,b) \<in> r" using assms
by (simp add: order_on_defs refl_on_def)
}
moreover
{assume "a \<noteq> b \<and> (b,a) \<in> r"
- hence "b \<in> underS a" unfolding underS_def by blast
- hence "b \<in> underS b" using * by blast
+ hence "b \<in> underS r a" unfolding underS_def by blast
+ hence "b \<in> underS r b" using * by blast
hence False by (simp add: underS_notIn)
}
ultimately
@@ -224,7 +201,4 @@
order_on_defs[of "Field r" r] total_on_def[of "Field r" r] by blast
qed
-
-end (* context rel *)
-
end
--- a/src/HOL/Cardinals/Ordinal_Arithmetic.thy Thu Jan 16 18:52:50 2014 +0100
+++ b/src/HOL/Cardinals/Ordinal_Arithmetic.thy Thu Jan 16 20:52:54 2014 +0100
@@ -148,7 +148,7 @@
have "compat r (r +o r') Inl" unfolding compat_def osum_def by auto
moreover
have "ofilter (r +o r') (Inl ` Field r)"
- unfolding wo_rel.ofilter_def[unfolded wo_rel_def, OF 1] Field_osum rel.under_def
+ unfolding wo_rel.ofilter_def[unfolded wo_rel_def, OF 1] Field_osum under_def
unfolding osum_def Field_def by auto
ultimately show ?thesis using assms by (auto simp add: embed_iff_compat_inj_on_ofilter)
qed
@@ -322,7 +322,7 @@
from r' have "compat r (r *o r') ?f" unfolding compat_def oprod_def by auto
moreover
from * have "ofilter (r *o r') (?f ` Field r)"
- unfolding wo_rel.ofilter_def[unfolded wo_rel_def, OF 1] Field_oprod rel.under_def
+ unfolding wo_rel.ofilter_def[unfolded wo_rel_def, OF 1] Field_oprod under_def
unfolding oprod_def by auto (auto simp: image_iff Field_def)
moreover have "inj_on ?f (Field r)" unfolding inj_on_def by auto
ultimately show ?thesis using assms by (auto simp add: embed_iff_compat_inj_on_ofilter)
@@ -924,11 +924,11 @@
lemma iso_ozero_empty[simp]: "r =o ozero = (r = {})"
unfolding ozero_def ordIso_def iso_def[abs_def] embed_def bij_betw_def
- by (auto dest: rel.well_order_on_domain)
+ by (auto dest: well_order_on_domain)
lemma ozero_ordLeq:
assumes "Well_order r" shows "ozero \<le>o r"
-using assms unfolding ozero_def ordLeq_def embed_def[abs_def] rel.under_def by auto
+using assms unfolding ozero_def ordLeq_def embed_def[abs_def] under_def by auto
definition "oone = {((),())}"
@@ -942,10 +942,10 @@
lemma oone_ordIso: "oone =o {(x,x)}"
unfolding ordIso_def oone_def well_order_on_def linear_order_on_def partial_order_on_def
preorder_on_def total_on_def refl_on_def trans_def antisym_def
- by (auto simp: iso_def embed_def bij_betw_def rel.under_def inj_on_def intro!: exI[of _ "\<lambda>_. x"])
+ by (auto simp: iso_def embed_def bij_betw_def under_def inj_on_def intro!: exI[of _ "\<lambda>_. x"])
lemma osum_ordLeqR: "Well_order r \<Longrightarrow> Well_order s \<Longrightarrow> s \<le>o r +o s"
- unfolding ordLeq_def2 rel.underS_def
+ unfolding ordLeq_def2 underS_def
by (auto intro!: exI[of _ Inr] osum_Well_order) (auto simp add: osum_def Field_def)
lemma osum_congL:
@@ -1043,7 +1043,7 @@
unfolding Field_oprod iso_def bij_betw_def inj_on_def by fastforce
with f have "bij_betw ?f (Field ?L) (Field ?R)"
unfolding Field_oprod iso_def bij_betw_def by (auto intro!: map_pair_surj_on)
- moreover from f rel.well_order_on_domain[OF r] have "compat ?L ?R ?f"
+ moreover from f well_order_on_domain[OF r] have "compat ?L ?R ?f"
unfolding iso_iff3[OF r s] compat_def oprod_def bij_betw_def
by (auto simp: map_pair_imageI dest: inj_onD)
ultimately have "iso ?L ?R ?f" by (subst iso_iff3) (auto intro: oprod_Well_order r s t)
@@ -1057,7 +1057,7 @@
assms[unfolded ordIso_def] by auto
lemma Field_singleton[simp]: "Field {(z,z)} = {z}"
- by (metis rel.well_order_on_Field well_order_on_singleton)
+ by (metis well_order_on_Field well_order_on_singleton)
lemma zero_singleton[simp]: "zero {(z,z)} = z"
using wo_rel.zero_in_Field[unfolded wo_rel_def, of "{(z, z)}"] well_order_on_singleton[of z]
@@ -1077,7 +1077,7 @@
then obtain x where "x \<in> Field r" by auto
with * have Fr: "Field r = {x}" by auto
interpret r: wo_rel r by unfold_locales (rule r)
- from Fr r.well_order_on_domain[OF r] refl_onD[OF r.REFL, of x] have r_def: "r = {(x, x)}" by fast
+ from Fr well_order_on_domain[OF r] refl_onD[OF r.REFL, of x] have r_def: "r = {(x, x)}" by fast
interpret wo_rel2 r s by unfold_locales (rule r, rule s)
have "bij_betw (\<lambda>x. ()) (Field ?L) (Field ?R)"
unfolding bij_betw_def Field_oexp by (auto simp: r_def FinFunc_singleton)
@@ -1138,7 +1138,7 @@
interpret t!: wo_rel t by unfold_locales (rule t)
interpret rt!: wo_rel ?R by unfold_locales (rule osum_Well_order[OF r t])
from *(3) have "ofilter ?R (?f ` Field ?L)"
- unfolding t.ofilter_def rt.ofilter_def Field_osum image_Un image_image rel.under_def
+ unfolding t.ofilter_def rt.ofilter_def Field_osum image_Un image_image under_def
by (auto simp: osum_def intro!: imageI) (auto simp: Field_def)
ultimately have "embed ?L ?R ?f" using embed_iff_compat_inj_on_ofilter[of ?L ?R ?f]
by (auto intro: osum_Well_order r s t)
@@ -1157,7 +1157,7 @@
let ?f = "sum_map f id"
from f have "\<forall>a\<in>Field (r +o t).
?f a \<in> Field (s +o t) \<and> ?f ` underS (r +o t) a \<subseteq> underS (s +o t) (?f a)"
- unfolding Field_osum rel.underS_def by (fastforce simp: osum_def)
+ unfolding Field_osum underS_def by (fastforce simp: osum_def)
thus ?thesis unfolding ordLeq_def2 by (auto intro: osum_Well_order r s t)
qed
@@ -1199,13 +1199,13 @@
from *(1) have "inj_on ?f (Field ?L)" unfolding Field_oprod inj_on_def by fastforce
moreover
from *(2,4) the_inv_into_f_f[OF *(1)] have "compat ?L ?R ?f" unfolding compat_def oprod_def
- by auto (metis rel.well_order_on_domain t, metis rel.well_order_on_domain s)
+ by auto (metis well_order_on_domain t, metis well_order_on_domain s)
moreover
interpret t!: wo_rel t by unfold_locales (rule t)
interpret rt!: wo_rel ?R by unfold_locales (rule oprod_Well_order[OF r t])
from *(3) have "ofilter ?R (?f ` Field ?L)"
- unfolding t.ofilter_def rt.ofilter_def Field_oprod rel.under_def
- by (auto simp: oprod_def image_iff) (fast | metis r rel.well_order_on_domain)+
+ unfolding t.ofilter_def rt.ofilter_def Field_oprod under_def
+ by (auto simp: oprod_def image_iff) (fast | metis r well_order_on_domain)+
ultimately have "embed ?L ?R ?f" using embed_iff_compat_inj_on_ofilter[of ?L ?R ?f]
by (auto intro: oprod_Well_order r s t)
moreover
@@ -1226,7 +1226,7 @@
let ?f = "map_pair f id"
from f have "\<forall>a\<in>Field (r *o t).
?f a \<in> Field (s *o t) \<and> ?f ` underS (r *o t) a \<subseteq> underS (s *o t) (?f a)"
- unfolding Field_oprod rel.underS_def unfolding map_pair_def oprod_def by auto
+ unfolding Field_oprod underS_def unfolding map_pair_def oprod_def by auto
thus ?thesis unfolding ordLeq_def2 by (auto intro: oprod_Well_order r s t)
qed
@@ -1269,7 +1269,7 @@
lemma ozero_oexp: "\<not> (s =o ozero) \<Longrightarrow> ozero ^o s =o ozero"
unfolding oexp_def[OF ozero_Well_order s] FinFunc_def
- by simp (metis Func_emp2 bot.extremum_uniqueI emptyE rel.well_order_on_domain s subrelI)
+ by simp (metis Func_emp2 bot.extremum_uniqueI emptyE well_order_on_domain s subrelI)
lemma oone_oexp: "oone ^o s =o oone" (is "?L =o ?R")
by (rule oone_ordIso_oexp[OF ordIso_reflexive[OF oone_Well_order] s])
@@ -1326,7 +1326,7 @@
qed
moreover
from FLR have "ofilter ?R (F ` Field ?L)"
- unfolding rexpt.ofilter_def rel.under_def rs.Field_oexp rt.Field_oexp unfolding rt.oexp_def
+ unfolding rexpt.ofilter_def under_def rs.Field_oexp rt.Field_oexp unfolding rt.oexp_def
proof (safe elim!: imageI)
fix g h assume gh: "g \<in> FinFunc r s" "h \<in> FinFunc r t" "F g \<in> FinFunc r t"
"let m = t.max_fun_diff h (F g) in (h m, F g m) \<in> r"
@@ -1348,7 +1348,7 @@
assume "(t.max_fun_diff h (F g), z) \<notin> t"
hence "(z, t.max_fun_diff h (F g)) \<in> t" using t.in_notinI[of "t.max_fun_diff h (F g)" z]
z max_Field by auto
- hence "z \<in> f ` Field s" using *(3) max_f_Field unfolding t.ofilter_def rel.under_def
+ hence "z \<in> f ` Field s" using *(3) max_f_Field unfolding t.ofilter_def under_def
by fastforce
with z show False by blast
qed
@@ -1356,9 +1356,9 @@
z max_f_Field unfolding F_def by auto
} note ** = this
with *(3) gh(2) have "h = F (\<lambda>x. if x \<in> Field s then h (f x) else undefined)" using invff
- unfolding F_def fun_eq_iff FinFunc_def Func_def Let_def t.ofilter_def rel.under_def by auto
+ unfolding F_def fun_eq_iff FinFunc_def Func_def Let_def t.ofilter_def under_def by auto
moreover from gh(2) *(1,3) have "(\<lambda>x. if x \<in> Field s then h (f x) else undefined) \<in> FinFunc r s"
- unfolding FinFunc_def Func_def fin_support_def support_def t.ofilter_def rel.under_def
+ unfolding FinFunc_def Func_def fin_support_def support_def t.ofilter_def under_def
by (auto intro: subset_inj_on elim!: finite_imageD[OF finite_subset[rotated]])
ultimately show "?thesis" by (rule image_eqI)
qed simp
@@ -1396,7 +1396,7 @@
interpret t!: wo_rel t by unfold_locales (rule t)
show ?thesis
proof (cases "t = {}")
- case True thus ?thesis using r s unfolding ordLeq_def2 rel.underS_def by auto
+ case True thus ?thesis using r s unfolding ordLeq_def2 underS_def by auto
next
case False thus ?thesis
proof (cases "r = {}")
@@ -1408,9 +1408,9 @@
hence f_underS: "\<forall>a\<in>Field r. f a \<in> Field s \<and> f ` underS r a \<subseteq> underS s (f a)"
using embed_in_Field[OF rt.rWELL f] embed_underS2[OF rt.rWELL st.rWELL f] by auto
from f `t \<noteq> {}` False have *: "Field r \<noteq> {}" "Field s \<noteq> {}" "Field t \<noteq> {}"
- unfolding Field_def embed_def rel.under_def bij_betw_def by auto
+ unfolding Field_def embed_def under_def bij_betw_def by auto
with f obtain x where "s.zero = f x" "x \<in> Field r" unfolding embed_def bij_betw_def
- using embed_in_Field[OF r.WELL f] s.zero_under set_mp[OF r.under_Field] by blast
+ using embed_in_Field[OF r.WELL f] s.zero_under set_mp[OF under_Field[of r]] by blast
with f have fz: "f r.zero = s.zero" and inj: "inj_on f (Field r)" and compat: "compat r s f"
unfolding embed_iff_compat_inj_on_ofilter[OF r s] compat_def
by (fastforce intro: s.leq_zero_imp)+
@@ -1424,11 +1424,11 @@
proof safe
fix h
assume h_underS: "h \<in> underS (r ^o t) g"
- hence "h \<in> Field (r ^o t)" unfolding rel.underS_def Field_def by auto
+ hence "h \<in> Field (r ^o t)" unfolding underS_def Field_def by auto
with fz f_underS have Field_fh: "?f h \<in> Field (s ^o t)"
unfolding st.Field_oexp rt.Field_oexp FinFunc_def Func_def fin_support_def support_def
by (auto elim!: finite_subset[rotated])
- from h_underS have "h \<noteq> g" and hg: "(h, g) \<in> rt.oexp" unfolding rel.underS_def by auto
+ from h_underS have "h \<noteq> g" and hg: "(h, g) \<in> rt.oexp" unfolding underS_def by auto
with f inj have neq: "?f h \<noteq> ?f g"
unfolding fun_eq_iff inj_on_def rt.oexp_def Option.map_def FinFunc_def Func_def Let_def
by simp metis
@@ -1440,7 +1440,7 @@
with Field_fg Field_fh hg fz f_underS compat neq have "(?f h, ?f g) \<in> st.oexp"
using rt.max_fun_diff[OF `h \<noteq> g`] rt.max_fun_diff_in[OF `h \<noteq> g`] unfolding st.Field_oexp
unfolding rt.oexp_def st.oexp_def Let_def compat_def by auto
- ultimately show "?f h \<in> underS (s ^o t) (?f g)" unfolding rel.underS_def by auto
+ ultimately show "?f h \<in> underS (s ^o t) (?f g)" unfolding underS_def by auto
qed
ultimately have "?f g \<in> Field (s ^o t) \<and> ?f ` underS (r ^o t) g \<subseteq> underS (s ^o t) (?f g)"
by blast
@@ -1457,11 +1457,11 @@
interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
interpret r!: wo_rel r by unfold_locales (rule r)
interpret s!: wo_rel s by unfold_locales (rule s)
- from assms rel.well_order_on_domain[OF r] obtain x where
+ from assms well_order_on_domain[OF r] obtain x where
x: "x \<in> Field r" "r.zero \<in> Field r" "x \<noteq> r.zero"
- unfolding ordLess_def oone_def embedS_def[abs_def] bij_betw_def embed_def rel.under_def
+ unfolding ordLess_def oone_def embedS_def[abs_def] bij_betw_def embed_def under_def
by (auto simp: image_def)
- (metis equals0D insert_not_empty r.under_def r.zero_in_Field rel.under_empty)
+ (metis (lifting) equals0D mem_Collect_eq r.zero_in_Field singletonI)
let ?f = "\<lambda>a b. if b \<in> Field s then if b = a then x else r.zero else undefined"
from x(3) have SUPP: "\<And>y. y \<in> Field s \<Longrightarrow> rs.SUPP (?f y) = {y}" unfolding support_def by auto
{ fix y assume y: "y \<in> Field s"
@@ -1472,7 +1472,7 @@
proof safe
fix z
assume "z \<in> underS s y"
- hence z: "z \<noteq> y" "(z, y) \<in> s" "z \<in> Field s" unfolding rel.underS_def Field_def by auto
+ hence z: "z \<noteq> y" "(z, y) \<in> s" "z \<in> Field s" unfolding underS_def Field_def by auto
from x(3) y z(1,3) have "?f z \<noteq> ?f y" unfolding fun_eq_iff by auto
moreover
{ from x(1,2) have "?f z \<in> FinFunc r s" "?f y \<in> FinFunc r s"
@@ -1484,7 +1484,7 @@
ultimately have "(?f z, ?f y) \<in> rs.oexp" using y x(1)
unfolding rs.oexp_def Let_def by auto
}
- ultimately show "?f z \<in> underS (r ^o s) (?f y)" unfolding rel.underS_def by blast
+ ultimately show "?f z \<in> underS (r ^o s) (?f y)" unfolding underS_def by blast
qed
ultimately have "?f y \<in> Field (r ^o s) \<and> ?f ` underS s y \<subseteq> underS (r ^o s) (?f y)" by blast
}
--- a/src/HOL/Cardinals/Wellfounded_More_FP.thy Thu Jan 16 18:52:50 2014 +0100
+++ b/src/HOL/Cardinals/Wellfounded_More_FP.thy Thu Jan 16 20:52:54 2014 +0100
@@ -151,7 +151,7 @@
moreover
{fix A assume *: "A \<le> Field r" and **: "A \<noteq> {}"
obtain a where 1: "r = {} \<or> r = {(a,a)}" using LI
- unfolding order_on_defs using Case1 rel.Total_subset_Id by auto
+ unfolding order_on_defs using Case1 Total_subset_Id by auto
hence "A = {a} \<and> r = {(a,a)}" using * ** unfolding Field_def by blast
hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" using 1 by blast
}
@@ -169,7 +169,7 @@
hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id"
using 1 * unfolding wf_eq_minimal2 by simp
moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. ((a,a') \<in> r) = ((a',a) \<notin> r - Id)"
- using rel.Linear_order_in_diff_Id[of r] ** LI by blast
+ using Linear_order_in_diff_Id[of r] ** LI by blast
ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" by blast
qed
next
@@ -180,7 +180,7 @@
hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r"
using 1 * by simp
moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. ((a,a') \<in> r) = ((a',a) \<notin> r - Id)"
- using rel.Linear_order_in_diff_Id[of r] ** LI mono_Field[of "r - Id" r] by blast
+ using Linear_order_in_diff_Id[of r] ** LI mono_Field[of "r - Id" r] by blast
ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id" by blast
qed
qed
--- a/src/HOL/Cardinals/Wellorder_Embedding.thy Thu Jan 16 18:52:50 2014 +0100
+++ b/src/HOL/Cardinals/Wellorder_Embedding.thy Thu Jan 16 20:52:54 2014 +0100
@@ -41,7 +41,7 @@
using EMB unfolding embed_def by simp
moreover
{have "under r a \<le> Field r"
- by (auto simp add: rel.under_Field)
+ by (auto simp add: under_Field)
hence "\<And> b. b \<in> under r a \<Longrightarrow> f b = g b"
using EQ by blast
}
@@ -80,10 +80,10 @@
proof-
obtain r where "well_order_on A r" by (fastforce simp add: well_order_on)
hence 1: "A = Field r \<and> Well_order r"
- using rel.well_order_on_Well_order by auto
+ using well_order_on_Well_order by auto
obtain r' where 2: "well_order_on A' r'" by (fastforce simp add: well_order_on)
hence 2: "A' = Field r' \<and> Well_order r'"
- using rel.well_order_on_Well_order by auto
+ using well_order_on_Well_order by auto
hence "(\<exists>f. embed r r' f) \<or> (\<exists>g. embed r' r g)"
using 1 2 by (auto simp add: wellorders_totally_ordered)
moreover
--- a/src/HOL/Cardinals/Wellorder_Embedding_FP.thy Thu Jan 16 18:52:50 2014 +0100
+++ b/src/HOL/Cardinals/Wellorder_Embedding_FP.thy Thu Jan 16 20:52:54 2014 +0100
@@ -40,20 +40,20 @@
lemma under_underS_bij_betw:
assumes WELL: "Well_order r" and WELL': "Well_order r'" and
IN: "a \<in> Field r" and IN': "f a \<in> Field r'" and
- BIJ: "bij_betw f (rel.underS r a) (rel.underS r' (f a))"
-shows "bij_betw f (rel.under r a) (rel.under r' (f a))"
+ BIJ: "bij_betw f (underS r a) (underS r' (f a))"
+shows "bij_betw f (under r a) (under r' (f a))"
proof-
- have "a \<notin> rel.underS r a \<and> f a \<notin> rel.underS r' (f a)"
- unfolding rel.underS_def by auto
+ have "a \<notin> underS r a \<and> f a \<notin> underS r' (f a)"
+ unfolding underS_def by auto
moreover
{have "Refl r \<and> Refl r'" using WELL WELL'
by (auto simp add: order_on_defs)
- hence "rel.under r a = rel.underS r a \<union> {a} \<and>
- rel.under r' (f a) = rel.underS r' (f a) \<union> {f a}"
- using IN IN' by(auto simp add: rel.Refl_under_underS)
+ hence "under r a = underS r a \<union> {a} \<and>
+ under r' (f a) = underS r' (f a) \<union> {f a}"
+ using IN IN' by(auto simp add: Refl_under_underS)
}
ultimately show ?thesis
- using BIJ notIn_Un_bij_betw[of a "rel.underS r a" f "rel.underS r' (f a)"] by auto
+ using BIJ notIn_Un_bij_betw[of a "underS r a" f "underS r' (f a)"] by auto
qed
@@ -75,7 +75,7 @@
definition embed :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> bool"
where
-"embed r r' f \<equiv> \<forall>a \<in> Field r. bij_betw f (rel.under r a) (rel.under r' (f a))"
+"embed r r' f \<equiv> \<forall>a \<in> Field r. bij_betw f (under r a) (under r' (f a))"
lemmas embed_defs = embed_def embed_def[abs_def]
@@ -133,11 +133,11 @@
using WELL by (auto simp add: wo_rel_def)
hence 1: "Refl r"
by (auto simp add: wo_rel.REFL)
- hence "a \<in> rel.under r a" using IN rel.Refl_under_in by fastforce
- hence "f a \<in> rel.under r' (f a)"
+ hence "a \<in> under r a" using IN Refl_under_in by fastforce
+ hence "f a \<in> under r' (f a)"
using EMB IN by (auto simp add: embed_def bij_betw_def)
thus ?thesis unfolding Field_def
- by (auto simp: rel.under_def)
+ by (auto simp: under_def)
qed
@@ -147,16 +147,16 @@
shows "embed r r'' (f' o f)"
proof(unfold embed_def, auto)
fix a assume *: "a \<in> Field r"
- hence "bij_betw f (rel.under r a) (rel.under r' (f a))"
+ hence "bij_betw f (under r a) (under r' (f a))"
using embed_def[of r] EMB by auto
moreover
{have "f a \<in> Field r'"
using EMB WELL * by (auto simp add: embed_in_Field)
- hence "bij_betw f' (rel.under r' (f a)) (rel.under r'' (f' (f a)))"
+ hence "bij_betw f' (under r' (f a)) (under r'' (f' (f a)))"
using embed_def[of r'] EMB' by auto
}
ultimately
- show "bij_betw (f' \<circ> f) (rel.under r a) (rel.under r'' (f'(f a)))"
+ show "bij_betw (f' \<circ> f) (under r a) (under r'' (f'(f a)))"
by(auto simp add: bij_betw_trans)
qed
@@ -190,14 +190,14 @@
show ?thesis using Well' WELL EMB 0 embed_Field[of r r' f]
proof(unfold wo_rel.ofilter_def, auto simp add: image_def)
fix a b'
- assume *: "a \<in> A" and **: "b' \<in> rel.under r' (f a)"
+ assume *: "a \<in> A" and **: "b' \<in> under r' (f a)"
hence "a \<in> Field r" using 0 by auto
- hence "bij_betw f (rel.under r a) (rel.under r' (f a))"
+ hence "bij_betw f (under r a) (under r' (f a))"
using * EMB by (auto simp add: embed_def)
- hence "f`(rel.under r a) = rel.under r' (f a)"
+ hence "f`(under r a) = under r' (f a)"
by (simp add: bij_betw_def)
- with ** image_def[of f "rel.under r a"] obtain b where
- 1: "b \<in> rel.under r a \<and> b' = f b" by blast
+ with ** image_def[of f "under r a"] obtain b where
+ 1: "b \<in> under r a \<and> b' = f b" by blast
hence "b \<in> A" using Well * OF
by (auto simp add: wo_rel.ofilter_def)
with 1 show "\<exists>b \<in> A. b' = f b" by blast
@@ -224,14 +224,14 @@
fix a b
assume *: "(a,b) \<in> r"
hence 1: "b \<in> Field r" using Field_def[of r] by blast
- have "a \<in> rel.under r b"
- using * rel.under_def[of r] by simp
- hence "f a \<in> rel.under r' (f b)"
+ have "a \<in> under r b"
+ using * under_def[of r] by simp
+ hence "f a \<in> under r' (f b)"
using EMB embed_def[of r r' f]
- bij_betw_def[of f "rel.under r b" "rel.under r' (f b)"]
- image_def[of f "rel.under r b"] 1 by auto
+ bij_betw_def[of f "under r b" "under r' (f b)"]
+ image_def[of f "under r b"] 1 by auto
thus "(f a, f b) \<in> r'"
- by (auto simp add: rel.under_def)
+ by (auto simp add: under_def)
qed
@@ -252,16 +252,16 @@
hence 1: "a \<in> Field r \<and> b \<in> Field r"
unfolding Field_def by auto
{assume "(a,b) \<in> r"
- hence "a \<in> rel.under r b \<and> b \<in> rel.under r b"
- using Refl by(auto simp add: rel.under_def refl_on_def)
+ hence "a \<in> under r b \<and> b \<in> under r b"
+ using Refl by(auto simp add: under_def refl_on_def)
hence "a = b"
using EMB 1 ***
by (auto simp add: embed_def bij_betw_def inj_on_def)
}
moreover
{assume "(b,a) \<in> r"
- hence "a \<in> rel.under r a \<and> b \<in> rel.under r a"
- using Refl by(auto simp add: rel.under_def refl_on_def)
+ hence "a \<in> under r a \<and> b \<in> under r a"
+ using Refl by(auto simp add: under_def refl_on_def)
hence "a = b"
using EMB 1 ***
by (auto simp add: embed_def bij_betw_def inj_on_def)
@@ -275,19 +275,19 @@
lemma embed_underS:
assumes WELL: "Well_order r" and WELL': "Well_order r'" and
EMB: "embed r r' f" and IN: "a \<in> Field r"
-shows "bij_betw f (rel.underS r a) (rel.underS r' (f a))"
+shows "bij_betw f (underS r a) (underS r' (f a))"
proof-
- have "bij_betw f (rel.under r a) (rel.under r' (f a))"
+ have "bij_betw f (under r a) (under r' (f a))"
using assms by (auto simp add: embed_def)
moreover
{have "f a \<in> Field r'" using assms embed_Field[of r r' f] by auto
- hence "rel.under r a = rel.underS r a \<union> {a} \<and>
- rel.under r' (f a) = rel.underS r' (f a) \<union> {f a}"
- using assms by (auto simp add: order_on_defs rel.Refl_under_underS)
+ hence "under r a = underS r a \<union> {a} \<and>
+ under r' (f a) = underS r' (f a) \<union> {f a}"
+ using assms by (auto simp add: order_on_defs Refl_under_underS)
}
moreover
- {have "a \<notin> rel.underS r a \<and> f a \<notin> rel.underS r' (f a)"
- unfolding rel.underS_def by blast
+ {have "a \<notin> underS r a \<and> f a \<notin> underS r' (f a)"
+ unfolding underS_def by blast
}
ultimately show ?thesis
by (auto simp add: notIn_Un_bij_betw3)
@@ -325,20 +325,20 @@
unfolding Field_def by auto
have "f a \<in> f`(Field r)"
using **** by auto
- hence 2: "rel.under r' (f a) \<le> f`(Field r)"
+ hence 2: "under r' (f a) \<le> f`(Field r)"
using Well' *** wo_rel.ofilter_def[of r' "f`(Field r)"] by fastforce
(* Main proof *)
- show "bij_betw f (rel.under r a) (rel.under r' (f a))"
+ show "bij_betw f (under r a) (under r' (f a))"
proof(unfold bij_betw_def, auto)
- show "inj_on f (rel.under r a)"
- using * by (metis (no_types) rel.under_Field subset_inj_on)
+ show "inj_on f (under r a)"
+ using * by (metis (no_types) under_Field subset_inj_on)
next
- fix b assume "b \<in> rel.under r a"
- thus "f b \<in> rel.under r' (f a)"
- unfolding rel.under_def using **
+ fix b assume "b \<in> under r a"
+ thus "f b \<in> under r' (f a)"
+ unfolding under_def using **
by (auto simp add: compat_def)
next
- fix b' assume *****: "b' \<in> rel.under r' (f a)"
+ fix b' assume *****: "b' \<in> under r' (f a)"
hence "b' \<in> f`(Field r)"
using 2 by auto
with Field_def[of r] obtain b where
@@ -349,7 +349,7 @@
with ** 4 have "(f a, b'): r'"
by (auto simp add: compat_def)
with ***** Antisym' have "f a = b'"
- by(auto simp add: rel.under_def antisym_def)
+ by(auto simp add: under_def antisym_def)
with 3 **** 4 * have "a = b"
by(auto simp add: inj_on_def)
}
@@ -361,15 +361,15 @@
ultimately
show ?thesis using Total **** 3 by (fastforce simp add: total_on_def)
qed
- with 4 show "b' \<in> f`(rel.under r a)"
- unfolding rel.under_def by auto
+ with 4 show "b' \<in> f`(under r a)"
+ unfolding under_def by auto
qed
qed
lemma inv_into_ofilter_embed:
assumes WELL: "Well_order r" and OF: "wo_rel.ofilter r A" and
- BIJ: "\<forall>b \<in> A. bij_betw f (rel.under r b) (rel.under r' (f b))" and
+ BIJ: "\<forall>b \<in> A. bij_betw f (under r b) (under r' (f b))" and
IMAGE: "f ` A = Field r'"
shows "embed r' r (inv_into A f)"
proof-
@@ -390,16 +390,16 @@
using * ** Well OF by (auto simp add: wo_rel.ofilter_def)
moreover
{assume "(b1,b2) \<in> r"
- hence "b1 \<in> rel.under r b2 \<and> b2 \<in> rel.under r b2"
- unfolding rel.under_def using 11 Refl
+ hence "b1 \<in> under r b2 \<and> b2 \<in> under r b2"
+ unfolding under_def using 11 Refl
by (auto simp add: refl_on_def)
hence "b1 = b2" using BIJ * ** ***
by (simp add: bij_betw_def inj_on_def)
}
moreover
{assume "(b2,b1) \<in> r"
- hence "b1 \<in> rel.under r b1 \<and> b2 \<in> rel.under r b1"
- unfolding rel.under_def using 11 Refl
+ hence "b1 \<in> under r b1 \<and> b2 \<in> under r b1"
+ unfolding under_def using 11 Refl
by (auto simp add: refl_on_def)
hence "b1 = b2" using BIJ * ** ***
by (simp add: bij_betw_def inj_on_def)
@@ -411,20 +411,20 @@
(* *)
let ?f' = "(inv_into A f)"
(* *)
- have 2: "\<forall>b \<in> A. bij_betw ?f' (rel.under r' (f b)) (rel.under r b)"
+ have 2: "\<forall>b \<in> A. bij_betw ?f' (under r' (f b)) (under r b)"
proof(clarify)
fix b assume *: "b \<in> A"
- hence "rel.under r b \<le> A"
+ hence "under r b \<le> A"
using Well OF by(auto simp add: wo_rel.ofilter_def)
moreover
- have "f ` (rel.under r b) = rel.under r' (f b)"
+ have "f ` (under r b) = under r' (f b)"
using * BIJ by (auto simp add: bij_betw_def)
ultimately
- show "bij_betw ?f' (rel.under r' (f b)) (rel.under r b)"
+ show "bij_betw ?f' (under r' (f b)) (under r b)"
using 1 by (auto simp add: bij_betw_inv_into_subset)
qed
(* *)
- have 3: "\<forall>b' \<in> Field r'. bij_betw ?f' (rel.under r' b') (rel.under r (?f' b'))"
+ have 3: "\<forall>b' \<in> Field r'. bij_betw ?f' (under r' b') (under r (?f' b'))"
proof(clarify)
fix b' assume *: "b' \<in> Field r'"
have "b' = f (?f' b')" using * 1
@@ -435,7 +435,7 @@
with 31 have "?f' b' \<in> A" by auto
}
ultimately
- show "bij_betw ?f' (rel.under r' b') (rel.under r (?f' b'))"
+ show "bij_betw ?f' (under r' b') (under r (?f' b'))"
using 2 by auto
qed
(* *)
@@ -445,10 +445,10 @@
lemma inv_into_underS_embed:
assumes WELL: "Well_order r" and
- BIJ: "\<forall>b \<in> rel.underS r a. bij_betw f (rel.under r b) (rel.under r' (f b))" and
+ BIJ: "\<forall>b \<in> underS r a. bij_betw f (under r b) (under r' (f b))" and
IN: "a \<in> Field r" and
- IMAGE: "f ` (rel.underS r a) = Field r'"
-shows "embed r' r (inv_into (rel.underS r a) f)"
+ IMAGE: "f ` (underS r a) = Field r'"
+shows "embed r' r (inv_into (underS r a) f)"
using assms
by(auto simp add: wo_rel_def wo_rel.underS_ofilter inv_into_ofilter_embed)
@@ -458,7 +458,7 @@
IMAGE: "Field r' \<le> f ` (Field r)"
shows "embed r' r (inv_into (Field r) f)"
proof-
- have "(\<forall>b \<in> Field r. bij_betw f (rel.under r b) (rel.under r' (f b)))"
+ have "(\<forall>b \<in> Field r. bij_betw f (under r b) (under r' (f b)))"
using EMB by (auto simp add: embed_def)
moreover
have "f ` (Field r) \<le> Field r'"
@@ -511,101 +511,101 @@
fixes r ::"'a rel" and r'::"'a' rel" and
f :: "'a \<Rightarrow> 'a'" and a::'a
assumes WELL: "Well_order r" and WELL': "Well_order r'" and IN: "a \<in> Field r" and
- IH: "\<forall>b \<in> rel.underS r a. bij_betw f (rel.under r b) (rel.under r' (f b))" and
- NOT: "f ` (rel.underS r a) \<noteq> Field r'" and SUC: "f a = wo_rel.suc r' (f`(rel.underS r a))"
-shows "bij_betw f (rel.under r a) (rel.under r' (f a))"
+ IH: "\<forall>b \<in> underS r a. bij_betw f (under r b) (under r' (f b))" and
+ NOT: "f ` (underS r a) \<noteq> Field r'" and SUC: "f a = wo_rel.suc r' (f`(underS r a))"
+shows "bij_betw f (under r a) (under r' (f a))"
proof-
(* Preliminary facts *)
have Well: "wo_rel r" using WELL unfolding wo_rel_def .
hence Refl: "Refl r" using wo_rel.REFL[of r] by auto
have Trans: "trans r" using Well wo_rel.TRANS[of r] by auto
have Well': "wo_rel r'" using WELL' unfolding wo_rel_def .
- have OF: "wo_rel.ofilter r (rel.underS r a)"
+ have OF: "wo_rel.ofilter r (underS r a)"
by (auto simp add: Well wo_rel.underS_ofilter)
- hence UN: "rel.underS r a = (\<Union> b \<in> rel.underS r a. rel.under r b)"
- using Well wo_rel.ofilter_under_UNION[of r "rel.underS r a"] by blast
- (* Gather facts about elements of rel.underS r a *)
- {fix b assume *: "b \<in> rel.underS r a"
- hence t0: "(b,a) \<in> r \<and> b \<noteq> a" unfolding rel.underS_def by auto
+ hence UN: "underS r a = (\<Union> b \<in> underS r a. under r b)"
+ using Well wo_rel.ofilter_under_UNION[of r "underS r a"] by blast
+ (* Gather facts about elements of underS r a *)
+ {fix b assume *: "b \<in> underS r a"
+ hence t0: "(b,a) \<in> r \<and> b \<noteq> a" unfolding underS_def by auto
have t1: "b \<in> Field r"
- using * rel.underS_Field[of r a] by auto
- have t2: "f`(rel.under r b) = rel.under r' (f b)"
+ using * underS_Field[of r a] by auto
+ have t2: "f`(under r b) = under r' (f b)"
using IH * by (auto simp add: bij_betw_def)
- hence t3: "wo_rel.ofilter r' (f`(rel.under r b))"
+ hence t3: "wo_rel.ofilter r' (f`(under r b))"
using Well' by (auto simp add: wo_rel.under_ofilter)
- have "f`(rel.under r b) \<le> Field r'"
- using t2 by (auto simp add: rel.under_Field)
+ have "f`(under r b) \<le> Field r'"
+ using t2 by (auto simp add: under_Field)
moreover
- have "b \<in> rel.under r b"
- using t1 by(auto simp add: Refl rel.Refl_under_in)
+ have "b \<in> under r b"
+ using t1 by(auto simp add: Refl Refl_under_in)
ultimately
have t4: "f b \<in> Field r'" by auto
- have "f`(rel.under r b) = rel.under r' (f b) \<and>
- wo_rel.ofilter r' (f`(rel.under r b)) \<and>
+ have "f`(under r b) = under r' (f b) \<and>
+ wo_rel.ofilter r' (f`(under r b)) \<and>
f b \<in> Field r'"
using t2 t3 t4 by auto
}
hence bFact:
- "\<forall>b \<in> rel.underS r a. f`(rel.under r b) = rel.under r' (f b) \<and>
- wo_rel.ofilter r' (f`(rel.under r b)) \<and>
+ "\<forall>b \<in> underS r a. f`(under r b) = under r' (f b) \<and>
+ wo_rel.ofilter r' (f`(under r b)) \<and>
f b \<in> Field r'" by blast
(* *)
- have subField: "f`(rel.underS r a) \<le> Field r'"
+ have subField: "f`(underS r a) \<le> Field r'"
using bFact by blast
(* *)
- have OF': "wo_rel.ofilter r' (f`(rel.underS r a))"
+ have OF': "wo_rel.ofilter r' (f`(underS r a))"
proof-
- have "f`(rel.underS r a) = f`(\<Union> b \<in> rel.underS r a. rel.under r b)"
+ have "f`(underS r a) = f`(\<Union> b \<in> underS r a. under r b)"
using UN by auto
- also have "\<dots> = (\<Union> b \<in> rel.underS r a. f`(rel.under r b))" by blast
- also have "\<dots> = (\<Union> b \<in> rel.underS r a. (rel.under r' (f b)))"
+ also have "\<dots> = (\<Union> b \<in> underS r a. f`(under r b))" by blast
+ also have "\<dots> = (\<Union> b \<in> underS r a. (under r' (f b)))"
using bFact by auto
finally
- have "f`(rel.underS r a) = (\<Union> b \<in> rel.underS r a. (rel.under r' (f b)))" .
+ have "f`(underS r a) = (\<Union> b \<in> underS r a. (under r' (f b)))" .
thus ?thesis
using Well' bFact
- wo_rel.ofilter_UNION[of r' "rel.underS r a" "\<lambda> b. rel.under r' (f b)"] by fastforce
+ wo_rel.ofilter_UNION[of r' "underS r a" "\<lambda> b. under r' (f b)"] by fastforce
qed
(* *)
- have "f`(rel.underS r a) \<union> rel.AboveS r' (f`(rel.underS r a)) = Field r'"
+ have "f`(underS r a) \<union> AboveS r' (f`(underS r a)) = Field r'"
using Well' OF' by (auto simp add: wo_rel.ofilter_AboveS_Field)
- hence NE: "rel.AboveS r' (f`(rel.underS r a)) \<noteq> {}"
+ hence NE: "AboveS r' (f`(underS r a)) \<noteq> {}"
using subField NOT by blast
(* Main proof *)
- have INCL1: "f`(rel.underS r a) \<le> rel.underS r' (f a) "
+ have INCL1: "f`(underS r a) \<le> underS r' (f a) "
proof(auto)
- fix b assume *: "b \<in> rel.underS r a"
+ fix b assume *: "b \<in> 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 force
- thus "f b \<in> rel.underS r' (f a)"
- unfolding rel.underS_def by simp
+ wo_rel.suc_greater[of r' "f`(underS r a)" "f b"] by force
+ thus "f b \<in> underS r' (f a)"
+ unfolding underS_def by simp
qed
(* *)
- have INCL2: "rel.underS r' (f a) \<le> f`(rel.underS r a)"
+ have INCL2: "underS r' (f a) \<le> f`(underS r a)"
proof
- fix b' assume "b' \<in> rel.underS r' (f a)"
+ fix b' assume "b' \<in> underS r' (f a)"
hence "b' \<noteq> f a \<and> (b', f a) \<in> r'"
- unfolding rel.underS_def by simp
- thus "b' \<in> f`(rel.underS r a)"
+ unfolding underS_def by simp
+ thus "b' \<in> f`(underS r a)"
using Well' SUC NE OF'
- wo_rel.suc_ofilter_in[of r' "f ` rel.underS r a" b'] by auto
+ wo_rel.suc_ofilter_in[of r' "f ` underS r a" b'] by auto
qed
(* *)
- have INJ: "inj_on f (rel.underS r a)"
+ have INJ: "inj_on f (underS r a)"
proof-
- have "\<forall>b \<in> rel.underS r a. inj_on f (rel.under r b)"
+ have "\<forall>b \<in> underS r a. inj_on f (under r b)"
using IH by (auto simp add: bij_betw_def)
moreover
- have "\<forall>b. wo_rel.ofilter r (rel.under r b)"
+ have "\<forall>b. wo_rel.ofilter r (under r b)"
using Well by (auto simp add: wo_rel.under_ofilter)
ultimately show ?thesis
using WELL bFact UN
- UNION_inj_on_ofilter[of r "rel.underS r a" "\<lambda>b. rel.under r b" f]
+ UNION_inj_on_ofilter[of r "underS r a" "\<lambda>b. under r b" f]
by auto
qed
(* *)
- have BIJ: "bij_betw f (rel.underS r a) (rel.underS r' (f a))"
+ have BIJ: "bij_betw f (underS r a) (underS r' (f a))"
unfolding bij_betw_def
using INJ INCL1 INCL2 by auto
(* *)
@@ -622,14 +622,14 @@
f :: "'a \<Rightarrow> 'a'" and g :: "'a \<Rightarrow> bool" and a::'a
assumes WELL: "Well_order r" and WELL': "Well_order r'" and
MAIN1:
- "\<And> a. (False \<notin> g`(rel.underS r a) \<and> f`(rel.underS r a) \<noteq> Field r'
- \<longrightarrow> f a = wo_rel.suc r' (f`(rel.underS r a)) \<and> g a = True)
+ "\<And> a. (False \<notin> g`(underS r a) \<and> f`(underS r a) \<noteq> Field r'
+ \<longrightarrow> f a = wo_rel.suc r' (f`(underS r a)) \<and> g a = True)
\<and>
- (\<not>(False \<notin> (g`(rel.underS r a)) \<and> f`(rel.underS r a) \<noteq> Field r')
+ (\<not>(False \<notin> (g`(underS r a)) \<and> f`(underS r a) \<noteq> Field r')
\<longrightarrow> g a = False)" and
-MAIN2: "\<And> a. a \<in> Field r \<and> False \<notin> g`(rel.under r a) \<longrightarrow>
- bij_betw f (rel.under r a) (rel.under r' (f a))" and
-Case: "a \<in> Field r \<and> False \<in> g`(rel.under r a)"
+MAIN2: "\<And> a. a \<in> Field r \<and> False \<notin> g`(under r a) \<longrightarrow>
+ bij_betw f (under r a) (under r' (f a))" and
+Case: "a \<in> Field r \<and> False \<in> g`(under r a)"
shows "\<exists>f'. embed r' r f'"
proof-
have Well: "wo_rel r" using WELL unfolding wo_rel_def .
@@ -638,13 +638,13 @@
have Antisym: "antisym r" using Well wo_rel.ANTISYM[of r] by auto
have Well': "wo_rel r'" using WELL' unfolding wo_rel_def .
(* *)
- have 0: "rel.under r a = rel.underS r a \<union> {a}"
- using Refl Case by(auto simp add: rel.Refl_under_underS)
+ have 0: "under r a = underS r a \<union> {a}"
+ using Refl Case by(auto simp add: Refl_under_underS)
(* *)
have 1: "g a = False"
proof-
{assume "g a \<noteq> False"
- with 0 Case have "False \<in> g`(rel.underS r a)" by blast
+ with 0 Case have "False \<in> g`(underS r a)" by blast
with MAIN1 have "g a = False" by blast}
thus ?thesis by blast
qed
@@ -653,12 +653,12 @@
(* *)
have 2: "?A \<noteq> {} \<and> ?A \<le> Field r" using Case 1 by blast
(* *)
- have 3: "False \<notin> g`(rel.underS r ?a)"
+ have 3: "False \<notin> g`(underS r ?a)"
proof
- assume "False \<in> g`(rel.underS r ?a)"
- then obtain b where "b \<in> rel.underS r ?a" and 31: "g b = False" by auto
+ assume "False \<in> g`(underS r ?a)"
+ then obtain b where "b \<in> underS r ?a" and 31: "g b = False" by auto
hence 32: "(b,?a) \<in> r \<and> b \<noteq> ?a"
- by (auto simp add: rel.underS_def)
+ by (auto simp add: underS_def)
hence "b \<in> Field r" unfolding Field_def by auto
with 31 have "b \<in> ?A" by auto
hence "(?a,b) \<in> r" using wo_rel.minim_least 2 Well by fastforce
@@ -672,25 +672,25 @@
(* *)
have 5: "g ?a = False" using temp by blast
(* *)
- have 6: "f`(rel.underS r ?a) = Field r'"
+ have 6: "f`(underS r ?a) = Field r'"
using MAIN1[of ?a] 3 5 by blast
(* *)
- have 7: "\<forall>b \<in> rel.underS r ?a. bij_betw f (rel.under r b) (rel.under r' (f b))"
+ have 7: "\<forall>b \<in> underS r ?a. bij_betw f (under r b) (under r' (f b))"
proof
- fix b assume as: "b \<in> rel.underS r ?a"
+ fix b assume as: "b \<in> underS r ?a"
moreover
- have "wo_rel.ofilter r (rel.underS r ?a)"
+ have "wo_rel.ofilter r (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 (subst (asm) wo_rel.ofilter_def) fast+
+ have "False \<notin> g`(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)
+ unfolding Field_def using as by (auto simp add: underS_def)
ultimately
- show "bij_betw f (rel.under r b) (rel.under r' (f b))"
+ show "bij_betw f (under r b) (under r' (f b))"
using MAIN2 by auto
qed
(* *)
- have "embed r' r (inv_into (rel.underS r ?a) f)"
+ have "embed r' r (inv_into (underS r ?a) f)"
using WELL WELL' 7 4 6 inv_into_underS_embed[of r ?a f r'] by auto
thus ?thesis
unfolding embed_def by blast
@@ -709,18 +709,18 @@
have Well': "wo_rel r'" using WELL' unfolding wo_rel_def .
(* Main proof *)
obtain H where H_def: "H =
- (\<lambda>h a. if False \<notin> (snd o h)`(rel.underS r a) \<and> (fst o h)`(rel.underS r a) \<noteq> Field r'
- then (wo_rel.suc r' ((fst o h)`(rel.underS r a)), True)
+ (\<lambda>h a. if False \<notin> (snd o h)`(underS r a) \<and> (fst o h)`(underS r a) \<noteq> Field r'
+ then (wo_rel.suc r' ((fst o h)`(underS r a)), True)
else (undefined, False))" by blast
have Adm: "wo_rel.adm_wo r H"
using Well
proof(unfold wo_rel.adm_wo_def, clarify)
fix h1::"'a \<Rightarrow> 'a' * bool" and h2::"'a \<Rightarrow> 'a' * bool" and x
- assume "\<forall>y\<in>rel.underS r x. h1 y = h2 y"
- hence "\<forall>y\<in>rel.underS r x. (fst o h1) y = (fst o h2) y \<and>
+ assume "\<forall>y\<in>underS r x. h1 y = h2 y"
+ hence "\<forall>y\<in>underS r x. (fst o h1) y = (fst o h2) y \<and>
(snd o h1) y = (snd o h2) y" by auto
- hence "(fst o h1)`(rel.underS r x) = (fst o h2)`(rel.underS r x) \<and>
- (snd o h1)`(rel.underS r x) = (snd o h2)`(rel.underS r x)"
+ hence "(fst o h1)`(underS r x) = (fst o h2)`(underS r x) \<and>
+ (snd o h1)`(underS r x) = (snd o h2)`(underS r x)"
by (auto simp add: image_def)
thus "H h1 x = H h2 x" by (simp add: H_def del: not_False_in_image_Ball)
qed
@@ -729,21 +729,21 @@
where h_def: "h = wo_rel.worec r H" and
f_def: "f = fst o h" and g_def: "g = snd o h" by blast
obtain test where test_def:
- "test = (\<lambda> a. False \<notin> (g`(rel.underS r a)) \<and> f`(rel.underS r a) \<noteq> Field r')" by blast
+ "test = (\<lambda> a. False \<notin> (g`(underS r a)) \<and> f`(underS r a) \<noteq> Field r')" by blast
(* *)
have *: "\<And> a. h a = H h a"
using Adm Well wo_rel.worec_fixpoint[of r H] by (simp add: h_def)
have Main1:
- "\<And> a. (test a \<longrightarrow> f a = wo_rel.suc r' (f`(rel.underS r a)) \<and> g a = True) \<and>
+ "\<And> a. (test a \<longrightarrow> f a = wo_rel.suc r' (f`(underS r a)) \<and> g a = True) \<and>
(\<not>(test a) \<longrightarrow> g a = False)"
proof- (* How can I prove this withou fixing a? *)
- fix a show "(test a \<longrightarrow> f a = wo_rel.suc r' (f`(rel.underS r a)) \<and> g a = True) \<and>
+ fix a show "(test a \<longrightarrow> f a = wo_rel.suc r' (f`(underS r a)) \<and> g a = True) \<and>
(\<not>(test a) \<longrightarrow> g a = False)"
using *[of a] test_def f_def g_def H_def by auto
qed
(* *)
- let ?phi = "\<lambda> a. a \<in> Field r \<and> False \<notin> g`(rel.under r a) \<longrightarrow>
- bij_betw f (rel.under r a) (rel.under r' (f a))"
+ let ?phi = "\<lambda> a. a \<in> Field r \<and> False \<notin> g`(under r a) \<longrightarrow>
+ bij_betw f (under r a) (under r' (f a))"
have Main2: "\<And> a. ?phi a"
proof-
fix a show "?phi a"
@@ -752,46 +752,46 @@
fix a
assume IH: "\<forall>b. b \<noteq> a \<and> (b,a) \<in> r \<longrightarrow> ?phi b" and
*: "a \<in> Field r" and
- **: "False \<notin> g`(rel.under r a)"
- have 1: "\<forall>b \<in> rel.underS r a. bij_betw f (rel.under r b) (rel.under r' (f b))"
+ **: "False \<notin> g`(under r a)"
+ have 1: "\<forall>b \<in> underS r a. bij_betw f (under r b) (under r' (f b))"
proof(clarify)
- fix b assume ***: "b \<in> rel.underS r a"
- hence 0: "(b,a) \<in> r \<and> b \<noteq> a" unfolding rel.underS_def by auto
+ fix b assume ***: "b \<in> underS r a"
+ hence 0: "(b,a) \<in> r \<and> b \<noteq> a" unfolding underS_def by auto
moreover have "b \<in> Field r"
- using *** rel.underS_Field[of r a] by auto
- moreover have "False \<notin> g`(rel.under r b)"
- using 0 ** Trans rel.under_incr[of r b a] by auto
- ultimately show "bij_betw f (rel.under r b) (rel.under r' (f b))"
+ using *** underS_Field[of r a] by auto
+ moreover have "False \<notin> g`(under r b)"
+ using 0 ** Trans under_incr[of r b a] by auto
+ ultimately show "bij_betw f (under r b) (under r' (f b))"
using IH by auto
qed
(* *)
- have 21: "False \<notin> g`(rel.underS r a)"
- using ** rel.underS_subset_under[of r a] by auto
- have 22: "g`(rel.under r a) \<le> {True}" using ** by auto
- moreover have 23: "a \<in> rel.under r a"
- using Refl * by (auto simp add: rel.Refl_under_in)
+ have 21: "False \<notin> g`(underS r a)"
+ using ** underS_subset_under[of r a] by auto
+ have 22: "g`(under r a) \<le> {True}" using ** by auto
+ moreover have 23: "a \<in> under r a"
+ using Refl * by (auto simp add: Refl_under_in)
ultimately have 24: "g a = True" by blast
- have 2: "f`(rel.underS r a) \<noteq> Field r'"
+ have 2: "f`(underS r a) \<noteq> Field r'"
proof
- assume "f`(rel.underS r a) = Field r'"
+ assume "f`(underS r a) = Field r'"
hence "g a = False" using Main1 test_def by blast
with 24 show False using ** by blast
qed
(* *)
- have 3: "f a = wo_rel.suc r' (f`(rel.underS r a))"
+ have 3: "f a = wo_rel.suc r' (f`(underS r a))"
using 21 2 Main1 test_def by blast
(* *)
- show "bij_betw f (rel.under r a) (rel.under r' (f a))"
+ show "bij_betw f (under r a) (under r' (f a))"
using WELL WELL' 1 2 3 *
wellorders_totally_ordered_aux[of r r' a f] by auto
qed
qed
(* *)
- let ?chi = "(\<lambda> a. a \<in> Field r \<and> False \<in> g`(rel.under r a))"
+ let ?chi = "(\<lambda> a. a \<in> Field r \<and> False \<in> g`(under r a))"
show ?thesis
proof(cases "\<exists>a. ?chi a")
assume "\<not> (\<exists>a. ?chi a)"
- hence "\<forall>a \<in> Field r. bij_betw f (rel.under r a) (rel.under r' (f a))"
+ hence "\<forall>a \<in> Field r. bij_betw f (under r a) (under r' (f a))"
using Main2 by blast
thus ?thesis unfolding embed_def by blast
next
@@ -817,16 +817,16 @@
lemma embed_determined:
assumes WELL: "Well_order r" and WELL': "Well_order r'" and
EMB: "embed r r' f" and IN: "a \<in> Field r"
-shows "f a = wo_rel.suc r' (f`(rel.underS r a))"
+shows "f a = wo_rel.suc r' (f`(underS r a))"
proof-
- have "bij_betw f (rel.underS r a) (rel.underS r' (f a))"
+ have "bij_betw f (underS r a) (underS r' (f a))"
using assms by (auto simp add: embed_underS)
- hence "f`(rel.underS r a) = rel.underS r' (f a)"
+ hence "f`(underS r a) = underS r' (f a)"
by (auto simp add: bij_betw_def)
moreover
{have "f a \<in> Field r'" using IN
using EMB WELL embed_Field[of r r' f] by auto
- hence "f a = wo_rel.suc r' (rel.underS r' (f a))"
+ hence "f a = wo_rel.suc r' (underS r' (f a))"
using WELL' by (auto simp add: wo_rel_def wo_rel.suc_underS)
}
ultimately show ?thesis by simp
@@ -841,9 +841,9 @@
fix a
assume IH: "\<forall>b. b \<noteq> a \<and> (b,a): r \<longrightarrow> b \<in> Field r \<longrightarrow> f b = g b" and
*: "a \<in> Field r"
- hence "\<forall>b \<in> rel.underS r a. f b = g b"
- unfolding rel.underS_def by (auto simp add: Field_def)
- hence "f`(rel.underS r a) = g`(rel.underS r a)" by force
+ hence "\<forall>b \<in> underS r a. f b = g b"
+ unfolding underS_def by (auto simp add: Field_def)
+ hence "f`(underS r a) = g`(underS r a)" by force
thus "f a = g a"
using assms * embed_determined[of r r' f a] embed_determined[of r r' g a] by auto
qed
@@ -1083,28 +1083,28 @@
next
assume *: "bij_betw f (Field r) (Field r')" and
**: "\<forall>a\<in>Field r. \<forall>b\<in>Field r. ((a, b) \<in> r) = ((f a, f b) \<in> r')"
- have 1: "\<And> a. rel.under r a \<le> Field r \<and> rel.under r' (f a) \<le> Field r'"
- by (auto simp add: rel.under_Field)
+ have 1: "\<And> a. under r a \<le> Field r \<and> under r' (f a) \<le> Field r'"
+ by (auto simp add: under_Field)
have 2: "inj_on f (Field r)" using * by (auto simp add: bij_betw_def)
{fix a assume ***: "a \<in> Field r"
- have "bij_betw f (rel.under r a) (rel.under r' (f a))"
+ have "bij_betw f (under r a) (under r' (f a))"
proof(unfold bij_betw_def, auto)
- show "inj_on f (rel.under r a)"
+ show "inj_on f (under r a)"
using 1 2 by (metis subset_inj_on)
next
- fix b assume "b \<in> rel.under r a"
+ fix b assume "b \<in> under r a"
hence "a \<in> Field r \<and> b \<in> Field r \<and> (b,a) \<in> r"
- unfolding rel.under_def by (auto simp add: Field_def Range_def Domain_def)
- with 1 ** show "f b \<in> rel.under r' (f a)"
- unfolding rel.under_def by auto
+ unfolding under_def by (auto simp add: Field_def Range_def Domain_def)
+ with 1 ** show "f b \<in> under r' (f a)"
+ unfolding under_def by auto
next
- fix b' assume "b' \<in> rel.under r' (f a)"
- hence 3: "(b',f a) \<in> r'" unfolding rel.under_def by simp
+ fix b' assume "b' \<in> under r' (f a)"
+ hence 3: "(b',f a) \<in> r'" unfolding under_def by simp
hence "b' \<in> Field r'" unfolding Field_def by auto
with * obtain b where "b \<in> Field r \<and> f b = b'"
unfolding bij_betw_def by force
with 3 ** ***
- show "b' \<in> f ` (rel.under r a)" unfolding rel.under_def by blast
+ show "b' \<in> f ` (under r a)" unfolding under_def by blast
qed
}
thus "embed r r' f" unfolding embed_def using * by auto
--- a/src/HOL/Cardinals/Wellorder_Extension.thy Thu Jan 16 18:52:50 2014 +0100
+++ b/src/HOL/Cardinals/Wellorder_Extension.thy Thu Jan 16 20:52:54 2014 +0100
@@ -178,7 +178,7 @@
where "p \<subseteq> w" and wo: "Well_order w" by blast
let ?A = "UNIV - Field w"
from well_order_on [of ?A] obtain w' where wo': "well_order_on ?A w'" ..
- have [simp]: "Field w' = ?A" using rel.well_order_on_Well_order [OF wo'] by simp
+ have [simp]: "Field w' = ?A" using well_order_on_Well_order [OF wo'] by simp
have *: "Field w \<inter> Field w' = {}" by simp
let ?w = "w \<union>o w'"
have "p \<subseteq> ?w" using `p \<subseteq> w` by (auto simp: Osum_def)
--- a/src/HOL/Cardinals/Wellorder_Relation.thy Thu Jan 16 18:52:50 2014 +0100
+++ b/src/HOL/Cardinals/Wellorder_Relation.thy Thu Jan 16 20:52:54 2014 +0100
@@ -37,7 +37,7 @@
proof-
have "adm_wf (r - Id) H"
unfolding adm_wf_def
- using ADM adm_wo_def[of H] underS_def by auto
+ using ADM adm_wo_def[of H] underS_def[of r] by auto
hence "f = wfrec (r - Id) H"
using fp WF wfrec_unique_fixpoint[of "r - Id" H] by simp
thus ?thesis unfolding worec_def .
@@ -97,7 +97,7 @@
have "Under A \<le> under (minim A)"
proof
fix x assume "x \<in> Under A"
- with 1 Under_def have "(x,minim A) \<in> r" by auto
+ with 1 Under_def[of r] have "(x,minim A) \<in> r" by auto
thus "x \<in> under(minim A)" unfolding under_def by simp
qed
(* *)
@@ -133,7 +133,7 @@
have "UnderS A \<le> underS (minim A)"
proof
fix x assume "x \<in> UnderS A"
- with 1 UnderS_def have "x \<noteq> minim A \<and> (x,minim A) \<in> r" by auto
+ with 1 UnderS_def[of r] have "x \<noteq> minim A \<and> (x,minim A) \<in> r" by auto
thus "x \<in> underS(minim A)" unfolding underS_def by simp
qed
(* *)
@@ -173,7 +173,7 @@
shows "supr B \<in> Above B"
proof(unfold supr_def)
have "Above B \<le> Field r"
- using Above_Field by auto
+ using Above_Field[of r] by auto
thus "minim (Above B) \<in> Above B"
using assms by (simp add: minim_in)
qed
@@ -185,7 +185,7 @@
proof-
from assms supr_Above
have "supr B \<in> Above B" by simp
- with IN Above_def show ?thesis by simp
+ with IN Above_def[of r] show ?thesis by simp
qed
lemma supr_least_Above:
@@ -194,7 +194,7 @@
shows "(supr B, a) \<in> r"
proof(unfold supr_def)
have "Above B \<le> Field r"
- using Above_Field by auto
+ using Above_Field[of r] by auto
thus "(minim (Above B), a) \<in> r"
using assms minim_least
by simp
@@ -211,7 +211,7 @@
shows "a = supr B"
proof(unfold supr_def)
have "Above B \<le> Field r"
- using Above_Field by auto
+ using Above_Field[of r] by auto
thus "a = minim (Above B)"
using assms equals_minim by simp
qed
@@ -236,7 +236,7 @@
shows "supr B \<in> Field r"
proof-
have "supr B \<in> Above B" using supr_Above assms by simp
- thus ?thesis using assms Above_Field by auto
+ thus ?thesis using assms Above_Field[of r] by auto
qed
lemma supr_above_Above:
@@ -264,13 +264,13 @@
shows "a = supr (under a)"
proof-
have "under a \<le> Field r"
- using under_Field by auto
+ using under_Field[of r] by auto
moreover
have "under a \<noteq> {}"
- using IN Refl_under_in REFL by auto
+ using IN Refl_under_in[of r] REFL by auto
moreover
have "a \<in> Above (under a)"
- using in_Above_under IN by auto
+ using in_Above_under[of _ r] IN by auto
moreover
have "\<forall>a' \<in> Above (under a). (a,a') \<in> r"
proof(unfold Above_def under_def, auto)
@@ -347,7 +347,7 @@
shows "a' = a \<or> (a',a) \<in> r"
proof-
have *: "suc {a} \<in> Field r \<and> a' \<in> Field r"
- using WELL REL well_order_on_domain by auto
+ using WELL REL well_order_on_domain by metis
{assume **: "a' \<noteq> a"
hence "(a,a') \<in> r \<or> (a',a) \<in> r"
using TOTAL IN * by (auto simp add: total_on_def)
@@ -369,7 +369,7 @@
shows "underS (suc {a}) = under a"
proof-
have 1: "AboveS {a} \<noteq> {}"
- using ABV aboveS_AboveS_singl by auto
+ using ABV aboveS_AboveS_singl[of r] by auto
have 2: "a \<noteq> suc {a} \<and> (a,suc {a}) \<in> r"
using suc_greater[of "{a}" a] IN 1 by auto
(* *)
@@ -408,12 +408,12 @@
proof(unfold ofilter_def, auto)
fix x assume "x \<in> Under A"
thus "x \<in> Field r"
- using Under_Field assms by auto
+ using Under_Field[of r] assms by auto
next
fix a x
assume "a \<in> Under A" and "x \<in> under a"
thus "x \<in> Under A"
- using TRANS under_Under_trans by auto
+ using TRANS under_Under_trans[of r] by auto
qed
lemma ofilter_UnderS[simp]:
@@ -422,12 +422,12 @@
proof(unfold ofilter_def, auto)
fix x assume "x \<in> UnderS A"
thus "x \<in> Field r"
- using UnderS_Field assms by auto
+ using UnderS_Field[of r] assms by auto
next
fix a x
assume "a \<in> UnderS A" and "x \<in> under a"
thus "x \<in> UnderS A"
- using TRANS ANTISYM under_UnderS_trans by auto
+ using TRANS ANTISYM under_UnderS_trans[of r] by auto
qed
lemma ofilter_Int[simp]: "\<lbrakk>ofilter A; ofilter B\<rbrakk> \<Longrightarrow> ofilter(A Int B)"
@@ -469,7 +469,7 @@
(* Main proof *)
fix x assume "x \<in> Under(Under A)"
with 1 have 1: "(x,minim A) \<in> r"
- using Under_def by auto
+ using Under_def[of r] by auto
with Field_def have "x \<in> Field r" by fastforce
moreover
{fix y assume *: "y \<in> A"
@@ -506,7 +506,7 @@
hence "(suc A,x) \<in> r"
using suc_least_AboveS by auto
moreover
- have "(x,suc A) \<in> r" using * under_def by auto
+ have "(x,suc A) \<in> r" using * under_def[of r] by auto
ultimately show "x = suc A"
using ANTISYM antisym_def[of r] by auto
qed
--- a/src/HOL/Cardinals/Wellorder_Relation_FP.thy Thu Jan 16 18:52:50 2014 +0100
+++ b/src/HOL/Cardinals/Wellorder_Relation_FP.thy Thu Jan 16 20:52:54 2014 +0100
@@ -18,7 +18,9 @@
i.e., as containing the diagonals of their fields. *}
-locale wo_rel = rel + assumes WELL: "Well_order r"
+locale wo_rel =
+ fixes r :: "'a rel"
+ assumes WELL: "Well_order r"
begin
text{* The following context encompasses all this section. In other words,
@@ -26,6 +28,15 @@
(* context wo_rel *)
+abbreviation under where "under \<equiv> Order_Relation_More_FP.under r"
+abbreviation underS where "underS \<equiv> Order_Relation_More_FP.underS r"
+abbreviation Under where "Under \<equiv> Order_Relation_More_FP.Under r"
+abbreviation UnderS where "UnderS \<equiv> Order_Relation_More_FP.UnderS r"
+abbreviation above where "above \<equiv> Order_Relation_More_FP.above r"
+abbreviation aboveS where "aboveS \<equiv> Order_Relation_More_FP.aboveS r"
+abbreviation Above where "Above \<equiv> Order_Relation_More_FP.Above r"
+abbreviation AboveS where "AboveS \<equiv> Order_Relation_More_FP.AboveS r"
+
subsection {* Auxiliaries *}
@@ -109,7 +120,7 @@
let ?rS = "r - Id"
have "adm_wf (r - Id) H"
unfolding adm_wf_def
- using ADM adm_wo_def[of H] underS_def by auto
+ using ADM adm_wo_def[of H] underS_def[of r] by auto
hence "wfrec ?rS H = H (wfrec ?rS H)"
using WF wfrec_fixpoint[of ?rS H] by simp
thus ?thesis unfolding worec_def .
@@ -327,7 +338,7 @@
shows "suc B \<in> AboveS B"
proof(unfold suc_def)
have "AboveS B \<le> Field r"
- using AboveS_Field by auto
+ using AboveS_Field[of r] by auto
thus "minim (AboveS B) \<in> AboveS B"
using assms by (simp add: minim_in)
qed
@@ -340,7 +351,7 @@
proof-
from assms suc_AboveS
have "suc B \<in> AboveS B" by simp
- with IN AboveS_def show ?thesis by simp
+ with IN AboveS_def[of r] show ?thesis by simp
qed
@@ -349,7 +360,7 @@
shows "(suc B,a) \<in> r"
proof(unfold suc_def)
have "AboveS B \<le> Field r"
- using AboveS_Field by auto
+ using AboveS_Field[of r] by auto
thus "(minim (AboveS B),a) \<in> r"
using assms minim_least by simp
qed
@@ -361,7 +372,7 @@
proof-
have "suc B \<in> AboveS B" using suc_AboveS assms by simp
thus ?thesis
- using assms AboveS_Field by auto
+ using assms AboveS_Field[of r] by auto
qed
@@ -371,7 +382,7 @@
shows "a = suc B"
proof(unfold suc_def)
have "AboveS B \<le> Field r"
- using AboveS_Field[of B] by auto
+ using AboveS_Field[of r B] by auto
thus "a = minim (AboveS B)"
using assms equals_minim
by simp
@@ -383,17 +394,17 @@
shows "a = suc (underS a)"
proof-
have "underS a \<le> Field r"
- using underS_Field by auto
+ using underS_Field[of r] by auto
moreover
have "a \<in> AboveS (underS a)"
- using in_AboveS_underS IN by auto
+ using in_AboveS_underS IN by fast
moreover
have "\<forall>a' \<in> AboveS (underS a). (a,a') \<in> r"
proof(clarify)
fix a'
assume *: "a' \<in> AboveS (underS a)"
hence **: "a' \<in> Field r"
- using AboveS_Field by auto
+ using AboveS_Field by fast
{assume "(a,a') \<notin> r"
hence "a' = a \<or> (a',a) \<in> r"
using TOTAL IN ** by (auto simp add: total_on_def)
@@ -407,7 +418,7 @@
hence "a' \<in> underS a"
unfolding underS_def by simp
hence "a' \<notin> AboveS (underS a)"
- using AboveS_disjoint by blast
+ using AboveS_disjoint by fast
with * have False by simp
}
ultimately have "(a,a') \<in> r" by blast
@@ -486,7 +497,7 @@
hence "(?a,x) \<in> r"
using TOTAL total_on_def[of "Field r" r]
2 4 11 12 by auto
- hence "?a \<in> under x" using under_def by auto
+ hence "?a \<in> under x" using under_def[of r] by auto
hence "?a \<in> A" using ** 13 by blast
with 4 have False by simp
}
@@ -527,7 +538,7 @@
thus "(\<Union> a \<in> A. under a) \<le> A" by blast
next
have "\<forall>a \<in> A. a \<in> under a"
- using REFL Refl_under_in assms ofilter_def by blast
+ using REFL Refl_under_in[of r] assms ofilter_def[of A] by blast
thus "A \<le> (\<Union> a \<in> A. under a)" by blast
qed
@@ -562,13 +573,13 @@
}
moreover
{assume "(a,b) \<in> r"
- with underS_incr TRANS ANTISYM 1 2
+ with underS_incr[of r] TRANS ANTISYM 1 2
have "A \<le> B" by auto
hence ?thesis by auto
}
moreover
{assume "(b,a) \<in> r"
- with underS_incr TRANS ANTISYM 1 2
+ with underS_incr[of r] TRANS ANTISYM 1 2
have "B \<le> A" by auto
hence ?thesis by auto
}
@@ -582,7 +593,7 @@
shows "A \<union> (AboveS A) = Field r"
proof
show "A \<union> (AboveS A) \<le> Field r"
- using assms ofilter_def AboveS_Field by auto
+ using assms ofilter_def AboveS_Field[of r] by auto
next
{fix x assume *: "x \<in> Field r" and **: "x \<notin> A"
{fix y assume ***: "y \<in> A"
@@ -592,7 +603,7 @@
have "y \<in> Field r" using assms ofilter_def *** by auto
ultimately have "(x,y) \<in> r"
using 1 * TOTAL total_on_def[of _ r] by auto
- with *** assms ofilter_def under_def have "x \<in> A" by auto
+ with *** assms ofilter_def under_def[of r] have "x \<in> A" by auto
with ** have False by contradiction
}
hence "(y,x) \<in> r" by blast
@@ -610,7 +621,7 @@
shows "b \<in> A"
proof-
have *: "suc A \<in> Field r \<and> b \<in> Field r"
- using WELL REL well_order_on_domain by auto
+ using WELL REL well_order_on_domain[of "Field r"] by auto
{assume **: "b \<notin> A"
hence "b \<in> AboveS A"
using OF * ofilter_AboveS_Field by auto