# Theory Zorn

```(*  Title:       HOL/Zorn.thy
Author:      Jacques D. Fleuriot
Author:      Tobias Nipkow, TUM
Author:      Christian Sternagel, JAIST

Zorn's Lemma (ported from Larry Paulson's Zorn.thy in ZF).
*)

section ‹Zorn's Lemma and the Well-ordering Theorem›

theory Zorn
imports Order_Relation Hilbert_Choice
begin

subsection ‹Zorn's Lemma for the Subset Relation›

subsubsection ‹Results that do not require an order›

text ‹Let ‹P› be a binary predicate on the set ‹A›.›
locale pred_on =
fixes A :: "'a set"
and P :: "'a ⇒ 'a ⇒ bool"  (infix "⊏" 50)
begin

abbreviation Peq :: "'a ⇒ 'a ⇒ bool"  (infix "⊑" 50)
where "x ⊑ y ≡ P⇧=⇧= x y"

text ‹A chain is a totally ordered subset of ‹A›.›
definition chain :: "'a set ⇒ bool"
where "chain C ⟷ C ⊆ A ∧ (∀x∈C. ∀y∈C. x ⊑ y ∨ y ⊑ x)"

text ‹
We call a chain that is a proper superset of some set ‹X›,
but not necessarily a chain itself, a superchain of ‹X›.
›
abbreviation superchain :: "'a set ⇒ 'a set ⇒ bool"  (infix "<c" 50)
where "X <c C ≡ chain C ∧ X ⊂ C"

text ‹A maximal chain is a chain that does not have a superchain.›
definition maxchain :: "'a set ⇒ bool"
where "maxchain C ⟷ chain C ∧ (∄S. C <c S)"

text ‹
We define the successor of a set to be an arbitrary
superchain, if such exists, or the set itself, otherwise.
›
definition suc :: "'a set ⇒ 'a set"
where "suc C = (if ¬ chain C ∨ maxchain C then C else (SOME D. C <c D))"

lemma chainI [Pure.intro?]: "C ⊆ A ⟹ (⋀x y. x ∈ C ⟹ y ∈ C ⟹ x ⊑ y ∨ y ⊑ x) ⟹ chain C"
unfolding chain_def by blast

lemma chain_total: "chain C ⟹ x ∈ C ⟹ y ∈ C ⟹ x ⊑ y ∨ y ⊑ x"
by (simp add: chain_def)

lemma not_chain_suc [simp]: "¬ chain X ⟹ suc X = X"
by (simp add: suc_def)

lemma maxchain_suc [simp]: "maxchain X ⟹ suc X = X"
by (simp add: suc_def)

lemma suc_subset: "X ⊆ suc X"
by (auto simp: suc_def maxchain_def intro: someI2)

lemma chain_empty [simp]: "chain {}"
by (auto simp: chain_def)

lemma not_maxchain_Some: "chain C ⟹ ¬ maxchain C ⟹ C <c (SOME D. C <c D)"
by (rule someI_ex) (auto simp: maxchain_def)

lemma suc_not_equals: "chain C ⟹ ¬ maxchain C ⟹ suc C ≠ C"
using not_maxchain_Some by (auto simp: suc_def)

lemma subset_suc:
assumes "X ⊆ Y"
shows "X ⊆ suc Y"
using assms by (rule subset_trans) (rule suc_subset)

text ‹
We build a set \<^term>‹𝒞› that is closed under applications
of \<^term>‹suc› and contains the union of all its subsets.
›
inductive_set suc_Union_closed ("𝒞")
where
suc: "X ∈ 𝒞 ⟹ suc X ∈ 𝒞"
| Union [unfolded Pow_iff]: "X ∈ Pow 𝒞 ⟹ ⋃X ∈ 𝒞"

text ‹
Since the empty set as well as the set itself is a subset of
every set, \<^term>‹𝒞› contains at least \<^term>‹{} ∈ 𝒞› and
\<^term>‹⋃𝒞 ∈ 𝒞›.
›
lemma suc_Union_closed_empty: "{} ∈ 𝒞"
and suc_Union_closed_Union: "⋃𝒞 ∈ 𝒞"
using Union [of "{}"] and Union [of "𝒞"] by simp_all

text ‹Thus closure under \<^term>‹suc› will hit a maximal chain
eventually, as is shown below.›

lemma suc_Union_closed_induct [consumes 1, case_names suc Union, induct pred: suc_Union_closed]:
assumes "X ∈ 𝒞"
and "⋀X. X ∈ 𝒞 ⟹ Q X ⟹ Q (suc X)"
and "⋀X. X ⊆ 𝒞 ⟹ ∀x∈X. Q x ⟹ Q (⋃X)"
shows "Q X"
using assms by induct blast+

lemma suc_Union_closed_cases [consumes 1, case_names suc Union, cases pred: suc_Union_closed]:
assumes "X ∈ 𝒞"
and "⋀Y. X = suc Y ⟹ Y ∈ 𝒞 ⟹ Q"
and "⋀Y. X = ⋃Y ⟹ Y ⊆ 𝒞 ⟹ Q"
shows "Q"
using assms by cases simp_all

text ‹On chains, \<^term>‹suc› yields a chain.›
lemma chain_suc:
assumes "chain X"
shows "chain (suc X)"
using assms
by (cases "¬ chain X ∨ maxchain X") (force simp: suc_def dest: not_maxchain_Some)+

lemma chain_sucD:
assumes "chain X"
shows "suc X ⊆ A ∧ chain (suc X)"
proof -
from ‹chain X› have *: "chain (suc X)"
by (rule chain_suc)
then have "suc X ⊆ A"
unfolding chain_def by blast
with * show ?thesis by blast
qed

lemma suc_Union_closed_total':
assumes "X ∈ 𝒞" and "Y ∈ 𝒞"
and *: "⋀Z. Z ∈ 𝒞 ⟹ Z ⊆ Y ⟹ Z = Y ∨ suc Z ⊆ Y"
shows "X ⊆ Y ∨ suc Y ⊆ X"
using ‹X ∈ 𝒞›
proof induct
case (suc X)
with * show ?case by (blast del: subsetI intro: subset_suc)
next
case Union
then show ?case by blast
qed

lemma suc_Union_closed_subsetD:
assumes "Y ⊆ X" and "X ∈ 𝒞" and "Y ∈ 𝒞"
shows "X = Y ∨ suc Y ⊆ X"
using assms(2,3,1)
proof (induct arbitrary: Y)
case (suc X)
note * = ‹⋀Y. Y ∈ 𝒞 ⟹ Y ⊆ X ⟹ X = Y ∨ suc Y ⊆ X›
with suc_Union_closed_total' [OF ‹Y ∈ 𝒞› ‹X ∈ 𝒞›]
have "Y ⊆ X ∨ suc X ⊆ Y" by blast
then show ?case
proof
assume "Y ⊆ X"
with * and ‹Y ∈ 𝒞› subset_suc show ?thesis
by fastforce
next
assume "suc X ⊆ Y"
with ‹Y ⊆ suc X› show ?thesis by blast
qed
next
case (Union X)
show ?case
proof (rule ccontr)
assume "¬ ?thesis"
with ‹Y ⊆ ⋃X› obtain x y z
where "¬ suc Y ⊆ ⋃X"
and "x ∈ X" and "y ∈ x" and "y ∉ Y"
and "z ∈ suc Y" and "∀x∈X. z ∉ x" by blast
with ‹X ⊆ 𝒞› have "x ∈ 𝒞" by blast
from Union and ‹x ∈ X› have *: "⋀y. y ∈ 𝒞 ⟹ y ⊆ x ⟹ x = y ∨ suc y ⊆ x"
by blast
with suc_Union_closed_total' [OF ‹Y ∈ 𝒞› ‹x ∈ 𝒞›] have "Y ⊆ x ∨ suc x ⊆ Y"
by blast
then show False
proof
assume "Y ⊆ x"
with * [OF ‹Y ∈ 𝒞›] ‹y ∈ x› ‹y ∉ Y› ‹x ∈ X› ‹¬ suc Y ⊆ ⋃X› show False
by blast
next
assume "suc x ⊆ Y"
with ‹y ∉ Y› suc_subset ‹y ∈ x› show False by blast
qed
qed
qed

text ‹The elements of \<^term>‹𝒞› are totally ordered by the subset relation.›
lemma suc_Union_closed_total:
assumes "X ∈ 𝒞" and "Y ∈ 𝒞"
shows "X ⊆ Y ∨ Y ⊆ X"
proof (cases "∀Z∈𝒞. Z ⊆ Y ⟶ Z = Y ∨ suc Z ⊆ Y")
case True
with suc_Union_closed_total' [OF assms]
have "X ⊆ Y ∨ suc Y ⊆ X" by blast
with suc_subset [of Y] show ?thesis by blast
next
case False
then obtain Z where "Z ∈ 𝒞" and "Z ⊆ Y" and "Z ≠ Y" and "¬ suc Z ⊆ Y"
by blast
with suc_Union_closed_subsetD and ‹Y ∈ 𝒞› show ?thesis
by blast
qed

text ‹Once we hit a fixed point w.r.t. \<^term>‹suc›, all other elements
of \<^term>‹𝒞› are subsets of this fixed point.›
lemma suc_Union_closed_suc:
assumes "X ∈ 𝒞" and "Y ∈ 𝒞" and "suc Y = Y"
shows "X ⊆ Y"
using ‹X ∈ 𝒞›
proof induct
case (suc X)
with ‹Y ∈ 𝒞› and suc_Union_closed_subsetD have "X = Y ∨ suc X ⊆ Y"
by blast
then show ?case
by (auto simp: ‹suc Y = Y›)
next
case Union
then show ?case by blast
qed

lemma eq_suc_Union:
assumes "X ∈ 𝒞"
shows "suc X = X ⟷ X = ⋃𝒞"
(is "?lhs ⟷ ?rhs")
proof
assume ?lhs
then have "⋃𝒞 ⊆ X"
by (rule suc_Union_closed_suc [OF suc_Union_closed_Union ‹X ∈ 𝒞›])
with ‹X ∈ 𝒞› show ?rhs
by blast
next
from ‹X ∈ 𝒞› have "suc X ∈ 𝒞" by (rule suc)
then have "suc X ⊆ ⋃𝒞" by blast
moreover assume ?rhs
ultimately have "suc X ⊆ X" by simp
moreover have "X ⊆ suc X" by (rule suc_subset)
ultimately show ?lhs ..
qed

lemma suc_in_carrier:
assumes "X ⊆ A"
shows "suc X ⊆ A"
using assms
by (cases "¬ chain X ∨ maxchain X") (auto dest: chain_sucD)

lemma suc_Union_closed_in_carrier:
assumes "X ∈ 𝒞"
shows "X ⊆ A"
using assms
by induct (auto dest: suc_in_carrier)

text ‹All elements of \<^term>‹𝒞› are chains.›
lemma suc_Union_closed_chain:
assumes "X ∈ 𝒞"
shows "chain X"
using assms
proof induct
case (suc X)
then show ?case
using not_maxchain_Some by (simp add: suc_def)
next
case (Union X)
then have "⋃X ⊆ A"
by (auto dest: suc_Union_closed_in_carrier)
moreover have "∀x∈⋃X. ∀y∈⋃X. x ⊑ y ∨ y ⊑ x"
proof (intro ballI)
fix x y
assume "x ∈ ⋃X" and "y ∈ ⋃X"
then obtain u v where "x ∈ u" and "u ∈ X" and "y ∈ v" and "v ∈ X"
by blast
with Union have "u ∈ 𝒞" and "v ∈ 𝒞" and "chain u" and "chain v"
by blast+
with suc_Union_closed_total have "u ⊆ v ∨ v ⊆ u"
by blast
then show "x ⊑ y ∨ y ⊑ x"
proof
assume "u ⊆ v"
from ‹chain v› show ?thesis
proof (rule chain_total)
show "y ∈ v" by fact
show "x ∈ v" using ‹u ⊆ v› and ‹x ∈ u› by blast
qed
next
assume "v ⊆ u"
from ‹chain u› show ?thesis
proof (rule chain_total)
show "x ∈ u" by fact
show "y ∈ u" using ‹v ⊆ u› and ‹y ∈ v› by blast
qed
qed
qed
ultimately show ?case unfolding chain_def ..
qed

subsubsection ‹Hausdorff's Maximum Principle›

text ‹There exists a maximal totally ordered subset of ‹A›. (Note that we do not
require ‹A› to be partially ordered.)›

theorem Hausdorff: "∃C. maxchain C"
proof -
let ?M = "⋃𝒞"
have "maxchain ?M"
proof (rule ccontr)
assume "¬ ?thesis"
then have "suc ?M ≠ ?M"
using suc_not_equals and suc_Union_closed_chain [OF suc_Union_closed_Union] by simp
moreover have "suc ?M = ?M"
using eq_suc_Union [OF suc_Union_closed_Union] by simp
ultimately show False by contradiction
qed
then show ?thesis by blast
qed

text ‹Make notation \<^term>‹𝒞› available again.›
no_notation suc_Union_closed  ("𝒞")

lemma chain_extend: "chain C ⟹ z ∈ A ⟹ ∀x∈C. x ⊑ z ⟹ chain ({z} ∪ C)"
unfolding chain_def by blast

lemma maxchain_imp_chain: "maxchain C ⟹ chain C"
by (simp add: maxchain_def)

end

text ‹Hide constant \<^const>‹pred_on.suc_Union_closed›, which was just needed
for the proof of Hausforff's maximum principle.›
hide_const pred_on.suc_Union_closed

lemma chain_mono:
assumes "⋀x y. x ∈ A ⟹ y ∈ A ⟹ P x y ⟹ Q x y"
and "pred_on.chain A P C"
shows "pred_on.chain A Q C"
using assms unfolding pred_on.chain_def by blast

subsubsection ‹Results for the proper subset relation›

interpretation subset: pred_on "A" "(⊂)" for A .

lemma subset_maxchain_max:
assumes "subset.maxchain A C"
and "X ∈ A"
and "⋃C ⊆ X"
shows "⋃C = X"
proof (rule ccontr)
let ?C = "{X} ∪ C"
from ‹subset.maxchain A C› have "subset.chain A C"
and *: "⋀S. subset.chain A S ⟹ ¬ C ⊂ S"
by (auto simp: subset.maxchain_def)
moreover have "∀x∈C. x ⊆ X" using ‹⋃C ⊆ X› by auto
ultimately have "subset.chain A ?C"
using subset.chain_extend [of A C X] and ‹X ∈ A› by auto
moreover assume **: "⋃C ≠ X"
moreover from ** have "C ⊂ ?C" using ‹⋃C ⊆ X› by auto
ultimately show False using * by blast
qed

lemma subset_chain_def: "⋀𝒜. subset.chain 𝒜 𝒞 = (𝒞 ⊆ 𝒜 ∧ (∀X∈𝒞. ∀Y∈𝒞. X ⊆ Y ∨ Y ⊆ X))"
by (auto simp: subset.chain_def)

lemma subset_chain_insert:
"subset.chain 𝒜 (insert B ℬ) ⟷ B ∈ 𝒜 ∧ (∀X∈ℬ. X ⊆ B ∨ B ⊆ X) ∧ subset.chain 𝒜 ℬ"
by (fastforce simp add: subset_chain_def)

subsubsection ‹Zorn's lemma›

text ‹If every chain has an upper bound, then there is a maximal set.›
theorem subset_Zorn:
assumes "⋀C. subset.chain A C ⟹ ∃U∈A. ∀X∈C. X ⊆ U"
shows "∃M∈A. ∀X∈A. M ⊆ X ⟶ X = M"
proof -
from subset.Hausdorff [of A] obtain M where "subset.maxchain A M" ..
then have "subset.chain A M"
by (rule subset.maxchain_imp_chain)
with assms obtain Y where "Y ∈ A" and "∀X∈M. X ⊆ Y"
by blast
moreover have "∀X∈A. Y ⊆ X ⟶ Y = X"
proof (intro ballI impI)
fix X
assume "X ∈ A" and "Y ⊆ X"
show "Y = X"
proof (rule ccontr)
assume "¬ ?thesis"
with ‹Y ⊆ X› have "¬ X ⊆ Y" by blast
from subset.chain_extend [OF ‹subset.chain A M› ‹X ∈ A›] and ‹∀X∈M. X ⊆ Y›
have "subset.chain A ({X} ∪ M)"
using ‹Y ⊆ X› by auto
moreover have "M ⊂ {X} ∪ M"
using ‹∀X∈M. X ⊆ Y› and ‹¬ X ⊆ Y› by auto
ultimately show False
using ‹subset.maxchain A M› by (auto simp: subset.maxchain_def)
qed
qed
ultimately show ?thesis by blast
qed

text ‹Alternative version of Zorn's lemma for the subset relation.›
lemma subset_Zorn':
assumes "⋀C. subset.chain A C ⟹ ⋃C ∈ A"
shows "∃M∈A. ∀X∈A. M ⊆ X ⟶ X = M"
proof -
from subset.Hausdorff [of A] obtain M where "subset.maxchain A M" ..
then have "subset.chain A M"
by (rule subset.maxchain_imp_chain)
with assms have "⋃M ∈ A" .
moreover have "∀Z∈A. ⋃M ⊆ Z ⟶ ⋃M = Z"
proof (intro ballI impI)
fix Z
assume "Z ∈ A" and "⋃M ⊆ Z"
with subset_maxchain_max [OF ‹subset.maxchain A M›]
show "⋃M = Z" .
qed
ultimately show ?thesis by blast
qed

subsection ‹Zorn's Lemma for Partial Orders›

text ‹Relate old to new definitions.›

definition chain_subset :: "'a set set ⇒ bool"  ("chain⇩⊆")  (* Define globally? In Set.thy? *)
where "chain⇩⊆ C ⟷ (∀A∈C. ∀B∈C. A ⊆ B ∨ B ⊆ A)"

definition chains :: "'a set set ⇒ 'a set set set"
where "chains A = {C. C ⊆ A ∧ chain⇩⊆ C}"

definition Chains :: "('a × 'a) set ⇒ 'a set set"  (* Define globally? In Relation.thy? *)
where "Chains r = {C. ∀a∈C. ∀b∈C. (a, b) ∈ r ∨ (b, a) ∈ r}"

lemma chains_extend: "c ∈ chains S ⟹ z ∈ S ⟹ ∀x ∈ c. x ⊆ z ⟹ {z} ∪ c ∈ chains S"
for z :: "'a set"
unfolding chains_def chain_subset_def by blast

lemma mono_Chains: "r ⊆ s ⟹ Chains r ⊆ Chains s"
unfolding Chains_def by blast

lemma chain_subset_alt_def: "chain⇩⊆ C = subset.chain UNIV C"
unfolding chain_subset_def subset.chain_def by fast

lemma chains_alt_def: "chains A = {C. subset.chain A C}"
by (simp add: chains_def chain_subset_alt_def subset.chain_def)

lemma Chains_subset: "Chains r ⊆ {C. pred_on.chain UNIV (λx y. (x, y) ∈ r) C}"
by (force simp add: Chains_def pred_on.chain_def)

lemma Chains_subset':
assumes "refl r"
shows "{C. pred_on.chain UNIV (λx y. (x, y) ∈ r) C} ⊆ Chains r"
using assms
by (auto simp add: Chains_def pred_on.chain_def refl_on_def)

lemma Chains_alt_def:
assumes "refl r"
shows "Chains r = {C. pred_on.chain UNIV (λx y. (x, y) ∈ r) C}"
using assms Chains_subset Chains_subset' by blast

lemma Chains_relation_of:
assumes "C ∈ Chains (relation_of P A)" shows "C ⊆ A"
using assms unfolding Chains_def relation_of_def by auto

lemma pairwise_chain_Union:
assumes P: "⋀S. S ∈ 𝒞 ⟹ pairwise R S" and "chain⇩⊆ 𝒞"
shows "pairwise R (⋃𝒞)"
using ‹chain⇩⊆ 𝒞› unfolding pairwise_def chain_subset_def
by (blast intro: P [unfolded pairwise_def, rule_format])

lemma Zorn_Lemma: "∀C∈chains A. ⋃C ∈ A ⟹ ∃M∈A. ∀X∈A. M ⊆ X ⟶ X = M"
using subset_Zorn' [of A] by (force simp: chains_alt_def)

lemma Zorn_Lemma2: "∀C∈chains A. ∃U∈A. ∀X∈C. X ⊆ U ⟹ ∃M∈A. ∀X∈A. M ⊆ X ⟶ X = M"
using subset_Zorn [of A] by (auto simp: chains_alt_def)

subsection ‹Other variants of Zorn's Lemma›

lemma chainsD: "c ∈ chains S ⟹ x ∈ c ⟹ y ∈ c ⟹ x ⊆ y ∨ y ⊆ x"
unfolding chains_def chain_subset_def by blast

lemma chainsD2: "c ∈ chains S ⟹ c ⊆ S"
unfolding chains_def by blast

lemma Zorns_po_lemma:
assumes po: "Partial_order r"
and u: "⋀C. C ∈ Chains 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)
txt ‹Mirror ‹r› in the set of subsets below (wrt ‹r›) elements of ‹A›.›
let ?B = "λx. r¯ `` {x}"
let ?S = "?B ` Field r"
have "∃u∈Field r. ∀A∈C. A ⊆ r¯ `` {u}"  (is "∃u∈Field r. ?P u")
if 1: "C ⊆ ?S" and 2: "∀A∈C. ∀B∈C. A ⊆ B ∨ B ⊆ A" for C
proof -
let ?A = "{x∈Field r. ∃M∈C. M = ?B x}"
from 1 have "C = ?B ` ?A" by (auto simp: image_def)
have "?A ∈ Chains r"
proof (simp add: Chains_def, intro allI impI, elim conjE)
fix a b
assume "a ∈ Field r" and "?B a ∈ C" and "b ∈ Field r" and "?B b ∈ C"
with 2 have "?B a ⊆ ?B b ∨ ?B b ⊆ ?B a" by auto
then show "(a, b) ∈ r ∨ (b, a) ∈ r"
using ‹Preorder r› and ‹a ∈ Field r› and ‹b ∈ Field r›
qed
then obtain u where uA: "u ∈ Field r" "∀a∈?A. (a, u) ∈ r"
by (auto simp: dest: u)
have "?P u"
proof auto
fix a B assume aB: "B ∈ C" "a ∈ B"
with 1 obtain x where "x ∈ Field r" and "B = r¯ `` {x}" by auto
then show "(a, u) ∈ r"
using uA and aB and ‹Preorder r›
unfolding preorder_on_def refl_on_def by simp (fast dest: transD)
qed
then show ?thesis
using ‹u ∈ Field r› by blast
qed
then have "∀C∈chains ?S. ∃U∈?S. ∀A∈C. A ⊆ U"
by (auto simp: chains_def chain_subset_def)
from Zorn_Lemma2 [OF this] obtain m B
where "m ∈ Field r"
and "B = r¯ `` {m}"
and "∀x∈Field r. B ⊆ r¯ `` {x} ⟶ r¯ `` {x} = B"
by auto
then have "∀a∈Field r. (m, a) ∈ r ⟶ a = m"
using po and ‹Preorder r› and ‹m ∈ Field r›
by (auto simp: subset_Image1_Image1_iff Partial_order_eq_Image1_Image1_iff)
then show ?thesis
using ‹m ∈ Field r› by blast
qed

lemma predicate_Zorn:
assumes po: "partial_order_on A (relation_of P A)"
and ch: "⋀C. C ∈ Chains (relation_of P A) ⟹ ∃u ∈ A. ∀a ∈ C. P a u"
shows "∃m ∈ A. ∀a ∈ A. P m a ⟶ a = m"
proof -
have "a ∈ A" if "C ∈ Chains (relation_of P A)" and "a ∈ C" for C a
using that unfolding Chains_def relation_of_def by auto
moreover have "(a, u) ∈ relation_of P A" if "a ∈ A" and "u ∈ A" and "P a u" for a u
unfolding relation_of_def using that by auto
ultimately have "∃m∈A. ∀a∈A. (m, a) ∈ relation_of P A ⟶ a = m"
using Zorns_po_lemma[OF Partial_order_relation_ofI[OF po], rule_format] ch
unfolding Field_relation_of[OF partial_order_onD(1)[OF po]] by blast
then show ?thesis
by (auto simp: relation_of_def)
qed

lemma Union_in_chain: "⟦finite ℬ; ℬ ≠ {}; subset.chain 𝒜 ℬ⟧ ⟹ ⋃ℬ ∈ ℬ"
proof (induction ℬ rule: finite_induct)
case (insert B ℬ)
show ?case
proof (cases "ℬ = {}")
case False
then show ?thesis
using insert sup.absorb2 by (auto simp: subset_chain_insert dest!: bspec [where x="⋃ℬ"])
qed auto
qed simp

lemma Inter_in_chain: "⟦finite ℬ; ℬ ≠ {}; subset.chain 𝒜 ℬ⟧ ⟹ ⋂ℬ ∈ ℬ"
proof (induction ℬ rule: finite_induct)
case (insert B ℬ)
show ?case
proof (cases "ℬ = {}")
case False
then show ?thesis
using insert inf.absorb2 by (auto simp: subset_chain_insert dest!: bspec [where x="⋂ℬ"])
qed auto
qed simp

lemma finite_subset_Union_chain:
assumes "finite A" "A ⊆ ⋃ℬ" "ℬ ≠ {}" and sub: "subset.chain 𝒜 ℬ"
obtains B where "B ∈ ℬ" "A ⊆ B"
proof -
obtain ℱ where ℱ: "finite ℱ" "ℱ ⊆ ℬ" "A ⊆ ⋃ℱ"
using assms by (auto intro: finite_subset_Union)
show thesis
proof (cases "ℱ = {}")
case True
then show ?thesis
using ‹A ⊆ ⋃ℱ› ‹ℬ ≠ {}› that by fastforce
next
case False
show ?thesis
proof
show "⋃ℱ ∈ ℬ"
using sub ‹ℱ ⊆ ℬ› ‹finite ℱ›
by (simp add: Union_in_chain False subset.chain_def subset_iff)
show "A ⊆ ⋃ℱ"
using ‹A ⊆ ⋃ℱ› by blast
qed
qed
qed

lemma subset_Zorn_nonempty:
assumes "𝒜 ≠ {}" and ch: "⋀𝒞. ⟦𝒞≠{}; subset.chain 𝒜 𝒞⟧ ⟹ ⋃𝒞 ∈ 𝒜"
shows "∃M∈𝒜. ∀X∈𝒜. M ⊆ X ⟶ X = M"
proof (rule subset_Zorn)
show "∃U∈𝒜. ∀X∈𝒞. X ⊆ U" if "subset.chain 𝒜 𝒞" for 𝒞
proof (cases "𝒞 = {}")
case True
then show ?thesis
using ‹𝒜 ≠ {}› by blast
next
case False
show ?thesis
by (blast intro!: ch False that Union_upper)
qed
qed

subsection ‹The Well Ordering Theorem›

(* The initial segment of a relation appears generally useful.
Move to Relation.thy?
Definition correct/most general?
Naming?
*)
definition init_seg_of :: "(('a × 'a) set × ('a × 'a) set) set"
where "init_seg_of = {(r, s). r ⊆ s ∧ (∀a b c. (a, b) ∈ s ∧ (b, c) ∈ r ⟶ (a, b) ∈ r)}"

abbreviation initial_segment_of_syntax :: "('a × 'a) set ⇒ ('a × 'a) set ⇒ bool"
(infix "initial'_segment'_of" 55)
where "r initial_segment_of s ≡ (r, s) ∈ init_seg_of"

lemma refl_on_init_seg_of [simp]: "r initial_segment_of r"
by (simp add: init_seg_of_def)

lemma trans_init_seg_of:
"r initial_segment_of s ⟹ s initial_segment_of t ⟹ r initial_segment_of t"
by (simp (no_asm_use) add: init_seg_of_def) blast

lemma antisym_init_seg_of: "r initial_segment_of s ⟹ s initial_segment_of r ⟹ r = s"
unfolding init_seg_of_def by safe

lemma Chains_init_seg_of_Union: "R ∈ Chains init_seg_of ⟹ r∈R ⟹ r initial_segment_of ⋃R"
by (auto simp: init_seg_of_def Ball_def Chains_def) blast

lemma chain_subset_trans_Union:
assumes "chain⇩⊆ R" "∀r∈R. trans r"
shows "trans (⋃R)"
proof (intro transI, elim UnionE)
fix S1 S2 :: "'a rel" and x y z :: 'a
assume "S1 ∈ R" "S2 ∈ R"
with assms(1) have "S1 ⊆ S2 ∨ S2 ⊆ S1"
unfolding chain_subset_def by blast
moreover assume "(x, y) ∈ S1" "(y, z) ∈ S2"
ultimately have "((x, y) ∈ S1 ∧ (y, z) ∈ S1) ∨ ((x, y) ∈ S2 ∧ (y, z) ∈ S2)"
by blast
with ‹S1 ∈ R› ‹S2 ∈ R› assms(2) show "(x, z) ∈ ⋃R"
by (auto elim: transE)
qed

lemma chain_subset_antisym_Union:
assumes "chain⇩⊆ R" "∀r∈R. antisym r"
shows "antisym (⋃R)"
proof (intro antisymI, elim UnionE)
fix S1 S2 :: "'a rel" and x y :: 'a
assume "S1 ∈ R" "S2 ∈ R"
with assms(1) have "S1 ⊆ S2 ∨ S2 ⊆ S1"
unfolding chain_subset_def by blast
moreover assume "(x, y) ∈ S1" "(y, x) ∈ S2"
ultimately have "((x, y) ∈ S1 ∧ (y, x) ∈ S1) ∨ ((x, y) ∈ S2 ∧ (y, x) ∈ S2)"
by blast
with ‹S1 ∈ R› ‹S2 ∈ R› assms(2) show "x = y"
unfolding antisym_def by auto
qed

lemma chain_subset_Total_Union:
assumes "chain⇩⊆ R" and "∀r∈R. Total r"
shows "Total (⋃R)"
proof (simp add: total_on_def Ball_def, auto del: disjCI)
fix r s a b
assume A: "r ∈ R" "s ∈ R" "a ∈ Field r" "b ∈ Field s" "a ≠ b"
from ‹chain⇩⊆ R› and ‹r ∈ R› and ‹s ∈ R› have "r ⊆ s ∨ s ⊆ r"
by (auto simp add: chain_subset_def)
then show "(∃r∈R. (a, b) ∈ r) ∨ (∃r∈R. (b, a) ∈ r)"
proof
assume "r ⊆ s"
then have "(a, b) ∈ s ∨ (b, a) ∈ s"
using assms(2) A mono_Field[of r s]
by (auto simp add: total_on_def)
then show ?thesis
using ‹s ∈ R› by blast
next
assume "s ⊆ r"
then have "(a, b) ∈ r ∨ (b, a) ∈ r"
using assms(2) A mono_Field[of s r]
by (fastforce simp add: total_on_def)
then show ?thesis
using ‹r ∈ R› by blast
qed
qed

lemma wf_Union_wf_init_segs:
assumes "R ∈ Chains init_seg_of"
and "∀r∈R. wf r"
shows "wf (⋃R)"
proof (simp add: wf_iff_no_infinite_down_chain, rule ccontr, auto)
fix f
assume 1: "∀i. ∃r∈R. (f (Suc i), f i) ∈ r"
then obtain r where "r ∈ R" and "(f (Suc 0), f 0) ∈ r" by auto
have "(f (Suc i), f i) ∈ r" for i
proof (induct i)
case 0
show ?case by fact
next
case (Suc i)
then obtain s where s: "s ∈ R" "(f (Suc (Suc i)), f(Suc i)) ∈ s"
using 1 by auto
then have "s initial_segment_of r ∨ r initial_segment_of s"
using assms(1) ‹r ∈ R› by (simp add: Chains_def)
with Suc s show ?case by (simp add: init_seg_of_def) blast
qed
then show False
using assms(2) and ‹r ∈ R›
by (simp add: wf_iff_no_infinite_down_chain) blast
qed

lemma initial_segment_of_Diff: "p initial_segment_of q ⟹ p - s initial_segment_of q - s"
unfolding init_seg_of_def by blast

lemma Chains_inits_DiffI: "R ∈ Chains init_seg_of ⟹ {r - s |r. r ∈ R} ∈ Chains init_seg_of"
unfolding Chains_def by (blast intro: initial_segment_of_Diff)

theorem well_ordering: "∃r::'a rel. Well_order r ∧ Field r = UNIV"
proof -
― ‹The initial segment relation on well-orders:›
let ?WO = "{r::'a rel. Well_order r}"
define I where "I = init_seg_of ∩ ?WO × ?WO"
then have I_init: "I ⊆ init_seg_of" by simp
then have subch: "⋀R. R ∈ Chains I ⟹ chain⇩⊆ R"
unfolding init_seg_of_def chain_subset_def Chains_def by blast
have Chains_wo: "⋀R r. R ∈ Chains I ⟹ r ∈ R ⟹ Well_order r"
by (simp add: Chains_def I_def) blast
have FI: "Field I = ?WO"
by (auto simp add: I_def init_seg_of_def Field_def)
then have 0: "Partial_order I"
by (auto simp: partial_order_on_def preorder_on_def antisym_def antisym_init_seg_of refl_on_def
trans_def I_def elim!: trans_init_seg_of)
― ‹‹I›-chains have upper bounds in ‹?WO› wrt ‹I›: their Union›
have "⋃R ∈ ?WO ∧ (∀r∈R. (r, ⋃R) ∈ I)" if "R ∈ Chains I" for R
proof -
from that have Ris: "R ∈ Chains init_seg_of"
using mono_Chains [OF I_init] by blast
have subch: "chain⇩⊆ R"
using ‹R ∈ Chains I› I_init by (auto simp: init_seg_of_def chain_subset_def Chains_def)
have "∀r∈R. Refl r" and "∀r∈R. trans r" and "∀r∈R. antisym r"
and "∀r∈R. Total r" and "∀r∈R. wf (r - Id)"
using Chains_wo [OF ‹R ∈ Chains I›] by (simp_all add: order_on_defs)
have "Refl (⋃R)"
using ‹∀r∈R. Refl r› unfolding refl_on_def by fastforce
moreover have "trans (⋃R)"
by (rule chain_subset_trans_Union [OF subch ‹∀r∈R. trans r›])
moreover have "antisym (⋃R)"
by (rule chain_subset_antisym_Union [OF subch ‹∀r∈R. antisym r›])
moreover have "Total (⋃R)"
by (rule chain_subset_Total_Union [OF subch ‹∀r∈R. Total r›])
moreover have "wf ((⋃R) - Id)"
proof -
have "(⋃R) - Id = ⋃{r - Id | r. r ∈ R}" by blast
with ‹∀r∈R. wf (r - Id)› and wf_Union_wf_init_segs [OF Chains_inits_DiffI [OF Ris]]
show ?thesis by fastforce
qed
ultimately have "Well_order (⋃R)"
moreover have "∀r ∈ R. r initial_segment_of ⋃R"
using Ris by (simp add: Chains_init_seg_of_Union)
ultimately show ?thesis
using mono_Chains [OF I_init] Chains_wo[of R] and ‹R ∈ Chains I›
unfolding I_def by blast
qed
then have 1: "∃u∈Field I. ∀r∈R. (r, u) ∈ I" if "R ∈ Chains I" for R
using that by (subst FI) blast
― ‹Zorn's Lemma yields a maximal well-order ‹m›:›
then obtain m :: "'a rel"
where "Well_order m"
and max: "∀r. Well_order r ∧ (m, r) ∈ I ⟶ r = m"
using Zorns_po_lemma[OF 0 1] unfolding FI by fastforce
― ‹Now show by contradiction that ‹m› covers the whole type:›
have False if "x ∉ Field m" for x :: 'a
proof -
― ‹Assuming that ‹x› is not covered and extend ‹m› at the top with ‹x››
have "m ≠ {}"
proof
assume "m = {}"
moreover have "Well_order {(x, x)}"
by (simp add: order_on_defs refl_on_def trans_def antisym_def total_on_def Field_def)
ultimately show False using max
by (auto simp: I_def init_seg_of_def simp del: Field_insert)
qed
then have "Field m ≠ {}" by (auto simp: Field_def)
moreover have "wf (m - Id)"
using ‹Well_order m› by (simp add: well_order_on_def)
― ‹The extension of ‹m› by ‹x›:›
let ?s = "{(a, x) | a. a ∈ Field m}"
let ?m = "insert (x, x) m ∪ ?s"
have Fm: "Field ?m = insert x (Field m)"
by (auto simp: Field_def)
have "Refl m" and "trans m" and "antisym m" and "Total m" and "wf (m - Id)"
using ‹Well_order m› by (simp_all add: order_on_defs)
― ‹We show that the extension is a well-order›
have "Refl ?m"
using ‹Refl m› Fm unfolding refl_on_def by blast
moreover have "trans ?m" using ‹trans m› and ‹x ∉ Field m›
unfolding trans_def Field_def by blast
moreover have "antisym ?m"
using ‹antisym m› and ‹x ∉ Field m› unfolding antisym_def Field_def by blast
moreover have "Total ?m"
using ‹Total m› and Fm by (auto simp: total_on_def)
moreover have "wf (?m - Id)"
proof -
have "wf ?s"
using ‹x ∉ Field m› by (auto simp: wf_eq_minimal Field_def Bex_def)
then show ?thesis
using ‹wf (m - Id)› and ‹x ∉ Field m› wf_subset [OF ‹wf ?s› Diff_subset]
by (auto simp: Un_Diff Field_def intro: wf_Un)
qed
ultimately have "Well_order ?m"
by (simp add: order_on_defs)
― ‹We show that the extension is above ‹m››
moreover have "(m, ?m) ∈ I"
using ‹Well_order ?m› and ‹Well_order m› and ‹x ∉ Field m›
by (fastforce simp: I_def init_seg_of_def Field_def)
ultimately
― ‹This contradicts maximality of ‹m›:›
show False
using max and ‹x ∉ Field m› unfolding Field_def by blast
qed
then have "Field m = UNIV" by auto
with ‹Well_order m› show ?thesis by blast
qed

corollary well_order_on: "∃r::'a rel. well_order_on A r"
proof -
obtain r :: "'a rel" where wo: "Well_order r" and univ: "Field r = UNIV"
using well_ordering [where 'a = "'a"] by blast
let ?r = "{(x, y). x ∈ A ∧ y ∈ A ∧ (x, y) ∈ r}"
have 1: "Field ?r = A"
using wo univ by (fastforce simp: Field_def order_on_defs refl_on_def)
from ‹Well_order r› have "Refl r" "trans r" "antisym r" "Total r" "wf (r - Id)"
by (simp_all add: order_on_defs)
from ‹Refl r› have "Refl ?r"
by (auto simp: refl_on_def 1 univ)
moreover from ‹trans r› have "trans ?r"
unfolding trans_def by blast
moreover from ‹antisym r› have "antisym ?r"
unfolding antisym_def by blast
moreover from ‹Total r› have "Total ?r"
by (simp add:total_on_def 1 univ)
moreover have "wf (?r - Id)"
by (rule wf_subset [OF ‹wf (r - Id)›]) blast
ultimately have "Well_order ?r"
by (simp add: order_on_defs)
with 1 show ?thesis by auto
qed

lemma dependent_wf_choice:
fixes P :: "('a ⇒ 'b) ⇒ 'a ⇒ 'b ⇒ bool"
assumes "wf R"
and adm: "⋀f g x r. (⋀z. (z, x) ∈ R ⟹ f z = g z) ⟹ P f x r = P g x r"
and P: "⋀x f. (⋀y. (y, x) ∈ R ⟹ P f y (f y)) ⟹ ∃r. P f x r"
shows "∃f. ∀x. P f x (f x)"
proof (intro exI allI)
fix x
define f where "f ≡ wfrec R (λf x. SOME r. P f x r)"
from ‹wf R› show "P f x (f x)"
proof (induct x)
case (less x)
show "P f x (f x)"
proof (subst (2) wfrec_def_adm[OF f_def ‹wf R›])
show "adm_wf R (λf x. SOME r. P f x r)"
by (auto simp: adm_wf_def intro!: arg_cong[where f=Eps] adm)
show "P f x (Eps (P f x))"
using P by (rule someI_ex) fact
qed
qed
qed

lemma (in wellorder) dependent_wellorder_choice:
assumes "⋀r f g x. (⋀y. y < x ⟹ f y = g y) ⟹ P f x r = P g x r"
and P: "⋀x f. (⋀y. y < x ⟹ P f y (f y)) ⟹ ∃r. P f x r"
shows "∃f. ∀x. P f x (f x)"
using wf by (rule dependent_wf_choice) (auto intro!: assms)

end
```