# Theory Zorn

Up to index of Isabelle/ZF

theory Zorn
imports AC
`(*  Title:      ZF/Zorn.thy    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory    Copyright   1994  University of Cambridge*)header{*Zorn's Lemma*}theory Zorn imports OrderArith AC Inductive_ZF begintext{*Based upon the unpublished article ``Towards the Mechanization of theProofs of Some Classical Theorems of Set Theory,'' by Abrial and Laffitte.*}definition  Subset_rel :: "i=>i"  where   "Subset_rel(A) == {z ∈ A*A . ∃x y. z=<x,y> & x<=y & x≠y}"definition  chain      :: "i=>i"  where   "chain(A)      == {F ∈ Pow(A). ∀X∈F. ∀Y∈F. X<=Y | Y<=X}"definition  super      :: "[i,i]=>i"  where   "super(A,c)    == {d ∈ chain(A). c<=d & c≠d}"definition  maxchain   :: "i=>i"  where   "maxchain(A)   == {c ∈ chain(A). super(A,c)=0}"definition  increasing :: "i=>i"  where    "increasing(A) == {f ∈ Pow(A)->Pow(A). ∀x. x<=A --> x<=f`x}"text{*Lemma for the inductive definition below*}lemma Union_in_Pow: "Y ∈ Pow(Pow(A)) ==> \<Union>(Y) ∈ Pow(A)"by blasttext{*We could make the inductive definition conditional on    @{term "next ∈ increasing(S)"}    but instead we make this a side-condition of an introduction rule.  Thus    the induction rule lets us assume that condition!  Many inductive proofs    are therefore unconditional.*}consts  "TFin" :: "[i,i]=>i"inductive  domains       "TFin(S,next)" ⊆ "Pow(S)"  intros    nextI:       "[| x ∈ TFin(S,next);  next ∈ increasing(S) |]                  ==> next`x ∈ TFin(S,next)"    Pow_UnionI: "Y ∈ Pow(TFin(S,next)) ==> \<Union>(Y) ∈ TFin(S,next)"  monos         Pow_mono  con_defs      increasing_def  type_intros   CollectD1 [THEN apply_funtype] Union_in_Powsubsection{*Mathematical Preamble *}lemma Union_lemma0: "(∀x∈C. x<=A | B<=x) ==> \<Union>(C)<=A | B<=\<Union>(C)"by blastlemma Inter_lemma0:     "[| c ∈ C; ∀x∈C. A<=x | x<=B |] ==> A ⊆ \<Inter>(C) | \<Inter>(C) ⊆ B"by blastsubsection{*The Transfinite Construction *}lemma increasingD1: "f ∈ increasing(A) ==> f ∈ Pow(A)->Pow(A)"apply (unfold increasing_def)apply (erule CollectD1)donelemma increasingD2: "[| f ∈ increasing(A); x<=A |] ==> x ⊆ f`x"by (unfold increasing_def, blast)lemmas TFin_UnionI = PowI [THEN TFin.Pow_UnionI]lemmas TFin_is_subset = TFin.dom_subset [THEN subsetD, THEN PowD]text{*Structural induction on @{term "TFin(S,next)"} *}lemma TFin_induct:  "[| n ∈ TFin(S,next);      !!x. [| x ∈ TFin(S,next);  P(x);  next ∈ increasing(S) |] ==> P(next`x);      !!Y. [| Y ⊆ TFin(S,next);  ∀y∈Y. P(y) |] ==> P(\<Union>(Y))   |] ==> P(n)"by (erule TFin.induct, blast+)subsection{*Some Properties of the Transfinite Construction *}lemmas increasing_trans = subset_trans [OF _ increasingD2,                                        OF _ _ TFin_is_subset]text{*Lemma 1 of section 3.1*}lemma TFin_linear_lemma1:     "[| n ∈ TFin(S,next);  m ∈ TFin(S,next);         ∀x ∈ TFin(S,next) . x<=m --> x=m | next`x<=m |]      ==> n<=m | next`m<=n"apply (erule TFin_induct)apply (erule_tac [2] Union_lemma0) (*or just Blast_tac*)(*downgrade subsetI from intro! to intro*)apply (blast dest: increasing_trans)donetext{*Lemma 2 of section 3.2.  Interesting in its own right!  Requires @{term "next ∈ increasing(S)"} in the second induction step.*}lemma TFin_linear_lemma2:    "[| m ∈ TFin(S,next);  next ∈ increasing(S) |]     ==> ∀n ∈ TFin(S,next). n<=m --> n=m | next`n ⊆ m"apply (erule TFin_induct)apply (rule impI [THEN ballI])txt{*case split using @{text TFin_linear_lemma1}*}apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],       assumption+)apply (blast del: subsetI             intro: increasing_trans subsetI, blast)txt{*second induction step*}apply (rule impI [THEN ballI])apply (rule Union_lemma0 [THEN disjE])apply (erule_tac [3] disjI2)prefer 2 apply blastapply (rule ballI)apply (drule bspec, assumption)apply (drule subsetD, assumption)apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],       assumption+, blast)apply (erule increasingD2 [THEN subset_trans, THEN disjI1])apply (blast dest: TFin_is_subset)+donetext{*a more convenient form for Lemma 2*}lemma TFin_subsetD:     "[| n<=m;  m ∈ TFin(S,next);  n ∈ TFin(S,next);  next ∈ increasing(S) |]      ==> n=m | next`n ⊆ m"by (blast dest: TFin_linear_lemma2 [rule_format])text{*Consequences from section 3.3 -- Property 3.2, the ordering is total*}lemma TFin_subset_linear:     "[| m ∈ TFin(S,next);  n ∈ TFin(S,next);  next ∈ increasing(S) |]      ==> n ⊆ m | m<=n"apply (rule disjE)apply (rule TFin_linear_lemma1 [OF _ _TFin_linear_lemma2])apply (assumption+, erule disjI2)apply (blast del: subsetI             intro: subsetI increasingD2 [THEN subset_trans] TFin_is_subset)donetext{*Lemma 3 of section 3.3*}lemma equal_next_upper:     "[| n ∈ TFin(S,next);  m ∈ TFin(S,next);  m = next`m |] ==> n ⊆ m"apply (erule TFin_induct)apply (drule TFin_subsetD)apply (assumption+, force, blast)donetext{*Property 3.3 of section 3.3*}lemma equal_next_Union:     "[| m ∈ TFin(S,next);  next ∈ increasing(S) |]      ==> m = next`m <-> m = \<Union>(TFin(S,next))"apply (rule iffI)apply (rule Union_upper [THEN equalityI])apply (rule_tac [2] equal_next_upper [THEN Union_least])apply (assumption+)apply (erule ssubst)apply (rule increasingD2 [THEN equalityI], assumption)apply (blast del: subsetI             intro: subsetI TFin_UnionI TFin.nextI TFin_is_subset)+donesubsection{*Hausdorff's Theorem: Every Set Contains a Maximal Chain*}text{*NOTE: We assume the partial ordering is @{text "⊆"}, the subsetrelation!*}text{** Defining the "next" operation for Hausdorff's Theorem **}lemma chain_subset_Pow: "chain(A) ⊆ Pow(A)"apply (unfold chain_def)apply (rule Collect_subset)donelemma super_subset_chain: "super(A,c) ⊆ chain(A)"apply (unfold super_def)apply (rule Collect_subset)donelemma maxchain_subset_chain: "maxchain(A) ⊆ chain(A)"apply (unfold maxchain_def)apply (rule Collect_subset)donelemma choice_super:     "[| ch ∈ (Π X ∈ Pow(chain(S)) - {0}. X); X ∈ chain(S);  X ∉ maxchain(S) |]      ==> ch ` super(S,X) ∈ super(S,X)"apply (erule apply_type)apply (unfold super_def maxchain_def, blast)donelemma choice_not_equals:     "[| ch ∈ (Π X ∈ Pow(chain(S)) - {0}. X); X ∈ chain(S);  X ∉ maxchain(S) |]      ==> ch ` super(S,X) ≠ X"apply (rule notI)apply (drule choice_super, assumption, assumption)apply (simp add: super_def)donetext{*This justifies Definition 4.4*}lemma Hausdorff_next_exists:     "ch ∈ (Π X ∈ Pow(chain(S))-{0}. X) ==>      ∃next ∈ increasing(S). ∀X ∈ Pow(S).                   next`X = if(X ∈ chain(S)-maxchain(S), ch`super(S,X), X)"apply (rule_tac x="λX∈Pow(S).                   if X ∈ chain(S) - maxchain(S) then ch ` super(S, X) else X"       in bexI)apply forceapply (unfold increasing_def)apply (rule CollectI)apply (rule lam_type)apply (simp (no_asm_simp))apply (blast dest: super_subset_chain [THEN subsetD]                    chain_subset_Pow [THEN subsetD] choice_super)txt{*Now, verify that it increases*}apply (simp (no_asm_simp) add: Pow_iff subset_refl)apply safeapply (drule choice_super)apply (assumption+)apply (simp add: super_def, blast)donetext{*Lemma 4*}lemma TFin_chain_lemma4:     "[| c ∈ TFin(S,next);         ch ∈ (Π X ∈ Pow(chain(S))-{0}. X);         next ∈ increasing(S);         ∀X ∈ Pow(S). next`X =                          if(X ∈ chain(S)-maxchain(S), ch`super(S,X), X) |]     ==> c ∈ chain(S)"apply (erule TFin_induct)apply (simp (no_asm_simp) add: chain_subset_Pow [THEN subsetD, THEN PowD]            choice_super [THEN super_subset_chain [THEN subsetD]])apply (unfold chain_def)apply (rule CollectI, blast, safe)apply (rule_tac m1=B and n1=Ba in TFin_subset_linear [THEN disjE], fast+)      txt{*@{text "Blast_tac's"} slow*}donetheorem Hausdorff: "∃c. c ∈ maxchain(S)"apply (rule AC_Pi_Pow [THEN exE])apply (rule Hausdorff_next_exists [THEN bexE], assumption)apply (rename_tac ch "next")apply (subgoal_tac "\<Union>(TFin (S,next)) ∈ chain (S) ")prefer 2 apply (blast intro!: TFin_chain_lemma4 subset_refl [THEN TFin_UnionI])apply (rule_tac x = "\<Union>(TFin (S,next))" in exI)apply (rule classical)apply (subgoal_tac "next ` Union(TFin (S,next)) = \<Union>(TFin (S,next))")apply (rule_tac [2] equal_next_Union [THEN iffD2, symmetric])apply (rule_tac [2] subset_refl [THEN TFin_UnionI])prefer 2 apply assumptionapply (rule_tac [2] refl)apply (simp add: subset_refl [THEN TFin_UnionI,                              THEN TFin.dom_subset [THEN subsetD, THEN PowD]])apply (erule choice_not_equals [THEN notE])apply (assumption+)donesubsection{*Zorn's Lemma: If All Chains in S Have Upper Bounds In S,       then S contains a Maximal Element*}text{*Used in the proof of Zorn's Lemma*}lemma chain_extend:    "[| c ∈ chain(A);  z ∈ A;  ∀x ∈ c. x<=z |] ==> cons(z,c) ∈ chain(A)"by (unfold chain_def, blast)lemma Zorn: "∀c ∈ chain(S). \<Union>(c) ∈ S ==> ∃y ∈ S. ∀z ∈ S. y<=z --> y=z"apply (rule Hausdorff [THEN exE])apply (simp add: maxchain_def)apply (rename_tac c)apply (rule_tac x = "\<Union>(c)" in bexI)prefer 2 apply blastapply safeapply (rename_tac z)apply (rule classical)apply (subgoal_tac "cons (z,c) ∈ super (S,c) ")apply (blast elim: equalityE)apply (unfold super_def, safe)apply (fast elim: chain_extend)apply (fast elim: equalityE)donetext {* 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 assumptionapply clarifyapply rule apply assumptionapply ruleapply (rule ccontr)apply (frule_tac z=z in chain_extend)  apply (assumption, blast)apply (unfold maxchain_def super_def)apply (blast elim!: equalityCE)donesubsection{*Zermelo's Theorem: Every Set can be Well-Ordered*}text{*Lemma 5*}lemma TFin_well_lemma5:     "[| n ∈ TFin(S,next);  Z ⊆ TFin(S,next);  z:Z;  ~ \<Inter>(Z) ∈ Z |]      ==> ∀m ∈ Z. n ⊆ m"apply (erule TFin_induct)prefer 2 apply blast txt{*second induction step is easy*}apply (rule ballI)apply (rule bspec [THEN TFin_subsetD, THEN disjE], auto)apply (subgoal_tac "m = \<Inter>(Z) ")apply blast+donetext{*Well-ordering of @{term "TFin(S,next)"} *}lemma well_ord_TFin_lemma: "[| Z ⊆ TFin(S,next);  z ∈ Z |] ==> \<Inter>(Z) ∈ Z"apply (rule classical)apply (subgoal_tac "Z = {\<Union>(TFin (S,next))}")apply (simp (no_asm_simp) add: Inter_singleton)apply (erule equal_singleton)apply (rule Union_upper [THEN equalityI])apply (rule_tac [2] subset_refl [THEN TFin_UnionI, THEN TFin_well_lemma5, THEN bspec], blast+)donetext{*This theorem just packages the previous result*}lemma well_ord_TFin:     "next ∈ increasing(S)       ==> well_ord(TFin(S,next), Subset_rel(TFin(S,next)))"apply (rule well_ordI)apply (unfold Subset_rel_def linear_def)txt{*Prove the well-foundedness goal*}apply (rule wf_onI)apply (frule well_ord_TFin_lemma, assumption)apply (drule_tac x = "\<Inter>(Z) " in bspec, assumption)apply blasttxt{*Now prove the linearity goal*}apply (intro ballI)apply (case_tac "x=y") apply blasttxt{*The @{term "x≠y"} case remains*}apply (rule_tac n1=x and m1=y in TFin_subset_linear [THEN disjE],       assumption+, blast+)donetext{** Defining the "next" operation for Zermelo's Theorem **}lemma choice_Diff:     "[| ch ∈ (Π X ∈ Pow(S) - {0}. X);  X ⊆ S;  X≠S |] ==> ch ` (S-X) ∈ S-X"apply (erule apply_type)apply (blast elim!: equalityE)donetext{*This justifies Definition 6.1*}lemma Zermelo_next_exists:     "ch ∈ (Π X ∈ Pow(S)-{0}. X) ==>           ∃next ∈ increasing(S). ∀X ∈ Pow(S).                      next`X = (if X=S then S else cons(ch`(S-X), X))"apply (rule_tac x="λX∈Pow(S). if X=S then S else cons(ch`(S-X), X)"       in bexI)apply forceapply (unfold increasing_def)apply (rule CollectI)apply (rule lam_type)txt{*Type checking is surprisingly hard!*}apply (simp (no_asm_simp) add: Pow_iff cons_subset_iff subset_refl)apply (blast intro!: choice_Diff [THEN DiffD1])txt{*Verify that it increases*}apply (intro allI impI)apply (simp add: Pow_iff subset_consI subset_refl)donetext{*The construction of the injection*}lemma choice_imp_injection:     "[| ch ∈ (Π X ∈ Pow(S)-{0}. X);         next ∈ increasing(S);         ∀X ∈ Pow(S). next`X = if(X=S, S, cons(ch`(S-X), X)) |]      ==> (λ x ∈ S. \<Union>({y ∈ TFin(S,next). x ∉ y}))               ∈ inj(S, TFin(S,next) - {S})"apply (rule_tac d = "%y. ch` (S-y) " in lam_injective)apply (rule DiffI)apply (rule Collect_subset [THEN TFin_UnionI])apply (blast intro!: Collect_subset [THEN TFin_UnionI] elim: equalityE)apply (subgoal_tac "x ∉ \<Union>({y ∈ TFin (S,next) . x ∉ y}) ")prefer 2 apply (blast elim: equalityE)apply (subgoal_tac "\<Union>({y ∈ TFin (S,next) . x ∉ y}) ≠ S")prefer 2 apply (blast elim: equalityE)txt{*For proving @{text "x ∈ next`\<Union>(...)"}.  Abrial and Laffitte's justification appears to be faulty.*}apply (subgoal_tac "~ next ` Union({y ∈ TFin (S,next) . x ∉ y})                     ⊆ \<Union>({y ∈ TFin (S,next) . x ∉ y}) ") prefer 2 apply (simp del: Union_iff             add: Collect_subset [THEN TFin_UnionI, THEN TFin_is_subset]             Pow_iff cons_subset_iff subset_refl choice_Diff [THEN DiffD2])apply (subgoal_tac "x ∈ next ` Union({y ∈ TFin (S,next) . x ∉ y}) ") prefer 2 apply (blast intro!: Collect_subset [THEN TFin_UnionI] TFin.nextI)txt{*End of the lemmas!*}apply (simp add: Collect_subset [THEN TFin_UnionI, THEN TFin_is_subset])donetext{*The wellordering theorem*}theorem AC_well_ord: "∃r. well_ord(S,r)"apply (rule AC_Pi_Pow [THEN exE])apply (rule Zermelo_next_exists [THEN bexE], assumption)apply (rule exI)apply (rule well_ord_rvimage)apply (erule_tac [2] well_ord_TFin)apply (rule choice_imp_injection [THEN inj_weaken_type], blast+)donesubsection {* Zorn's Lemma for Partial Orders *}text {* Reimported from HOL by Clemens Ballarin. *}definition Chain :: "i => i" where  "Chain(r) = {A ∈ Pow(field(r)). ∀a∈A. ∀b∈A. <a, b> ∈ r | <b, a> ∈ r}"lemma mono_Chain:  "r ⊆ s ==> Chain(r) ⊆ Chain(s)"  unfolding Chain_def  by blasttheorem Zorn_po:  assumes po: "Partial_order(r)"    and u: "∀C∈Chain(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∈field(r). r -`` {x}" let ?S = "?B `` field(r)"  have "∀C∈chain(?S). ∃U∈?S. ∀A∈C. A ⊆ U"  proof (clarsimp simp: chain_def Subset_rel_def bex_image_simp)    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      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 "<a, b> ∈ r | <b, a> ∈ 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)" "∀a∈?A. <a, u> ∈ r"      using u      apply auto      apply (drule bspec) apply assumption      apply auto      done    have "∀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 "<a, u> ∈ r" using uA aB `Preorder(r)`        by (auto simp: preorder_on_def refl_def) (blast dest: trans_onD)+    qed    then show "∃U∈field(r). ∀A∈C. A ⊆ r -`` {U}"      using `u ∈ field(r)` ..  qed  from Zorn2 [OF this]  obtain m B where "m ∈ field(r)" "B = r -`` {m}"    "∀x∈field(r). B ⊆ r -`` {x} --> B = r -`` {x}"    by (auto elim!: lamE simp: ball_image_simp)  then have "∀a∈field(r). <m, a> ∈ 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 blastqedend`