Theory More_Lattices

(*<*)
theory More_Lattices
imports
  HOL_Basis
begin

(*>*)
section‹ More lattice\label{sec:more_lattices}  ›

lemma (in semilattice_sup) sup_iff_le:
  shows "x ⊔ y = y ⟷ x ≤ y"
    and "y ⊔ x = y ⟷ x ≤ y"
by (simp_all add: le_iff_sup ac_simps)

lemma (in semilattice_inf) inf_iff_le:
  shows "x ⊓ y = x ⟷ x ≤ y"
    and "y ⊓ x = x ⟷ x ≤ y"
by (simp_all add: le_iff_inf ac_simps)

lemma if_sup_distr:
  fixes t e :: "_::semilattice_sup"
  shows if_sup_distrL: "(if b then t⇩1 ⊔ t⇩2 else e) = (if b then t⇩1 else e) ⊔ (if b then t⇩2 else e)"
    and if_sup_distrR: "(if b then t else e⇩1 ⊔ e⇩2) = (if b then t else e⇩1) ⊔ (if b then t else e⇩2)"
by (simp_all split: if_splits)

lemma INF_bot:
  assumes "F i = (⊥::_::complete_lattice)"
  assumes "i ∈ X"
  shows "(⨅i∈X. F i) = ⊥"
using assms by (metis INF_lower bot.extremum_uniqueI)

lemma mcont_fun_app_const[cont_intro]:
  shows "mcont Sup (≤) Sup (≤) (λf. f c)"
by (fastforce intro!: mcontI monotoneI contI simp: le_fun_def)

declare mcont_applyI[cont_intro]

lemma INF_rename_bij:
  assumes "bij_betw π X Y"
  shows "(⨅y∈Y. F Y y) = (⨅x∈X. F (π ` X) (π x))"
using assms by (metis bij_betw_imp_surj_on image_image)

lemma Inf_rename_surj:
  assumes "surj π"
  shows "(⨅x. F x) = (⨅x. F (π x))"
using assms by (metis image_image)

lemma INF_unwind_index:
  fixes A :: "_⇒_:: complete_lattice"
  assumes "i ∈ I"
  shows "(⨅x∈I. A x) = A i ⊓ (⨅x∈I - {i}. A x)"
by (metis INF_insert assms insert_Diff)

lemma Sup_fst:
  shows "(⨆x∈X. P (fst x)) = (⨆x∈fst ` X. P x)"
by (simp add: image_image)

setup ‹Sign.mandatory_path "order"›

lemma assms_cong: ―‹ simplify assumptions only ›
  assumes "x = x'"
  shows "x ≤ y ⟷ x' ≤ y"
using assms by simp

lemma concl_cong: ―‹ simplify conclusions only ›
  assumes "y = y'"
  shows "x ≤ y ⟷ x ≤ y'"
using assms by simp

lemma "subgoal": ―‹ cut for lattice logics ›
  fixes P :: "_::semilattice_inf"
  assumes "P ≤ Q"
  assumes "P ⊓ Q ≤ R"
  shows "P ≤ R"
using assms by (simp add: inf_absorb1)

setup ‹Sign.parent_path›

paragraph‹ Logical rules ala HOL ›

lemmas SupI = Sup_upper
lemmas rev_SUPI = SUP_upper2[of x A b f for x A b f]
lemmas SUPI = rev_SUPI[rotated]

lemmas SUPE = SUP_least[where u=z for z]
lemmas SupE = Sup_least

lemmas INFI = INF_greatest
lemmas InfI = Inf_greatest
lemmas infI = semilattice_inf_class.le_infI

lemma InfE:
  fixes R::"_::complete_lattice"
  assumes "P x ≤ R"
  shows "(⨅x. P x) ≤ R"
using assms by (meson Inf_lower2 rangeI)

lemma INFE:
  fixes R::"'a::complete_lattice"
  assumes "P x ≤ R"
  assumes "x ∈ A"
  shows "⨅(P ` A) ≤ R"
using assms by (metis INF_lower2)

lemmas rev_INFE = INFE[rotated]

lemma Inf_inf_distrib:
  fixes P::"_::complete_lattice"
  shows "(⨅x. P x ⊓ Q x) = (⨅x. P x) ⊓ (⨅x. Q x)"
by (simp add: INF_inf_distrib)

lemma Sup_sup_distrib:
  fixes P::"_::complete_lattice"
  shows "(⨆x. P x ⊔ Q x) = (⨆x. P x) ⊔ (⨆x. Q x)"
by (simp add: SUP_sup_distrib)

lemma Inf_inf:
  fixes Q :: "_::complete_lattice"
  shows "(⨅x. P x ⊓ Q) = (⨅x. P x) ⊓ Q"
by (simp add: INF_inf_const2)

lemma inf_Inf:
  fixes P :: "_::complete_lattice"
  shows "(⨅x. P ⊓ Q x) = P ⊓ (⨅x. Q x)"
by (simp add: INF_inf_const1)

lemma SUP_sup:
  fixes Q :: "_::complete_lattice"
  assumes "X ≠ {}"
  shows "(⨆x∈X. P x ⊔ Q) = (⨆x∈X. P x) ⊔ Q" (is "?lhs = ?rhs")
proof(rule antisym)
  show "?lhs ≤ ?rhs" by (simp add: SUP_le_iff SupI le_supI1)
  from assms show "?rhs ≤ ?lhs" by (auto simp add: SUP_le_iff intro: SUPI le_supI1)
qed

lemma sup_SUP:
  fixes P :: "_::complete_lattice"
  assumes "X ≠ {}"
  shows "(⨆x∈X. P ⊔ Q x) = P ⊔ (⨆x∈X. Q x)"
using SUP_sup[OF assms, where P=Q and Q=P] by (simp add: ac_simps)


subsection‹ Boolean lattices and implication\label{sec:more_lattices-boolean_implication} ›

lemma
  shows minus_Not[simp]: "- Not = id"
    and minus_id[simp]: "- id = Not"
by fastforce+

definition boolean_implication :: "'a::boolean_algebra ⇒ 'a ⇒ 'a" (infixr "❙⟶⇩B" 60) where
  "x ❙⟶⇩B y = -x ⊔ y"

definition boolean_eq :: "'a::boolean_algebra ⇒ 'a ⇒ 'a" (infixr "❙⟷⇩B" 60) where
  "x ❙⟷⇩B y = x ❙⟶⇩B y ⊓ y ❙⟶⇩B x"

setup ‹Sign.mandatory_path "boolean_implication"›

lemma bool_alt_def[simp]:
  shows "P ❙⟶⇩B Q = (P ⟶ Q)"
by (auto simp: boolean_implication_def)

lemma pred__alt_def[simp]:
  shows "(P ❙⟶⇩B Q) x = (P x ❙⟶⇩B Q x)"
by (auto simp: boolean_implication_def)

lemma set_alt_def:
  shows "P ❙⟶⇩B Q = {x. x ∈ P ⟶ x ∈ Q}"
by (auto simp: boolean_implication_def)

lemma member:
  shows "x ∈ P ❙⟶⇩B Q ⟷ x ∈ P ⟶ x ∈ Q"
by (simp add: boolean_implication.set_alt_def)

lemmas setI = iffD2[OF boolean_implication.member, rule_format]

lemma simps[simp]:
  shows
    "⊤ ❙⟶⇩B P = P"
    "⊥ ❙⟶⇩B P = ⊤"
    "P ❙⟶⇩B ⊤ = ⊤"
    "P ❙⟶⇩B P = ⊤"
    "P ❙⟶⇩B ⊥ = -P"
    "P ❙⟶⇩B -P = -P"
by (simp_all add: boolean_implication_def shunt1)

lemma Inf_simps[simp]: ―‹Miniscoping: pushing in universal quantifiers.›
  shows
    "⋀P (Q::_::complete_boolean_algebra).    (⨅x. P x ❙⟶⇩B Q) = ((⨆x. P x) ❙⟶⇩B Q)"
    "⋀P (Q::_::complete_boolean_algebra).    (⨅x∈X. P x ❙⟶⇩B Q) = ((⨆x∈X. P x) ❙⟶⇩B Q)"
    "⋀P (Q::_⇒_::complete_boolean_algebra). (⨅x. P ❙⟶⇩B Q x) = (P ❙⟶⇩B (⨅x. Q x))"
    "⋀P (Q::_⇒_::complete_boolean_algebra). (⨅x∈X. P ❙⟶⇩B Q x) = (P ❙⟶⇩B (⨅x∈X. Q x))"
by (simp_all add: boolean_implication_def INF_sup sup_INF uminus_SUP)

lemma mono:
  assumes "x' ≤ x"
  assumes "y ≤ y'"
  shows "x ❙⟶⇩B y ≤ x' ❙⟶⇩B y'"
using assms by (simp add: boolean_implication_def sup.coboundedI1 sup.coboundedI2)

lemma strengthen[strg]:
  assumes "st_ord (¬ F) X X'"
  assumes "st_ord F Y Y'"
  shows "st_ord F (X ❙⟶⇩B Y) (X' ❙⟶⇩B Y')"
using assms by (cases F) (use boolean_implication.mono in auto)

lemma eq_conv:
  shows "(P = Q) ⟷ (P ❙⟶⇩B Q) ⊓ (Q ❙⟶⇩B P) = ⊤"
unfolding boolean_implication_def order.eq_iff by (simp add: sup_shunt top.extremum_unique)

lemma uminus_imp[simp]:
  shows "-(P ❙⟶⇩B Q) = P ⊓ -Q"
by (simp add: boolean_implication_def)

lemma cases_simp[simp]:
  shows "(P ❙⟶⇩B Q) ⊓ (-P ❙⟶⇩B Q) = Q"
by (simp add: boolean_implication_def order.eq_iff boolean_algebra.disj_conj_distrib2 shunt1)

lemma conv_sup:
  shows "(P ❙⟶⇩B Q) = -P ⊔ Q"
by (rule boolean_implication_def)

lemma infL:
  shows "P ⊓ Q ❙⟶⇩B R = P ❙⟶⇩B Q ❙⟶⇩B R"
by (simp add: boolean_implication_def sup_assoc)

lemmas uncurry = boolean_implication.infL[symmetric]

lemma shunt1:
  shows "x ⊓ y ≤ z ⟷ x ≤ y ❙⟶⇩B z"
by (simp add: boolean_implication_def shunt1)

lemma shunt2:
  shows "x ⊓ y ≤ z ⟷ y ≤ x ❙⟶⇩B z"
by (subst inf.commute) (rule boolean_implication.shunt1)

lemma mp:
  assumes "x ⊓ y ≤ z"
  shows "x ≤ y ❙⟶⇩B z"
using assms by (simp add: boolean_implication.shunt1)

lemma imp_trivialI:
  assumes "P ⊓ -R ≤ -Q"
  shows "P ≤ Q ❙⟶⇩B R"
using assms by (simp add: boolean_implication_def shunt2 sup.commute)

lemma shunt_top:
  shows "P ❙⟶⇩B Q = ⊤ ⟷ P ≤ Q"
by (simp add: boolean_implication_def sup_shunt)

lemma detachment:
  shows "x ⊓ (x ❙⟶⇩B y) = x ⊓ y" (is ?thesis1)
    and "(x ❙⟶⇩B y) ⊓ x = x ⊓ y" (is ?thesis2)
proof -
  show ?thesis1 by (simp add: boolean_algebra.conj_disj_distrib boolean_implication_def)
  then show ?thesis2 by (simp add: ac_simps)
qed

lemma discharge:
  assumes "x' ≤ x"
  shows "x' ⊓ (x ❙⟶⇩B y) = x' ⊓ y" (is ?thesis1)
    and "(x ❙⟶⇩B y) ⊓ x' = y ⊓ x'" (is ?thesis2)
proof -
  from assms show ?thesis1
    by (simp add: boolean_implication_def inf_sup_distrib sup.absorb2 le_supI1 flip: sup_neg_inf)
  then show ?thesis2
    by (simp add: ac_simps)
qed

lemma trans:
  shows "(x ❙⟶⇩B y) ⊓ (y ❙⟶⇩B z) ≤ (x ❙⟶⇩B z)"
by (simp add: boolean_implication_def inf_sup_distrib le_supI1 le_supI2)

setup ‹Sign.parent_path›


subsection‹ Compactness and algebraicity\label{sec:more_lattices-concepts} ›

text‹

Fundamental lattice concepts drawn from \<^citet>‹"DaveyPriestley:2002"›.

›

context complete_lattice
begin

definition compact_points :: "'a set" where ―‹ \<^citet>‹‹Definition~7.15(ii)› in "DaveyPriestley:2002"› ›
  "compact_points = {x. ∀S. x ≤ ⨆S ⟶ (∃T⊆S. finite T ∧ x ≤ ⨆T)}"

lemmas compact_pointsI = subsetD[OF equalityD2[OF compact_points_def], simplified, rule_format]
lemmas compact_pointsD = subsetD[OF equalityD1[OF compact_points_def], simplified, rule_format]

lemma compact_point_bot:
  shows "⊥ ∈ compact_points"
by (rule compact_pointsI) auto

lemma compact_points_sup: ―‹ \<^citet>‹‹Lemma~7.16› in "DaveyPriestley:2002"› ›
  assumes "x ∈ compact_points"
  assumes "y ∈ compact_points"
  shows "x ⊔ y ∈ compact_points"
proof(rule compact_pointsI)
  fix S assume "x ⊔ y ≤ ⨆S"
  with compact_pointsD[OF assms(1), of S] compact_pointsD[OF assms(2), of S]
  obtain X Y
    where "X ⊆ S ∧ finite X ∧ x ≤ ⨆X"
      and "Y ⊆ S ∧ finite Y ∧ y ≤ ⨆Y"
    by auto
  then show "∃T⊆S. finite T ∧ x ⊔ y ≤ ⨆ T"
    by (simp add: exI[where x="X ∪ Y"] Sup_union_distrib le_supI1 le_supI2)
qed

lemma compact_points_Sup: ―‹ \<^citet>‹‹Lemma~7.16› in "DaveyPriestley:2002"› ›
  assumes "X ⊆ compact_points"
  assumes "finite X"
  shows "⨆X ∈ compact_points"
using assms(2,1) by induct (simp_all add: compact_point_bot compact_points_sup)

lemma compact_points_are_ccpo_compact: ―‹ converse should hold ›
  assumes "x ∈ compact_points"
  shows "ccpo.compact Sup (≤) x"
proof(rule ccpo.compactI[OF complete_lattice_ccpo], rule ccpo.admissibleI, rule notI)
  fix X
  assume "Complete_Partial_Order.chain (≤) X" and "x ≤ ⨆X" and *: "X ≠ {}" "∀y∈X. ¬x ≤ y" 
  from compact_pointsD[OF assms ‹x ≤ ⨆X›]
  obtain T where "T ⊆ X" and "finite T" and "x ≤ ⨆T" by blast
  with * Complete_Partial_Order.chain_subset[OF ‹Complete_Partial_Order.chain (≤) X› ‹T ⊆ X›]
  show False
    by (auto simp: sup.absorb1 sup.absorb2 bot_unique dest: chainD dest!: finite_Sup_in)
qed

definition directed :: "'a set ⇒ bool" where ―‹ \<^citet>‹‹Definition~7.7› in "DaveyPriestley:2002"› ›
  "directed X ⟷ X ≠ {} ∧ (∀x∈X. ∀y∈X. ∃z∈X. x ≤ z ∧ y ≤ z)"

lemmas directedI = iffD2[OF directed_def, simplified conj_explode, rule_format]
lemmas directedD = iffD1[OF directed_def]

lemma directed_empty:
  assumes "directed X"
  shows "X ≠ {}"
using assms by (simp add: directed_def)

lemma chain_directed:
  assumes "Complete_Partial_Order.chain (≤) Y"
  assumes "Y ≠ {}"
  shows "directed Y"
using assms by (metis chainD directedI)

lemma directed_alt_def:
  shows "directed X ⟷ (∀Y⊆X. finite Y ⟶ (∃x∈X. ∀y∈Y. y ≤ x))" (is "?lhs ⟷ ?rhs")
proof(rule iffI)
  have "∃x∈X. ∀y∈Y. y ≤ x" if "finite Y" and "directed X" and "Y ⊆ X" and "Y ≠ {}"for Y
    using that by induct (force dest: directedD)+
  then show "?lhs ⟹ ?rhs" by (auto simp: directed_def)
next
  assume ?rhs show ?lhs
  proof(rule directedI)
    from ‹?rhs› show "X ≠ {}" by blast
    fix x y assume "x ∈ X" and "y ∈ X" with ‹?rhs› show "∃z∈X. x ≤ z ∧ y ≤ z"
      by (clarsimp dest!: spec[where x="{x, y}"])
  qed
qed

lemma compact_points_alt_def: ―‹ \<^citet>‹‹Definition~7.15(i) (finite points)› in "DaveyPriestley:2002"› ›
  shows "compact_points = {x::'a. ∀D. directed D ∧ x ≤ ⨆D ⟶ (∃d∈D. x ≤ d)}" (is "?lhs = ?rhs")
proof(rule antisym)
  show "?lhs ⊆ ?rhs"
    by (clarsimp simp: compact_points_def directed_alt_def) (metis Sup_least order.trans)
next
  have *: "⨆S = ⨆{⨆T |T. T ≠ {} ∧ T ⊆ S ∧ finite T}" for S :: "'a set" ―‹ \<^citet>‹‹Exercise~7.5› in "DaveyPriestley:2002"› ›
    by (fastforce intro: order.antisym Sup_subset_mono Sup_least exI[where x="{x}" for x])
  have **: "directed {⨆T |T. T ≠ {} ∧ T ⊆ S ∧ finite T}" (is "directed ?D") if "S ≠ {}" for S :: "'a set"
  proof(rule directedI)
    from ‹S ≠ {}› show "?D ≠ {}" by blast
    fix x y assume "x ∈ ?D" "y ∈ ?D"
    then obtain X Y
      where "x = ⨆X ∧ X ≠ {} ∧ X ⊆ S ∧ finite X"
        and "y = ⨆Y ∧ Y ≠ {} ∧ Y ⊆ S ∧ finite Y"
      by blast
    then show "∃z∈?D. x ≤ z ∧ y ≤ z"
      by - (rule bexI[where x="⨆(X ∪ Y)"]; auto simp: Sup_subset_mono)
  qed
  have "∃T⊆X. finite T ∧ x ≤ ⨆T" if "∀D. directed D ∧ x ≤ ⨆D ⟶ (∃d∈D. x ≤ d)" and "x ≤ ⨆X" for x X
    using that *[of X] **[of X] by force
  then show "?rhs ⊆ ?lhs"
    by (fastforce intro: compact_pointsI)
qed

lemmas compact_points_directedD
  = subsetD[OF equalityD1[OF compact_points_alt_def], simplified, rule_format, simplified conj_explode, rotated -1]

end

class algebraic_lattice = complete_lattice + ―‹ \<^citet>‹‹Definition~7.18› in "DaveyPriestley:2002"› ›
  assumes algebraic: "(x :: 'a) = ⨆({Y. Y ≤ x} ∩ compact_points)"
begin

lemma le_compact:
  shows "x ≤ y ⟷ (∀z∈compact_points. z ≤ x ⟶ z ≤ y)"
by (subst algebraic) (auto simp: Sup_le_iff)

end

lemma (in ccpo) compact_alt_def:
  shows "ccpo.compact Sup (≤) x ⟷ (∀Y. Y ≠ {} ∧ Complete_Partial_Order.chain (≤) Y ∧ x ≤ Sup Y ⟶ (∃y∈Y. x ≤ y))"
by (auto elim!: ccpo.compact.cases dest: ccpo.admissibleD intro!: compactI ccpo.admissibleI)

lemma compact_points_eq_finite_sets: ―‹ \<^citet>‹‹Examples~7.17› in "DaveyPriestley:2002"› ›
  shows "compact_points = Collect finite" (is "?lhs = ?rhs")
proof(rule antisym)
  have *: "X ⊆ ⋃{{x} |x. x ∈ X}" for X :: "'a set" by blast
  show "?lhs ⊆ ?rhs" by (force dest: compact_pointsD[OF _ *] elim: finite_subset)
next
  show "?rhs ⊆ ?lhs" by (metis CollectD compact_pointsI finite_subset_Union subsetI)
qed

instance set :: (type) algebraic_lattice
by standard (fastforce simp: compact_points_eq_finite_sets)

context semilattice_sup
begin

definition sup_irreducible_on :: "'a set ⇒ 'a ⇒ bool" where ―‹ \<^citet>‹‹Definition~2.42› in "DaveyPriestley:2002"› ›
  "sup_irreducible_on A x ⟷ (∀y∈A. ∀z∈A. x = y ⊔ z ⟶ x = y ∨ x = z)"

abbreviation sup_irreducible :: "'a ⇒ bool" where
  "sup_irreducible ≡ sup_irreducible_on UNIV"

lemma sup_irreducible_onI:
  assumes "⋀y z. ⟦y ∈ A; z ∈ A; x = y ⊔ z⟧ ⟹ x = y ∨ x = z"
  shows "sup_irreducible_on A x"
using assms by (simp add: sup_irreducible_on_def)

lemma sup_irreducible_onD:
  assumes "sup_irreducible_on A x"
  assumes "x = y ⊔ z"
  assumes "y ∈ A"
  assumes "z ∈ A"
  shows "x = y ∨ x = z"
using assms by (auto simp: sup_irreducible_on_def)

lemma sup_irreducible_on_less: ―‹ \<^citet>‹‹Definition~2.42 (alt)› in "DaveyPriestley:2002"› ›
  shows "sup_irreducible_on A x ⟷ (∀y∈A. ∀z∈A. y < x ∧ z < x ⟶ y ⊔ z < x)"
by (simp add: sup_irreducible_on_def ac_simps sup.strict_order_iff)
   (metis local.sup.commute local.sup.left_idem)

end

lemma sup_irreducible_bot:
  assumes "⊥ ∈ A"
  shows "sup_irreducible_on A (⊥::_::bounded_semilattice_sup_bot)"
using assms by (auto intro: sup_irreducible_onI)

lemma sup_irreducible_le_conv:
  fixes x::"_::distrib_lattice"
  assumes "sup_irreducible x"
  shows "x ≤ y ⊔ z ⟷ x ≤ y ∨ x ≤ z"
by (auto simp: inf.absorb_iff2 inf_sup_distrib1 ac_simps
         dest: sup_irreducible_onD[OF assms sym, simplified])

lemma set_sup_irreducible:
  shows "sup_irreducible X ⟷ (X = {} ∨ (∃y. X = {y}))" (is "?lhs ⟷ ?rhs")
proof(rule iffI)
  show "?lhs ⟹ ?rhs"
    by (auto simp: sup_irreducible_on_def) (metis insert_is_Un mk_disjoint_insert)
  show "?rhs ⟹ ?lhs" by (auto intro: sup_irreducible_onI)
qed

definition Sup_irreducible_on :: "'a::complete_lattice set ⇒ 'a ⇒ bool" where ―‹ \<^citet>‹‹Definition~10.26› in "DaveyPriestley:2002"› ›
  "Sup_irreducible_on A x ⟷ (∀S⊆A. x = ⨆S ⟶ x ∈ S)"

abbreviation Sup_irreducible :: "'a::complete_lattice ⇒ bool" where
  "Sup_irreducible ≡ Sup_irreducible_on UNIV"

definition Sup_prime_on :: "'a::complete_lattice set ⇒ 'a ⇒ bool" where ―‹ \<^citet>‹‹Definition~10.26› in "DaveyPriestley:2002"› ›
  "Sup_prime_on A x ⟷ (∀S⊆A. x ≤ ⨆S ⟶ (∃s∈S. x ≤ s))"

abbreviation Sup_prime :: "'a::complete_lattice ⇒ bool" where
  "Sup_prime ≡ Sup_prime_on UNIV"

lemma Sup_irreducible_onI:
  assumes "⋀S. ⟦S ⊆ A; x = ⨆S⟧ ⟹ x ∈ S"
  shows "Sup_irreducible_on A x"
using assms by (simp add: Sup_irreducible_on_def)

lemma Sup_irreducible_onD:
  assumes "x = ⨆S"
  assumes "S ⊆ A"
  assumes "Sup_irreducible_on A x"
  shows "x ∈ S"
using assms by (simp add: Sup_irreducible_on_def)

lemma Sup_prime_onI:
  assumes "⋀S. ⟦S ⊆ A; x ≤ ⨆S⟧ ⟹ ∃s∈S. x ≤ s"
  shows "Sup_prime_on A x"
using assms by (simp add: Sup_prime_on_def)

lemma Sup_prime_onE:
  assumes "Sup_prime_on A x"
  assumes "x ≤ ⨆S"
  assumes "S ⊆ A"
  obtains s where "s ∈ S" and "x ≤ s"
using assms Sup_prime_on_def by blast

lemma Sup_prime_on_conv:
  assumes "Sup_prime_on A x"
  assumes "S ⊆ A"
  shows "x ≤ ⨆S ⟷ (∃s∈S. x ≤ s)"
using assms by (auto simp: Sup_prime_on_def intro: Sup_upper2)

lemma Sup_prime_not_bot:
  assumes "Sup_prime_on A x"
  shows "x ≠ ⊥"
using assms by (force simp: Sup_prime_on_def)

lemma Sup_prime_on_imp_Sup_irreducible_on: ―‹ the converse holds in Heyting algebras ›
  assumes "Sup_prime_on A x"
  shows "Sup_irreducible_on A x"
using Sup_upper
by (fastforce intro!: Sup_irreducible_onI intro: antisym elim!: Sup_prime_onE[OF assms, rotated])

lemma Sup_irreducible_on_imp_sup_irreducible_on:
  assumes "Sup_irreducible_on A x"
  assumes "x ∈ A"
  shows "sup_irreducible_on A x"
using assms by (fastforce simp: Sup_irreducible_on_def sup_irreducible_on_def
                          dest: spec[where x="{x, y}" for x y])

lemma Sup_prime_is_compact:
  assumes "Sup_prime x"
  shows "x ∈ compact_points"
using assms by (simp add: compact_points_alt_def Sup_prime_on_def)
(*<*)

end
(*>*)