equal
deleted
inserted
replaced
489 lemma chainsD2: "c \<in> chains S \<Longrightarrow> c \<subseteq> S" |
489 lemma chainsD2: "c \<in> chains S \<Longrightarrow> c \<subseteq> S" |
490 unfolding chains_def by blast |
490 unfolding chains_def by blast |
491 |
491 |
492 lemma Zorns_po_lemma: |
492 lemma Zorns_po_lemma: |
493 assumes po: "Partial_order r" |
493 assumes po: "Partial_order r" |
494 and u: "\<forall>C\<in>Chains r. \<exists>u\<in>Field r. \<forall>a\<in>C. (a, u) \<in> r" |
494 and u: "\<And>C. C \<in> Chains r \<Longrightarrow> \<exists>u\<in>Field r. \<forall>a\<in>C. (a, u) \<in> r" |
495 shows "\<exists>m\<in>Field r. \<forall>a\<in>Field r. (m, a) \<in> r \<longrightarrow> a = m" |
495 shows "\<exists>m\<in>Field r. \<forall>a\<in>Field r. (m, a) \<in> r \<longrightarrow> a = m" |
496 proof - |
496 proof - |
497 have "Preorder r" |
497 have "Preorder r" |
498 using po by (simp add: partial_order_on_def) |
498 using po by (simp add: partial_order_on_def) |
499 txt \<open>Mirror \<open>r\<close> in the set of subsets below (wrt \<open>r\<close>) elements of \<open>A\<close>.\<close> |
499 txt \<open>Mirror \<open>r\<close> in the set of subsets below (wrt \<open>r\<close>) elements of \<open>A\<close>.\<close> |
511 with 2 have "?B a \<subseteq> ?B b \<or> ?B b \<subseteq> ?B a" by auto |
511 with 2 have "?B a \<subseteq> ?B b \<or> ?B b \<subseteq> ?B a" by auto |
512 then show "(a, b) \<in> r \<or> (b, a) \<in> r" |
512 then show "(a, b) \<in> r \<or> (b, a) \<in> r" |
513 using \<open>Preorder r\<close> and \<open>a \<in> Field r\<close> and \<open>b \<in> Field r\<close> |
513 using \<open>Preorder r\<close> and \<open>a \<in> Field r\<close> and \<open>b \<in> Field r\<close> |
514 by (simp add:subset_Image1_Image1_iff) |
514 by (simp add:subset_Image1_Image1_iff) |
515 qed |
515 qed |
516 with u obtain u where uA: "u \<in> Field r" "\<forall>a\<in>?A. (a, u) \<in> r" by auto |
516 then obtain u where uA: "u \<in> Field r" "\<forall>a\<in>?A. (a, u) \<in> r" |
|
517 by (auto simp: dest: u) |
517 have "?P u" |
518 have "?P u" |
518 proof auto |
519 proof auto |
519 fix a B assume aB: "B \<in> C" "a \<in> B" |
520 fix a B assume aB: "B \<in> C" "a \<in> B" |
520 with 1 obtain x where "x \<in> Field r" and "B = r\<inverse> `` {x}" by auto |
521 with 1 obtain x where "x \<in> Field r" and "B = r\<inverse> `` {x}" by auto |
521 then show "(a, u) \<in> r" |
522 then show "(a, u) \<in> r" |
535 then have "\<forall>a\<in>Field r. (m, a) \<in> r \<longrightarrow> a = m" |
536 then have "\<forall>a\<in>Field r. (m, a) \<in> r \<longrightarrow> a = m" |
536 using po and \<open>Preorder r\<close> and \<open>m \<in> Field r\<close> |
537 using po and \<open>Preorder r\<close> and \<open>m \<in> Field r\<close> |
537 by (auto simp: subset_Image1_Image1_iff Partial_order_eq_Image1_Image1_iff) |
538 by (auto simp: subset_Image1_Image1_iff Partial_order_eq_Image1_Image1_iff) |
538 then show ?thesis |
539 then show ?thesis |
539 using \<open>m \<in> Field r\<close> by blast |
540 using \<open>m \<in> Field r\<close> by blast |
|
541 qed |
|
542 |
|
543 lemma predicate_Zorn: |
|
544 assumes po: "partial_order_on A (relation_of P A)" |
|
545 and ch: "\<And>C. C \<in> Chains (relation_of P A) \<Longrightarrow> \<exists>u \<in> A. \<forall>a \<in> C. P a u" |
|
546 shows "\<exists>m \<in> A. \<forall>a \<in> A. P m a \<longrightarrow> a = m" |
|
547 proof - |
|
548 have "a \<in> A" if "C \<in> Chains (relation_of P A)" and "a \<in> C" for C a |
|
549 using that unfolding Chains_def relation_of_def by auto |
|
550 moreover have "(a, u) \<in> relation_of P A" if "a \<in> A" and "u \<in> A" and "P a u" for a u |
|
551 unfolding relation_of_def using that by auto |
|
552 ultimately have "\<exists>m\<in>A. \<forall>a\<in>A. (m, a) \<in> relation_of P A \<longrightarrow> a = m" |
|
553 using Zorns_po_lemma[OF Partial_order_relation_ofI[OF po], rule_format] ch |
|
554 unfolding Field_relation_of[OF partial_order_onD(1)[OF po]] by blast |
|
555 then show ?thesis |
|
556 by (auto simp: relation_of_def) |
540 qed |
557 qed |
541 |
558 |
542 |
559 |
543 subsection \<open>The Well Ordering Theorem\<close> |
560 subsection \<open>The Well Ordering Theorem\<close> |
544 |
561 |
699 using Ris by (simp add: Chains_init_seg_of_Union) |
716 using Ris by (simp add: Chains_init_seg_of_Union) |
700 ultimately show ?thesis |
717 ultimately show ?thesis |
701 using mono_Chains [OF I_init] Chains_wo[of R] and \<open>R \<in> Chains I\<close> |
718 using mono_Chains [OF I_init] Chains_wo[of R] and \<open>R \<in> Chains I\<close> |
702 unfolding I_def by blast |
719 unfolding I_def by blast |
703 qed |
720 qed |
704 then have 1: "\<forall>R \<in> Chains I. \<exists>u\<in>Field I. \<forall>r\<in>R. (r, u) \<in> I" |
721 then have 1: "\<exists>u\<in>Field I. \<forall>r\<in>R. (r, u) \<in> I" if "R \<in> Chains I" for R |
705 by (subst FI) blast |
722 using that by (subst FI) blast |
706 \<comment> \<open>Zorn's Lemma yields a maximal well-order \<open>m\<close>:\<close> |
723 \<comment> \<open>Zorn's Lemma yields a maximal well-order \<open>m\<close>:\<close> |
707 then obtain m :: "'a rel" |
724 then obtain m :: "'a rel" |
708 where "Well_order m" |
725 where "Well_order m" |
709 and max: "\<forall>r. Well_order r \<and> (m, r) \<in> I \<longrightarrow> r = m" |
726 and max: "\<forall>r. Well_order r \<and> (m, r) \<in> I \<longrightarrow> r = m" |
710 using Zorns_po_lemma[OF 0 1] unfolding FI by fastforce |
727 using Zorns_po_lemma[OF 0 1] unfolding FI by fastforce |