Theory Complete_Non_Orders.Well_Relations

theory Well_Relations
  imports Binary_Relations
begin

section ‹Well-Relations›

text ‹
A related set $\tp{A,\SLE}$ is called \emph{topped} if there is a ``top'' element $\top \in A$,
a greatest element in $A$.
Note that there might be multiple tops if $(\SLE)$ is not antisymmetric.›

definition "extremed A r ≡ ∃e. extreme A r e"

lemma extremedI: "extreme A r e ⟹ extremed A r"
  by (auto simp: extremed_def)

lemma extremedE: "extremed A r ⟹ (⋀e. extreme A r e ⟹ thesis) ⟹ thesis"
  by (auto simp: extremed_def)

lemma extremed_imp_ex_bound: "extremed A r ⟹ X ⊆ A ⟹ ∃b ∈ A. bound X r b"
  by (auto simp: extremed_def)

locale well_founded = related_set _ "(⊏)" + less_syntax +
  assumes induct[consumes 1, case_names less, induct set]:
    "a ∈ A ⟹ (⋀x. x ∈ A ⟹ (⋀y. y ∈ A ⟹ y ⊏ x ⟹ P y) ⟹ P x) ⟹ P a"
begin

sublocale asymmetric
proof (intro asymmetric.intro notI)
  fix x y
  assume xA: "x ∈ A"
  then show "y ∈ A ⟹ x ⊏ y ⟹ y ⊏ x ⟹ False"
    by (induct arbitrary: y rule: induct, auto)
qed

lemma prefixed_Imagep_imp_empty:
  assumes a: "X ⊆ ((⊏) ``` X) ∩ A" shows "X = {}"
proof -
  from a have XA: "X ⊆ A" by auto
  have "x ∈ A ⟹ x ∉ X" for x
  proof (induct x rule: induct)
    case (less x)
    with a show ?case by (auto simp: Imagep_def)
  qed
  with XA show ?thesis by auto
qed

lemma nonempty_imp_ex_extremal:
  assumes QA: "Q ⊆ A" and Q: "Q ≠ {}"
  shows "∃z ∈ Q. ∀y ∈ Q. ¬ y ⊏ z"
  using Q prefixed_Imagep_imp_empty[of Q] QA by (auto simp: Imagep_def)

interpretation Restrp: well_founded UNIV "(⊏)↾A"
  rewrites "⋀x. x ∈ UNIV ≡ True"
    and "(⊏)↾A↾UNIV = (⊏)↾A"
    and "⋀P1. (True ⟹ PROP P1) ≡ PROP P1"
    and "⋀P1. (True ⟹ P1) ≡ Trueprop P1"
    and "⋀P1 P2. (True ⟹ PROP P1 ⟹ PROP P2) ≡ (PROP P1 ⟹ PROP P2)"
proof -
  have "(⋀x. (⋀y. ((⊏) ↾ A) y x ⟹ P y) ⟹ P x) ⟹ P a" for a P
    using induct[of a P] by (auto simp: Restrp_def)
  then show "well_founded UNIV ((⊏)↾A)" apply unfold_locales by auto
qed auto

lemmas Restrp_well_founded = Restrp.well_founded_axioms
lemmas Restrp_induct[consumes 0, case_names less] = Restrp.induct

interpretation Restrp.tranclp: well_founded UNIV "((⊏)↾A)⇧+⇧+"
  rewrites "⋀x. x ∈ UNIV ≡ True"
    and "((⊏)↾A)⇧+⇧+ ↾ UNIV = ((⊏)↾A)⇧+⇧+"
    and "(((⊏)↾A)⇧+⇧+)⇧+⇧+ = ((⊏)↾A)⇧+⇧+"
    and "⋀P1. (True ⟹ PROP P1) ≡ PROP P1"
    and "⋀P1. (True ⟹ P1) ≡ Trueprop P1"
    and "⋀P1 P2. (True ⟹ PROP P1 ⟹ PROP P2) ≡ (PROP P1 ⟹ PROP P2)"
proof-
  { fix P x
    assume induct_step: "⋀x. (⋀y. ((⊏)↾A)⇧+⇧+ y x ⟹ P y) ⟹ P x"
    have "P x"
    proof (rule induct_step)
      show "⋀y. ((⊏)↾A)⇧+⇧+ y x ⟹ P y"
      proof (induct x rule: Restrp_induct)
        case (less x)
        from ‹((⊏)↾A)⇧+⇧+ y x›
        show ?case
        proof (cases rule: tranclp.cases)
          case r_into_trancl
          with induct_step less show ?thesis by auto
        next
          case (trancl_into_trancl b)
          with less show ?thesis by auto
        qed
      qed
    qed
  }
  then show "well_founded UNIV ((⊏)↾A)⇧+⇧+" by unfold_locales auto
qed auto

lemmas Restrp_tranclp_well_founded = Restrp.tranclp.well_founded_axioms
lemmas Restrp_tranclp_induct[consumes 0, case_names less] = Restrp.tranclp.induct

end

context
  fixes A :: "'a set" and less :: "'a ⇒ 'a ⇒ bool" (infix "⊏" 50)
begin

lemma well_foundedI_pf:
  assumes pre: "⋀X. X ⊆ A ⟹ X ⊆ ((⊏) ``` X) ∩ A ⟹ X = {}"
  shows "well_founded A (⊏)"
proof
  fix P a assume aA: "a ∈ A" and Ind: "⋀x. x ∈ A ⟹ (⋀y. y ∈ A ⟹ y ⊏ x ⟹ P y) ⟹ P x"
  from Ind have "{a∈A. ¬P a} ⊆ ((⊏) ``` {a∈A. ¬P a}) ∩ A" by (auto simp: Imagep_def)
  from pre[OF _ this] aA
  show "P a" by auto
qed

lemma well_foundedI_extremal:
  assumes a: "⋀X. X ⊆ A ⟹ X ≠ {} ⟹ ∃x ∈ X. ∀y ∈ X. ¬ y ⊏ x"
  shows "well_founded A (⊏)"
proof (rule well_foundedI_pf)
  fix X assume XA: "X ⊆ A" and pf: "X ⊆ ((⊏) ``` X) ∩ A"
  from a[OF XA] pf show "X = {}" by (auto simp: Imagep_def)
qed

lemma well_founded_iff_ex_extremal:
  "well_founded A (⊏) ⟷ (∀X ⊆ A. X ≠ {} ⟶ (∃x ∈ X. ∀z ∈ X. ¬ z ⊏ x))"
  using well_founded.nonempty_imp_ex_extremal well_foundedI_extremal by blast

end

lemma well_founded_cong:
  assumes r: "⋀a b. a ∈ A ⟹ b ∈ A ⟹ r a b ⟷ r' a b"
    and A: "⋀a b. r' a b ⟹ a ∈ A ⟷ a ∈ A'"
    and B: "⋀a b. r' a b ⟹ b ∈ A ⟷ b ∈ A'"
  shows "well_founded A r ⟷ well_founded A' r'"
proof (intro iffI)
  assume wf: "well_founded A r"
  show "well_founded A' r'"
  proof (intro well_foundedI_extremal)
    fix X
    assume X: "X ⊆ A'" and X0: "X ≠ {}"
    show "∃x∈X. ∀y∈X. ¬ r' y x"
    proof (cases "X ∩ A = {}")
      case True
      from X0 obtain x where xX: "x ∈ X" by auto
      with True have "x ∉ A" by auto
      with xX X have "∀y∈X. ¬ r' y x" by (auto simp: B)
      with xX show ?thesis by auto
    next
      case False
      from well_founded.nonempty_imp_ex_extremal[OF wf _ this]
      obtain x where x: "x ∈ X ∩ A" and Ar: "⋀y. y ∈ X ⟹ y ∈ A ⟹ ¬ r y x" by auto
      have "∀y ∈ X. ¬ r' y x"
      proof (intro ballI notI)
        fix y assume yX: "y ∈ X" and yx: "r' y x"
        from yX X have yA': "y ∈ A'" by auto
        show False
        proof (cases "y ∈ A")
          case True with x Ar[OF yX] yx r show ?thesis by auto
        next
          case False with yA' x A[OF yx] r X show ?thesis by (auto simp:)
        qed
      qed
      with x show "∃x ∈ X. ∀y ∈ X. ¬ r' y x" by auto
    qed
  qed
next
  assume wf: "well_founded A' r'"
  show "well_founded A r"
  proof (intro well_foundedI_extremal)
    fix X
    assume X: "X ⊆ A" and X0: "X ≠ {}"
    show "∃x∈X. ∀y∈X. ¬ r y x"
    proof (cases "X ∩ A' = {}")
      case True
      from X0 obtain x where xX: "x ∈ X" by auto
      with True have "x ∉ A'" by auto
      with xX X B have "∀y∈X. ¬ r y x" by (auto simp: r in_mono)
      with xX show ?thesis by auto
    next
      case False
      from well_founded.nonempty_imp_ex_extremal[OF wf _ this]
      obtain x where x: "x ∈ X ∩ A'" and Ar: "⋀y. y ∈ X ⟹ y ∈ A' ⟹ ¬ r' y x" by auto
      have "∀y ∈ X. ¬ r y x"
      proof (intro ballI notI)
        fix y assume yX: "y ∈ X" and yx: "r y x"
        from yX X have y: "y ∈ A" by auto
        show False
        proof (cases "y ∈ A'")
          case True with x Ar[OF yX] yx r X y show ?thesis by auto
        next
          case False with y x A yx r X show ?thesis by auto
        qed
      qed
      with x show "∃x ∈ X. ∀y ∈ X. ¬ r y x" by auto
    qed
  qed
qed

lemma wfP_iff_well_founded_UNIV: "wfP r ⟷ well_founded UNIV r"
  by (auto simp: wfP_def wf_def well_founded_def)

lemma well_founded_empty[intro!]: "well_founded {} r"
  by (auto simp: well_founded_iff_ex_extremal)

lemma well_founded_singleton:
  assumes "¬r x x" shows "well_founded {x} r"
  using assms by (auto simp: well_founded_iff_ex_extremal)

lemma well_founded_Restrp[simp]: "well_founded A (r↾B) ⟷ well_founded (A∩B) r" (is "?l ⟷ ?r")
proof (intro iffI well_foundedI_extremal)
  assume l: ?l
  fix X assume XAB: "X ⊆ A ∩ B" and X0: "X ≠ {}"
  with l[THEN well_founded.nonempty_imp_ex_extremal]
  have "∃x∈X. ∀z∈X. ¬ (r ↾ B) z x" by auto
  with XAB show "∃x∈X. ∀y∈X. ¬ r y x" by (auto simp: Restrp_def)
next
  assume r: ?r
  fix X assume XA: "X ⊆ A" and X0: "X ≠ {}"
  show "∃x∈X. ∀y∈X. ¬ (r ↾ B) y x"
  proof (cases "X ⊆ B")
    case True
    with r[THEN well_founded.nonempty_imp_ex_extremal, of X] XA X0
    have "∃z∈X. ∀y∈X. ¬ r y z" by auto
    then show ?thesis by auto
  next
    case False
    then obtain x where x: "x ∈ X - B" by auto
    then have "∀y∈X. ¬ (r ↾ B) y x" by auto
    with x show ?thesis by auto
  qed
qed

lemma Restrp_tranclp_well_founded_iff:
  fixes less (infix "⊏" 50)
  shows "well_founded UNIV ((⊏) ↾ A)⇧+⇧+ ⟷ well_founded A (⊏)" (is "?l ⟷ ?r")
proof (rule iffI)
  show "?r ⟹ ?l" by (fact well_founded.Restrp_tranclp_well_founded)
  assume ?l
  then interpret well_founded UNIV "((⊏) ↾ A)⇧+⇧+".
  show ?r
  proof (unfold well_founded_iff_ex_extremal, intro allI impI)
    fix X assume XA: "X ⊆ A" and X0: "X ≠ {}"
    from nonempty_imp_ex_extremal[OF _ X0]
    obtain z where zX: "z ∈ X" and Xz: "∀y∈X. ¬ ((⊏) ↾ A)⇧+⇧+ y z" by auto
    show "∃z ∈ X. ∀y ∈ X. ¬ y ⊏ z"
    proof (intro bexI[OF _ zX] ballI notI)
      fix y assume yX: "y ∈ X" and yz: "y ⊏ z"
      from yX yz zX XA have "((⊏) ↾ A) y z" by auto
      with yX Xz show False by auto
    qed
  qed
qed

lemma (in well_founded) well_founded_subset:
  assumes "B ⊆ A" shows "well_founded B (⊏)"
  using assms well_founded_axioms by (auto simp: well_founded_iff_ex_extremal)

lemma well_founded_extend:
  fixes less (infix "⊏" 50)
  assumes A: "well_founded A (⊏)"
  assumes B: "well_founded B (⊏)"
  assumes AB: "∀a ∈ A. ∀b ∈ B. ¬b ⊏ a"
  shows "well_founded (A ∪ B) (⊏)"
proof (intro well_foundedI_extremal)
  interpret A: well_founded A "(⊏)" using A.
  interpret B: well_founded B "(⊏)" using B.
  fix X assume XAB: "X ⊆ A ∪ B" and X0: "X ≠ {}"
  show "∃x∈X. ∀y∈X. ¬ y ⊏ x"
  proof (cases "X ∩ A = {}")
    case True
    with XAB have XB: "X ⊆ B" by auto
    from B.nonempty_imp_ex_extremal[OF XB X0] show ?thesis.
  next
    case False
    with A.nonempty_imp_ex_extremal[OF _ this]
    obtain e where XAe: "e ∈ X ∩ A" "∀y∈X ∩ A. ¬ y ⊏ e" by auto
    then have eX: "e ∈ X" and eA: "e ∈ A" by auto
    { fix x assume xX: "x ∈ X"
      have "¬x ⊏ e"
      proof (cases "x ∈ A")
        case True with XAe xX show ?thesis by auto
      next
        case False
        with xX XAB have "x ∈ B" by auto
        with AB eA show ?thesis by auto
      qed
    }
    with eX show ?thesis by auto
  qed
qed

lemma closed_UN_well_founded:
  fixes r (infix "⊏" 50)
  assumes XX: "∀X∈XX. well_founded X (⊏) ∧ (∀x∈X. ∀y∈⋃XX. y ⊏ x ⟶ y ∈ X)"
  shows "well_founded (⋃XX) (⊏)"
proof (intro well_foundedI_extremal)
  have *: "X ∈ XX ⟹ x∈X ⟹ y ∈ ⋃XX ⟹ y ⊏ x ⟹ y ∈ X" for X x y using XX by blast
  fix S
  assume S: "S ⊆ ⋃XX" and S0: "S ≠ {}"
  from S0 obtain x where xS: "x ∈ S" by auto
  with S obtain X where X: "X ∈ XX" and xX: "x ∈ X" by auto
  from xS xX have Sx0: "S ∩ X ≠ {}" by auto
  from X XX interpret well_founded X "(⊏)" by auto
  from nonempty_imp_ex_extremal[OF _ Sx0]
  obtain z where zS: "z ∈ S" and zX: "z ∈ X" and min: "∀y ∈ S ∩ X. ¬ y ⊏ z" by auto
  show "∃x∈S. ∀y∈S. ¬ y ⊏ x"
  proof (intro bexI[OF _ zS] ballI notI)
    fix y
    assume yS: "y ∈ S" and yz: "y ⊏ z"
    have yXX: "y ∈ ⋃ XX" using S yS by auto
    from *[OF X zX yXX yz] yS have "y ∈ X ∩ S" by auto
    with min yz show False by auto
  qed
qed

lemma well_founded_cmono:
  assumes r': "r' ≤ r" and wf: "well_founded A r"
  shows "well_founded A r'"
proof (intro well_foundedI_extremal)
  fix X assume "X ⊆ A" and "X ≠ {}"
  from well_founded.nonempty_imp_ex_extremal[OF wf this]
  show "∃x∈X. ∀y∈X. ¬ r' y x" using r' by auto
qed

locale well_founded_ordered_set = well_founded + transitive _ "(⊏)"
begin

sublocale strict_ordered_set..

interpretation Restrp: strict_ordered_set UNIV "(⊏)↾A" + Restrp: well_founded UNIV "(⊏)↾A"
  using Restrp_strict_order Restrp_well_founded .

lemma Restrp_well_founded_order: "well_founded_ordered_set UNIV ((⊏)↾A)"..

lemma well_founded_ordered_subset: "B ⊆ A ⟹ well_founded_ordered_set B (⊏)"
  apply intro_locales
  using well_founded_subset transitive_subset by auto

end

lemmas well_founded_ordered_setI = well_founded_ordered_set.intro

lemma well_founded_ordered_set_empty[intro!]: "well_founded_ordered_set {} r"
  by (auto intro!: well_founded_ordered_setI)


locale well_related_set = related_set +
  assumes nonempty_imp_ex_extreme: "X ⊆ A ⟹ X ≠ {} ⟹ ∃e. extreme X (⊑)⇧- e"
begin

sublocale connex
proof
  fix x y assume "x ∈ A" and "y ∈ A"
  with nonempty_imp_ex_extreme[of "{x,y}"] show "x ⊑ y ∨ y ⊑ x" by auto 
qed

lemmas connex = connex_axioms(* I'd like to access well_related_set.connex_axioms,
  but it's not visible without interpretation. *)

interpretation less_eq_asymmetrize.

sublocale asym: well_founded A "(⊏)"
proof (unfold well_founded_iff_ex_extremal, intro allI impI)
  fix X
  assume XA: "X ⊆ A" and X0: "X ≠ {}"
  from nonempty_imp_ex_extreme[OF XA X0] obtain e where "extreme X (⊑)⇧- e" by auto
  then show "∃x∈X. ∀z∈X. ¬z ⊏ x" by (auto intro!: bexI[of _ e])
qed

lemma well_related_subset: "B ⊆ A ⟹ well_related_set B (⊑)"
  by (auto intro!: well_related_set.intro nonempty_imp_ex_extreme)

lemma monotone_image_well_related:
  fixes leB (infix "⊴" 50)
  assumes mono: "monotone_on A (⊑) (⊴) f" shows "well_related_set (f ` A) (⊴)"
proof (intro well_related_set.intro)
  interpret less_eq_dualize.
  fix X' assume X'fA: "X' ⊆ f ` A" and X'0: "X' ≠ {}"
  then obtain X where XA: "X ⊆ A" and X': "X' = f ` X" and X0: "X ≠ {}"
    by (auto elim!: subset_imageE)
  from nonempty_imp_ex_extreme[OF XA X0]
  obtain e where Xe: "extreme X (⊒) e" by auto
  note monotone_on_subset[OF mono XA]
  note monotone_on_dual[OF this]
  from monotone_image_extreme[OF this Xe]
  show "∃e'. extreme X' (⊴)⇧- e'" by (auto simp: X')
qed

end

sublocale well_related_set ⊆ reflexive using local.reflexive_axioms.

lemmas well_related_setI = well_related_set.intro

lemmas well_related_iff_ex_extreme = well_related_set_def

lemma well_related_set_empty[intro!]: "well_related_set {} r"
  by (auto intro!: well_related_setI)

context
  fixes less_eq :: "'a ⇒ 'a ⇒ bool" (infix "⊑" 50)
begin

lemma well_related_iff_neg_well_founded:
  "well_related_set A (⊑) ⟷ well_founded A (λx y. ¬ y ⊑ x)"
  by (simp add: well_related_set_def well_founded_iff_ex_extremal extreme_def Bex_def)

lemma well_related_singleton_refl: 
  assumes "x ⊑ x" shows "well_related_set {x} (⊑)"
  by (intro well_related_set.intro exI[of _ x], auto simp: subset_singleton_iff assms)

lemma closed_UN_well_related:
  assumes XX: "∀X∈XX. well_related_set X (⊑) ∧ (∀x∈X. ∀y∈⋃XX. ¬x ⊑ y ⟶ y ∈ X)"
  shows "well_related_set (⋃XX) (⊑)"
  using XX
  apply (unfold well_related_iff_neg_well_founded)
  using closed_UN_well_founded[of _ "λx y. ¬ y ⊑ x"].

end

lemma well_related_extend:
  fixes r (infix "⊑" 50)
  assumes "well_related_set A (⊑)" and "well_related_set B (⊑)" and "∀a ∈ A. ∀b ∈ B. a ⊑ b"
  shows "well_related_set (A ∪ B) (⊑)"
  using well_founded_extend[of _ "λx y. ¬ y ⊑ x", folded well_related_iff_neg_well_founded]
  using assms by auto

lemma pair_well_related:
  fixes less_eq (infix "⊑" 50)
  assumes "i ⊑ i" and "i ⊑ j" and "j ⊑ j"
  shows "well_related_set {i, j} (⊑)"
proof (intro well_related_setI)
  fix X assume "X ⊆ {i,j}" and "X ≠ {}"
  then have "X = {i,j} ∨ X = {i} ∨ X = {j}" by auto
  with assms show "∃e. extreme X (⊑)⇧- e" by auto
qed

locale pre_well_ordered_set = semiattractive + well_related_set
begin

interpretation less_eq_asymmetrize.

sublocale transitive
proof
  fix x y z assume xy: "x ⊑ y" and yz: "y ⊑ z" and x: "x ∈ A" and y: "y ∈ A" and z: "z ∈ A"
  from x y z have "∃e. extreme {x,y,z} (⊒) e" (is "∃e. ?P e") by (auto intro!: nonempty_imp_ex_extreme)
  then have "?P x ∨ ?P y ∨ ?P z" by auto
  then show "x ⊑ z"
  proof (elim disjE)
    assume "?P x"
    then show ?thesis by auto
  next
    assume "?P y"
    then have "y ⊑ x" by auto
    from attract[OF xy this yz] x y z show ?thesis by auto
  next
    assume "?P z"
    then have zx: "z ⊑ x" and zy: "z ⊑ y" by auto
    from attract[OF yz zy zx] x y z have yx: "y ⊑ x" by auto
    from attract[OF xy yx yz] x y z show ?thesis by auto
  qed
qed

sublocale total_quasi_ordered_set..

end

lemmas pre_well_ordered_iff_semiattractive_well_related =
  pre_well_ordered_set_def[unfolded atomize_eq]

lemma pre_well_ordered_set_empty[intro!]: "pre_well_ordered_set {} r"
  by (auto simp: pre_well_ordered_iff_semiattractive_well_related)

lemma pre_well_ordered_iff:
  "pre_well_ordered_set A r ⟷ total_quasi_ordered_set A r ∧ well_founded A (asympartp r)"
  (is "?p ⟷ ?t ∧ ?w")
proof safe
  assume ?p
  then interpret pre_well_ordered_set A r.
  show ?t ?w by unfold_locales
next
  assume ?t
  then interpret total_quasi_ordered_set A r.
  assume ?w
  then have "well_founded UNIV (asympartp r ↾ A)" by simp
  also have "asympartp r ↾ A = (λx y. ¬ r y x) ↾ A" by (intro ext, auto simp: not_iff_asym)
  finally have "well_related_set A r" by (simp add: well_related_iff_neg_well_founded)
  then show ?p by intro_locales
qed

lemma (in semiattractive) pre_well_ordered_iff_well_related:
  assumes XA: "X ⊆ A"
  shows "pre_well_ordered_set X (⊑) ⟷ well_related_set X (⊑)" (is "?l ⟷ ?r")
proof
  interpret X: semiattractive X using semiattractive_subset[OF XA].
  { assume ?l
    then interpret X: pre_well_ordered_set X.
    show ?r by unfold_locales
  }
  assume ?r
  then interpret X: well_related_set X.
  show ?l by unfold_locales
qed

lemma semiattractive_extend:
  fixes r (infix "⊑" 50)
  assumes A: "semiattractive A (⊑)" and B: "semiattractive B (⊑)"
    and AB: "∀a ∈ A. ∀b ∈ B. a ⊑ b ∧ ¬ b ⊑ a"
  shows "semiattractive (A ∪ B) (⊑)"
proof-
  interpret A: semiattractive A "(⊑)" using A.
  interpret B: semiattractive B "(⊑)" using B.
  {
    fix x y z
    assume yB: "y ∈ B" and zA: "z ∈ A" and yz: "y ⊑ z"
    have False using AB[rule_format, OF zA yB] yz by auto
  }
  note * = this
  show ?thesis 
    by (auto intro!: semiattractive.intro dest:* AB[rule_format] A.attract B.attract)
qed

lemma pre_well_order_extend:
  fixes r (infix "⊑" 50)
  assumes A: "pre_well_ordered_set A (⊑)" and B: "pre_well_ordered_set B (⊑)"
    and AB: "∀a ∈ A. ∀b ∈ B. a ⊑ b ∧ ¬ b ⊑ a"
  shows "pre_well_ordered_set (A∪B) (⊑)"
proof-
  interpret A: pre_well_ordered_set A "(⊑)" using A.
  interpret B: pre_well_ordered_set B "(⊑)" using B.
  show ?thesis
    apply (intro pre_well_ordered_set.intro well_related_extend semiattractive_extend)
    apply unfold_locales
    by (auto dest: AB[rule_format])
qed

lemma (in well_related_set) monotone_image_pre_well_ordered:
  fixes leB (infix "⊑''" 50)
  assumes mono: "monotone_on A (⊑) (⊑') f"
    and image: "semiattractive (f ` A) (⊑')"
  shows "pre_well_ordered_set (f ` A) (⊑')"
  by (intro pre_well_ordered_set.intro monotone_image_well_related[OF mono] image)

locale well_ordered_set = antisymmetric + well_related_set
begin

sublocale pre_well_ordered_set..

sublocale total_ordered_set..

lemma well_ordered_subset: "B ⊆ A ⟹ well_ordered_set B (⊑)"
  using well_related_subset antisymmetric_subset by (intro well_ordered_set.intro)

sublocale asym: well_founded_ordered_set A "asympartp (⊑)"
  by (intro well_founded_ordered_set.intro asym.well_founded_axioms asympartp_transitive)

end

lemmas well_ordered_iff_antisymmetric_well_related = well_ordered_set_def[unfolded atomize_eq]

lemma well_ordered_set_empty[intro!]: "well_ordered_set {} r"
  by (auto simp: well_ordered_iff_antisymmetric_well_related)

lemma (in antisymmetric) well_ordered_iff_well_related:
  assumes XA: "X ⊆ A"
  shows "well_ordered_set X (⊑) ⟷ well_related_set X (⊑)" (is "?l ⟷ ?r")
proof
  interpret X: antisymmetric X using antisymmetric_subset[OF XA].
  { assume ?l
    then interpret X: well_ordered_set X.
    show ?r by unfold_locales
  }
  assume ?r
  then interpret X: well_related_set X.
  show ?l by unfold_locales
qed

context
  fixes A :: "'a set" and less_eq :: "'a ⇒ 'a ⇒ bool" (infix "⊑" 50)
begin

context
  assumes A: "∀a ∈ A. ∀b ∈ A. a ⊑ b"
begin

interpretation well_related_set A "(⊑)"
  apply unfold_locales
  using A by blast

lemmas trivial_well_related = well_related_set_axioms

lemma trivial_pre_well_order: "pre_well_ordered_set A (⊑)"
  apply unfold_locales
  using A by blast

end

interpretation less_eq_asymmetrize.

lemma well_ordered_iff_well_founded_total_ordered:
  "well_ordered_set A (⊑) ⟷ total_ordered_set A (⊑) ∧ well_founded A (⊏)"
proof (safe)
  assume "well_ordered_set A (⊑)"
  then interpret well_ordered_set A "(⊑)".
  show "total_ordered_set A (⊑)" "well_founded A (⊏)" by unfold_locales
next
  assume "total_ordered_set A (⊑)" and "well_founded A (⊏)"
  then interpret total_ordered_set A "(⊑)" + asympartp: well_founded A "(⊏)".
  show "well_ordered_set A (⊑)"
  proof
    fix X assume XA: "X ⊆ A" and "X ≠ {}"
    from XA asympartp.nonempty_imp_ex_extremal[OF this] 
    show "∃e. extreme X (⊒) e" by (auto simp: not_asym_iff subsetD)
  qed
qed

end

context
  fixes less_eq :: "'a ⇒ 'a ⇒ bool" (infix "⊑" 50)
begin

lemma well_order_extend:
  assumes A: "well_ordered_set A (⊑)" and B: "well_ordered_set B (⊑)"
    and ABa: "∀a ∈ A. ∀b ∈ B. a ⊑ b ⟶ b ⊑ a ⟶ a = b"
    and AB: "∀a ∈ A. ∀b ∈ B. a ⊑ b"
  shows "well_ordered_set (A∪B) (⊑)"
proof-
  interpret A: well_ordered_set A "(⊑)" using A.
  interpret B: well_ordered_set B "(⊑)" using B.
  show ?thesis
    apply (intro well_ordered_set.intro antisymmetric_union well_related_extend ABa AB)
    by unfold_locales
qed

interpretation singleton: antisymmetric "{a}" "(⊑)" for a apply unfold_locales by auto

lemmas singleton_antisymmetric[intro!] = singleton.antisymmetric_axioms

lemma singleton_well_ordered[intro!]: "a ⊑ a ⟹ well_ordered_set {a} (⊑)"
  apply unfold_locales by auto

lemma closed_UN_well_ordered:
  assumes anti: "antisymmetric (⋃ XX) (⊑)"
    and XX: "∀X∈XX. well_ordered_set X (⊑) ∧ (∀x∈X. ∀y∈⋃XX. ¬ x ⊑ y ⟶ y ∈ X)"
  shows "well_ordered_set (⋃XX) (⊑)"
  apply (intro well_ordered_set.intro closed_UN_well_related anti)
  using XX well_ordered_set.axioms by fast

end

lemma (in well_related_set) monotone_image_well_ordered:
  fixes leB (infix "⊑''" 50)
  assumes mono: "monotone_on A (⊑) (⊑') f"
    and image: "antisymmetric (f ` A) (⊑')"
  shows "well_ordered_set (f ` A) (⊑')"
  by (intro well_ordered_set.intro monotone_image_well_related[OF mono] image)


subsection ‹Relating to Classes›

locale well_founded_quasi_ordering = quasi_ordering + well_founded
begin

lemma well_founded_quasi_ordering_subset:
  assumes "X ⊆ A" shows "well_founded_quasi_ordering X (⊑) (⊏)"
  by (intro well_founded_quasi_ordering.intro quasi_ordering_subset well_founded_subset assms)

end

class wf_qorder = ord +
  assumes "well_founded_quasi_ordering UNIV (≤) (<)"
begin

interpretation well_founded_quasi_ordering UNIV
  using wf_qorder_axioms unfolding class.wf_qorder_def by auto

subclass qorder ..

sublocale order: well_founded_quasi_ordering UNIV
  rewrites "⋀x. x ∈ UNIV ≡ True"
    and "⋀X. X ⊆ UNIV ≡ True"
    and "⋀r. r ↾ UNIV ≡ r"
    and "⋀P. True ∧ P ≡ P"
    and "Ball UNIV ≡ All"
    and "Bex UNIV ≡ Ex"
    and "sympartp (≤)⇧- ≡ sympartp (≤)"
    and "⋀P1. (True ⟹ PROP P1) ≡ PROP P1"
    and "⋀P1. (True ⟹ P1) ≡ Trueprop P1"
    and "⋀P1 P2. (True ⟹ PROP P1 ⟹ PROP P2) ≡ (PROP P1 ⟹ PROP P2)"
  apply unfold_locales by (auto simp:atomize_eq)

end

context wellorder begin

subclass wf_qorder
  apply (unfold_locales)
  using less_induct by auto

sublocale order: well_ordered_set UNIV
  rewrites "⋀x. x ∈ UNIV ≡ True"
    and "⋀X. X ⊆ UNIV ≡ True"
    and "⋀r. r ↾ UNIV ≡ r"
    and "⋀P. True ∧ P ≡ P"
    and "Ball UNIV ≡ All"
    and "Bex UNIV ≡ Ex"
    and "sympartp (≤)⇧- ≡ sympartp (≤)"
    and "⋀P1. (True ⟹ PROP P1) ≡ PROP P1"
    and "⋀P1. (True ⟹ P1) ≡ Trueprop P1"
    and "⋀P1 P2. (True ⟹ PROP P1 ⟹ PROP P2) ≡ (PROP P1 ⟹ PROP P2)"
  apply (unfold well_ordered_iff_well_founded_total_ordered)
  apply (intro conjI order.total_ordered_set_axioms)
  by (auto simp: order.well_founded_axioms atomize_eq)

end

thm order.nonempty_imp_ex_extreme

subsection ‹omega-Chains›

definition "omega_chain A r ≡ ∃f :: nat ⇒ 'a. monotone (≤) r f ∧ range f = A"

lemma omega_chainI:
  fixes f :: "nat ⇒ 'a"
  assumes "monotone (≤) r f" "range f = A" shows "omega_chain A r"
  using assms by (auto simp: omega_chain_def)

lemma omega_chainE:
  assumes "omega_chain A r"
    and "⋀f :: nat ⇒ 'a. monotone (≤) r f ⟹ range f = A ⟹ thesis"
  shows thesis
  using assms by (auto simp: omega_chain_def)

lemma (in transitive) local_chain:
  assumes CA: "range C ⊆ A"
  shows "(∀i::nat. C i ⊑ C (Suc i)) ⟷ monotone (<) (⊑) C"
proof (intro iffI allI monotoneI)
  fix i j :: nat
  assume loc: "∀i. C i ⊑ C (Suc i)" and ij: "i < j"
  have "C i ⊑ C (i+k+1)" for k
  proof (induct k)
    case 0
    from loc show ?case by auto
  next
    case (Suc k)
    also have "C (i+k+1) ⊑ C (i+k+Suc 1)" using loc by auto
    finally show ?case using CA by auto
  qed
  from this[of "j-i-1"] ij show "C i ⊑ C j" by auto
next
  fix i
  assume "monotone (<) (⊑) C"
  then show "C i ⊑ C (Suc i)" by (auto dest: monotoneD)
qed

lemma pair_omega_chain:
  assumes "r a a" "r b b" "r a b" shows "omega_chain {a,b} r"
  using assms by (auto intro!: omega_chainI[of r "λi. if i = 0 then a else b"] monotoneI)

text ‹Every omega-chain is a well-order.›

lemma omega_chain_imp_well_related:
  fixes less_eq (infix "⊑" 50)
  assumes A: "omega_chain A (⊑)" shows "well_related_set A (⊑)"
proof
  interpret less_eq_dualize.
  from A obtain f :: "nat ⇒ 'a" where mono: "monotone_on UNIV (≤) (⊑) f" and A: "A = range f"
    by (auto elim!: omega_chainE)
  fix X assume XA: "X ⊆ A" and "X ≠ {}"
  then obtain I where X: "X = f ` I" and I0: "I ≠ {}" by (auto simp: A subset_image_iff)
  from order.nonempty_imp_ex_extreme[OF I0]
  obtain i where "least I i" by auto
  with mono 
  show "∃e. extreme X (⊒) e" by (auto intro!: exI[of _ "f i"] extremeI simp: X monotoneD)
qed

lemma (in semiattractive) omega_chain_imp_pre_well_ordered:
  assumes "omega_chain A (⊑)" shows "pre_well_ordered_set A (⊑)"
  apply (intro pre_well_ordered_set.intro omega_chain_imp_well_related assms)..

lemma (in antisymmetric) omega_chain_imp_well_ordered:
  assumes "omega_chain A (⊑)" shows "well_ordered_set A (⊑)"
  by (intro well_ordered_set.intro omega_chain_imp_well_related assms antisymmetric_axioms)

subsubsection ‹Relation image that preserves well-orderedness.›

definition "well_image f A (⊑) fa fb ≡
  ∀a b. extreme {x∈A. fa = f x} (⊑)⇧- a ⟶ extreme {y∈A. fb = f y} (⊑)⇧- b ⟶ a ⊑ b"
  for less_eq (infix "⊑" 50)

lemmas well_imageI = well_image_def[unfolded atomize_eq, THEN iffD2, rule_format]
lemmas well_imageD = well_image_def[unfolded atomize_eq, THEN iffD1, rule_format]

lemma (in pre_well_ordered_set)
  well_image_well_related: "pre_well_ordered_set (f`A) (well_image f A (⊑))"
proof-
  interpret less_eq_dualize.
  interpret im: transitive "f`A" "well_image f A (⊑)"
  proof (safe intro!: transitiveI well_imageI)
    interpret less_eq_dualize.
    fix x y z a c
    assume fxfy: "well_image f A (⊑) (f x) (f y)"
      and fyfz: "well_image f A (⊑) (f y) (f z)"
      and xA: "x ∈ A" and yA: "y ∈ A" and zA: "z ∈ A"
      and a: "extreme {a ∈ A. f x = f a} (⊒) a"
      and c: "extreme {c ∈ A. f z = f c} (⊒) c"
    have "∃b. extreme {b ∈ A. f y = f b} (⊒) b"
      apply (rule nonempty_imp_ex_extreme) using yA by auto
    then obtain b where b: "extreme {b ∈ A. f y = f b} (⊒) b" by auto
    from trans[OF well_imageD[OF fxfy a b] well_imageD[OF fyfz b c]] a b c
    show "a ⊑ c" by auto
  qed
  interpret im: well_related_set "f`A" "well_image f A (⊑)"
  proof
    fix fX
    assume fXfA: "fX ⊆ f ` A" and fX0: "fX ≠ {}"
    define X where "X ≡ {x∈A. f x ∈ fX}"
    with fXfA fX0 have XA: "X ⊆ A" and "X ≠ {}" by (auto simp: ex_in_conv[symmetric])
    from nonempty_imp_ex_extreme[OF this] obtain e where Xe: "extreme X (⊒) e" by auto
    with XA have eA: "e ∈ A" by auto
    from fXfA have fX: "f ` X = fX" by (auto simp: X_def intro!: equalityI)
    show "∃fe. extreme fX (well_image f A (⊑))⇧- fe"
    proof (safe intro!: exI extremeI elim!: subset_imageE)
      from Xe fX show fefX: "f e ∈ fX" by auto
      fix fx assume fxfX: "fx ∈ fX"
      show "well_image f A (⊑) (f e) fx"
      proof (intro well_imageI)
        fix a b
        assume fea: "extreme {a ∈ A. f e = f a} (⊒) a"
          and feb: "extreme {b ∈ A. fx = f b} (⊒) b"
        from fea eA have aA: "a ∈ A" and ae: "a ⊑ e" by auto
        from feb fxfX have bA: "b ∈ A" and bX: "b ∈ X" by (auto simp: X_def)
        with Xe have eb: "e ⊑ b" by auto
        from trans[OF ae eb aA eA bA]
        show "a ⊑ b".
      qed
    qed
  qed
  show ?thesis by unfold_locales
qed


end