1 (* Title: HOL/Ordinals_and_Cardinals/Constructions_on_Wellorders.thy |
|
2 Author: Andrei Popescu, TU Muenchen |
|
3 Copyright 2012 |
|
4 |
|
5 Constructions on wellorders. |
|
6 *) |
|
7 |
|
8 header {* Constructions on Wellorders *} |
|
9 |
|
10 theory Constructions_on_Wellorders |
|
11 imports Constructions_on_Wellorders_Base Wellorder_Embedding |
|
12 begin |
|
13 |
|
14 declare |
|
15 ordLeq_Well_order_simp[simp] |
|
16 ordLess_Well_order_simp[simp] |
|
17 ordIso_Well_order_simp[simp] |
|
18 not_ordLeq_iff_ordLess[simp] |
|
19 not_ordLess_iff_ordLeq[simp] |
|
20 |
|
21 |
|
22 subsection {* Restriction to a set *} |
|
23 |
|
24 lemma Restr_incr2: |
|
25 "r <= r' \<Longrightarrow> Restr r A <= Restr r' A" |
|
26 by blast |
|
27 |
|
28 lemma Restr_incr: |
|
29 "\<lbrakk>r \<le> r'; A \<le> A'\<rbrakk> \<Longrightarrow> Restr r A \<le> Restr r' A'" |
|
30 by blast |
|
31 |
|
32 lemma Restr_Int: |
|
33 "Restr (Restr r A) B = Restr r (A Int B)" |
|
34 by blast |
|
35 |
|
36 lemma Restr_iff: "(a,b) : Restr r A = (a : A \<and> b : A \<and> (a,b) : r)" |
|
37 by (auto simp add: Field_def) |
|
38 |
|
39 lemma Restr_subset1: "Restr r A \<le> r" |
|
40 by auto |
|
41 |
|
42 lemma Restr_subset2: "Restr r A \<le> A \<times> A" |
|
43 by auto |
|
44 |
|
45 lemma wf_Restr: |
|
46 "wf r \<Longrightarrow> wf(Restr r A)" |
|
47 using wf_subset Restr_subset by blast |
|
48 |
|
49 lemma Restr_incr1: |
|
50 "A \<le> B \<Longrightarrow> Restr r A \<le> Restr r B" |
|
51 by blast |
|
52 |
|
53 |
|
54 subsection {* Order filters versus restrictions and embeddings *} |
|
55 |
|
56 lemma ofilter_Restr: |
|
57 assumes WELL: "Well_order r" and |
|
58 OFA: "ofilter r A" and OFB: "ofilter r B" and SUB: "A \<le> B" |
|
59 shows "ofilter (Restr r B) A" |
|
60 proof- |
|
61 let ?rB = "Restr r B" |
|
62 have Well: "wo_rel r" unfolding wo_rel_def using WELL . |
|
63 hence Refl: "Refl r" by (auto simp add: wo_rel.REFL) |
|
64 hence Field: "Field ?rB = Field r Int B" |
|
65 using Refl_Field_Restr by blast |
|
66 have WellB: "wo_rel ?rB \<and> Well_order ?rB" using WELL |
|
67 by (auto simp add: Well_order_Restr wo_rel_def) |
|
68 (* Main proof *) |
|
69 show ?thesis |
|
70 proof(auto simp add: WellB wo_rel.ofilter_def) |
|
71 fix a assume "a \<in> A" |
|
72 hence "a \<in> Field r \<and> a \<in> B" using assms Well |
|
73 by (auto simp add: wo_rel.ofilter_def) |
|
74 with Field show "a \<in> Field(Restr r B)" by auto |
|
75 next |
|
76 fix a b assume *: "a \<in> A" and "b \<in> under (Restr r B) a" |
|
77 hence "b \<in> under r a" |
|
78 using WELL OFB SUB ofilter_Restr_under[of r B a] by auto |
|
79 thus "b \<in> A" using * Well OFA by(auto simp add: wo_rel.ofilter_def) |
|
80 qed |
|
81 qed |
|
82 |
|
83 lemma ofilter_subset_iso: |
|
84 assumes WELL: "Well_order r" and |
|
85 OFA: "ofilter r A" and OFB: "ofilter r B" |
|
86 shows "(A = B) = iso (Restr r A) (Restr r B) id" |
|
87 using assms |
|
88 by (auto simp add: ofilter_subset_embedS_iso) |
|
89 |
|
90 |
|
91 subsection {* Ordering the well-orders by existence of embeddings *} |
|
92 |
|
93 corollary ordLeq_refl_on: "refl_on {r. Well_order r} ordLeq" |
|
94 using ordLeq_reflexive unfolding ordLeq_def refl_on_def |
|
95 by blast |
|
96 |
|
97 corollary ordLeq_trans: "trans ordLeq" |
|
98 using trans_def[of ordLeq] ordLeq_transitive by blast |
|
99 |
|
100 corollary ordLeq_preorder_on: "preorder_on {r. Well_order r} ordLeq" |
|
101 by(auto simp add: preorder_on_def ordLeq_refl_on ordLeq_trans) |
|
102 |
|
103 corollary ordIso_refl_on: "refl_on {r. Well_order r} ordIso" |
|
104 using ordIso_reflexive unfolding refl_on_def ordIso_def |
|
105 by blast |
|
106 |
|
107 corollary ordIso_trans: "trans ordIso" |
|
108 using trans_def[of ordIso] ordIso_transitive by blast |
|
109 |
|
110 corollary ordIso_sym: "sym ordIso" |
|
111 by (auto simp add: sym_def ordIso_symmetric) |
|
112 |
|
113 corollary ordIso_equiv: "equiv {r. Well_order r} ordIso" |
|
114 by (auto simp add: equiv_def ordIso_sym ordIso_refl_on ordIso_trans) |
|
115 |
|
116 lemma ordLess_irrefl: "irrefl ordLess" |
|
117 by(unfold irrefl_def, auto simp add: ordLess_irreflexive) |
|
118 |
|
119 lemma ordLess_or_ordIso: |
|
120 assumes WELL: "Well_order r" and WELL': "Well_order r'" |
|
121 shows "r <o r' \<or> r' <o r \<or> r =o r'" |
|
122 unfolding ordLess_def ordIso_def |
|
123 using assms embedS_or_iso[of r r'] by auto |
|
124 |
|
125 corollary ordLeq_ordLess_Un_ordIso: |
|
126 "ordLeq = ordLess \<union> ordIso" |
|
127 by (auto simp add: ordLeq_iff_ordLess_or_ordIso) |
|
128 |
|
129 lemma not_ordLeq_ordLess: |
|
130 "r \<le>o r' \<Longrightarrow> \<not> r' <o r" |
|
131 using not_ordLess_ordLeq by blast |
|
132 |
|
133 lemma ordIso_or_ordLess: |
|
134 assumes WELL: "Well_order r" and WELL': "Well_order r'" |
|
135 shows "r =o r' \<or> r <o r' \<or> r' <o r" |
|
136 using assms ordLess_or_ordLeq ordLeq_iff_ordLess_or_ordIso by blast |
|
137 |
|
138 lemmas ord_trans = ordIso_transitive ordLeq_transitive ordLess_transitive |
|
139 ordIso_ordLeq_trans ordLeq_ordIso_trans |
|
140 ordIso_ordLess_trans ordLess_ordIso_trans |
|
141 ordLess_ordLeq_trans ordLeq_ordLess_trans |
|
142 |
|
143 lemma ofilter_ordLeq: |
|
144 assumes "Well_order r" and "ofilter r A" |
|
145 shows "Restr r A \<le>o r" |
|
146 proof- |
|
147 have "A \<le> Field r" using assms by (auto simp add: wo_rel_def wo_rel.ofilter_def) |
|
148 thus ?thesis using assms |
|
149 by (simp add: ofilter_subset_ordLeq wo_rel.Field_ofilter |
|
150 wo_rel_def Restr_Field) |
|
151 qed |
|
152 |
|
153 corollary under_Restr_ordLeq: |
|
154 "Well_order r \<Longrightarrow> Restr r (under r a) \<le>o r" |
|
155 by (auto simp add: ofilter_ordLeq wo_rel.under_ofilter wo_rel_def) |
|
156 |
|
157 |
|
158 subsection {* Copy via direct images *} |
|
159 |
|
160 lemma Id_dir_image: "dir_image Id f \<le> Id" |
|
161 unfolding dir_image_def by auto |
|
162 |
|
163 lemma Un_dir_image: |
|
164 "dir_image (r1 \<union> r2) f = (dir_image r1 f) \<union> (dir_image r2 f)" |
|
165 unfolding dir_image_def by auto |
|
166 |
|
167 lemma Int_dir_image: |
|
168 assumes "inj_on f (Field r1 \<union> Field r2)" |
|
169 shows "dir_image (r1 Int r2) f = (dir_image r1 f) Int (dir_image r2 f)" |
|
170 proof |
|
171 show "dir_image (r1 Int r2) f \<le> (dir_image r1 f) Int (dir_image r2 f)" |
|
172 using assms unfolding dir_image_def inj_on_def by auto |
|
173 next |
|
174 show "(dir_image r1 f) Int (dir_image r2 f) \<le> dir_image (r1 Int r2) f" |
|
175 proof(clarify) |
|
176 fix a' b' |
|
177 assume "(a',b') \<in> dir_image r1 f" "(a',b') \<in> dir_image r2 f" |
|
178 then obtain a1 b1 a2 b2 |
|
179 where 1: "a' = f a1 \<and> b' = f b1 \<and> a' = f a2 \<and> b' = f b2" and |
|
180 2: "(a1,b1) \<in> r1 \<and> (a2,b2) \<in> r2" and |
|
181 3: "{a1,b1} \<le> Field r1 \<and> {a2,b2} \<le> Field r2" |
|
182 unfolding dir_image_def Field_def by blast |
|
183 hence "a1 = a2 \<and> b1 = b2" using assms unfolding inj_on_def by auto |
|
184 hence "a' = f a1 \<and> b' = f b1 \<and> (a1,b1) \<in> r1 Int r2 \<and> (a2,b2) \<in> r1 Int r2" |
|
185 using 1 2 by auto |
|
186 thus "(a',b') \<in> dir_image (r1 \<inter> r2) f" |
|
187 unfolding dir_image_def by blast |
|
188 qed |
|
189 qed |
|
190 |
|
191 |
|
192 subsection {* Ordinal-like sum of two (disjoint) well-orders *} |
|
193 |
|
194 text{* This is roughly obtained by ``concatenating" the two well-orders -- thus, all elements |
|
195 of the first will be smaller than all elements of the second. This construction |
|
196 only makes sense if the fields of the two well-order relations are disjoint. *} |
|
197 |
|
198 definition Osum :: "'a rel \<Rightarrow> 'a rel \<Rightarrow> 'a rel" (infix "Osum" 60) |
|
199 where |
|
200 "r Osum r' = r \<union> r' \<union> {(a,a'). a \<in> Field r \<and> a' \<in> Field r'}" |
|
201 |
|
202 abbreviation Osum2 :: "'a rel \<Rightarrow> 'a rel \<Rightarrow> 'a rel" (infix "\<union>o" 60) |
|
203 where "r \<union>o r' \<equiv> r Osum r'" |
|
204 |
|
205 lemma Field_Osum: "Field(r Osum r') = Field r \<union> Field r'" |
|
206 unfolding Osum_def Field_def by blast |
|
207 |
|
208 lemma Osum_Refl: |
|
209 assumes FLD: "Field r Int Field r' = {}" and |
|
210 REFL: "Refl r" and REFL': "Refl r'" |
|
211 shows "Refl (r Osum r')" |
|
212 using assms (* Need first unfold Field_Osum, only then Osum_def *) |
|
213 unfolding refl_on_def Field_Osum unfolding Osum_def by blast |
|
214 |
|
215 lemma Osum_trans: |
|
216 assumes FLD: "Field r Int Field r' = {}" and |
|
217 TRANS: "trans r" and TRANS': "trans r'" |
|
218 shows "trans (r Osum r')" |
|
219 proof(unfold trans_def, auto) |
|
220 fix x y z assume *: "(x, y) \<in> r \<union>o r'" and **: "(y, z) \<in> r \<union>o r'" |
|
221 show "(x, z) \<in> r \<union>o r'" |
|
222 proof- |
|
223 {assume Case1: "(x,y) \<in> r" |
|
224 hence 1: "x \<in> Field r \<and> y \<in> Field r" unfolding Field_def by auto |
|
225 have ?thesis |
|
226 proof- |
|
227 {assume Case11: "(y,z) \<in> r" |
|
228 hence "(x,z) \<in> r" using Case1 TRANS trans_def[of r] by blast |
|
229 hence ?thesis unfolding Osum_def by auto |
|
230 } |
|
231 moreover |
|
232 {assume Case12: "(y,z) \<in> r'" |
|
233 hence "y \<in> Field r'" unfolding Field_def by auto |
|
234 hence False using FLD 1 by auto |
|
235 } |
|
236 moreover |
|
237 {assume Case13: "z \<in> Field r'" |
|
238 hence ?thesis using 1 unfolding Osum_def by auto |
|
239 } |
|
240 ultimately show ?thesis using ** unfolding Osum_def by blast |
|
241 qed |
|
242 } |
|
243 moreover |
|
244 {assume Case2: "(x,y) \<in> r'" |
|
245 hence 2: "x \<in> Field r' \<and> y \<in> Field r'" unfolding Field_def by auto |
|
246 have ?thesis |
|
247 proof- |
|
248 {assume Case21: "(y,z) \<in> r" |
|
249 hence "y \<in> Field r" unfolding Field_def by auto |
|
250 hence False using FLD 2 by auto |
|
251 } |
|
252 moreover |
|
253 {assume Case22: "(y,z) \<in> r'" |
|
254 hence "(x,z) \<in> r'" using Case2 TRANS' trans_def[of r'] by blast |
|
255 hence ?thesis unfolding Osum_def by auto |
|
256 } |
|
257 moreover |
|
258 {assume Case23: "y \<in> Field r" |
|
259 hence False using FLD 2 by auto |
|
260 } |
|
261 ultimately show ?thesis using ** unfolding Osum_def by blast |
|
262 qed |
|
263 } |
|
264 moreover |
|
265 {assume Case3: "x \<in> Field r \<and> y \<in> Field r'" |
|
266 have ?thesis |
|
267 proof- |
|
268 {assume Case31: "(y,z) \<in> r" |
|
269 hence "y \<in> Field r" unfolding Field_def by auto |
|
270 hence False using FLD Case3 by auto |
|
271 } |
|
272 moreover |
|
273 {assume Case32: "(y,z) \<in> r'" |
|
274 hence "z \<in> Field r'" unfolding Field_def by blast |
|
275 hence ?thesis unfolding Osum_def using Case3 by auto |
|
276 } |
|
277 moreover |
|
278 {assume Case33: "y \<in> Field r" |
|
279 hence False using FLD Case3 by auto |
|
280 } |
|
281 ultimately show ?thesis using ** unfolding Osum_def by blast |
|
282 qed |
|
283 } |
|
284 ultimately show ?thesis using * unfolding Osum_def by blast |
|
285 qed |
|
286 qed |
|
287 |
|
288 lemma Osum_Preorder: |
|
289 "\<lbrakk>Field r Int Field r' = {}; Preorder r; Preorder r'\<rbrakk> \<Longrightarrow> Preorder (r Osum r')" |
|
290 unfolding preorder_on_def using Osum_Refl Osum_trans by blast |
|
291 |
|
292 lemma Osum_antisym: |
|
293 assumes FLD: "Field r Int Field r' = {}" and |
|
294 AN: "antisym r" and AN': "antisym r'" |
|
295 shows "antisym (r Osum r')" |
|
296 proof(unfold antisym_def, auto) |
|
297 fix x y assume *: "(x, y) \<in> r \<union>o r'" and **: "(y, x) \<in> r \<union>o r'" |
|
298 show "x = y" |
|
299 proof- |
|
300 {assume Case1: "(x,y) \<in> r" |
|
301 hence 1: "x \<in> Field r \<and> y \<in> Field r" unfolding Field_def by auto |
|
302 have ?thesis |
|
303 proof- |
|
304 have "(y,x) \<in> r \<Longrightarrow> ?thesis" |
|
305 using Case1 AN antisym_def[of r] by blast |
|
306 moreover |
|
307 {assume "(y,x) \<in> r'" |
|
308 hence "y \<in> Field r'" unfolding Field_def by auto |
|
309 hence False using FLD 1 by auto |
|
310 } |
|
311 moreover |
|
312 have "x \<in> Field r' \<Longrightarrow> False" using FLD 1 by auto |
|
313 ultimately show ?thesis using ** unfolding Osum_def by blast |
|
314 qed |
|
315 } |
|
316 moreover |
|
317 {assume Case2: "(x,y) \<in> r'" |
|
318 hence 2: "x \<in> Field r' \<and> y \<in> Field r'" unfolding Field_def by auto |
|
319 have ?thesis |
|
320 proof- |
|
321 {assume "(y,x) \<in> r" |
|
322 hence "y \<in> Field r" unfolding Field_def by auto |
|
323 hence False using FLD 2 by auto |
|
324 } |
|
325 moreover |
|
326 have "(y,x) \<in> r' \<Longrightarrow> ?thesis" |
|
327 using Case2 AN' antisym_def[of r'] by blast |
|
328 moreover |
|
329 {assume "y \<in> Field r" |
|
330 hence False using FLD 2 by auto |
|
331 } |
|
332 ultimately show ?thesis using ** unfolding Osum_def by blast |
|
333 qed |
|
334 } |
|
335 moreover |
|
336 {assume Case3: "x \<in> Field r \<and> y \<in> Field r'" |
|
337 have ?thesis |
|
338 proof- |
|
339 {assume "(y,x) \<in> r" |
|
340 hence "y \<in> Field r" unfolding Field_def by auto |
|
341 hence False using FLD Case3 by auto |
|
342 } |
|
343 moreover |
|
344 {assume Case32: "(y,x) \<in> r'" |
|
345 hence "x \<in> Field r'" unfolding Field_def by blast |
|
346 hence False using FLD Case3 by auto |
|
347 } |
|
348 moreover |
|
349 have "\<not> y \<in> Field r" using FLD Case3 by auto |
|
350 ultimately show ?thesis using ** unfolding Osum_def by blast |
|
351 qed |
|
352 } |
|
353 ultimately show ?thesis using * unfolding Osum_def by blast |
|
354 qed |
|
355 qed |
|
356 |
|
357 lemma Osum_Partial_order: |
|
358 "\<lbrakk>Field r Int Field r' = {}; Partial_order r; Partial_order r'\<rbrakk> \<Longrightarrow> |
|
359 Partial_order (r Osum r')" |
|
360 unfolding partial_order_on_def using Osum_Preorder Osum_antisym by blast |
|
361 |
|
362 lemma Osum_Total: |
|
363 assumes FLD: "Field r Int Field r' = {}" and |
|
364 TOT: "Total r" and TOT': "Total r'" |
|
365 shows "Total (r Osum r')" |
|
366 using assms |
|
367 unfolding total_on_def Field_Osum unfolding Osum_def by blast |
|
368 |
|
369 lemma Osum_Linear_order: |
|
370 "\<lbrakk>Field r Int Field r' = {}; Linear_order r; Linear_order r'\<rbrakk> \<Longrightarrow> |
|
371 Linear_order (r Osum r')" |
|
372 unfolding linear_order_on_def using Osum_Partial_order Osum_Total by blast |
|
373 |
|
374 lemma Osum_wf: |
|
375 assumes FLD: "Field r Int Field r' = {}" and |
|
376 WF: "wf r" and WF': "wf r'" |
|
377 shows "wf (r Osum r')" |
|
378 unfolding wf_eq_minimal2 unfolding Field_Osum |
|
379 proof(intro allI impI, elim conjE) |
|
380 fix A assume *: "A \<subseteq> Field r \<union> Field r'" and **: "A \<noteq> {}" |
|
381 obtain B where B_def: "B = A Int Field r" by blast |
|
382 show "\<exists>a\<in>A. \<forall>a'\<in>A. (a', a) \<notin> r \<union>o r'" |
|
383 proof(cases "B = {}") |
|
384 assume Case1: "B \<noteq> {}" |
|
385 hence "B \<noteq> {} \<and> B \<le> Field r" using B_def by auto |
|
386 then obtain a where 1: "a \<in> B" and 2: "\<forall>a1 \<in> B. (a1,a) \<notin> r" |
|
387 using WF unfolding wf_eq_minimal2 by blast |
|
388 hence 3: "a \<in> Field r \<and> a \<notin> Field r'" using B_def FLD by auto |
|
389 (* *) |
|
390 have "\<forall>a1 \<in> A. (a1,a) \<notin> r Osum r'" |
|
391 proof(intro ballI) |
|
392 fix a1 assume **: "a1 \<in> A" |
|
393 {assume Case11: "a1 \<in> Field r" |
|
394 hence "(a1,a) \<notin> r" using B_def ** 2 by auto |
|
395 moreover |
|
396 have "(a1,a) \<notin> r'" using 3 by (auto simp add: Field_def) |
|
397 ultimately have "(a1,a) \<notin> r Osum r'" |
|
398 using 3 unfolding Osum_def by auto |
|
399 } |
|
400 moreover |
|
401 {assume Case12: "a1 \<notin> Field r" |
|
402 hence "(a1,a) \<notin> r" unfolding Field_def by auto |
|
403 moreover |
|
404 have "(a1,a) \<notin> r'" using 3 unfolding Field_def by auto |
|
405 ultimately have "(a1,a) \<notin> r Osum r'" |
|
406 using 3 unfolding Osum_def by auto |
|
407 } |
|
408 ultimately show "(a1,a) \<notin> r Osum r'" by blast |
|
409 qed |
|
410 thus ?thesis using 1 B_def by auto |
|
411 next |
|
412 assume Case2: "B = {}" |
|
413 hence 1: "A \<noteq> {} \<and> A \<le> Field r'" using * ** B_def by auto |
|
414 then obtain a' where 2: "a' \<in> A" and 3: "\<forall>a1' \<in> A. (a1',a') \<notin> r'" |
|
415 using WF' unfolding wf_eq_minimal2 by blast |
|
416 hence 4: "a' \<in> Field r' \<and> a' \<notin> Field r" using 1 FLD by blast |
|
417 (* *) |
|
418 have "\<forall>a1' \<in> A. (a1',a') \<notin> r Osum r'" |
|
419 proof(unfold Osum_def, auto simp add: 3) |
|
420 fix a1' assume "(a1', a') \<in> r" |
|
421 thus False using 4 unfolding Field_def by blast |
|
422 next |
|
423 fix a1' assume "a1' \<in> A" and "a1' \<in> Field r" |
|
424 thus False using Case2 B_def by auto |
|
425 qed |
|
426 thus ?thesis using 2 by blast |
|
427 qed |
|
428 qed |
|
429 |
|
430 lemma Osum_minus_Id: |
|
431 assumes TOT: "Total r" and TOT': "Total r'" and |
|
432 NID: "\<not> (r \<le> Id)" and NID': "\<not> (r' \<le> Id)" |
|
433 shows "(r Osum r') - Id \<le> (r - Id) Osum (r' - Id)" |
|
434 proof- |
|
435 {fix a a' assume *: "(a,a') \<in> (r Osum r')" and **: "a \<noteq> a'" |
|
436 have "(a,a') \<in> (r - Id) Osum (r' - Id)" |
|
437 proof- |
|
438 {assume "(a,a') \<in> r \<or> (a,a') \<in> r'" |
|
439 with ** have ?thesis unfolding Osum_def by auto |
|
440 } |
|
441 moreover |
|
442 {assume "a \<in> Field r \<and> a' \<in> Field r'" |
|
443 hence "a \<in> Field(r - Id) \<and> a' \<in> Field (r' - Id)" |
|
444 using assms rel.Total_Id_Field by blast |
|
445 hence ?thesis unfolding Osum_def by auto |
|
446 } |
|
447 ultimately show ?thesis using * unfolding Osum_def by blast |
|
448 qed |
|
449 } |
|
450 thus ?thesis by(auto simp add: Osum_def) |
|
451 qed |
|
452 |
|
453 |
|
454 lemma wf_Int_Times: |
|
455 assumes "A Int B = {}" |
|
456 shows "wf(A \<times> B)" |
|
457 proof(unfold wf_def, auto) |
|
458 fix P x |
|
459 assume *: "\<forall>x. (\<forall>y. y \<in> A \<and> x \<in> B \<longrightarrow> P y) \<longrightarrow> P x" |
|
460 moreover have "\<forall>y \<in> A. P y" using assms * by blast |
|
461 ultimately show "P x" using * by (case_tac "x \<in> B", auto) |
|
462 qed |
|
463 |
|
464 lemma Osum_minus_Id1: |
|
465 assumes "r \<le> Id" |
|
466 shows "(r Osum r') - Id \<le> (r' - Id) \<union> (Field r \<times> Field r')" |
|
467 proof- |
|
468 let ?Left = "(r Osum r') - Id" |
|
469 let ?Right = "(r' - Id) \<union> (Field r \<times> Field r')" |
|
470 {fix a::'a and b assume *: "(a,b) \<notin> Id" |
|
471 {assume "(a,b) \<in> r" |
|
472 with * have False using assms by auto |
|
473 } |
|
474 moreover |
|
475 {assume "(a,b) \<in> r'" |
|
476 with * have "(a,b) \<in> r' - Id" by auto |
|
477 } |
|
478 ultimately |
|
479 have "(a,b) \<in> ?Left \<Longrightarrow> (a,b) \<in> ?Right" |
|
480 unfolding Osum_def by auto |
|
481 } |
|
482 thus ?thesis by auto |
|
483 qed |
|
484 |
|
485 lemma Osum_minus_Id2: |
|
486 assumes "r' \<le> Id" |
|
487 shows "(r Osum r') - Id \<le> (r - Id) \<union> (Field r \<times> Field r')" |
|
488 proof- |
|
489 let ?Left = "(r Osum r') - Id" |
|
490 let ?Right = "(r - Id) \<union> (Field r \<times> Field r')" |
|
491 {fix a::'a and b assume *: "(a,b) \<notin> Id" |
|
492 {assume "(a,b) \<in> r'" |
|
493 with * have False using assms by auto |
|
494 } |
|
495 moreover |
|
496 {assume "(a,b) \<in> r" |
|
497 with * have "(a,b) \<in> r - Id" by auto |
|
498 } |
|
499 ultimately |
|
500 have "(a,b) \<in> ?Left \<Longrightarrow> (a,b) \<in> ?Right" |
|
501 unfolding Osum_def by auto |
|
502 } |
|
503 thus ?thesis by auto |
|
504 qed |
|
505 |
|
506 lemma Osum_wf_Id: |
|
507 assumes TOT: "Total r" and TOT': "Total r'" and |
|
508 FLD: "Field r Int Field r' = {}" and |
|
509 WF: "wf(r - Id)" and WF': "wf(r' - Id)" |
|
510 shows "wf ((r Osum r') - Id)" |
|
511 proof(cases "r \<le> Id \<or> r' \<le> Id") |
|
512 assume Case1: "\<not>(r \<le> Id \<or> r' \<le> Id)" |
|
513 have "Field(r - Id) Int Field(r' - Id) = {}" |
|
514 using FLD mono_Field[of "r - Id" r] mono_Field[of "r' - Id" r'] |
|
515 Diff_subset[of r Id] Diff_subset[of r' Id] by blast |
|
516 thus ?thesis |
|
517 using Case1 Osum_minus_Id[of r r'] assms Osum_wf[of "r - Id" "r' - Id"] |
|
518 wf_subset[of "(r - Id) \<union>o (r' - Id)" "(r Osum r') - Id"] by auto |
|
519 next |
|
520 have 1: "wf(Field r \<times> Field r')" |
|
521 using FLD by (auto simp add: wf_Int_Times) |
|
522 assume Case2: "r \<le> Id \<or> r' \<le> Id" |
|
523 moreover |
|
524 {assume Case21: "r \<le> Id" |
|
525 hence "(r Osum r') - Id \<le> (r' - Id) \<union> (Field r \<times> Field r')" |
|
526 using Osum_minus_Id1[of r r'] by simp |
|
527 moreover |
|
528 {have "Domain(Field r \<times> Field r') Int Range(r' - Id) = {}" |
|
529 using FLD unfolding Field_def by blast |
|
530 hence "wf((r' - Id) \<union> (Field r \<times> Field r'))" |
|
531 using 1 WF' wf_Un[of "Field r \<times> Field r'" "r' - Id"] |
|
532 by (auto simp add: Un_commute) |
|
533 } |
|
534 ultimately have ?thesis by (auto simp add: wf_subset) |
|
535 } |
|
536 moreover |
|
537 {assume Case22: "r' \<le> Id" |
|
538 hence "(r Osum r') - Id \<le> (r - Id) \<union> (Field r \<times> Field r')" |
|
539 using Osum_minus_Id2[of r' r] by simp |
|
540 moreover |
|
541 {have "Range(Field r \<times> Field r') Int Domain(r - Id) = {}" |
|
542 using FLD unfolding Field_def by blast |
|
543 hence "wf((r - Id) \<union> (Field r \<times> Field r'))" |
|
544 using 1 WF wf_Un[of "r - Id" "Field r \<times> Field r'"] |
|
545 by (auto simp add: Un_commute) |
|
546 } |
|
547 ultimately have ?thesis by (auto simp add: wf_subset) |
|
548 } |
|
549 ultimately show ?thesis by blast |
|
550 qed |
|
551 |
|
552 lemma Osum_Well_order: |
|
553 assumes FLD: "Field r Int Field r' = {}" and |
|
554 WELL: "Well_order r" and WELL': "Well_order r'" |
|
555 shows "Well_order (r Osum r')" |
|
556 proof- |
|
557 have "Total r \<and> Total r'" using WELL WELL' |
|
558 by (auto simp add: order_on_defs) |
|
559 thus ?thesis using assms unfolding well_order_on_def |
|
560 using Osum_Linear_order Osum_wf_Id by blast |
|
561 qed |
|
562 |
|
563 lemma Osum_embed: |
|
564 assumes FLD: "Field r Int Field r' = {}" and |
|
565 WELL: "Well_order r" and WELL': "Well_order r'" |
|
566 shows "embed r (r Osum r') id" |
|
567 proof- |
|
568 have 1: "Well_order (r Osum r')" |
|
569 using assms by (auto simp add: Osum_Well_order) |
|
570 moreover |
|
571 have "compat r (r Osum r') id" |
|
572 unfolding compat_def Osum_def by auto |
|
573 moreover |
|
574 have "inj_on id (Field r)" by simp |
|
575 moreover |
|
576 have "ofilter (r Osum r') (Field r)" |
|
577 using 1 proof(auto simp add: wo_rel_def wo_rel.ofilter_def |
|
578 Field_Osum rel.under_def) |
|
579 fix a b assume 2: "a \<in> Field r" and 3: "(b,a) \<in> r Osum r'" |
|
580 moreover |
|
581 {assume "(b,a) \<in> r'" |
|
582 hence "a \<in> Field r'" using Field_def[of r'] by blast |
|
583 hence False using 2 FLD by blast |
|
584 } |
|
585 moreover |
|
586 {assume "a \<in> Field r'" |
|
587 hence False using 2 FLD by blast |
|
588 } |
|
589 ultimately |
|
590 show "b \<in> Field r" by (auto simp add: Osum_def Field_def) |
|
591 qed |
|
592 ultimately show ?thesis |
|
593 using assms by (auto simp add: embed_iff_compat_inj_on_ofilter) |
|
594 qed |
|
595 |
|
596 corollary Osum_ordLeq: |
|
597 assumes FLD: "Field r Int Field r' = {}" and |
|
598 WELL: "Well_order r" and WELL': "Well_order r'" |
|
599 shows "r \<le>o r Osum r'" |
|
600 using assms Osum_embed Osum_Well_order |
|
601 unfolding ordLeq_def by blast |
|
602 |
|
603 lemma Well_order_embed_copy: |
|
604 assumes WELL: "well_order_on A r" and |
|
605 INJ: "inj_on f A" and SUB: "f ` A \<le> B" |
|
606 shows "\<exists>r'. well_order_on B r' \<and> r \<le>o r'" |
|
607 proof- |
|
608 have "bij_betw f A (f ` A)" |
|
609 using INJ inj_on_imp_bij_betw by blast |
|
610 then obtain r'' where "well_order_on (f ` A) r''" and 1: "r =o r''" |
|
611 using WELL Well_order_iso_copy by blast |
|
612 hence 2: "Well_order r'' \<and> Field r'' = (f ` A)" |
|
613 using rel.well_order_on_Well_order by blast |
|
614 (* *) |
|
615 let ?C = "B - (f ` A)" |
|
616 obtain r''' where "well_order_on ?C r'''" |
|
617 using well_order_on by blast |
|
618 hence 3: "Well_order r''' \<and> Field r''' = ?C" |
|
619 using rel.well_order_on_Well_order by blast |
|
620 (* *) |
|
621 let ?r' = "r'' Osum r'''" |
|
622 have "Field r'' Int Field r''' = {}" |
|
623 using 2 3 by auto |
|
624 hence "r'' \<le>o ?r'" using Osum_ordLeq[of r'' r'''] 2 3 by blast |
|
625 hence 4: "r \<le>o ?r'" using 1 ordIso_ordLeq_trans by blast |
|
626 (* *) |
|
627 hence "Well_order ?r'" unfolding ordLeq_def by auto |
|
628 moreover |
|
629 have "Field ?r' = B" using 2 3 SUB by (auto simp add: Field_Osum) |
|
630 ultimately show ?thesis using 4 by blast |
|
631 qed |
|
632 |
|
633 |
|
634 subsection {* The maxim among a finite set of ordinals *} |
|
635 |
|
636 text {* The correct phrasing would be ``a maxim of ...", as @{text "\<le>o"} is only a preorder. *} |
|
637 |
|
638 definition isOmax :: "'a rel set \<Rightarrow> 'a rel \<Rightarrow> bool" |
|
639 where |
|
640 "isOmax R r == r \<in> R \<and> (ALL r' : R. r' \<le>o r)" |
|
641 |
|
642 definition omax :: "'a rel set \<Rightarrow> 'a rel" |
|
643 where |
|
644 "omax R == SOME r. isOmax R r" |
|
645 |
|
646 lemma exists_isOmax: |
|
647 assumes "finite R" and "R \<noteq> {}" and "\<forall> r \<in> R. Well_order r" |
|
648 shows "\<exists> r. isOmax R r" |
|
649 proof- |
|
650 have "finite R \<Longrightarrow> R \<noteq> {} \<longrightarrow> (\<forall> r \<in> R. Well_order r) \<longrightarrow> (\<exists> r. isOmax R r)" |
|
651 apply(erule finite_induct) apply(simp add: isOmax_def) |
|
652 proof(clarsimp) |
|
653 fix r :: "('a \<times> 'a) set" and R assume *: "finite R" and **: "r \<notin> R" |
|
654 and ***: "Well_order r" and ****: "\<forall>r\<in>R. Well_order r" |
|
655 and IH: "R \<noteq> {} \<longrightarrow> (\<exists>p. isOmax R p)" |
|
656 let ?R' = "insert r R" |
|
657 show "\<exists>p'. (isOmax ?R' p')" |
|
658 proof(cases "R = {}") |
|
659 assume Case1: "R = {}" |
|
660 thus ?thesis unfolding isOmax_def using *** |
|
661 by (simp add: ordLeq_reflexive) |
|
662 next |
|
663 assume Case2: "R \<noteq> {}" |
|
664 then obtain p where p: "isOmax R p" using IH by auto |
|
665 hence 1: "Well_order p" using **** unfolding isOmax_def by simp |
|
666 {assume Case21: "r \<le>o p" |
|
667 hence "isOmax ?R' p" using p unfolding isOmax_def by simp |
|
668 hence ?thesis by auto |
|
669 } |
|
670 moreover |
|
671 {assume Case22: "p \<le>o r" |
|
672 {fix r' assume "r' \<in> ?R'" |
|
673 moreover |
|
674 {assume "r' \<in> R" |
|
675 hence "r' \<le>o p" using p unfolding isOmax_def by simp |
|
676 hence "r' \<le>o r" using Case22 by(rule ordLeq_transitive) |
|
677 } |
|
678 moreover have "r \<le>o r" using *** by(rule ordLeq_reflexive) |
|
679 ultimately have "r' \<le>o r" by auto |
|
680 } |
|
681 hence "isOmax ?R' r" unfolding isOmax_def by simp |
|
682 hence ?thesis by auto |
|
683 } |
|
684 moreover have "r \<le>o p \<or> p \<le>o r" |
|
685 using 1 *** ordLeq_total by auto |
|
686 ultimately show ?thesis by blast |
|
687 qed |
|
688 qed |
|
689 thus ?thesis using assms by auto |
|
690 qed |
|
691 |
|
692 lemma omax_isOmax: |
|
693 assumes "finite R" and "R \<noteq> {}" and "\<forall> r \<in> R. Well_order r" |
|
694 shows "isOmax R (omax R)" |
|
695 unfolding omax_def using assms |
|
696 by(simp add: exists_isOmax someI_ex) |
|
697 |
|
698 lemma omax_in: |
|
699 assumes "finite R" and "R \<noteq> {}" and "\<forall> r \<in> R. Well_order r" |
|
700 shows "omax R \<in> R" |
|
701 using assms omax_isOmax unfolding isOmax_def by blast |
|
702 |
|
703 lemma Well_order_omax: |
|
704 assumes "finite R" and "R \<noteq> {}" and "\<forall>r\<in>R. Well_order r" |
|
705 shows "Well_order (omax R)" |
|
706 using assms apply - apply(drule omax_in) by auto |
|
707 |
|
708 lemma omax_maxim: |
|
709 assumes "finite R" and "\<forall> r \<in> R. Well_order r" and "r \<in> R" |
|
710 shows "r \<le>o omax R" |
|
711 using assms omax_isOmax unfolding isOmax_def by blast |
|
712 |
|
713 lemma omax_ordLeq: |
|
714 assumes "finite R" and "R \<noteq> {}" and *: "\<forall> r \<in> R. r \<le>o p" |
|
715 shows "omax R \<le>o p" |
|
716 proof- |
|
717 have "\<forall> r \<in> R. Well_order r" using * unfolding ordLeq_def by simp |
|
718 thus ?thesis using assms omax_in by auto |
|
719 qed |
|
720 |
|
721 lemma omax_ordLess: |
|
722 assumes "finite R" and "R \<noteq> {}" and *: "\<forall> r \<in> R. r <o p" |
|
723 shows "omax R <o p" |
|
724 proof- |
|
725 have "\<forall> r \<in> R. Well_order r" using * unfolding ordLess_def by simp |
|
726 thus ?thesis using assms omax_in by auto |
|
727 qed |
|
728 |
|
729 lemma omax_ordLeq_elim: |
|
730 assumes "finite R" and "\<forall> r \<in> R. Well_order r" |
|
731 and "omax R \<le>o p" and "r \<in> R" |
|
732 shows "r \<le>o p" |
|
733 using assms omax_maxim[of R r] apply simp |
|
734 using ordLeq_transitive by blast |
|
735 |
|
736 lemma omax_ordLess_elim: |
|
737 assumes "finite R" and "\<forall> r \<in> R. Well_order r" |
|
738 and "omax R <o p" and "r \<in> R" |
|
739 shows "r <o p" |
|
740 using assms omax_maxim[of R r] apply simp |
|
741 using ordLeq_ordLess_trans by blast |
|
742 |
|
743 lemma ordLeq_omax: |
|
744 assumes "finite R" and "\<forall> r \<in> R. Well_order r" |
|
745 and "r \<in> R" and "p \<le>o r" |
|
746 shows "p \<le>o omax R" |
|
747 using assms omax_maxim[of R r] apply simp |
|
748 using ordLeq_transitive by blast |
|
749 |
|
750 lemma ordLess_omax: |
|
751 assumes "finite R" and "\<forall> r \<in> R. Well_order r" |
|
752 and "r \<in> R" and "p <o r" |
|
753 shows "p <o omax R" |
|
754 using assms omax_maxim[of R r] apply simp |
|
755 using ordLess_ordLeq_trans by blast |
|
756 |
|
757 lemma omax_ordLeq_mono: |
|
758 assumes P: "finite P" and R: "finite R" |
|
759 and NE_P: "P \<noteq> {}" and Well_R: "\<forall> r \<in> R. Well_order r" |
|
760 and LEQ: "\<forall> p \<in> P. \<exists> r \<in> R. p \<le>o r" |
|
761 shows "omax P \<le>o omax R" |
|
762 proof- |
|
763 let ?mp = "omax P" let ?mr = "omax R" |
|
764 {fix p assume "p : P" |
|
765 then obtain r where r: "r : R" and "p \<le>o r" |
|
766 using LEQ by blast |
|
767 moreover have "r <=o ?mr" |
|
768 using r R Well_R omax_maxim by blast |
|
769 ultimately have "p <=o ?mr" |
|
770 using ordLeq_transitive by blast |
|
771 } |
|
772 thus "?mp <=o ?mr" |
|
773 using NE_P P using omax_ordLeq by blast |
|
774 qed |
|
775 |
|
776 lemma omax_ordLess_mono: |
|
777 assumes P: "finite P" and R: "finite R" |
|
778 and NE_P: "P \<noteq> {}" and Well_R: "\<forall> r \<in> R. Well_order r" |
|
779 and LEQ: "\<forall> p \<in> P. \<exists> r \<in> R. p <o r" |
|
780 shows "omax P <o omax R" |
|
781 proof- |
|
782 let ?mp = "omax P" let ?mr = "omax R" |
|
783 {fix p assume "p : P" |
|
784 then obtain r where r: "r : R" and "p <o r" |
|
785 using LEQ by blast |
|
786 moreover have "r <=o ?mr" |
|
787 using r R Well_R omax_maxim by blast |
|
788 ultimately have "p <o ?mr" |
|
789 using ordLess_ordLeq_trans by blast |
|
790 } |
|
791 thus "?mp <o ?mr" |
|
792 using NE_P P omax_ordLess by blast |
|
793 qed |
|
794 |
|
795 end |
|