(* Title: HOL/Library/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. The extension of any well-founded relation to a well-order. *) header {* Zorn's Lemma *} theory Zorn imports Order_Union begin subsection {* Zorn's Lemma for the Subset Relation *} subsubsection {* Results that do not require an order *} text {*Let @{text P} be a binary predicate on the set @{text 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\<^sup>=\<^sup>= x y" text {*A chain is a totally ordered subset of @{term 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 @{term X}, but not necessarily a chain itself, a superchain of @{term X}.*} abbreviation superchain :: "'a set \ 'a set \ bool" (infix " 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 'a set" where "suc C = (if \ chain C \ maxchain C then C else (SOME D. C 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 \ maxchain C \ suc C \ C" by (auto simp: suc_def) (metis less_irrefl not_maxchain_Some) 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+ 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+ 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) moreover then have "suc X \ A" unfolding chain_def by blast ultimately 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) qed blast lemma suc_Union_closed_subsetD: assumes "Y \ X" and "X \ \" and "Y \ \" shows "X = Y \ suc Y \ X" using assms(2-, 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 then show ?thesis using suc_subset [of Y] 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`) qed blast lemma eq_suc_Union: assumes "X \ \" shows "suc X = X \ X = \\" proof assume "suc X = X" with suc_Union_closed_suc [OF suc_Union_closed_Union `X \ \`] have "\\ \ X" . with `X \ \` show "X = \\" by blast next from `X \ \` have "suc X \ \" by (rule suc) then have "suc X \ \\" by blast moreover assume "X = \\" ultimately have "suc X \ X" by simp moreover have "X \ suc X" by (rule suc_subset) ultimately show "suc X = X" .. 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 by (simp add: suc_def) (metis not_maxchain_Some) 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 @{term A}. (Note that we do not require @{term A} to be partially ordered.)*} theorem Hausdorff: "\C. maxchain C" proof - let ?M = "\\" have "maxchain ?M" proof (rule ccontr) assume "\ maxchain ?M" 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" "op \" 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 then 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 "Y \ X" 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.*} (* Define globally? In Set.thy? *) definition chain_subset :: "'a set set \ bool" ("chain\<^sub>\") where "chain\<^sub>\ 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\<^sub>\ C}" (* Define globally? In Relation.thy? *) definition Chains :: "('a \ 'a) set \ 'a set set" 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:: 'a set) |] ==> {z} Un c \ chains S" by (unfold chains_def chain_subset_def) blast lemma mono_Chains: "r \ s \ Chains r \ Chains s" unfolding Chains_def by blast lemma chain_subset_alt_def: "chain\<^sub>\ C = subset.chain UNIV C" by (auto simp add: chain_subset_def subset.chain_def) 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 by (metis Chains_subset Chains_subset' subset_antisym) 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" by (unfold chains_def chain_subset_def) blast lemma chainsD2: "!!(c :: 'a set set). c \ chains S ==> c \ S" by (unfold chains_def) 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) --{* Mirror r in the set of subsets below (wrt r) elements of A*} let ?B = "%x. r\ `` {x}" let ?S = "?B ` Field r" { fix C assume 1: "C \ ?S" and 2: "\A\C. \B\C. A \ B \ B \ A" let ?A = "{x\Field r. \M\C. M = ?B x}" have "C = ?B ` ?A" using 1 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" hence "?B a \ ?B b \ ?B b \ ?B a" using 2 by auto thus "(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 then obtain u where uA: "u \ Field r" "\a\?A. (a, u) \ r" using u by auto have "\A\C. A \ r\ `` {u}" (is "?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 thus "(a, u) \ r" using uA and aB and `Preorder r` by (auto simp add: preorder_on_def refl_on_def) (metis transD) qed then have "\u\Field r. ?P u" using `u \ Field r` by blast } 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 hence "\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) thus ?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 initialSegmentOf :: "('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) (metis UnCI Un_absorb2 subset_trans) 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: "chain\<^sub>\ R \ \r\R. trans r \ trans (\R)" apply (auto simp add: chain_subset_def) apply (simp (no_asm_use) add: trans_def) apply (metis subsetD) done lemma chain_subset_antisym_Union: "chain\<^sub>\ R \ \r\R. antisym r \ antisym (\R)" apply (auto simp add: chain_subset_def antisym_def) apply (metis subsetD) done lemma chain_subset_Total_Union: assumes "chain\<^sub>\ 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\<^sub>\ R` and `r \ R` and `s \ R` have "r \ s \ s \ r" by (auto simp add: chain_subset_def) thus "(\r\R. (a, b) \ r) \ (\r\R. (b, a) \ r)" proof assume "r \ s" hence "(a, b) \ s \ (b, a) \ s" using assms(2) A by (simp add: total_on_def) (metis mono_Field subsetD) thus ?thesis using `s \ R` by blast next assume "s \ r" hence "(a, b) \ r \ (b, a) \ r" using assms(2) A by (simp add: total_on_def) (metis mono_Field subsetD) thus ?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 { fix i have "(f (Suc i), f i) \ r" proof (induct i) case 0 show ?case by fact next case (Suc i) moreover obtain s where "s \ R" and "(f (Suc (Suc i)), f(Suc i)) \ s" using 1 by auto moreover hence "s initial_segment_of r \ r initial_segment_of s" using assms(1) `r \ R` by (simp add: Chains_def) ultimately show ?case by (simp add: init_seg_of_def) blast qed } thus 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}" def I \ "init_seg_of \ ?WO \ ?WO" have I_init: "I \ init_seg_of" by (auto simp: I_def) hence subch: "\R. R \ Chains I \ chain\<^sub>\ R" by (auto simp: init_seg_of_def chain_subset_def Chains_def) 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) hence 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*} { fix R assume "R \ Chains I" hence Ris: "R \ Chains init_seg_of" using mono_Chains [OF I_init] by blast have subch: "chain\<^sub>\ 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` by (auto simp: refl_on_def) 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 (simp (no_asm_simp)) blast 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 have "\R \ ?WO \ (\r\R. (r, \R) \ I)" using mono_Chains [OF I_init] and `R \ Chains I` by (simp (no_asm) add: I_def del: Field_Union) (metis Chains_wo) } hence 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] by (auto simp:FI) --{*Now show by contradiction that m covers the whole type:*} { fix x::'a assume "x \ Field m" --{*We assume 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 hence "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 by (auto simp: refl_on_def) 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 add: wf_eq_minimal Field_def) metis thus ?thesis using `wf (m - Id)` and `x \ Field m` wf_subset [OF `wf ?s` Diff_subset] by (fastforce intro!: wf_Un simp add: Un_Diff Field_def) qed ultimately have "Well_order ?m" by (simp add: order_on_defs) --{*We show that the extension is above m*} moreover hence "(m, ?m) \ I" using `Well_order m` and `x \ Field m` by (fastforce simp: I_def init_seg_of_def Field_def) ultimately --{*This contradicts maximality of m:*} have False using max and `x \ Field m` unfolding Field_def by blast } hence "Field m = UNIV" by auto moreover with `Well_order m` have "Well_order m" by simp ultimately 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) have "Refl r" and "trans r" and "antisym r" and "Total r" and "wf (r - Id)" using `Well_order r` by (simp_all add: order_on_defs) have "Refl ?r" using `Refl r` by (auto simp: refl_on_def 1 univ) moreover have "trans ?r" using `trans r` unfolding trans_def by blast moreover have "antisym ?r" using `antisym r` unfolding antisym_def by blast moreover have "Total ?r" using `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 metis qed subsection {* Extending Well-founded Relations to Well-Orders *} text {*A \emph{downset} (also lower set, decreasing set, initial segment, or downward closed set) is closed w.r.t.\ smaller elements.*} definition downset_on where "downset_on A r = (\x y. (x, y) \ r \ y \ A \ x \ A)" (* text {*Connection to order filters of the @{theory Cardinals} theory.*} lemma (in wo_rel) ofilter_downset_on_conv: "ofilter A \ downset_on A r \ A \ Field r" by (auto simp: downset_on_def ofilter_def under_def) *) lemma downset_onI: "(\x y. (x, y) \ r \ y \ A \ x \ A) \ downset_on A r" by (auto simp: downset_on_def) lemma downset_onD: "downset_on A r \ (x, y) \ r \ y \ A \ x \ A" by (auto simp: downset_on_def) text {*Extensions of relations w.r.t.\ a given set.*} definition extension_on where "extension_on A r s = (\x\A. \y\A. (x, y) \ s \ (x, y) \ r)" lemma extension_onI: "(\x y. \x \ A; y \ A; (x, y) \ s\ \ (x, y) \ r) \ extension_on A r s" by (auto simp: extension_on_def) lemma extension_onD: "extension_on A r s \ x \ A \ y \ A \ (x, y) \ s \ (x, y) \ r" by (auto simp: extension_on_def) lemma downset_on_Union: assumes "\r. r \ R \ downset_on (Field r) p" shows "downset_on (Field (\R)) p" using assms by (auto intro: downset_onI dest: downset_onD) lemma chain_subset_extension_on_Union: assumes "chain\<^sub>\ R" and "\r. r \ R \ extension_on (Field r) r p" shows "extension_on (Field (\R)) (\R) p" using assms by (simp add: chain_subset_def extension_on_def) (metis mono_Field set_mp) lemma downset_on_empty [simp]: "downset_on {} p" by (auto simp: downset_on_def) lemma extension_on_empty [simp]: "extension_on {} p q" by (auto simp: extension_on_def) text {*Every well-founded relation can be extended to a well-order.*} theorem well_order_extension: assumes "wf p" shows "\w. p \ w \ Well_order w" proof - let ?K = "{r. Well_order r \ downset_on (Field r) p \ extension_on (Field r) r p}" def I \ "init_seg_of \ ?K \ ?K" have I_init: "I \ init_seg_of" by (simp add: I_def) then have subch: "\R. R \ Chains I \ chain\<^sub>\ R" by (auto simp: init_seg_of_def chain_subset_def Chains_def) have Chains_wo: "\R r. R \ Chains I \ r \ R \ Well_order r \ downset_on (Field r) p \ extension_on (Field r) r p" by (simp add: Chains_def I_def) blast have FI: "Field I = ?K" by (auto simp: 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) { fix R assume "R \ Chains I" then have Ris: "R \ Chains init_seg_of" using mono_Chains [OF I_init] by blast have subch: "chain\<^sub>\ 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)" and "\r. r \ R \ downset_on (Field r) p" and "\r. r \ R \ extension_on (Field r) r p" using Chains_wo [OF `R \ Chains I`] by (simp_all add: order_on_defs) have "Refl (\R)" using `\r\R. Refl r` by (auto simp: refl_on_def) 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)` wf_Union_wf_init_segs [OF Chains_inits_DiffI [OF Ris]] show ?thesis by (simp (no_asm_simp)) blast 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) moreover have "downset_on (Field (\R)) p" by (rule downset_on_Union [OF `\r. r \ R \ downset_on (Field r) p`]) moreover have "extension_on (Field (\R)) (\R) p" by (rule chain_subset_extension_on_Union [OF subch `\r. r \ R \ extension_on (Field r) r p`]) ultimately have "\R \ ?K \ (\r\R. (r,\R) \ I)" using mono_Chains [OF I_init] and `R \ Chains I` by (simp (no_asm) add: I_def del: Field_Union) (metis Chains_wo) } then have 1: "\R\Chains I. \u\Field I. \r\R. (r, u) \ I" by (subst FI) blast txt {*Zorn's Lemma yields a maximal well-order m.*} from Zorns_po_lemma [OF 0 1] obtain m :: "('a \ 'a) set" where "Well_order m" and "downset_on (Field m) p" and "extension_on (Field m) m p" and max: "\r. Well_order r \ downset_on (Field r) p \ extension_on (Field r) r p \ (m, r) \ I \ r = m" by (auto simp: FI) have "Field p \ Field m" proof (rule ccontr) let ?Q = "Field p - Field m" assume "\ (Field p \ Field m)" with assms [unfolded wf_eq_minimal, THEN spec, of ?Q] obtain x where "x \ Field p" and "x \ Field m" and min: "\y. (y, x) \ p \ y \ ?Q" by blast txt {*Add @{term x} as topmost element to @{term m}.*} let ?s = "{(y, x) | y. y \ 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) txt {*We show that the extension is a well-order.*} have "Refl ?m" using `Refl m` Fm by (auto simp: refl_on_def) moreover have "trans ?m" using `trans m` `x \ Field m` unfolding trans_def Field_def Domain_unfold Domain_converse [symmetric] by blast moreover have "antisym ?m" using `antisym m` `x \ Field m` unfolding antisym_def Field_def Domain_unfold Domain_converse [symmetric] by blast moreover have "Total ?m" using `Total m` Fm by (auto simp: Relation.total_on_def) moreover have "wf (?m - Id)" proof - have "wf ?s" using `x \ Field m` by (simp add: wf_eq_minimal Field_def Domain_unfold Domain_converse [symmetric]) metis thus ?thesis using `wf (m - Id)` `x \ Field m` wf_subset [OF `wf ?s` Diff_subset] by (fastforce intro!: wf_Un simp add: Un_Diff Field_def) qed ultimately have "Well_order ?m" by (simp add: order_on_defs) moreover have "extension_on (Field ?m) ?m p" using `extension_on (Field m) m p` `downset_on (Field m) p` by (subst Fm) (auto simp: extension_on_def dest: downset_onD) moreover have "downset_on (Field ?m) p" using `downset_on (Field m) p` and min by (subst Fm, simp add: downset_on_def Field_def) (metis Domain_iff) moreover have "(m, ?m) \ I" using `Well_order m` and `Well_order ?m` and `downset_on (Field m) p` and `downset_on (Field ?m) p` and `extension_on (Field m) m p` and `extension_on (Field ?m) ?m p` and `Refl m` and `x \ Field m` by (auto simp: I_def init_seg_of_def refl_on_def) ultimately --{*This contradicts maximality of m:*} show False using max and `x \ Field m` unfolding Field_def by blast qed have "p \ m" using `Field p \ Field m` and `extension_on (Field m) m p` by (force simp: Field_def extension_on_def) with `Well_order m` show ?thesis by blast qed text {*Every well-founded relation can be extended to a total well-order.*} corollary total_well_order_extension: assumes "wf p" shows "\w. p \ w \ Well_order w \ Field w = UNIV" proof - from well_order_extension [OF assms] obtain w where "p \ w" and wo: "Well_order w" by blast let ?A = "UNIV - Field w" from well_order_on [of ?A] obtain w' where wo': "well_order_on ?A w'" .. have [simp]: "Field w' = ?A" using rel.well_order_on_Well_order [OF wo'] by simp have *: "Field w \ Field w' = {}" by simp let ?w = "w \o w'" have "p \ ?w" using `p \ w` by (auto simp: Osum_def) moreover have "Well_order ?w" using Osum_Well_order [OF * wo] and wo' by simp moreover have "Field ?w = UNIV" by (simp add: Field_Osum) ultimately show ?thesis by blast qed corollary well_order_on_extension: assumes "wf p" and "Field p \ A" shows "\w. p \ w \ well_order_on A w" proof - from total_well_order_extension [OF `wf p`] obtain r where "p \ r" and wo: "Well_order r" and univ: "Field r = UNIV" by blast let ?r = "{(x, y). x \ A \ y \ A \ (x, y) \ r}" from `p \ r` have "p \ ?r" using `Field p \ A` by (auto simp: Field_def) have 1: "Field ?r = A" using wo univ by (fastforce simp: Field_def order_on_defs refl_on_def) have "Refl r" "trans r" "antisym r" "Total r" "wf (r - Id)" using `Well_order r` by (simp_all add: order_on_defs) have "refl_on A ?r" using `Refl r` by (auto simp: refl_on_def univ) moreover have "trans ?r" using `trans r` unfolding trans_def by blast moreover have "antisym ?r" using `antisym r` unfolding antisym_def by blast moreover have "total_on A ?r" using `Total r` by (simp add: total_on_def univ) moreover have "wf (?r - Id)" by (rule wf_subset [OF `wf(r - Id)`]) blast ultimately have "well_order_on A ?r" by (simp add: order_on_defs) with `p \ ?r` show ?thesis by blast qed end