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