Quelle  Zorn.thy   Sprache: Isabelle

(*  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\<^sup>=\<^sup>= 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 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

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

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
  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 🍋‹C› that is closed under applications
  of 🍋‹suc› and contains the union of all its subsets.
›
inductive_set suc_Union_closed (‹C›)
  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, 🍋‹C› contains at least 🍋‹{} ∈ C› and
  🍋‹∪C ∈ C›.
›
lemma suc_Union_closed_empty: "{} \ \"
  and suc_Union_closed_Union: "\\ \ \"
  using Union [of "{}"] and Union [of "\"] by simp_all

text ‹Thus closure under 🍋‹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, 🍋‹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 ∈ C›
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 ∈ C ==> 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 ∈ C› 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 ⊆ C› 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 ∈ C›] ‹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 🍋‹C› 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 ∈ C› show ?thesis
    by blast
qed

text ‹Once we hit a fixed point w.r.t. 🍋‹suc›, all other elements
  of 🍋‹C› are subsets of this fixed point.›
lemma suc_Union_closed_suc:
  assumes "X \ \" and "Y \ \" 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›)
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 ∈ C›])
  with ‹X ∈ C› show ?rhs
    by blast
next
  from ‹X ∈ C› 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 🍋‹C› 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 🍋‹C› available again.›
no_notation suc_Union_closed  (‹C›)

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 🍋‹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\<^sub>\ 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\<^sub>\ 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\<^sub>\ 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\<^sub>\ \"
  shows "pairwise R (\\)"
  using ‹chain🚫⊆ C› 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›
        by (simp add:subset_Image1_Image1_iff)
    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(4)[OF po] 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 B rule: finite_induct)
  case (insert B 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 B rule: finite_induct)
  case (insert B 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 F where F: "finite \" "\ \ \" "A \ \\"
    using assms by (auto intro: finite_subset_Union)
  show thesis
  proof (cases "\ = {}")
    case True
    then show ?thesis
      using ‹A ⊆ ∪F› ‹B ≠ {}› that by fastforce
  next
    case False
    show ?thesis
    proof
      show "\\ \ \"
        using sub ‹F ⊆ B› ‹finite F›
        by (simp add: Union_in_chain False subset.chain_def subset_iff)
      show "A \ \\"
        using ‹A ⊆ ∪F› 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 C
  proof (cases "\ = {}")
    case True
    then show ?thesis
      using ‹A ≠ {}› 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\<^sub>\ 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\<^sub>\ 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\<^sub>\ 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\<^sub>\ 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\<^sub>\ 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 "(\ R) \ Field (\ R) \ Field (\ R)"
      unfolding Field_def by auto
    moreover 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)"
      by (simp add:order_on_defs)
    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)" and
      "m \ Field m \ Field m"
      using ‹Well_order m› by (simp_all add: order_on_defs)
🍋 ‹We show that the extension is a well-order›
    have "?m \ Field ?m \ Field ?m"
      using ‹m ⊆ Field m × Field m› by auto
    moreover 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)" and
    "r \ Field r \ Field r"
    by (simp_all add: order_on_defs)
  have "?r \ Field ?r \ Field ?r"
      using ‹r ⊆ Field r × Field r› by (auto simp: 1)
  moreover 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