get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
authorblanchet
Thu Jan 16 20:52:54 2014 +0100 (2014-01-16)
changeset 5502338db7814481d
parent 55022 eeba3ba73486
child 55024 05cc0dbf3a50
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
src/HOL/BNF/BNF_LFP.thy
src/HOL/BNF/Tools/bnf_lfp_util.ML
src/HOL/Cardinals/Cardinal_Order_Relation.thy
src/HOL/Cardinals/Cardinal_Order_Relation_FP.thy
src/HOL/Cardinals/Constructions_on_Wellorders.thy
src/HOL/Cardinals/Constructions_on_Wellorders_FP.thy
src/HOL/Cardinals/Order_Relation_More.thy
src/HOL/Cardinals/Order_Relation_More_FP.thy
src/HOL/Cardinals/Ordinal_Arithmetic.thy
src/HOL/Cardinals/Wellfounded_More_FP.thy
src/HOL/Cardinals/Wellorder_Embedding.thy
src/HOL/Cardinals/Wellorder_Embedding_FP.thy
src/HOL/Cardinals/Wellorder_Extension.thy
src/HOL/Cardinals/Wellorder_Relation.thy
src/HOL/Cardinals/Wellorder_Relation_FP.thy
     1.1 --- a/src/HOL/BNF/BNF_LFP.thy	Thu Jan 16 18:52:50 2014 +0100
     1.2 +++ b/src/HOL/BNF/BNF_LFP.thy	Thu Jan 16 20:52:54 2014 +0100
     1.3 @@ -30,14 +30,14 @@
     1.4  lemma prop_restrict: "\<lbrakk>x \<in> Z; Z \<subseteq> {x. x \<in> X \<and> P x}\<rbrakk> \<Longrightarrow> P x"
     1.5  by auto
     1.6  
     1.7 -lemma underS_I: "\<lbrakk>i \<noteq> j; (i, j) \<in> R\<rbrakk> \<Longrightarrow> i \<in> rel.underS R j"
     1.8 -unfolding rel.underS_def by simp
     1.9 +lemma underS_I: "\<lbrakk>i \<noteq> j; (i, j) \<in> R\<rbrakk> \<Longrightarrow> i \<in> underS R j"
    1.10 +unfolding underS_def by simp
    1.11  
    1.12 -lemma underS_E: "i \<in> rel.underS R j \<Longrightarrow> i \<noteq> j \<and> (i, j) \<in> R"
    1.13 -unfolding rel.underS_def by simp
    1.14 +lemma underS_E: "i \<in> underS R j \<Longrightarrow> i \<noteq> j \<and> (i, j) \<in> R"
    1.15 +unfolding underS_def by simp
    1.16  
    1.17 -lemma underS_Field: "i \<in> rel.underS R j \<Longrightarrow> i \<in> Field R"
    1.18 -unfolding rel.underS_def Field_def by auto
    1.19 +lemma underS_Field: "i \<in> underS R j \<Longrightarrow> i \<in> Field R"
    1.20 +unfolding underS_def Field_def by auto
    1.21  
    1.22  lemma FieldI2: "(i, j) \<in> R \<Longrightarrow> j \<in> Field R"
    1.23  unfolding Field_def by auto
     2.1 --- a/src/HOL/BNF/Tools/bnf_lfp_util.ML	Thu Jan 16 18:52:50 2014 +0100
     2.2 +++ b/src/HOL/BNF/Tools/bnf_lfp_util.ML	Thu Jan 16 20:52:54 2014 +0100
     2.3 @@ -34,7 +34,7 @@
     2.4  
     2.5  fun mk_underS r =
     2.6    let val T = fst (dest_relT (fastype_of r));
     2.7 -  in Const (@{const_name rel.underS}, mk_relT (T, T) --> T --> HOLogic.mk_setT T) $ r end;
     2.8 +  in Const (@{const_name underS}, mk_relT (T, T) --> T --> HOLogic.mk_setT T) $ r end;
     2.9  
    2.10  fun mk_worec r f =
    2.11    let val (A, AB) = apfst domain_type (dest_funT (fastype_of f));
     3.1 --- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Thu Jan 16 18:52:50 2014 +0100
     3.2 +++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Thu Jan 16 20:52:54 2014 +0100
     3.3 @@ -1012,11 +1012,11 @@
     3.4  
     3.5  lemma natLeq_ofilter_less: "ofilter natLeq {0 ..< n}"
     3.6  by(auto simp add: natLeq_wo_rel wo_rel.ofilter_def,
     3.7 -   simp add: Field_natLeq, unfold rel.under_def, auto)
     3.8 +   simp add: Field_natLeq, unfold under_def, auto)
     3.9  
    3.10  lemma natLeq_ofilter_leq: "ofilter natLeq {0 .. n}"
    3.11  by(auto simp add: natLeq_wo_rel wo_rel.ofilter_def,
    3.12 -   simp add: Field_natLeq, unfold rel.under_def, auto)
    3.13 +   simp add: Field_natLeq, unfold under_def, auto)
    3.14  
    3.15  lemma natLeq_UNIV_ofilter: "wo_rel.ofilter natLeq UNIV"
    3.16  using natLeq_wo_rel Field_natLeq wo_rel.Field_ofilter[of natLeq] by auto
    3.17 @@ -1047,7 +1047,7 @@
    3.18  proof(rule iffI)
    3.19    assume "ofilter natLeq A"
    3.20    hence "\<forall>m n. n \<in> A \<and> m \<le> n \<longrightarrow> m \<in> A"
    3.21 -  by(auto simp add: natLeq_wo_rel wo_rel.ofilter_def rel.under_def)
    3.22 +  by(auto simp add: natLeq_wo_rel wo_rel.ofilter_def under_def)
    3.23    thus "A = UNIV \<or> (\<exists>n. A = {0 ..< n})" using closed_nat_set_iff by blast
    3.24  next
    3.25    assume "A = UNIV \<or> (\<exists>n. A = {0 ..< n})"
    3.26 @@ -1056,22 +1056,22 @@
    3.27  qed
    3.28  
    3.29  lemma natLeq_under_leq: "under natLeq n = {0 .. n}"
    3.30 -unfolding rel.under_def by auto
    3.31 +unfolding under_def by auto
    3.32  
    3.33  lemma natLeq_on_ofilter_less_eq:
    3.34  "n \<le> m \<Longrightarrow> wo_rel.ofilter (natLeq_on m) {0 ..< n}"
    3.35  apply (auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def)
    3.36  apply (simp add: Field_natLeq_on)
    3.37 -by (auto simp add: rel.under_def)
    3.38 +by (auto simp add: under_def)
    3.39  
    3.40  lemma natLeq_on_ofilter_iff:
    3.41  "wo_rel.ofilter (natLeq_on m) A = (\<exists>n \<le> m. A = {0 ..< n})"
    3.42  proof(rule iffI)
    3.43    assume *: "wo_rel.ofilter (natLeq_on m) A"
    3.44    hence 1: "A \<le> {0..<m}"
    3.45 -  by (auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def rel.under_def Field_natLeq_on)
    3.46 +  by (auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def under_def Field_natLeq_on)
    3.47    hence "\<forall>n1 n2. n2 \<in> A \<and> n1 \<le> n2 \<longrightarrow> n1 \<in> A"
    3.48 -  using * by(fastforce simp add: natLeq_on_wo_rel wo_rel.ofilter_def rel.under_def)
    3.49 +  using * by(fastforce simp add: natLeq_on_wo_rel wo_rel.ofilter_def under_def)
    3.50    hence "A = UNIV \<or> (\<exists>n. A = {0 ..< n})" using closed_nat_set_iff by blast
    3.51    thus "\<exists>n \<le> m. A = {0 ..< n}" using 1 atLeastLessThan_less_eq by blast
    3.52  next
    3.53 @@ -1086,7 +1086,7 @@
    3.54  lemma natLeq_on_ofilter_less:
    3.55  "n < m \<Longrightarrow> ofilter (natLeq_on m) {0 .. n}"
    3.56  by(auto simp add: natLeq_on_wo_rel wo_rel.ofilter_def,
    3.57 -   simp add: Field_natLeq_on, unfold rel.under_def, auto)
    3.58 +   simp add: Field_natLeq_on, unfold under_def, auto)
    3.59  
    3.60  lemma natLeq_on_ordLess_natLeq: "natLeq_on n <o natLeq"
    3.61  using Field_natLeq Field_natLeq_on[of n]
    3.62 @@ -1331,13 +1331,13 @@
    3.63  lemma under_mono[simp]:
    3.64  assumes "Well_order r" and "(i,j) \<in> r"
    3.65  shows "under r i \<subseteq> under r j"
    3.66 -using assms unfolding rel.under_def order_on_defs
    3.67 +using assms unfolding under_def order_on_defs
    3.68  trans_def by blast
    3.69  
    3.70  lemma underS_under:
    3.71  assumes "i \<in> Field r"
    3.72  shows "underS r i = under r i - {i}"
    3.73 -using assms unfolding rel.underS_def rel.under_def by auto
    3.74 +using assms unfolding underS_def under_def by auto
    3.75  
    3.76  lemma relChain_under:
    3.77  assumes "Well_order r"
    3.78 @@ -1593,7 +1593,7 @@
    3.79      unfolding p_def apply(rule Refl_Field_Restr2[OF rr]) by auto
    3.80      have of: "ofilter r (Field p)" unfolding wo_rel.ofilter_def[OF 0] proof safe
    3.81        fix a x assume a: "a \<in> Field p" and "x \<in> under r a"
    3.82 -      hence x: "(x,a) \<in> r" "x \<in> Field r" unfolding rel.under_def Field_def by auto
    3.83 +      hence x: "(x,a) \<in> r" "x \<in> Field r" unfolding under_def Field_def by auto
    3.84        moreover have a: "a \<noteq> j" "a \<in> Field r" "(a,j) \<in> r" using a jm  unfolding fp by auto
    3.85        ultimately have "x \<noteq> j" using j jm  by (metis 0 wo_rel.max2_def wo_rel.max2_equals1)
    3.86        thus "x \<in> Field p" using x unfolding fp by auto
    3.87 @@ -1654,7 +1654,7 @@
    3.88      hence "As (succ r i) \<subseteq> As j" using rc unfolding relChain_def by auto
    3.89      moreover
    3.90      {have "(i,succ r i) \<in> r" apply(rule wo_rel.succ_in[OF 0])
    3.91 -     using 1 unfolding rel.aboveS_def by auto
    3.92 +     using 1 unfolding aboveS_def by auto
    3.93       hence "As i \<subset> As (succ r i)" using As_s rc rij unfolding relChain_def Field_def by auto
    3.94      }
    3.95      ultimately show False unfolding Asij by auto
    3.96 @@ -1721,13 +1721,13 @@
    3.97     def g \<equiv> "\<lambda> a. if F a \<noteq> {} then gg a else j0"
    3.98     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
    3.99     hence 1: "Field r \<subseteq> (\<Union> a \<in> A. under r (g a))"
   3.100 -   using f[symmetric] unfolding rel.under_def image_def by auto
   3.101 +   using f[symmetric] unfolding under_def image_def by auto
   3.102     have gA: "g ` A \<subseteq> Field r" using gg j0 unfolding Field_def g_def by auto
   3.103     moreover have "cofinal (g ` A) r" unfolding cofinal_def proof safe
   3.104       fix i assume "i \<in> Field r"
   3.105       then obtain j where ij: "(i,j) \<in> r" "i \<noteq> j" using cr ir by (metis infinite_Card_order_limit)
   3.106 -     hence "j \<in> Field r" by (metis card_order_on_def cr rel.well_order_on_domain)
   3.107 -     then obtain a where a: "a \<in> A" and j: "(j, g a) \<in> r" using 1 unfolding rel.under_def by auto
   3.108 +     hence "j \<in> Field r" by (metis card_order_on_def cr well_order_on_domain)
   3.109 +     then obtain a where a: "a \<in> A" and j: "(j, g a) \<in> r" using 1 unfolding under_def by auto
   3.110       hence "(i, g a) \<in> r" using ij wo_rel.TRANS[OF r] unfolding trans_def by blast
   3.111       moreover have "i \<noteq> g a"
   3.112       using ij j r unfolding wo_rel_def unfolding well_order_on_def linear_order_on_def
   3.113 @@ -1752,7 +1752,7 @@
   3.114    {assume Kr: "|K| <o r"
   3.115     then obtain f where "\<forall> a \<in> Field r. f a \<in> K \<and> a \<noteq> f a \<and> (a, f a) \<in> r"
   3.116     using cof unfolding cofinal_def by metis
   3.117 -   hence "Field r \<subseteq> (\<Union> a \<in> K. underS r a)" unfolding rel.underS_def by auto
   3.118 +   hence "Field r \<subseteq> (\<Union> a \<in> K. underS r a)" unfolding underS_def by auto
   3.119     hence "r \<le>o |\<Union> a \<in> K. underS r a|" using cr
   3.120     by (metis Card_order_iff_ordLeq_card_of card_of_mono1 ordLeq_transitive)
   3.121     also have "|\<Union> a \<in> K. underS r a| \<le>o |SIGMA a: K. underS r a|" by (rule card_of_UNION_Sigma)
     4.1 --- a/src/HOL/Cardinals/Cardinal_Order_Relation_FP.thy	Thu Jan 16 18:52:50 2014 +0100
     4.2 +++ b/src/HOL/Cardinals/Cardinal_Order_Relation_FP.thy	Thu Jan 16 20:52:54 2014 +0100
     4.3 @@ -59,7 +59,7 @@
     4.4  
     4.5  lemma card_order_on_Card_order:
     4.6  "card_order_on A r \<Longrightarrow> A = Field r \<and> Card_order r"
     4.7 -unfolding card_order_on_def using rel.well_order_on_Field by blast
     4.8 +unfolding card_order_on_def using well_order_on_Field by blast
     4.9  
    4.10  
    4.11  text{* The existence of a cardinal relation on any given set (which will mean
    4.12 @@ -77,7 +77,7 @@
    4.13  proof-
    4.14    obtain R where R_def: "R = {r. well_order_on A r}" by blast
    4.15    have 1: "R \<noteq> {} \<and> (\<forall>r \<in> R. Well_order r)"
    4.16 -  using well_order_on[of A] R_def rel.well_order_on_Well_order by blast
    4.17 +  using well_order_on[of A] R_def well_order_on_Well_order by blast
    4.18    hence "\<exists>r \<in> R. \<forall>r' \<in> R. r \<le>o r'"
    4.19    using  exists_minim_Well_order[of R] by auto
    4.20    thus ?thesis using R_def unfolding card_order_on_def by auto
    4.21 @@ -98,7 +98,7 @@
    4.22  proof(unfold card_order_on_def, auto)
    4.23    fix p' assume "well_order_on (Field r') p'"
    4.24    hence 0: "Well_order p' \<and> Field p' = Field r'"
    4.25 -  using rel.well_order_on_Well_order by blast
    4.26 +  using well_order_on_Well_order by blast
    4.27    obtain f where 1: "iso r' r f" and 2: "Well_order r \<and> Well_order r'"
    4.28    using ISO unfolding ordIso_def by auto
    4.29    hence 3: "inj_on f (Field r') \<and> f ` (Field r') = Field r"
    4.30 @@ -143,7 +143,7 @@
    4.31  
    4.32  lemma Field_card_of: "Field |A| = A"
    4.33  using card_of_card_order_on[of A] unfolding card_order_on_def
    4.34 -using rel.well_order_on_Field by blast
    4.35 +using well_order_on_Field by blast
    4.36  
    4.37  
    4.38  lemma card_of_Card_order: "Card_order |A|"
    4.39 @@ -273,7 +273,7 @@
    4.40    obtain f where
    4.41    1: "well_order_on (Field r) r \<and> well_order_on (Field r) r \<and> embed r r' f"
    4.42    using assms unfolding ordLeq_def
    4.43 -  by (auto simp add: rel.well_order_on_Well_order)
    4.44 +  by (auto simp add: well_order_on_Well_order)
    4.45    hence "inj_on f (Field r) \<and> f ` (Field r) \<le> Field r'"
    4.46    by (auto simp add: embed_inj_on embed_Field)
    4.47    thus "|Field r| \<le>o |Field r'|" using card_of_ordLeq by blast
    4.48 @@ -285,7 +285,7 @@
    4.49  
    4.50  
    4.51  lemma card_of_Field_ordLess: "Well_order r \<Longrightarrow> |Field r| \<le>o r"
    4.52 -using card_of_least card_of_well_order_on rel.well_order_on_Well_order by blast
    4.53 +using card_of_least card_of_well_order_on well_order_on_Well_order by blast
    4.54  
    4.55  
    4.56  lemma card_of_Field_ordIso:
    4.57 @@ -321,16 +321,16 @@
    4.58  
    4.59  lemma Card_order_iff_Restr_underS:
    4.60  assumes "Well_order r"
    4.61 -shows "Card_order r = (\<forall>a \<in> Field r. Restr r (rel.underS r a) <o |Field r| )"
    4.62 +shows "Card_order r = (\<forall>a \<in> Field r. Restr r (underS r a) <o |Field r| )"
    4.63  using assms unfolding Card_order_iff_ordLeq_card_of
    4.64  using ordLeq_iff_ordLess_Restr card_of_Well_order by blast
    4.65  
    4.66  
    4.67  lemma card_of_underS:
    4.68  assumes r: "Card_order r" and a: "a : Field r"
    4.69 -shows "|rel.underS r a| <o r"
    4.70 +shows "|underS r a| <o r"
    4.71  proof-
    4.72 -  let ?A = "rel.underS r a"  let ?r' = "Restr r ?A"
    4.73 +  let ?A = "underS r a"  let ?r' = "Restr r ?A"
    4.74    have 1: "Well_order r"
    4.75    using r unfolding card_order_on_def by simp
    4.76    have "Well_order ?r'" using 1 Well_order_Restr by auto
    4.77 @@ -355,7 +355,7 @@
    4.78  shows "|Field r| <o r'"
    4.79  proof-
    4.80    have "well_order_on (Field r) r" using assms unfolding ordLess_def
    4.81 -  by (auto simp add: rel.well_order_on_Well_order)
    4.82 +  by (auto simp add: well_order_on_Well_order)
    4.83    hence "|Field r| \<le>o r" using card_of_least by blast
    4.84    thus ?thesis using assms ordLeq_ordLess_trans by blast
    4.85  qed
    4.86 @@ -937,35 +937,35 @@
    4.87  
    4.88  lemma Card_order_infinite_not_under:
    4.89  assumes CARD: "Card_order r" and INF: "\<not>finite (Field r)"
    4.90 -shows "\<not> (\<exists>a. Field r = rel.under r a)"
    4.91 +shows "\<not> (\<exists>a. Field r = under r a)"
    4.92  proof(auto)
    4.93    have 0: "Well_order r \<and> wo_rel r \<and> Refl r"
    4.94    using CARD unfolding wo_rel_def card_order_on_def order_on_defs by auto
    4.95 -  fix a assume *: "Field r = rel.under r a"
    4.96 +  fix a assume *: "Field r = under r a"
    4.97    show False
    4.98    proof(cases "a \<in> Field r")
    4.99      assume Case1: "a \<notin> Field r"
   4.100 -    hence "rel.under r a = {}" unfolding Field_def rel.under_def by auto
   4.101 +    hence "under r a = {}" unfolding Field_def under_def by auto
   4.102      thus False using INF *  by auto
   4.103    next
   4.104 -    let ?r' = "Restr r (rel.underS r a)"
   4.105 +    let ?r' = "Restr r (underS r a)"
   4.106      assume Case2: "a \<in> Field r"
   4.107 -    hence 1: "rel.under r a = rel.underS r a \<union> {a} \<and> a \<notin> rel.underS r a"
   4.108 -    using 0 rel.Refl_under_underS rel.underS_notIn by metis
   4.109 -    have 2: "wo_rel.ofilter r (rel.underS r a) \<and> rel.underS r a < Field r"
   4.110 +    hence 1: "under r a = underS r a \<union> {a} \<and> a \<notin> underS r a"
   4.111 +    using 0 Refl_under_underS underS_notIn by metis
   4.112 +    have 2: "wo_rel.ofilter r (underS r a) \<and> underS r a < Field r"
   4.113      using 0 wo_rel.underS_ofilter * 1 Case2 by fast
   4.114      hence "?r' <o r" using 0 using ofilter_ordLess by blast
   4.115      moreover
   4.116 -    have "Field ?r' = rel.underS r a \<and> Well_order ?r'"
   4.117 +    have "Field ?r' = underS r a \<and> Well_order ?r'"
   4.118      using  2 0 Field_Restr_ofilter[of r] Well_order_Restr[of r] by blast
   4.119 -    ultimately have "|rel.underS r a| <o r" using ordLess_Field[of ?r'] by auto
   4.120 -    moreover have "|rel.under r a| =o r" using * CARD card_of_Field_ordIso[of r] by auto
   4.121 -    ultimately have "|rel.underS r a| <o |rel.under r a|"
   4.122 +    ultimately have "|underS r a| <o r" using ordLess_Field[of ?r'] by auto
   4.123 +    moreover have "|under r a| =o r" using * CARD card_of_Field_ordIso[of r] by auto
   4.124 +    ultimately have "|underS r a| <o |under r a|"
   4.125      using ordIso_symmetric ordLess_ordIso_trans by blast
   4.126      moreover
   4.127 -    {have "\<exists>f. bij_betw f (rel.under r a) (rel.underS r a)"
   4.128 +    {have "\<exists>f. bij_betw f (under r a) (underS r a)"
   4.129       using infinite_imp_bij_betw[of "Field r" a] INF * 1 by auto
   4.130 -     hence "|rel.under r a| =o |rel.underS r a|" using card_of_ordIso by blast
   4.131 +     hence "|under r a| =o |underS r a|" using card_of_ordIso by blast
   4.132      }
   4.133      ultimately show False using not_ordLess_ordIso ordIso_symmetric by blast
   4.134    qed
   4.135 @@ -977,13 +977,13 @@
   4.136  and a: "a : Field r"
   4.137  shows "EX b : Field r. a \<noteq> b \<and> (a,b) : r"
   4.138  proof-
   4.139 -  have "Field r \<noteq> rel.under r a"
   4.140 +  have "Field r \<noteq> under r a"
   4.141    using assms Card_order_infinite_not_under by blast
   4.142 -  moreover have "rel.under r a \<le> Field r"
   4.143 -  using rel.under_Field .
   4.144 -  ultimately have "rel.under r a < Field r" by blast
   4.145 +  moreover have "under r a \<le> Field r"
   4.146 +  using under_Field .
   4.147 +  ultimately have "under r a < Field r" by blast
   4.148    then obtain b where 1: "b : Field r \<and> ~ (b,a) : r"
   4.149 -  unfolding rel.under_def by blast
   4.150 +  unfolding under_def by blast
   4.151    moreover have ba: "b \<noteq> a"
   4.152    using 1 r unfolding card_order_on_def well_order_on_def
   4.153    linear_order_on_def partial_order_on_def preorder_on_def refl_on_def by auto
   4.154 @@ -1036,7 +1036,7 @@
   4.155      using 7 unfolding bij_betw_def using 6 3 embed_inj_on 4 by auto
   4.156      hence temp2: "wo_rel.ofilter ?r' ?B \<and> ?B < ?A \<times> ?A"
   4.157      using 4 wo_rel_def[of ?r'] wo_rel.ofilter_def[of ?r' ?B] by blast
   4.158 -    have "\<not> (\<exists>a. Field r = rel.under r a)"
   4.159 +    have "\<not> (\<exists>a. Field r = under r a)"
   4.160      using 1 unfolding phi_def using Card_order_infinite_not_under[of r] by auto
   4.161      then obtain A1 where temp3: "wo_rel.ofilter r A1 \<and> A1 < ?A" and 9: "?B \<le> A1 \<times> A1"
   4.162      using temp2 3 bsqr_ofilter[of r ?B] by blast
   4.163 @@ -1332,8 +1332,8 @@
   4.164  unfolding Field_def by auto
   4.165  
   4.166  
   4.167 -lemma natLeq_underS_less: "rel.underS natLeq n = {x. x < n}"
   4.168 -unfolding rel.underS_def by auto
   4.169 +lemma natLeq_underS_less: "underS natLeq n = {x. x < n}"
   4.170 +unfolding underS_def by auto
   4.171  
   4.172  
   4.173  lemma Restr_natLeq: "Restr natLeq {x. x < n} = natLeq_on n"
   4.174 @@ -1341,7 +1341,7 @@
   4.175  
   4.176  
   4.177  lemma Restr_natLeq2:
   4.178 -"Restr natLeq (rel.underS natLeq n) = natLeq_on n"
   4.179 +"Restr natLeq (underS natLeq n) = natLeq_on n"
   4.180  by (auto simp add: Restr_natLeq natLeq_underS_less)
   4.181  
   4.182  
   4.183 @@ -1728,7 +1728,7 @@
   4.184      using r' by (simp add: card_of_Field_ordIso[of ?r'])
   4.185      finally have "|K| \<le>o ?r'" .
   4.186      moreover
   4.187 -    {let ?L = "UN j : K. rel.underS ?r' j"
   4.188 +    {let ?L = "UN j : K. underS ?r' j"
   4.189       let ?J = "Field r"
   4.190       have rJ: "r =o |?J|"
   4.191       using r_card card_of_Field_ordIso ordIso_symmetric by blast
   4.192 @@ -1736,11 +1736,11 @@
   4.193       hence "|K| <=o r" using r' card_of_Card_order[of K] by blast
   4.194       hence "|K| \<le>o |?J|" using rJ ordLeq_ordIso_trans by blast
   4.195       moreover
   4.196 -     {have "ALL j : K. |rel.underS ?r' j| <o ?r'"
   4.197 +     {have "ALL j : K. |underS ?r' j| <o ?r'"
   4.198        using r' 1 by (auto simp: card_of_underS)
   4.199 -      hence "ALL j : K. |rel.underS ?r' j| \<le>o r"
   4.200 +      hence "ALL j : K. |underS ?r' j| \<le>o r"
   4.201        using r' card_of_Card_order by blast
   4.202 -      hence "ALL j : K. |rel.underS ?r' j| \<le>o |?J|"
   4.203 +      hence "ALL j : K. |underS ?r' j| \<le>o |?J|"
   4.204        using rJ ordLeq_ordIso_trans by blast
   4.205       }
   4.206       ultimately have "|?L| \<le>o |?J|"
   4.207 @@ -1750,7 +1750,7 @@
   4.208       moreover
   4.209       {
   4.210        have "Field ?r' \<le> ?L"
   4.211 -      using 2 unfolding rel.underS_def cofinal_def by auto
   4.212 +      using 2 unfolding underS_def cofinal_def by auto
   4.213        hence "|Field ?r'| \<le>o |?L|" by (simp add: card_of_mono1)
   4.214        hence "?r' \<le>o |?L|"
   4.215        using 22 ordIso_ordLeq_trans ordIso_symmetric by blast
     5.1 --- a/src/HOL/Cardinals/Constructions_on_Wellorders.thy	Thu Jan 16 18:52:50 2014 +0100
     5.2 +++ b/src/HOL/Cardinals/Constructions_on_Wellorders.thy	Thu Jan 16 20:52:54 2014 +0100
     5.3 @@ -216,7 +216,7 @@
     5.4    moreover
     5.5    have "ofilter (r Osum r') (Field r)"
     5.6    using 1 proof(auto simp add: wo_rel_def wo_rel.ofilter_def
     5.7 -                               Field_Osum rel.under_def)
     5.8 +                               Field_Osum under_def)
     5.9      fix a b assume 2: "a \<in> Field r" and 3: "(b,a) \<in> r Osum r'"
    5.10      moreover
    5.11      {assume "(b,a) \<in> r'"
    5.12 @@ -251,13 +251,13 @@
    5.13    then obtain r'' where "well_order_on (f ` A) r''" and 1: "r =o r''"
    5.14    using WELL  Well_order_iso_copy by blast
    5.15    hence 2: "Well_order r'' \<and> Field r'' = (f ` A)"
    5.16 -  using rel.well_order_on_Well_order by blast
    5.17 +  using well_order_on_Well_order by blast
    5.18    (*  *)
    5.19    let ?C = "B - (f ` A)"
    5.20    obtain r''' where "well_order_on ?C r'''"
    5.21    using well_order_on by blast
    5.22    hence 3: "Well_order r''' \<and> Field r''' = ?C"
    5.23 -  using rel.well_order_on_Well_order by blast
    5.24 +  using well_order_on_Well_order by blast
    5.25    (*  *)
    5.26    let ?r' = "r'' Osum r'''"
    5.27    have "Field r'' Int Field r''' = {}"
    5.28 @@ -479,23 +479,18 @@
    5.29    have bb: "b \<in> Field r" using bA unfolding underS_def Field_def by auto
    5.30    assume "\<forall>a\<in>A.  b \<notin> under a"
    5.31    hence 0: "\<forall>a \<in> A. a \<in> underS b" using A bA unfolding underS_def
    5.32 -  by simp (metis (lifting) bb max2_def max2_greater mem_Collect_eq rel.under_def set_rev_mp)
    5.33 -  have "(suc A, b) \<in> r" apply(rule suc_least[OF A bb]) using 0 unfolding rel.underS_def by auto
    5.34 +  by simp (metis (lifting) bb max2_def max2_greater mem_Collect_eq under_def set_rev_mp)
    5.35 +  have "(suc A, b) \<in> r" apply(rule suc_least[OF A bb]) using 0 unfolding underS_def by auto
    5.36    thus False using bA unfolding underS_def by simp (metis ANTISYM antisymD)
    5.37  qed
    5.38  
    5.39 -lemma (in rel) AboveS_underS:
    5.40 -assumes "i \<in> Field r"
    5.41 -shows "i \<in> AboveS (underS i)"
    5.42 -using assms unfolding AboveS_def underS_def by auto
    5.43 -
    5.44  lemma (in wo_rel) in_underS_supr:
    5.45  assumes j: "j \<in> underS i" and i: "i \<in> A" and A: "A \<subseteq> Field r" and AA: "Above A \<noteq> {}"
    5.46  shows "j \<in> underS (supr A)"
    5.47  proof-
    5.48    have "(i,supr A) \<in> r" using supr_greater[OF A AA i] .
    5.49    thus ?thesis using j unfolding underS_def
    5.50 -  by simp (metis REFL TRANS max2_def max2_equals1 rel.refl_on_domain transD)
    5.51 +  by simp (metis REFL TRANS max2_def max2_equals1 refl_on_domain transD)
    5.52  qed
    5.53  
    5.54  lemma inj_on_Field:
    5.55 @@ -530,7 +525,7 @@
    5.56    and init: "(R ja, R j) \<notin> init_seg_of"
    5.57    hence jja: "{j,ja} \<subseteq> Field r" and j: "j \<in> Field r" and ja: "ja \<in> Field r"
    5.58    and jjai: "(j,i) \<in> r" "(ja,i) \<in> r"
    5.59 -  and i: "i \<notin> {j,ja}" unfolding Field_def rel.underS_def by auto
    5.60 +  and i: "i \<notin> {j,ja}" unfolding Field_def underS_def by auto
    5.61    have jj: "(j,j) \<in> r" and jaja: "(ja,ja) \<in> r" using j ja by (metis in_notinI)+
    5.62    show "R j initial_segment_of R ja"
    5.63    using jja init jjai i
    5.64 @@ -544,7 +539,7 @@
    5.65    fix j ja assume jS: "j \<in> Field r" and jaS: "ja \<in> Field r"
    5.66    and init: "(R ja, R j) \<notin> init_seg_of"
    5.67    hence jja: "{j,ja} \<subseteq> Field r" and j: "j \<in> Field r" and ja: "ja \<in> Field r"
    5.68 -  unfolding Field_def rel.underS_def by auto
    5.69 +  unfolding Field_def underS_def by auto
    5.70    have jj: "(j,j) \<in> r" and jaja: "(ja,ja) \<in> r" using j ja by (metis in_notinI)+
    5.71    show "R j initial_segment_of R ja"
    5.72    using jja init
    5.73 @@ -700,8 +695,8 @@
    5.74  assumes "aboveS i \<noteq> {}"
    5.75  shows "(j, succ i) \<in> r \<longleftrightarrow> (j,i) \<in> r \<or> j = succ i"
    5.76  apply safe
    5.77 -  apply (metis WELL assms in_notinI rel.well_order_on_domain suc_singl_pred succ_def succ_in_diff)
    5.78 -  apply (metis (hide_lams, full_types) REFL TRANS assms max2_def max2_equals1 rel.refl_on_domain succ_in_Field succ_not_in transD)
    5.79 +  apply (metis WELL assms in_notinI well_order_on_domain suc_singl_pred succ_def succ_in_diff)
    5.80 +  apply (metis (hide_lams, full_types) REFL TRANS assms max2_def max2_equals1 refl_on_domain succ_in_Field succ_not_in transD)
    5.81    apply (metis assms in_notinI succ_in_Field)
    5.82  done
    5.83  
    5.84 @@ -926,7 +921,7 @@
    5.85  lemma oproj_under: 
    5.86  assumes f:  "oproj r s f" and a: "a \<in> under r a'"
    5.87  shows "f a \<in> under s (f a')"
    5.88 -using oproj_in[OF f] a unfolding rel.under_def by auto
    5.89 +using oproj_in[OF f] a unfolding under_def by auto
    5.90  
    5.91  (* An ordinal is embedded in another whenever it is embedded as an order 
    5.92  (not necessarily as initial segment):*)
    5.93 @@ -950,55 +945,55 @@
    5.94       and IH1a: "\<And> a1. a1 \<in> underS r a \<Longrightarrow> inj_on g (under r a1)"
    5.95       and IH1b: "\<And> a1. a1 \<in> underS r a \<Longrightarrow> g ` under r a1 = under s (g a1)"
    5.96       and IH2: "\<And> a1. a1 \<in> underS r a \<Longrightarrow> g a1 \<in> under s (f a1)"
    5.97 -     unfolding rel.underS_def Field_def bij_betw_def by auto
    5.98 +     unfolding underS_def Field_def bij_betw_def by auto
    5.99       have fa: "f a \<in> Field s" using f[OF a] by auto
   5.100       have g: "g a = suc s (g ` underS r a)" 
   5.101       using r.worec_fixpoint[OF adm] unfolding g_def fun_eq_iff by simp
   5.102       have A0: "g ` underS r a \<subseteq> Field s" 
   5.103 -     using IH1b by (metis IH2 image_subsetI in_mono rel.under_Field)
   5.104 +     using IH1b by (metis IH2 image_subsetI in_mono under_Field)
   5.105       {fix a1 assume a1: "a1 \<in> underS r a"
   5.106        from IH2[OF this] have "g a1 \<in> under s (f a1)" .
   5.107        moreover have "f a1 \<in> underS s (f a)" using f[OF a] a1 by auto
   5.108 -      ultimately have "g a1 \<in> underS s (f a)" by (metis s.ANTISYM s.TRANS rel.under_underS_trans)
   5.109 +      ultimately have "g a1 \<in> underS s (f a)" by (metis s.ANTISYM s.TRANS under_underS_trans)
   5.110       }
   5.111 -     hence "f a \<in> AboveS s (g ` underS r a)" unfolding rel.AboveS_def 
   5.112 -     using fa by simp (metis (lifting, full_types) mem_Collect_eq rel.underS_def)
   5.113 +     hence "f a \<in> AboveS s (g ` underS r a)" unfolding AboveS_def 
   5.114 +     using fa by simp (metis (lifting, full_types) mem_Collect_eq underS_def)
   5.115       hence A: "AboveS s (g ` underS r a) \<noteq> {}" by auto
   5.116       have B: "\<And> a1. a1 \<in> underS r a \<Longrightarrow> g a1 \<in> underS s (g a)"
   5.117       unfolding g apply(rule s.suc_underS[OF A0 A]) by auto
   5.118       {fix a1 a2 assume a2: "a2 \<in> underS r a" and 1: "a1 \<in> underS r a2"
   5.119        hence a12: "{a1,a2} \<subseteq> under r a2" and "a1 \<noteq> a2" using r.REFL a
   5.120 -      unfolding rel.underS_def rel.under_def refl_on_def Field_def by auto 
   5.121 +      unfolding underS_def under_def refl_on_def Field_def by auto 
   5.122        hence "g a1 \<noteq> g a2" using IH1a[OF a2] unfolding inj_on_def by auto
   5.123        hence "g a1 \<in> underS s (g a2)" using IH1b[OF a2] a12 
   5.124 -      unfolding rel.underS_def rel.under_def by auto
   5.125 +      unfolding underS_def under_def by auto
   5.126       } note C = this
   5.127       have ga: "g a \<in> Field s" unfolding g using s.suc_inField[OF A0 A] .
   5.128       have aa: "a \<in> under r a" 
   5.129 -     using a r.REFL unfolding rel.under_def rel.underS_def refl_on_def by auto
   5.130 +     using a r.REFL unfolding under_def underS_def refl_on_def by auto
   5.131       show ?case proof safe
   5.132         show "bij_betw g (under r a) (under s (g a))" unfolding bij_betw_def proof safe
   5.133           show "inj_on g (under r a)" proof(rule r.inj_on_Field)
   5.134             fix a1 a2 assume "a1 \<in> under r a" and a2: "a2 \<in> under r a" and a1: "a1 \<in> underS r a2"
   5.135             hence a22: "a2 \<in> under r a2" and a12: "a1 \<in> under r a2" "a1 \<noteq> a2"
   5.136 -           using a r.REFL unfolding rel.under_def rel.underS_def refl_on_def by auto
   5.137 +           using a r.REFL unfolding under_def underS_def refl_on_def by auto
   5.138             show "g a1 \<noteq> g a2"
   5.139             proof(cases "a2 = a")
   5.140               case False hence "a2 \<in> underS r a" 
   5.141 -             using a2 unfolding rel.underS_def rel.under_def by auto 
   5.142 +             using a2 unfolding underS_def under_def by auto 
   5.143               from IH1a[OF this] show ?thesis using a12 a22 unfolding inj_on_def by auto
   5.144 -           qed(insert B a1, unfold rel.underS_def, auto)
   5.145 -         qed(unfold rel.under_def Field_def, auto)
   5.146 +           qed(insert B a1, unfold underS_def, auto)
   5.147 +         qed(unfold under_def Field_def, auto)
   5.148         next
   5.149           fix a1 assume a1: "a1 \<in> under r a" 
   5.150           show "g a1 \<in> under s (g a)"
   5.151           proof(cases "a1 = a")
   5.152             case True thus ?thesis 
   5.153 -           using ga s.REFL unfolding refl_on_def rel.under_def by auto
   5.154 +           using ga s.REFL unfolding refl_on_def under_def by auto
   5.155           next
   5.156             case False
   5.157 -           hence a1: "a1 \<in> underS r a" using a1 unfolding rel.underS_def rel.under_def by auto 
   5.158 -           thus ?thesis using B unfolding rel.underS_def rel.under_def by auto
   5.159 +           hence a1: "a1 \<in> underS r a" using a1 unfolding underS_def under_def by auto 
   5.160 +           thus ?thesis using B unfolding underS_def under_def by auto
   5.161           qed
   5.162         next
   5.163           fix b1 assume b1: "b1 \<in> under s (g a)"
   5.164 @@ -1007,12 +1002,12 @@
   5.165             case True thus ?thesis using aa by auto
   5.166           next
   5.167             case False 
   5.168 -           hence "b1 \<in> underS s (g a)" using b1 unfolding rel.underS_def rel.under_def by auto
   5.169 +           hence "b1 \<in> underS s (g a)" using b1 unfolding underS_def under_def by auto
   5.170             from s.underS_suc[OF this[unfolded g] A0]
   5.171             obtain a1 where a1: "a1 \<in> underS r a" and b1: "b1 \<in> under s (g a1)" by auto
   5.172             obtain a2 where "a2 \<in> under r a1" and b1: "b1 = g a2" using IH1b[OF a1] b1 by auto
   5.173             hence "a2 \<in> under r a" using a1 
   5.174 -           by (metis r.ANTISYM r.TRANS in_mono rel.underS_subset_under rel.under_underS_trans)
   5.175 +           by (metis r.ANTISYM r.TRANS in_mono underS_subset_under under_underS_trans)
   5.176             thus ?thesis using b1 by auto
   5.177           qed
   5.178         qed
   5.179 @@ -1022,9 +1017,9 @@
   5.180           then obtain a1 where a1: "b1 = g a1" and a1: "a1 \<in> underS r a" by auto
   5.181           hence "b1 \<in> underS s (f a)" 
   5.182           using a by (metis `\<And>a1. a1 \<in> underS r a \<Longrightarrow> g a1 \<in> underS s (f a)`)
   5.183 -         thus "f a \<noteq> b1 \<and> (b1, f a) \<in> s" unfolding rel.underS_def by auto
   5.184 +         thus "f a \<noteq> b1 \<and> (b1, f a) \<in> s" unfolding underS_def by auto
   5.185         qed(insert fa, auto)
   5.186 -       thus "g a \<in> under s (f a)" unfolding rel.under_def by auto
   5.187 +       thus "g a \<in> under s (f a)" unfolding under_def by auto
   5.188       qed
   5.189     qed
   5.190    }
   5.191 @@ -1046,7 +1041,7 @@
   5.192  theorem oproj_embed:
   5.193  assumes r: "Well_order r" and s: "Well_order s" and f: "oproj r s f"
   5.194  shows "\<exists> g. embed s r g"
   5.195 -proof (rule embedI[OF s r, of "inv_into (Field r) f"], unfold rel.underS_def, safe)
   5.196 +proof (rule embedI[OF s r, of "inv_into (Field r) f"], unfold underS_def, safe)
   5.197    fix b assume "b \<in> Field s"
   5.198    thus "inv_into (Field r) f b \<in> Field r" using oproj_Field2[OF f] by (metis imageI inv_into_into)
   5.199  next
     6.1 --- a/src/HOL/Cardinals/Constructions_on_Wellorders_FP.thy	Thu Jan 16 18:52:50 2014 +0100
     6.2 +++ b/src/HOL/Cardinals/Constructions_on_Wellorders_FP.thy	Thu Jan 16 20:52:54 2014 +0100
     6.3 @@ -116,12 +116,12 @@
     6.4  
     6.5  lemma ofilter_Restr_under:
     6.6  assumes WELL: "Well_order r" and OF: "wo_rel.ofilter r A" and IN: "a \<in> A"
     6.7 -shows "rel.under (Restr r A) a = rel.under r a"
     6.8 +shows "under (Restr r A) a = under r a"
     6.9  using assms wo_rel_def
    6.10 -proof(auto simp add: wo_rel.ofilter_def rel.under_def)
    6.11 +proof(auto simp add: wo_rel.ofilter_def under_def)
    6.12    fix b assume *: "a \<in> A" and "(b,a) \<in> r"
    6.13 -  hence "b \<in> rel.under r a \<and> a \<in> Field r"
    6.14 -  unfolding rel.under_def using Field_def by fastforce
    6.15 +  hence "b \<in> under r a \<and> a \<in> Field r"
    6.16 +  unfolding under_def using Field_def by fastforce
    6.17    thus "b \<in> A" using * assms by (auto simp add: wo_rel_def wo_rel.ofilter_def)
    6.18  qed
    6.19  
    6.20 @@ -137,7 +137,7 @@
    6.21      by (auto simp add: wo_rel_def wo_rel.ofilter_def)
    6.22    next
    6.23      fix a assume "a \<in> Field (Restr r A)"
    6.24 -    thus "bij_betw id (rel.under (Restr r A) a) (rel.under r a)" using assms *
    6.25 +    thus "bij_betw id (under (Restr r A) a) (under r a)" using assms *
    6.26      by (simp add: ofilter_Restr_under Field_Restr_ofilter)
    6.27    qed
    6.28  next
    6.29 @@ -148,13 +148,13 @@
    6.30    {fix a assume "a \<in> A"
    6.31     hence "a \<in> Field(Restr r A)" using * assms
    6.32     by (simp add: order_on_defs Refl_Field_Restr2)
    6.33 -   hence "bij_betw id (rel.under (Restr r A) a) (rel.under r a)"
    6.34 +   hence "bij_betw id (under (Restr r A) a) (under r a)"
    6.35     using * unfolding embed_def by auto
    6.36 -   hence "rel.under r a \<le> rel.under (Restr r A) a"
    6.37 +   hence "under r a \<le> under (Restr r A) a"
    6.38     unfolding bij_betw_def by auto
    6.39 -   also have "\<dots> \<le> Field(Restr r A)" by (simp add: rel.under_Field)
    6.40 +   also have "\<dots> \<le> Field(Restr r A)" by (simp add: under_Field)
    6.41     also have "\<dots> \<le> A" by (simp add: Field_Restr_subset)
    6.42 -   finally have "rel.under r a \<le> A" .
    6.43 +   finally have "under r a \<le> A" .
    6.44    }
    6.45    thus "wo_rel.ofilter r A" using assms * by (simp add: wo_rel_def wo_rel.ofilter_def)
    6.46  qed
    6.47 @@ -173,13 +173,13 @@
    6.48    by (simp add: Well_order_Restr wo_rel_def)
    6.49    (* Main proof *)
    6.50    show ?thesis using WellB assms
    6.51 -  proof(auto simp add: wo_rel.ofilter_def rel.under_def)
    6.52 +  proof(auto simp add: wo_rel.ofilter_def under_def)
    6.53      fix a assume "a \<in> A" and *: "a \<in> B"
    6.54      hence "a \<in> Field r" using OFA Well by (auto simp add: wo_rel.ofilter_def)
    6.55      with * show "a \<in> Field ?rB" using Field by auto
    6.56    next
    6.57      fix a b assume "a \<in> A" and "(b,a) \<in> r"
    6.58 -    thus "b \<in> A" using Well OFA by (auto simp add: wo_rel.ofilter_def rel.under_def)
    6.59 +    thus "b \<in> A" using Well OFA by (auto simp add: wo_rel.ofilter_def under_def)
    6.60    qed
    6.61  qed
    6.62  
    6.63 @@ -312,12 +312,12 @@
    6.64      assume *: "wo_rel.ofilter r A" "A \<noteq> Field r" and
    6.65             **: "wo_rel.ofilter r B" "B \<noteq> Field r" and ***: "A < B"
    6.66      then obtain a and b where 0: "a \<in> Field r \<and> b \<in> Field r" and
    6.67 -                         1: "A = rel.underS r a \<and> B = rel.underS r b"
    6.68 +                         1: "A = underS r a \<and> B = underS r b"
    6.69      using Well by (auto simp add: wo_rel.ofilter_underS_Field)
    6.70      hence "a \<noteq> b" using *** by auto
    6.71      moreover
    6.72      have "(a,b) \<in> r" using 0 1 Lo ***
    6.73 -    by (auto simp add: rel.underS_incl_iff)
    6.74 +    by (auto simp add: underS_incl_iff)
    6.75      moreover
    6.76      have "a = wo_rel.suc r A \<and> b = wo_rel.suc r B"
    6.77      using Well 0 1 by (simp add: wo_rel.suc_underS)
    6.78 @@ -714,10 +714,10 @@
    6.79  
    6.80  corollary underS_Restr_ordLess:
    6.81  assumes "Well_order r" and "Field r \<noteq> {}"
    6.82 -shows "Restr r (rel.underS r a) <o r"
    6.83 +shows "Restr r (underS r a) <o r"
    6.84  proof-
    6.85 -  have "rel.underS r a < Field r" using assms
    6.86 -  by (simp add: rel.underS_Field3)
    6.87 +  have "underS r a < Field r" using assms
    6.88 +  by (simp add: underS_Field3)
    6.89    thus ?thesis using assms
    6.90    by (simp add: ofilter_ordLess wo_rel.underS_ofilter wo_rel_def)
    6.91  qed
    6.92 @@ -772,10 +772,10 @@
    6.93  
    6.94  lemma ordLess_iff_ordIso_Restr:
    6.95  assumes WELL: "Well_order r" and WELL': "Well_order r'"
    6.96 -shows "(r' <o r) = (\<exists>a \<in> Field r. r' =o Restr r (rel.underS r a))"
    6.97 +shows "(r' <o r) = (\<exists>a \<in> Field r. r' =o Restr r (underS r a))"
    6.98  proof(auto)
    6.99 -  fix a assume *: "a \<in> Field r" and **: "r' =o Restr r (rel.underS r a)"
   6.100 -  hence "Restr r (rel.underS r a) <o r" using WELL underS_Restr_ordLess[of r] by blast
   6.101 +  fix a assume *: "a \<in> Field r" and **: "r' =o Restr r (underS r a)"
   6.102 +  hence "Restr r (underS r a) <o r" using WELL underS_Restr_ordLess[of r] by blast
   6.103    thus "r' <o r" using ** ordIso_ordLess_trans by blast
   6.104  next
   6.105    assume "r' <o r"
   6.106 @@ -783,7 +783,7 @@
   6.107                        2: "embed r' r f \<and> f ` (Field r') \<noteq> Field r"
   6.108    unfolding ordLess_def embedS_def[abs_def] bij_betw_def using embed_inj_on by blast
   6.109    hence "wo_rel.ofilter r (f ` (Field r'))" using embed_Field_ofilter by blast
   6.110 -  then obtain a where 3: "a \<in> Field r" and 4: "rel.underS r a = f ` (Field r')"
   6.111 +  then obtain a where 3: "a \<in> Field r" and 4: "underS r a = f ` (Field r')"
   6.112    using 1 2 by (auto simp add: wo_rel.ofilter_underS_Field wo_rel_def)
   6.113    have "iso r' (Restr r (f ` (Field r'))) f"
   6.114    using embed_implies_iso_Restr 2 assms by blast
   6.115 @@ -791,8 +791,8 @@
   6.116    using WELL Well_order_Restr by blast
   6.117    ultimately have "r' =o Restr r (f ` (Field r'))"
   6.118    using WELL' unfolding ordIso_def by auto
   6.119 -  hence "r' =o Restr r (rel.underS r a)" using 4 by auto
   6.120 -  thus "\<exists>a \<in> Field r. r' =o Restr r (rel.underS r a)" using 3 by auto
   6.121 +  hence "r' =o Restr r (underS r a)" using 4 by auto
   6.122 +  thus "\<exists>a \<in> Field r. r' =o Restr r (underS r a)" using 3 by auto
   6.123  qed
   6.124  
   6.125  
   6.126 @@ -801,13 +801,13 @@
   6.127  proof
   6.128    assume *: "r' <o r"
   6.129    hence 0: "Well_order r \<and> Well_order r'" unfolding ordLess_def by auto
   6.130 -  with * obtain a where 1: "a \<in> Field r" and 2: "r' =o Restr r (rel.underS r a)"
   6.131 +  with * obtain a where 1: "a \<in> Field r" and 2: "r' =o Restr r (underS r a)"
   6.132    using ordLess_iff_ordIso_Restr by blast
   6.133 -  let ?p = "Restr r (rel.underS r a)"
   6.134 -  have "wo_rel.ofilter r (rel.underS r a)" using 0
   6.135 +  let ?p = "Restr r (underS r a)"
   6.136 +  have "wo_rel.ofilter r (underS r a)" using 0
   6.137    by (simp add: wo_rel_def wo_rel.underS_ofilter)
   6.138 -  hence "Field ?p = rel.underS r a" using 0 Field_Restr_ofilter by blast
   6.139 -  hence "Field ?p < Field r" using rel.underS_Field2 1 by fast
   6.140 +  hence "Field ?p = underS r a" using 0 Field_Restr_ofilter by blast
   6.141 +  hence "Field ?p < Field r" using underS_Field2 1 by fast
   6.142    moreover have "?p <o r" using underS_Restr_ordLess[of r a] 0 1 by blast
   6.143    ultimately
   6.144    show "\<exists>p. Field p < Field r \<and> r' =o p \<and> p <o r" using 2 by blast
   6.145 @@ -840,18 +840,18 @@
   6.146  
   6.147  lemma ordLeq_iff_ordLess_Restr:
   6.148  assumes WELL: "Well_order r" and WELL': "Well_order r'"
   6.149 -shows "(r \<le>o r') = (\<forall>a \<in> Field r. Restr r (rel.underS r a) <o r')"
   6.150 +shows "(r \<le>o r') = (\<forall>a \<in> Field r. Restr r (underS r a) <o r')"
   6.151  proof(auto)
   6.152    assume *: "r \<le>o r'"
   6.153    fix a assume "a \<in> Field r"
   6.154 -  hence "Restr r (rel.underS r a) <o r"
   6.155 +  hence "Restr r (underS r a) <o r"
   6.156    using WELL underS_Restr_ordLess[of r] by blast
   6.157 -  thus "Restr r (rel.underS r a) <o r'"
   6.158 +  thus "Restr r (underS r a) <o r'"
   6.159    using * ordLess_ordLeq_trans by blast
   6.160  next
   6.161 -  assume *: "\<forall>a \<in> Field r. Restr r (rel.underS r a) <o r'"
   6.162 +  assume *: "\<forall>a \<in> Field r. Restr r (underS r a) <o r'"
   6.163    {assume "r' <o r"
   6.164 -   then obtain a where "a \<in> Field r \<and> r' =o Restr r (rel.underS r a)"
   6.165 +   then obtain a where "a \<in> Field r \<and> r' =o Restr r (underS r a)"
   6.166     using assms ordLess_iff_ordIso_Restr by blast
   6.167     hence False using * not_ordLess_ordIso ordIso_symmetric by blast
   6.168    }
   6.169 @@ -879,14 +879,14 @@
   6.170  shows "r =o r'"
   6.171  proof-
   6.172    have 0: "Well_order r \<and> Well_order r' \<and> Field r = A \<and> Field r' = A"
   6.173 -  using assms rel.well_order_on_Well_order by blast
   6.174 +  using assms well_order_on_Well_order by blast
   6.175    moreover
   6.176    have "\<forall>r r'. well_order_on A r \<and> well_order_on A r' \<and> r \<le>o r'
   6.177                    \<longrightarrow> r =o r'"
   6.178    proof(clarify)
   6.179      fix r r' assume *: "well_order_on A r" and **: "well_order_on A r'"
   6.180      have 2: "Well_order r \<and> Well_order r' \<and> Field r = A \<and> Field r' = A"
   6.181 -    using * ** rel.well_order_on_Well_order by blast
   6.182 +    using * ** well_order_on_Well_order by blast
   6.183      assume "r \<le>o r'"
   6.184      then obtain f where 1: "embed r r' f" and
   6.185                          "inj_on f A \<and> f ` A \<le> A"
   6.186 @@ -1137,7 +1137,7 @@
   6.187  proof-
   6.188     let ?r' = "dir_image r f"
   6.189     have 1: "A = Field r \<and> Well_order r"
   6.190 -   using WELL rel.well_order_on_Well_order by blast
   6.191 +   using WELL well_order_on_Well_order by blast
   6.192     hence 2: "iso r ?r' f"
   6.193     using dir_image_iso using BIJ unfolding bij_betw_def by auto
   6.194     hence "f ` (Field r) = Field ?r'" using 1 iso_iff[of r ?r'] by blast
   6.195 @@ -1576,7 +1576,7 @@
   6.196  lemma bsqr_ofilter:
   6.197  assumes WELL: "Well_order r" and
   6.198          OF: "wo_rel.ofilter (bsqr r) D" and SUB: "D < Field r \<times> Field r" and
   6.199 -        NE: "\<not> (\<exists>a. Field r = rel.under r a)"
   6.200 +        NE: "\<not> (\<exists>a. Field r = under r a)"
   6.201  shows "\<exists>A. wo_rel.ofilter r A \<and> A < Field r \<and> D \<le> A \<times> A"
   6.202  proof-
   6.203    let ?r' = "bsqr r"
   6.204 @@ -1587,17 +1587,17 @@
   6.205    (*  *)
   6.206    have "D < Field ?r'" unfolding Field_bsqr using SUB .
   6.207    with OF obtain a1 and a2 where
   6.208 -  "(a1,a2) \<in> Field ?r'" and 1: "D = rel.underS ?r' (a1,a2)"
   6.209 +  "(a1,a2) \<in> Field ?r'" and 1: "D = underS ?r' (a1,a2)"
   6.210    using Well' wo_rel.ofilter_underS_Field[of ?r' D] by auto
   6.211    hence 2: "{a1,a2} \<le> Field r" unfolding Field_bsqr by auto
   6.212    let ?m = "wo_rel.max2 r a1 a2"
   6.213 -  have "D \<le> (rel.under r ?m) \<times> (rel.under r ?m)"
   6.214 +  have "D \<le> (under r ?m) \<times> (under r ?m)"
   6.215    proof(unfold 1)
   6.216      {fix b1 b2
   6.217       let ?n = "wo_rel.max2 r b1 b2"
   6.218 -     assume "(b1,b2) \<in> rel.underS ?r' (a1,a2)"
   6.219 +     assume "(b1,b2) \<in> underS ?r' (a1,a2)"
   6.220       hence 3: "((b1,b2),(a1,a2)) \<in> ?r'"
   6.221 -     unfolding rel.underS_def by blast
   6.222 +     unfolding underS_def by blast
   6.223       hence "(?n,?m) \<in> r" using WELL by (simp add: bsqr_max2)
   6.224       moreover
   6.225       {have "(b1,b2) \<in> Field ?r'" using 3 unfolding Field_def by auto
   6.226 @@ -1607,13 +1607,13 @@
   6.227       }
   6.228       ultimately have "(b1,?m) \<in> r \<and> (b2,?m) \<in> r"
   6.229       using Trans trans_def[of r] by blast
   6.230 -     hence "(b1,b2) \<in> (rel.under r ?m) \<times> (rel.under r ?m)" unfolding rel.under_def by simp}
   6.231 -     thus "rel.underS ?r' (a1,a2) \<le> (rel.under r ?m) \<times> (rel.under r ?m)" by auto
   6.232 +     hence "(b1,b2) \<in> (under r ?m) \<times> (under r ?m)" unfolding under_def by simp}
   6.233 +     thus "underS ?r' (a1,a2) \<le> (under r ?m) \<times> (under r ?m)" by auto
   6.234    qed
   6.235 -  moreover have "wo_rel.ofilter r (rel.under r ?m)"
   6.236 +  moreover have "wo_rel.ofilter r (under r ?m)"
   6.237    using Well by (simp add: wo_rel.under_ofilter)
   6.238 -  moreover have "rel.under r ?m < Field r"
   6.239 -  using NE rel.under_Field[of r ?m] by blast
   6.240 +  moreover have "under r ?m < Field r"
   6.241 +  using NE under_Field[of r ?m] by blast
   6.242    ultimately show ?thesis by blast
   6.243  qed
   6.244  
     7.1 --- a/src/HOL/Cardinals/Order_Relation_More.thy	Thu Jan 16 18:52:50 2014 +0100
     7.2 +++ b/src/HOL/Cardinals/Order_Relation_More.thy	Thu Jan 16 20:52:54 2014 +0100
     7.3 @@ -14,66 +14,63 @@
     7.4  
     7.5  subsection {* The upper and lower bounds operators  *}
     7.6  
     7.7 -context rel
     7.8 -begin
     7.9 -
    7.10 -lemma aboveS_subset_above: "aboveS a \<le> above a"
    7.11 +lemma aboveS_subset_above: "aboveS r a \<le> above r a"
    7.12  by(auto simp add: aboveS_def above_def)
    7.13  
    7.14 -lemma AboveS_subset_Above: "AboveS A \<le> Above A"
    7.15 +lemma AboveS_subset_Above: "AboveS r A \<le> Above r A"
    7.16  by(auto simp add: AboveS_def Above_def)
    7.17  
    7.18 -lemma UnderS_disjoint: "A Int (UnderS A) = {}"
    7.19 +lemma UnderS_disjoint: "A Int (UnderS r A) = {}"
    7.20  by(auto simp add: UnderS_def)
    7.21  
    7.22 -lemma aboveS_notIn: "a \<notin> aboveS a"
    7.23 +lemma aboveS_notIn: "a \<notin> aboveS r a"
    7.24  by(auto simp add: aboveS_def)
    7.25  
    7.26 -lemma Refl_above_in: "\<lbrakk>Refl r; a \<in> Field r\<rbrakk> \<Longrightarrow> a \<in> above a"
    7.27 +lemma Refl_above_in: "\<lbrakk>Refl r; a \<in> Field r\<rbrakk> \<Longrightarrow> a \<in> above r a"
    7.28  by(auto simp add: refl_on_def above_def)
    7.29  
    7.30 -lemma in_Above_under: "a \<in> Field r \<Longrightarrow> a \<in> Above (under a)"
    7.31 +lemma in_Above_under: "a \<in> Field r \<Longrightarrow> a \<in> Above r (under r a)"
    7.32  by(auto simp add: Above_def under_def)
    7.33  
    7.34 -lemma in_Under_above: "a \<in> Field r \<Longrightarrow> a \<in> Under (above a)"
    7.35 +lemma in_Under_above: "a \<in> Field r \<Longrightarrow> a \<in> Under r (above r a)"
    7.36  by(auto simp add: Under_def above_def)
    7.37  
    7.38 -lemma in_UnderS_aboveS: "a \<in> Field r \<Longrightarrow> a \<in> UnderS (aboveS a)"
    7.39 +lemma in_UnderS_aboveS: "a \<in> Field r \<Longrightarrow> a \<in> UnderS r (aboveS r a)"
    7.40  by(auto simp add: UnderS_def aboveS_def)
    7.41  
    7.42 -lemma UnderS_subset_Under: "UnderS A \<le> Under A"
    7.43 +lemma UnderS_subset_Under: "UnderS r A \<le> Under r A"
    7.44  by(auto simp add: UnderS_def Under_def)
    7.45  
    7.46 -lemma subset_Above_Under: "B \<le> Field r \<Longrightarrow> B \<le> Above (Under B)"
    7.47 +lemma subset_Above_Under: "B \<le> Field r \<Longrightarrow> B \<le> Above r (Under r B)"
    7.48  by(auto simp add: Above_def Under_def)
    7.49  
    7.50 -lemma subset_Under_Above: "B \<le> Field r \<Longrightarrow> B \<le> Under (Above B)"
    7.51 +lemma subset_Under_Above: "B \<le> Field r \<Longrightarrow> B \<le> Under r (Above r B)"
    7.52  by(auto simp add: Under_def Above_def)
    7.53  
    7.54 -lemma subset_AboveS_UnderS: "B \<le> Field r \<Longrightarrow> B \<le> AboveS (UnderS B)"
    7.55 +lemma subset_AboveS_UnderS: "B \<le> Field r \<Longrightarrow> B \<le> AboveS r (UnderS r B)"
    7.56  by(auto simp add: AboveS_def UnderS_def)
    7.57  
    7.58 -lemma subset_UnderS_AboveS: "B \<le> Field r \<Longrightarrow> B \<le> UnderS (AboveS B)"
    7.59 +lemma subset_UnderS_AboveS: "B \<le> Field r \<Longrightarrow> B \<le> UnderS r (AboveS r B)"
    7.60  by(auto simp add: UnderS_def AboveS_def)
    7.61  
    7.62  lemma Under_Above_Galois:
    7.63 -"\<lbrakk>B \<le> Field r; C \<le> Field r\<rbrakk> \<Longrightarrow> (B \<le> Above C) = (C \<le> Under B)"
    7.64 +"\<lbrakk>B \<le> Field r; C \<le> Field r\<rbrakk> \<Longrightarrow> (B \<le> Above r C) = (C \<le> Under r B)"
    7.65  by(unfold Above_def Under_def, blast)
    7.66  
    7.67  lemma UnderS_AboveS_Galois:
    7.68 -"\<lbrakk>B \<le> Field r; C \<le> Field r\<rbrakk> \<Longrightarrow> (B \<le> AboveS C) = (C \<le> UnderS B)"
    7.69 +"\<lbrakk>B \<le> Field r; C \<le> Field r\<rbrakk> \<Longrightarrow> (B \<le> AboveS r C) = (C \<le> UnderS r B)"
    7.70  by(unfold AboveS_def UnderS_def, blast)
    7.71  
    7.72  lemma Refl_above_aboveS:
    7.73 -assumes REFL: "Refl r" and IN: "a \<in> Field r"
    7.74 -shows "above a = aboveS a \<union> {a}"
    7.75 +  assumes REFL: "Refl r" and IN: "a \<in> Field r"
    7.76 +  shows "above r a = aboveS r a \<union> {a}"
    7.77  proof(unfold above_def aboveS_def, auto)
    7.78    show "(a,a) \<in> r" using REFL IN refl_on_def[of _ r] by blast
    7.79  qed
    7.80  
    7.81  lemma Linear_order_under_aboveS_Field:
    7.82 -assumes LIN: "Linear_order r" and IN: "a \<in> Field r"
    7.83 -shows "Field r = under a \<union> aboveS a"
    7.84 +  assumes LIN: "Linear_order r" and IN: "a \<in> Field r"
    7.85 +  shows "Field r = under r a \<union> aboveS r a"
    7.86  proof(unfold under_def aboveS_def, auto)
    7.87    assume "a \<in> Field r" "(a, a) \<notin> r"
    7.88    with LIN IN order_on_defs[of _ r] refl_on_def[of _ r]
    7.89 @@ -96,7 +93,7 @@
    7.90  
    7.91  lemma Linear_order_underS_above_Field:
    7.92  assumes LIN: "Linear_order r" and IN: "a \<in> Field r"
    7.93 -shows "Field r = underS a \<union> above a"
    7.94 +shows "Field r = underS r a \<union> above r a"
    7.95  proof(unfold underS_def above_def, auto)
    7.96    assume "a \<in> Field r" "(a, a) \<notin> r"
    7.97    with LIN IN order_on_defs[of _ r] refl_on_def[of _ r]
    7.98 @@ -117,155 +114,155 @@
    7.99    using LIN order_on_defs[of "Field r" r] refl_on_def[of "Field r" r] by blast
   7.100  qed
   7.101  
   7.102 -lemma under_empty: "a \<notin> Field r \<Longrightarrow> under a = {}"
   7.103 +lemma under_empty: "a \<notin> Field r \<Longrightarrow> under r a = {}"
   7.104  unfolding Field_def under_def by auto
   7.105  
   7.106 -lemma Under_Field: "Under A \<le> Field r"
   7.107 +lemma Under_Field: "Under r A \<le> Field r"
   7.108  by(unfold Under_def Field_def, auto)
   7.109  
   7.110 -lemma UnderS_Field: "UnderS A \<le> Field r"
   7.111 +lemma UnderS_Field: "UnderS r A \<le> Field r"
   7.112  by(unfold UnderS_def Field_def, auto)
   7.113  
   7.114 -lemma above_Field: "above a \<le> Field r"
   7.115 +lemma above_Field: "above r a \<le> Field r"
   7.116  by(unfold above_def Field_def, auto)
   7.117  
   7.118 -lemma aboveS_Field: "aboveS a \<le> Field r"
   7.119 +lemma aboveS_Field: "aboveS r a \<le> Field r"
   7.120  by(unfold aboveS_def Field_def, auto)
   7.121  
   7.122 -lemma Above_Field: "Above A \<le> Field r"
   7.123 +lemma Above_Field: "Above r A \<le> Field r"
   7.124  by(unfold Above_def Field_def, auto)
   7.125  
   7.126  lemma Refl_under_Under:
   7.127  assumes REFL: "Refl r" and NE: "A \<noteq> {}"
   7.128 -shows "Under A = (\<Inter> a \<in> A. under a)"
   7.129 +shows "Under r A = (\<Inter> a \<in> A. under r a)"
   7.130  proof
   7.131 -  show "Under A \<subseteq> (\<Inter> a \<in> A. under a)"
   7.132 +  show "Under r A \<subseteq> (\<Inter> a \<in> A. under r a)"
   7.133    by(unfold Under_def under_def, auto)
   7.134  next
   7.135 -  show "(\<Inter> a \<in> A. under a) \<subseteq> Under A"
   7.136 +  show "(\<Inter> a \<in> A. under r a) \<subseteq> Under r A"
   7.137    proof(auto)
   7.138      fix x
   7.139 -    assume *: "\<forall>xa \<in> A. x \<in> under xa"
   7.140 +    assume *: "\<forall>xa \<in> A. x \<in> under r xa"
   7.141      hence "\<forall>xa \<in> A. (x,xa) \<in> r"
   7.142      by (simp add: under_def)
   7.143      moreover
   7.144      {from NE obtain a where "a \<in> A" by blast
   7.145 -     with * have "x \<in> under a" by simp
   7.146 +     with * have "x \<in> under r a" by simp
   7.147       hence "x \<in> Field r"
   7.148 -     using under_Field[of a] by auto
   7.149 +     using under_Field[of r a] by auto
   7.150      }
   7.151 -    ultimately show "x \<in> Under A"
   7.152 +    ultimately show "x \<in> Under r A"
   7.153      unfolding Under_def by auto
   7.154    qed
   7.155  qed
   7.156  
   7.157  lemma Refl_underS_UnderS:
   7.158  assumes REFL: "Refl r" and NE: "A \<noteq> {}"
   7.159 -shows "UnderS A = (\<Inter> a \<in> A. underS a)"
   7.160 +shows "UnderS r A = (\<Inter> a \<in> A. underS r a)"
   7.161  proof
   7.162 -  show "UnderS A \<subseteq> (\<Inter> a \<in> A. underS a)"
   7.163 +  show "UnderS r A \<subseteq> (\<Inter> a \<in> A. underS r a)"
   7.164    by(unfold UnderS_def underS_def, auto)
   7.165  next
   7.166 -  show "(\<Inter> a \<in> A. underS a) \<subseteq> UnderS A"
   7.167 +  show "(\<Inter> a \<in> A. underS r a) \<subseteq> UnderS r A"
   7.168    proof(auto)
   7.169      fix x
   7.170 -    assume *: "\<forall>xa \<in> A. x \<in> underS xa"
   7.171 +    assume *: "\<forall>xa \<in> A. x \<in> underS r xa"
   7.172      hence "\<forall>xa \<in> A. x \<noteq> xa \<and> (x,xa) \<in> r"
   7.173      by (auto simp add: underS_def)
   7.174      moreover
   7.175      {from NE obtain a where "a \<in> A" by blast
   7.176 -     with * have "x \<in> underS a" by simp
   7.177 +     with * have "x \<in> underS r a" by simp
   7.178       hence "x \<in> Field r"
   7.179 -     using underS_Field[of a] by auto
   7.180 +     using underS_Field[of r a] by auto
   7.181      }
   7.182 -    ultimately show "x \<in> UnderS A"
   7.183 +    ultimately show "x \<in> UnderS r A"
   7.184      unfolding UnderS_def by auto
   7.185    qed
   7.186  qed
   7.187  
   7.188  lemma Refl_above_Above:
   7.189  assumes REFL: "Refl r" and NE: "A \<noteq> {}"
   7.190 -shows "Above A = (\<Inter> a \<in> A. above a)"
   7.191 +shows "Above r A = (\<Inter> a \<in> A. above r a)"
   7.192  proof
   7.193 -  show "Above A \<subseteq> (\<Inter> a \<in> A. above a)"
   7.194 +  show "Above r A \<subseteq> (\<Inter> a \<in> A. above r a)"
   7.195    by(unfold Above_def above_def, auto)
   7.196  next
   7.197 -  show "(\<Inter> a \<in> A. above a) \<subseteq> Above A"
   7.198 +  show "(\<Inter> a \<in> A. above r a) \<subseteq> Above r A"
   7.199    proof(auto)
   7.200      fix x
   7.201 -    assume *: "\<forall>xa \<in> A. x \<in> above xa"
   7.202 +    assume *: "\<forall>xa \<in> A. x \<in> above r xa"
   7.203      hence "\<forall>xa \<in> A. (xa,x) \<in> r"
   7.204      by (simp add: above_def)
   7.205      moreover
   7.206      {from NE obtain a where "a \<in> A" by blast
   7.207 -     with * have "x \<in> above a" by simp
   7.208 +     with * have "x \<in> above r a" by simp
   7.209       hence "x \<in> Field r"
   7.210 -     using above_Field[of a] by auto
   7.211 +     using above_Field[of r a] by auto
   7.212      }
   7.213 -    ultimately show "x \<in> Above A"
   7.214 +    ultimately show "x \<in> Above r A"
   7.215      unfolding Above_def by auto
   7.216    qed
   7.217  qed
   7.218  
   7.219  lemma Refl_aboveS_AboveS:
   7.220  assumes REFL: "Refl r" and NE: "A \<noteq> {}"
   7.221 -shows "AboveS A = (\<Inter> a \<in> A. aboveS a)"
   7.222 +shows "AboveS r A = (\<Inter> a \<in> A. aboveS r a)"
   7.223  proof
   7.224 -  show "AboveS A \<subseteq> (\<Inter> a \<in> A. aboveS a)"
   7.225 +  show "AboveS r A \<subseteq> (\<Inter> a \<in> A. aboveS r a)"
   7.226    by(unfold AboveS_def aboveS_def, auto)
   7.227  next
   7.228 -  show "(\<Inter> a \<in> A. aboveS a) \<subseteq> AboveS A"
   7.229 +  show "(\<Inter> a \<in> A. aboveS r a) \<subseteq> AboveS r A"
   7.230    proof(auto)
   7.231      fix x
   7.232 -    assume *: "\<forall>xa \<in> A. x \<in> aboveS xa"
   7.233 +    assume *: "\<forall>xa \<in> A. x \<in> aboveS r xa"
   7.234      hence "\<forall>xa \<in> A. xa \<noteq> x \<and> (xa,x) \<in> r"
   7.235      by (auto simp add: aboveS_def)
   7.236      moreover
   7.237      {from NE obtain a where "a \<in> A" by blast
   7.238 -     with * have "x \<in> aboveS a" by simp
   7.239 +     with * have "x \<in> aboveS r a" by simp
   7.240       hence "x \<in> Field r"
   7.241 -     using aboveS_Field[of a] by auto
   7.242 +     using aboveS_Field[of r a] by auto
   7.243      }
   7.244 -    ultimately show "x \<in> AboveS A"
   7.245 +    ultimately show "x \<in> AboveS r A"
   7.246      unfolding AboveS_def by auto
   7.247    qed
   7.248  qed
   7.249  
   7.250 -lemma under_Under_singl: "under a = Under {a}"
   7.251 +lemma under_Under_singl: "under r a = Under r {a}"
   7.252  by(unfold Under_def under_def, auto simp add: Field_def)
   7.253  
   7.254 -lemma underS_UnderS_singl: "underS a = UnderS {a}"
   7.255 +lemma underS_UnderS_singl: "underS r a = UnderS r {a}"
   7.256  by(unfold UnderS_def underS_def, auto simp add: Field_def)
   7.257  
   7.258 -lemma above_Above_singl: "above a = Above {a}"
   7.259 +lemma above_Above_singl: "above r a = Above r {a}"
   7.260  by(unfold Above_def above_def, auto simp add: Field_def)
   7.261  
   7.262 -lemma aboveS_AboveS_singl: "aboveS a = AboveS {a}"
   7.263 +lemma aboveS_AboveS_singl: "aboveS r a = AboveS r {a}"
   7.264  by(unfold AboveS_def aboveS_def, auto simp add: Field_def)
   7.265  
   7.266 -lemma Under_decr: "A \<le> B \<Longrightarrow> Under B \<le> Under A"
   7.267 +lemma Under_decr: "A \<le> B \<Longrightarrow> Under r B \<le> Under r A"
   7.268  by(unfold Under_def, auto)
   7.269  
   7.270 -lemma UnderS_decr: "A \<le> B \<Longrightarrow> UnderS B \<le> UnderS A"
   7.271 +lemma UnderS_decr: "A \<le> B \<Longrightarrow> UnderS r B \<le> UnderS r A"
   7.272  by(unfold UnderS_def, auto)
   7.273  
   7.274 -lemma Above_decr: "A \<le> B \<Longrightarrow> Above B \<le> Above A"
   7.275 +lemma Above_decr: "A \<le> B \<Longrightarrow> Above r B \<le> Above r A"
   7.276  by(unfold Above_def, auto)
   7.277  
   7.278 -lemma AboveS_decr: "A \<le> B \<Longrightarrow> AboveS B \<le> AboveS A"
   7.279 +lemma AboveS_decr: "A \<le> B \<Longrightarrow> AboveS r B \<le> AboveS r A"
   7.280  by(unfold AboveS_def, auto)
   7.281  
   7.282  lemma under_incl_iff:
   7.283  assumes TRANS: "trans r" and REFL: "Refl r" and IN: "a \<in> Field r"
   7.284 -shows "(under a \<le> under b) = ((a,b) \<in> r)"
   7.285 +shows "(under r a \<le> under r b) = ((a,b) \<in> r)"
   7.286  proof
   7.287    assume "(a,b) \<in> r"
   7.288 -  thus "under a \<le> under b" using TRANS
   7.289 +  thus "under r a \<le> under r b" using TRANS
   7.290    by (auto simp add: under_incr)
   7.291  next
   7.292 -  assume "under a \<le> under b"
   7.293 +  assume "under r a \<le> under r b"
   7.294    moreover
   7.295 -  have "a \<in> under a" using REFL IN
   7.296 +  have "a \<in> under r a" using REFL IN
   7.297    by (auto simp add: Refl_under_in)
   7.298    ultimately show "(a,b) \<in> r"
   7.299    by (auto simp add: under_def)
   7.300 @@ -273,7 +270,7 @@
   7.301  
   7.302  lemma above_decr:
   7.303  assumes TRANS: "trans r" and REL: "(a,b) \<in> r"
   7.304 -shows "above b \<le> above a"
   7.305 +shows "above r b \<le> above r a"
   7.306  proof(unfold above_def, auto)
   7.307    fix x assume "(b,x) \<in> r"
   7.308    with REL TRANS trans_def[of r]
   7.309 @@ -283,7 +280,7 @@
   7.310  lemma aboveS_decr:
   7.311  assumes TRANS: "trans r" and ANTISYM: "antisym r" and
   7.312          REL: "(a,b) \<in> r"
   7.313 -shows "aboveS b \<le> aboveS a"
   7.314 +shows "aboveS r b \<le> aboveS r a"
   7.315  proof(unfold aboveS_def, auto)
   7.316    assume *: "a \<noteq> b" and **: "(b,a) \<in> r"
   7.317    with ANTISYM antisym_def[of r] REL
   7.318 @@ -296,11 +293,11 @@
   7.319  
   7.320  lemma under_trans:
   7.321  assumes TRANS: "trans r" and
   7.322 -        IN1: "a \<in> under b" and IN2: "b \<in> under c"
   7.323 -shows "a \<in> under c"
   7.324 +        IN1: "a \<in> under r b" and IN2: "b \<in> under r c"
   7.325 +shows "a \<in> under r c"
   7.326  proof-
   7.327    have "(a,b) \<in> r \<and> (b,c) \<in> r"
   7.328 -  using IN1 IN2 under_def by auto
   7.329 +  using IN1 IN2 under_def by fastforce
   7.330    hence "(a,c) \<in> r"
   7.331    using TRANS trans_def[of r] by blast
   7.332    thus ?thesis unfolding under_def by simp
   7.333 @@ -308,14 +305,14 @@
   7.334  
   7.335  lemma under_underS_trans:
   7.336  assumes TRANS: "trans r" and ANTISYM: "antisym r" and
   7.337 -        IN1: "a \<in> under b" and IN2: "b \<in> underS c"
   7.338 -shows "a \<in> underS c"
   7.339 +        IN1: "a \<in> under r b" and IN2: "b \<in> underS r c"
   7.340 +shows "a \<in> underS r c"
   7.341  proof-
   7.342    have 0: "(a,b) \<in> r \<and> (b,c) \<in> r"
   7.343 -  using IN1 IN2 under_def underS_def by auto
   7.344 +  using IN1 IN2 under_def underS_def by fastforce
   7.345    hence 1: "(a,c) \<in> r"
   7.346    using TRANS trans_def[of r] by blast
   7.347 -  have 2: "b \<noteq> c" using IN2 underS_def by auto
   7.348 +  have 2: "b \<noteq> c" using IN2 underS_def by force
   7.349    have 3: "a \<noteq> c"
   7.350    proof
   7.351      assume "a = c" with 0 2 ANTISYM antisym_def[of r]
   7.352 @@ -326,14 +323,14 @@
   7.353  
   7.354  lemma underS_under_trans:
   7.355  assumes TRANS: "trans r" and ANTISYM: "antisym r" and
   7.356 -        IN1: "a \<in> underS b" and IN2: "b \<in> under c"
   7.357 -shows "a \<in> underS c"
   7.358 +        IN1: "a \<in> underS r b" and IN2: "b \<in> under r c"
   7.359 +shows "a \<in> underS r c"
   7.360  proof-
   7.361    have 0: "(a,b) \<in> r \<and> (b,c) \<in> r"
   7.362 -  using IN1 IN2 under_def underS_def by auto
   7.363 +  using IN1 IN2 under_def underS_def by fast
   7.364    hence 1: "(a,c) \<in> r"
   7.365 -  using TRANS trans_def[of r] by blast
   7.366 -  have 2: "a \<noteq> b" using IN1 underS_def by auto
   7.367 +  using TRANS trans_def[of r] by fast
   7.368 +  have 2: "a \<noteq> b" using IN1 underS_def by force
   7.369    have 3: "a \<noteq> c"
   7.370    proof
   7.371      assume "a = c" with 0 2 ANTISYM antisym_def[of r]
   7.372 @@ -344,21 +341,21 @@
   7.373  
   7.374  lemma underS_underS_trans:
   7.375  assumes TRANS: "trans r" and ANTISYM: "antisym r" and
   7.376 -        IN1: "a \<in> underS b" and IN2: "b \<in> underS c"
   7.377 -shows "a \<in> underS c"
   7.378 +        IN1: "a \<in> underS r b" and IN2: "b \<in> underS r c"
   7.379 +shows "a \<in> underS r c"
   7.380  proof-
   7.381 -  have "a \<in> under b"
   7.382 -  using IN1 underS_subset_under by auto
   7.383 -  with assms under_underS_trans show ?thesis by auto
   7.384 +  have "a \<in> under r b"
   7.385 +  using IN1 underS_subset_under by fast
   7.386 +  with assms under_underS_trans show ?thesis by fast
   7.387  qed
   7.388  
   7.389  lemma above_trans:
   7.390  assumes TRANS: "trans r" and
   7.391 -        IN1: "b \<in> above a" and IN2: "c \<in> above b"
   7.392 -shows "c \<in> above a"
   7.393 +        IN1: "b \<in> above r a" and IN2: "c \<in> above r b"
   7.394 +shows "c \<in> above r a"
   7.395  proof-
   7.396    have "(a,b) \<in> r \<and> (b,c) \<in> r"
   7.397 -  using IN1 IN2 above_def by auto
   7.398 +  using IN1 IN2 above_def by fast
   7.399    hence "(a,c) \<in> r"
   7.400    using TRANS trans_def[of r] by blast
   7.401    thus ?thesis unfolding above_def by simp
   7.402 @@ -366,14 +363,14 @@
   7.403  
   7.404  lemma above_aboveS_trans:
   7.405  assumes TRANS: "trans r" and ANTISYM: "antisym r" and
   7.406 -        IN1: "b \<in> above a" and IN2: "c \<in> aboveS b"
   7.407 -shows "c \<in> aboveS a"
   7.408 +        IN1: "b \<in> above r a" and IN2: "c \<in> aboveS r b"
   7.409 +shows "c \<in> aboveS r a"
   7.410  proof-
   7.411    have 0: "(a,b) \<in> r \<and> (b,c) \<in> r"
   7.412 -  using IN1 IN2 above_def aboveS_def by auto
   7.413 +  using IN1 IN2 above_def aboveS_def by fast
   7.414    hence 1: "(a,c) \<in> r"
   7.415    using TRANS trans_def[of r] by blast
   7.416 -  have 2: "b \<noteq> c" using IN2 aboveS_def by auto
   7.417 +  have 2: "b \<noteq> c" using IN2 aboveS_def by force
   7.418    have 3: "a \<noteq> c"
   7.419    proof
   7.420      assume "a = c" with 0 2 ANTISYM antisym_def[of r]
   7.421 @@ -384,14 +381,14 @@
   7.422  
   7.423  lemma aboveS_above_trans:
   7.424  assumes TRANS: "trans r" and ANTISYM: "antisym r" and
   7.425 -        IN1: "b \<in> aboveS a" and IN2: "c \<in> above b"
   7.426 -shows "c \<in> aboveS a"
   7.427 +        IN1: "b \<in> aboveS r a" and IN2: "c \<in> above r b"
   7.428 +shows "c \<in> aboveS r a"
   7.429  proof-
   7.430    have 0: "(a,b) \<in> r \<and> (b,c) \<in> r"
   7.431 -  using IN1 IN2 above_def aboveS_def by auto
   7.432 +  using IN1 IN2 above_def aboveS_def by fast
   7.433    hence 1: "(a,c) \<in> r"
   7.434    using TRANS trans_def[of r] by blast
   7.435 -  have 2: "a \<noteq> b" using IN1 aboveS_def by auto
   7.436 +  have 2: "a \<noteq> b" using IN1 aboveS_def by force
   7.437    have 3: "a \<noteq> c"
   7.438    proof
   7.439      assume "a = c" with 0 2 ANTISYM antisym_def[of r]
   7.440 @@ -402,21 +399,23 @@
   7.441  
   7.442  lemma aboveS_aboveS_trans:
   7.443  assumes TRANS: "trans r" and ANTISYM: "antisym r" and
   7.444 -        IN1: "b \<in> aboveS a" and IN2: "c \<in> aboveS b"
   7.445 -shows "c \<in> aboveS a"
   7.446 +        IN1: "b \<in> aboveS r a" and IN2: "c \<in> aboveS r b"
   7.447 +shows "c \<in> aboveS r a"
   7.448  proof-
   7.449 -  have "b \<in> above a"
   7.450 -  using IN1 aboveS_subset_above by auto
   7.451 -  with assms above_aboveS_trans show ?thesis by auto
   7.452 +  have "b \<in> above r a"
   7.453 +  using IN1 aboveS_subset_above by fast
   7.454 +  with assms above_aboveS_trans show ?thesis by fast
   7.455  qed
   7.456  
   7.457  lemma under_Under_trans:
   7.458  assumes TRANS: "trans r" and
   7.459 -        IN1: "a \<in> under b" and IN2: "b \<in> Under C"
   7.460 -shows "a \<in> Under C"
   7.461 +        IN1: "a \<in> under r b" and IN2: "b \<in> Under r C"
   7.462 +shows "a \<in> Under r C"
   7.463  proof-
   7.464 -  have "(a,b) \<in> r \<and> (\<forall>c \<in> C. (b,c) \<in> r)"
   7.465 -  using IN1 IN2 under_def Under_def by blast
   7.466 +  have "b \<in> {u \<in> Field r. \<forall>x. x \<in> C \<longrightarrow> (u, x) \<in> r}"
   7.467 +    using IN2 Under_def by force
   7.468 +  hence "(a,b) \<in> r \<and> (\<forall>c \<in> C. (b,c) \<in> r)"
   7.469 +    using IN1 under_def by fast
   7.470    hence "\<forall>c \<in> C. (a,c) \<in> r"
   7.471    using TRANS trans_def[of r] by blast
   7.472    moreover
   7.473 @@ -427,22 +426,22 @@
   7.474  
   7.475  lemma underS_Under_trans:
   7.476  assumes TRANS: "trans r" and ANTISYM: "antisym r" and
   7.477 -        IN1: "a \<in> underS b" and IN2: "b \<in> Under C"
   7.478 -shows "a \<in> UnderS C"
   7.479 +        IN1: "a \<in> underS r b" and IN2: "b \<in> Under r C"
   7.480 +shows "a \<in> UnderS r C"
   7.481  proof-
   7.482 -  from IN1 have "a \<in> under b"
   7.483 -  using underS_subset_under[of b] by blast
   7.484 +  from IN1 have "a \<in> under r b"
   7.485 +  using underS_subset_under[of r b] by fast
   7.486    with assms under_Under_trans
   7.487 -  have "a \<in> Under C" by auto
   7.488 +  have "a \<in> Under r C" by fast
   7.489    (*  *)
   7.490    moreover
   7.491    have "a \<notin> C"
   7.492    proof
   7.493      assume *: "a \<in> C"
   7.494      have 1: "b \<noteq> a \<and> (a,b) \<in> r"
   7.495 -    using IN1 underS_def[of b] by auto
   7.496 +    using IN1 underS_def[of r b] by auto
   7.497      have "\<forall>c \<in> C. (b,c) \<in> r"
   7.498 -    using IN2 Under_def[of C] by auto
   7.499 +    using IN2 Under_def[of r C] by auto
   7.500      with * have "(b,a) \<in> r" by simp
   7.501      with 1 ANTISYM antisym_def[of r]
   7.502      show False by blast
   7.503 @@ -450,53 +449,53 @@
   7.504    (*  *)
   7.505    ultimately
   7.506    show ?thesis unfolding UnderS_def
   7.507 -  using Under_def by auto
   7.508 +  using Under_def by force
   7.509  qed
   7.510  
   7.511  lemma underS_UnderS_trans:
   7.512  assumes TRANS: "trans r" and ANTISYM: "antisym r" and
   7.513 -        IN1: "a \<in> underS b" and IN2: "b \<in> UnderS C"
   7.514 -shows "a \<in> UnderS C"
   7.515 +        IN1: "a \<in> underS r b" and IN2: "b \<in> UnderS r C"
   7.516 +shows "a \<in> UnderS r C"
   7.517  proof-
   7.518 -  from IN2 have "b \<in> Under C"
   7.519 -  using UnderS_subset_Under[of C] by blast
   7.520 +  from IN2 have "b \<in> Under r C"
   7.521 +  using UnderS_subset_Under[of r C] by blast
   7.522    with underS_Under_trans assms
   7.523 -  show ?thesis by auto
   7.524 +  show ?thesis by force
   7.525  qed
   7.526  
   7.527  lemma above_Above_trans:
   7.528  assumes TRANS: "trans r" and
   7.529 -        IN1: "a \<in> above b" and IN2: "b \<in> Above C"
   7.530 -shows "a \<in> Above C"
   7.531 +        IN1: "a \<in> above r b" and IN2: "b \<in> Above r C"
   7.532 +shows "a \<in> Above r C"
   7.533  proof-
   7.534    have "(b,a) \<in> r \<and> (\<forall>c \<in> C. (c,b) \<in> r)"
   7.535 -  using IN1 IN2 above_def Above_def by auto
   7.536 +    using IN1[unfolded above_def] IN2[unfolded Above_def] by simp
   7.537    hence "\<forall>c \<in> C. (c,a) \<in> r"
   7.538    using TRANS trans_def[of r] by blast
   7.539    moreover
   7.540 -  have "a \<in> Field r" using IN1 Field_def above_def by force
   7.541 +  have "a \<in> Field r" using IN1[unfolded above_def] Field_def by fast
   7.542    ultimately
   7.543    show ?thesis unfolding Above_def by auto
   7.544  qed
   7.545  
   7.546  lemma aboveS_Above_trans:
   7.547  assumes TRANS: "trans r" and ANTISYM: "antisym r" and
   7.548 -        IN1: "a \<in> aboveS b" and IN2: "b \<in> Above C"
   7.549 -shows "a \<in> AboveS C"
   7.550 +        IN1: "a \<in> aboveS r b" and IN2: "b \<in> Above r C"
   7.551 +shows "a \<in> AboveS r C"
   7.552  proof-
   7.553 -  from IN1 have "a \<in> above b"
   7.554 -  using aboveS_subset_above[of b] by blast
   7.555 +  from IN1 have "a \<in> above r b"
   7.556 +  using aboveS_subset_above[of r b] by blast
   7.557    with assms above_Above_trans
   7.558 -  have "a \<in> Above C" by auto
   7.559 +  have "a \<in> Above r C" by fast
   7.560    (*  *)
   7.561    moreover
   7.562    have "a \<notin> C"
   7.563    proof
   7.564      assume *: "a \<in> C"
   7.565      have 1: "b \<noteq> a \<and> (b,a) \<in> r"
   7.566 -    using IN1 aboveS_def[of b] by auto
   7.567 +    using IN1 aboveS_def[of r b] by auto
   7.568      have "\<forall>c \<in> C. (c,b) \<in> r"
   7.569 -    using IN2 Above_def[of C] by auto
   7.570 +    using IN2 Above_def[of r C] by auto
   7.571      with * have "(a,b) \<in> r" by simp
   7.572      with 1 ANTISYM antisym_def[of r]
   7.573      show False by blast
   7.574 @@ -504,27 +503,27 @@
   7.575    (*  *)
   7.576    ultimately
   7.577    show ?thesis unfolding AboveS_def
   7.578 -  using Above_def by auto
   7.579 +  using Above_def by force
   7.580  qed
   7.581  
   7.582  lemma above_AboveS_trans:
   7.583  assumes TRANS: "trans r" and ANTISYM: "antisym r" and
   7.584 -        IN1: "a \<in> above b" and IN2: "b \<in> AboveS C"
   7.585 -shows "a \<in> AboveS C"
   7.586 +        IN1: "a \<in> above r b" and IN2: "b \<in> AboveS r C"
   7.587 +shows "a \<in> AboveS r C"
   7.588  proof-
   7.589 -  from IN2 have "b \<in> Above C"
   7.590 -  using AboveS_subset_Above[of C] by blast
   7.591 +  from IN2 have "b \<in> Above r C"
   7.592 +  using AboveS_subset_Above[of r C] by blast
   7.593    with assms above_Above_trans
   7.594 -  have "a \<in> Above C" by auto
   7.595 +  have "a \<in> Above r C" by force
   7.596    (*  *)
   7.597    moreover
   7.598    have "a \<notin> C"
   7.599    proof
   7.600      assume *: "a \<in> C"
   7.601      have 1: "(b,a) \<in> r"
   7.602 -    using IN1 above_def[of b] by auto
   7.603 +    using IN1 above_def[of r b] by auto
   7.604      have "\<forall>c \<in> C. b \<noteq> c \<and> (c,b) \<in> r"
   7.605 -    using IN2 AboveS_def[of C] by auto
   7.606 +    using IN2 AboveS_def[of r C] by auto
   7.607      with * have "b \<noteq> a \<and> (a,b) \<in> r" by simp
   7.608      with 1 ANTISYM antisym_def[of r]
   7.609      show False by blast
   7.610 @@ -532,38 +531,38 @@
   7.611    (*  *)
   7.612    ultimately
   7.613    show ?thesis unfolding AboveS_def
   7.614 -  using Above_def by auto
   7.615 +  using Above_def by force
   7.616  qed
   7.617  
   7.618  lemma aboveS_AboveS_trans:
   7.619  assumes TRANS: "trans r" and ANTISYM: "antisym r" and
   7.620 -        IN1: "a \<in> aboveS b" and IN2: "b \<in> AboveS C"
   7.621 -shows "a \<in> AboveS C"
   7.622 +        IN1: "a \<in> aboveS r b" and IN2: "b \<in> AboveS r C"
   7.623 +shows "a \<in> AboveS r C"
   7.624  proof-
   7.625 -  from IN2 have "b \<in> Above C"
   7.626 -  using AboveS_subset_Above[of C] by blast
   7.627 +  from IN2 have "b \<in> Above r C"
   7.628 +  using AboveS_subset_Above[of r C] by blast
   7.629    with aboveS_Above_trans assms
   7.630 -  show ?thesis by auto
   7.631 +  show ?thesis by force
   7.632  qed
   7.633  
   7.634  lemma under_UnderS_trans:
   7.635  assumes TRANS: "trans r" and ANTISYM: "antisym r" and
   7.636 -        IN1: "a \<in> under b" and IN2: "b \<in> UnderS C"
   7.637 -shows "a \<in> UnderS C"
   7.638 +        IN1: "a \<in> under r b" and IN2: "b \<in> UnderS r C"
   7.639 +shows "a \<in> UnderS r C"
   7.640  proof-
   7.641 -  from IN2 have "b \<in> Under C"
   7.642 -  using UnderS_subset_Under[of C] by blast
   7.643 +  from IN2 have "b \<in> Under r C"
   7.644 +  using UnderS_subset_Under[of r C] by blast
   7.645    with assms under_Under_trans
   7.646 -  have "a \<in> Under C" by blast
   7.647 +  have "a \<in> Under r C" by force
   7.648    (*  *)
   7.649    moreover
   7.650    have "a \<notin> C"
   7.651    proof
   7.652      assume *: "a \<in> C"
   7.653      have 1: "(a,b) \<in> r"
   7.654 -    using IN1 under_def[of b] by auto
   7.655 +    using IN1 under_def[of r b] by auto
   7.656      have "\<forall>c \<in> C. b \<noteq> c \<and> (b,c) \<in> r"
   7.657 -    using IN2 UnderS_def[of C] by blast
   7.658 +    using IN2 UnderS_def[of r C] by blast
   7.659      with * have "b \<noteq> a \<and> (b,a) \<in> r" by blast
   7.660      with 1 ANTISYM antisym_def[of r]
   7.661      show False by blast
   7.662 @@ -573,66 +572,59 @@
   7.663    show ?thesis unfolding UnderS_def Under_def by fast
   7.664  qed
   7.665  
   7.666 -end  (* context rel *)
   7.667 -
   7.668  
   7.669  subsection {* Properties depending on more than one relation  *}
   7.670  
   7.671 -abbreviation "under \<equiv> rel.under"
   7.672 -abbreviation "underS \<equiv> rel.underS"
   7.673 -abbreviation "Under \<equiv> rel.Under"
   7.674 -abbreviation "UnderS \<equiv> rel.UnderS"
   7.675 -abbreviation "above \<equiv> rel.above"
   7.676 -abbreviation "aboveS \<equiv> rel.aboveS"
   7.677 -abbreviation "Above \<equiv> rel.Above"
   7.678 -abbreviation "AboveS \<equiv> rel.AboveS"
   7.679 -
   7.680  lemma under_incr2:
   7.681  "r \<le> r' \<Longrightarrow> under r a \<le> under r' a"
   7.682 -unfolding rel.under_def by blast
   7.683 +unfolding under_def by blast
   7.684  
   7.685  lemma underS_incr2:
   7.686  "r \<le> r' \<Longrightarrow> underS r a \<le> underS r' a"
   7.687 -unfolding rel.underS_def by blast
   7.688 +unfolding underS_def by blast
   7.689  
   7.690 +(* FIXME: r \<leadsto> r'
   7.691  lemma Under_incr:
   7.692  "r \<le> r' \<Longrightarrow> Under r A \<le> Under r A"
   7.693 -unfolding rel.Under_def by blast
   7.694 +unfolding Under_def by blast
   7.695  
   7.696  lemma UnderS_incr:
   7.697  "r \<le> r' \<Longrightarrow> UnderS r A \<le> UnderS r A"
   7.698 -unfolding rel.UnderS_def by blast
   7.699 +unfolding UnderS_def by blast
   7.700  
   7.701  lemma Under_incr_decr:
   7.702  "\<lbrakk>r \<le> r'; A' \<le> A\<rbrakk>  \<Longrightarrow> Under r A \<le> Under r A'"
   7.703 -unfolding rel.Under_def by blast
   7.704 +unfolding Under_def by blast
   7.705  
   7.706  lemma UnderS_incr_decr:
   7.707  "\<lbrakk>r \<le> r'; A' \<le> A\<rbrakk>  \<Longrightarrow> UnderS r A \<le> UnderS r A'"
   7.708 -unfolding rel.UnderS_def by blast
   7.709 +unfolding UnderS_def by blast
   7.710 +*)
   7.711  
   7.712  lemma above_incr2:
   7.713  "r \<le> r' \<Longrightarrow> above r a \<le> above r' a"
   7.714 -unfolding rel.above_def by blast
   7.715 +unfolding above_def by blast
   7.716  
   7.717  lemma aboveS_incr2:
   7.718  "r \<le> r' \<Longrightarrow> aboveS r a \<le> aboveS r' a"
   7.719 -unfolding rel.aboveS_def by blast
   7.720 +unfolding aboveS_def by blast
   7.721  
   7.722 +(* FIXME
   7.723  lemma Above_incr:
   7.724  "r \<le> r' \<Longrightarrow> Above r A \<le> Above r A"
   7.725 -unfolding rel.Above_def by blast
   7.726 +unfolding Above_def by blast
   7.727  
   7.728  lemma AboveS_incr:
   7.729  "r \<le> r' \<Longrightarrow> AboveS r A \<le> AboveS r A"
   7.730 -unfolding rel.AboveS_def by blast
   7.731 +unfolding AboveS_def by blast
   7.732  
   7.733  lemma Above_incr_decr:
   7.734 -"\<lbrakk>r \<le> r'; A' \<le> A\<rbrakk>  \<Longrightarrow> Above r A \<le> Above r A'"
   7.735 -unfolding rel.Above_def by blast
   7.736 +"\<lbrakk>r \<le> r'; A' \<le> A\<rbrakk> \<Longrightarrow> Above r A \<le> Above r A'"
   7.737 +unfolding Above_def by blast
   7.738  
   7.739  lemma AboveS_incr_decr:
   7.740 -"\<lbrakk>r \<le> r'; A' \<le> A\<rbrakk>  \<Longrightarrow> AboveS r A \<le> AboveS r A'"
   7.741 -unfolding rel.AboveS_def by blast
   7.742 +"\<lbrakk>r \<le> r'; A' \<le> A\<rbrakk> \<Longrightarrow> AboveS r A \<le> AboveS r A'"
   7.743 +unfolding AboveS_def by blast
   7.744 +*)
   7.745  
   7.746  end
     8.1 --- a/src/HOL/Cardinals/Order_Relation_More_FP.thy	Thu Jan 16 18:52:50 2014 +0100
     8.2 +++ b/src/HOL/Cardinals/Order_Relation_More_FP.thy	Thu Jan 16 20:52:54 2014 +0100
     8.3 @@ -19,16 +19,6 @@
     8.4  further define upper and lower bounds operators. *}
     8.5  
     8.6  
     8.7 -locale rel = fixes r :: "'a rel"
     8.8 -
     8.9 -text{* The following context encompasses all this section, except
    8.10 -for its last subsection. In other words, for the rest of this section except its last
    8.11 -subsection, we consider a fixed relation @{text "r"}. *}
    8.12 -
    8.13 -context rel
    8.14 -begin
    8.15 -
    8.16 -
    8.17  subsection {* Auxiliaries *}
    8.18  
    8.19  
    8.20 @@ -39,7 +29,7 @@
    8.21  
    8.22  corollary well_order_on_domain:
    8.23  "\<lbrakk>well_order_on A r; (a,b) \<in> r\<rbrakk> \<Longrightarrow> a \<in> A \<and> b \<in> A"
    8.24 -by(simp add: refl_on_domain order_on_defs)
    8.25 +by (auto simp add: refl_on_domain order_on_defs)
    8.26  
    8.27  
    8.28  lemma well_order_on_Field:
    8.29 @@ -49,7 +39,7 @@
    8.30  
    8.31  lemma well_order_on_Well_order:
    8.32  "well_order_on A r \<Longrightarrow> A = Field r \<and> Well_order r"
    8.33 -using well_order_on_Field by simp
    8.34 +using well_order_on_Field by auto
    8.35  
    8.36  
    8.37  lemma Total_subset_Id:
    8.38 @@ -91,103 +81,91 @@
    8.39  Capitalization of the first letter in the name reminds that the operator acts on sets, rather
    8.40  than on individual elements. *}
    8.41  
    8.42 -definition under::"'a \<Rightarrow> 'a set"
    8.43 -where "under a \<equiv> {b. (b,a) \<in> r}"
    8.44 +definition under::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
    8.45 +where "under r a \<equiv> {b. (b,a) \<in> r}"
    8.46  
    8.47 -definition underS::"'a \<Rightarrow> 'a set"
    8.48 -where "underS a \<equiv> {b. b \<noteq> a \<and> (b,a) \<in> r}"
    8.49 +definition underS::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
    8.50 +where "underS r a \<equiv> {b. b \<noteq> a \<and> (b,a) \<in> r}"
    8.51  
    8.52 -definition Under::"'a set \<Rightarrow> 'a set"
    8.53 -where "Under A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (b,a) \<in> r}"
    8.54 +definition Under::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
    8.55 +where "Under r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (b,a) \<in> r}"
    8.56  
    8.57 -definition UnderS::"'a set \<Rightarrow> 'a set"
    8.58 -where "UnderS A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (b,a) \<in> r}"
    8.59 +definition UnderS::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
    8.60 +where "UnderS r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (b,a) \<in> r}"
    8.61  
    8.62 -definition above::"'a \<Rightarrow> 'a set"
    8.63 -where "above a \<equiv> {b. (a,b) \<in> r}"
    8.64 +definition above::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
    8.65 +where "above r a \<equiv> {b. (a,b) \<in> r}"
    8.66  
    8.67 -definition aboveS::"'a \<Rightarrow> 'a set"
    8.68 -where "aboveS a \<equiv> {b. b \<noteq> a \<and> (a,b) \<in> r}"
    8.69 +definition aboveS::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
    8.70 +where "aboveS r a \<equiv> {b. b \<noteq> a \<and> (a,b) \<in> r}"
    8.71  
    8.72 -definition Above::"'a set \<Rightarrow> 'a set"
    8.73 -where "Above A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (a,b) \<in> r}"
    8.74 +definition Above::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
    8.75 +where "Above r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (a,b) \<in> r}"
    8.76  
    8.77 -definition AboveS::"'a set \<Rightarrow> 'a set"
    8.78 -where "AboveS A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (a,b) \<in> r}"
    8.79 -(*  *)
    8.80 +definition AboveS::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
    8.81 +where "AboveS r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (a,b) \<in> r}"
    8.82  
    8.83  text{* Note:  In the definitions of @{text "Above[S]"} and @{text "Under[S]"},
    8.84    we bounded comprehension by @{text "Field r"} in order to properly cover
    8.85    the case of @{text "A"} being empty. *}
    8.86  
    8.87 -
    8.88 -lemma underS_subset_under: "underS a \<le> under a"
    8.89 +lemma underS_subset_under: "underS r a \<le> under r a"
    8.90  by(auto simp add: underS_def under_def)
    8.91  
    8.92  
    8.93 -lemma underS_notIn: "a \<notin> underS a"
    8.94 +lemma underS_notIn: "a \<notin> underS r a"
    8.95  by(simp add: underS_def)
    8.96  
    8.97  
    8.98 -lemma Refl_under_in: "\<lbrakk>Refl r; a \<in> Field r\<rbrakk> \<Longrightarrow> a \<in> under a"
    8.99 +lemma Refl_under_in: "\<lbrakk>Refl r; a \<in> Field r\<rbrakk> \<Longrightarrow> a \<in> under r a"
   8.100  by(simp add: refl_on_def under_def)
   8.101  
   8.102  
   8.103 -lemma AboveS_disjoint: "A Int (AboveS A) = {}"
   8.104 +lemma AboveS_disjoint: "A Int (AboveS r A) = {}"
   8.105  by(auto simp add: AboveS_def)
   8.106  
   8.107 -
   8.108 -lemma in_AboveS_underS: "a \<in> Field r \<Longrightarrow> a \<in> AboveS (underS a)"
   8.109 +lemma in_AboveS_underS: "a \<in> Field r \<Longrightarrow> a \<in> AboveS r (underS r a)"
   8.110  by(auto simp add: AboveS_def underS_def)
   8.111  
   8.112 -
   8.113  lemma Refl_under_underS:
   8.114 -assumes "Refl r" "a \<in> Field r"
   8.115 -shows "under a = underS a \<union> {a}"
   8.116 +  assumes "Refl r" "a \<in> Field r"
   8.117 +  shows "under r a = underS r a \<union> {a}"
   8.118  unfolding under_def underS_def
   8.119  using assms refl_on_def[of _ r] by fastforce
   8.120  
   8.121 -
   8.122 -lemma underS_empty: "a \<notin> Field r \<Longrightarrow> underS a = {}"
   8.123 +lemma underS_empty: "a \<notin> Field r \<Longrightarrow> underS r a = {}"
   8.124  by (auto simp: Field_def underS_def)
   8.125  
   8.126 -
   8.127 -lemma under_Field: "under a \<le> Field r"
   8.128 +lemma under_Field: "under r a \<le> Field r"
   8.129  by(unfold under_def Field_def, auto)
   8.130  
   8.131 -
   8.132 -lemma underS_Field: "underS a \<le> Field r"
   8.133 +lemma underS_Field: "underS r a \<le> Field r"
   8.134  by(unfold underS_def Field_def, auto)
   8.135  
   8.136 -
   8.137  lemma underS_Field2:
   8.138 -"a \<in> Field r \<Longrightarrow> underS a < Field r"
   8.139 -using assms underS_notIn underS_Field by blast
   8.140 -
   8.141 +"a \<in> Field r \<Longrightarrow> underS r a < Field r"
   8.142 +using underS_notIn underS_Field by fast
   8.143  
   8.144  lemma underS_Field3:
   8.145 -"Field r \<noteq> {} \<Longrightarrow> underS a < Field r"
   8.146 +"Field r \<noteq> {} \<Longrightarrow> underS r a < Field r"
   8.147  by(cases "a \<in> Field r", simp add: underS_Field2, auto simp add: underS_empty)
   8.148  
   8.149 -
   8.150 -lemma AboveS_Field: "AboveS A \<le> Field r"
   8.151 +lemma AboveS_Field: "AboveS r A \<le> Field r"
   8.152  by(unfold AboveS_def Field_def, auto)
   8.153  
   8.154 -
   8.155  lemma under_incr:
   8.156 -assumes TRANS: "trans r" and REL: "(a,b) \<in> r"
   8.157 -shows "under a \<le> under b"
   8.158 +  assumes TRANS: "trans r" and REL: "(a,b) \<in> r"
   8.159 +  shows "under r a \<le> under r b"
   8.160  proof(unfold under_def, auto)
   8.161    fix x assume "(x,a) \<in> r"
   8.162    with REL TRANS trans_def[of r]
   8.163    show "(x,b) \<in> r" by blast
   8.164  qed
   8.165  
   8.166 -
   8.167  lemma underS_incr:
   8.168  assumes TRANS: "trans r" and ANTISYM: "antisym r" and
   8.169          REL: "(a,b) \<in> r"
   8.170 -shows "underS a \<le> underS b"
   8.171 +shows "underS r a \<le> underS r b"
   8.172  proof(unfold underS_def, auto)
   8.173    assume *: "b \<noteq> a" and **: "(b,a) \<in> r"
   8.174    with ANTISYM antisym_def[of r] REL
   8.175 @@ -198,25 +176,24 @@
   8.176    show "(x,b) \<in> r" by blast
   8.177  qed
   8.178  
   8.179 -
   8.180  lemma underS_incl_iff:
   8.181  assumes LO: "Linear_order r" and
   8.182          INa: "a \<in> Field r" and INb: "b \<in> Field r"
   8.183 -shows "(underS a \<le> underS b) = ((a,b) \<in> r)"
   8.184 +shows "(underS r a \<le> underS r b) = ((a,b) \<in> r)"
   8.185  proof
   8.186    assume "(a,b) \<in> r"
   8.187 -  thus "underS a \<le> underS b" using LO
   8.188 +  thus "underS r a \<le> underS r b" using LO
   8.189    by (simp add: order_on_defs underS_incr)
   8.190  next
   8.191 -  assume *: "underS a \<le> underS b"
   8.192 +  assume *: "underS r a \<le> underS r b"
   8.193    {assume "a = b"
   8.194     hence "(a,b) \<in> r" using assms
   8.195     by (simp add: order_on_defs refl_on_def)
   8.196    }
   8.197    moreover
   8.198    {assume "a \<noteq> b \<and> (b,a) \<in> r"
   8.199 -   hence "b \<in> underS a" unfolding underS_def by blast
   8.200 -   hence "b \<in> underS b" using * by blast
   8.201 +   hence "b \<in> underS r a" unfolding underS_def by blast
   8.202 +   hence "b \<in> underS r b" using * by blast
   8.203     hence False by (simp add: underS_notIn)
   8.204    }
   8.205    ultimately
   8.206 @@ -224,7 +201,4 @@
   8.207    order_on_defs[of "Field r" r] total_on_def[of "Field r" r] by blast
   8.208  qed
   8.209  
   8.210 -
   8.211 -end  (* context rel *)
   8.212 -
   8.213  end
     9.1 --- a/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Thu Jan 16 18:52:50 2014 +0100
     9.2 +++ b/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Thu Jan 16 20:52:54 2014 +0100
     9.3 @@ -148,7 +148,7 @@
     9.4    have "compat r (r +o r') Inl" unfolding compat_def osum_def by auto
     9.5    moreover
     9.6    have "ofilter (r +o r') (Inl ` Field r)"
     9.7 -    unfolding wo_rel.ofilter_def[unfolded wo_rel_def, OF 1] Field_osum rel.under_def
     9.8 +    unfolding wo_rel.ofilter_def[unfolded wo_rel_def, OF 1] Field_osum under_def
     9.9      unfolding osum_def Field_def by auto
    9.10    ultimately show ?thesis using assms by (auto simp add: embed_iff_compat_inj_on_ofilter)
    9.11  qed
    9.12 @@ -322,7 +322,7 @@
    9.13    from r' have "compat r (r *o r') ?f"  unfolding compat_def oprod_def by auto
    9.14    moreover
    9.15    from * have "ofilter (r *o r') (?f ` Field r)"
    9.16 -    unfolding wo_rel.ofilter_def[unfolded wo_rel_def, OF 1] Field_oprod rel.under_def
    9.17 +    unfolding wo_rel.ofilter_def[unfolded wo_rel_def, OF 1] Field_oprod under_def
    9.18      unfolding oprod_def by auto (auto simp: image_iff Field_def)
    9.19    moreover have "inj_on ?f (Field r)" unfolding inj_on_def by auto
    9.20    ultimately show ?thesis using assms by (auto simp add: embed_iff_compat_inj_on_ofilter)
    9.21 @@ -924,11 +924,11 @@
    9.22  
    9.23  lemma iso_ozero_empty[simp]: "r =o ozero = (r = {})"
    9.24    unfolding ozero_def ordIso_def iso_def[abs_def] embed_def bij_betw_def 
    9.25 -  by (auto dest: rel.well_order_on_domain)
    9.26 +  by (auto dest: well_order_on_domain)
    9.27  
    9.28  lemma ozero_ordLeq: 
    9.29  assumes "Well_order r"  shows "ozero \<le>o r"
    9.30 -using assms unfolding ozero_def ordLeq_def embed_def[abs_def] rel.under_def by auto
    9.31 +using assms unfolding ozero_def ordLeq_def embed_def[abs_def] under_def by auto
    9.32  
    9.33  definition "oone = {((),())}"
    9.34  
    9.35 @@ -942,10 +942,10 @@
    9.36  lemma oone_ordIso: "oone =o {(x,x)}"
    9.37    unfolding ordIso_def oone_def well_order_on_def linear_order_on_def partial_order_on_def
    9.38      preorder_on_def total_on_def refl_on_def trans_def antisym_def
    9.39 -  by (auto simp: iso_def embed_def bij_betw_def rel.under_def inj_on_def intro!: exI[of _ "\<lambda>_. x"])
    9.40 +  by (auto simp: iso_def embed_def bij_betw_def under_def inj_on_def intro!: exI[of _ "\<lambda>_. x"])
    9.41  
    9.42  lemma osum_ordLeqR: "Well_order r \<Longrightarrow> Well_order s \<Longrightarrow> s \<le>o r +o s"
    9.43 -  unfolding ordLeq_def2 rel.underS_def
    9.44 +  unfolding ordLeq_def2 underS_def
    9.45    by (auto intro!: exI[of _ Inr] osum_Well_order) (auto simp add: osum_def Field_def)
    9.46  
    9.47  lemma osum_congL:
    9.48 @@ -1043,7 +1043,7 @@
    9.49      unfolding Field_oprod iso_def bij_betw_def inj_on_def by fastforce
    9.50    with f have "bij_betw ?f (Field ?L) (Field ?R)"
    9.51      unfolding Field_oprod iso_def bij_betw_def by (auto intro!: map_pair_surj_on)
    9.52 -  moreover from f rel.well_order_on_domain[OF r] have "compat ?L ?R ?f"
    9.53 +  moreover from f well_order_on_domain[OF r] have "compat ?L ?R ?f"
    9.54      unfolding iso_iff3[OF r s] compat_def oprod_def bij_betw_def
    9.55      by (auto simp: map_pair_imageI dest: inj_onD)
    9.56    ultimately have "iso ?L ?R ?f" by (subst iso_iff3) (auto intro: oprod_Well_order r s t)
    9.57 @@ -1057,7 +1057,7 @@
    9.58    assms[unfolded ordIso_def] by auto
    9.59  
    9.60  lemma Field_singleton[simp]: "Field {(z,z)} = {z}"
    9.61 -  by (metis rel.well_order_on_Field well_order_on_singleton)
    9.62 +  by (metis well_order_on_Field well_order_on_singleton)
    9.63  
    9.64  lemma zero_singleton[simp]: "zero {(z,z)} = z"
    9.65    using wo_rel.zero_in_Field[unfolded wo_rel_def, of "{(z, z)}"] well_order_on_singleton[of z]
    9.66 @@ -1077,7 +1077,7 @@
    9.67    then obtain x where "x \<in> Field r" by auto
    9.68    with * have Fr: "Field r = {x}" by auto
    9.69    interpret r: wo_rel r by unfold_locales (rule r)
    9.70 -  from Fr r.well_order_on_domain[OF r] refl_onD[OF r.REFL, of x] have r_def: "r = {(x, x)}" by fast
    9.71 +  from Fr well_order_on_domain[OF r] refl_onD[OF r.REFL, of x] have r_def: "r = {(x, x)}" by fast
    9.72    interpret wo_rel2 r s by unfold_locales (rule r, rule s)
    9.73    have "bij_betw (\<lambda>x. ()) (Field ?L) (Field ?R)"
    9.74      unfolding bij_betw_def Field_oexp by (auto simp: r_def FinFunc_singleton)
    9.75 @@ -1138,7 +1138,7 @@
    9.76    interpret t!: wo_rel t by unfold_locales (rule t)
    9.77    interpret rt!: wo_rel ?R by unfold_locales (rule osum_Well_order[OF r t])
    9.78    from *(3) have "ofilter ?R (?f ` Field ?L)"
    9.79 -    unfolding t.ofilter_def rt.ofilter_def Field_osum image_Un image_image rel.under_def
    9.80 +    unfolding t.ofilter_def rt.ofilter_def Field_osum image_Un image_image under_def
    9.81      by (auto simp: osum_def intro!: imageI) (auto simp: Field_def)
    9.82    ultimately have "embed ?L ?R ?f" using embed_iff_compat_inj_on_ofilter[of ?L ?R ?f]
    9.83      by (auto intro: osum_Well_order r s t)
    9.84 @@ -1157,7 +1157,7 @@
    9.85    let ?f = "sum_map f id"
    9.86    from f have "\<forall>a\<in>Field (r +o t).
    9.87       ?f a \<in> Field (s +o t) \<and> ?f ` underS (r +o t) a \<subseteq> underS (s +o t) (?f a)"
    9.88 -     unfolding Field_osum rel.underS_def by (fastforce simp: osum_def)
    9.89 +     unfolding Field_osum underS_def by (fastforce simp: osum_def)
    9.90    thus ?thesis unfolding ordLeq_def2 by (auto intro: osum_Well_order r s t)
    9.91  qed
    9.92  
    9.93 @@ -1199,13 +1199,13 @@
    9.94    from *(1) have "inj_on ?f (Field ?L)" unfolding Field_oprod inj_on_def by fastforce
    9.95    moreover
    9.96    from *(2,4) the_inv_into_f_f[OF *(1)] have "compat ?L ?R ?f" unfolding compat_def oprod_def
    9.97 -    by auto (metis rel.well_order_on_domain t, metis rel.well_order_on_domain s)
    9.98 +    by auto (metis well_order_on_domain t, metis well_order_on_domain s)
    9.99    moreover
   9.100    interpret t!: wo_rel t by unfold_locales (rule t)
   9.101    interpret rt!: wo_rel ?R by unfold_locales (rule oprod_Well_order[OF r t])
   9.102    from *(3) have "ofilter ?R (?f ` Field ?L)"
   9.103 -    unfolding t.ofilter_def rt.ofilter_def Field_oprod rel.under_def
   9.104 -    by (auto simp: oprod_def image_iff) (fast | metis r rel.well_order_on_domain)+
   9.105 +    unfolding t.ofilter_def rt.ofilter_def Field_oprod under_def
   9.106 +    by (auto simp: oprod_def image_iff) (fast | metis r well_order_on_domain)+
   9.107    ultimately have "embed ?L ?R ?f" using embed_iff_compat_inj_on_ofilter[of ?L ?R ?f]
   9.108      by (auto intro: oprod_Well_order r s t)
   9.109    moreover
   9.110 @@ -1226,7 +1226,7 @@
   9.111    let ?f = "map_pair f id"
   9.112    from f have "\<forall>a\<in>Field (r *o t).
   9.113       ?f a \<in> Field (s *o t) \<and> ?f ` underS (r *o t) a \<subseteq> underS (s *o t) (?f a)"
   9.114 -     unfolding Field_oprod rel.underS_def unfolding map_pair_def oprod_def by auto
   9.115 +     unfolding Field_oprod underS_def unfolding map_pair_def oprod_def by auto
   9.116    thus ?thesis unfolding ordLeq_def2 by (auto intro: oprod_Well_order r s t)
   9.117  qed
   9.118  
   9.119 @@ -1269,7 +1269,7 @@
   9.120  
   9.121  lemma ozero_oexp: "\<not> (s =o ozero) \<Longrightarrow> ozero ^o s =o ozero"
   9.122    unfolding oexp_def[OF ozero_Well_order s] FinFunc_def
   9.123 -  by simp (metis Func_emp2 bot.extremum_uniqueI emptyE rel.well_order_on_domain s subrelI)
   9.124 +  by simp (metis Func_emp2 bot.extremum_uniqueI emptyE well_order_on_domain s subrelI)
   9.125        
   9.126  lemma oone_oexp: "oone ^o s =o oone" (is "?L =o ?R")
   9.127    by (rule oone_ordIso_oexp[OF ordIso_reflexive[OF oone_Well_order] s])
   9.128 @@ -1326,7 +1326,7 @@
   9.129    qed
   9.130    moreover
   9.131    from FLR have "ofilter ?R (F ` Field ?L)"
   9.132 -  unfolding rexpt.ofilter_def rel.under_def rs.Field_oexp rt.Field_oexp unfolding rt.oexp_def
   9.133 +  unfolding rexpt.ofilter_def under_def rs.Field_oexp rt.Field_oexp unfolding rt.oexp_def
   9.134    proof (safe elim!: imageI)
   9.135      fix g h assume gh: "g \<in> FinFunc r s" "h \<in> FinFunc r t" "F g \<in> FinFunc r t"
   9.136        "let m = t.max_fun_diff h (F g) in (h m, F g m) \<in> r"
   9.137 @@ -1348,7 +1348,7 @@
   9.138            assume "(t.max_fun_diff h (F g), z) \<notin> t"
   9.139            hence "(z, t.max_fun_diff h (F g)) \<in> t" using t.in_notinI[of "t.max_fun_diff h (F g)" z]
   9.140              z max_Field by auto
   9.141 -          hence "z \<in> f ` Field s" using *(3) max_f_Field unfolding t.ofilter_def rel.under_def
   9.142 +          hence "z \<in> f ` Field s" using *(3) max_f_Field unfolding t.ofilter_def under_def
   9.143              by fastforce
   9.144            with z show False by blast
   9.145          qed
   9.146 @@ -1356,9 +1356,9 @@
   9.147            z max_f_Field unfolding F_def by auto
   9.148        } note ** = this
   9.149        with *(3) gh(2) have "h = F (\<lambda>x. if x \<in> Field s then h (f x) else undefined)" using invff
   9.150 -        unfolding F_def fun_eq_iff FinFunc_def Func_def Let_def t.ofilter_def rel.under_def by auto
   9.151 +        unfolding F_def fun_eq_iff FinFunc_def Func_def Let_def t.ofilter_def under_def by auto
   9.152        moreover from gh(2) *(1,3) have "(\<lambda>x. if x \<in> Field s then h (f x) else undefined) \<in> FinFunc r s"
   9.153 -        unfolding FinFunc_def Func_def fin_support_def support_def t.ofilter_def rel.under_def
   9.154 +        unfolding FinFunc_def Func_def fin_support_def support_def t.ofilter_def under_def
   9.155          by (auto intro: subset_inj_on elim!: finite_imageD[OF finite_subset[rotated]])
   9.156        ultimately show "?thesis" by (rule image_eqI)
   9.157      qed simp
   9.158 @@ -1396,7 +1396,7 @@
   9.159    interpret t!: wo_rel t by unfold_locales (rule t)
   9.160    show ?thesis
   9.161    proof (cases "t = {}")
   9.162 -    case True thus ?thesis using r s unfolding ordLeq_def2 rel.underS_def by auto
   9.163 +    case True thus ?thesis using r s unfolding ordLeq_def2 underS_def by auto
   9.164    next
   9.165      case False thus ?thesis
   9.166      proof (cases "r = {}")
   9.167 @@ -1408,9 +1408,9 @@
   9.168        hence f_underS: "\<forall>a\<in>Field r. f a \<in> Field s \<and> f ` underS r a \<subseteq> underS s (f a)"
   9.169          using embed_in_Field[OF rt.rWELL f] embed_underS2[OF rt.rWELL st.rWELL f] by auto
   9.170        from f `t \<noteq> {}` False have *: "Field r \<noteq> {}" "Field s \<noteq> {}" "Field t \<noteq> {}"
   9.171 -        unfolding Field_def embed_def rel.under_def bij_betw_def by auto
   9.172 +        unfolding Field_def embed_def under_def bij_betw_def by auto
   9.173        with f obtain x where "s.zero = f x" "x \<in> Field r" unfolding embed_def bij_betw_def
   9.174 -        using embed_in_Field[OF r.WELL f] s.zero_under set_mp[OF r.under_Field] by blast
   9.175 +        using embed_in_Field[OF r.WELL f] s.zero_under set_mp[OF under_Field[of r]] by blast
   9.176        with f have fz: "f r.zero = s.zero" and inj: "inj_on f (Field r)" and compat: "compat r s f"
   9.177          unfolding embed_iff_compat_inj_on_ofilter[OF r s] compat_def
   9.178          by (fastforce intro: s.leq_zero_imp)+
   9.179 @@ -1424,11 +1424,11 @@
   9.180          proof safe
   9.181            fix h
   9.182            assume h_underS: "h \<in> underS (r ^o t) g"
   9.183 -          hence "h \<in> Field (r ^o t)" unfolding rel.underS_def Field_def by auto
   9.184 +          hence "h \<in> Field (r ^o t)" unfolding underS_def Field_def by auto
   9.185            with fz f_underS have Field_fh: "?f h \<in> Field (s ^o t)"
   9.186              unfolding st.Field_oexp rt.Field_oexp FinFunc_def Func_def fin_support_def support_def
   9.187              by (auto elim!: finite_subset[rotated])
   9.188 -          from h_underS have "h \<noteq> g" and hg: "(h, g) \<in> rt.oexp" unfolding rel.underS_def by auto
   9.189 +          from h_underS have "h \<noteq> g" and hg: "(h, g) \<in> rt.oexp" unfolding underS_def by auto
   9.190            with f inj have neq: "?f h \<noteq> ?f g"
   9.191              unfolding fun_eq_iff inj_on_def rt.oexp_def Option.map_def FinFunc_def Func_def Let_def
   9.192              by simp metis
   9.193 @@ -1440,7 +1440,7 @@
   9.194            with Field_fg Field_fh hg fz f_underS compat neq have "(?f h, ?f g) \<in> st.oexp"
   9.195               using rt.max_fun_diff[OF `h \<noteq> g`] rt.max_fun_diff_in[OF `h \<noteq> g`] unfolding st.Field_oexp
   9.196               unfolding rt.oexp_def st.oexp_def Let_def compat_def by auto
   9.197 -          ultimately show "?f h \<in> underS (s ^o t) (?f g)" unfolding rel.underS_def by auto
   9.198 +          ultimately show "?f h \<in> underS (s ^o t) (?f g)" unfolding underS_def by auto
   9.199          qed
   9.200          ultimately have "?f g \<in> Field (s ^o t) \<and> ?f ` underS (r ^o t) g \<subseteq> underS (s ^o t) (?f g)"
   9.201            by blast
   9.202 @@ -1457,11 +1457,11 @@
   9.203    interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
   9.204    interpret r!: wo_rel r by unfold_locales (rule r)
   9.205    interpret s!: wo_rel s by unfold_locales (rule s)
   9.206 -  from assms rel.well_order_on_domain[OF r] obtain x where
   9.207 +  from assms well_order_on_domain[OF r] obtain x where
   9.208      x: "x \<in> Field r" "r.zero \<in> Field r" "x \<noteq> r.zero"
   9.209 -    unfolding ordLess_def oone_def embedS_def[abs_def] bij_betw_def embed_def rel.under_def
   9.210 +    unfolding ordLess_def oone_def embedS_def[abs_def] bij_betw_def embed_def under_def
   9.211      by (auto simp: image_def)
   9.212 -      (metis equals0D insert_not_empty r.under_def r.zero_in_Field rel.under_empty)
   9.213 +       (metis (lifting) equals0D mem_Collect_eq r.zero_in_Field singletonI)
   9.214    let ?f = "\<lambda>a b. if b \<in> Field s then if b = a then x else r.zero else undefined"
   9.215    from x(3) have SUPP: "\<And>y. y \<in> Field s \<Longrightarrow> rs.SUPP (?f y) = {y}" unfolding support_def by auto
   9.216    { fix y assume y: "y \<in> Field s"
   9.217 @@ -1472,7 +1472,7 @@
   9.218      proof safe
   9.219        fix z
   9.220        assume "z \<in> underS s y"
   9.221 -      hence z: "z \<noteq> y" "(z, y) \<in> s" "z \<in> Field s" unfolding rel.underS_def Field_def by auto
   9.222 +      hence z: "z \<noteq> y" "(z, y) \<in> s" "z \<in> Field s" unfolding underS_def Field_def by auto
   9.223        from x(3) y z(1,3) have "?f z \<noteq> ?f y" unfolding fun_eq_iff by auto
   9.224        moreover
   9.225        { from x(1,2) have "?f z \<in> FinFunc r s" "?f y \<in> FinFunc r s"
   9.226 @@ -1484,7 +1484,7 @@
   9.227          ultimately have "(?f z, ?f y) \<in> rs.oexp" using y x(1)
   9.228            unfolding rs.oexp_def Let_def by auto
   9.229        }
   9.230 -      ultimately show "?f z \<in> underS (r ^o s) (?f y)" unfolding rel.underS_def by blast
   9.231 +      ultimately show "?f z \<in> underS (r ^o s) (?f y)" unfolding underS_def by blast
   9.232      qed
   9.233      ultimately have "?f y \<in> Field (r ^o s) \<and> ?f ` underS s y \<subseteq> underS (r ^o s) (?f y)" by blast
   9.234    }
    10.1 --- a/src/HOL/Cardinals/Wellfounded_More_FP.thy	Thu Jan 16 18:52:50 2014 +0100
    10.2 +++ b/src/HOL/Cardinals/Wellfounded_More_FP.thy	Thu Jan 16 20:52:54 2014 +0100
    10.3 @@ -151,7 +151,7 @@
    10.4    moreover
    10.5    {fix A assume *: "A \<le> Field r" and **: "A \<noteq> {}"
    10.6     obtain a where 1: "r = {} \<or> r = {(a,a)}" using LI
    10.7 -   unfolding order_on_defs using Case1 rel.Total_subset_Id by auto
    10.8 +   unfolding order_on_defs using Case1 Total_subset_Id by auto
    10.9     hence "A = {a} \<and> r = {(a,a)}" using * ** unfolding Field_def by blast
   10.10     hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" using 1 by blast
   10.11    }
   10.12 @@ -169,7 +169,7 @@
   10.13        hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id"
   10.14        using 1 * unfolding wf_eq_minimal2 by simp
   10.15        moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. ((a,a') \<in> r) = ((a',a) \<notin> r - Id)"
   10.16 -      using rel.Linear_order_in_diff_Id[of r] ** LI by blast
   10.17 +      using Linear_order_in_diff_Id[of r] ** LI by blast
   10.18        ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" by blast
   10.19      qed
   10.20    next
   10.21 @@ -180,7 +180,7 @@
   10.22        hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r"
   10.23        using 1 * by simp
   10.24        moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. ((a,a') \<in> r) = ((a',a) \<notin> r - Id)"
   10.25 -      using rel.Linear_order_in_diff_Id[of r] ** LI mono_Field[of "r - Id" r] by blast
   10.26 +      using Linear_order_in_diff_Id[of r] ** LI mono_Field[of "r - Id" r] by blast
   10.27        ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id" by blast
   10.28      qed
   10.29    qed
    11.1 --- a/src/HOL/Cardinals/Wellorder_Embedding.thy	Thu Jan 16 18:52:50 2014 +0100
    11.2 +++ b/src/HOL/Cardinals/Wellorder_Embedding.thy	Thu Jan 16 20:52:54 2014 +0100
    11.3 @@ -41,7 +41,7 @@
    11.4    using EMB unfolding embed_def by simp
    11.5    moreover
    11.6    {have "under r a \<le> Field r"
    11.7 -   by (auto simp add: rel.under_Field)
    11.8 +   by (auto simp add: under_Field)
    11.9     hence "\<And> b. b \<in> under r a \<Longrightarrow> f b = g b"
   11.10     using EQ by blast
   11.11    }
   11.12 @@ -80,10 +80,10 @@
   11.13  proof-
   11.14    obtain r where "well_order_on A r" by (fastforce simp add: well_order_on)
   11.15    hence 1: "A = Field r \<and> Well_order r"
   11.16 -  using rel.well_order_on_Well_order by auto
   11.17 +  using well_order_on_Well_order by auto
   11.18    obtain r' where 2: "well_order_on A' r'" by (fastforce simp add: well_order_on)
   11.19    hence 2: "A' = Field r' \<and> Well_order r'"
   11.20 -  using rel.well_order_on_Well_order by auto
   11.21 +  using well_order_on_Well_order by auto
   11.22    hence "(\<exists>f. embed r r' f) \<or> (\<exists>g. embed r' r g)"
   11.23    using 1 2 by (auto simp add: wellorders_totally_ordered)
   11.24    moreover
    12.1 --- a/src/HOL/Cardinals/Wellorder_Embedding_FP.thy	Thu Jan 16 18:52:50 2014 +0100
    12.2 +++ b/src/HOL/Cardinals/Wellorder_Embedding_FP.thy	Thu Jan 16 20:52:54 2014 +0100
    12.3 @@ -40,20 +40,20 @@
    12.4  lemma under_underS_bij_betw:
    12.5  assumes WELL: "Well_order r" and WELL': "Well_order r'" and
    12.6          IN: "a \<in> Field r" and IN': "f a \<in> Field r'" and
    12.7 -        BIJ: "bij_betw f (rel.underS r a) (rel.underS r' (f a))"
    12.8 -shows "bij_betw f (rel.under r a) (rel.under r' (f a))"
    12.9 +        BIJ: "bij_betw f (underS r a) (underS r' (f a))"
   12.10 +shows "bij_betw f (under r a) (under r' (f a))"
   12.11  proof-
   12.12 -  have "a \<notin> rel.underS r a \<and> f a \<notin> rel.underS r' (f a)"
   12.13 -  unfolding rel.underS_def by auto
   12.14 +  have "a \<notin> underS r a \<and> f a \<notin> underS r' (f a)"
   12.15 +  unfolding underS_def by auto
   12.16    moreover
   12.17    {have "Refl r \<and> Refl r'" using WELL WELL'
   12.18     by (auto simp add: order_on_defs)
   12.19 -   hence "rel.under r a = rel.underS r a \<union> {a} \<and>
   12.20 -          rel.under r' (f a) = rel.underS r' (f a) \<union> {f a}"
   12.21 -   using IN IN' by(auto simp add: rel.Refl_under_underS)
   12.22 +   hence "under r a = underS r a \<union> {a} \<and>
   12.23 +          under r' (f a) = underS r' (f a) \<union> {f a}"
   12.24 +   using IN IN' by(auto simp add: Refl_under_underS)
   12.25    }
   12.26    ultimately show ?thesis
   12.27 -  using BIJ notIn_Un_bij_betw[of a "rel.underS r a" f "rel.underS r' (f a)"] by auto
   12.28 +  using BIJ notIn_Un_bij_betw[of a "underS r a" f "underS r' (f a)"] by auto
   12.29  qed
   12.30  
   12.31  
   12.32 @@ -75,7 +75,7 @@
   12.33  
   12.34  definition embed :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> bool"
   12.35  where
   12.36 -"embed r r' f \<equiv> \<forall>a \<in> Field r. bij_betw f (rel.under r a) (rel.under r' (f a))"
   12.37 +"embed r r' f \<equiv> \<forall>a \<in> Field r. bij_betw f (under r a) (under r' (f a))"
   12.38  
   12.39  
   12.40  lemmas embed_defs = embed_def embed_def[abs_def]
   12.41 @@ -133,11 +133,11 @@
   12.42    using WELL by (auto simp add: wo_rel_def)
   12.43    hence 1: "Refl r"
   12.44    by (auto simp add: wo_rel.REFL)
   12.45 -  hence "a \<in> rel.under r a" using IN rel.Refl_under_in by fastforce
   12.46 -  hence "f a \<in> rel.under r' (f a)"
   12.47 +  hence "a \<in> under r a" using IN Refl_under_in by fastforce
   12.48 +  hence "f a \<in> under r' (f a)"
   12.49    using EMB IN by (auto simp add: embed_def bij_betw_def)
   12.50    thus ?thesis unfolding Field_def
   12.51 -  by (auto simp: rel.under_def)
   12.52 +  by (auto simp: under_def)
   12.53  qed
   12.54  
   12.55  
   12.56 @@ -147,16 +147,16 @@
   12.57  shows "embed r r'' (f' o f)"
   12.58  proof(unfold embed_def, auto)
   12.59    fix a assume *: "a \<in> Field r"
   12.60 -  hence "bij_betw f (rel.under r a) (rel.under r' (f a))"
   12.61 +  hence "bij_betw f (under r a) (under r' (f a))"
   12.62    using embed_def[of r] EMB by auto
   12.63    moreover
   12.64    {have "f a \<in> Field r'"
   12.65     using EMB WELL * by (auto simp add: embed_in_Field)
   12.66 -   hence "bij_betw f' (rel.under r' (f a)) (rel.under r'' (f' (f a)))"
   12.67 +   hence "bij_betw f' (under r' (f a)) (under r'' (f' (f a)))"
   12.68     using embed_def[of r'] EMB' by auto
   12.69    }
   12.70    ultimately
   12.71 -  show "bij_betw (f' \<circ> f) (rel.under r a) (rel.under r'' (f'(f a)))"
   12.72 +  show "bij_betw (f' \<circ> f) (under r a) (under r'' (f'(f a)))"
   12.73    by(auto simp add: bij_betw_trans)
   12.74  qed
   12.75  
   12.76 @@ -190,14 +190,14 @@
   12.77    show ?thesis  using Well' WELL EMB 0 embed_Field[of r r' f]
   12.78    proof(unfold wo_rel.ofilter_def, auto simp add: image_def)
   12.79      fix a b'
   12.80 -    assume *: "a \<in> A" and **: "b' \<in> rel.under r' (f a)"
   12.81 +    assume *: "a \<in> A" and **: "b' \<in> under r' (f a)"
   12.82      hence "a \<in> Field r" using 0 by auto
   12.83 -    hence "bij_betw f (rel.under r a) (rel.under r' (f a))"
   12.84 +    hence "bij_betw f (under r a) (under r' (f a))"
   12.85      using * EMB by (auto simp add: embed_def)
   12.86 -    hence "f`(rel.under r a) = rel.under r' (f a)"
   12.87 +    hence "f`(under r a) = under r' (f a)"
   12.88      by (simp add: bij_betw_def)
   12.89 -    with ** image_def[of f "rel.under r a"] obtain b where
   12.90 -    1: "b \<in> rel.under r a \<and> b' = f b" by blast
   12.91 +    with ** image_def[of f "under r a"] obtain b where
   12.92 +    1: "b \<in> under r a \<and> b' = f b" by blast
   12.93      hence "b \<in> A" using Well * OF
   12.94      by (auto simp add: wo_rel.ofilter_def)
   12.95      with 1 show "\<exists>b \<in> A. b' = f b" by blast
   12.96 @@ -224,14 +224,14 @@
   12.97    fix a b
   12.98    assume *: "(a,b) \<in> r"
   12.99    hence 1: "b \<in> Field r" using Field_def[of r] by blast
  12.100 -  have "a \<in> rel.under r b"
  12.101 -  using * rel.under_def[of r] by simp
  12.102 -  hence "f a \<in> rel.under r' (f b)"
  12.103 +  have "a \<in> under r b"
  12.104 +  using * under_def[of r] by simp
  12.105 +  hence "f a \<in> under r' (f b)"
  12.106    using EMB embed_def[of r r' f]
  12.107 -        bij_betw_def[of f "rel.under r b" "rel.under r' (f b)"]
  12.108 -        image_def[of f "rel.under r b"] 1 by auto
  12.109 +        bij_betw_def[of f "under r b" "under r' (f b)"]
  12.110 +        image_def[of f "under r b"] 1 by auto
  12.111    thus "(f a, f b) \<in> r'"
  12.112 -  by (auto simp add: rel.under_def)
  12.113 +  by (auto simp add: under_def)
  12.114  qed
  12.115  
  12.116  
  12.117 @@ -252,16 +252,16 @@
  12.118    hence 1: "a \<in> Field r \<and> b \<in> Field r"
  12.119    unfolding Field_def by auto
  12.120    {assume "(a,b) \<in> r"
  12.121 -   hence "a \<in> rel.under r b \<and> b \<in> rel.under r b"
  12.122 -   using Refl by(auto simp add: rel.under_def refl_on_def)
  12.123 +   hence "a \<in> under r b \<and> b \<in> under r b"
  12.124 +   using Refl by(auto simp add: under_def refl_on_def)
  12.125     hence "a = b"
  12.126     using EMB 1 ***
  12.127     by (auto simp add: embed_def bij_betw_def inj_on_def)
  12.128    }
  12.129    moreover
  12.130    {assume "(b,a) \<in> r"
  12.131 -   hence "a \<in> rel.under r a \<and> b \<in> rel.under r a"
  12.132 -   using Refl by(auto simp add: rel.under_def refl_on_def)
  12.133 +   hence "a \<in> under r a \<and> b \<in> under r a"
  12.134 +   using Refl by(auto simp add: under_def refl_on_def)
  12.135     hence "a = b"
  12.136     using EMB 1 ***
  12.137     by (auto simp add: embed_def bij_betw_def inj_on_def)
  12.138 @@ -275,19 +275,19 @@
  12.139  lemma embed_underS:
  12.140  assumes WELL: "Well_order r" and WELL': "Well_order r'" and
  12.141          EMB: "embed r r' f" and IN: "a \<in> Field r"
  12.142 -shows "bij_betw f (rel.underS r a) (rel.underS r' (f a))"
  12.143 +shows "bij_betw f (underS r a) (underS r' (f a))"
  12.144  proof-
  12.145 -  have "bij_betw f (rel.under r a) (rel.under r' (f a))"
  12.146 +  have "bij_betw f (under r a) (under r' (f a))"
  12.147    using assms by (auto simp add: embed_def)
  12.148    moreover
  12.149    {have "f a \<in> Field r'" using assms  embed_Field[of r r' f] by auto
  12.150 -   hence "rel.under r a = rel.underS r a \<union> {a} \<and>
  12.151 -          rel.under r' (f a) = rel.underS r' (f a) \<union> {f a}"
  12.152 -   using assms by (auto simp add: order_on_defs rel.Refl_under_underS)
  12.153 +   hence "under r a = underS r a \<union> {a} \<and>
  12.154 +          under r' (f a) = underS r' (f a) \<union> {f a}"
  12.155 +   using assms by (auto simp add: order_on_defs Refl_under_underS)
  12.156    }
  12.157    moreover
  12.158 -  {have "a \<notin> rel.underS r a \<and> f a \<notin> rel.underS r' (f a)"
  12.159 -   unfolding rel.underS_def by blast
  12.160 +  {have "a \<notin> underS r a \<and> f a \<notin> underS r' (f a)"
  12.161 +   unfolding underS_def by blast
  12.162    }
  12.163    ultimately show ?thesis
  12.164    by (auto simp add: notIn_Un_bij_betw3)
  12.165 @@ -325,20 +325,20 @@
  12.166    unfolding Field_def by auto
  12.167    have "f a \<in> f`(Field r)"
  12.168    using **** by auto
  12.169 -  hence 2: "rel.under r' (f a) \<le> f`(Field r)"
  12.170 +  hence 2: "under r' (f a) \<le> f`(Field r)"
  12.171    using Well' *** wo_rel.ofilter_def[of r' "f`(Field r)"] by fastforce
  12.172    (* Main proof *)
  12.173 -  show "bij_betw f (rel.under r a) (rel.under r' (f a))"
  12.174 +  show "bij_betw f (under r a) (under r' (f a))"
  12.175    proof(unfold bij_betw_def, auto)
  12.176 -    show  "inj_on f (rel.under r a)"
  12.177 -    using * by (metis (no_types) rel.under_Field subset_inj_on)
  12.178 +    show  "inj_on f (under r a)"
  12.179 +    using * by (metis (no_types) under_Field subset_inj_on)
  12.180    next
  12.181 -    fix b assume "b \<in> rel.under r a"
  12.182 -    thus "f b \<in> rel.under r' (f a)"
  12.183 -    unfolding rel.under_def using **
  12.184 +    fix b assume "b \<in> under r a"
  12.185 +    thus "f b \<in> under r' (f a)"
  12.186 +    unfolding under_def using **
  12.187      by (auto simp add: compat_def)
  12.188    next
  12.189 -    fix b' assume *****: "b' \<in> rel.under r' (f a)"
  12.190 +    fix b' assume *****: "b' \<in> under r' (f a)"
  12.191      hence "b' \<in> f`(Field r)"
  12.192      using 2 by auto
  12.193      with Field_def[of r] obtain b where
  12.194 @@ -349,7 +349,7 @@
  12.195         with ** 4 have "(f a, b'): r'"
  12.196         by (auto simp add: compat_def)
  12.197         with ***** Antisym' have "f a = b'"
  12.198 -       by(auto simp add: rel.under_def antisym_def)
  12.199 +       by(auto simp add: under_def antisym_def)
  12.200         with 3 **** 4 * have "a = b"
  12.201         by(auto simp add: inj_on_def)
  12.202        }
  12.203 @@ -361,15 +361,15 @@
  12.204        ultimately
  12.205        show ?thesis using Total **** 3 by (fastforce simp add: total_on_def)
  12.206      qed
  12.207 -    with 4 show  "b' \<in> f`(rel.under r a)"
  12.208 -    unfolding rel.under_def by auto
  12.209 +    with 4 show  "b' \<in> f`(under r a)"
  12.210 +    unfolding under_def by auto
  12.211    qed
  12.212  qed
  12.213  
  12.214  
  12.215  lemma inv_into_ofilter_embed:
  12.216  assumes WELL: "Well_order r" and OF: "wo_rel.ofilter r A" and
  12.217 -        BIJ: "\<forall>b \<in> A. bij_betw f (rel.under r b) (rel.under r' (f b))" and
  12.218 +        BIJ: "\<forall>b \<in> A. bij_betw f (under r b) (under r' (f b))" and
  12.219          IMAGE: "f ` A = Field r'"
  12.220  shows "embed r' r (inv_into A f)"
  12.221  proof-
  12.222 @@ -390,16 +390,16 @@
  12.223      using * ** Well OF by (auto simp add: wo_rel.ofilter_def)
  12.224      moreover
  12.225      {assume "(b1,b2) \<in> r"
  12.226 -     hence "b1 \<in> rel.under r b2 \<and> b2 \<in> rel.under r b2"
  12.227 -     unfolding rel.under_def using 11 Refl
  12.228 +     hence "b1 \<in> under r b2 \<and> b2 \<in> under r b2"
  12.229 +     unfolding under_def using 11 Refl
  12.230       by (auto simp add: refl_on_def)
  12.231       hence "b1 = b2" using BIJ * ** ***
  12.232       by (simp add: bij_betw_def inj_on_def)
  12.233      }
  12.234      moreover
  12.235       {assume "(b2,b1) \<in> r"
  12.236 -     hence "b1 \<in> rel.under r b1 \<and> b2 \<in> rel.under r b1"
  12.237 -     unfolding rel.under_def using 11 Refl
  12.238 +     hence "b1 \<in> under r b1 \<and> b2 \<in> under r b1"
  12.239 +     unfolding under_def using 11 Refl
  12.240       by (auto simp add: refl_on_def)
  12.241       hence "b1 = b2" using BIJ * ** ***
  12.242       by (simp add: bij_betw_def inj_on_def)
  12.243 @@ -411,20 +411,20 @@
  12.244    (*  *)
  12.245    let ?f' = "(inv_into A f)"
  12.246    (*  *)
  12.247 -  have 2: "\<forall>b \<in> A. bij_betw ?f' (rel.under r' (f b)) (rel.under r b)"
  12.248 +  have 2: "\<forall>b \<in> A. bij_betw ?f' (under r' (f b)) (under r b)"
  12.249    proof(clarify)
  12.250      fix b assume *: "b \<in> A"
  12.251 -    hence "rel.under r b \<le> A"
  12.252 +    hence "under r b \<le> A"
  12.253      using Well OF by(auto simp add: wo_rel.ofilter_def)
  12.254      moreover
  12.255 -    have "f ` (rel.under r b) = rel.under r' (f b)"
  12.256 +    have "f ` (under r b) = under r' (f b)"
  12.257      using * BIJ by (auto simp add: bij_betw_def)
  12.258      ultimately
  12.259 -    show "bij_betw ?f' (rel.under r' (f b)) (rel.under r b)"
  12.260 +    show "bij_betw ?f' (under r' (f b)) (under r b)"
  12.261      using 1 by (auto simp add: bij_betw_inv_into_subset)
  12.262    qed
  12.263    (*  *)
  12.264 -  have 3: "\<forall>b' \<in> Field r'. bij_betw ?f' (rel.under r' b') (rel.under r (?f' b'))"
  12.265 +  have 3: "\<forall>b' \<in> Field r'. bij_betw ?f' (under r' b') (under r (?f' b'))"
  12.266    proof(clarify)
  12.267      fix b' assume *: "b' \<in> Field r'"
  12.268      have "b' = f (?f' b')" using * 1
  12.269 @@ -435,7 +435,7 @@
  12.270       with 31 have "?f' b' \<in> A" by auto
  12.271      }
  12.272      ultimately
  12.273 -    show  "bij_betw ?f' (rel.under r' b') (rel.under r (?f' b'))"
  12.274 +    show  "bij_betw ?f' (under r' b') (under r (?f' b'))"
  12.275      using 2 by auto
  12.276    qed
  12.277    (*  *)
  12.278 @@ -445,10 +445,10 @@
  12.279  
  12.280  lemma inv_into_underS_embed:
  12.281  assumes WELL: "Well_order r" and
  12.282 -        BIJ: "\<forall>b \<in> rel.underS r a. bij_betw f (rel.under r b) (rel.under r' (f b))" and
  12.283 +        BIJ: "\<forall>b \<in> underS r a. bij_betw f (under r b) (under r' (f b))" and
  12.284          IN: "a \<in> Field r" and
  12.285 -        IMAGE: "f ` (rel.underS r a) = Field r'"
  12.286 -shows "embed r' r (inv_into (rel.underS r a) f)"
  12.287 +        IMAGE: "f ` (underS r a) = Field r'"
  12.288 +shows "embed r' r (inv_into (underS r a) f)"
  12.289  using assms
  12.290  by(auto simp add: wo_rel_def wo_rel.underS_ofilter inv_into_ofilter_embed)
  12.291  
  12.292 @@ -458,7 +458,7 @@
  12.293          IMAGE: "Field r' \<le> f ` (Field r)"
  12.294  shows "embed r' r (inv_into (Field r) f)"
  12.295  proof-
  12.296 -  have "(\<forall>b \<in> Field r. bij_betw f (rel.under r b) (rel.under r' (f b)))"
  12.297 +  have "(\<forall>b \<in> Field r. bij_betw f (under r b) (under r' (f b)))"
  12.298    using EMB by (auto simp add: embed_def)
  12.299    moreover
  12.300    have "f ` (Field r) \<le> Field r'"
  12.301 @@ -511,101 +511,101 @@
  12.302  fixes r ::"'a rel"  and r'::"'a' rel" and
  12.303        f :: "'a \<Rightarrow> 'a'" and a::'a
  12.304  assumes WELL: "Well_order r" and WELL': "Well_order r'" and IN: "a \<in> Field r" and
  12.305 -        IH: "\<forall>b \<in> rel.underS r a. bij_betw f (rel.under r b) (rel.under r' (f b))" and
  12.306 -        NOT: "f ` (rel.underS r a) \<noteq> Field r'" and SUC: "f a = wo_rel.suc r' (f`(rel.underS r a))"
  12.307 -shows "bij_betw f (rel.under r a) (rel.under r' (f a))"
  12.308 +        IH: "\<forall>b \<in> underS r a. bij_betw f (under r b) (under r' (f b))" and
  12.309 +        NOT: "f ` (underS r a) \<noteq> Field r'" and SUC: "f a = wo_rel.suc r' (f`(underS r a))"
  12.310 +shows "bij_betw f (under r a) (under r' (f a))"
  12.311  proof-
  12.312    (* Preliminary facts *)
  12.313    have Well: "wo_rel r" using WELL unfolding wo_rel_def .
  12.314    hence Refl: "Refl r" using wo_rel.REFL[of r] by auto
  12.315    have Trans: "trans r" using Well wo_rel.TRANS[of r] by auto
  12.316    have Well': "wo_rel r'" using WELL' unfolding wo_rel_def .
  12.317 -  have OF: "wo_rel.ofilter r (rel.underS r a)"
  12.318 +  have OF: "wo_rel.ofilter r (underS r a)"
  12.319    by (auto simp add: Well wo_rel.underS_ofilter)
  12.320 -  hence UN: "rel.underS r a = (\<Union>  b \<in> rel.underS r a. rel.under r b)"
  12.321 -  using Well wo_rel.ofilter_under_UNION[of r "rel.underS r a"] by blast
  12.322 -  (* Gather facts about elements of rel.underS r a *)
  12.323 -  {fix b assume *: "b \<in> rel.underS r a"
  12.324 -   hence t0: "(b,a) \<in> r \<and> b \<noteq> a" unfolding rel.underS_def by auto
  12.325 +  hence UN: "underS r a = (\<Union>  b \<in> underS r a. under r b)"
  12.326 +  using Well wo_rel.ofilter_under_UNION[of r "underS r a"] by blast
  12.327 +  (* Gather facts about elements of underS r a *)
  12.328 +  {fix b assume *: "b \<in> underS r a"
  12.329 +   hence t0: "(b,a) \<in> r \<and> b \<noteq> a" unfolding underS_def by auto
  12.330     have t1: "b \<in> Field r"
  12.331 -   using * rel.underS_Field[of r a] by auto
  12.332 -   have t2: "f`(rel.under r b) = rel.under r' (f b)"
  12.333 +   using * underS_Field[of r a] by auto
  12.334 +   have t2: "f`(under r b) = under r' (f b)"
  12.335     using IH * by (auto simp add: bij_betw_def)
  12.336 -   hence t3: "wo_rel.ofilter r' (f`(rel.under r b))"
  12.337 +   hence t3: "wo_rel.ofilter r' (f`(under r b))"
  12.338     using Well' by (auto simp add: wo_rel.under_ofilter)
  12.339 -   have "f`(rel.under r b) \<le> Field r'"
  12.340 -   using t2 by (auto simp add: rel.under_Field)
  12.341 +   have "f`(under r b) \<le> Field r'"
  12.342 +   using t2 by (auto simp add: under_Field)
  12.343     moreover
  12.344 -   have "b \<in> rel.under r b"
  12.345 -   using t1 by(auto simp add: Refl rel.Refl_under_in)
  12.346 +   have "b \<in> under r b"
  12.347 +   using t1 by(auto simp add: Refl Refl_under_in)
  12.348     ultimately
  12.349     have t4:  "f b \<in> Field r'" by auto
  12.350 -   have "f`(rel.under r b) = rel.under r' (f b) \<and>
  12.351 -         wo_rel.ofilter r' (f`(rel.under r b)) \<and>
  12.352 +   have "f`(under r b) = under r' (f b) \<and>
  12.353 +         wo_rel.ofilter r' (f`(under r b)) \<and>
  12.354           f b \<in> Field r'"
  12.355     using t2 t3 t4 by auto
  12.356    }
  12.357    hence bFact:
  12.358 -  "\<forall>b \<in> rel.underS r a. f`(rel.under r b) = rel.under r' (f b) \<and>
  12.359 -                       wo_rel.ofilter r' (f`(rel.under r b)) \<and>
  12.360 +  "\<forall>b \<in> underS r a. f`(under r b) = under r' (f b) \<and>
  12.361 +                       wo_rel.ofilter r' (f`(under r b)) \<and>
  12.362                         f b \<in> Field r'" by blast
  12.363    (*  *)
  12.364 -  have subField: "f`(rel.underS r a) \<le> Field r'"
  12.365 +  have subField: "f`(underS r a) \<le> Field r'"
  12.366    using bFact by blast
  12.367    (*  *)
  12.368 -  have OF': "wo_rel.ofilter r' (f`(rel.underS r a))"
  12.369 +  have OF': "wo_rel.ofilter r' (f`(underS r a))"
  12.370    proof-
  12.371 -    have "f`(rel.underS r a) = f`(\<Union>  b \<in> rel.underS r a. rel.under r b)"
  12.372 +    have "f`(underS r a) = f`(\<Union>  b \<in> underS r a. under r b)"
  12.373      using UN by auto
  12.374 -    also have "\<dots> = (\<Union>  b \<in> rel.underS r a. f`(rel.under r b))" by blast
  12.375 -    also have "\<dots> = (\<Union>  b \<in> rel.underS r a. (rel.under r' (f b)))"
  12.376 +    also have "\<dots> = (\<Union>  b \<in> underS r a. f`(under r b))" by blast
  12.377 +    also have "\<dots> = (\<Union>  b \<in> underS r a. (under r' (f b)))"
  12.378      using bFact by auto
  12.379      finally
  12.380 -    have "f`(rel.underS r a) = (\<Union>  b \<in> rel.underS r a. (rel.under r' (f b)))" .
  12.381 +    have "f`(underS r a) = (\<Union>  b \<in> underS r a. (under r' (f b)))" .
  12.382      thus ?thesis
  12.383      using Well' bFact
  12.384 -          wo_rel.ofilter_UNION[of r' "rel.underS r a" "\<lambda> b. rel.under r' (f b)"] by fastforce
  12.385 +          wo_rel.ofilter_UNION[of r' "underS r a" "\<lambda> b. under r' (f b)"] by fastforce
  12.386    qed
  12.387    (*  *)
  12.388 -  have "f`(rel.underS r a) \<union> rel.AboveS r' (f`(rel.underS r a)) = Field r'"
  12.389 +  have "f`(underS r a) \<union> AboveS r' (f`(underS r a)) = Field r'"
  12.390    using Well' OF' by (auto simp add: wo_rel.ofilter_AboveS_Field)
  12.391 -  hence NE: "rel.AboveS r' (f`(rel.underS r a)) \<noteq> {}"
  12.392 +  hence NE: "AboveS r' (f`(underS r a)) \<noteq> {}"
  12.393    using subField NOT by blast
  12.394    (* Main proof *)
  12.395 -  have INCL1: "f`(rel.underS r a) \<le> rel.underS r' (f a) "
  12.396 +  have INCL1: "f`(underS r a) \<le> underS r' (f a) "
  12.397    proof(auto)
  12.398 -    fix b assume *: "b \<in> rel.underS r a"
  12.399 +    fix b assume *: "b \<in> underS r a"
  12.400      have "f b \<noteq> f a \<and> (f b, f a) \<in> r'"
  12.401      using subField Well' SUC NE *
  12.402 -          wo_rel.suc_greater[of r' "f`(rel.underS r a)" "f b"] by force
  12.403 -    thus "f b \<in> rel.underS r' (f a)"
  12.404 -    unfolding rel.underS_def by simp
  12.405 +          wo_rel.suc_greater[of r' "f`(underS r a)" "f b"] by force
  12.406 +    thus "f b \<in> underS r' (f a)"
  12.407 +    unfolding underS_def by simp
  12.408    qed
  12.409    (*  *)
  12.410 -  have INCL2: "rel.underS r' (f a) \<le> f`(rel.underS r a)"
  12.411 +  have INCL2: "underS r' (f a) \<le> f`(underS r a)"
  12.412    proof
  12.413 -    fix b' assume "b' \<in> rel.underS r' (f a)"
  12.414 +    fix b' assume "b' \<in> underS r' (f a)"
  12.415      hence "b' \<noteq> f a \<and> (b', f a) \<in> r'"
  12.416 -    unfolding rel.underS_def by simp
  12.417 -    thus "b' \<in> f`(rel.underS r a)"
  12.418 +    unfolding underS_def by simp
  12.419 +    thus "b' \<in> f`(underS r a)"
  12.420      using Well' SUC NE OF'
  12.421 -          wo_rel.suc_ofilter_in[of r' "f ` rel.underS r a" b'] by auto
  12.422 +          wo_rel.suc_ofilter_in[of r' "f ` underS r a" b'] by auto
  12.423    qed
  12.424    (*  *)
  12.425 -  have INJ: "inj_on f (rel.underS r a)"
  12.426 +  have INJ: "inj_on f (underS r a)"
  12.427    proof-
  12.428 -    have "\<forall>b \<in> rel.underS r a. inj_on f (rel.under r b)"
  12.429 +    have "\<forall>b \<in> underS r a. inj_on f (under r b)"
  12.430      using IH by (auto simp add: bij_betw_def)
  12.431      moreover
  12.432 -    have "\<forall>b. wo_rel.ofilter r (rel.under r b)"
  12.433 +    have "\<forall>b. wo_rel.ofilter r (under r b)"
  12.434      using Well by (auto simp add: wo_rel.under_ofilter)
  12.435      ultimately show  ?thesis
  12.436      using WELL bFact UN
  12.437 -          UNION_inj_on_ofilter[of r "rel.underS r a" "\<lambda>b. rel.under r b" f]
  12.438 +          UNION_inj_on_ofilter[of r "underS r a" "\<lambda>b. under r b" f]
  12.439      by auto
  12.440    qed
  12.441    (*  *)
  12.442 -  have BIJ: "bij_betw f (rel.underS r a) (rel.underS r' (f a))"
  12.443 +  have BIJ: "bij_betw f (underS r a) (underS r' (f a))"
  12.444    unfolding bij_betw_def
  12.445    using INJ INCL1 INCL2 by auto
  12.446    (*  *)
  12.447 @@ -622,14 +622,14 @@
  12.448        f :: "'a \<Rightarrow> 'a'" and g :: "'a \<Rightarrow> bool"  and a::'a
  12.449  assumes WELL: "Well_order r" and WELL': "Well_order r'" and
  12.450  MAIN1:
  12.451 -  "\<And> a. (False \<notin> g`(rel.underS r a) \<and> f`(rel.underS r a) \<noteq> Field r'
  12.452 -          \<longrightarrow> f a = wo_rel.suc r' (f`(rel.underS r a)) \<and> g a = True)
  12.453 +  "\<And> a. (False \<notin> g`(underS r a) \<and> f`(underS r a) \<noteq> Field r'
  12.454 +          \<longrightarrow> f a = wo_rel.suc r' (f`(underS r a)) \<and> g a = True)
  12.455           \<and>
  12.456 -         (\<not>(False \<notin> (g`(rel.underS r a)) \<and> f`(rel.underS r a) \<noteq> Field r')
  12.457 +         (\<not>(False \<notin> (g`(underS r a)) \<and> f`(underS r a) \<noteq> Field r')
  12.458            \<longrightarrow> g a = False)" and
  12.459 -MAIN2: "\<And> a. a \<in> Field r \<and> False \<notin> g`(rel.under r a) \<longrightarrow>
  12.460 -              bij_betw f (rel.under r a) (rel.under r' (f a))" and
  12.461 -Case: "a \<in> Field r \<and> False \<in> g`(rel.under r a)"
  12.462 +MAIN2: "\<And> a. a \<in> Field r \<and> False \<notin> g`(under r a) \<longrightarrow>
  12.463 +              bij_betw f (under r a) (under r' (f a))" and
  12.464 +Case: "a \<in> Field r \<and> False \<in> g`(under r a)"
  12.465  shows "\<exists>f'. embed r' r f'"
  12.466  proof-
  12.467    have Well: "wo_rel r" using WELL unfolding wo_rel_def .
  12.468 @@ -638,13 +638,13 @@
  12.469    have Antisym: "antisym r" using Well wo_rel.ANTISYM[of r] by auto
  12.470    have Well': "wo_rel r'" using WELL' unfolding wo_rel_def .
  12.471    (*  *)
  12.472 -  have 0: "rel.under r a = rel.underS r a \<union> {a}"
  12.473 -  using Refl Case by(auto simp add: rel.Refl_under_underS)
  12.474 +  have 0: "under r a = underS r a \<union> {a}"
  12.475 +  using Refl Case by(auto simp add: Refl_under_underS)
  12.476    (*  *)
  12.477    have 1: "g a = False"
  12.478    proof-
  12.479      {assume "g a \<noteq> False"
  12.480 -     with 0 Case have "False \<in> g`(rel.underS r a)" by blast
  12.481 +     with 0 Case have "False \<in> g`(underS r a)" by blast
  12.482       with MAIN1 have "g a = False" by blast}
  12.483      thus ?thesis by blast
  12.484    qed
  12.485 @@ -653,12 +653,12 @@
  12.486    (*  *)
  12.487    have 2: "?A \<noteq> {} \<and> ?A \<le> Field r" using Case 1 by blast
  12.488    (*  *)
  12.489 -  have 3: "False \<notin> g`(rel.underS r ?a)"
  12.490 +  have 3: "False \<notin> g`(underS r ?a)"
  12.491    proof
  12.492 -    assume "False \<in> g`(rel.underS r ?a)"
  12.493 -    then obtain b where "b \<in> rel.underS r ?a" and 31: "g b = False" by auto
  12.494 +    assume "False \<in> g`(underS r ?a)"
  12.495 +    then obtain b where "b \<in> underS r ?a" and 31: "g b = False" by auto
  12.496      hence 32: "(b,?a) \<in> r \<and> b \<noteq> ?a"
  12.497 -    by (auto simp add: rel.underS_def)
  12.498 +    by (auto simp add: underS_def)
  12.499      hence "b \<in> Field r" unfolding Field_def by auto
  12.500      with 31 have "b \<in> ?A" by auto
  12.501      hence "(?a,b) \<in> r" using wo_rel.minim_least 2 Well by fastforce
  12.502 @@ -672,25 +672,25 @@
  12.503    (*   *)
  12.504    have 5: "g ?a = False" using temp by blast
  12.505    (*  *)
  12.506 -  have 6: "f`(rel.underS r ?a) = Field r'"
  12.507 +  have 6: "f`(underS r ?a) = Field r'"
  12.508    using MAIN1[of ?a] 3 5 by blast
  12.509    (*  *)
  12.510 -  have 7: "\<forall>b \<in> rel.underS r ?a. bij_betw f (rel.under r b) (rel.under r' (f b))"
  12.511 +  have 7: "\<forall>b \<in> underS r ?a. bij_betw f (under r b) (under r' (f b))"
  12.512    proof
  12.513 -    fix b assume as: "b \<in> rel.underS r ?a"
  12.514 +    fix b assume as: "b \<in> underS r ?a"
  12.515      moreover
  12.516 -    have "wo_rel.ofilter r (rel.underS r ?a)"
  12.517 +    have "wo_rel.ofilter r (underS r ?a)"
  12.518      using Well by (auto simp add: wo_rel.underS_ofilter)
  12.519      ultimately
  12.520 -    have "False \<notin> g`(rel.under r b)" using 3 Well by (subst (asm) wo_rel.ofilter_def) fast+
  12.521 +    have "False \<notin> g`(under r b)" using 3 Well by (subst (asm) wo_rel.ofilter_def) fast+
  12.522      moreover have "b \<in> Field r"
  12.523 -    unfolding Field_def using as by (auto simp add: rel.underS_def)
  12.524 +    unfolding Field_def using as by (auto simp add: underS_def)
  12.525      ultimately
  12.526 -    show "bij_betw f (rel.under r b) (rel.under r' (f b))"
  12.527 +    show "bij_betw f (under r b) (under r' (f b))"
  12.528      using MAIN2 by auto
  12.529    qed
  12.530    (*  *)
  12.531 -  have "embed r' r (inv_into (rel.underS r ?a) f)"
  12.532 +  have "embed r' r (inv_into (underS r ?a) f)"
  12.533    using WELL WELL' 7 4 6 inv_into_underS_embed[of r ?a f r'] by auto
  12.534    thus ?thesis
  12.535    unfolding embed_def by blast
  12.536 @@ -709,18 +709,18 @@
  12.537    have Well': "wo_rel r'" using WELL' unfolding wo_rel_def .
  12.538    (* Main proof *)
  12.539    obtain H where H_def: "H =
  12.540 -  (\<lambda>h a. if False \<notin> (snd o h)`(rel.underS r a) \<and> (fst o h)`(rel.underS r a) \<noteq> Field r'
  12.541 -                then (wo_rel.suc r' ((fst o h)`(rel.underS r a)), True)
  12.542 +  (\<lambda>h a. if False \<notin> (snd o h)`(underS r a) \<and> (fst o h)`(underS r a) \<noteq> Field r'
  12.543 +                then (wo_rel.suc r' ((fst o h)`(underS r a)), True)
  12.544                  else (undefined, False))" by blast
  12.545    have Adm: "wo_rel.adm_wo r H"
  12.546    using Well
  12.547    proof(unfold wo_rel.adm_wo_def, clarify)
  12.548      fix h1::"'a \<Rightarrow> 'a' * bool" and h2::"'a \<Rightarrow> 'a' * bool" and x
  12.549 -    assume "\<forall>y\<in>rel.underS r x. h1 y = h2 y"
  12.550 -    hence "\<forall>y\<in>rel.underS r x. (fst o h1) y = (fst o h2) y \<and>
  12.551 +    assume "\<forall>y\<in>underS r x. h1 y = h2 y"
  12.552 +    hence "\<forall>y\<in>underS r x. (fst o h1) y = (fst o h2) y \<and>
  12.553                            (snd o h1) y = (snd o h2) y" by auto
  12.554 -    hence "(fst o h1)`(rel.underS r x) = (fst o h2)`(rel.underS r x) \<and>
  12.555 -           (snd o h1)`(rel.underS r x) = (snd o h2)`(rel.underS r x)"
  12.556 +    hence "(fst o h1)`(underS r x) = (fst o h2)`(underS r x) \<and>
  12.557 +           (snd o h1)`(underS r x) = (snd o h2)`(underS r x)"
  12.558        by (auto simp add: image_def)
  12.559      thus "H h1 x = H h2 x" by (simp add: H_def del: not_False_in_image_Ball)
  12.560    qed
  12.561 @@ -729,21 +729,21 @@
  12.562    where h_def: "h = wo_rel.worec r H" and
  12.563          f_def: "f = fst o h" and g_def: "g = snd o h" by blast
  12.564    obtain test where test_def:
  12.565 -  "test = (\<lambda> a. False \<notin> (g`(rel.underS r a)) \<and> f`(rel.underS r a) \<noteq> Field r')" by blast
  12.566 +  "test = (\<lambda> a. False \<notin> (g`(underS r a)) \<and> f`(underS r a) \<noteq> Field r')" by blast
  12.567    (*  *)
  12.568    have *: "\<And> a. h a  = H h a"
  12.569    using Adm Well wo_rel.worec_fixpoint[of r H] by (simp add: h_def)
  12.570    have Main1:
  12.571 -  "\<And> a. (test a \<longrightarrow> f a = wo_rel.suc r' (f`(rel.underS r a)) \<and> g a = True) \<and>
  12.572 +  "\<And> a. (test a \<longrightarrow> f a = wo_rel.suc r' (f`(underS r a)) \<and> g a = True) \<and>
  12.573           (\<not>(test a) \<longrightarrow> g a = False)"
  12.574    proof-  (* How can I prove this withou fixing a? *)
  12.575 -    fix a show "(test a \<longrightarrow> f a = wo_rel.suc r' (f`(rel.underS r a)) \<and> g a = True) \<and>
  12.576 +    fix a show "(test a \<longrightarrow> f a = wo_rel.suc r' (f`(underS r a)) \<and> g a = True) \<and>
  12.577                  (\<not>(test a) \<longrightarrow> g a = False)"
  12.578      using *[of a] test_def f_def g_def H_def by auto
  12.579    qed
  12.580    (*  *)
  12.581 -  let ?phi = "\<lambda> a. a \<in> Field r \<and> False \<notin> g`(rel.under r a) \<longrightarrow>
  12.582 -                   bij_betw f (rel.under r a) (rel.under r' (f a))"
  12.583 +  let ?phi = "\<lambda> a. a \<in> Field r \<and> False \<notin> g`(under r a) \<longrightarrow>
  12.584 +                   bij_betw f (under r a) (under r' (f a))"
  12.585    have Main2: "\<And> a. ?phi a"
  12.586    proof-
  12.587      fix a show "?phi a"
  12.588 @@ -752,46 +752,46 @@
  12.589        fix a
  12.590        assume IH: "\<forall>b. b \<noteq> a \<and> (b,a) \<in> r \<longrightarrow> ?phi b" and
  12.591               *: "a \<in> Field r" and
  12.592 -             **: "False \<notin> g`(rel.under r a)"
  12.593 -      have 1: "\<forall>b \<in> rel.underS r a. bij_betw f (rel.under r b) (rel.under r' (f b))"
  12.594 +             **: "False \<notin> g`(under r a)"
  12.595 +      have 1: "\<forall>b \<in> underS r a. bij_betw f (under r b) (under r' (f b))"
  12.596        proof(clarify)
  12.597 -        fix b assume ***: "b \<in> rel.underS r a"
  12.598 -        hence 0: "(b,a) \<in> r \<and> b \<noteq> a" unfolding rel.underS_def by auto
  12.599 +        fix b assume ***: "b \<in> underS r a"
  12.600 +        hence 0: "(b,a) \<in> r \<and> b \<noteq> a" unfolding underS_def by auto
  12.601          moreover have "b \<in> Field r"
  12.602 -        using *** rel.underS_Field[of r a] by auto
  12.603 -        moreover have "False \<notin> g`(rel.under r b)"
  12.604 -        using 0 ** Trans rel.under_incr[of r b a] by auto
  12.605 -        ultimately show "bij_betw f (rel.under r b) (rel.under r' (f b))"
  12.606 +        using *** underS_Field[of r a] by auto
  12.607 +        moreover have "False \<notin> g`(under r b)"
  12.608 +        using 0 ** Trans under_incr[of r b a] by auto
  12.609 +        ultimately show "bij_betw f (under r b) (under r' (f b))"
  12.610          using IH by auto
  12.611        qed
  12.612        (*  *)
  12.613 -      have 21: "False \<notin> g`(rel.underS r a)"
  12.614 -      using ** rel.underS_subset_under[of r a] by auto
  12.615 -      have 22: "g`(rel.under r a) \<le> {True}" using ** by auto
  12.616 -      moreover have 23: "a \<in> rel.under r a"
  12.617 -      using Refl * by (auto simp add: rel.Refl_under_in)
  12.618 +      have 21: "False \<notin> g`(underS r a)"
  12.619 +      using ** underS_subset_under[of r a] by auto
  12.620 +      have 22: "g`(under r a) \<le> {True}" using ** by auto
  12.621 +      moreover have 23: "a \<in> under r a"
  12.622 +      using Refl * by (auto simp add: Refl_under_in)
  12.623        ultimately have 24: "g a = True" by blast
  12.624 -      have 2: "f`(rel.underS r a) \<noteq> Field r'"
  12.625 +      have 2: "f`(underS r a) \<noteq> Field r'"
  12.626        proof
  12.627 -        assume "f`(rel.underS r a) = Field r'"
  12.628 +        assume "f`(underS r a) = Field r'"
  12.629          hence "g a = False" using Main1 test_def by blast
  12.630          with 24 show False using ** by blast
  12.631        qed
  12.632        (*  *)
  12.633 -      have 3: "f a = wo_rel.suc r' (f`(rel.underS r a))"
  12.634 +      have 3: "f a = wo_rel.suc r' (f`(underS r a))"
  12.635        using 21 2 Main1 test_def by blast
  12.636        (*  *)
  12.637 -      show "bij_betw f (rel.under r a) (rel.under r' (f a))"
  12.638 +      show "bij_betw f (under r a) (under r' (f a))"
  12.639        using WELL  WELL' 1 2 3 *
  12.640              wellorders_totally_ordered_aux[of r r' a f] by auto
  12.641      qed
  12.642    qed
  12.643    (*  *)
  12.644 -  let ?chi = "(\<lambda> a. a \<in> Field r \<and> False \<in> g`(rel.under r a))"
  12.645 +  let ?chi = "(\<lambda> a. a \<in> Field r \<and> False \<in> g`(under r a))"
  12.646    show ?thesis
  12.647    proof(cases "\<exists>a. ?chi a")
  12.648      assume "\<not> (\<exists>a. ?chi a)"
  12.649 -    hence "\<forall>a \<in> Field r.  bij_betw f (rel.under r a) (rel.under r' (f a))"
  12.650 +    hence "\<forall>a \<in> Field r.  bij_betw f (under r a) (under r' (f a))"
  12.651      using Main2 by blast
  12.652      thus ?thesis unfolding embed_def by blast
  12.653    next
  12.654 @@ -817,16 +817,16 @@
  12.655  lemma embed_determined:
  12.656  assumes WELL: "Well_order r" and WELL': "Well_order r'" and
  12.657          EMB: "embed r r' f" and IN: "a \<in> Field r"
  12.658 -shows "f a = wo_rel.suc r' (f`(rel.underS r a))"
  12.659 +shows "f a = wo_rel.suc r' (f`(underS r a))"
  12.660  proof-
  12.661 -  have "bij_betw f (rel.underS r a) (rel.underS r' (f a))"
  12.662 +  have "bij_betw f (underS r a) (underS r' (f a))"
  12.663    using assms by (auto simp add: embed_underS)
  12.664 -  hence "f`(rel.underS r a) = rel.underS r' (f a)"
  12.665 +  hence "f`(underS r a) = underS r' (f a)"
  12.666    by (auto simp add: bij_betw_def)
  12.667    moreover
  12.668    {have "f a \<in> Field r'" using IN
  12.669     using EMB WELL embed_Field[of r r' f] by auto
  12.670 -   hence "f a = wo_rel.suc r' (rel.underS r' (f a))"
  12.671 +   hence "f a = wo_rel.suc r' (underS r' (f a))"
  12.672     using WELL' by (auto simp add: wo_rel_def wo_rel.suc_underS)
  12.673    }
  12.674    ultimately show ?thesis by simp
  12.675 @@ -841,9 +841,9 @@
  12.676    fix a
  12.677    assume IH: "\<forall>b. b \<noteq> a \<and> (b,a): r \<longrightarrow> b \<in> Field r \<longrightarrow> f b = g b" and
  12.678           *: "a \<in> Field r"
  12.679 -  hence "\<forall>b \<in> rel.underS r a. f b = g b"
  12.680 -  unfolding rel.underS_def by (auto simp add: Field_def)
  12.681 -  hence "f`(rel.underS r a) = g`(rel.underS r a)" by force
  12.682 +  hence "\<forall>b \<in> underS r a. f b = g b"
  12.683 +  unfolding underS_def by (auto simp add: Field_def)
  12.684 +  hence "f`(underS r a) = g`(underS r a)" by force
  12.685    thus "f a = g a"
  12.686    using assms * embed_determined[of r r' f a] embed_determined[of r r' g a] by auto
  12.687  qed
  12.688 @@ -1083,28 +1083,28 @@
  12.689  next
  12.690    assume *: "bij_betw f (Field r) (Field r')" and
  12.691           **: "\<forall>a\<in>Field r. \<forall>b\<in>Field r. ((a, b) \<in> r) = ((f a, f b) \<in> r')"
  12.692 -  have 1: "\<And> a. rel.under r a \<le> Field r \<and> rel.under r' (f a) \<le> Field r'"
  12.693 -  by (auto simp add: rel.under_Field)
  12.694 +  have 1: "\<And> a. under r a \<le> Field r \<and> under r' (f a) \<le> Field r'"
  12.695 +  by (auto simp add: under_Field)
  12.696    have 2: "inj_on f (Field r)" using * by (auto simp add: bij_betw_def)
  12.697    {fix a assume ***: "a \<in> Field r"
  12.698 -   have "bij_betw f (rel.under r a) (rel.under r' (f a))"
  12.699 +   have "bij_betw f (under r a) (under r' (f a))"
  12.700     proof(unfold bij_betw_def, auto)
  12.701 -     show "inj_on f (rel.under r a)"
  12.702 +     show "inj_on f (under r a)"
  12.703       using 1 2 by (metis subset_inj_on)
  12.704     next
  12.705 -     fix b assume "b \<in> rel.under r a"
  12.706 +     fix b assume "b \<in> under r a"
  12.707       hence "a \<in> Field r \<and> b \<in> Field r \<and> (b,a) \<in> r"
  12.708 -     unfolding rel.under_def by (auto simp add: Field_def Range_def Domain_def)
  12.709 -     with 1 ** show "f b \<in> rel.under r' (f a)"
  12.710 -     unfolding rel.under_def by auto
  12.711 +     unfolding under_def by (auto simp add: Field_def Range_def Domain_def)
  12.712 +     with 1 ** show "f b \<in> under r' (f a)"
  12.713 +     unfolding under_def by auto
  12.714     next
  12.715 -     fix b' assume "b' \<in> rel.under r' (f a)"
  12.716 -     hence 3: "(b',f a) \<in> r'" unfolding rel.under_def by simp
  12.717 +     fix b' assume "b' \<in> under r' (f a)"
  12.718 +     hence 3: "(b',f a) \<in> r'" unfolding under_def by simp
  12.719       hence "b' \<in> Field r'" unfolding Field_def by auto
  12.720       with * obtain b where "b \<in> Field r \<and> f b = b'"
  12.721       unfolding bij_betw_def by force
  12.722       with 3 ** ***
  12.723 -     show "b' \<in> f ` (rel.under r a)" unfolding rel.under_def by blast
  12.724 +     show "b' \<in> f ` (under r a)" unfolding under_def by blast
  12.725     qed
  12.726    }
  12.727    thus "embed r r' f" unfolding embed_def using * by auto
    13.1 --- a/src/HOL/Cardinals/Wellorder_Extension.thy	Thu Jan 16 18:52:50 2014 +0100
    13.2 +++ b/src/HOL/Cardinals/Wellorder_Extension.thy	Thu Jan 16 20:52:54 2014 +0100
    13.3 @@ -178,7 +178,7 @@
    13.4      where "p \<subseteq> w" and wo: "Well_order w" by blast
    13.5    let ?A = "UNIV - Field w"
    13.6    from well_order_on [of ?A] obtain w' where wo': "well_order_on ?A w'" ..
    13.7 -  have [simp]: "Field w' = ?A" using rel.well_order_on_Well_order [OF wo'] by simp
    13.8 +  have [simp]: "Field w' = ?A" using well_order_on_Well_order [OF wo'] by simp
    13.9    have *: "Field w \<inter> Field w' = {}" by simp
   13.10    let ?w = "w \<union>o w'"
   13.11    have "p \<subseteq> ?w" using `p \<subseteq> w` by (auto simp: Osum_def)
    14.1 --- a/src/HOL/Cardinals/Wellorder_Relation.thy	Thu Jan 16 18:52:50 2014 +0100
    14.2 +++ b/src/HOL/Cardinals/Wellorder_Relation.thy	Thu Jan 16 20:52:54 2014 +0100
    14.3 @@ -37,7 +37,7 @@
    14.4  proof-
    14.5    have "adm_wf (r - Id) H"
    14.6    unfolding adm_wf_def
    14.7 -  using ADM adm_wo_def[of H] underS_def by auto
    14.8 +  using ADM adm_wo_def[of H] underS_def[of r] by auto
    14.9    hence "f = wfrec (r - Id) H"
   14.10    using fp WF wfrec_unique_fixpoint[of "r - Id" H] by simp
   14.11    thus ?thesis unfolding worec_def .
   14.12 @@ -97,7 +97,7 @@
   14.13    have "Under A \<le> under (minim A)"
   14.14    proof
   14.15      fix x assume "x \<in> Under A"
   14.16 -    with 1 Under_def have "(x,minim A) \<in> r" by auto
   14.17 +    with 1 Under_def[of r] have "(x,minim A) \<in> r" by auto
   14.18      thus "x \<in> under(minim A)" unfolding under_def by simp
   14.19    qed
   14.20    (*  *)
   14.21 @@ -133,7 +133,7 @@
   14.22    have "UnderS A \<le> underS (minim A)"
   14.23    proof
   14.24      fix x assume "x \<in> UnderS A"
   14.25 -    with 1 UnderS_def have "x \<noteq> minim A \<and> (x,minim A) \<in> r" by auto
   14.26 +    with 1 UnderS_def[of r] have "x \<noteq> minim A \<and> (x,minim A) \<in> r" by auto
   14.27      thus "x \<in> underS(minim A)" unfolding underS_def by simp
   14.28    qed
   14.29    (*  *)
   14.30 @@ -173,7 +173,7 @@
   14.31  shows "supr B \<in> Above B"
   14.32  proof(unfold supr_def)
   14.33    have "Above B \<le> Field r"
   14.34 -  using Above_Field by auto
   14.35 +  using Above_Field[of r] by auto
   14.36    thus "minim (Above B) \<in> Above B"
   14.37    using assms by (simp add: minim_in)
   14.38  qed
   14.39 @@ -185,7 +185,7 @@
   14.40  proof-
   14.41    from assms supr_Above
   14.42    have "supr B \<in> Above B" by simp
   14.43 -  with IN Above_def show ?thesis by simp
   14.44 +  with IN Above_def[of r] show ?thesis by simp
   14.45  qed
   14.46  
   14.47  lemma supr_least_Above:
   14.48 @@ -194,7 +194,7 @@
   14.49  shows "(supr B, a) \<in> r"
   14.50  proof(unfold supr_def)
   14.51    have "Above B \<le> Field r"
   14.52 -  using Above_Field by auto
   14.53 +  using Above_Field[of r] by auto
   14.54    thus "(minim (Above B), a) \<in> r"
   14.55    using assms minim_least
   14.56    by simp
   14.57 @@ -211,7 +211,7 @@
   14.58  shows "a = supr B"
   14.59  proof(unfold supr_def)
   14.60    have "Above B \<le> Field r"
   14.61 -  using Above_Field by auto
   14.62 +  using Above_Field[of r] by auto
   14.63    thus "a = minim (Above B)"
   14.64    using assms equals_minim by simp
   14.65  qed
   14.66 @@ -236,7 +236,7 @@
   14.67  shows "supr B \<in> Field r"
   14.68  proof-
   14.69    have "supr B \<in> Above B" using supr_Above assms by simp
   14.70 -  thus ?thesis using assms Above_Field by auto
   14.71 +  thus ?thesis using assms Above_Field[of r] by auto
   14.72  qed
   14.73  
   14.74  lemma supr_above_Above:
   14.75 @@ -264,13 +264,13 @@
   14.76  shows "a = supr (under a)"
   14.77  proof-
   14.78    have "under a \<le> Field r"
   14.79 -  using under_Field by auto
   14.80 +  using under_Field[of r] by auto
   14.81    moreover
   14.82    have "under a \<noteq> {}"
   14.83 -  using IN Refl_under_in REFL by auto
   14.84 +  using IN Refl_under_in[of r] REFL by auto
   14.85    moreover
   14.86    have "a \<in> Above (under a)"
   14.87 -  using in_Above_under IN by auto
   14.88 +  using in_Above_under[of _ r] IN by auto
   14.89    moreover
   14.90    have "\<forall>a' \<in> Above (under a). (a,a') \<in> r"
   14.91    proof(unfold Above_def under_def, auto)
   14.92 @@ -347,7 +347,7 @@
   14.93  shows "a' = a \<or> (a',a) \<in> r"
   14.94  proof-
   14.95    have *: "suc {a} \<in> Field r \<and> a' \<in> Field r"
   14.96 -  using WELL REL well_order_on_domain by auto
   14.97 +  using WELL REL well_order_on_domain by metis
   14.98    {assume **: "a' \<noteq> a"
   14.99     hence "(a,a') \<in> r \<or> (a',a) \<in> r"
  14.100     using TOTAL IN * by (auto simp add: total_on_def)
  14.101 @@ -369,7 +369,7 @@
  14.102  shows "underS (suc {a}) = under a"
  14.103  proof-
  14.104    have 1: "AboveS {a} \<noteq> {}"
  14.105 -  using ABV aboveS_AboveS_singl by auto
  14.106 +  using ABV aboveS_AboveS_singl[of r] by auto
  14.107    have 2: "a \<noteq> suc {a} \<and> (a,suc {a}) \<in> r"
  14.108    using suc_greater[of "{a}" a] IN 1 by auto
  14.109    (*   *)
  14.110 @@ -408,12 +408,12 @@
  14.111  proof(unfold ofilter_def, auto)
  14.112    fix x assume "x \<in> Under A"
  14.113    thus "x \<in> Field r"
  14.114 -  using Under_Field assms by auto
  14.115 +  using Under_Field[of r] assms by auto
  14.116  next
  14.117    fix a x
  14.118    assume "a \<in> Under A" and "x \<in> under a"
  14.119    thus "x \<in> Under A"
  14.120 -  using TRANS under_Under_trans by auto
  14.121 +  using TRANS under_Under_trans[of r] by auto
  14.122  qed
  14.123  
  14.124  lemma ofilter_UnderS[simp]:
  14.125 @@ -422,12 +422,12 @@
  14.126  proof(unfold ofilter_def, auto)
  14.127    fix x assume "x \<in> UnderS A"
  14.128    thus "x \<in> Field r"
  14.129 -  using UnderS_Field assms by auto
  14.130 +  using UnderS_Field[of r] assms by auto
  14.131  next
  14.132    fix a x
  14.133    assume "a \<in> UnderS A" and "x \<in> under a"
  14.134    thus "x \<in> UnderS A"
  14.135 -  using TRANS ANTISYM under_UnderS_trans by auto
  14.136 +  using TRANS ANTISYM under_UnderS_trans[of r] by auto
  14.137  qed
  14.138  
  14.139  lemma ofilter_Int[simp]: "\<lbrakk>ofilter A; ofilter B\<rbrakk> \<Longrightarrow> ofilter(A Int B)"
  14.140 @@ -469,7 +469,7 @@
  14.141    (* Main proof *)
  14.142    fix x assume "x \<in> Under(Under A)"
  14.143    with 1 have 1: "(x,minim A) \<in> r"
  14.144 -  using Under_def by auto
  14.145 +  using Under_def[of r] by auto
  14.146    with Field_def have "x \<in> Field r" by fastforce
  14.147    moreover
  14.148    {fix y assume *: "y \<in> A"
  14.149 @@ -506,7 +506,7 @@
  14.150      hence "(suc A,x) \<in> r"
  14.151      using suc_least_AboveS by auto
  14.152      moreover
  14.153 -    have "(x,suc A) \<in> r" using * under_def by auto
  14.154 +    have "(x,suc A) \<in> r" using * under_def[of r] by auto
  14.155      ultimately show "x = suc A"
  14.156      using ANTISYM antisym_def[of r] by auto
  14.157    qed
    15.1 --- a/src/HOL/Cardinals/Wellorder_Relation_FP.thy	Thu Jan 16 18:52:50 2014 +0100
    15.2 +++ b/src/HOL/Cardinals/Wellorder_Relation_FP.thy	Thu Jan 16 20:52:54 2014 +0100
    15.3 @@ -18,7 +18,9 @@
    15.4  i.e., as containing the diagonals of their fields. *}
    15.5  
    15.6  
    15.7 -locale wo_rel = rel + assumes WELL: "Well_order r"
    15.8 +locale wo_rel =
    15.9 +  fixes r :: "'a rel"
   15.10 +  assumes WELL: "Well_order r"
   15.11  begin
   15.12  
   15.13  text{* The following context encompasses all this section. In other words,
   15.14 @@ -26,6 +28,15 @@
   15.15  
   15.16  (* context wo_rel  *)
   15.17  
   15.18 +abbreviation under where "under \<equiv> Order_Relation_More_FP.under r"
   15.19 +abbreviation underS where "underS \<equiv> Order_Relation_More_FP.underS r"
   15.20 +abbreviation Under where "Under \<equiv> Order_Relation_More_FP.Under r"
   15.21 +abbreviation UnderS where "UnderS \<equiv> Order_Relation_More_FP.UnderS r"
   15.22 +abbreviation above where "above \<equiv> Order_Relation_More_FP.above r"
   15.23 +abbreviation aboveS where "aboveS \<equiv> Order_Relation_More_FP.aboveS r"
   15.24 +abbreviation Above where "Above \<equiv> Order_Relation_More_FP.Above r"
   15.25 +abbreviation AboveS where "AboveS \<equiv> Order_Relation_More_FP.AboveS r"
   15.26 +
   15.27  
   15.28  subsection {* Auxiliaries *}
   15.29  
   15.30 @@ -109,7 +120,7 @@
   15.31    let ?rS = "r - Id"
   15.32    have "adm_wf (r - Id) H"
   15.33    unfolding adm_wf_def
   15.34 -  using ADM adm_wo_def[of H] underS_def by auto
   15.35 +  using ADM adm_wo_def[of H] underS_def[of r] by auto
   15.36    hence "wfrec ?rS H = H (wfrec ?rS H)"
   15.37    using WF wfrec_fixpoint[of ?rS H] by simp
   15.38    thus ?thesis unfolding worec_def .
   15.39 @@ -327,7 +338,7 @@
   15.40  shows "suc B \<in> AboveS B"
   15.41  proof(unfold suc_def)
   15.42    have "AboveS B \<le> Field r"
   15.43 -  using AboveS_Field by auto
   15.44 +  using AboveS_Field[of r] by auto
   15.45    thus "minim (AboveS B) \<in> AboveS B"
   15.46    using assms by (simp add: minim_in)
   15.47  qed
   15.48 @@ -340,7 +351,7 @@
   15.49  proof-
   15.50    from assms suc_AboveS
   15.51    have "suc B \<in> AboveS B" by simp
   15.52 -  with IN AboveS_def show ?thesis by simp
   15.53 +  with IN AboveS_def[of r] show ?thesis by simp
   15.54  qed
   15.55  
   15.56  
   15.57 @@ -349,7 +360,7 @@
   15.58  shows "(suc B,a) \<in> r"
   15.59  proof(unfold suc_def)
   15.60    have "AboveS B \<le> Field r"
   15.61 -  using AboveS_Field by auto
   15.62 +  using AboveS_Field[of r] by auto
   15.63    thus "(minim (AboveS B),a) \<in> r"
   15.64    using assms minim_least by simp
   15.65  qed
   15.66 @@ -361,7 +372,7 @@
   15.67  proof-
   15.68    have "suc B \<in> AboveS B" using suc_AboveS assms by simp
   15.69    thus ?thesis
   15.70 -  using assms AboveS_Field by auto
   15.71 +  using assms AboveS_Field[of r] by auto
   15.72  qed
   15.73  
   15.74  
   15.75 @@ -371,7 +382,7 @@
   15.76  shows "a = suc B"
   15.77  proof(unfold suc_def)
   15.78    have "AboveS B \<le> Field r"
   15.79 -  using AboveS_Field[of B] by auto
   15.80 +  using AboveS_Field[of r B] by auto
   15.81    thus "a = minim (AboveS B)"
   15.82    using assms equals_minim
   15.83    by simp
   15.84 @@ -383,17 +394,17 @@
   15.85  shows "a = suc (underS a)"
   15.86  proof-
   15.87    have "underS a \<le> Field r"
   15.88 -  using underS_Field by auto
   15.89 +  using underS_Field[of r] by auto
   15.90    moreover
   15.91    have "a \<in> AboveS (underS a)"
   15.92 -  using in_AboveS_underS IN by auto
   15.93 +  using in_AboveS_underS IN by fast
   15.94    moreover
   15.95    have "\<forall>a' \<in> AboveS (underS a). (a,a') \<in> r"
   15.96    proof(clarify)
   15.97      fix a'
   15.98      assume *: "a' \<in> AboveS (underS a)"
   15.99      hence **: "a' \<in> Field r"
  15.100 -    using AboveS_Field by auto
  15.101 +    using AboveS_Field by fast
  15.102      {assume "(a,a') \<notin> r"
  15.103       hence "a' = a \<or> (a',a) \<in> r"
  15.104       using TOTAL IN ** by (auto simp add: total_on_def)
  15.105 @@ -407,7 +418,7 @@
  15.106        hence "a' \<in> underS a"
  15.107        unfolding underS_def by simp
  15.108        hence "a' \<notin> AboveS (underS a)"
  15.109 -      using AboveS_disjoint by blast
  15.110 +      using AboveS_disjoint by fast
  15.111        with * have False by simp
  15.112       }
  15.113       ultimately have "(a,a') \<in> r" by blast
  15.114 @@ -486,7 +497,7 @@
  15.115           hence "(?a,x) \<in> r"
  15.116           using TOTAL total_on_def[of "Field r" r]
  15.117                 2 4 11 12 by auto
  15.118 -         hence "?a \<in> under x" using under_def by auto
  15.119 +         hence "?a \<in> under x" using under_def[of r] by auto
  15.120           hence "?a \<in> A" using ** 13 by blast
  15.121           with 4 have False by simp
  15.122          }
  15.123 @@ -527,7 +538,7 @@
  15.124    thus "(\<Union> a \<in> A. under a) \<le> A" by blast
  15.125  next
  15.126    have "\<forall>a \<in> A. a \<in> under a"
  15.127 -  using REFL Refl_under_in assms ofilter_def by blast
  15.128 +  using REFL Refl_under_in[of r] assms ofilter_def[of A] by blast
  15.129    thus "A \<le> (\<Union> a \<in> A. under a)" by blast
  15.130  qed
  15.131  
  15.132 @@ -562,13 +573,13 @@
  15.133      }
  15.134      moreover
  15.135      {assume "(a,b) \<in> r"
  15.136 -     with underS_incr TRANS ANTISYM 1 2
  15.137 +     with underS_incr[of r] TRANS ANTISYM 1 2
  15.138       have "A \<le> B" by auto
  15.139       hence ?thesis by auto
  15.140      }
  15.141      moreover
  15.142       {assume "(b,a) \<in> r"
  15.143 -     with underS_incr TRANS ANTISYM 1 2
  15.144 +     with underS_incr[of r] TRANS ANTISYM 1 2
  15.145       have "B \<le> A" by auto
  15.146       hence ?thesis by auto
  15.147      }
  15.148 @@ -582,7 +593,7 @@
  15.149  shows "A \<union> (AboveS A) = Field r"
  15.150  proof
  15.151    show "A \<union> (AboveS A) \<le> Field r"
  15.152 -  using assms ofilter_def AboveS_Field by auto
  15.153 +  using assms ofilter_def AboveS_Field[of r] by auto
  15.154  next
  15.155    {fix x assume *: "x \<in> Field r" and **: "x \<notin> A"
  15.156     {fix y assume ***: "y \<in> A"
  15.157 @@ -592,7 +603,7 @@
  15.158       have "y \<in> Field r" using assms ofilter_def *** by auto
  15.159       ultimately have "(x,y) \<in> r"
  15.160       using 1 * TOTAL total_on_def[of _ r] by auto
  15.161 -     with *** assms ofilter_def under_def have "x \<in> A" by auto
  15.162 +     with *** assms ofilter_def under_def[of r] have "x \<in> A" by auto
  15.163       with ** have False by contradiction
  15.164      }
  15.165      hence "(y,x) \<in> r" by blast
  15.166 @@ -610,7 +621,7 @@
  15.167  shows "b \<in> A"
  15.168  proof-
  15.169    have *: "suc A \<in> Field r \<and> b \<in> Field r"
  15.170 -  using WELL REL well_order_on_domain by auto
  15.171 +  using WELL REL well_order_on_domain[of "Field r"] by auto
  15.172    {assume **: "b \<notin> A"
  15.173     hence "b \<in> AboveS A"
  15.174     using OF * ofilter_AboveS_Field by auto