src/HOL/BNF_Wellorder_Relation.thy
author haftmann
Fri Jun 19 07:53:35 2015 +0200 (2015-06-19)
changeset 60517 f16e4fb20652
parent 58889 5b7a9633cfa8
child 60585 48fdff264eb2
permissions -rw-r--r--
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
     1 (*  Title:      HOL/BNF_Wellorder_Relation.thy
     2     Author:     Andrei Popescu, TU Muenchen
     3     Copyright   2012
     4 
     5 Well-order relations as needed by bounded natural functors.
     6 *)
     7 
     8 section {* Well-Order Relations as Needed by Bounded Natural Functors *}
     9 
    10 theory BNF_Wellorder_Relation
    11 imports Order_Relation
    12 begin
    13 
    14 text{* In this section, we develop basic concepts and results pertaining
    15 to well-order relations.  Note that we consider well-order relations
    16 as {\em non-strict relations},
    17 i.e., as containing the diagonals of their fields. *}
    18 
    19 locale wo_rel =
    20   fixes r :: "'a rel"
    21   assumes WELL: "Well_order r"
    22 begin
    23 
    24 text{* The following context encompasses all this section. In other words,
    25 for the whole section, we consider a fixed well-order relation @{term "r"}. *}
    26 
    27 (* context wo_rel  *)
    28 
    29 abbreviation under where "under \<equiv> Order_Relation.under r"
    30 abbreviation underS where "underS \<equiv> Order_Relation.underS r"
    31 abbreviation Under where "Under \<equiv> Order_Relation.Under r"
    32 abbreviation UnderS where "UnderS \<equiv> Order_Relation.UnderS r"
    33 abbreviation above where "above \<equiv> Order_Relation.above r"
    34 abbreviation aboveS where "aboveS \<equiv> Order_Relation.aboveS r"
    35 abbreviation Above where "Above \<equiv> Order_Relation.Above r"
    36 abbreviation AboveS where "AboveS \<equiv> Order_Relation.AboveS r"
    37 abbreviation ofilter where "ofilter \<equiv> Order_Relation.ofilter r"
    38 lemmas ofilter_def = Order_Relation.ofilter_def[of r]
    39 
    40 
    41 subsection {* Auxiliaries *}
    42 
    43 lemma REFL: "Refl r"
    44 using WELL order_on_defs[of _ r] by auto
    45 
    46 lemma TRANS: "trans r"
    47 using WELL order_on_defs[of _ r] by auto
    48 
    49 lemma ANTISYM: "antisym r"
    50 using WELL order_on_defs[of _ r] by auto
    51 
    52 lemma TOTAL: "Total r"
    53 using WELL order_on_defs[of _ r] by auto
    54 
    55 lemma TOTALS: "\<forall>a \<in> Field r. \<forall>b \<in> Field r. (a,b) \<in> r \<or> (b,a) \<in> r"
    56 using REFL TOTAL refl_on_def[of _ r] total_on_def[of _ r] by force
    57 
    58 lemma LIN: "Linear_order r"
    59 using WELL well_order_on_def[of _ r] by auto
    60 
    61 lemma WF: "wf (r - Id)"
    62 using WELL well_order_on_def[of _ r] by auto
    63 
    64 lemma cases_Total:
    65 "\<And> phi a b. \<lbrakk>{a,b} <= Field r; ((a,b) \<in> r \<Longrightarrow> phi a b); ((b,a) \<in> r \<Longrightarrow> phi a b)\<rbrakk>
    66              \<Longrightarrow> phi a b"
    67 using TOTALS by auto
    68 
    69 lemma cases_Total3:
    70 "\<And> phi a b. \<lbrakk>{a,b} \<le> Field r; ((a,b) \<in> r - Id \<or> (b,a) \<in> r - Id \<Longrightarrow> phi a b);
    71               (a = b \<Longrightarrow> phi a b)\<rbrakk>  \<Longrightarrow> phi a b"
    72 using TOTALS by auto
    73 
    74 
    75 subsection {* Well-founded induction and recursion adapted to non-strict well-order relations *}
    76 
    77 text{* Here we provide induction and recursion principles specific to {\em non-strict}
    78 well-order relations.
    79 Although minor variations of those for well-founded relations, they will be useful
    80 for doing away with the tediousness of
    81 having to take out the diagonal each time in order to switch to a well-founded relation. *}
    82 
    83 lemma well_order_induct:
    84 assumes IND: "\<And>x. \<forall>y. y \<noteq> x \<and> (y, x) \<in> r \<longrightarrow> P y \<Longrightarrow> P x"
    85 shows "P a"
    86 proof-
    87   have "\<And>x. \<forall>y. (y, x) \<in> r - Id \<longrightarrow> P y \<Longrightarrow> P x"
    88   using IND by blast
    89   thus "P a" using WF wf_induct[of "r - Id" P a] by blast
    90 qed
    91 
    92 definition
    93 worec :: "(('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    94 where
    95 "worec F \<equiv> wfrec (r - Id) F"
    96 
    97 definition
    98 adm_wo :: "(('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> bool"
    99 where
   100 "adm_wo H \<equiv> \<forall>f g x. (\<forall>y \<in> underS x. f y = g y) \<longrightarrow> H f x = H g x"
   101 
   102 lemma worec_fixpoint:
   103 assumes ADM: "adm_wo H"
   104 shows "worec H = H (worec H)"
   105 proof-
   106   let ?rS = "r - Id"
   107   have "adm_wf (r - Id) H"
   108   unfolding adm_wf_def
   109   using ADM adm_wo_def[of H] underS_def[of r] by auto
   110   hence "wfrec ?rS H = H (wfrec ?rS H)"
   111   using WF wfrec_fixpoint[of ?rS H] by simp
   112   thus ?thesis unfolding worec_def .
   113 qed
   114 
   115 
   116 subsection {* The notions of maximum, minimum, supremum, successor and order filter *}
   117 
   118 text{*
   119 We define the successor {\em of a set}, and not of an element (the latter is of course
   120 a particular case).  Also, we define the maximum {\em of two elements}, @{text "max2"},
   121 and the minimum {\em of a set}, @{text "minim"} -- we chose these variants since we
   122 consider them the most useful for well-orders.  The minimum is defined in terms of the
   123 auxiliary relational operator @{text "isMinim"}.  Then, supremum and successor are
   124 defined in terms of minimum as expected.
   125 The minimum is only meaningful for non-empty sets, and the successor is only
   126 meaningful for sets for which strict upper bounds exist.
   127 Order filters for well-orders are also known as ``initial segments". *}
   128 
   129 definition max2 :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
   130 where "max2 a b \<equiv> if (a,b) \<in> r then b else a"
   131 
   132 definition isMinim :: "'a set \<Rightarrow> 'a \<Rightarrow> bool"
   133 where "isMinim A b \<equiv> b \<in> A \<and> (\<forall>a \<in> A. (b,a) \<in> r)"
   134 
   135 definition minim :: "'a set \<Rightarrow> 'a"
   136 where "minim A \<equiv> THE b. isMinim A b"
   137 
   138 definition supr :: "'a set \<Rightarrow> 'a"
   139 where "supr A \<equiv> minim (Above A)"
   140 
   141 definition suc :: "'a set \<Rightarrow> 'a"
   142 where "suc A \<equiv> minim (AboveS A)"
   143 
   144 
   145 subsubsection {* Properties of max2 *}
   146 
   147 lemma max2_greater_among:
   148 assumes "a \<in> Field r" and "b \<in> Field r"
   149 shows "(a, max2 a b) \<in> r \<and> (b, max2 a b) \<in> r \<and> max2 a b \<in> {a,b}"
   150 proof-
   151   {assume "(a,b) \<in> r"
   152    hence ?thesis using max2_def assms REFL refl_on_def
   153    by (auto simp add: refl_on_def)
   154   }
   155   moreover
   156   {assume "a = b"
   157    hence "(a,b) \<in> r" using REFL  assms
   158    by (auto simp add: refl_on_def)
   159   }
   160   moreover
   161   {assume *: "a \<noteq> b \<and> (b,a) \<in> r"
   162    hence "(a,b) \<notin> r" using ANTISYM
   163    by (auto simp add: antisym_def)
   164    hence ?thesis using * max2_def assms REFL refl_on_def
   165    by (auto simp add: refl_on_def)
   166   }
   167   ultimately show ?thesis using assms TOTAL
   168   total_on_def[of "Field r" r] by blast
   169 qed
   170 
   171 lemma max2_greater:
   172 assumes "a \<in> Field r" and "b \<in> Field r"
   173 shows "(a, max2 a b) \<in> r \<and> (b, max2 a b) \<in> r"
   174 using assms by (auto simp add: max2_greater_among)
   175 
   176 lemma max2_among:
   177 assumes "a \<in> Field r" and "b \<in> Field r"
   178 shows "max2 a b \<in> {a, b}"
   179 using assms max2_greater_among[of a b] by simp
   180 
   181 lemma max2_equals1:
   182 assumes "a \<in> Field r" and "b \<in> Field r"
   183 shows "(max2 a b = a) = ((b,a) \<in> r)"
   184 using assms ANTISYM unfolding antisym_def using TOTALS
   185 by(auto simp add: max2_def max2_among)
   186 
   187 lemma max2_equals2:
   188 assumes "a \<in> Field r" and "b \<in> Field r"
   189 shows "(max2 a b = b) = ((a,b) \<in> r)"
   190 using assms ANTISYM unfolding antisym_def using TOTALS
   191 unfolding max2_def by auto
   192 
   193 
   194 subsubsection {* Existence and uniqueness for isMinim and well-definedness of minim *}
   195 
   196 lemma isMinim_unique:
   197 assumes MINIM: "isMinim B a" and MINIM': "isMinim B a'"
   198 shows "a = a'"
   199 proof-
   200   {have "a \<in> B"
   201    using MINIM isMinim_def by simp
   202    hence "(a',a) \<in> r"
   203    using MINIM' isMinim_def by simp
   204   }
   205   moreover
   206   {have "a' \<in> B"
   207    using MINIM' isMinim_def by simp
   208    hence "(a,a') \<in> r"
   209    using MINIM isMinim_def by simp
   210   }
   211   ultimately
   212   show ?thesis using ANTISYM antisym_def[of r] by blast
   213 qed
   214 
   215 lemma Well_order_isMinim_exists:
   216 assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}"
   217 shows "\<exists>b. isMinim B b"
   218 proof-
   219   from spec[OF WF[unfolded wf_eq_minimal[of "r - Id"]], of B] NE obtain b where
   220   *: "b \<in> B \<and> (\<forall>b'. b' \<noteq> b \<and> (b',b) \<in> r \<longrightarrow> b' \<notin> B)" by auto
   221   show ?thesis
   222   proof(simp add: isMinim_def, rule exI[of _ b], auto)
   223     show "b \<in> B" using * by simp
   224   next
   225     fix b' assume As: "b' \<in> B"
   226     hence **: "b \<in> Field r \<and> b' \<in> Field r" using As SUB * by auto
   227     (*  *)
   228     from As  * have "b' = b \<or> (b',b) \<notin> r" by auto
   229     moreover
   230     {assume "b' = b"
   231      hence "(b,b') \<in> r"
   232      using ** REFL by (auto simp add: refl_on_def)
   233     }
   234     moreover
   235     {assume "b' \<noteq> b \<and> (b',b) \<notin> r"
   236      hence "(b,b') \<in> r"
   237      using ** TOTAL by (auto simp add: total_on_def)
   238     }
   239     ultimately show "(b,b') \<in> r" by blast
   240   qed
   241 qed
   242 
   243 lemma minim_isMinim:
   244 assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}"
   245 shows "isMinim B (minim B)"
   246 proof-
   247   let ?phi = "(\<lambda> b. isMinim B b)"
   248   from assms Well_order_isMinim_exists
   249   obtain b where *: "?phi b" by blast
   250   moreover
   251   have "\<And> b'. ?phi b' \<Longrightarrow> b' = b"
   252   using isMinim_unique * by auto
   253   ultimately show ?thesis
   254   unfolding minim_def using theI[of ?phi b] by blast
   255 qed
   256 
   257 subsubsection{* Properties of minim *}
   258 
   259 lemma minim_in:
   260 assumes "B \<le> Field r" and "B \<noteq> {}"
   261 shows "minim B \<in> B"
   262 proof-
   263   from minim_isMinim[of B] assms
   264   have "isMinim B (minim B)" by simp
   265   thus ?thesis by (simp add: isMinim_def)
   266 qed
   267 
   268 lemma minim_inField:
   269 assumes "B \<le> Field r" and "B \<noteq> {}"
   270 shows "minim B \<in> Field r"
   271 proof-
   272   have "minim B \<in> B" using assms by (simp add: minim_in)
   273   thus ?thesis using assms by blast
   274 qed
   275 
   276 lemma minim_least:
   277 assumes  SUB: "B \<le> Field r" and IN: "b \<in> B"
   278 shows "(minim B, b) \<in> r"
   279 proof-
   280   from minim_isMinim[of B] assms
   281   have "isMinim B (minim B)" by auto
   282   thus ?thesis by (auto simp add: isMinim_def IN)
   283 qed
   284 
   285 lemma equals_minim:
   286 assumes SUB: "B \<le> Field r" and IN: "a \<in> B" and
   287         LEAST: "\<And> b. b \<in> B \<Longrightarrow> (a,b) \<in> r"
   288 shows "a = minim B"
   289 proof-
   290   from minim_isMinim[of B] assms
   291   have "isMinim B (minim B)" by auto
   292   moreover have "isMinim B a" using IN LEAST isMinim_def by auto
   293   ultimately show ?thesis
   294   using isMinim_unique by auto
   295 qed
   296 
   297 subsubsection{* Properties of successor *}
   298 
   299 lemma suc_AboveS:
   300 assumes SUB: "B \<le> Field r" and ABOVES: "AboveS B \<noteq> {}"
   301 shows "suc B \<in> AboveS B"
   302 proof(unfold suc_def)
   303   have "AboveS B \<le> Field r"
   304   using AboveS_Field[of r] by auto
   305   thus "minim (AboveS B) \<in> AboveS B"
   306   using assms by (simp add: minim_in)
   307 qed
   308 
   309 lemma suc_greater:
   310 assumes SUB: "B \<le> Field r" and ABOVES: "AboveS B \<noteq> {}" and
   311         IN: "b \<in> B"
   312 shows "suc B \<noteq> b \<and> (b,suc B) \<in> r"
   313 proof-
   314   from assms suc_AboveS
   315   have "suc B \<in> AboveS B" by simp
   316   with IN AboveS_def[of r] show ?thesis by simp
   317 qed
   318 
   319 lemma suc_least_AboveS:
   320 assumes ABOVES: "a \<in> AboveS B"
   321 shows "(suc B,a) \<in> r"
   322 proof(unfold suc_def)
   323   have "AboveS B \<le> Field r"
   324   using AboveS_Field[of r] by auto
   325   thus "(minim (AboveS B),a) \<in> r"
   326   using assms minim_least by simp
   327 qed
   328 
   329 lemma suc_inField:
   330 assumes "B \<le> Field r" and "AboveS B \<noteq> {}"
   331 shows "suc B \<in> Field r"
   332 proof-
   333   have "suc B \<in> AboveS B" using suc_AboveS assms by simp
   334   thus ?thesis
   335   using assms AboveS_Field[of r] by auto
   336 qed
   337 
   338 lemma equals_suc_AboveS:
   339 assumes SUB: "B \<le> Field r" and ABV: "a \<in> AboveS B" and
   340         MINIM: "\<And> a'. a' \<in> AboveS B \<Longrightarrow> (a,a') \<in> r"
   341 shows "a = suc B"
   342 proof(unfold suc_def)
   343   have "AboveS B \<le> Field r"
   344   using AboveS_Field[of r B] by auto
   345   thus "a = minim (AboveS B)"
   346   using assms equals_minim
   347   by simp
   348 qed
   349 
   350 lemma suc_underS:
   351 assumes IN: "a \<in> Field r"
   352 shows "a = suc (underS a)"
   353 proof-
   354   have "underS a \<le> Field r"
   355   using underS_Field[of r] by auto
   356   moreover
   357   have "a \<in> AboveS (underS a)"
   358   using in_AboveS_underS IN by fast
   359   moreover
   360   have "\<forall>a' \<in> AboveS (underS a). (a,a') \<in> r"
   361   proof(clarify)
   362     fix a'
   363     assume *: "a' \<in> AboveS (underS a)"
   364     hence **: "a' \<in> Field r"
   365     using AboveS_Field by fast
   366     {assume "(a,a') \<notin> r"
   367      hence "a' = a \<or> (a',a) \<in> r"
   368      using TOTAL IN ** by (auto simp add: total_on_def)
   369      moreover
   370      {assume "a' = a"
   371       hence "(a,a') \<in> r"
   372       using REFL IN ** by (auto simp add: refl_on_def)
   373      }
   374      moreover
   375      {assume "a' \<noteq> a \<and> (a',a) \<in> r"
   376       hence "a' \<in> underS a"
   377       unfolding underS_def by simp
   378       hence "a' \<notin> AboveS (underS a)"
   379       using AboveS_disjoint by fast
   380       with * have False by simp
   381      }
   382      ultimately have "(a,a') \<in> r" by blast
   383     }
   384     thus  "(a, a') \<in> r" by blast
   385   qed
   386   ultimately show ?thesis
   387   using equals_suc_AboveS by auto
   388 qed
   389 
   390 
   391 subsubsection {* Properties of order filters *}
   392 
   393 lemma under_ofilter:
   394 "ofilter (under a)"
   395 proof(unfold ofilter_def under_def, auto simp add: Field_def)
   396   fix aa x
   397   assume "(aa,a) \<in> r" "(x,aa) \<in> r"
   398   thus "(x,a) \<in> r"
   399   using TRANS trans_def[of r] by blast
   400 qed
   401 
   402 lemma underS_ofilter:
   403 "ofilter (underS a)"
   404 proof(unfold ofilter_def underS_def under_def, auto simp add: Field_def)
   405   fix aa assume "(a, aa) \<in> r" "(aa, a) \<in> r" and DIFF: "aa \<noteq> a"
   406   thus False
   407   using ANTISYM antisym_def[of r] by blast
   408 next
   409   fix aa x
   410   assume "(aa,a) \<in> r" "aa \<noteq> a" "(x,aa) \<in> r"
   411   thus "(x,a) \<in> r"
   412   using TRANS trans_def[of r] by blast
   413 qed
   414 
   415 lemma Field_ofilter:
   416 "ofilter (Field r)"
   417 by(unfold ofilter_def under_def, auto simp add: Field_def)
   418 
   419 lemma ofilter_underS_Field:
   420 "ofilter A = ((\<exists>a \<in> Field r. A = underS a) \<or> (A = Field r))"
   421 proof
   422   assume "(\<exists>a\<in>Field r. A = underS a) \<or> A = Field r"
   423   thus "ofilter A"
   424   by (auto simp: underS_ofilter Field_ofilter)
   425 next
   426   assume *: "ofilter A"
   427   let ?One = "(\<exists>a\<in>Field r. A = underS a)"
   428   let ?Two = "(A = Field r)"
   429   show "?One \<or> ?Two"
   430   proof(cases ?Two, simp)
   431     let ?B = "(Field r) - A"
   432     let ?a = "minim ?B"
   433     assume "A \<noteq> Field r"
   434     moreover have "A \<le> Field r" using * ofilter_def by simp
   435     ultimately have 1: "?B \<noteq> {}" by blast
   436     hence 2: "?a \<in> Field r" using minim_inField[of ?B] by blast
   437     have 3: "?a \<in> ?B" using minim_in[of ?B] 1 by blast
   438     hence 4: "?a \<notin> A" by blast
   439     have 5: "A \<le> Field r" using * ofilter_def by auto
   440     (*  *)
   441     moreover
   442     have "A = underS ?a"
   443     proof
   444       show "A \<le> underS ?a"
   445       proof(unfold underS_def, auto simp add: 4)
   446         fix x assume **: "x \<in> A"
   447         hence 11: "x \<in> Field r" using 5 by auto
   448         have 12: "x \<noteq> ?a" using 4 ** by auto
   449         have 13: "under x \<le> A" using * ofilter_def ** by auto
   450         {assume "(x,?a) \<notin> r"
   451          hence "(?a,x) \<in> r"
   452          using TOTAL total_on_def[of "Field r" r]
   453                2 4 11 12 by auto
   454          hence "?a \<in> under x" using under_def[of r] by auto
   455          hence "?a \<in> A" using ** 13 by blast
   456          with 4 have False by simp
   457         }
   458         thus "(x,?a) \<in> r" by blast
   459       qed
   460     next
   461       show "underS ?a \<le> A"
   462       proof(unfold underS_def, auto)
   463         fix x
   464         assume **: "x \<noteq> ?a" and ***: "(x,?a) \<in> r"
   465         hence 11: "x \<in> Field r" using Field_def by fastforce
   466          {assume "x \<notin> A"
   467           hence "x \<in> ?B" using 11 by auto
   468           hence "(?a,x) \<in> r" using 3 minim_least[of ?B x] by blast
   469           hence False
   470           using ANTISYM antisym_def[of r] ** *** by auto
   471          }
   472         thus "x \<in> A" by blast
   473       qed
   474     qed
   475     ultimately have ?One using 2 by blast
   476     thus ?thesis by simp
   477   qed
   478 qed
   479 
   480 lemma ofilter_UNION:
   481 "(\<And> i. i \<in> I \<Longrightarrow> ofilter(A i)) \<Longrightarrow> ofilter (\<Union> i \<in> I. A i)"
   482 unfolding ofilter_def by blast
   483 
   484 lemma ofilter_under_UNION:
   485 assumes "ofilter A"
   486 shows "A = (\<Union> a \<in> A. under a)"
   487 proof
   488   have "\<forall>a \<in> A. under a \<le> A"
   489   using assms ofilter_def by auto
   490   thus "(\<Union> a \<in> A. under a) \<le> A" by blast
   491 next
   492   have "\<forall>a \<in> A. a \<in> under a"
   493   using REFL Refl_under_in[of r] assms ofilter_def[of A] by blast
   494   thus "A \<le> (\<Union> a \<in> A. under a)" by blast
   495 qed
   496 
   497 subsubsection{* Other properties *}
   498 
   499 lemma ofilter_linord:
   500 assumes OF1: "ofilter A" and OF2: "ofilter B"
   501 shows "A \<le> B \<or> B \<le> A"
   502 proof(cases "A = Field r")
   503   assume Case1: "A = Field r"
   504   hence "B \<le> A" using OF2 ofilter_def by auto
   505   thus ?thesis by simp
   506 next
   507   assume Case2: "A \<noteq> Field r"
   508   with ofilter_underS_Field OF1 obtain a where
   509   1: "a \<in> Field r \<and> A = underS a" by auto
   510   show ?thesis
   511   proof(cases "B = Field r")
   512     assume Case21: "B = Field r"
   513     hence "A \<le> B" using OF1 ofilter_def by auto
   514     thus ?thesis by simp
   515   next
   516     assume Case22: "B \<noteq> Field r"
   517     with ofilter_underS_Field OF2 obtain b where
   518     2: "b \<in> Field r \<and> B = underS b" by auto
   519     have "a = b \<or> (a,b) \<in> r \<or> (b,a) \<in> r"
   520     using 1 2 TOTAL total_on_def[of _ r] by auto
   521     moreover
   522     {assume "a = b" with 1 2 have ?thesis by auto
   523     }
   524     moreover
   525     {assume "(a,b) \<in> r"
   526      with underS_incr[of r] TRANS ANTISYM 1 2
   527      have "A \<le> B" by auto
   528      hence ?thesis by auto
   529     }
   530     moreover
   531      {assume "(b,a) \<in> r"
   532      with underS_incr[of r] TRANS ANTISYM 1 2
   533      have "B \<le> A" by auto
   534      hence ?thesis by auto
   535     }
   536     ultimately show ?thesis by blast
   537   qed
   538 qed
   539 
   540 lemma ofilter_AboveS_Field:
   541 assumes "ofilter A"
   542 shows "A \<union> (AboveS A) = Field r"
   543 proof
   544   show "A \<union> (AboveS A) \<le> Field r"
   545   using assms ofilter_def AboveS_Field[of r] by auto
   546 next
   547   {fix x assume *: "x \<in> Field r" and **: "x \<notin> A"
   548    {fix y assume ***: "y \<in> A"
   549     with ** have 1: "y \<noteq> x" by auto
   550     {assume "(y,x) \<notin> r"
   551      moreover
   552      have "y \<in> Field r" using assms ofilter_def *** by auto
   553      ultimately have "(x,y) \<in> r"
   554      using 1 * TOTAL total_on_def[of _ r] by auto
   555      with *** assms ofilter_def under_def[of r] have "x \<in> A" by auto
   556      with ** have False by contradiction
   557     }
   558     hence "(y,x) \<in> r" by blast
   559     with 1 have "y \<noteq> x \<and> (y,x) \<in> r" by auto
   560    }
   561    with * have "x \<in> AboveS A" unfolding AboveS_def by auto
   562   }
   563   thus "Field r \<le> A \<union> (AboveS A)" by blast
   564 qed
   565 
   566 lemma suc_ofilter_in:
   567 assumes OF: "ofilter A" and ABOVE_NE: "AboveS A \<noteq> {}" and
   568         REL: "(b,suc A) \<in> r" and DIFF: "b \<noteq> suc A"
   569 shows "b \<in> A"
   570 proof-
   571   have *: "suc A \<in> Field r \<and> b \<in> Field r"
   572   using WELL REL well_order_on_domain[of "Field r"] by auto
   573   {assume **: "b \<notin> A"
   574    hence "b \<in> AboveS A"
   575    using OF * ofilter_AboveS_Field by auto
   576    hence "(suc A, b) \<in> r"
   577    using suc_least_AboveS by auto
   578    hence False using REL DIFF ANTISYM *
   579    by (auto simp add: antisym_def)
   580   }
   581   thus ?thesis by blast
   582 qed
   583 
   584 end (* context wo_rel *)
   585 
   586 end