Theory Zorn_Lemma

(*  Title:      HOL/Hahn_Banach/Zorn_Lemma.thy
    Author:     Gertrud Bauer, TU Munich
*)

section ‹Zorn's Lemma›

theory Zorn_Lemma
imports Main
begin

text ‹
  Zorn's Lemmas states: if every linear ordered subset of an ordered set ‹S›
  has an upper bound in ‹S›, then there exists a maximal element in ‹S›. In
  our application, ‹S› is a set of sets ordered by set inclusion. Since the
  union of a chain of sets is an upper bound for all elements of the chain,
  the conditions of Zorn's lemma can be modified: if ‹S› is non-empty, it
  suffices to show that for every non-empty chain ‹c› in ‹S› the union of ‹c›
  also lies in ‹S›.
›

theorem Zorn's_Lemma:
  assumes r: "⋀c. c ∈ chains S ⟹ ∃x. x ∈ c ⟹ ⋃c ∈ S"
    and aS: "a ∈ S"
  shows "∃y ∈ S. ∀z ∈ S. y ⊆ z ⟶ z = y"
proof (rule Zorn_Lemma2)
  show "∀c ∈ chains S. ∃y ∈ S. ∀z ∈ c. z ⊆ y"
  proof
    fix c assume "c ∈ chains S"
    show "∃y ∈ S. ∀z ∈ c. z ⊆ y"
    proof cases
      txt ‹If ‹c› is an empty chain, then every element in ‹S› is an upper
        bound of ‹c›.›

      assume "c = {}"
      with aS show ?thesis by fast

      txt ‹If ‹c› is non-empty, then ‹⋃c› is an upper bound of ‹c›, lying in
        ‹S›.›
    next
      assume "c ≠ {}"
      show ?thesis
      proof
        show "∀z ∈ c. z ⊆ ⋃c" by fast
        show "⋃c ∈ S"
        proof (rule r)
          from ‹c ≠ {}› show "∃x. x ∈ c" by fast
          show "c ∈ chains S" by fact
        qed
      qed
    qed
  qed
qed

end