# HG changeset patch # User ballarin # Date 1217346648 -7200 # Node ID 5b1585b489527012cdaa741d10e6a55532052b50 # Parent cb6c513922e0fb273cb6e5fa47c1d4ca64ff2550 Zorn's Lemma for partial orders. diff -r cb6c513922e0 -r 5b1585b48952 NEWS --- a/NEWS Tue Jul 29 17:50:12 2008 +0200 +++ b/NEWS Tue Jul 29 17:50:48 2008 +0200 @@ -147,6 +147,11 @@ Complex_Main.thy should now use new entry point Hypercomplex.thy. +*** ZF *** + +* Proof of Zorn's Lemma for partial orders. + + *** ML *** * Rules and tactics that read instantiations (read_instantiate, diff -r cb6c513922e0 -r 5b1585b48952 src/ZF/Zorn.thy --- a/src/ZF/Zorn.thy Tue Jul 29 17:50:12 2008 +0200 +++ b/src/ZF/Zorn.thy Tue Jul 29 17:50:48 2008 +0200 @@ -298,6 +298,26 @@ apply (fast elim: equalityE) done +text {* Alternative version of Zorn's Lemma *} + +theorem Zorn2: + "\c \ chain(S). \y \ S. \x \ c. x <= y ==> \y \ S. \z \ S. y<=z --> y=z" +apply (cut_tac Hausdorff maxchain_subset_chain) +apply (erule exE) +apply (drule subsetD, assumption) +apply (drule bspec, assumption, erule bexE) +apply (rule_tac x = y in bexI) + prefer 2 apply assumption +apply clarify +apply rule apply assumption +apply rule +apply (rule ccontr) +apply (frule_tac z=z in chain_extend) + apply (assumption, blast) +apply (unfold maxchain_def super_def) +apply (blast elim!: equalityCE) +done + subsection{*Zermelo's Theorem: Every Set can be Well-Ordered*} @@ -411,4 +431,89 @@ apply (rule choice_imp_injection [THEN inj_weaken_type], blast+) done + +subsection {* Zorn's Lemma for Partial Orders *} + +text {* Reimported from HOL by Clemens Ballarin. *} + + +definition Chain :: "i => i" where + "Chain(r) = {A : Pow(field(r)). ALL a:A. ALL b:A. : r | : r}" + +lemma mono_Chain: + "r \ s ==> Chain(r) \ Chain(s)" + unfolding Chain_def + by blast + +theorem Zorn_po: + assumes po: "Partial_order(r)" + and u: "ALL C:Chain(r). EX u:field(r). ALL a:C. : r" + shows "EX m:field(r). ALL a:field(r). : 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 = "lam x:field(r). r -`` {x}" let ?S = "?B `` field(r)" + have "ALL C:chain(?S). EX U:?S. ALL A:C. A \ U" + proof (clarsimp simp: chain_def Subset_rel_def bex_image_simp) + fix C + assume 1: "C \ ?S" and 2: "ALL A:C. ALL B:C. A \ B | B \ A" + let ?A = "{x : field(r). EX M:C. M = ?B`x}" + have "C = ?B `` ?A" using 1 + apply (auto simp: image_def) + apply rule + apply rule + apply (drule subsetD) apply assumption + apply (erule CollectE) + apply rule apply assumption + apply (erule bexE) + apply rule prefer 2 apply assumption + apply rule + apply (erule lamE) apply simp + apply assumption + + apply (thin_tac "C \ ?X") + apply (fast elim: lamE) + done + have "?A : Chain(r)" + proof (simp add: Chain_def subsetI, intro conjI ballI impI) + fix a b + assume "a : field(r)" "r -`` {a} : C" "b : field(r)" "r -`` {b} : C" + hence "r -`` {a} \ r -`` {b} | r -`` {b} \ r -`` {a}" using 2 by auto + then show " : r | : r" + using `Preorder(r)` `a : field(r)` `b : field(r)` + by (simp add: subset_vimage1_vimage1_iff) + qed + then obtain u where uA: "u : field(r)" "ALL a:?A. : r" + using u + apply auto + apply (drule bspec) apply assumption + apply auto + done + have "ALL A:C. A \ r -`` {u}" + proof (auto intro!: vimageI) + fix a B + assume aB: "B : C" "a : B" + with 1 obtain x where "x : field(r)" "B = r -`` {x}" + apply - + apply (drule subsetD) apply assumption + apply (erule imageE) + apply (erule lamE) + apply simp + done + then show " : r" using uA aB `Preorder(r)` + by (auto simp: preorder_on_def refl_def) (blast dest: trans_onD)+ + qed + then show "EX U:field(r). ALL A:C. A \ r -`` {U}" + using `u : field(r)` .. + qed + from Zorn2 [OF this] + obtain m B where "m : field(r)" "B = r -`` {m}" + "ALL x:field(r). B \ r -`` {x} --> B = r -`` {x}" + by (auto elim!: lamE simp: ball_image_simp) + then have "ALL a:field(r). : r --> a = m" + using po `Preorder(r)` `m : field(r)` + by (auto simp: subset_vimage1_vimage1_iff Partial_order_eq_vimage1_vimage1_iff) + then show ?thesis using `m : field(r)` by blast +qed + end