src/HOL/BNF_Wellorder_Relation.thy
 author hoelzl Fri Feb 19 13:40:50 2016 +0100 (2016-02-19) changeset 62378 85ed00c1fe7c parent 61799 4cf66f21b764 child 69593 3dda49e08b9d permissions -rw-r--r--
generalize more theorems to support enat and ennreal
     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 \<open>Well-Order Relations as Needed by Bounded Natural Functors\<close>

     9

    10 theory BNF_Wellorder_Relation

    11 imports Order_Relation

    12 begin

    13

    14 text\<open>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.\<close>

    18

    19 locale wo_rel =

    20   fixes r :: "'a rel"

    21   assumes WELL: "Well_order r"

    22 begin

    23

    24 text\<open>The following context encompasses all this section. In other words,

    25 for the whole section, we consider a fixed well-order relation @{term "r"}.\<close>

    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 \<open>Auxiliaries\<close>

    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 \<open>Well-founded induction and recursion adapted to non-strict well-order relations\<close>

    76

    77 text\<open>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.\<close>

    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 \<open>The notions of maximum, minimum, supremum, successor and order filter\<close>

   117

   118 text\<open>

   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}, \<open>max2\<close>,

   121 and the minimum {\em of a set}, \<open>minim\<close> -- 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 \<open>isMinim\<close>.  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".\<close>

   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 \<open>Properties of max2\<close>

   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 \<open>Existence and uniqueness for isMinim and well-definedness of minim\<close>

   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\<open>Properties of minim\<close>

   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\<open>Properties of successor\<close>

   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 \<open>Properties of order filters\<close>

   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\<open>Other properties\<close>

   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