141 |
141 |
142 text{*NB: We assume the partial ordering is @{text "\<subseteq>"}, |
142 text{*NB: We assume the partial ordering is @{text "\<subseteq>"}, |
143 the subset relation!*} |
143 the subset relation!*} |
144 |
144 |
145 lemma empty_set_mem_chain: "({} :: 'a set set) \<in> chain S" |
145 lemma empty_set_mem_chain: "({} :: 'a set set) \<in> chain S" |
146 by (unfold chain_def chain_subset_def) auto |
146 by (unfold chain_def chain_subset_def) simp |
147 |
147 |
148 lemma super_subset_chain: "super S c \<subseteq> chain S" |
148 lemma super_subset_chain: "super S c \<subseteq> chain S" |
149 by (unfold super_def) blast |
149 by (unfold super_def) blast |
150 |
150 |
151 lemma maxchain_subset_chain: "maxchain S \<subseteq> chain S" |
151 lemma maxchain_subset_chain: "maxchain S \<subseteq> chain S" |
152 by (unfold maxchain_def) blast |
152 by (unfold maxchain_def) blast |
153 |
153 |
154 lemma mem_super_Ex: "c \<in> chain S - maxchain S ==> EX d. d \<in> super S c" |
154 lemma mem_super_Ex: "c \<in> chain S - maxchain S ==> EX d. d \<in> super S c" |
155 by (unfold super_def maxchain_def) auto |
155 by (unfold super_def maxchain_def) simp |
156 |
156 |
157 lemma select_super: |
157 lemma select_super: |
158 "c \<in> chain S - maxchain S ==> (\<some>c'. c': super S c): super S c" |
158 "c \<in> chain S - maxchain S ==> (\<some>c'. c': super S c): super S c" |
159 apply (erule mem_super_Ex [THEN exE]) |
159 apply (erule mem_super_Ex [THEN exE]) |
160 apply (rule someI2) |
160 apply (rule someI2) |
161 apply auto |
161 apply simp+ |
162 done |
162 done |
163 |
163 |
164 lemma select_not_equals: |
164 lemma select_not_equals: |
165 "c \<in> chain S - maxchain S ==> (\<some>c'. c': super S c) \<noteq> c" |
165 "c \<in> chain S - maxchain S ==> (\<some>c'. c': super S c) \<noteq> c" |
166 apply (rule notI) |
166 apply (rule notI) |
284 have "C = ?B ` ?A" using 1 by(auto simp: image_def) |
284 have "C = ?B ` ?A" using 1 by(auto simp: image_def) |
285 have "?A\<in>Chain r" |
285 have "?A\<in>Chain r" |
286 proof (simp add:Chain_def, intro allI impI, elim conjE) |
286 proof (simp add:Chain_def, intro allI impI, elim conjE) |
287 fix a b |
287 fix a b |
288 assume "a \<in> Field r" "?B a \<in> C" "b \<in> Field r" "?B b \<in> C" |
288 assume "a \<in> Field r" "?B a \<in> C" "b \<in> Field r" "?B b \<in> C" |
289 hence "?B a \<subseteq> ?B b \<or> ?B b \<subseteq> ?B a" using 2 by auto |
289 hence "?B a \<subseteq> ?B b \<or> ?B b \<subseteq> ?B a" using 2 by simp |
290 thus "(a, b) \<in> r \<or> (b, a) \<in> r" using `Preorder r` `a:Field r` `b:Field r` |
290 thus "(a, b) \<in> r \<or> (b, a) \<in> r" using `Preorder r` `a:Field r` `b:Field r` |
291 by (simp add:subset_Image1_Image1_iff) |
291 by (simp add:subset_Image1_Image1_iff) |
292 qed |
292 qed |
293 then obtain u where uA: "u:Field r" "\<forall>a\<in>?A. (a,u) : r" using u by auto |
293 then obtain u where uA: "u:Field r" "\<forall>a\<in>?A. (a,u) : r" using u by auto |
294 have "\<forall>A\<in>C. A \<subseteq> r^-1 `` {u}" (is "?P u") |
294 have "\<forall>A\<in>C. A \<subseteq> r^-1 `` {u}" (is "?P u") |
295 proof auto |
295 proof auto |
296 fix a B assume aB: "B:C" "a:B" |
296 fix a B assume aB: "B:C" "a:B" |
297 with 1 obtain x where "x:Field r" "B = r^-1 `` {x}" by auto |
297 with 1 obtain x where "x:Field r" "B = r^-1 `` {x}" by auto |
298 thus "(a,u) : r" using uA aB `Preorder r` |
298 thus "(a,u) : r" using uA aB `Preorder r` |
299 by (auto simp add: preorder_on_def refl_on_def) (metis transD) |
299 by (simp add: preorder_on_def refl_on_def) (rule transD, blast+) |
300 qed |
300 qed |
301 thus "EX u:Field r. ?P u" using `u:Field r` by blast |
301 thus "EX u:Field r. ?P u" using `u:Field r` by blast |
302 qed |
302 qed |
303 from Zorn_Lemma2[OF this] |
303 from Zorn_Lemma2[OF this] |
304 obtain m B where "m:Field r" "B = r^-1 `` {m}" |
304 obtain m B where "m:Field r" "B = r^-1 `` {m}" |
324 lemma refl_on_init_seg_of[simp]: "r initial_segment_of r" |
324 lemma refl_on_init_seg_of[simp]: "r initial_segment_of r" |
325 by(simp add:init_seg_of_def) |
325 by(simp add:init_seg_of_def) |
326 |
326 |
327 lemma trans_init_seg_of: |
327 lemma trans_init_seg_of: |
328 "r initial_segment_of s \<Longrightarrow> s initial_segment_of t \<Longrightarrow> r initial_segment_of t" |
328 "r initial_segment_of s \<Longrightarrow> s initial_segment_of t \<Longrightarrow> r initial_segment_of t" |
329 by(simp (no_asm_use) add: init_seg_of_def) |
329 by (simp (no_asm_use) add: init_seg_of_def) (metis (no_types) in_mono order_trans) |
330 (metis Domain_iff UnCI Un_absorb2 subset_trans) |
|
331 |
330 |
332 lemma antisym_init_seg_of: |
331 lemma antisym_init_seg_of: |
333 "r initial_segment_of s \<Longrightarrow> s initial_segment_of r \<Longrightarrow> r=s" |
332 "r initial_segment_of s \<Longrightarrow> s initial_segment_of r \<Longrightarrow> r=s" |
334 unfolding init_seg_of_def by safe |
333 unfolding init_seg_of_def by safe |
335 |
334 |
336 lemma Chain_init_seg_of_Union: |
335 lemma Chain_init_seg_of_Union: |
337 "R \<in> Chain init_seg_of \<Longrightarrow> r\<in>R \<Longrightarrow> r initial_segment_of \<Union>R" |
336 "R \<in> Chain init_seg_of \<Longrightarrow> r\<in>R \<Longrightarrow> r initial_segment_of \<Union>R" |
338 by(auto simp add:init_seg_of_def Chain_def Ball_def) blast |
337 by(simp add: init_seg_of_def Chain_def Ball_def) blast |
339 |
338 |
340 lemma chain_subset_trans_Union: |
339 lemma chain_subset_trans_Union: |
341 "chain\<^bsub>\<subseteq>\<^esub> R \<Longrightarrow> \<forall>r\<in>R. trans r \<Longrightarrow> trans(\<Union>R)" |
340 "chain\<^bsub>\<subseteq>\<^esub> R \<Longrightarrow> \<forall>r\<in>R. trans r \<Longrightarrow> trans(\<Union>R)" |
342 apply(auto simp add:chain_subset_def) |
341 apply(simp add:chain_subset_def) |
343 apply(simp (no_asm_use) add:trans_def) |
342 apply(simp (no_asm_use) add:trans_def) |
344 apply (metis subsetD) |
343 by (metis subsetD) |
345 done |
|
346 |
344 |
347 lemma chain_subset_antisym_Union: |
345 lemma chain_subset_antisym_Union: |
348 "chain\<^bsub>\<subseteq>\<^esub> R \<Longrightarrow> \<forall>r\<in>R. antisym r \<Longrightarrow> antisym(\<Union>R)" |
346 "chain\<^bsub>\<subseteq>\<^esub> R \<Longrightarrow> \<forall>r\<in>R. antisym r \<Longrightarrow> antisym(\<Union>R)" |
349 apply(auto simp add:chain_subset_def antisym_def) |
347 by (simp add:chain_subset_def antisym_def) (metis subsetD) |
350 apply (metis subsetD) |
|
351 done |
|
352 |
348 |
353 lemma chain_subset_Total_Union: |
349 lemma chain_subset_Total_Union: |
354 assumes "chain\<^bsub>\<subseteq>\<^esub> R" "\<forall>r\<in>R. Total r" |
350 assumes "chain\<^bsub>\<subseteq>\<^esub> R" "\<forall>r\<in>R. Total r" |
355 shows "Total (\<Union>R)" |
351 shows "Total (\<Union>R)" |
356 proof (simp add: total_on_def Ball_def, auto del:disjCI) |
352 proof (simp add: total_on_def Ball_def, auto del:disjCI) |
401 theorem well_ordering: "\<exists>r::('a*'a)set. Well_order r \<and> Field r = UNIV" |
397 theorem well_ordering: "\<exists>r::('a*'a)set. Well_order r \<and> Field r = UNIV" |
402 proof- |
398 proof- |
403 -- {*The initial segment relation on well-orders: *} |
399 -- {*The initial segment relation on well-orders: *} |
404 let ?WO = "{r::('a*'a)set. Well_order r}" |
400 let ?WO = "{r::('a*'a)set. Well_order r}" |
405 def I \<equiv> "init_seg_of \<inter> ?WO \<times> ?WO" |
401 def I \<equiv> "init_seg_of \<inter> ?WO \<times> ?WO" |
406 have I_init: "I \<subseteq> init_seg_of" by(auto simp:I_def) |
402 have I_init: "I \<subseteq> init_seg_of" by(simp add: I_def) |
407 hence subch: "!!R. R : Chain I \<Longrightarrow> chain\<^bsub>\<subseteq>\<^esub> R" |
403 hence subch: "!!R. R : Chain I \<Longrightarrow> chain\<^bsub>\<subseteq>\<^esub> R" |
408 by(auto simp:init_seg_of_def chain_subset_def Chain_def) |
404 by(auto simp:init_seg_of_def chain_subset_def Chain_def) |
409 have Chain_wo: "!!R r. R \<in> Chain I \<Longrightarrow> r \<in> R \<Longrightarrow> Well_order r" |
405 have Chain_wo: "!!R r. R \<in> Chain I \<Longrightarrow> r \<in> R \<Longrightarrow> Well_order r" |
410 by(simp add:Chain_def I_def) blast |
406 by(simp add:Chain_def I_def) blast |
411 have FI: "Field I = ?WO" by(auto simp add:I_def init_seg_of_def Field_def) |
407 have FI: "Field I = ?WO" by(auto simp add:I_def init_seg_of_def Field_def) |
435 ultimately have "Well_order (\<Union>R)" by(simp add:order_on_defs) |
431 ultimately have "Well_order (\<Union>R)" by(simp add:order_on_defs) |
436 moreover have "\<forall>r \<in> R. r initial_segment_of \<Union>R" using Ris |
432 moreover have "\<forall>r \<in> R. r initial_segment_of \<Union>R" using Ris |
437 by(simp add: Chain_init_seg_of_Union) |
433 by(simp add: Chain_init_seg_of_Union) |
438 ultimately have "\<Union>R : ?WO \<and> (\<forall>r\<in>R. (r,\<Union>R) : I)" |
434 ultimately have "\<Union>R : ?WO \<and> (\<forall>r\<in>R. (r,\<Union>R) : I)" |
439 using mono_Chain[OF I_init] `R \<in> Chain I` |
435 using mono_Chain[OF I_init] `R \<in> Chain I` |
440 by(simp (no_asm) add:I_def del:Field_Union)(metis Chain_wo subsetD) |
436 by(simp (no_asm) add:I_def del:Field_Union)(metis Chain_wo) |
441 } |
437 } |
442 hence 1: "\<forall>R \<in> Chain I. \<exists>u\<in>Field I. \<forall>r\<in>R. (r,u) : I" by (subst FI) blast |
438 hence 1: "\<forall>R \<in> Chain I. \<exists>u\<in>Field I. \<forall>r\<in>R. (r,u) : I" by (subst FI) blast |
443 --{*Zorn's Lemma yields a maximal well-order m:*} |
439 --{*Zorn's Lemma yields a maximal well-order m:*} |
444 then obtain m::"('a*'a)set" where "Well_order m" and |
440 then obtain m::"('a*'a)set" where "Well_order m" and |
445 max: "\<forall>r. Well_order r \<and> (m,r):I \<longrightarrow> r=m" |
441 max: "\<forall>r. Well_order r \<and> (m,r):I \<longrightarrow> r=m" |
473 unfolding antisym_def Field_def Domain_unfold Domain_converse [symmetric] by blast |
469 unfolding antisym_def Field_def Domain_unfold Domain_converse [symmetric] by blast |
474 moreover have "Total ?m" using `Total m` Fm by(auto simp: total_on_def) |
470 moreover have "Total ?m" using `Total m` Fm by(auto simp: total_on_def) |
475 moreover have "wf(?m-Id)" |
471 moreover have "wf(?m-Id)" |
476 proof- |
472 proof- |
477 have "wf ?s" using `x \<notin> Field m` |
473 have "wf ?s" using `x \<notin> Field m` |
478 by(auto simp add:wf_eq_minimal Field_def Domain_unfold Domain_converse [symmetric]) metis |
474 by(simp add:wf_eq_minimal Field_def Domain_unfold Domain_converse [symmetric]) metis |
479 thus ?thesis using `wf(m-Id)` `x \<notin> Field m` |
475 thus ?thesis using `wf(m-Id)` `x \<notin> Field m` |
480 wf_subset[OF `wf ?s` Diff_subset] |
476 wf_subset[OF `wf ?s` Diff_subset] |
481 by (fastforce intro!: wf_Un simp add: Un_Diff Field_def) |
477 by (fastforce intro!: wf_Un simp add: Un_Diff Field_def) |
482 qed |
478 qed |
483 ultimately have "Well_order ?m" by(simp add:order_on_defs) |
479 ultimately have "Well_order ?m" by(simp add:order_on_defs) |