Theory Zorn

theory Zorn
imports Order_Union
(*  Title:      HOL/Library/Zorn.thy    Author:     Jacques D. Fleuriot    Author:     Tobias Nipkow, TUM    Author:     Christian Sternagel, JAISTZorn'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 Zornimports Order_Unionbeginsubsection {* 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)beginabbreviation 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 arbitrarysuperchain, 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 blastlemma 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 applicationsof @{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 ofevery 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 chaineventually, 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 blastqedlemma 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 blastlemma 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  qednext  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  qedqedtext {*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 blastnext  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 blastqedtext {*Once we hit a fixed point w.r.t. @{term suc}, all other elementsof @{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 blastlemma 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 blastnext  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" ..qedlemma 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 assmsproof (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 ..qedsubsubsection {* Hausdorff's Maximum Principle *}text {*There exists a maximal totally ordered subset of @{term A}. (Note that we do notrequire @{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 blastqedtext {*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 blastlemma maxchain_imp_chain:  "maxchain C ==> chain C"  by (simp add: maxchain_def)endtext {*Hide constant @{const pred_on.suc_Union_closed}, which was just neededfor the proof of Hausforff's maximum principle.*}hide_const pred_on.suc_Union_closedlemma 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 blastsubsubsection {* 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 blastqedsubsubsection {* 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 blastqedtext{*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 blastqedsubsection {* 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) blastlemma mono_Chains: "r ⊆ s ==> Chains r ⊆ Chains s"  unfolding Chains_def by blastlemma 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) blastlemma chainsD2: "!!(c :: 'a set set). c ∈ chains S ==> c ⊆ S"by (unfold chains_def) blastlemma 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 blastqedsubsection {* 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 safelemma 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) blastlemma 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)donelemma 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)donelemma 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  qedqedlemma 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) blastqedlemma initial_segment_of_Diff:  "p initial_segment_of q ==> p - s initial_segment_of q - s"  unfolding init_seg_of_def by blastlemma 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 blastqedcorollary 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 metisqedsubsection {* Extending Well-founded Relations to Well-Orders *}text {*A \emph{downset} (also lower set, decreasing set, initial segment, ordownward 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 blastqedtext {*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 blastqedcorollary 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 blastqedend