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