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 "(⊏)AUNIV = (⊏)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 "{aA. ¬P a}  ((⊏) ``` {aA. ¬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 "xX. yX. ¬ 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 "yX. ¬ 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 "xX. yX. ¬ 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 "yX. ¬ 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 (rB)  well_founded (AB) 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 "xX. zX. ¬ (r  B) z x" by auto
  with XAB show "xX. yX. ¬ r y x" by (auto simp: Restrp_def)
next
  assume r: ?r
  fix X assume XA: "X  A" and X0: "X  {}"
  show "xX. yX. ¬ (r  B) y x"
  proof (cases "X  B")
    case True
    with r[THEN well_founded.nonempty_imp_ex_extremal, of X] XA X0
    have "zX. yX. ¬ 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 "yX. ¬ (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: "yX. ¬ ((⊏)  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 "xX. yX. ¬ 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" "yX  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: "XXX. well_founded X (⊏)  (xX. yXX. y  x  y  X)"
  shows "well_founded (XX) (⊏)"
proof (intro well_foundedI_extremal)
  have *: "X  XX  xX  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 "xS. yS. ¬ 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 "xX. yX. ¬ 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 "xX. zX. ¬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: "XXX. well_related_set X (⊑)  (xX. yXX. ¬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 (AB) (⊑)"
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 (AB) (⊑)"
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: "XXX. well_ordered_set X (⊑)  (xX. yXX. ¬ 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 {xA. fa = f x} (⊑)- a  extreme {yA. 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  {xA. 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