Theory Complete_Non_Orders.Complete_Relations

(*
Author:  Akihisa Yamada (2018-2021)
License: LGPL (see file COPYING.LESSER)
*)
section ‹ Completeness of Relations ›

text ‹Here we formalize various order-theoretic completeness conditions.›

theory Complete_Relations
  imports Well_Relations Directedness
begin

subsection ‹Completeness Conditions›

text ‹Order-theoretic completeness demands certain subsets of elements to admit suprema or infima.›

definition complete ("_-complete"[999]1000) where
 "𝒞-complete A (⊑) ≡ ∀X ⊆ A. 𝒞 X (⊑) ⟶ (∃s. extreme_bound A (⊑) X s)" for less_eq (infix "⊑" 50)

lemmas completeI = complete_def[unfolded atomize_eq, THEN iffD2, rule_format]
lemmas completeD = complete_def[unfolded atomize_eq, THEN iffD1, rule_format]
lemmas completeE = complete_def[unfolded atomize_eq, THEN iffD1, rule_format, THEN exE]

lemma complete_cmono: "CC ≤ DD ⟹ DD-complete ≤ CC-complete"
  by (force simp: complete_def)

lemma complete_subclass:
  fixes less_eq (infix "⊑" 50)
  assumes "𝒞-complete A (⊑)" and "∀X ⊆ A. 𝒟 X (⊑) ⟶ 𝒞 X (⊑)"
  shows "𝒟-complete A (⊑)"
  using assms by (auto simp: complete_def)


lemma complete_empty[simp]: "𝒞-complete {} r ⟷ ¬ 𝒞 {} r" by (auto simp: complete_def)

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

text‹Toppedness can be also seen as a completeness condition,
since it is equivalent to saying that the universe has a supremum.›

lemma extremed_iff_UNIV_complete: "extremed A (⊑) ⟷ (λX r. X = A)-complete A (⊑)" (is "?l ⟷ ?r")
proof
  assume ?l
  then obtain e where "extreme A (⊑) e" by (erule extremedE)
  then have "extreme_bound A (⊑) A e" by auto
  then show ?r by (auto intro!: completeI)
next
  assume ?r
  from completeD[OF this] obtain s where "extreme_bound A (⊑) A s" by auto
  then have "extreme A (⊑) s" by auto
  then show ?l by (auto simp: extremed_def)
qed

text ‹The dual notion of topped is called ``pointed'', equivalently ensuring a supremum
of the empty set.›

lemma pointed_iff_empty_complete: "extremed A (⊑) ⟷ (λX r. X = {})-complete A (⊑)⇧-"
  by (auto simp: complete_def extremed_def)

text ‹Downward closure is topped.›
lemma dual_closure_is_extremed:
  assumes bA: "b ∈ A" and "b ⊑ b"
  shows "extremed {a ∈ A. a ⊑ b} (⊑)"
  using assms by (auto intro!: extremedI[of _ _ b])

text ‹Downward closure preserves completeness.›
lemma dual_closure_is_complete:
  assumes A: "𝒞-complete A (⊑)" and bA: "b ∈ A"
  shows "𝒞-complete {x∈A. x ⊑ b} (⊑)"
proof (intro completeI)
  fix X assume XAb:"X ⊆ {x ∈ A. x ⊑ b}" and X: "𝒞 X (⊑)"
  with completeD[OF A] obtain x where x: "extreme_bound A (⊑) X x" by auto
  then have xA: "x ∈ A" by auto
  from XAb have "x ⊑ b" by (auto intro!: extreme_boundD[OF x] bA)
  with xA x show "∃x. extreme_bound {x ∈ A. x ⊑ b} (⊑) X x" by (auto intro!: exI[of _ x])
qed

interpretation less_eq_dualize.

text ‹Upward closure preserves completeness, under a condition.›
lemma closure_is_complete:
  assumes A: "𝒞-complete A (⊑)" and bA: "b ∈ A"
    and Cb: "∀X ⊆ A. 𝒞 X (⊑) ⟶ bound X (⊒) b ⟶ 𝒞 (X ∪ {b}) (⊑)"
  shows "𝒞-complete {x∈A. b ⊑ x} (⊑)"
proof (intro completeI)
  fix X assume XAb:"X ⊆ {x ∈ A. b ⊑ x}" and X: "𝒞 X (⊑)"
  with Cb have XbC: "𝒞 (X ∪ {b}) (⊑)" by auto
  from XAb bA have XbA: "X ∪ {b} ⊆ A" by auto
  with completeD[OF A XbA] XbC
  obtain x where x: "extreme_bound A (⊑) (X∪{b}) x" by auto
  then show "∃x. extreme_bound {x ∈ A. b ⊑ x} (⊑) X x"
    by (auto intro!: exI[of _ x] extreme_boundI)
qed

lemma biclosure_is_complete:
  assumes A: "𝒞-complete A (⊑)" and aA: "a ∈ A" and bA: "b ∈ A" and ab: "a ⊑ b"
    and Ca: "∀X ⊆ A. 𝒞 X (⊑) ⟶ bound X (⊒) a ⟶ 𝒞 (X ∪ {a}) (⊑)"
  shows "𝒞-complete {x∈A. a ⊑ x ∧ x ⊑ b} (⊑)"
proof-
  note closure_is_complete[OF A aA Ca]
  from dual_closure_is_complete[OF this, of b] bA ab show ?thesis by auto
qed

end


text ‹One of the most well-studied notion of completeness would be the semilattice condition:
every pair of elements $x$ and $y$ has a supremum $x \sqcup y$
(not necessarily unique if the underlying relation is not antisymmetric).›

definition "pair_complete ≡ (λX r. ∃x y. X = {x,y})-complete"

lemma pair_completeI:
  assumes "⋀x y. x ∈ A ⟹ y ∈ A ⟹ ∃s. extreme_bound A r {x,y} s"
  shows "pair_complete A r"
  using assms by (auto simp: pair_complete_def complete_def)

lemma pair_completeD:
  assumes "pair_complete A r"
  shows "x ∈ A ⟹ y ∈ A ⟹ ∃s. extreme_bound A r {x,y} s"
   by (intro completeD[OF assms[unfolded pair_complete_def]], auto)


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

lemma pair_complete_imp_directed:
  assumes comp: "pair_complete A (⊑)" shows "directed A (⊑)"
proof
  fix x y :: 'a
  assume "x ∈ A" "y ∈ A"
  with pair_completeD[OF comp this] show "∃z ∈ A. x ⊑ z ∧ y ⊑ z" by auto
qed

end

lemma (in connex) pair_complete: "pair_complete A (⊑)"
proof (safe intro!: pair_completeI)
  fix x y
  assume x: "x ∈ A" and y: "y ∈ A"
  then show "∃s. extreme_bound A (⊑) {x, y} s"
  proof (cases rule:comparable_cases)
    case le
    with x y show ?thesis by (auto intro!: exI[of _ y])
  next
    case ge
    with x y show ?thesis by (auto intro!: exI[of _ x])
  qed
qed

text ‹The next one assumes that every nonempty finite set has a supremum.›

abbreviation "finite_complete ≡ (λX r. finite X ∧ X ≠ {})-complete"

lemma finite_complete_le_pair_complete: "finite_complete ≤ pair_complete"
  by (unfold pair_complete_def, rule complete_cmono, auto)

text ‹The next one assumes that every nonempty bounded set has a supremum.
It is also called the Dedekind completeness.›

abbreviation "conditionally_complete A ≡ (λX r. ∃b ∈ A. bound X r b ∧ X ≠ {})-complete A"

lemma conditionally_complete_imp_nonempty_imp_ex_extreme_bound_iff_ex_bound:
  assumes comp: "conditionally_complete A r"
  assumes "X ⊆ A" and "X ≠ {}"
  shows "(∃s. extreme_bound A r X s) ⟷ (∃b∈A. bound X r b)"
  using assms by (auto 0 4 intro!:completeD[OF comp])

text ‹The $\omega$-completeness condition demands a supremum for an $\omega$-chain.›

text‹\emph{Directed completeness} is an important notion in domain theory~\cite{abramski94},
asserting that every nonempty directed set has a supremum.
Here, a set $X$ is \emph{directed} if any pair of two elements in $X$ has a bound in $X$.›

definition "directed_complete ≡ (λX r. directed X r ∧ X ≠ {})-complete"

lemma monotone_directed_complete:
  assumes comp: "directed_complete A r"
  assumes fI: "f ` I ⊆ A" and dir: "directed I ri" and I0: "I ≠ {}" and mono: "monotone_on I ri r f"
  shows "∃s. extreme_bound A r (f ` I) s"
  apply (rule completeD[OF comp[unfolded directed_complete_def], OF fI])
  using monotone_directed_image[OF mono dir] I0 by auto

lemma (in reflexive) dual_closure_is_directed_complete:
  assumes comp: "directed-complete A (⊑)" and bA: "b ∈ A"
  shows "directed-complete {X ∈ A. b ⊑ X} (⊑)"
  apply (rule closure_is_complete[OF comp bA])
proof (intro allI impI directedI CollectI)
  interpret less_eq_dualize.
  fix X x y assume Xdir: "directed X (⊑)" and X: "X ⊆ A"
    and bX: "bound X (⊒) b" and x: "x ∈ X ∪ {b}" and y: "y ∈ X ∪ {b}"
  from x y X bA have xA: "x ∈ A" and yA: "y ∈ A" by auto
  show "∃z∈X ∪ {b}. x ⊑ z ∧ y ⊑ z"
  proof (cases "x = b")
    case [simp]: True
    with y bX bA have "b ⊑ y" by auto
    with y yA bA show ?thesis by (auto intro!: bexI[of _ y])
  next
    case False
    with x have x: "x ∈ X" by auto
    show ?thesis
    proof (cases "y = b")
      case [simp]: True
      with x bX have "b ⊑ x" by auto
      with x xA bA show ?thesis by (auto intro!: bexI[of _ x])
    next
      case False
      with y have y: "y ∈ X" by auto
      from directedD[OF Xdir x y] show ?thesis by simp
    qed
  qed
qed


text ‹The next one is quite complete, only the empty set may fail to have a supremum.
The terminology follows \cite{Bergman2015},
although there it is defined more generally depending on a cardinal $\alpha$
such that a nonempty set $X$ of cardinality below $\alpha$ has a supremum.›

abbreviation "semicomplete ≡ (λX r. X ≠ {})-complete"

lemma semicomplete_nonempty_imp_extremed:
  "semicomplete A r ⟹ A ≠ {} ⟹ extremed A r"
  unfolding extremed_iff_UNIV_complete
  using complete_cmono[of "λX r. X = A" "λX r. X ≠ {}"]
  by auto

lemma connex_dual_semicomplete: "semicomplete {C. connex C r} (⊇)"
proof (intro completeI)
  fix X
  assume "X ⊆ {C. connex C r}" and "X ≠ {}"
  then have "connex (⋂X) r" by (auto simp: connex_def)
  then have "extreme_bound {C. connex C r} (⊇) X (⋂ X)" by auto
  then show "∃S. extreme_bound {C. connex C r} (⊇) X S" by auto
qed

subsection ‹Pointed Ones›

text ‹The term `pointed' refers to the dual notion of toppedness, i.e., there is a global least element.
  This serves as the supremum of the empty set.›

lemma complete_sup: "(CC ⊔ CC')-complete A r ⟷ CC-complete A r ∧ CC'-complete A r"
  by (auto simp: complete_def)

lemma pointed_directed_complete:
  "directed-complete A r ⟷ directed_complete A r ∧ extremed A r⇧-"
proof-
  have [simp]: "(λX r. directed X r ∧ X ≠ {} ∨ X = {}) = directed" by auto
  show ?thesis
    by (auto simp: directed_complete_def pointed_iff_empty_complete complete_sup[symmetric]
        sup_fun_def)
qed

text ‹``Bounded complete'' refers to pointed conditional complete,
but this notion is just the dual of semicompleteness. We prove this later.›

abbreviation "bounded_complete A ≡ (λX r. ∃b∈A. bound X r b)-complete A"

subsection ‹Relations between Completeness Conditions›

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

interpretation less_eq_dualize.

text ‹Pair-completeness implies that the universe is directed. Thus, with directed completeness
implies toppedness.›

proposition directed_complete_pair_complete_imp_extremed:
  assumes dc: "directed_complete A (⊑)" and pc: "pair_complete A (⊑)" and A: "A ≠ {}"
  shows "extremed A (⊑)"
proof-
  have "∃s. extreme_bound A (⊑) A s"
    apply (rule completeD[OF dc[unfolded directed_complete_def]])
    using pair_complete_imp_directed[OF pc] A by auto
  then obtain t where "extreme_bound A (⊑) A t" by auto
  then have "∀x ∈ A. x ⊑ t" and "t ∈ A" by auto
  then show ?thesis by (auto simp: extremed_def)
qed

text ‹Semicomplete is conditional complete and topped.›

proposition semicomplete_iff_conditionally_complete_extremed:
  assumes A: "A ≠ {}"
  shows "semicomplete A (⊑) ⟷ conditionally_complete A (⊑) ∧ extremed A (⊑)" (is "?l ⟷ ?r")
proof (intro iffI)
  assume r: "?r"
  then have cc: "conditionally_complete A (⊑)" and e: "extremed A (⊑)" by auto
  show ?l
  proof (intro completeI)
    fix X
    assume X: "X ⊆ A" and "X ≠ {}"
    with extremed_imp_ex_bound[OF e X]
    show "∃s. extreme_bound A (⊑) X s" by (auto intro!: completeD[OF cc X])
  qed
next
  assume l: ?l
  with semicomplete_nonempty_imp_extremed[OF l] A
  show ?r by (auto intro!: completeI dest: completeD)
qed

proposition complete_iff_pointed_semicomplete:
  "⊤-complete A (⊑) ⟷ semicomplete A (⊑) ∧ extremed A (⊒)" (is "?l ⟷ ?r")
  by (unfold pointed_iff_empty_complete complete_sup[symmetric], auto simp: sup_fun_def top_fun_def)

text ‹Conditional completeness only lacks top and bottom to be complete.›

proposition complete_iff_conditionally_complete_extremed_pointed:
  "⊤-complete A (⊑) ⟷ conditionally_complete A (⊑) ∧ extremed A (⊑) ∧ extremed A (⊒)"
  unfolding complete_iff_pointed_semicomplete
  apply (cases "A = {}")
   apply (auto intro!: completeI dest: extremed_imp_ex_bound)[1]
  unfolding semicomplete_iff_conditionally_complete_extremed
  apply (auto intro:completeI)
  done


text ‹If the universe is directed, then every pair is bounded, and thus has a supremum.
  On the other hand, supremum gives an upper bound, witnessing directedness.›

proposition conditionally_complete_imp_pair_complete_iff_directed:
  assumes comp: "conditionally_complete A (⊑)"
  shows "pair_complete A (⊑) ⟷ directed A (⊑)" (is "?l ⟷ ?r")
proof(intro iffI)
  assume ?r
  then show ?l
    by (auto intro!: pair_completeI completeD[OF comp] elim: directedE)
next
  assume pc: ?l
  show ?r
  proof (intro directedI)
    fix x y assume "x ∈ A" and "y ∈ A"
    with pc obtain z where "extreme_bound A (⊑) {x,y} z" by (auto dest: pair_completeD)
    then show "∃z∈A. x ⊑ z ∧ y ⊑ z" by auto
  qed
qed

end

subsection ‹Duality of Completeness Conditions›

text ‹Conditional completeness is symmetric.›

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

interpretation less_eq_dualize.

lemma conditionally_complete_dual:
  assumes comp: "conditionally_complete A (⊑)" shows "conditionally_complete A (⊒)"
proof (intro completeI)
  fix X assume XA: "X ⊆ A"
  define B where [simp]: "B ≡ {b∈A. bound X (⊒) b}"
  assume bound: "∃b∈A. bound X (⊒) b ∧ X ≠ {}"
  with in_mono[OF XA] have B: "B ⊆ A" and "∃b ∈ A. bound B (⊑) b" and "B ≠ {}" by auto
  from comp[THEN completeD, OF B] this
  obtain s where "s ∈ A" and "extreme_bound A (⊑) B s" by auto
  with in_mono[OF XA] show "∃s. extreme_bound A (⊒) X s"
    by (intro exI[of _ s] extreme_boundI, auto)
qed

text ‹Full completeness is symmetric.›

lemma complete_dual:
  "⊤-complete A (⊑) ⟹ ⊤-complete A (⊒)"
  apply (unfold complete_iff_conditionally_complete_extremed_pointed)
  using conditionally_complete_dual by auto

text ‹Now we show that bounded completeness is the dual of semicompleteness.›

lemma bounded_complete_iff_pointed_conditionally_complete:
  assumes A: "A ≠ {}"
  shows "bounded_complete A (⊑) ⟷ conditionally_complete A (⊑) ∧ extremed A (⊒)"
  apply (unfold pointed_iff_empty_complete)
  apply (fold complete_sup)
  apply (unfold sup_fun_def)
  apply (rule arg_cong[of _ _ "λCC. CC-complete A (⊑)"])
  using A by auto

proposition bounded_complete_iff_dual_semicomplete:
  "bounded_complete A (⊑) ⟷ semicomplete A (⊒)"
proof (cases "A = {}")
  case True
  then show ?thesis by auto
next
  case False
  then show ?thesis
    apply (unfold bounded_complete_iff_pointed_conditionally_complete[OF False])
    apply (unfold semicomplete_iff_conditionally_complete_extremed)
    using Complete_Relations.conditionally_complete_dual by auto
qed

lemma bounded_complete_imp_conditionally_complete:
  assumes "bounded_complete A (⊑)" shows "conditionally_complete A (⊑)"
  using assms by (cases "A = {}", auto simp:bounded_complete_iff_pointed_conditionally_complete)

text ‹Completeness in downward-closure:›
lemma conditionally_complete_imp_semicomplete_in_dual_closure:
  assumes A: "conditionally_complete A (⊑)" and bA: "b ∈ A"
  shows "semicomplete {a ∈ A. a ⊑ b} (⊑)"
proof (intro completeI)
  fix X assume X: "X ⊆ {a ∈ A. a ⊑ b}" and X0: "X ≠ {}"
  then have "X ⊆ A" and Xb: "bound X (⊑) b" by auto
  with bA completeD[OF A] X0 obtain s where Xs: "extreme_bound A (⊑) X s" by auto
  with Xb bA have sb: "s ⊑ b" by auto
  with Xs have "extreme_bound {a ∈ A. a ⊑ b} (⊑) X s"
    by (intro extreme_boundI, auto)
  then show "∃s. extreme_bound {a ∈ A. a ⊑ b} (⊑) X s" by auto
qed

end

text ‹Completeness in intervals:›
lemma conditionally_complete_imp_complete_in_interval:
  fixes less_eq (infix "⊑" 50)
  assumes comp: "conditionally_complete A (⊑)" and aA: "a ∈ A" and bA: "b ∈ A"
    and aa: "a ⊑ a" and ab: "a ⊑ b"
  shows "⊤-complete {x ∈ A. a ⊑ x ∧ x ⊑ b} (⊑)"
proof (intro completeI)
  fix X assume X: "X ⊆ {x ∈ A. a ⊑ x ∧ x ⊑ b}"
  note conditionally_complete_imp_semicomplete_in_dual_closure[OF comp bA]
  from closure_is_complete[OF this, of a,simplified] aA ab
  have semi: "semicomplete {x ∈ A. a ⊑ x ∧ x ⊑ b} (⊑)" by (simp add: conj_commute cong: Collect_cong)
  show "Ex (extreme_bound {x ∈ A. a ⊑ x ∧ x ⊑ b} (⊑) X)"
  proof (cases "X = {}")
    case True
    with aA aa ab have "extreme_bound {x ∈ A. a ⊑ x ∧ x ⊑ b} (⊑) X a" by (auto simp: bound_empty)
    then show ?thesis by auto
  next
    case False
    with completeD[OF semi X] show ?thesis by simp
  qed
qed

lemmas connex_bounded_complete = connex_dual_semicomplete[folded bounded_complete_iff_dual_semicomplete]

subsection ‹Completeness Results Requiring Order-Like Properties›

text ‹Above results hold without any assumption on the relation.
This part demands some order-like properties.›

text ‹It is well known that in a semilattice, i.e., a pair-complete partial order,
every finite nonempty subset of elements has a supremum.
We prove the result assuming transitivity, but only that.›

lemma (in transitive) pair_complete_iff_finite_complete:
  "pair_complete A (⊑) ⟷ finite_complete A (⊑)" (is "?l ⟷ ?r")
proof (intro iffI completeI, elim CollectE conjE)
  fix X
  assume pc: ?l
  show "finite X ⟹ X ⊆ A ⟹ X ≠ {} ⟹ Ex (extreme_bound A (⊑) X)"
  proof (induct X rule: finite_induct)
  case empty
    then show ?case by auto
  next
    case (insert x X)
    then have x: "x ∈ A" and X: "X ⊆ A" by auto
    show ?case
    proof (cases "X = {}")
      case True
      obtain x' where "extreme_bound A (⊑) {x,x} x'" using pc[THEN pair_completeD, OF x x] by auto
      with True show ?thesis by (auto intro!: exI[of _ x'])
    next
      case False
      with insert obtain b where b: "extreme_bound A (⊑) X b" by auto
      with pc[THEN pair_completeD] x obtain c where c: "extreme_bound A (⊑) {x,b} c" by auto
      from c have cA: "c ∈ A" and xc: "x ⊑ c" and bc: "b ⊑ c" by auto
      from b have bA: "b ∈ A" and bX: "bound X (⊑) b" by auto
      show ?thesis
      proof (intro exI extreme_boundI)
        fix xb assume xb: "xb ∈ insert x X"
        from bound_trans[OF bX bc X bA cA] have "bound X (⊑) c".
        with xb xc show "xb ⊑ c" by auto
      next
        fix d assume "bound (insert x X) (⊑) d" and dA: "d ∈ A"
        with b have "bound {x,b} (⊑) d" by auto
        with c show "c ⊑ d" using dA by auto
      qed (fact cA)
    qed
  qed
qed (insert finite_complete_le_pair_complete, auto)


text ‹Gierz et al.~\cite{gierz03} showed that a directed complete partial order is semicomplete
if and only if it is also a semilattice.
We generalize the claim so that the underlying relation is only transitive.›

proposition(in transitive) semicomplete_iff_directed_complete_pair_complete:
  "semicomplete A (⊑) ⟷ directed_complete A (⊑) ∧ pair_complete A (⊑)" (is "?l ⟷ ?r")
proof (intro iffI)
  assume l: ?l
  then show ?r by (auto simp: directed_complete_def intro!: completeI pair_completeI completeD[OF l])
next
  assume ?r
  then have dc: "directed_complete A (⊑)" and pc: "pair_complete A (⊑)" by auto
  with pair_complete_iff_finite_complete have fc: "finite_complete A (⊑)" by auto
  show ?l
  proof (intro completeI)
    fix X assume XA: "X ⊆ A"
    have 1: "directed {x. ∃Y ⊆ X. finite Y ∧ Y ≠ {} ∧ extreme_bound A (⊑) Y x} (⊑)" (is "directed ?B _")
    proof (intro directedI)
      fix a b assume a: "a ∈ ?B" and b: "b ∈ ?B"
      from a obtain Y where Y: "extreme_bound A (⊑) Y a" "finite Y" "Y ≠ {}" "Y ⊆ X" by auto
      from b obtain B where B: "extreme_bound A (⊑) B b" "finite B" "B ≠ {}" "B ⊆ X" by auto
      from XA Y B have AB: "Y ⊆ A" "B ⊆ A" "finite (Y ∪ B)" "Y ∪ B ≠ {}" "Y ∪ B ⊆ X" by auto
      with fc[THEN completeD] have "Ex (extreme_bound A (⊑) (Y ∪ B))" by auto
      then obtain c where c: "extreme_bound A (⊑) (Y ∪ B) c" by auto
      show "∃c ∈ ?B. a ⊑ c ∧ b ⊑ c"
      proof (intro bexI conjI)
        from Y B c show "a ⊑ c" and "b ⊑ c" by (auto simp: extreme_bound_iff)
        from AB c show "c ∈ ?B" by (auto intro!: exI[of _ "Y ∪ B"])
      qed
    qed
    have B: "?B ⊆ A" by auto
    assume "X ≠ {}"
    then obtain x where xX: "x ∈ X" by auto
    with fc[THEN completeD, of "{x}"] XA
    obtain x' where "extreme_bound A (⊑) {x} x'" by auto
    with xX have x'B: "x' ∈ ?B" by (auto intro!: exI[of _ "{x}"] extreme_boundI)
    then have 2: "?B ≠ {}" by auto
    from dc[unfolded directed_complete_def, THEN completeD, of ?B] 1 2
    obtain b where b: "extreme_bound A (⊑) ?B b" by auto
    then have bA: "b ∈ A" by auto
    show "Ex (extreme_bound A (⊑) X)"
    proof (intro exI extreme_boundI UNIV_I)
      fix x
      assume xX: "x ∈ X"
      with XA fc[THEN completeD, of "{x}"]
      obtain c where c: "extreme_bound A (⊑) {x} c" by auto
      then have cA: "c ∈ A" and xc: "x ⊑ c" by auto
      from c xX have cB: "c ∈ ?B" by (auto intro!: exI[of _ "{x}"] extreme_boundI)
      with b have bA: "b ∈ A" and cb: "c ⊑ b" by auto
      from xX XA cA bA trans[OF xc cb]
      show "x ⊑ b" by auto text‹ Here transitivity is needed. ›
    next
      fix x
      assume xA: "x ∈ A" and Xx: "bound X (⊑) x"
      have "bound ?B (⊑) x"
      proof (intro boundI UNIV_I, clarify)
        fix c Y
        assume "finite Y" and YX: "Y ⊆ X" and "Y ≠ {}" and c: "extreme_bound A (⊑) Y c"
        from YX Xx have "bound Y (⊑) x" by auto
        with c xA show "c ⊑ x" by auto
      qed
      with b xA show "b ⊑ x" by auto
    qed (fact bA)
  qed
qed

text‹The last argument in the above proof requires transitivity,
but if we had reflexivity then $x$ itself is a supremum of $\set{x}$
(see @{thm reflexive.extreme_bound_singleton}) and so $x \SLE s$ would be immediate.
Thus we can replace transitivity by reflexivity,
but then pair-completeness does not imply finite completeness.
We obtain the following result.›

proposition (in reflexive) semicomplete_iff_directed_complete_finite_complete:
  "semicomplete A (⊑) ⟷ directed_complete A (⊑) ∧ finite_complete A (⊑)" (is "?l ⟷ ?r")
proof (intro iffI)
  assume l: ?l
  then show ?r by (auto simp: directed_complete_def intro!: completeI pair_completeI completeD[OF l])
next
  assume ?r
  then have dc: "directed_complete A (⊑)" and fc: "finite_complete A (⊑)" by auto
  show ?l
  proof (intro completeI)
    fix X assume XA: "X ⊆ A"
    have 1: "directed {x. ∃Y ⊆ X. finite Y ∧ Y ≠ {} ∧ extreme_bound A (⊑) Y x} (⊑)" (is "directed ?B _")
    proof (intro directedI)
      fix a b assume a: "a ∈ ?B" and b: "b ∈ ?B"
      from a obtain Y where Y: "extreme_bound A (⊑) Y a" "finite Y" "Y ≠ {}" "Y ⊆ X" by auto
      from b obtain B where B: "extreme_bound A (⊑) B b" "finite B" "B ≠ {}" "B ⊆ X" by auto
      from XA Y B have AB: "Y ⊆ A" "B ⊆ A" "finite (Y ∪ B)" "Y ∪ B ≠ {}" "Y ∪ B ⊆ X" by auto
      with fc[THEN completeD] have "Ex (extreme_bound A (⊑) (Y ∪ B))" by auto
      then obtain c where c: "extreme_bound A (⊑) (Y ∪ B) c" by auto
      show "∃c ∈ ?B. a ⊑ c ∧ b ⊑ c"
      proof (intro bexI conjI)
        from Y B c show "a ⊑ c" and "b ⊑ c" by (auto simp: extreme_bound_iff)
        from AB c show "c ∈ ?B" by (auto intro!: exI[of _ "Y ∪ B"])
      qed
    qed
    have B: "?B ⊆ A" by auto
    assume "X ≠ {}"
    then obtain x where xX: "x ∈ X" by auto
    with XA have "extreme_bound A (⊑) {x} x"
      by (intro extreme_bound_singleton, auto)
    with xX have xB: "x ∈ ?B" by (auto intro!: exI[of _ "{x}"])
    then have 2: "?B ≠ {}" by auto
    from dc[unfolded directed_complete_def, THEN completeD, of ?B] B 1 2
    obtain b where b: "extreme_bound A (⊑) ?B b" by auto
    then have bA: "b ∈ A" by auto
    show "Ex (extreme_bound A (⊑) X)"
    proof (intro exI extreme_boundI UNIV_I)
      fix x
      assume xX: "x ∈ X"
      with XA have x: "extreme_bound A (⊑) {x} x" by (intro extreme_bound_singleton, auto)
      from x xX have cB: "x ∈ ?B" by (auto intro!: exI[of _ "{x}"])
      with b show "x ⊑ b" by auto
    next
      fix x
      assume Xx: "bound X (⊑) x" and xA: "x ∈ A"
      have "bound ?B (⊑) x"
      proof (intro boundI UNIV_I, clarify)
        fix c Y
        assume "finite Y" and YX: "Y ⊆ X" and "Y ≠ {}" and c: "extreme_bound A (⊑) Y c"
        from YX Xx have "bound Y (⊑) x" by auto
        with YX XA xA c show "c ⊑ x" by auto
      qed
      with xA b show "b ⊑ x" by auto
    qed (fact bA)
  qed
qed


subsection ‹Relating to Classes›

(* HOL.Conditionally_Complete_Lattices imports choice.

text ‹Isabelle's class @{class conditionally_complete_lattice} satisfies @{const conditionally_complete}.
The other direction does not hold, since for the former,
@{term "Sup {}"} and @{term "Inf {}"} are arbitrary even if there are top or bottom elements.›

lemma (in conditionally_complete_lattice) "conditionally_complete UNIV (≤)"
proof (intro completeI, elim CollectE)
  fix X :: "'a set"
  assume "∃b∈UNIV. bound X (≤) b ∧ X ≠ {}"
  then have bdd:"bdd_above X" and X0: "X ≠ {}" by (auto 0 3)
  from cSup_upper[OF _ bdd] cSup_least[OF X0]
  have "supremum X (Sup X)" by (intro extremeI boundI, auto)
  then show "∃s. least {b ∈ UNIV. bound X (≤) b} s" by auto
qed
*)
text ‹Isabelle's class @{class complete_lattice} is @{term "⊤-complete"}.›

lemma (in complete_lattice) "⊤-complete UNIV (≤)"
  by (auto intro!: completeI extreme_boundI Sup_upper Sup_least Inf_lower Inf_greatest)

subsection ‹Set-wise Completeness›

lemma Pow_extreme_bound: "X ⊆ Pow A ⟹ extreme_bound (Pow A) (⊆) X (⋃X)"
  by (intro extreme_boundI, auto 2 3)

lemma Pow_complete: "𝒞-complete (Pow A) (⊆)"
  by (auto intro!: completeI dest: Pow_extreme_bound)

lemma directed_directed_Un:
assumes ch: "XX ⊆ {X. directed X r}" and dir: "directed XX (⊆)"
    shows "directed (⋃XX) r"
proof (intro directedI, elim UnionE)
  fix x y X Y assume xX: "x ∈ X" and X: "X ∈ XX" and yY: "y ∈ Y" and Y: "Y ∈ XX"
  from directedD[OF dir X Y]
  obtain Z where "X ⊆ Z" "Y ⊆ Z" and Z: "Z ∈ XX" by auto
  with ch xX yY have "directed Z r" "x ∈ Z" "y ∈ Z" by auto
  then obtain z where "z ∈ Z" "r x z ∧ r y z" by (auto elim:directedE)
  with Z show "∃z∈⋃ XX. r x z ∧ r y z" by auto
qed

lemmas directed_connex_Un = directed_directed_Un[OF _ connex.directed]

lemma directed_sets_directed_complete:
  assumes cl: "∀DC. DC ⊆ AA ⟶ (∀X∈DC. directed X r) ⟶ (⋃DC) ∈ AA"
  shows "directed-complete {X ∈ AA. directed X r} (⊆)"
proof (intro completeI)
  fix XX
  assume ch: "XX ⊆ {X ∈ AA. directed X r}" and dir: "directed XX (⊆)"
  with cl have "(⋃XX) ∈ AA" by auto
  moreover have "directed (⋃XX) r"
    apply (rule directed_directed_Un) using ch by (auto simp: dir)
  ultimately show "Ex (extreme_bound {X ∈ AA. directed X r} (⊆) XX)"
    by (auto intro!: exI[of _ "⋃XX"])
qed

lemma connex_directed_Un:
  assumes ch: "CC ⊆ {C. connex C r}" and dir: "directed CC (⊆)"
  shows "connex (⋃CC) r"
proof (intro connexI, elim UnionE)
  fix x y X Y assume xX: "x ∈ X" and X: "X ∈ CC" and yY: "y ∈ Y" and Y: "Y ∈ CC"
  from directedD[OF dir X Y]
  obtain Z where "X ⊆ Z" "Y ⊆ Z" "Z ∈ CC" by auto
  with xX yY ch have "x ∈ Z" "y ∈ Z" "connex Z r" by auto
  then show "r x y ∨ r y x" by (auto elim:connexE)
qed

lemma connex_is_directed_complete: "directed-complete {C. C ⊆ A ∧ connex C r} (⊆)"
proof (intro completeI)
  fix CC assume CC: "CC ⊆ {C. C ⊆ A ∧ connex C r}" and "directed CC (⊆)"
  with connex_directed_Un have Scon: "connex (⋃CC) r" by auto
  from CC have SA: "⋃CC ⊆ A" by auto
  from Scon SA show "∃S. extreme_bound {C. C ⊆ A ∧ connex C r} (⊆) CC S"
    by (auto intro!: exI[of _ "⋃CC"] extreme_boundI)
qed

lemma (in well_ordered_set) well_ordered_set_insert:
  assumes aA: "total_ordered_set (insert a A) (⊑)"
  shows "well_ordered_set (insert a A) (⊑)"
proof-
  interpret less_eq_asymmetrize.
  interpret aA: total_ordered_set "insert a A" "(⊑)" using aA.
  show ?thesis
  proof (intro well_ordered_set.intro aA.antisymmetric_axioms well_related_setI)
    fix X assume XaA: "X ⊆ insert a A" and X0: "X ≠ {}"
    show "∃e. extreme X (⊒) e"
    proof (cases "a ∈ X")
      case False
      with XaA have "X ⊆ A" by auto
      from nonempty_imp_ex_extreme[OF this X0] show ?thesis.
    next
      case aX: True
      show ?thesis
      proof (cases "X - {a} = {}")
        case True
        with aX XaA have Xa: "X = {a}" by auto
        from aA.refl[of a]
        have "a ⊑ a" by auto
        then show ?thesis by (auto simp: Xa)
      next
        case False
        from nonempty_imp_ex_extreme[OF _ False] XaA
        obtain e where Xae: "extreme (X-{a}) (⊒) e" by auto
        with Xae XaA have eaA: "e ∈ insert a A" by auto
        then have "e ⊑ a ∨ a ⊑ e" by (intro aA.comparable, auto)
        then show ?thesis
        proof (elim disjE)
          assume ea: "e ⊑ a"
          with Xae show ?thesis by (auto intro!:exI[of _ e])
        next
          assume ae: "a ⊑ e"
          show ?thesis
          proof (intro exI[of _ a] extremeI aX)
            fix x assume xX: "x ∈ X"
            show "a ⊑ x"
            proof (cases "a = x")
              case True with aA.refl[of a] show ?thesis by auto
            next
              case False
              with xX have "x ∈ X - {a}" by auto
              with Xae have "e ⊑ x" by auto
              from aA.trans[OF ae this _ eaA] xX XaA
              show ?thesis by auto
            qed
          qed
        qed
      qed
    qed
  qed
qed

text ‹The following should be true in general, but here we use antisymmetry to avoid
  the axiom of choice.›

lemma (in antisymmetric) pointwise_connex_complete:
  assumes comp: "connex-complete A (⊑)"
  shows "connex-complete {f. f ` X ⊆ A} (pointwise X (⊑))"
proof (safe intro!: completeI exI)
  fix F
  assume FXA: "F ⊆ {f. f ` X ⊆ A}" and F: "connex F (pointwise X (⊑))"
  show "extreme_bound {f. f ` X ⊆ A} (pointwise X (⊑)) F (λx. The (extreme_bound A (⊑) {f x |. f ∈ F}))"
  proof (unfold pointwise_extreme_bound[OF FXA], safe)
    fix x assume xX: "x ∈ X"
    from FXA xX have FxA: "{f x |. f ∈ F} ⊆ A" by auto
    have "Ex (extreme_bound A (⊑) {f x |. f ∈ F})"
    proof (intro completeD[OF comp] FxA CollectI connexI, elim imageE, fold atomize_eq)
      fix f g assume fF: "f ∈ F" and gF: "g ∈ F"
      from connex.comparable[OF F this] xX show "f x ⊑ g x ∨ g x ⊑ f x" by auto
    qed
    also note ex_extreme_bound_iff_the
    finally
    show "extreme_bound A (⊑) {f x |. f ∈ F} (The (extreme_bound A (⊑) {f x |. f ∈ F}))".
  qed
qed

text ‹Our supremum/infimum coincides with those of Isabelle's @{class complete_lattice}.›

lemma complete_UNIV: "⊤-complete (UNIV::'a::complete_lattice set) (≤)"
proof-
  have "Ex (supremum X)" for X :: "'a set"
    by (auto intro!: exI[of _ "⨆X"] supremumI simp:Sup_upper Sup_least)
  then show ?thesis by (auto intro!: completeI )
qed

context
  fixes X :: "'a :: complete_lattice set"
begin

lemma supremum_Sup: "supremum X (⨆X)"
proof-
  define it where "it ≡ The (supremum X)"
  note completeD[OF complete_UNIV,simplified, of X]
  from this[unfolded order.dual.ex_extreme_iff_the]
  have 1: "supremum X it" by (simp add: it_def)
  then have "⨆X = it" by (intro Sup_eqI, auto)
  with 1 show ?thesis by auto
qed

lemmas Sup_eq_The_supremum = order.dual.eq_The_extreme[OF supremum_Sup]

lemma supremum_eq_Sup: "supremum X x ⟷ ⨆X = x"
  using order.dual.eq_The_extreme supremum_Sup by auto

lemma infimum_Inf:
  shows "infimum X (⨅X)"
proof-
  define it where "it ≡ The (infimum X)"
  note completeD[OF complete_dual[OF complete_UNIV],simplified, of X]
  from this[unfolded order.ex_extreme_iff_the]
  have 1: "infimum X it" by (simp add: it_def)
  then have "⨅X = it" by (intro Inf_eqI, auto)
  with 1 show ?thesis by auto
qed

lemmas Inf_eq_The_infimum = order.eq_The_extreme[OF infimum_Inf]

lemma infimum_eq_Inf: "infimum X x ⟷ ⨅X = x"
  using order.eq_The_extreme infimum_Inf by auto

end

end