(* Title: HOL/Zorn.thy Author: Jacques D. Fleuriot Author: Tobias Nipkow, TUM Author: Christian Sternagel, JAIST Zorn's Lemma (ported from Larry Paulson's Zorn.thy in ZF). The well-ordering theorem. *) section ‹Zorn's Lemma› theory Zorn imports Order_Relation Hilbert_Choice begin subsection ‹Zorn's Lemma for the Subset Relation› subsubsection ‹Results that do not require an order› text ‹Let ‹P› be a binary predicate on the set ‹A›.› locale pred_on = fixes A :: "'a set" and P :: "'a ⇒ 'a ⇒ bool" (infix "⊏" 50) begin abbreviation Peq :: "'a ⇒ 'a ⇒ bool" (infix "⊑" 50) where "x ⊑ y ≡ P⇧^{=}⇧^{=}x y" text ‹A chain is a totally ordered subset of ‹A›.› definition chain :: "'a set ⇒ bool" where "chain C ⟷ C ⊆ A ∧ (∀x∈C. ∀y∈C. x ⊑ y ∨ y ⊑ x)" text ‹ We call a chain that is a proper superset of some set ‹X›, but not necessarily a chain itself, a superchain of ‹X›. › abbreviation superchain :: "'a set ⇒ 'a set ⇒ bool" (infix "<c" 50) where "X <c C ≡ chain C ∧ X ⊂ C" text ‹A maximal chain is a chain that does not have a superchain.› definition maxchain :: "'a set ⇒ bool" where "maxchain C ⟷ chain C ∧ (∄S. C <c S)" text ‹ We define the successor of a set to be an arbitrary superchain, if such exists, or the set itself, otherwise. › definition suc :: "'a set ⇒ 'a set" where "suc C = (if ¬ chain C ∨ maxchain C then C else (SOME D. C <c D))" lemma chainI [Pure.intro?]: "C ⊆ A ⟹ (⋀x y. x ∈ C ⟹ y ∈ C ⟹ x ⊑ y ∨ y ⊑ x) ⟹ chain C" unfolding chain_def by blast lemma chain_total: "chain C ⟹ x ∈ C ⟹ y ∈ C ⟹ x ⊑ y ∨ y ⊑ x" by (simp add: chain_def) lemma not_chain_suc [simp]: "¬ chain X ⟹ suc X = X" by (simp add: suc_def) lemma maxchain_suc [simp]: "maxchain X ⟹ suc X = X" by (simp add: suc_def) lemma suc_subset: "X ⊆ suc X" by (auto simp: suc_def maxchain_def intro: someI2) lemma chain_empty [simp]: "chain {}" by (auto simp: chain_def) lemma not_maxchain_Some: "chain C ⟹ ¬ maxchain C ⟹ C <c (SOME D. C <c D)" by (rule someI_ex) (auto simp: maxchain_def) lemma suc_not_equals: "chain C ⟹ ¬ maxchain C ⟹ suc C ≠ C" using not_maxchain_Some by (auto simp: suc_def) lemma subset_suc: assumes "X ⊆ Y" shows "X ⊆ suc Y" using assms by (rule subset_trans) (rule suc_subset) text ‹ We build a set @{term 𝒞} that is closed under applications of @{term suc} and contains the union of all its subsets. › inductive_set suc_Union_closed ("𝒞") where suc: "X ∈ 𝒞 ⟹ suc X ∈ 𝒞" | Union [unfolded Pow_iff]: "X ∈ Pow 𝒞 ⟹ ⋃X ∈ 𝒞" text ‹ Since the empty set as well as the set itself is a subset of every set, @{term 𝒞} contains at least @{term "{} ∈ 𝒞"} and @{term "⋃𝒞 ∈ 𝒞"}. › lemma suc_Union_closed_empty: "{} ∈ 𝒞" and suc_Union_closed_Union: "⋃𝒞 ∈ 𝒞" using Union [of "{}"] and Union [of "𝒞"] by simp_all text ‹Thus closure under @{term suc} will hit a maximal chain eventually, as is shown below.› lemma suc_Union_closed_induct [consumes 1, case_names suc Union, induct pred: suc_Union_closed]: assumes "X ∈ 𝒞" and "⋀X. X ∈ 𝒞 ⟹ Q X ⟹ Q (suc X)" and "⋀X. X ⊆ 𝒞 ⟹ ∀x∈X. Q x ⟹ Q (⋃X)" shows "Q X" using assms by induct blast+ lemma suc_Union_closed_cases [consumes 1, case_names suc Union, cases pred: suc_Union_closed]: assumes "X ∈ 𝒞" and "⋀Y. X = suc Y ⟹ Y ∈ 𝒞 ⟹ Q" and "⋀Y. X = ⋃Y ⟹ Y ⊆ 𝒞 ⟹ Q" shows "Q" using assms by cases simp_all text ‹On chains, @{term suc} yields a chain.› lemma chain_suc: assumes "chain X" shows "chain (suc X)" using assms by (cases "¬ chain X ∨ maxchain X") (force simp: suc_def dest: not_maxchain_Some)+ lemma chain_sucD: assumes "chain X" shows "suc X ⊆ A ∧ chain (suc X)" proof - from ‹chain X› have *: "chain (suc X)" by (rule chain_suc) then have "suc X ⊆ A" unfolding chain_def by blast with * show ?thesis by blast qed lemma suc_Union_closed_total': assumes "X ∈ 𝒞" and "Y ∈ 𝒞" and *: "⋀Z. Z ∈ 𝒞 ⟹ Z ⊆ Y ⟹ Z = Y ∨ suc Z ⊆ Y" shows "X ⊆ Y ∨ suc Y ⊆ X" using ‹X ∈ 𝒞› proof induct case (suc X) with * show ?case by (blast del: subsetI intro: subset_suc) next case Union then show ?case by blast qed lemma suc_Union_closed_subsetD: assumes "Y ⊆ X" and "X ∈ 𝒞" and "Y ∈ 𝒞" shows "X = Y ∨ suc Y ⊆ X" using assms(2,3,1) proof (induct arbitrary: Y) case (suc X) note * = ‹⋀Y. Y ∈ 𝒞 ⟹ Y ⊆ X ⟹ X = Y ∨ suc Y ⊆ X› with suc_Union_closed_total' [OF ‹Y ∈ 𝒞› ‹X ∈ 𝒞›] have "Y ⊆ X ∨ suc X ⊆ Y" by blast then show ?case proof assume "Y ⊆ X" with * and ‹Y ∈ 𝒞› have "X = Y ∨ suc Y ⊆ X" by blast then show ?thesis proof assume "X = Y" then show ?thesis by simp next assume "suc Y ⊆ X" then have "suc Y ⊆ suc X" by (rule subset_suc) then show ?thesis by simp qed next assume "suc X ⊆ Y" with ‹Y ⊆ suc X› show ?thesis by blast qed next case (Union X) show ?case proof (rule ccontr) assume "¬ ?thesis" with ‹Y ⊆ ⋃X› obtain x y z where "¬ suc Y ⊆ ⋃X" and "x ∈ X" and "y ∈ x" and "y ∉ Y" and "z ∈ suc Y" and "∀x∈X. z ∉ x" by blast with ‹X ⊆ 𝒞› have "x ∈ 𝒞" by blast from Union and ‹x ∈ X› have *: "⋀y. y ∈ 𝒞 ⟹ y ⊆ x ⟹ x = y ∨ suc y ⊆ x" by blast with suc_Union_closed_total' [OF ‹Y ∈ 𝒞› ‹x ∈ 𝒞›] have "Y ⊆ x ∨ suc x ⊆ Y" by blast then show False proof assume "Y ⊆ x" with * [OF ‹Y ∈ 𝒞›] have "x = Y ∨ suc Y ⊆ x" by blast then show False proof assume "x = Y" with ‹y ∈ x› and ‹y ∉ Y› show False by blast next assume "suc Y ⊆ x" with ‹x ∈ X› have "suc Y ⊆ ⋃X" by blast with ‹¬ suc Y ⊆ ⋃X› show False by contradiction qed next assume "suc x ⊆ Y" moreover from suc_subset and ‹y ∈ x› have "y ∈ suc x" by blast ultimately show False using ‹y ∉ Y› by blast qed qed qed text ‹The elements of @{term 𝒞} are totally ordered by the subset relation.› lemma suc_Union_closed_total: assumes "X ∈ 𝒞" and "Y ∈ 𝒞" shows "X ⊆ Y ∨ Y ⊆ X" proof (cases "∀Z∈𝒞. Z ⊆ Y ⟶ Z = Y ∨ suc Z ⊆ Y") case True with suc_Union_closed_total' [OF assms] have "X ⊆ Y ∨ suc Y ⊆ X" by blast with suc_subset [of Y] show ?thesis by blast next case False then obtain Z where "Z ∈ 𝒞" and "Z ⊆ Y" and "Z ≠ Y" and "¬ suc Z ⊆ Y" by blast with suc_Union_closed_subsetD and ‹Y ∈ 𝒞› show ?thesis by blast qed text ‹Once we hit a fixed point w.r.t. @{term suc}, all other elements of @{term 𝒞} are subsets of this fixed point.› lemma suc_Union_closed_suc: assumes "X ∈ 𝒞" and "Y ∈ 𝒞" and "suc Y = Y" shows "X ⊆ Y" using ‹X ∈ 𝒞› proof induct case (suc X) with ‹Y ∈ 𝒞› and suc_Union_closed_subsetD have "X = Y ∨ suc X ⊆ Y" by blast then show ?case by (auto simp: ‹suc Y = Y›) next case Union then show ?case by blast qed lemma eq_suc_Union: assumes "X ∈ 𝒞" shows "suc X = X ⟷ X = ⋃𝒞" (is "?lhs ⟷ ?rhs") proof assume ?lhs then have "⋃𝒞 ⊆ X" by (rule suc_Union_closed_suc [OF suc_Union_closed_Union ‹X ∈ 𝒞›]) with ‹X ∈ 𝒞› show ?rhs by blast next from ‹X ∈ 𝒞› have "suc X ∈ 𝒞" by (rule suc) then have "suc X ⊆ ⋃𝒞" by blast moreover assume ?rhs ultimately have "suc X ⊆ X" by simp moreover have "X ⊆ suc X" by (rule suc_subset) ultimately show ?lhs .. qed lemma suc_in_carrier: assumes "X ⊆ A" shows "suc X ⊆ A" using assms by (cases "¬ chain X ∨ maxchain X") (auto dest: chain_sucD) lemma suc_Union_closed_in_carrier: assumes "X ∈ 𝒞" shows "X ⊆ A" using assms by induct (auto dest: suc_in_carrier) text ‹All elements of @{term 𝒞} are chains.› lemma suc_Union_closed_chain: assumes "X ∈ 𝒞" shows "chain X" using assms proof induct case (suc X) then show ?case using not_maxchain_Some by (simp add: suc_def) next case (Union X) then have "⋃X ⊆ A" by (auto dest: suc_Union_closed_in_carrier) moreover have "∀x∈⋃X. ∀y∈⋃X. x ⊑ y ∨ y ⊑ x" proof (intro ballI) fix x y assume "x ∈ ⋃X" and "y ∈ ⋃X" then obtain u v where "x ∈ u" and "u ∈ X" and "y ∈ v" and "v ∈ X" by blast with Union have "u ∈ 𝒞" and "v ∈ 𝒞" and "chain u" and "chain v" by blast+ with suc_Union_closed_total have "u ⊆ v ∨ v ⊆ u" by blast then show "x ⊑ y ∨ y ⊑ x" proof assume "u ⊆ v" from ‹chain v› show ?thesis proof (rule chain_total) show "y ∈ v" by fact show "x ∈ v" using ‹u ⊆ v› and ‹x ∈ u› by blast qed next assume "v ⊆ u" from ‹chain u› show ?thesis proof (rule chain_total) show "x ∈ u" by fact show "y ∈ u" using ‹v ⊆ u› and ‹y ∈ v› by blast qed qed qed ultimately show ?case unfolding chain_def .. qed subsubsection ‹Hausdorff's Maximum Principle› text ‹There exists a maximal totally ordered subset of ‹A›. (Note that we do not require ‹A› to be partially ordered.)› theorem Hausdorff: "∃C. maxchain C" proof - let ?M = "⋃𝒞" have "maxchain ?M" proof (rule ccontr) assume "¬ ?thesis" then have "suc ?M ≠ ?M" using suc_not_equals and suc_Union_closed_chain [OF suc_Union_closed_Union] by simp moreover have "suc ?M = ?M" using eq_suc_Union [OF suc_Union_closed_Union] by simp ultimately show False by contradiction qed then show ?thesis by blast qed text ‹Make notation @{term 𝒞} available again.› no_notation suc_Union_closed ("𝒞") lemma chain_extend: "chain C ⟹ z ∈ A ⟹ ∀x∈C. x ⊑ z ⟹ chain ({z} ∪ C)" unfolding chain_def by blast lemma maxchain_imp_chain: "maxchain C ⟹ chain C" by (simp add: maxchain_def) end text ‹Hide constant @{const pred_on.suc_Union_closed}, which was just needed for the proof of Hausforff's maximum principle.› hide_const pred_on.suc_Union_closed lemma chain_mono: assumes "⋀x y. x ∈ A ⟹ y ∈ A ⟹ P x y ⟹ Q x y" and "pred_on.chain A P C" shows "pred_on.chain A Q C" using assms unfolding pred_on.chain_def by blast subsubsection ‹Results for the proper subset relation› interpretation subset: pred_on "A" "(⊂)" for A . lemma subset_maxchain_max: assumes "subset.maxchain A C" and "X ∈ A" and "⋃C ⊆ X" shows "⋃C = X" proof (rule ccontr) let ?C = "{X} ∪ C" from ‹subset.maxchain A C› have "subset.chain A C" and *: "⋀S. subset.chain A S ⟹ ¬ C ⊂ S" by (auto simp: subset.maxchain_def) moreover have "∀x∈C. x ⊆ X" using ‹⋃C ⊆ X› by auto ultimately have "subset.chain A ?C" using subset.chain_extend [of A C X] and ‹X ∈ A› by auto moreover assume **: "⋃C ≠ X" moreover from ** have "C ⊂ ?C" using ‹⋃C ⊆ X› by auto ultimately show False using * by blast qed subsubsection ‹Zorn's lemma› text ‹If every chain has an upper bound, then there is a maximal set.› lemma subset_Zorn: assumes "⋀C. subset.chain A C ⟹ ∃U∈A. ∀X∈C. X ⊆ U" shows "∃M∈A. ∀X∈A. M ⊆ X ⟶ X = M" proof - from subset.Hausdorff [of A] obtain M where "subset.maxchain A M" .. then have "subset.chain A M" by (rule subset.maxchain_imp_chain) with assms obtain Y where "Y ∈ A" and "∀X∈M. X ⊆ Y" by blast moreover have "∀X∈A. Y ⊆ X ⟶ Y = X" proof (intro ballI impI) fix X assume "X ∈ A" and "Y ⊆ X" show "Y = X" proof (rule ccontr) assume "¬ ?thesis" with ‹Y ⊆ X› have "¬ X ⊆ Y" by blast from subset.chain_extend [OF ‹subset.chain A M› ‹X ∈ A›] and ‹∀X∈M. X ⊆ Y› have "subset.chain A ({X} ∪ M)" using ‹Y ⊆ X› by auto moreover have "M ⊂ {X} ∪ M" using ‹∀X∈M. X ⊆ Y› and ‹¬ X ⊆ Y› by auto ultimately show False using ‹subset.maxchain A M› by (auto simp: subset.maxchain_def) qed qed ultimately show ?thesis by blast qed text ‹Alternative version of Zorn's lemma for the subset relation.› lemma subset_Zorn': assumes "⋀C. subset.chain A C ⟹ ⋃C ∈ A" shows "∃M∈A. ∀X∈A. M ⊆ X ⟶ X = M" proof - from subset.Hausdorff [of A] obtain M where "subset.maxchain A M" .. then have "subset.chain A M" by (rule subset.maxchain_imp_chain) with assms have "⋃M ∈ A" . moreover have "∀Z∈A. ⋃M ⊆ Z ⟶ ⋃M = Z" proof (intro ballI impI) fix Z assume "Z ∈ A" and "⋃M ⊆ Z" with subset_maxchain_max [OF ‹subset.maxchain A M›] show "⋃M = Z" . qed ultimately show ?thesis by blast qed subsection ‹Zorn's Lemma for Partial Orders› text ‹Relate old to new definitions.› definition chain_subset :: "'a set set ⇒ bool" ("chain⇩_{⊆}") (* Define globally? In Set.thy? *) where "chain⇩_{⊆}C ⟷ (∀A∈C. ∀B∈C. A ⊆ B ∨ B ⊆ A)" definition chains :: "'a set set ⇒ 'a set set set" where "chains A = {C. C ⊆ A ∧ chain⇩_{⊆}C}" definition Chains :: "('a × 'a) set ⇒ 'a set set" (* Define globally? In Relation.thy? *) where "Chains r = {C. ∀a∈C. ∀b∈C. (a, b) ∈ r ∨ (b, a) ∈ r}" lemma chains_extend: "c ∈ chains S ⟹ z ∈ S ⟹ ∀x ∈ c. x ⊆ z ⟹ {z} ∪ c ∈ chains S" for z :: "'a set" unfolding chains_def chain_subset_def by blast lemma mono_Chains: "r ⊆ s ⟹ Chains r ⊆ Chains s" unfolding Chains_def by blast lemma chain_subset_alt_def: "chain⇩_{⊆}C = subset.chain UNIV C" unfolding chain_subset_def subset.chain_def by fast lemma chains_alt_def: "chains A = {C. subset.chain A C}" by (simp add: chains_def chain_subset_alt_def subset.chain_def) lemma Chains_subset: "Chains r ⊆ {C. pred_on.chain UNIV (λx y. (x, y) ∈ r) C}" by (force simp add: Chains_def pred_on.chain_def) lemma Chains_subset': assumes "refl r" shows "{C. pred_on.chain UNIV (λx y. (x, y) ∈ r) C} ⊆ Chains r" using assms by (auto simp add: Chains_def pred_on.chain_def refl_on_def) lemma Chains_alt_def: assumes "refl r" shows "Chains r = {C. pred_on.chain UNIV (λx y. (x, y) ∈ r) C}" using assms Chains_subset Chains_subset' by blast lemma pairwise_chain_Union: assumes P: "⋀S. S ∈ 𝒞 ⟹ pairwise R S" and "chain⇩_{⊆}𝒞" shows "pairwise R (⋃𝒞)" using ‹chain⇩_{⊆}𝒞› unfolding pairwise_def chain_subset_def by (blast intro: P [unfolded pairwise_def, rule_format]) lemma Zorn_Lemma: "∀C∈chains A. ⋃C ∈ A ⟹ ∃M∈A. ∀X∈A. M ⊆ X ⟶ X = M" using subset_Zorn' [of A] by (force simp: chains_alt_def) lemma Zorn_Lemma2: "∀C∈chains A. ∃U∈A. ∀X∈C. X ⊆ U ⟹ ∃M∈A. ∀X∈A. M ⊆ X ⟶ X = M" using subset_Zorn [of A] by (auto simp: chains_alt_def) text ‹Various other lemmas› lemma chainsD: "c ∈ chains S ⟹ x ∈ c ⟹ y ∈ c ⟹ x ⊆ y ∨ y ⊆ x" unfolding chains_def chain_subset_def by blast lemma chainsD2: "c ∈ chains S ⟹ c ⊆ S" unfolding chains_def by blast lemma Zorns_po_lemma: assumes po: "Partial_order r" and u: "∀C∈Chains r. ∃u∈Field r. ∀a∈C. (a, u) ∈ r" shows "∃m∈Field r. ∀a∈Field r. (m, a) ∈ r ⟶ a = m" proof - have "Preorder r" using po by (simp add: partial_order_on_def) txt ‹Mirror ‹r› in the set of subsets below (wrt ‹r›) elements of ‹A›.› let ?B = "λx. r¯ `` {x}" let ?S = "?B ` Field r" have "∃u∈Field r. ∀A∈C. A ⊆ r¯ `` {u}" (is "∃u∈Field r. ?P u") if 1: "C ⊆ ?S" and 2: "∀A∈C. ∀B∈C. A ⊆ B ∨ B ⊆ A" for C proof - let ?A = "{x∈Field r. ∃M∈C. M = ?B x}" from 1 have "C = ?B ` ?A" by (auto simp: image_def) have "?A ∈ Chains r" proof (simp add: Chains_def, intro allI impI, elim conjE) fix a b assume "a ∈ Field r" and "?B a ∈ C" and "b ∈ Field r" and "?B b ∈ C" with 2 have "?B a ⊆ ?B b ∨ ?B b ⊆ ?B a" by auto then show "(a, b) ∈ r ∨ (b, a) ∈ r" using ‹Preorder r› and ‹a ∈ Field r› and ‹b ∈ Field r› by (simp add:subset_Image1_Image1_iff) qed with u obtain u where uA: "u ∈ Field r" "∀a∈?A. (a, u) ∈ r" by auto have "?P u" proof auto fix a B assume aB: "B ∈ C" "a ∈ B" with 1 obtain x where "x ∈ Field r" and "B = r¯ `` {x}" by auto then show "(a, u) ∈ r" using uA and aB and ‹Preorder r› unfolding preorder_on_def refl_on_def by simp (fast dest: transD) qed then show ?thesis using ‹u ∈ Field r› by blast qed then have "∀C∈chains ?S. ∃U∈?S. ∀A∈C. A ⊆ U" by (auto simp: chains_def chain_subset_def) from Zorn_Lemma2 [OF this] obtain m B where "m ∈ Field r" and "B = r¯ `` {m}" and "∀x∈Field r. B ⊆ r¯ `` {x} ⟶ r¯ `` {x} = B" by auto then have "∀a∈Field r. (m, a) ∈ r ⟶ a = m" using po and ‹Preorder r› and ‹m ∈ Field r› by (auto simp: subset_Image1_Image1_iff Partial_order_eq_Image1_Image1_iff) then show ?thesis using ‹m ∈ Field r› by blast qed subsection ‹The Well Ordering Theorem› (* The initial segment of a relation appears generally useful. Move to Relation.thy? Definition correct/most general? Naming? *) definition init_seg_of :: "(('a × 'a) set × ('a × 'a) set) set" where "init_seg_of = {(r, s). r ⊆ s ∧ (∀a b c. (a, b) ∈ s ∧ (b, c) ∈ r ⟶ (a, b) ∈ r)}" abbreviation initial_segment_of_syntax :: "('a × 'a) set ⇒ ('a × 'a) set ⇒ bool" (infix "initial'_segment'_of" 55) where "r initial_segment_of s ≡ (r, s) ∈ init_seg_of" lemma refl_on_init_seg_of [simp]: "r initial_segment_of r" by (simp add: init_seg_of_def) lemma trans_init_seg_of: "r initial_segment_of s ⟹ s initial_segment_of t ⟹ r initial_segment_of t" by (simp (no_asm_use) add: init_seg_of_def) blast lemma antisym_init_seg_of: "r initial_segment_of s ⟹ s initial_segment_of r ⟹ r = s" unfolding init_seg_of_def by safe lemma Chains_init_seg_of_Union: "R ∈ Chains init_seg_of ⟹ r∈R ⟹ r initial_segment_of ⋃R" by (auto simp: init_seg_of_def Ball_def Chains_def) blast lemma chain_subset_trans_Union: assumes "chain⇩_{⊆}R" "∀r∈R. trans r" shows "trans (⋃R)" proof (intro transI, elim UnionE) fix S1 S2 :: "'a rel" and x y z :: 'a assume "S1 ∈ R" "S2 ∈ R" with assms(1) have "S1 ⊆ S2 ∨ S2 ⊆ S1" unfolding chain_subset_def by blast moreover assume "(x, y) ∈ S1" "(y, z) ∈ S2" ultimately have "((x, y) ∈ S1 ∧ (y, z) ∈ S1) ∨ ((x, y) ∈ S2 ∧ (y, z) ∈ S2)" by blast with ‹S1 ∈ R› ‹S2 ∈ R› assms(2) show "(x, z) ∈ ⋃R" by (auto elim: transE) qed lemma chain_subset_antisym_Union: assumes "chain⇩_{⊆}R" "∀r∈R. antisym r" shows "antisym (⋃R)" proof (intro antisymI, elim UnionE) fix S1 S2 :: "'a rel" and x y :: 'a assume "S1 ∈ R" "S2 ∈ R" with assms(1) have "S1 ⊆ S2 ∨ S2 ⊆ S1" unfolding chain_subset_def by blast moreover assume "(x, y) ∈ S1" "(y, x) ∈ S2" ultimately have "((x, y) ∈ S1 ∧ (y, x) ∈ S1) ∨ ((x, y) ∈ S2 ∧ (y, x) ∈ S2)" by blast with ‹S1 ∈ R› ‹S2 ∈ R› assms(2) show "x = y" unfolding antisym_def by auto qed lemma chain_subset_Total_Union: assumes "chain⇩_{⊆}R" and "∀r∈R. Total r" shows "Total (⋃R)" proof (simp add: total_on_def Ball_def, auto del: disjCI) fix r s a b assume A: "r ∈ R" "s ∈ R" "a ∈ Field r" "b ∈ Field s" "a ≠ b" from ‹chain⇩_{⊆}R› and ‹r ∈ R› and ‹s ∈ R› have "r ⊆ s ∨ s ⊆ r" by (auto simp add: chain_subset_def) then show "(∃r∈R. (a, b) ∈ r) ∨ (∃r∈R. (b, a) ∈ r)" proof assume "r ⊆ s" then have "(a, b) ∈ s ∨ (b, a) ∈ s" using assms(2) A mono_Field[of r s] by (auto simp add: total_on_def) then show ?thesis using ‹s ∈ R› by blast next assume "s ⊆ r" then have "(a, b) ∈ r ∨ (b, a) ∈ r" using assms(2) A mono_Field[of s r] by (fastforce simp add: total_on_def) then show ?thesis using ‹r ∈ R› by blast qed qed lemma wf_Union_wf_init_segs: assumes "R ∈ Chains init_seg_of" and "∀r∈R. wf r" shows "wf (⋃R)" proof (simp add: wf_iff_no_infinite_down_chain, rule ccontr, auto) fix f assume 1: "∀i. ∃r∈R. (f (Suc i), f i) ∈ r" then obtain r where "r ∈ R" and "(f (Suc 0), f 0) ∈ r" by auto have "(f (Suc i), f i) ∈ r" for i proof (induct i) case 0 show ?case by fact next case (Suc i) then obtain s where s: "s ∈ R" "(f (Suc (Suc i)), f(Suc i)) ∈ s" using 1 by auto then have "s initial_segment_of r ∨ r initial_segment_of s" using assms(1) ‹r ∈ R› by (simp add: Chains_def) with Suc s show ?case by (simp add: init_seg_of_def) blast qed then show False using assms(2) and ‹r ∈ R› by (simp add: wf_iff_no_infinite_down_chain) blast qed lemma initial_segment_of_Diff: "p initial_segment_of q ⟹ p - s initial_segment_of q - s" unfolding init_seg_of_def by blast lemma Chains_inits_DiffI: "R ∈ Chains init_seg_of ⟹ {r - s |r. r ∈ R} ∈ Chains init_seg_of" unfolding Chains_def by (blast intro: initial_segment_of_Diff) theorem well_ordering: "∃r::'a rel. Well_order r ∧ Field r = UNIV" proof - ― ‹The initial segment relation on well-orders:› let ?WO = "{r::'a rel. Well_order r}" define I where "I = init_seg_of ∩ ?WO × ?WO" then have I_init: "I ⊆ init_seg_of" by simp then have subch: "⋀R. R ∈ Chains I ⟹ chain⇩_{⊆}R" unfolding init_seg_of_def chain_subset_def Chains_def by blast have Chains_wo: "⋀R r. R ∈ Chains I ⟹ r ∈ R ⟹ Well_order r" by (simp add: Chains_def I_def) blast have FI: "Field I = ?WO" by (auto simp add: I_def init_seg_of_def Field_def) then have 0: "Partial_order I" by (auto simp: partial_order_on_def preorder_on_def antisym_def antisym_init_seg_of refl_on_def trans_def I_def elim!: trans_init_seg_of) ― ‹‹I›-chains have upper bounds in ‹?WO› wrt ‹I›: their Union› have "⋃R ∈ ?WO ∧ (∀r∈R. (r, ⋃R) ∈ I)" if "R ∈ Chains I" for R proof - from that have Ris: "R ∈ Chains init_seg_of" using mono_Chains [OF I_init] by blast have subch: "chain⇩_{⊆}R" using ‹R ∈ Chains I› I_init by (auto simp: init_seg_of_def chain_subset_def Chains_def) have "∀r∈R. Refl r" and "∀r∈R. trans r" and "∀r∈R. antisym r" and "∀r∈R. Total r" and "∀r∈R. wf (r - Id)" using Chains_wo [OF ‹R ∈ Chains I›] by (simp_all add: order_on_defs) have "Refl (⋃R)" using ‹∀r∈R. Refl r› unfolding refl_on_def by fastforce moreover have "trans (⋃R)" by (rule chain_subset_trans_Union [OF subch ‹∀r∈R. trans r›]) moreover have "antisym (⋃R)" by (rule chain_subset_antisym_Union [OF subch ‹∀r∈R. antisym r›]) moreover have "Total (⋃R)" by (rule chain_subset_Total_Union [OF subch ‹∀r∈R. Total r›]) moreover have "wf ((⋃R) - Id)" proof - have "(⋃R) - Id = ⋃{r - Id | r. r ∈ R}" by blast with ‹∀r∈R. wf (r - Id)› and wf_Union_wf_init_segs [OF Chains_inits_DiffI [OF Ris]] show ?thesis by fastforce qed ultimately have "Well_order (⋃R)" by (simp add:order_on_defs) moreover have "∀r ∈ R. r initial_segment_of ⋃R" using Ris by (simp add: Chains_init_seg_of_Union) ultimately show ?thesis using mono_Chains [OF I_init] Chains_wo[of R] and ‹R ∈ Chains I› unfolding I_def by blast qed then have 1: "∀R ∈ Chains I. ∃u∈Field I. ∀r∈R. (r, u) ∈ I" by (subst FI) blast ― ‹Zorn's Lemma yields a maximal well-order ‹m›:› then obtain m :: "'a rel" where "Well_order m" and max: "∀r. Well_order r ∧ (m, r) ∈ I ⟶ r = m" using Zorns_po_lemma[OF 0 1] unfolding FI by fastforce ― ‹Now show by contradiction that ‹m› covers the whole type:› have False if "x ∉ Field m" for x :: 'a proof - ― ‹Assuming that ‹x› is not covered and extend ‹m› at the top with ‹x›› have "m ≠ {}" proof assume "m = {}" moreover have "Well_order {(x, x)}" by (simp add: order_on_defs refl_on_def trans_def antisym_def total_on_def Field_def) ultimately show False using max by (auto simp: I_def init_seg_of_def simp del: Field_insert) qed then have "Field m ≠ {}" by (auto simp: Field_def) moreover have "wf (m - Id)" using ‹Well_order m› by (simp add: well_order_on_def) ― ‹The extension of ‹m› by ‹x›:› let ?s = "{(a, x) | a. a ∈ Field m}" let ?m = "insert (x, x) m ∪ ?s" have Fm: "Field ?m = insert x (Field m)" by (auto simp: Field_def) have "Refl m" and "trans m" and "antisym m" and "Total m" and "wf (m - Id)" using ‹Well_order m› by (simp_all add: order_on_defs) ― ‹We show that the extension is a well-order› have "Refl ?m" using ‹Refl m› Fm unfolding refl_on_def by blast moreover have "trans ?m" using ‹trans m› and ‹x ∉ Field m› unfolding trans_def Field_def by blast moreover have "antisym ?m" using ‹antisym m› and ‹x ∉ Field m› unfolding antisym_def Field_def by blast moreover have "Total ?m" using ‹Total m› and Fm by (auto simp: total_on_def) moreover have "wf (?m - Id)" proof - have "wf ?s" using ‹x ∉ Field m› by (auto simp: wf_eq_minimal Field_def Bex_def) then show ?thesis using ‹wf (m - Id)› and ‹x ∉ Field m› wf_subset [OF ‹wf ?s› Diff_subset] by (auto simp: Un_Diff Field_def intro: wf_Un) qed ultimately have "Well_order ?m" by (simp add: order_on_defs) ― ‹We show that the extension is above ‹m›› moreover have "(m, ?m) ∈ I" using ‹Well_order ?m› and ‹Well_order m› and ‹x ∉ Field m› by (fastforce simp: I_def init_seg_of_def Field_def) ultimately ― ‹This contradicts maximality of ‹m›:› show False using max and ‹x ∉ Field m› unfolding Field_def by blast qed then have "Field m = UNIV" by auto with ‹Well_order m› show ?thesis by blast qed corollary well_order_on: "∃r::'a rel. well_order_on A r" proof - obtain r :: "'a rel" where wo: "Well_order r" and univ: "Field r = UNIV" using well_ordering [where 'a = "'a"] by blast let ?r = "{(x, y). x ∈ A ∧ y ∈ A ∧ (x, y) ∈ r}" have 1: "Field ?r = A" using wo univ by (fastforce simp: Field_def order_on_defs refl_on_def) from ‹Well_order r› have "Refl r" "trans r" "antisym r" "Total r" "wf (r - Id)" by (simp_all add: order_on_defs) from ‹Refl r› have "Refl ?r" by (auto simp: refl_on_def 1 univ) moreover from ‹trans r› have "trans ?r" unfolding trans_def by blast moreover from ‹antisym r› have "antisym ?r" unfolding antisym_def by blast moreover from ‹Total r› have "Total ?r" by (simp add:total_on_def 1 univ) moreover have "wf (?r - Id)" by (rule wf_subset [OF ‹wf (r - Id)›]) blast ultimately have "Well_order ?r" by (simp add: order_on_defs) with 1 show ?thesis by auto qed (* Move this to Hilbert Choice and wfrec to Wellfounded*) lemma wfrec_def_adm: "f ≡ wfrec R F ⟹ wf R ⟹ adm_wf R F ⟹ f = F f" using wfrec_fixpoint by simp lemma dependent_wf_choice: fixes P :: "('a ⇒ 'b) ⇒ 'a ⇒ 'b ⇒ bool" assumes "wf R" and adm: "⋀f g x r. (⋀z. (z, x) ∈ R ⟹ f z = g z) ⟹ P f x r = P g x r" and P: "⋀x f. (⋀y. (y, x) ∈ R ⟹ P f y (f y)) ⟹ ∃r. P f x r" shows "∃f. ∀x. P f x (f x)" proof (intro exI allI) fix x define f where "f ≡ wfrec R (λf x. SOME r. P f x r)" from ‹wf R› show "P f x (f x)" proof (induct x) case (less x) show "P f x (f x)" proof (subst (2) wfrec_def_adm[OF f_def ‹wf R›]) show "adm_wf R (λf x. SOME r. P f x r)" by (auto simp add: adm_wf_def intro!: arg_cong[where f=Eps] ext adm) show "P f x (Eps (P f x))" using P by (rule someI_ex) fact qed qed qed lemma (in wellorder) dependent_wellorder_choice: assumes "⋀r f g x. (⋀y. y < x ⟹ f y = g y) ⟹ P f x r = P g x r" and P: "⋀x f. (⋀y. y < x ⟹ P f y (f y)) ⟹ ∃r. P f x r" shows "∃f. ∀x. P f x (f x)" using wf by (rule dependent_wf_choice) (auto intro!: assms) end