(* 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 @{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" 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+ 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) 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) 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 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 @{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 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 "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" 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 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` unfolding preorder_on_def refl_on_def by simp (fast dest: 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) 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\<^sub>\ 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\<^sub>\ 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\<^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 mono_Field[of r s] by (auto simp add: total_on_def) thus ?thesis using `s \ R` by blast next assume "s \ r" hence "(a, b) \ r \ (b, a) \ r" using assms(2) A mono_Field[of s r] by (fastforce simp add: total_on_def) 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) 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 } 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" 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) 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` 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 have "\R \ ?WO \ (\r\R. (r, \R) \ I)" using mono_Chains [OF I_init] Chains_wo[of R] and `R \ Chains I` unfolding I_def by blast } 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] unfolding FI by fastforce --{*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 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` unfolding wf_eq_minimal Field_def by (auto simp: Bex_def) thus ?thesis using `wf (m - Id)` and `x \ Field m` wf_subset [OF `wf ?s` Diff_subset] unfolding Un_Diff Field_def by (auto 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:*} have False using max and `x \ Field m` unfolding Field_def by blast } hence "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) 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 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" assumes 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 def f \ "wfrec R (\f x. SOME r. P f x r)" from `wf R` show "P f x (f x)" proof (induct x) fix x assume "\y. (y, x) \ R \ P f y (f y)" 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" assumes 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