src/HOL/BNF_Wellorder_Relation.thy
changeset 55056 b5c94200d081
parent 55054 e1f3714bc508
child 55059 ef2e0fb783c6
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/BNF_Wellorder_Relation.thy	Mon Jan 20 18:24:55 2014 +0100
     1.3 @@ -0,0 +1,642 @@
     1.4 +(*  Title:      HOL/BNF_Wellorder_Relation.thy
     1.5 +    Author:     Andrei Popescu, TU Muenchen
     1.6 +    Copyright   2012
     1.7 +
     1.8 +Well-order relations (BNF).
     1.9 +*)
    1.10 +
    1.11 +header {* Well-Order Relations (BNF) *}
    1.12 +
    1.13 +theory BNF_Wellorder_Relation
    1.14 +imports Order_Relation
    1.15 +begin
    1.16 +
    1.17 +
    1.18 +text{* In this section, we develop basic concepts and results pertaining
    1.19 +to well-order relations.  Note that we consider well-order relations
    1.20 +as {\em non-strict relations},
    1.21 +i.e., as containing the diagonals of their fields. *}
    1.22 +
    1.23 +
    1.24 +locale wo_rel =
    1.25 +  fixes r :: "'a rel"
    1.26 +  assumes WELL: "Well_order r"
    1.27 +begin
    1.28 +
    1.29 +text{* The following context encompasses all this section. In other words,
    1.30 +for the whole section, we consider a fixed well-order relation @{term "r"}. *}
    1.31 +
    1.32 +(* context wo_rel  *)
    1.33 +
    1.34 +abbreviation under where "under \<equiv> Order_Relation.under r"
    1.35 +abbreviation underS where "underS \<equiv> Order_Relation.underS r"
    1.36 +abbreviation Under where "Under \<equiv> Order_Relation.Under r"
    1.37 +abbreviation UnderS where "UnderS \<equiv> Order_Relation.UnderS r"
    1.38 +abbreviation above where "above \<equiv> Order_Relation.above r"
    1.39 +abbreviation aboveS where "aboveS \<equiv> Order_Relation.aboveS r"
    1.40 +abbreviation Above where "Above \<equiv> Order_Relation.Above r"
    1.41 +abbreviation AboveS where "AboveS \<equiv> Order_Relation.AboveS r"
    1.42 +
    1.43 +
    1.44 +subsection {* Auxiliaries *}
    1.45 +
    1.46 +
    1.47 +lemma REFL: "Refl r"
    1.48 +using WELL order_on_defs[of _ r] by auto
    1.49 +
    1.50 +
    1.51 +lemma TRANS: "trans r"
    1.52 +using WELL order_on_defs[of _ r] by auto
    1.53 +
    1.54 +
    1.55 +lemma ANTISYM: "antisym r"
    1.56 +using WELL order_on_defs[of _ r] by auto
    1.57 +
    1.58 +
    1.59 +lemma TOTAL: "Total r"
    1.60 +using WELL order_on_defs[of _ r] by auto
    1.61 +
    1.62 +
    1.63 +lemma TOTALS: "\<forall>a \<in> Field r. \<forall>b \<in> Field r. (a,b) \<in> r \<or> (b,a) \<in> r"
    1.64 +using REFL TOTAL refl_on_def[of _ r] total_on_def[of _ r] by force
    1.65 +
    1.66 +
    1.67 +lemma LIN: "Linear_order r"
    1.68 +using WELL well_order_on_def[of _ r] by auto
    1.69 +
    1.70 +
    1.71 +lemma WF: "wf (r - Id)"
    1.72 +using WELL well_order_on_def[of _ r] by auto
    1.73 +
    1.74 +
    1.75 +lemma cases_Total:
    1.76 +"\<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>
    1.77 +             \<Longrightarrow> phi a b"
    1.78 +using TOTALS by auto
    1.79 +
    1.80 +
    1.81 +lemma cases_Total3:
    1.82 +"\<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);
    1.83 +              (a = b \<Longrightarrow> phi a b)\<rbrakk>  \<Longrightarrow> phi a b"
    1.84 +using TOTALS by auto
    1.85 +
    1.86 +
    1.87 +subsection {* Well-founded induction and recursion adapted to non-strict well-order relations  *}
    1.88 +
    1.89 +
    1.90 +text{* Here we provide induction and recursion principles specific to {\em non-strict}
    1.91 +well-order relations.
    1.92 +Although minor variations of those for well-founded relations, they will be useful
    1.93 +for doing away with the tediousness of
    1.94 +having to take out the diagonal each time in order to switch to a well-founded relation. *}
    1.95 +
    1.96 +
    1.97 +lemma well_order_induct:
    1.98 +assumes IND: "\<And>x. \<forall>y. y \<noteq> x \<and> (y, x) \<in> r \<longrightarrow> P y \<Longrightarrow> P x"
    1.99 +shows "P a"
   1.100 +proof-
   1.101 +  have "\<And>x. \<forall>y. (y, x) \<in> r - Id \<longrightarrow> P y \<Longrightarrow> P x"
   1.102 +  using IND by blast
   1.103 +  thus "P a" using WF wf_induct[of "r - Id" P a] by blast
   1.104 +qed
   1.105 +
   1.106 +
   1.107 +definition
   1.108 +worec :: "(('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
   1.109 +where
   1.110 +"worec F \<equiv> wfrec (r - Id) F"
   1.111 +
   1.112 +
   1.113 +definition
   1.114 +adm_wo :: "(('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> bool"
   1.115 +where
   1.116 +"adm_wo H \<equiv> \<forall>f g x. (\<forall>y \<in> underS x. f y = g y) \<longrightarrow> H f x = H g x"
   1.117 +
   1.118 +
   1.119 +lemma worec_fixpoint:
   1.120 +assumes ADM: "adm_wo H"
   1.121 +shows "worec H = H (worec H)"
   1.122 +proof-
   1.123 +  let ?rS = "r - Id"
   1.124 +  have "adm_wf (r - Id) H"
   1.125 +  unfolding adm_wf_def
   1.126 +  using ADM adm_wo_def[of H] underS_def[of r] by auto
   1.127 +  hence "wfrec ?rS H = H (wfrec ?rS H)"
   1.128 +  using WF wfrec_fixpoint[of ?rS H] by simp
   1.129 +  thus ?thesis unfolding worec_def .
   1.130 +qed
   1.131 +
   1.132 +
   1.133 +subsection {* The notions of maximum, minimum, supremum, successor and order filter  *}
   1.134 +
   1.135 +
   1.136 +text{*
   1.137 +We define the successor {\em of a set}, and not of an element (the latter is of course
   1.138 +a particular case).  Also, we define the maximum {\em of two elements}, @{text "max2"},
   1.139 +and the minimum {\em of a set}, @{text "minim"} -- we chose these variants since we
   1.140 +consider them the most useful for well-orders.  The minimum is defined in terms of the
   1.141 +auxiliary relational operator @{text "isMinim"}.  Then, supremum and successor are
   1.142 +defined in terms of minimum as expected.
   1.143 +The minimum is only meaningful for non-empty sets, and the successor is only
   1.144 +meaningful for sets for which strict upper bounds exist.
   1.145 +Order filters for well-orders are also known as ``initial segments". *}
   1.146 +
   1.147 +
   1.148 +definition max2 :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
   1.149 +where "max2 a b \<equiv> if (a,b) \<in> r then b else a"
   1.150 +
   1.151 +
   1.152 +definition isMinim :: "'a set \<Rightarrow> 'a \<Rightarrow> bool"
   1.153 +where "isMinim A b \<equiv> b \<in> A \<and> (\<forall>a \<in> A. (b,a) \<in> r)"
   1.154 +
   1.155 +definition minim :: "'a set \<Rightarrow> 'a"
   1.156 +where "minim A \<equiv> THE b. isMinim A b"
   1.157 +
   1.158 +
   1.159 +definition supr :: "'a set \<Rightarrow> 'a"
   1.160 +where "supr A \<equiv> minim (Above A)"
   1.161 +
   1.162 +definition suc :: "'a set \<Rightarrow> 'a"
   1.163 +where "suc A \<equiv> minim (AboveS A)"
   1.164 +
   1.165 +definition ofilter :: "'a set \<Rightarrow> bool"
   1.166 +where
   1.167 +"ofilter A \<equiv> (A \<le> Field r) \<and> (\<forall>a \<in> A. under a \<le> A)"
   1.168 +
   1.169 +
   1.170 +subsubsection {* Properties of max2 *}
   1.171 +
   1.172 +
   1.173 +lemma max2_greater_among:
   1.174 +assumes "a \<in> Field r" and "b \<in> Field r"
   1.175 +shows "(a, max2 a b) \<in> r \<and> (b, max2 a b) \<in> r \<and> max2 a b \<in> {a,b}"
   1.176 +proof-
   1.177 +  {assume "(a,b) \<in> r"
   1.178 +   hence ?thesis using max2_def assms REFL refl_on_def
   1.179 +   by (auto simp add: refl_on_def)
   1.180 +  }
   1.181 +  moreover
   1.182 +  {assume "a = b"
   1.183 +   hence "(a,b) \<in> r" using REFL  assms
   1.184 +   by (auto simp add: refl_on_def)
   1.185 +  }
   1.186 +  moreover
   1.187 +  {assume *: "a \<noteq> b \<and> (b,a) \<in> r"
   1.188 +   hence "(a,b) \<notin> r" using ANTISYM
   1.189 +   by (auto simp add: antisym_def)
   1.190 +   hence ?thesis using * max2_def assms REFL refl_on_def
   1.191 +   by (auto simp add: refl_on_def)
   1.192 +  }
   1.193 +  ultimately show ?thesis using assms TOTAL
   1.194 +  total_on_def[of "Field r" r] by blast
   1.195 +qed
   1.196 +
   1.197 +
   1.198 +lemma max2_greater:
   1.199 +assumes "a \<in> Field r" and "b \<in> Field r"
   1.200 +shows "(a, max2 a b) \<in> r \<and> (b, max2 a b) \<in> r"
   1.201 +using assms by (auto simp add: max2_greater_among)
   1.202 +
   1.203 +
   1.204 +lemma max2_among:
   1.205 +assumes "a \<in> Field r" and "b \<in> Field r"
   1.206 +shows "max2 a b \<in> {a, b}"
   1.207 +using assms max2_greater_among[of a b] by simp
   1.208 +
   1.209 +
   1.210 +lemma max2_equals1:
   1.211 +assumes "a \<in> Field r" and "b \<in> Field r"
   1.212 +shows "(max2 a b = a) = ((b,a) \<in> r)"
   1.213 +using assms ANTISYM unfolding antisym_def using TOTALS
   1.214 +by(auto simp add: max2_def max2_among)
   1.215 +
   1.216 +
   1.217 +lemma max2_equals2:
   1.218 +assumes "a \<in> Field r" and "b \<in> Field r"
   1.219 +shows "(max2 a b = b) = ((a,b) \<in> r)"
   1.220 +using assms ANTISYM unfolding antisym_def using TOTALS
   1.221 +unfolding max2_def by auto
   1.222 +
   1.223 +
   1.224 +subsubsection {* Existence and uniqueness for isMinim and well-definedness of minim *}
   1.225 +
   1.226 +
   1.227 +lemma isMinim_unique:
   1.228 +assumes MINIM: "isMinim B a" and MINIM': "isMinim B a'"
   1.229 +shows "a = a'"
   1.230 +proof-
   1.231 +  {have "a \<in> B"
   1.232 +   using MINIM isMinim_def by simp
   1.233 +   hence "(a',a) \<in> r"
   1.234 +   using MINIM' isMinim_def by simp
   1.235 +  }
   1.236 +  moreover
   1.237 +  {have "a' \<in> B"
   1.238 +   using MINIM' isMinim_def by simp
   1.239 +   hence "(a,a') \<in> r"
   1.240 +   using MINIM isMinim_def by simp
   1.241 +  }
   1.242 +  ultimately
   1.243 +  show ?thesis using ANTISYM antisym_def[of r] by blast
   1.244 +qed
   1.245 +
   1.246 +
   1.247 +lemma Well_order_isMinim_exists:
   1.248 +assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}"
   1.249 +shows "\<exists>b. isMinim B b"
   1.250 +proof-
   1.251 +  from spec[OF WF[unfolded wf_eq_minimal[of "r - Id"]], of B] NE obtain b where
   1.252 +  *: "b \<in> B \<and> (\<forall>b'. b' \<noteq> b \<and> (b',b) \<in> r \<longrightarrow> b' \<notin> B)" by auto
   1.253 +  show ?thesis
   1.254 +  proof(simp add: isMinim_def, rule exI[of _ b], auto)
   1.255 +    show "b \<in> B" using * by simp
   1.256 +  next
   1.257 +    fix b' assume As: "b' \<in> B"
   1.258 +    hence **: "b \<in> Field r \<and> b' \<in> Field r" using As SUB * by auto
   1.259 +    (*  *)
   1.260 +    from As  * have "b' = b \<or> (b',b) \<notin> r" by auto
   1.261 +    moreover
   1.262 +    {assume "b' = b"
   1.263 +     hence "(b,b') \<in> r"
   1.264 +     using ** REFL by (auto simp add: refl_on_def)
   1.265 +    }
   1.266 +    moreover
   1.267 +    {assume "b' \<noteq> b \<and> (b',b) \<notin> r"
   1.268 +     hence "(b,b') \<in> r"
   1.269 +     using ** TOTAL by (auto simp add: total_on_def)
   1.270 +    }
   1.271 +    ultimately show "(b,b') \<in> r" by blast
   1.272 +  qed
   1.273 +qed
   1.274 +
   1.275 +
   1.276 +lemma minim_isMinim:
   1.277 +assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}"
   1.278 +shows "isMinim B (minim B)"
   1.279 +proof-
   1.280 +  let ?phi = "(\<lambda> b. isMinim B b)"
   1.281 +  from assms Well_order_isMinim_exists
   1.282 +  obtain b where *: "?phi b" by blast
   1.283 +  moreover
   1.284 +  have "\<And> b'. ?phi b' \<Longrightarrow> b' = b"
   1.285 +  using isMinim_unique * by auto
   1.286 +  ultimately show ?thesis
   1.287 +  unfolding minim_def using theI[of ?phi b] by blast
   1.288 +qed
   1.289 +
   1.290 +
   1.291 +subsubsection{* Properties of minim *}
   1.292 +
   1.293 +
   1.294 +lemma minim_in:
   1.295 +assumes "B \<le> Field r" and "B \<noteq> {}"
   1.296 +shows "minim B \<in> B"
   1.297 +proof-
   1.298 +  from minim_isMinim[of B] assms
   1.299 +  have "isMinim B (minim B)" by simp
   1.300 +  thus ?thesis by (simp add: isMinim_def)
   1.301 +qed
   1.302 +
   1.303 +
   1.304 +lemma minim_inField:
   1.305 +assumes "B \<le> Field r" and "B \<noteq> {}"
   1.306 +shows "minim B \<in> Field r"
   1.307 +proof-
   1.308 +  have "minim B \<in> B" using assms by (simp add: minim_in)
   1.309 +  thus ?thesis using assms by blast
   1.310 +qed
   1.311 +
   1.312 +
   1.313 +lemma minim_least:
   1.314 +assumes  SUB: "B \<le> Field r" and IN: "b \<in> B"
   1.315 +shows "(minim B, b) \<in> r"
   1.316 +proof-
   1.317 +  from minim_isMinim[of B] assms
   1.318 +  have "isMinim B (minim B)" by auto
   1.319 +  thus ?thesis by (auto simp add: isMinim_def IN)
   1.320 +qed
   1.321 +
   1.322 +
   1.323 +lemma equals_minim:
   1.324 +assumes SUB: "B \<le> Field r" and IN: "a \<in> B" and
   1.325 +        LEAST: "\<And> b. b \<in> B \<Longrightarrow> (a,b) \<in> r"
   1.326 +shows "a = minim B"
   1.327 +proof-
   1.328 +  from minim_isMinim[of B] assms
   1.329 +  have "isMinim B (minim B)" by auto
   1.330 +  moreover have "isMinim B a" using IN LEAST isMinim_def by auto
   1.331 +  ultimately show ?thesis
   1.332 +  using isMinim_unique by auto
   1.333 +qed
   1.334 +
   1.335 +
   1.336 +subsubsection{* Properties of successor *}
   1.337 +
   1.338 +
   1.339 +lemma suc_AboveS:
   1.340 +assumes SUB: "B \<le> Field r" and ABOVES: "AboveS B \<noteq> {}"
   1.341 +shows "suc B \<in> AboveS B"
   1.342 +proof(unfold suc_def)
   1.343 +  have "AboveS B \<le> Field r"
   1.344 +  using AboveS_Field[of r] by auto
   1.345 +  thus "minim (AboveS B) \<in> AboveS B"
   1.346 +  using assms by (simp add: minim_in)
   1.347 +qed
   1.348 +
   1.349 +
   1.350 +lemma suc_greater:
   1.351 +assumes SUB: "B \<le> Field r" and ABOVES: "AboveS B \<noteq> {}" and
   1.352 +        IN: "b \<in> B"
   1.353 +shows "suc B \<noteq> b \<and> (b,suc B) \<in> r"
   1.354 +proof-
   1.355 +  from assms suc_AboveS
   1.356 +  have "suc B \<in> AboveS B" by simp
   1.357 +  with IN AboveS_def[of r] show ?thesis by simp
   1.358 +qed
   1.359 +
   1.360 +
   1.361 +lemma suc_least_AboveS:
   1.362 +assumes ABOVES: "a \<in> AboveS B"
   1.363 +shows "(suc B,a) \<in> r"
   1.364 +proof(unfold suc_def)
   1.365 +  have "AboveS B \<le> Field r"
   1.366 +  using AboveS_Field[of r] by auto
   1.367 +  thus "(minim (AboveS B),a) \<in> r"
   1.368 +  using assms minim_least by simp
   1.369 +qed
   1.370 +
   1.371 +
   1.372 +lemma suc_inField:
   1.373 +assumes "B \<le> Field r" and "AboveS B \<noteq> {}"
   1.374 +shows "suc B \<in> Field r"
   1.375 +proof-
   1.376 +  have "suc B \<in> AboveS B" using suc_AboveS assms by simp
   1.377 +  thus ?thesis
   1.378 +  using assms AboveS_Field[of r] by auto
   1.379 +qed
   1.380 +
   1.381 +
   1.382 +lemma equals_suc_AboveS:
   1.383 +assumes SUB: "B \<le> Field r" and ABV: "a \<in> AboveS B" and
   1.384 +        MINIM: "\<And> a'. a' \<in> AboveS B \<Longrightarrow> (a,a') \<in> r"
   1.385 +shows "a = suc B"
   1.386 +proof(unfold suc_def)
   1.387 +  have "AboveS B \<le> Field r"
   1.388 +  using AboveS_Field[of r B] by auto
   1.389 +  thus "a = minim (AboveS B)"
   1.390 +  using assms equals_minim
   1.391 +  by simp
   1.392 +qed
   1.393 +
   1.394 +
   1.395 +lemma suc_underS:
   1.396 +assumes IN: "a \<in> Field r"
   1.397 +shows "a = suc (underS a)"
   1.398 +proof-
   1.399 +  have "underS a \<le> Field r"
   1.400 +  using underS_Field[of r] by auto
   1.401 +  moreover
   1.402 +  have "a \<in> AboveS (underS a)"
   1.403 +  using in_AboveS_underS IN by fast
   1.404 +  moreover
   1.405 +  have "\<forall>a' \<in> AboveS (underS a). (a,a') \<in> r"
   1.406 +  proof(clarify)
   1.407 +    fix a'
   1.408 +    assume *: "a' \<in> AboveS (underS a)"
   1.409 +    hence **: "a' \<in> Field r"
   1.410 +    using AboveS_Field by fast
   1.411 +    {assume "(a,a') \<notin> r"
   1.412 +     hence "a' = a \<or> (a',a) \<in> r"
   1.413 +     using TOTAL IN ** by (auto simp add: total_on_def)
   1.414 +     moreover
   1.415 +     {assume "a' = a"
   1.416 +      hence "(a,a') \<in> r"
   1.417 +      using REFL IN ** by (auto simp add: refl_on_def)
   1.418 +     }
   1.419 +     moreover
   1.420 +     {assume "a' \<noteq> a \<and> (a',a) \<in> r"
   1.421 +      hence "a' \<in> underS a"
   1.422 +      unfolding underS_def by simp
   1.423 +      hence "a' \<notin> AboveS (underS a)"
   1.424 +      using AboveS_disjoint by fast
   1.425 +      with * have False by simp
   1.426 +     }
   1.427 +     ultimately have "(a,a') \<in> r" by blast
   1.428 +    }
   1.429 +    thus  "(a, a') \<in> r" by blast
   1.430 +  qed
   1.431 +  ultimately show ?thesis
   1.432 +  using equals_suc_AboveS by auto
   1.433 +qed
   1.434 +
   1.435 +
   1.436 +subsubsection {* Properties of order filters *}
   1.437 +
   1.438 +
   1.439 +lemma under_ofilter:
   1.440 +"ofilter (under a)"
   1.441 +proof(unfold ofilter_def under_def, auto simp add: Field_def)
   1.442 +  fix aa x
   1.443 +  assume "(aa,a) \<in> r" "(x,aa) \<in> r"
   1.444 +  thus "(x,a) \<in> r"
   1.445 +  using TRANS trans_def[of r] by blast
   1.446 +qed
   1.447 +
   1.448 +
   1.449 +lemma underS_ofilter:
   1.450 +"ofilter (underS a)"
   1.451 +proof(unfold ofilter_def underS_def under_def, auto simp add: Field_def)
   1.452 +  fix aa assume "(a, aa) \<in> r" "(aa, a) \<in> r" and DIFF: "aa \<noteq> a"
   1.453 +  thus False
   1.454 +  using ANTISYM antisym_def[of r] by blast
   1.455 +next
   1.456 +  fix aa x
   1.457 +  assume "(aa,a) \<in> r" "aa \<noteq> a" "(x,aa) \<in> r"
   1.458 +  thus "(x,a) \<in> r"
   1.459 +  using TRANS trans_def[of r] by blast
   1.460 +qed
   1.461 +
   1.462 +
   1.463 +lemma Field_ofilter:
   1.464 +"ofilter (Field r)"
   1.465 +by(unfold ofilter_def under_def, auto simp add: Field_def)
   1.466 +
   1.467 +
   1.468 +lemma ofilter_underS_Field:
   1.469 +"ofilter A = ((\<exists>a \<in> Field r. A = underS a) \<or> (A = Field r))"
   1.470 +proof
   1.471 +  assume "(\<exists>a\<in>Field r. A = underS a) \<or> A = Field r"
   1.472 +  thus "ofilter A"
   1.473 +  by (auto simp: underS_ofilter Field_ofilter)
   1.474 +next
   1.475 +  assume *: "ofilter A"
   1.476 +  let ?One = "(\<exists>a\<in>Field r. A = underS a)"
   1.477 +  let ?Two = "(A = Field r)"
   1.478 +  show "?One \<or> ?Two"
   1.479 +  proof(cases ?Two, simp)
   1.480 +    let ?B = "(Field r) - A"
   1.481 +    let ?a = "minim ?B"
   1.482 +    assume "A \<noteq> Field r"
   1.483 +    moreover have "A \<le> Field r" using * ofilter_def by simp
   1.484 +    ultimately have 1: "?B \<noteq> {}" by blast
   1.485 +    hence 2: "?a \<in> Field r" using minim_inField[of ?B] by blast
   1.486 +    have 3: "?a \<in> ?B" using minim_in[of ?B] 1 by blast
   1.487 +    hence 4: "?a \<notin> A" by blast
   1.488 +    have 5: "A \<le> Field r" using * ofilter_def[of A] by auto
   1.489 +    (*  *)
   1.490 +    moreover
   1.491 +    have "A = underS ?a"
   1.492 +    proof
   1.493 +      show "A \<le> underS ?a"
   1.494 +      proof(unfold underS_def, auto simp add: 4)
   1.495 +        fix x assume **: "x \<in> A"
   1.496 +        hence 11: "x \<in> Field r" using 5 by auto
   1.497 +        have 12: "x \<noteq> ?a" using 4 ** by auto
   1.498 +        have 13: "under x \<le> A" using * ofilter_def ** by auto
   1.499 +        {assume "(x,?a) \<notin> r"
   1.500 +         hence "(?a,x) \<in> r"
   1.501 +         using TOTAL total_on_def[of "Field r" r]
   1.502 +               2 4 11 12 by auto
   1.503 +         hence "?a \<in> under x" using under_def[of r] by auto
   1.504 +         hence "?a \<in> A" using ** 13 by blast
   1.505 +         with 4 have False by simp
   1.506 +        }
   1.507 +        thus "(x,?a) \<in> r" by blast
   1.508 +      qed
   1.509 +    next
   1.510 +      show "underS ?a \<le> A"
   1.511 +      proof(unfold underS_def, auto)
   1.512 +        fix x
   1.513 +        assume **: "x \<noteq> ?a" and ***: "(x,?a) \<in> r"
   1.514 +        hence 11: "x \<in> Field r" using Field_def by fastforce
   1.515 +         {assume "x \<notin> A"
   1.516 +          hence "x \<in> ?B" using 11 by auto
   1.517 +          hence "(?a,x) \<in> r" using 3 minim_least[of ?B x] by blast
   1.518 +          hence False
   1.519 +          using ANTISYM antisym_def[of r] ** *** by auto
   1.520 +         }
   1.521 +        thus "x \<in> A" by blast
   1.522 +      qed
   1.523 +    qed
   1.524 +    ultimately have ?One using 2 by blast
   1.525 +    thus ?thesis by simp
   1.526 +  qed
   1.527 +qed
   1.528 +
   1.529 +
   1.530 +lemma ofilter_UNION:
   1.531 +"(\<And> i. i \<in> I \<Longrightarrow> ofilter(A i)) \<Longrightarrow> ofilter (\<Union> i \<in> I. A i)"
   1.532 +unfolding ofilter_def by blast
   1.533 +
   1.534 +
   1.535 +lemma ofilter_under_UNION:
   1.536 +assumes "ofilter A"
   1.537 +shows "A = (\<Union> a \<in> A. under a)"
   1.538 +proof
   1.539 +  have "\<forall>a \<in> A. under a \<le> A"
   1.540 +  using assms ofilter_def by auto
   1.541 +  thus "(\<Union> a \<in> A. under a) \<le> A" by blast
   1.542 +next
   1.543 +  have "\<forall>a \<in> A. a \<in> under a"
   1.544 +  using REFL Refl_under_in[of r] assms ofilter_def[of A] by blast
   1.545 +  thus "A \<le> (\<Union> a \<in> A. under a)" by blast
   1.546 +qed
   1.547 +
   1.548 +
   1.549 +subsubsection{* Other properties *}
   1.550 +
   1.551 +
   1.552 +lemma ofilter_linord:
   1.553 +assumes OF1: "ofilter A" and OF2: "ofilter B"
   1.554 +shows "A \<le> B \<or> B \<le> A"
   1.555 +proof(cases "A = Field r")
   1.556 +  assume Case1: "A = Field r"
   1.557 +  hence "B \<le> A" using OF2 ofilter_def by auto
   1.558 +  thus ?thesis by simp
   1.559 +next
   1.560 +  assume Case2: "A \<noteq> Field r"
   1.561 +  with ofilter_underS_Field OF1 obtain a where
   1.562 +  1: "a \<in> Field r \<and> A = underS a" by auto
   1.563 +  show ?thesis
   1.564 +  proof(cases "B = Field r")
   1.565 +    assume Case21: "B = Field r"
   1.566 +    hence "A \<le> B" using OF1 ofilter_def by auto
   1.567 +    thus ?thesis by simp
   1.568 +  next
   1.569 +    assume Case22: "B \<noteq> Field r"
   1.570 +    with ofilter_underS_Field OF2 obtain b where
   1.571 +    2: "b \<in> Field r \<and> B = underS b" by auto
   1.572 +    have "a = b \<or> (a,b) \<in> r \<or> (b,a) \<in> r"
   1.573 +    using 1 2 TOTAL total_on_def[of _ r] by auto
   1.574 +    moreover
   1.575 +    {assume "a = b" with 1 2 have ?thesis by auto
   1.576 +    }
   1.577 +    moreover
   1.578 +    {assume "(a,b) \<in> r"
   1.579 +     with underS_incr[of r] TRANS ANTISYM 1 2
   1.580 +     have "A \<le> B" by auto
   1.581 +     hence ?thesis by auto
   1.582 +    }
   1.583 +    moreover
   1.584 +     {assume "(b,a) \<in> r"
   1.585 +     with underS_incr[of r] TRANS ANTISYM 1 2
   1.586 +     have "B \<le> A" by auto
   1.587 +     hence ?thesis by auto
   1.588 +    }
   1.589 +    ultimately show ?thesis by blast
   1.590 +  qed
   1.591 +qed
   1.592 +
   1.593 +
   1.594 +lemma ofilter_AboveS_Field:
   1.595 +assumes "ofilter A"
   1.596 +shows "A \<union> (AboveS A) = Field r"
   1.597 +proof
   1.598 +  show "A \<union> (AboveS A) \<le> Field r"
   1.599 +  using assms ofilter_def AboveS_Field[of r] by auto
   1.600 +next
   1.601 +  {fix x assume *: "x \<in> Field r" and **: "x \<notin> A"
   1.602 +   {fix y assume ***: "y \<in> A"
   1.603 +    with ** have 1: "y \<noteq> x" by auto
   1.604 +    {assume "(y,x) \<notin> r"
   1.605 +     moreover
   1.606 +     have "y \<in> Field r" using assms ofilter_def *** by auto
   1.607 +     ultimately have "(x,y) \<in> r"
   1.608 +     using 1 * TOTAL total_on_def[of _ r] by auto
   1.609 +     with *** assms ofilter_def under_def[of r] have "x \<in> A" by auto
   1.610 +     with ** have False by contradiction
   1.611 +    }
   1.612 +    hence "(y,x) \<in> r" by blast
   1.613 +    with 1 have "y \<noteq> x \<and> (y,x) \<in> r" by auto
   1.614 +   }
   1.615 +   with * have "x \<in> AboveS A" unfolding AboveS_def by auto
   1.616 +  }
   1.617 +  thus "Field r \<le> A \<union> (AboveS A)" by blast
   1.618 +qed
   1.619 +
   1.620 +
   1.621 +lemma suc_ofilter_in:
   1.622 +assumes OF: "ofilter A" and ABOVE_NE: "AboveS A \<noteq> {}" and
   1.623 +        REL: "(b,suc A) \<in> r" and DIFF: "b \<noteq> suc A"
   1.624 +shows "b \<in> A"
   1.625 +proof-
   1.626 +  have *: "suc A \<in> Field r \<and> b \<in> Field r"
   1.627 +  using WELL REL well_order_on_domain[of "Field r"] by auto
   1.628 +  {assume **: "b \<notin> A"
   1.629 +   hence "b \<in> AboveS A"
   1.630 +   using OF * ofilter_AboveS_Field by auto
   1.631 +   hence "(suc A, b) \<in> r"
   1.632 +   using suc_least_AboveS by auto
   1.633 +   hence False using REL DIFF ANTISYM *
   1.634 +   by (auto simp add: antisym_def)
   1.635 +  }
   1.636 +  thus ?thesis by blast
   1.637 +qed
   1.638 +
   1.639 +
   1.640 +
   1.641 +end (* context wo_rel *)
   1.642 +
   1.643 +
   1.644 +
   1.645 +end