src/HOL/Cardinals/Wellorder_Relation_FP.thy

 to well-order relations.  Note that we consider well-order relations
 as {\em non-strict relations},
 i.e., as containing the diagonals of their fields. *}
 
 
-locale wo_rel = rel + assumes WELL: "Well_order r"
+locale wo_rel =
+  fixes r :: "'a rel"
+  assumes WELL: "Well_order r"
 begin
 
 text{* The following context encompasses all this section. In other words,
 for the whole section, we consider a fixed well-order relation @{term "r"}. *}
 
 (* context wo_rel  *)
+
+abbreviation under where "under \<equiv> Order_Relation_More_FP.under r"
+abbreviation underS where "underS \<equiv> Order_Relation_More_FP.underS r"
+abbreviation Under where "Under \<equiv> Order_Relation_More_FP.Under r"
+abbreviation UnderS where "UnderS \<equiv> Order_Relation_More_FP.UnderS r"
+abbreviation above where "above \<equiv> Order_Relation_More_FP.above r"
+abbreviation aboveS where "aboveS \<equiv> Order_Relation_More_FP.aboveS r"
+abbreviation Above where "Above \<equiv> Order_Relation_More_FP.Above r"
+abbreviation AboveS where "AboveS \<equiv> Order_Relation_More_FP.AboveS r"
 
 
 subsection {* Auxiliaries *}
 
 

 shows "worec H = H (worec H)"
 proof-
   let ?rS = "r - Id"
   have "adm_wf (r - Id) H"
   unfolding adm_wf_def
-  using ADM adm_wo_def[of H] underS_def by auto
+  using ADM adm_wo_def[of H] underS_def[of r] by auto
   hence "wfrec ?rS H = H (wfrec ?rS H)"
   using WF wfrec_fixpoint[of ?rS H] by simp
   thus ?thesis unfolding worec_def .
 qed
 

 lemma suc_AboveS:
 assumes SUB: "B \<le> Field r" and ABOVES: "AboveS B \<noteq> {}"
 shows "suc B \<in> AboveS B"
 proof(unfold suc_def)
   have "AboveS B \<le> Field r"
-  using AboveS_Field by auto
+  using AboveS_Field[of r] by auto
   thus "minim (AboveS B) \<in> AboveS B"
   using assms by (simp add: minim_in)
 qed
 
 

         IN: "b \<in> B"
 shows "suc B \<noteq> b \<and> (b,suc B) \<in> r"
 proof-
   from assms suc_AboveS
   have "suc B \<in> AboveS B" by simp
-  with IN AboveS_def show ?thesis by simp
+  with IN AboveS_def[of r] show ?thesis by simp
 qed
 
 
 lemma suc_least_AboveS:
 assumes ABOVES: "a \<in> AboveS B"
 shows "(suc B,a) \<in> r"
 proof(unfold suc_def)
   have "AboveS B \<le> Field r"
-  using AboveS_Field by auto
+  using AboveS_Field[of r] by auto
   thus "(minim (AboveS B),a) \<in> r"
   using assms minim_least by simp
 qed
 
 

 assumes "B \<le> Field r" and "AboveS B \<noteq> {}"
 shows "suc B \<in> Field r"
 proof-
   have "suc B \<in> AboveS B" using suc_AboveS assms by simp
   thus ?thesis
-  using assms AboveS_Field by auto
+  using assms AboveS_Field[of r] by auto
 qed
 
 
 lemma equals_suc_AboveS:
 assumes SUB: "B \<le> Field r" and ABV: "a \<in> AboveS B" and
         MINIM: "\<And> a'. a' \<in> AboveS B \<Longrightarrow> (a,a') \<in> r"
 shows "a = suc B"
 proof(unfold suc_def)
   have "AboveS B \<le> Field r"
-  using AboveS_Field[of B] by auto
+  using AboveS_Field[of r B] by auto
   thus "a = minim (AboveS B)"
   using assms equals_minim
   by simp
 qed
 

 lemma suc_underS:
 assumes IN: "a \<in> Field r"
 shows "a = suc (underS a)"
 proof-
   have "underS a \<le> Field r"
-  using underS_Field by auto
+  using underS_Field[of r] by auto
   moreover
   have "a \<in> AboveS (underS a)"
-  using in_AboveS_underS IN by auto
+  using in_AboveS_underS IN by fast
   moreover
   have "\<forall>a' \<in> AboveS (underS a). (a,a') \<in> r"
   proof(clarify)
     fix a'
     assume *: "a' \<in> AboveS (underS a)"
     hence **: "a' \<in> Field r"
-    using AboveS_Field by auto
+    using AboveS_Field by fast
     {assume "(a,a') \<notin> r"
      hence "a' = a \<or> (a',a) \<in> r"
      using TOTAL IN ** by (auto simp add: total_on_def)
      moreover
      {assume "a' = a"

      moreover
      {assume "a' \<noteq> a \<and> (a',a) \<in> r"
       hence "a' \<in> underS a"
       unfolding underS_def by simp
       hence "a' \<notin> AboveS (underS a)"
-      using AboveS_disjoint by blast
+      using AboveS_disjoint by fast
       with * have False by simp
      }
      ultimately have "(a,a') \<in> r" by blast
     }
     thus  "(a, a') \<in> r" by blast

         have 13: "under x \<le> A" using * ofilter_def ** by auto
         {assume "(x,?a) \<notin> r"
          hence "(?a,x) \<in> r"
          using TOTAL total_on_def[of "Field r" r]
                2 4 11 12 by auto
-         hence "?a \<in> under x" using under_def by auto
+         hence "?a \<in> under x" using under_def[of r] by auto
          hence "?a \<in> A" using ** 13 by blast
          with 4 have False by simp
         }
         thus "(x,?a) \<in> r" by blast
       qed

   have "\<forall>a \<in> A. under a \<le> A"
   using assms ofilter_def by auto
   thus "(\<Union> a \<in> A. under a) \<le> A" by blast
 next
   have "\<forall>a \<in> A. a \<in> under a"
-  using REFL Refl_under_in assms ofilter_def by blast
+  using REFL Refl_under_in[of r] assms ofilter_def[of A] by blast
   thus "A \<le> (\<Union> a \<in> A. under a)" by blast
 qed
 
 
 subsubsection{* Other properties *}

     moreover
     {assume "a = b" with 1 2 have ?thesis by auto
     }
     moreover
     {assume "(a,b) \<in> r"
-     with underS_incr TRANS ANTISYM 1 2
+     with underS_incr[of r] TRANS ANTISYM 1 2
      have "A \<le> B" by auto
      hence ?thesis by auto
     }
     moreover
      {assume "(b,a) \<in> r"
-     with underS_incr TRANS ANTISYM 1 2
+     with underS_incr[of r] TRANS ANTISYM 1 2
      have "B \<le> A" by auto
      hence ?thesis by auto
     }
     ultimately show ?thesis by blast
   qed

 lemma ofilter_AboveS_Field:
 assumes "ofilter A"
 shows "A \<union> (AboveS A) = Field r"
 proof
   show "A \<union> (AboveS A) \<le> Field r"
-  using assms ofilter_def AboveS_Field by auto
+  using assms ofilter_def AboveS_Field[of r] by auto
 next
   {fix x assume *: "x \<in> Field r" and **: "x \<notin> A"
    {fix y assume ***: "y \<in> A"
     with ** have 1: "y \<noteq> x" by auto
     {assume "(y,x) \<notin> r"
      moreover
      have "y \<in> Field r" using assms ofilter_def *** by auto
      ultimately have "(x,y) \<in> r"
      using 1 * TOTAL total_on_def[of _ r] by auto
-     with *** assms ofilter_def under_def have "x \<in> A" by auto
+     with *** assms ofilter_def under_def[of r] have "x \<in> A" by auto
      with ** have False by contradiction
     }
     hence "(y,x) \<in> r" by blast
     with 1 have "y \<noteq> x \<and> (y,x) \<in> r" by auto
    }

 assumes OF: "ofilter A" and ABOVE_NE: "AboveS A \<noteq> {}" and
         REL: "(b,suc A) \<in> r" and DIFF: "b \<noteq> suc A"
 shows "b \<in> A"
 proof-
   have *: "suc A \<in> Field r \<and> b \<in> Field r"
-  using WELL REL well_order_on_domain by auto
+  using WELL REL well_order_on_domain[of "Field r"] by auto
   {assume **: "b \<notin> A"
    hence "b \<in> AboveS A"
    using OF * ofilter_AboveS_Field by auto
    hence "(suc A, b) \<in> r"
    using suc_least_AboveS by auto