src/HOL/Cardinals/Wellorder_Relation.thy
 author wenzelm Sun Nov 02 18:21:45 2014 +0100 (2014-11-02) changeset 58889 5b7a9633cfa8 parent 55173 5556470a02b7 child 60585 48fdff264eb2 permissions -rw-r--r--
```     1 (*  Title:      HOL/Cardinals/Wellorder_Relation.thy
```
```     2     Author:     Andrei Popescu, TU Muenchen
```
```     3     Copyright   2012
```
```     4
```
```     5 Well-order relations.
```
```     6 *)
```
```     7
```
```     8 section {* Well-Order Relations *}
```
```     9
```
```    10 theory Wellorder_Relation
```
```    11 imports BNF_Wellorder_Relation Wellfounded_More
```
```    12 begin
```
```    13
```
```    14 context wo_rel
```
```    15 begin
```
```    16
```
```    17 subsection {* Auxiliaries *}
```
```    18
```
```    19 lemma PREORD: "Preorder r"
```
```    20 using WELL order_on_defs[of _ r] by auto
```
```    21
```
```    22 lemma PARORD: "Partial_order r"
```
```    23 using WELL order_on_defs[of _ r] by auto
```
```    24
```
```    25 lemma cases_Total2:
```
```    26 "\<And> phi a b. \<lbrakk>{a,b} \<le> Field r; ((a,b) \<in> r - Id \<Longrightarrow> phi a b);
```
```    27               ((b,a) \<in> r - Id \<Longrightarrow> phi a b); (a = b \<Longrightarrow> phi a b)\<rbrakk>
```
```    28              \<Longrightarrow> phi a b"
```
```    29 using TOTALS by auto
```
```    30
```
```    31
```
```    32 subsection {* Well-founded induction and recursion adapted to non-strict well-order relations *}
```
```    33
```
```    34 lemma worec_unique_fixpoint:
```
```    35 assumes ADM: "adm_wo H" and fp: "f = H f"
```
```    36 shows "f = worec H"
```
```    37 proof-
```
```    38   have "adm_wf (r - Id) H"
```
```    39   unfolding adm_wf_def
```
```    40   using ADM adm_wo_def[of H] underS_def[of r] by auto
```
```    41   hence "f = wfrec (r - Id) H"
```
```    42   using fp WF wfrec_unique_fixpoint[of "r - Id" H] by simp
```
```    43   thus ?thesis unfolding worec_def .
```
```    44 qed
```
```    45
```
```    46
```
```    47 subsubsection {* Properties of max2 *}
```
```    48
```
```    49 lemma max2_iff:
```
```    50 assumes "a \<in> Field r" and "b \<in> Field r"
```
```    51 shows "((max2 a b, c) \<in> r) = ((a,c) \<in> r \<and> (b,c) \<in> r)"
```
```    52 proof
```
```    53   assume "(max2 a b, c) \<in> r"
```
```    54   thus "(a,c) \<in> r \<and> (b,c) \<in> r"
```
```    55   using assms max2_greater[of a b] TRANS trans_def[of r] by blast
```
```    56 next
```
```    57   assume "(a,c) \<in> r \<and> (b,c) \<in> r"
```
```    58   thus "(max2 a b, c) \<in> r"
```
```    59   using assms max2_among[of a b] by auto
```
```    60 qed
```
```    61
```
```    62
```
```    63 subsubsection {* Properties of minim *}
```
```    64
```
```    65 lemma minim_Under:
```
```    66 "\<lbrakk>B \<le> Field r; B \<noteq> {}\<rbrakk> \<Longrightarrow> minim B \<in> Under B"
```
```    67 by(auto simp add: Under_def minim_inField minim_least)
```
```    68
```
```    69 lemma equals_minim_Under:
```
```    70 "\<lbrakk>B \<le> Field r; a \<in> B; a \<in> Under B\<rbrakk>
```
```    71  \<Longrightarrow> a = minim B"
```
```    72 by(auto simp add: Under_def equals_minim)
```
```    73
```
```    74 lemma minim_iff_In_Under:
```
```    75 assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}"
```
```    76 shows "(a = minim B) = (a \<in> B \<and> a \<in> Under B)"
```
```    77 proof
```
```    78   assume "a = minim B"
```
```    79   thus "a \<in> B \<and> a \<in> Under B"
```
```    80   using assms minim_in minim_Under by simp
```
```    81 next
```
```    82   assume "a \<in> B \<and> a \<in> Under B"
```
```    83   thus "a = minim B"
```
```    84   using assms equals_minim_Under by simp
```
```    85 qed
```
```    86
```
```    87 lemma minim_Under_under:
```
```    88 assumes NE: "A \<noteq> {}" and SUB: "A \<le> Field r"
```
```    89 shows "Under A = under (minim A)"
```
```    90 proof-
```
```    91   (* Preliminary facts *)
```
```    92   have 1: "minim A \<in> A"
```
```    93   using assms minim_in by auto
```
```    94   have 2: "\<forall>x \<in> A. (minim A, x) \<in> r"
```
```    95   using assms minim_least by auto
```
```    96   (* Main proof *)
```
```    97   have "Under A \<le> under (minim A)"
```
```    98   proof
```
```    99     fix x assume "x \<in> Under A"
```
```   100     with 1 Under_def[of r] have "(x,minim A) \<in> r" by auto
```
```   101     thus "x \<in> under(minim A)" unfolding under_def by simp
```
```   102   qed
```
```   103   (*  *)
```
```   104   moreover
```
```   105   (*  *)
```
```   106   have "under (minim A) \<le> Under A"
```
```   107   proof
```
```   108     fix x assume "x \<in> under(minim A)"
```
```   109     hence 11: "(x,minim A) \<in> r" unfolding under_def by simp
```
```   110     hence "x \<in> Field r" unfolding Field_def by auto
```
```   111     moreover
```
```   112     {fix a assume "a \<in> A"
```
```   113      with 2 have "(minim A, a) \<in> r" by simp
```
```   114      with 11 have "(x,a) \<in> r"
```
```   115      using TRANS trans_def[of r] by blast
```
```   116     }
```
```   117     ultimately show "x \<in> Under A" by (unfold Under_def, auto)
```
```   118   qed
```
```   119   (*  *)
```
```   120   ultimately show ?thesis by blast
```
```   121 qed
```
```   122
```
```   123 lemma minim_UnderS_underS:
```
```   124 assumes NE: "A \<noteq> {}" and SUB: "A \<le> Field r"
```
```   125 shows "UnderS A = underS (minim A)"
```
```   126 proof-
```
```   127   (* Preliminary facts *)
```
```   128   have 1: "minim A \<in> A"
```
```   129   using assms minim_in by auto
```
```   130   have 2: "\<forall>x \<in> A. (minim A, x) \<in> r"
```
```   131   using assms minim_least by auto
```
```   132   (* Main proof *)
```
```   133   have "UnderS A \<le> underS (minim A)"
```
```   134   proof
```
```   135     fix x assume "x \<in> UnderS A"
```
```   136     with 1 UnderS_def[of r] have "x \<noteq> minim A \<and> (x,minim A) \<in> r" by auto
```
```   137     thus "x \<in> underS(minim A)" unfolding underS_def by simp
```
```   138   qed
```
```   139   (*  *)
```
```   140   moreover
```
```   141   (*  *)
```
```   142   have "underS (minim A) \<le> UnderS A"
```
```   143   proof
```
```   144     fix x assume "x \<in> underS(minim A)"
```
```   145     hence 11: "x \<noteq> minim A \<and> (x,minim A) \<in> r" unfolding underS_def by simp
```
```   146     hence "x \<in> Field r" unfolding Field_def by auto
```
```   147     moreover
```
```   148     {fix a assume "a \<in> A"
```
```   149      with 2 have 3: "(minim A, a) \<in> r" by simp
```
```   150      with 11 have "(x,a) \<in> r"
```
```   151      using TRANS trans_def[of r] by blast
```
```   152      moreover
```
```   153      have "x \<noteq> a"
```
```   154      proof
```
```   155        assume "x = a"
```
```   156        with 11 3 ANTISYM antisym_def[of r]
```
```   157        show False by auto
```
```   158      qed
```
```   159      ultimately
```
```   160      have "x \<noteq> a \<and> (x,a) \<in> r" by simp
```
```   161     }
```
```   162     ultimately show "x \<in> UnderS A" by (unfold UnderS_def, auto)
```
```   163   qed
```
```   164   (*  *)
```
```   165   ultimately show ?thesis by blast
```
```   166 qed
```
```   167
```
```   168
```
```   169 subsubsection {* Properties of supr *}
```
```   170
```
```   171 lemma supr_Above:
```
```   172 assumes SUB: "B \<le> Field r" and ABOVE: "Above B \<noteq> {}"
```
```   173 shows "supr B \<in> Above B"
```
```   174 proof(unfold supr_def)
```
```   175   have "Above B \<le> Field r"
```
```   176   using Above_Field[of r] by auto
```
```   177   thus "minim (Above B) \<in> Above B"
```
```   178   using assms by (simp add: minim_in)
```
```   179 qed
```
```   180
```
```   181 lemma supr_greater:
```
```   182 assumes SUB: "B \<le> Field r" and ABOVE: "Above B \<noteq> {}" and
```
```   183         IN: "b \<in> B"
```
```   184 shows "(b, supr B) \<in> r"
```
```   185 proof-
```
```   186   from assms supr_Above
```
```   187   have "supr B \<in> Above B" by simp
```
```   188   with IN Above_def[of r] show ?thesis by simp
```
```   189 qed
```
```   190
```
```   191 lemma supr_least_Above:
```
```   192 assumes SUB: "B \<le> Field r" and
```
```   193         ABOVE: "a \<in> Above B"
```
```   194 shows "(supr B, a) \<in> r"
```
```   195 proof(unfold supr_def)
```
```   196   have "Above B \<le> Field r"
```
```   197   using Above_Field[of r] by auto
```
```   198   thus "(minim (Above B), a) \<in> r"
```
```   199   using assms minim_least
```
```   200   by simp
```
```   201 qed
```
```   202
```
```   203 lemma supr_least:
```
```   204 "\<lbrakk>B \<le> Field r; a \<in> Field r; (\<And> b. b \<in> B \<Longrightarrow> (b,a) \<in> r)\<rbrakk>
```
```   205  \<Longrightarrow> (supr B, a) \<in> r"
```
```   206 by(auto simp add: supr_least_Above Above_def)
```
```   207
```
```   208 lemma equals_supr_Above:
```
```   209 assumes SUB: "B \<le> Field r" and ABV: "a \<in> Above B" and
```
```   210         MINIM: "\<And> a'. a' \<in> Above B \<Longrightarrow> (a,a') \<in> r"
```
```   211 shows "a = supr B"
```
```   212 proof(unfold supr_def)
```
```   213   have "Above B \<le> Field r"
```
```   214   using Above_Field[of r] by auto
```
```   215   thus "a = minim (Above B)"
```
```   216   using assms equals_minim by simp
```
```   217 qed
```
```   218
```
```   219 lemma equals_supr:
```
```   220 assumes SUB: "B \<le> Field r" and IN: "a \<in> Field r" and
```
```   221         ABV: "\<And> b. b \<in> B \<Longrightarrow> (b,a) \<in> r" and
```
```   222         MINIM: "\<And> a'. \<lbrakk> a' \<in> Field r; \<And> b. b \<in> B \<Longrightarrow> (b,a') \<in> r\<rbrakk> \<Longrightarrow> (a,a') \<in> r"
```
```   223 shows "a = supr B"
```
```   224 proof-
```
```   225   have "a \<in> Above B"
```
```   226   unfolding Above_def using ABV IN by simp
```
```   227   moreover
```
```   228   have "\<And> a'. a' \<in> Above B \<Longrightarrow> (a,a') \<in> r"
```
```   229   unfolding Above_def using MINIM by simp
```
```   230   ultimately show ?thesis
```
```   231   using equals_supr_Above SUB by auto
```
```   232 qed
```
```   233
```
```   234 lemma supr_inField:
```
```   235 assumes "B \<le> Field r" and  "Above B \<noteq> {}"
```
```   236 shows "supr B \<in> Field r"
```
```   237 proof-
```
```   238   have "supr B \<in> Above B" using supr_Above assms by simp
```
```   239   thus ?thesis using assms Above_Field[of r] by auto
```
```   240 qed
```
```   241
```
```   242 lemma supr_above_Above:
```
```   243 assumes SUB: "B \<le> Field r" and  ABOVE: "Above B \<noteq> {}"
```
```   244 shows "Above B = above (supr B)"
```
```   245 proof(unfold Above_def above_def, auto)
```
```   246   fix a assume "a \<in> Field r" "\<forall>b \<in> B. (b,a) \<in> r"
```
```   247   with supr_least assms
```
```   248   show "(supr B, a) \<in> r" by auto
```
```   249 next
```
```   250   fix b assume "(supr B, b) \<in> r"
```
```   251   thus "b \<in> Field r"
```
```   252   using REFL refl_on_def[of _ r] by auto
```
```   253 next
```
```   254   fix a b
```
```   255   assume 1: "(supr B, b) \<in> r" and 2: "a \<in> B"
```
```   256   with assms supr_greater
```
```   257   have "(a,supr B) \<in> r" by auto
```
```   258   thus "(a,b) \<in> r"
```
```   259   using 1 TRANS trans_def[of r] by blast
```
```   260 qed
```
```   261
```
```   262 lemma supr_under:
```
```   263 assumes IN: "a \<in> Field r"
```
```   264 shows "a = supr (under a)"
```
```   265 proof-
```
```   266   have "under a \<le> Field r"
```
```   267   using under_Field[of r] by auto
```
```   268   moreover
```
```   269   have "under a \<noteq> {}"
```
```   270   using IN Refl_under_in[of r] REFL by auto
```
```   271   moreover
```
```   272   have "a \<in> Above (under a)"
```
```   273   using in_Above_under[of _ r] IN by auto
```
```   274   moreover
```
```   275   have "\<forall>a' \<in> Above (under a). (a,a') \<in> r"
```
```   276   proof(unfold Above_def under_def, auto)
```
```   277     fix a'
```
```   278     assume "\<forall>aa. (aa, a) \<in> r \<longrightarrow> (aa, a') \<in> r"
```
```   279     hence "(a,a) \<in> r \<longrightarrow> (a,a') \<in> r" by blast
```
```   280     moreover have "(a,a) \<in> r"
```
```   281     using REFL IN by (auto simp add: refl_on_def)
```
```   282     ultimately
```
```   283     show  "(a, a') \<in> r" by (rule mp)
```
```   284   qed
```
```   285   ultimately show ?thesis
```
```   286   using equals_supr_Above by auto
```
```   287 qed
```
```   288
```
```   289
```
```   290 subsubsection {* Properties of successor *}
```
```   291
```
```   292 lemma suc_least:
```
```   293 "\<lbrakk>B \<le> Field r; a \<in> Field r; (\<And> b. b \<in> B \<Longrightarrow> a \<noteq> b \<and> (b,a) \<in> r)\<rbrakk>
```
```   294  \<Longrightarrow> (suc B, a) \<in> r"
```
```   295 by(auto simp add: suc_least_AboveS AboveS_def)
```
```   296
```
```   297 lemma equals_suc:
```
```   298 assumes SUB: "B \<le> Field r" and IN: "a \<in> Field r" and
```
```   299  ABVS: "\<And> b. b \<in> B \<Longrightarrow> a \<noteq> b \<and> (b,a) \<in> r" and
```
```   300  MINIM: "\<And> a'. \<lbrakk>a' \<in> Field r; \<And> b. b \<in> B \<Longrightarrow> a' \<noteq> b \<and> (b,a') \<in> r\<rbrakk> \<Longrightarrow> (a,a') \<in> r"
```
```   301 shows "a = suc B"
```
```   302 proof-
```
```   303   have "a \<in> AboveS B"
```
```   304   unfolding AboveS_def using ABVS IN by simp
```
```   305   moreover
```
```   306   have "\<And> a'. a' \<in> AboveS B \<Longrightarrow> (a,a') \<in> r"
```
```   307   unfolding AboveS_def using MINIM by simp
```
```   308   ultimately show ?thesis
```
```   309   using equals_suc_AboveS SUB by auto
```
```   310 qed
```
```   311
```
```   312 lemma suc_above_AboveS:
```
```   313 assumes SUB: "B \<le> Field r" and
```
```   314         ABOVE: "AboveS B \<noteq> {}"
```
```   315 shows "AboveS B = above (suc B)"
```
```   316 proof(unfold AboveS_def above_def, auto)
```
```   317   fix a assume "a \<in> Field r" "\<forall>b \<in> B. a \<noteq> b \<and> (b,a) \<in> r"
```
```   318   with suc_least assms
```
```   319   show "(suc B,a) \<in> r" by auto
```
```   320 next
```
```   321   fix b assume "(suc B, b) \<in> r"
```
```   322   thus "b \<in> Field r"
```
```   323   using REFL refl_on_def[of _ r] by auto
```
```   324 next
```
```   325   fix a b
```
```   326   assume 1: "(suc B, b) \<in> r" and 2: "a \<in> B"
```
```   327   with assms suc_greater[of B a]
```
```   328   have "(a,suc B) \<in> r" by auto
```
```   329   thus "(a,b) \<in> r"
```
```   330   using 1 TRANS trans_def[of r] by blast
```
```   331 next
```
```   332   fix a
```
```   333   assume 1: "(suc B, a) \<in> r" and 2: "a \<in> B"
```
```   334   with assms suc_greater[of B a]
```
```   335   have "(a,suc B) \<in> r" by auto
```
```   336   moreover have "suc B \<in> Field r"
```
```   337   using assms suc_inField by simp
```
```   338   ultimately have "a = suc B"
```
```   339   using 1 2 SUB ANTISYM antisym_def[of r] by auto
```
```   340   thus False
```
```   341   using assms suc_greater[of B a] 2 by auto
```
```   342 qed
```
```   343
```
```   344 lemma suc_singl_pred:
```
```   345 assumes IN: "a \<in> Field r" and ABOVE_NE: "aboveS a \<noteq> {}" and
```
```   346         REL: "(a',suc {a}) \<in> r" and DIFF: "a' \<noteq> suc {a}"
```
```   347 shows "a' = a \<or> (a',a) \<in> r"
```
```   348 proof-
```
```   349   have *: "suc {a} \<in> Field r \<and> a' \<in> Field r"
```
```   350   using WELL REL well_order_on_domain by metis
```
```   351   {assume **: "a' \<noteq> a"
```
```   352    hence "(a,a') \<in> r \<or> (a',a) \<in> r"
```
```   353    using TOTAL IN * by (auto simp add: total_on_def)
```
```   354    moreover
```
```   355    {assume "(a,a') \<in> r"
```
```   356     with ** * assms WELL suc_least[of "{a}" a']
```
```   357     have "(suc {a},a') \<in> r" by auto
```
```   358     with REL DIFF * ANTISYM antisym_def[of r]
```
```   359     have False by simp
```
```   360    }
```
```   361    ultimately have "(a',a) \<in> r"
```
```   362    by blast
```
```   363   }
```
```   364   thus ?thesis by blast
```
```   365 qed
```
```   366
```
```   367 lemma under_underS_suc:
```
```   368 assumes IN: "a \<in> Field r" and ABV: "aboveS a \<noteq> {}"
```
```   369 shows "underS (suc {a}) = under a"
```
```   370 proof-
```
```   371   have 1: "AboveS {a} \<noteq> {}"
```
```   372   using ABV aboveS_AboveS_singl[of r] by auto
```
```   373   have 2: "a \<noteq> suc {a} \<and> (a,suc {a}) \<in> r"
```
```   374   using suc_greater[of "{a}" a] IN 1 by auto
```
```   375   (*   *)
```
```   376   have "underS (suc {a}) \<le> under a"
```
```   377   proof(unfold underS_def under_def, auto)
```
```   378     fix x assume *: "x \<noteq> suc {a}" and **: "(x,suc {a}) \<in> r"
```
```   379     with suc_singl_pred[of a x] IN ABV
```
```   380     have "x = a \<or> (x,a) \<in> r" by auto
```
```   381     with REFL refl_on_def[of _ r] IN
```
```   382     show "(x,a) \<in> r" by auto
```
```   383   qed
```
```   384   (*  *)
```
```   385   moreover
```
```   386   (*   *)
```
```   387   have "under a \<le> underS (suc {a})"
```
```   388   proof(unfold underS_def under_def, auto)
```
```   389     assume "(suc {a}, a) \<in> r"
```
```   390     with 2 ANTISYM antisym_def[of r]
```
```   391     show False by auto
```
```   392   next
```
```   393     fix x assume *: "(x,a) \<in> r"
```
```   394     with 2 TRANS trans_def[of r]
```
```   395     show "(x,suc {a}) \<in> r" by blast
```
```   396   (*  blast is often better than auto/auto for transitivity-like properties *)
```
```   397   qed
```
```   398   (*  *)
```
```   399   ultimately show ?thesis by blast
```
```   400 qed
```
```   401
```
```   402
```
```   403 subsubsection {* Properties of order filters *}
```
```   404
```
```   405 lemma ofilter_Under[simp]:
```
```   406 assumes "A \<le> Field r"
```
```   407 shows "ofilter(Under A)"
```
```   408 proof(unfold ofilter_def, auto)
```
```   409   fix x assume "x \<in> Under A"
```
```   410   thus "x \<in> Field r"
```
```   411   using Under_Field[of r] assms by auto
```
```   412 next
```
```   413   fix a x
```
```   414   assume "a \<in> Under A" and "x \<in> under a"
```
```   415   thus "x \<in> Under A"
```
```   416   using TRANS under_Under_trans[of r] by auto
```
```   417 qed
```
```   418
```
```   419 lemma ofilter_UnderS[simp]:
```
```   420 assumes "A \<le> Field r"
```
```   421 shows "ofilter(UnderS A)"
```
```   422 proof(unfold ofilter_def, auto)
```
```   423   fix x assume "x \<in> UnderS A"
```
```   424   thus "x \<in> Field r"
```
```   425   using UnderS_Field[of r] assms by auto
```
```   426 next
```
```   427   fix a x
```
```   428   assume "a \<in> UnderS A" and "x \<in> under a"
```
```   429   thus "x \<in> UnderS A"
```
```   430   using TRANS ANTISYM under_UnderS_trans[of r] by auto
```
```   431 qed
```
```   432
```
```   433 lemma ofilter_Int[simp]: "\<lbrakk>ofilter A; ofilter B\<rbrakk> \<Longrightarrow> ofilter(A Int B)"
```
```   434 unfolding ofilter_def by blast
```
```   435
```
```   436 lemma ofilter_Un[simp]: "\<lbrakk>ofilter A; ofilter B\<rbrakk> \<Longrightarrow> ofilter(A \<union> B)"
```
```   437 unfolding ofilter_def by blast
```
```   438
```
```   439 lemma ofilter_INTER:
```
```   440 "\<lbrakk>I \<noteq> {}; \<And> i. i \<in> I \<Longrightarrow> ofilter(A i)\<rbrakk> \<Longrightarrow> ofilter (\<Inter> i \<in> I. A i)"
```
```   441 unfolding ofilter_def by blast
```
```   442
```
```   443 lemma ofilter_Inter:
```
```   444 "\<lbrakk>S \<noteq> {}; \<And> A. A \<in> S \<Longrightarrow> ofilter A\<rbrakk> \<Longrightarrow> ofilter (Inter S)"
```
```   445 unfolding ofilter_def by blast
```
```   446
```
```   447 lemma ofilter_Union:
```
```   448 "(\<And> A. A \<in> S \<Longrightarrow> ofilter A) \<Longrightarrow> ofilter (Union S)"
```
```   449 unfolding ofilter_def by blast
```
```   450
```
```   451 lemma ofilter_under_Union:
```
```   452 "ofilter A \<Longrightarrow> A = Union {under a| a. a \<in> A}"
```
```   453 using ofilter_under_UNION[of A]
```
```   454 by(unfold Union_eq, auto)
```
```   455
```
```   456
```
```   457 subsubsection {* Other properties *}
```
```   458
```
```   459 lemma Trans_Under_regressive:
```
```   460 assumes NE: "A \<noteq> {}" and SUB: "A \<le> Field r"
```
```   461 shows "Under(Under A) \<le> Under A"
```
```   462 proof
```
```   463   let ?a = "minim A"
```
```   464   (*  Preliminary facts *)
```
```   465   have 1: "minim A \<in> Under A"
```
```   466   using assms minim_Under by auto
```
```   467   have 2: "\<forall>y \<in> A. (minim A, y) \<in> r"
```
```   468   using assms minim_least by auto
```
```   469   (* Main proof *)
```
```   470   fix x assume "x \<in> Under(Under A)"
```
```   471   with 1 have 1: "(x,minim A) \<in> r"
```
```   472   using Under_def[of r] by auto
```
```   473   with Field_def have "x \<in> Field r" by fastforce
```
```   474   moreover
```
```   475   {fix y assume *: "y \<in> A"
```
```   476    hence "(x,y) \<in> r"
```
```   477    using 1 2 TRANS trans_def[of r] by blast
```
```   478    with Field_def have "(x,y) \<in> r" by auto
```
```   479   }
```
```   480   ultimately
```
```   481   show "x \<in> Under A" unfolding Under_def by auto
```
```   482 qed
```
```   483
```
```   484 lemma ofilter_suc_Field:
```
```   485 assumes OF: "ofilter A" and NE: "A \<noteq> Field r"
```
```   486 shows "ofilter (A \<union> {suc A})"
```
```   487 proof-
```
```   488   (* Preliminary facts *)
```
```   489   have 1: "A \<le> Field r" using OF ofilter_def by auto
```
```   490   hence 2: "AboveS A \<noteq> {}"
```
```   491   using ofilter_AboveS_Field NE OF by blast
```
```   492   from 1 2 suc_inField
```
```   493   have 3: "suc A \<in> Field r" by auto
```
```   494   (* Main proof *)
```
```   495   show ?thesis
```
```   496   proof(unfold ofilter_def, auto simp add: 1 3)
```
```   497     fix a x
```
```   498     assume "a \<in> A" "x \<in> under a" "x \<notin> A"
```
```   499     with OF ofilter_def have False by auto
```
```   500     thus "x = suc A" by simp
```
```   501   next
```
```   502     fix x assume *: "x \<in> under (suc A)" and **: "x \<notin> A"
```
```   503     hence "x \<in> Field r" using under_def Field_def by fastforce
```
```   504     with ** have "x \<in> AboveS A"
```
```   505     using ofilter_AboveS_Field[of A] OF by auto
```
```   506     hence "(suc A,x) \<in> r"
```
```   507     using suc_least_AboveS by auto
```
```   508     moreover
```
```   509     have "(x,suc A) \<in> r" using * under_def[of r] by auto
```
```   510     ultimately show "x = suc A"
```
```   511     using ANTISYM antisym_def[of r] by auto
```
```   512   qed
```
```   513 qed
```
```   514
```
```   515 (* FIXME: needed? *)
```
```   516 declare
```
```   517   minim_in[simp]
```
```   518   minim_inField[simp]
```
```   519   minim_least[simp]
```
```   520   under_ofilter[simp]
```
```   521   underS_ofilter[simp]
```
```   522   Field_ofilter[simp]
```
```   523
```
```   524 end
```
```   525
```
```   526 abbreviation "worec \<equiv> wo_rel.worec"
```
```   527 abbreviation "adm_wo \<equiv> wo_rel.adm_wo"
```
```   528 abbreviation "isMinim \<equiv> wo_rel.isMinim"
```
```   529 abbreviation "minim \<equiv> wo_rel.minim"
```
```   530 abbreviation "max2 \<equiv> wo_rel.max2"
```
```   531 abbreviation "supr \<equiv> wo_rel.supr"
```
```   532 abbreviation "suc \<equiv> wo_rel.suc"
```
```   533
```
```   534 end
```