(* Title: HOL/Library/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).

The well-ordering theorem.

The extension of any well-founded relation to a well-order.

*)

header {* Zorn's Lemma *}

theory Zorn

imports Order_Union

begin

subsection {* Zorn's Lemma for the Subset Relation *}

subsubsection {* Results that do not require an order *}

text {*Let @{text P} be a binary predicate on the set @{text A}.*}

locale pred_on =

fixes A :: "'a set"

and P :: "'a => 'a => bool" (infix "\<sqsubset>" 50)

begin

abbreviation Peq :: "'a => 'a => bool" (infix "\<sqsubseteq>" 50) where

"x \<sqsubseteq> y ≡ P⇧^{=}⇧^{=}x y"

text {*A chain is a totally ordered subset of @{term A}.*}

definition chain :: "'a set => bool" where

"chain C <-> C ⊆ A ∧ (∀x∈C. ∀y∈C. x \<sqsubseteq> y ∨ y \<sqsubseteq> x)"

text {*We call a chain that is a proper superset of some set @{term X},

but not necessarily a chain itself, a superchain of @{term 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 \<sqsubseteq> y ∨ y \<sqsubseteq> x|] ==> chain C"

unfolding chain_def by blast

lemma chain_total:

"chain C ==> x ∈ C ==> y ∈ C ==> x \<sqsubseteq> y ∨ y \<sqsubseteq> 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"

by (auto simp: suc_def) (metis less_irrefl not_maxchain_Some)

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 \<C>} that is closed under applications

of @{term suc} and contains the union of all its subsets.*}

inductive_set suc_Union_closed ("\<C>") where

suc: "X ∈ \<C> ==> suc X ∈ \<C>" |

Union [unfolded Pow_iff]: "X ∈ Pow \<C> ==> \<Union>X ∈ \<C>"

text {*Since the empty set as well as the set itself is a subset of

every set, @{term \<C>} contains at least @{term "{} ∈ \<C>"} and

@{term "\<Union>\<C> ∈ \<C>"}.*}

lemma

suc_Union_closed_empty: "{} ∈ \<C>" and

suc_Union_closed_Union: "\<Union>\<C> ∈ \<C>"

using Union [of "{}"] and Union [of "\<C>"] by simp+

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 ∈ \<C>"

and "!!X. [|X ∈ \<C>; Q X|] ==> Q (suc X)"

and "!!X. [|X ⊆ \<C>; ∀x∈X. Q x|] ==> Q (\<Union>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 ∈ \<C>"

and "!!Y. [|X = suc Y; Y ∈ \<C>|] ==> Q"

and "!!Y. [|X = \<Union>Y; Y ⊆ \<C>|] ==> Q"

shows "Q"

using assms by (cases) simp+

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 ∈ \<C>" and "Y ∈ \<C>"

and *: "!!Z. Z ∈ \<C> ==> Z ⊆ Y ==> Z = Y ∨ suc Z ⊆ Y"

shows "X ⊆ Y ∨ suc Y ⊆ X"

using `X ∈ \<C>`

proof (induct)

case (suc X)

with * show ?case by (blast del: subsetI intro: subset_suc)

qed blast

lemma suc_Union_closed_subsetD:

assumes "Y ⊆ X" and "X ∈ \<C>" and "Y ∈ \<C>"

shows "X = Y ∨ suc Y ⊆ X"

using assms(2-, 1)

proof (induct arbitrary: Y)

case (suc X)

note * = `!!Y. [|Y ∈ \<C>; Y ⊆ X|] ==> X = Y ∨ suc Y ⊆ X`

with suc_Union_closed_total' [OF `Y ∈ \<C>` `X ∈ \<C>`]

have "Y ⊆ X ∨ suc X ⊆ Y" by blast

then show ?case

proof

assume "Y ⊆ X"

with * and `Y ∈ \<C>` have "X = Y ∨ suc Y ⊆ X" by blast

then show ?thesis

proof

assume "X = Y" then show ?thesis by simp

next

assume "suc Y ⊆ X"

then have "suc Y ⊆ suc X" by (rule subset_suc)

then show ?thesis by simp

qed

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 ⊆ \<Union>X` obtain x y z

where "¬ suc Y ⊆ \<Union>X"

and "x ∈ X" and "y ∈ x" and "y ∉ Y"

and "z ∈ suc Y" and "∀x∈X. z ∉ x" by blast

with `X ⊆ \<C>` have "x ∈ \<C>" by blast

from Union and `x ∈ X`

have *: "!!y. [|y ∈ \<C>; y ⊆ x|] ==> x = y ∨ suc y ⊆ x" by blast

with suc_Union_closed_total' [OF `Y ∈ \<C>` `x ∈ \<C>`]

have "Y ⊆ x ∨ suc x ⊆ Y" by blast

then show False

proof

assume "Y ⊆ x"

with * [OF `Y ∈ \<C>`] have "x = Y ∨ suc Y ⊆ x" by blast

then show False

proof

assume "x = Y" with `y ∈ x` and `y ∉ Y` show False by blast

next

assume "suc Y ⊆ x"

with `x ∈ X` have "suc Y ⊆ \<Union>X" by blast

with `¬ suc Y ⊆ \<Union>X` show False by contradiction

qed

next

assume "suc x ⊆ Y"

moreover from suc_subset and `y ∈ x` have "y ∈ suc x" by blast

ultimately show False using `y ∉ Y` by blast

qed

qed

qed

text {*The elements of @{term \<C>} are totally ordered by the subset relation.*}

lemma suc_Union_closed_total:

assumes "X ∈ \<C>" and "Y ∈ \<C>"

shows "X ⊆ Y ∨ Y ⊆ X"

proof (cases "∀Z∈\<C>. Z ⊆ Y --> Z = Y ∨ suc Z ⊆ Y")

case True

with suc_Union_closed_total' [OF assms]

have "X ⊆ Y ∨ suc Y ⊆ X" by blast

then show ?thesis using suc_subset [of Y] by blast

next

case False

then obtain Z

where "Z ∈ \<C>" and "Z ⊆ Y" and "Z ≠ Y" and "¬ suc Z ⊆ Y" by blast

with suc_Union_closed_subsetD and `Y ∈ \<C>` show ?thesis by blast

qed

text {*Once we hit a fixed point w.r.t. @{term suc}, all other elements

of @{term \<C>} are subsets of this fixed point.*}

lemma suc_Union_closed_suc:

assumes "X ∈ \<C>" and "Y ∈ \<C>" and "suc Y = Y"

shows "X ⊆ Y"

using `X ∈ \<C>`

proof (induct)

case (suc X)

with `Y ∈ \<C>` and suc_Union_closed_subsetD

have "X = Y ∨ suc X ⊆ Y" by blast

then show ?case by (auto simp: `suc Y = Y`)

qed blast

lemma eq_suc_Union:

assumes "X ∈ \<C>"

shows "suc X = X <-> X = \<Union>\<C>"

proof

assume "suc X = X"

with suc_Union_closed_suc [OF suc_Union_closed_Union `X ∈ \<C>`]

have "\<Union>\<C> ⊆ X" .

with `X ∈ \<C>` show "X = \<Union>\<C>" by blast

next

from `X ∈ \<C>` have "suc X ∈ \<C>" by (rule suc)

then have "suc X ⊆ \<Union>\<C>" by blast

moreover assume "X = \<Union>\<C>"

ultimately have "suc X ⊆ X" by simp

moreover have "X ⊆ suc X" by (rule suc_subset)

ultimately show "suc X = X" ..

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 ∈ \<C>"

shows "X ⊆ A"

using assms

by (induct) (auto dest: suc_in_carrier)

text {*All elements of @{term \<C>} are chains.*}

lemma suc_Union_closed_chain:

assumes "X ∈ \<C>"

shows "chain X"

using assms

proof (induct)

case (suc X) then show ?case by (simp add: suc_def) (metis not_maxchain_Some)

next

case (Union X)

then have "\<Union>X ⊆ A" by (auto dest: suc_Union_closed_in_carrier)

moreover have "∀x∈\<Union>X. ∀y∈\<Union>X. x \<sqsubseteq> y ∨ y \<sqsubseteq> x"

proof (intro ballI)

fix x y

assume "x ∈ \<Union>X" and "y ∈ \<Union>X"

then obtain u v where "x ∈ u" and "u ∈ X" and "y ∈ v" and "v ∈ X" by blast

with Union have "u ∈ \<C>" and "v ∈ \<C>" and "chain u" and "chain v" by blast+

with suc_Union_closed_total have "u ⊆ v ∨ v ⊆ u" by blast

then show "x \<sqsubseteq> y ∨ y \<sqsubseteq> 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 @{term A}. (Note that we do not

require @{term A} to be partially ordered.)*}

theorem Hausdorff: "∃C. maxchain C"

proof -

let ?M = "\<Union>\<C>"

have "maxchain ?M"

proof (rule ccontr)

assume "¬ maxchain ?M"

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 \<C>} available again.*}

no_notation suc_Union_closed ("\<C>")

lemma chain_extend:

"chain C ==> z ∈ A ==> ∀x∈C. x \<sqsubseteq> 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" "op ⊂" for A .

lemma subset_maxchain_max:

assumes "subset.maxchain A C" and "X ∈ A" and "\<Union>C ⊆ X"

shows "\<Union>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 `\<Union>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 **: "\<Union>C ≠ X"

moreover from ** have "C ⊂ ?C" using `\<Union>C ⊆ X` by auto

ultimately show False using * by blast

qed

subsubsection {* Zorn's lemma *}

text {*If every chain has an upper bound, then there is a maximal set.*}

lemma 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 "Y ≠ X"

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 ==> \<Union>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 "\<Union>M ∈ A" .

moreover have "∀Z∈A. \<Union>M ⊆ Z --> \<Union>M = Z"

proof (intro ballI impI)

fix Z

assume "Z ∈ A" and "\<Union>M ⊆ Z"

with subset_maxchain_max [OF `subset.maxchain A M`]

show "\<Union>M = Z" .

qed

ultimately show ?thesis by blast

qed

subsection {* Zorn's Lemma for Partial Orders *}

text {*Relate old to new definitions.*}

(* Define globally? In Set.thy? *)

definition chain_subset :: "'a set set => bool" ("chain⇩_{⊆}") 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}"

(* Define globally? In Relation.thy? *)

definition Chains :: "('a × 'a) set => 'a set set" 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:: 'a set) |] ==> {z} Un c ∈ chains S"

by (unfold chains_def chain_subset_def) 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"

by (auto simp add: chain_subset_def subset.chain_def)

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

by (metis Chains_subset Chains_subset' subset_antisym)

lemma Zorn_Lemma:

"∀C∈chains A. \<Union>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)

text{*Various other lemmas*}

lemma chainsD: "[| c ∈ chains S; x ∈ c; y ∈ c |] ==> x ⊆ y | y ⊆ x"

by (unfold chains_def chain_subset_def) blast

lemma chainsD2: "!!(c :: 'a set set). c ∈ chains S ==> c ⊆ S"

by (unfold chains_def) blast

lemma Zorns_po_lemma:

assumes po: "Partial_order r"

and u: "∀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)

--{* Mirror r in the set of subsets below (wrt r) elements of A*}

let ?B = "%x. r¯ `` {x}" let ?S = "?B ` Field r"

{

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 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"

hence "?B a ⊆ ?B b ∨ ?B b ⊆ ?B a" using 2 by auto

thus "(a, b) ∈ r ∨ (b, a) ∈ r"

using `Preorder r` and `a ∈ Field r` and `b ∈ Field r`

by (simp add:subset_Image1_Image1_iff)

qed

then obtain u where uA: "u ∈ Field r" "∀a∈?A. (a, u) ∈ r" using u by auto

have "∀A∈C. A ⊆ r¯ `` {u}" (is "?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

thus "(a, u) ∈ r" using uA and aB and `Preorder r`

by (auto simp add: preorder_on_def refl_on_def) (metis transD)

qed

then have "∃u∈Field r. ?P u" using `u ∈ Field r` by blast

}

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

hence "∀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)

thus ?thesis using `m ∈ Field r` by blast

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

initialSegmentOf :: "('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)

(metis UnCI Un_absorb2 subset_trans)

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 \<Union>R"

by (auto simp: init_seg_of_def Ball_def Chains_def) blast

lemma chain_subset_trans_Union:

"chain⇩_{⊆}R ==> ∀r∈R. trans r ==> trans (\<Union>R)"

apply (auto simp add: chain_subset_def)

apply (simp (no_asm_use) add: trans_def)

apply (metis subsetD)

done

lemma chain_subset_antisym_Union:

"chain⇩_{⊆}R ==> ∀r∈R. antisym r ==> antisym (\<Union>R)"

apply (auto simp add: chain_subset_def antisym_def)

apply (metis subsetD)

done

lemma chain_subset_Total_Union:

assumes "chain⇩_{⊆}R" and "∀r∈R. Total r"

shows "Total (\<Union>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)

thus "(∃r∈R. (a, b) ∈ r) ∨ (∃r∈R. (b, a) ∈ r)"

proof

assume "r ⊆ s" hence "(a, b) ∈ s ∨ (b, a) ∈ s" using assms(2) A

by (simp add: total_on_def) (metis mono_Field subsetD)

thus ?thesis using `s ∈ R` by blast

next

assume "s ⊆ r" hence "(a, b) ∈ r ∨ (b, a) ∈ r" using assms(2) A

by (simp add: total_on_def) (metis mono_Field subsetD)

thus ?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 (\<Union>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

{ fix i have "(f (Suc i), f i) ∈ r"

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

}

thus 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}"

def I ≡ "init_seg_of ∩ ?WO × ?WO"

have I_init: "I ⊆ init_seg_of" by (auto simp: I_def)

hence subch: "!!R. R ∈ Chains I ==> chain⇩_{⊆}R"

by (auto simp: init_seg_of_def chain_subset_def Chains_def)

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)

hence 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*}

{ fix R assume "R ∈ Chains I"

hence 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 (\<Union>R)" using `∀r∈R. Refl r` by (auto simp: refl_on_def)

moreover have "trans (\<Union>R)"

by (rule chain_subset_trans_Union [OF subch `∀r∈R. trans r`])

moreover have "antisym (\<Union>R)"

by (rule chain_subset_antisym_Union [OF subch `∀r∈R. antisym r`])

moreover have "Total (\<Union>R)"

by (rule chain_subset_Total_Union [OF subch `∀r∈R. Total r`])

moreover have "wf ((\<Union>R) - Id)"

proof -

have "(\<Union>R) - Id = \<Union>{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 (simp (no_asm_simp)) blast

qed

ultimately have "Well_order (\<Union>R)" by(simp add:order_on_defs)

moreover have "∀r ∈ R. r initial_segment_of \<Union>R" using Ris

by(simp add: Chains_init_seg_of_Union)

ultimately have "\<Union>R ∈ ?WO ∧ (∀r∈R. (r, \<Union>R) ∈ I)"

using mono_Chains [OF I_init] and `R ∈ Chains I`

by (simp (no_asm) add: I_def del: Field_Union) (metis Chains_wo)

}

hence 1: "∀R ∈ Chains I. ∃u∈Field I. ∀r∈R. (r, u) ∈ I" 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] by (auto simp:FI)

--{*Now show by contradiction that m covers the whole type:*}

{ fix x::'a assume "x ∉ Field m"

--{*We assume 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

hence "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 by (auto simp: refl_on_def)

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 add: wf_eq_minimal Field_def) metis

thus ?thesis using `wf (m - Id)` and `x ∉ Field m`

wf_subset [OF `wf ?s` Diff_subset]

by (fastforce intro!: wf_Un simp add: Un_Diff Field_def)

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:*}

have False using max and `x ∉ Field m` unfolding Field_def by blast

}

hence "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)

have "Refl r" and "trans r" and "antisym r" and "Total r" and "wf (r - Id)"

using `Well_order r` by (simp_all add: order_on_defs)

have "Refl ?r" using `Refl r` by (auto simp: refl_on_def 1 univ)

moreover have "trans ?r" using `trans r`

unfolding trans_def by blast

moreover have "antisym ?r" using `antisym r`

unfolding antisym_def by blast

moreover have "Total ?r" using `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 metis

qed

subsection {* Extending Well-founded Relations to Well-Orders *}

text {*A \emph{downset} (also lower set, decreasing set, initial segment, or

downward closed set) is closed w.r.t.\ smaller elements.*}

definition downset_on where

"downset_on A r = (∀x y. (x, y) ∈ r ∧ y ∈ A --> x ∈ A)"

(*

text {*Connection to order filters of the @{theory Cardinals} theory.*}

lemma (in wo_rel) ofilter_downset_on_conv:

"ofilter A <-> downset_on A r ∧ A ⊆ Field r"

by (auto simp: downset_on_def ofilter_def under_def)

*)

lemma downset_onI:

"(!!x y. (x, y) ∈ r ==> y ∈ A ==> x ∈ A) ==> downset_on A r"

by (auto simp: downset_on_def)

lemma downset_onD:

"downset_on A r ==> (x, y) ∈ r ==> y ∈ A ==> x ∈ A"

by (auto simp: downset_on_def)

text {*Extensions of relations w.r.t.\ a given set.*}

definition extension_on where

"extension_on A r s = (∀x∈A. ∀y∈A. (x, y) ∈ s --> (x, y) ∈ r)"

lemma extension_onI:

"(!!x y. [|x ∈ A; y ∈ A; (x, y) ∈ s|] ==> (x, y) ∈ r) ==> extension_on A r s"

by (auto simp: extension_on_def)

lemma extension_onD:

"extension_on A r s ==> x ∈ A ==> y ∈ A ==> (x, y) ∈ s ==> (x, y) ∈ r"

by (auto simp: extension_on_def)

lemma downset_on_Union:

assumes "!!r. r ∈ R ==> downset_on (Field r) p"

shows "downset_on (Field (\<Union>R)) p"

using assms by (auto intro: downset_onI dest: downset_onD)

lemma chain_subset_extension_on_Union:

assumes "chain⇩_{⊆}R" and "!!r. r ∈ R ==> extension_on (Field r) r p"

shows "extension_on (Field (\<Union>R)) (\<Union>R) p"

using assms

by (simp add: chain_subset_def extension_on_def) (metis mono_Field set_mp)

lemma downset_on_empty [simp]: "downset_on {} p"

by (auto simp: downset_on_def)

lemma extension_on_empty [simp]: "extension_on {} p q"

by (auto simp: extension_on_def)

text {*Every well-founded relation can be extended to a well-order.*}

theorem well_order_extension:

assumes "wf p"

shows "∃w. p ⊆ w ∧ Well_order w"

proof -

let ?K = "{r. Well_order r ∧ downset_on (Field r) p ∧ extension_on (Field r) r p}"

def I ≡ "init_seg_of ∩ ?K × ?K"

have I_init: "I ⊆ init_seg_of" by (simp add: I_def)

then have subch: "!!R. R ∈ Chains I ==> chain⇩_{⊆}R"

by (auto simp: init_seg_of_def chain_subset_def Chains_def)

have Chains_wo: "!!R r. R ∈ Chains I ==> r ∈ R ==>

Well_order r ∧ downset_on (Field r) p ∧ extension_on (Field r) r p"

by (simp add: Chains_def I_def) blast

have FI: "Field I = ?K" by (auto simp: 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)

{ fix R assume "R ∈ Chains I"

then 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)" and

"!!r. r ∈ R ==> downset_on (Field r) p" and

"!!r. r ∈ R ==> extension_on (Field r) r p"

using Chains_wo [OF `R ∈ Chains I`] by (simp_all add: order_on_defs)

have "Refl (\<Union>R)" using `∀r∈R. Refl r` by (auto simp: refl_on_def)

moreover have "trans (\<Union>R)"

by (rule chain_subset_trans_Union [OF subch `∀r∈R. trans r`])

moreover have "antisym (\<Union>R)"

by (rule chain_subset_antisym_Union [OF subch `∀r∈R. antisym r`])

moreover have "Total (\<Union>R)"

by (rule chain_subset_Total_Union [OF subch `∀r∈R. Total r`])

moreover have "wf ((\<Union>R) - Id)"

proof -

have "(\<Union>R) - Id = \<Union>{r - Id | r. r ∈ R}" by blast

with `∀r∈R. wf (r - Id)` wf_Union_wf_init_segs [OF Chains_inits_DiffI [OF Ris]]

show ?thesis by (simp (no_asm_simp)) blast

qed

ultimately have "Well_order (\<Union>R)" by (simp add: order_on_defs)

moreover have "∀r∈R. r initial_segment_of \<Union>R" using Ris

by (simp add: Chains_init_seg_of_Union)

moreover have "downset_on (Field (\<Union>R)) p"

by (rule downset_on_Union [OF `!!r. r ∈ R ==> downset_on (Field r) p`])

moreover have "extension_on (Field (\<Union>R)) (\<Union>R) p"

by (rule chain_subset_extension_on_Union [OF subch `!!r. r ∈ R ==> extension_on (Field r) r p`])

ultimately have "\<Union>R ∈ ?K ∧ (∀r∈R. (r,\<Union>R) ∈ I)"

using mono_Chains [OF I_init] and `R ∈ Chains I`

by (simp (no_asm) add: I_def del: Field_Union) (metis Chains_wo)

}

then have 1: "∀R∈Chains I. ∃u∈Field I. ∀r∈R. (r, u) ∈ I" by (subst FI) blast

txt {*Zorn's Lemma yields a maximal well-order m.*}

from Zorns_po_lemma [OF 0 1] obtain m :: "('a × 'a) set"

where "Well_order m" and "downset_on (Field m) p" and "extension_on (Field m) m p" and

max: "∀r. Well_order r ∧ downset_on (Field r) p ∧ extension_on (Field r) r p ∧

(m, r) ∈ I --> r = m"

by (auto simp: FI)

have "Field p ⊆ Field m"

proof (rule ccontr)

let ?Q = "Field p - Field m"

assume "¬ (Field p ⊆ Field m)"

with assms [unfolded wf_eq_minimal, THEN spec, of ?Q]

obtain x where "x ∈ Field p" and "x ∉ Field m" and

min: "∀y. (y, x) ∈ p --> y ∉ ?Q" by blast

txt {*Add @{term x} as topmost element to @{term m}.*}

let ?s = "{(y, x) | y. y ∈ 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)

txt {*We show that the extension is a well-order.*}

have "Refl ?m" using `Refl m` Fm by (auto simp: refl_on_def)

moreover have "trans ?m" using `trans m` `x ∉ Field m`

unfolding trans_def Field_def Domain_unfold Domain_converse [symmetric] by blast

moreover have "antisym ?m" using `antisym m` `x ∉ Field m`

unfolding antisym_def Field_def Domain_unfold Domain_converse [symmetric] by blast

moreover have "Total ?m" using `Total m` Fm by (auto simp: Relation.total_on_def)

moreover have "wf (?m - Id)"

proof -

have "wf ?s" using `x ∉ Field m`

by (simp add: wf_eq_minimal Field_def Domain_unfold Domain_converse [symmetric]) metis

thus ?thesis using `wf (m - Id)` `x ∉ Field m`

wf_subset [OF `wf ?s` Diff_subset]

by (fastforce intro!: wf_Un simp add: Un_Diff Field_def)

qed

ultimately have "Well_order ?m" by (simp add: order_on_defs)

moreover have "extension_on (Field ?m) ?m p"

using `extension_on (Field m) m p` `downset_on (Field m) p`

by (subst Fm) (auto simp: extension_on_def dest: downset_onD)

moreover have "downset_on (Field ?m) p"

using `downset_on (Field m) p` and min

by (subst Fm, simp add: downset_on_def Field_def) (metis Domain_iff)

moreover have "(m, ?m) ∈ I"

using `Well_order m` and `Well_order ?m` and

`downset_on (Field m) p` and `downset_on (Field ?m) p` and

`extension_on (Field m) m p` and `extension_on (Field ?m) ?m p` and

`Refl m` and `x ∉ Field m`

by (auto simp: I_def init_seg_of_def refl_on_def)

ultimately

--{*This contradicts maximality of m:*}

show False using max and `x ∉ Field m` unfolding Field_def by blast

qed

have "p ⊆ m"

using `Field p ⊆ Field m` and `extension_on (Field m) m p`

by (force simp: Field_def extension_on_def)

with `Well_order m` show ?thesis by blast

qed

text {*Every well-founded relation can be extended to a total well-order.*}

corollary total_well_order_extension:

assumes "wf p"

shows "∃w. p ⊆ w ∧ Well_order w ∧ Field w = UNIV"

proof -

from well_order_extension [OF assms] obtain w

where "p ⊆ w" and wo: "Well_order w" by blast

let ?A = "UNIV - Field w"

from well_order_on [of ?A] obtain w' where wo': "well_order_on ?A w'" ..

have [simp]: "Field w' = ?A" using rel.well_order_on_Well_order [OF wo'] by simp

have *: "Field w ∩ Field w' = {}" by simp

let ?w = "w ∪o w'"

have "p ⊆ ?w" using `p ⊆ w` by (auto simp: Osum_def)

moreover have "Well_order ?w" using Osum_Well_order [OF * wo] and wo' by simp

moreover have "Field ?w = UNIV" by (simp add: Field_Osum)

ultimately show ?thesis by blast

qed

corollary well_order_on_extension:

assumes "wf p" and "Field p ⊆ A"

shows "∃w. p ⊆ w ∧ well_order_on A w"

proof -

from total_well_order_extension [OF `wf p`] obtain r

where "p ⊆ r" and wo: "Well_order r" and univ: "Field r = UNIV" by blast

let ?r = "{(x, y). x ∈ A ∧ y ∈ A ∧ (x, y) ∈ r}"

from `p ⊆ r` have "p ⊆ ?r" using `Field p ⊆ A` by (auto simp: Field_def)

have 1: "Field ?r = A" using wo univ

by (fastforce simp: Field_def order_on_defs refl_on_def)

have "Refl r" "trans r" "antisym r" "Total r" "wf (r - Id)"

using `Well_order r` by (simp_all add: order_on_defs)

have "refl_on A ?r" using `Refl r` by (auto simp: refl_on_def univ)

moreover have "trans ?r" using `trans r`

unfolding trans_def by blast

moreover have "antisym ?r" using `antisym r`

unfolding antisym_def by blast

moreover have "total_on A ?r" using `Total r` by (simp add: total_on_def univ)

moreover have "wf (?r - Id)" by (rule wf_subset [OF `wf(r - Id)`]) blast

ultimately have "well_order_on A ?r" by (simp add: order_on_defs)

with `p ⊆ ?r` show ?thesis by blast

qed

end