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