Theory Zorn

(*  Title:      ZF/Zorn.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1994  University of Cambridge
*)

sectionZorn's Lemma

theory Zorn imports OrderArith AC Inductive begin

textBased upon the unpublished article ``Towards the Mechanization of the
Proofs of Some Classical Theorems of Set Theory,'' by Abrial and Laffitte.

definition
  Subset_rel :: "ii"  where
   "Subset_rel(A)  {z  A*A . x y. z=x,y  x<=y  xy}"

definition
  chain      :: "ii"  where
   "chain(A)       {F  Pow(A). XF. YF. X<=Y | Y<=X}"

definition
  super      :: "[i,i]i"  where
   "super(A,c)     {d  chain(A). c<=d  cd}"

definition
  maxchain   :: "ii"  where
   "maxchain(A)    {c  chain(A). super(A,c)=0}"

definition
  increasing :: "ii"  where
    "increasing(A)  {f  Pow(A)->Pow(A). x. x<=A  x<=f`x}"


textLemma for the inductive definition below
lemma Union_in_Pow: "Y  Pow(Pow(A))  (Y)  Pow(A)"
by blast


textWe could make the inductive definition conditional on
    termnext  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))  (Y)  TFin(S,next)"

  monos         Pow_mono
  con_defs      increasing_def
  type_intros   CollectD1 [THEN apply_funtype] Union_in_Pow


subsectionMathematical Preamble

lemma Union_lemma0: "(xC. x<=A | B<=x)  (C)<=A | B<=(C)"
by blast

lemma Inter_lemma0:
     "c  C; xC. A<=x | x<=B  A  (C) | (C)  B"
by blast


subsectionThe Transfinite Construction

lemma increasingD1: "f  increasing(A)  f  Pow(A)->Pow(A)"
  unfolding increasing_def
apply (erule CollectD1)
done

lemma 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]


textStructural induction on termTFin(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);  yY. P(y)  P((Y))
  P(n)"
by (erule TFin.induct, blast+)


subsectionSome Properties of the Transfinite Construction

lemmas increasing_trans = subset_trans [OF _ increasingD2,
                                        OF _ _ TFin_is_subset]

textLemma 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)
done

textLemma 2 of section 3.2.  Interesting in its own right!
  Requires termnext  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])
txtcase split using 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)
txtsecond induction step
apply (rule impI [THEN ballI])
apply (rule Union_lemma0 [THEN disjE])
apply (erule_tac [3] disjI2)
prefer 2 apply blast
apply (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)+
done

texta 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])

textConsequences 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)
done


textLemma 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)
done

textProperty 3.3 of section 3.3
lemma equal_next_Union:
     "m  TFin(S,next);  next  increasing(S)
       m = next`m <-> m = (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)+
done


subsectionHausdorff's Theorem: Every Set Contains a Maximal Chain

textNOTE: We assume the partial ordering is ⊆›, the subset
relation!

text* Defining the "next" operation for Hausdorff's Theorem *

lemma chain_subset_Pow: "chain(A)  Pow(A)"
  unfolding chain_def
apply (rule Collect_subset)
done

lemma super_subset_chain: "super(A,c)  chain(A)"
  unfolding super_def
apply (rule Collect_subset)
done

lemma maxchain_subset_chain: "maxchain(A)  chain(A)"
  unfolding maxchain_def
apply (rule Collect_subset)
done

lemma 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)
done

lemma 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)
done

textThis 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="λXPow(S).
                   if X  chain(S) - maxchain(S) then ch ` super(S, X) else X"
       in bexI)
apply force
  unfolding 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)
txtNow, verify that it increases
apply (simp (no_asm_simp) add: Pow_iff subset_refl)
apply safe
apply (drule choice_super)
apply (assumption+)
apply (simp add: super_def, blast)
done

textLemma 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]])
  unfolding chain_def
apply (rule CollectI, blast, safe)
apply (rule_tac m1=B and n1=Ba in TFin_subset_linear [THEN disjE], fast+)
      txtBlast_tac's› slow
done

theorem 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 "(TFin (S,next))  chain (S) ")
prefer 2
 apply (blast intro!: TFin_chain_lemma4 subset_refl [THEN TFin_UnionI])
apply (rule_tac x = "(TFin (S,next))" in exI)
apply (rule classical)
apply (subgoal_tac "next ` Union(TFin (S,next)) = (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 assumption
apply (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+)
done


subsectionZorn's Lemma: If All Chains in S Have Upper Bounds In S,
       then S contains a Maximal Element

textUsed 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). (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 = "(c)" in bexI)
prefer 2 apply blast
apply safe
apply (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)
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)
  unfolding maxchain_def super_def
apply (blast elim!: equalityCE)
done


subsectionZermelo's Theorem: Every Set can be Well-Ordered

textLemma 5
lemma TFin_well_lemma5:
     "n  TFin(S,next);  Z  TFin(S,next);  z:Z;  ¬ (Z)  Z
       m  Z. n  m"
apply (erule TFin_induct)
prefer 2 apply blast txtsecond induction step is easy
apply (rule ballI)
apply (rule bspec [THEN TFin_subsetD, THEN disjE], auto)
apply (subgoal_tac "m = (Z) ")
apply blast+
done

textWell-ordering of termTFin(S,next)
lemma well_ord_TFin_lemma: "Z  TFin(S,next);  z  Z  (Z)  Z"
apply (rule classical)
apply (subgoal_tac "Z = {(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+)
done

textThis 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)
  unfolding Subset_rel_def linear_def
txtProve the well-foundedness goal
apply (rule wf_onI)
apply (frule well_ord_TFin_lemma, assumption)
apply (drule_tac x = "(Z) " in bspec, assumption)
apply blast
txtNow prove the linearity goal
apply (intro ballI)
apply (case_tac "x=y")
 apply blast
txtThe termxy case remains
apply (rule_tac n1=x and m1=y in TFin_subset_linear [THEN disjE],
       assumption+, blast+)
done

text* Defining the "next" operation for Zermelo's Theorem *

lemma choice_Diff:
     "ch  (X  Pow(S) - {0}. X);  X  S;  XS  ch ` (S-X)  S-X"
apply (erule apply_type)
apply (blast elim!: equalityE)
done

textThis 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="λXPow(S). if X=S then S else cons(ch`(S-X), X)"
       in bexI)
apply force
  unfolding increasing_def
apply (rule CollectI)
apply (rule lam_type)
txtType checking is surprisingly hard!
apply (simp (no_asm_simp) add: Pow_iff cons_subset_iff subset_refl)
apply (blast intro!: choice_Diff [THEN DiffD1])
txtVerify that it increases
apply (intro allI impI)
apply (simp add: Pow_iff subset_consI subset_refl)
done


textThe 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. ({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  ({y  TFin (S,next) . x  y}) ")
prefer 2 apply (blast elim: equalityE)
apply (subgoal_tac "({y  TFin (S,next) . x  y})  S")
prefer 2 apply (blast elim: equalityE)
txtFor proving x ∈ next`⋃(...)›.
  Abrial and Laffitte's justification appears to be faulty.
apply (subgoal_tac "¬ next ` Union({y  TFin (S,next) . x  y}) 
                     ({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)
txtEnd of the lemmas!
apply (simp add: Collect_subset [THEN TFin_UnionI, THEN TFin_is_subset])
done

textThe 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+)
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)). aA. bA. a, b  r | b, a  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: "CChain(r). ufield(r). aC. a, u  r"
  shows "mfield(r). afield(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 = "λxfield(r). r -`` {x}" let ?S = "?B `` field(r)"
  have "Cchain(?S). U?S. AC. A  U"
  proof (clarsimp simp: chain_def Subset_rel_def bex_image_simp)
    fix C
    assume 1: "C  ?S" and 2: "AC. BC. A  B | B  A"
    let ?A = "{x  field(r). MC. 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" for 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 "AC. 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 "Ufield(r). AC. A  r -`` {U}"
      using u  field(r) ..
  qed
  from Zorn2 [OF this]
  obtain m B where "m  field(r)" "B = r -`` {m}"
    "xfield(r). B  r -`` {x}  B = r -`` {x}"
    by (auto elim!: lamE simp: ball_image_simp)
  then have "afield(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 blast
qed

end