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