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 "c = {}")
      txt ‹If ‹c› is an empty chain, then every element in ‹S› is an upper
        bound of ‹c›.›
      case True
      with aS show ?thesis by fast
    next
      txt ‹If ‹c› is non-empty, then ‹⋃c› is an upper bound of ‹c›, lying in
        ‹S›.›
      case False
      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