Theory Heyting

(*<*)
theory Heyting
imports
  Closures
begin

(*>*)
section‹ Heyting algebras \label{sec:heyting_algebras} ›

text‹

Our (complete) lattices are Heyting algebras. The following development is oriented towards
using the derived Heyting implication in a logical fashion. As there are no standard classes for
semi-(complete-)lattices we simply work with complete lattices.

References:
 ▪ \<^citet>‹"Esakia:2019"› -- fundamental theory
 ▪ \<^citet>‹‹Lemma 5.2.1› in "vanDalen:2004"› -- some equivalences
 ▪ 🌐‹https://en.wikipedia.org/wiki/Pseudocomplement› -- properties

›

class heyting_algebra = complete_lattice +
  assumes inf_Sup_distrib1: "⋀Y::'a set. ⋀x::'a. x ⊓ (⨆Y) = (⨆y∈Y. x ⊓ y)"
begin

definition heyting :: "'a ⇒ 'a ⇒ 'a" (infixr "❙⟶⇩H" 53) where
  "x ❙⟶⇩H y = ⨆{z. x ⊓ z ≤ y}"

lemma heyting: ―‹ The Galois property for ‹(⊓)› and ‹❙⟶⇩H› ›
  shows "z ≤ x ❙⟶⇩H y ⟷ z ⊓ x ≤ y" (is "?lhs ⟷ ?rhs")
proof(rule iffI)
  from inf_Sup_distrib1 have "⨆{a. x ⊓ a ≤ y} ⊓ x ≤ y" by (simp add: SUP_le_iff inf_commute)
  then show "?lhs ⟹ ?rhs" unfolding heyting_def by (meson inf_mono order.trans order_refl)
  show "?rhs ⟹ ?lhs" by (simp add: heyting_def Sup_upper inf.commute)
qed

end

setup ‹Sign.mandatory_path "heyting"›

context heyting_algebra
begin

lemma commute:
  shows "x ⊓ z ≤ y ⟷ z ≤ (x ❙⟶⇩H y)"
by (simp add: heyting inf.commute)

lemmas uncurry = iffD1[OF heyting]
lemmas curry = iffD2[OF heyting]

lemma curry_conv:
  shows "(x ⊓ y ❙⟶⇩H z) = (x ❙⟶⇩H y ❙⟶⇩H z)"
by (simp add: order_eq_iff) (metis heyting eq_refl inf.assoc)

lemma swap:
  shows "P ❙⟶⇩H Q ❙⟶⇩H R = Q ❙⟶⇩H P ❙⟶⇩H R"
by (metis curry_conv inf.commute)

lemma absorb:
  shows "y ⊓ (x ❙⟶⇩H y) = y"
    and "(x ❙⟶⇩H y) ⊓ y = y"
by (simp_all add: curry inf_absorb1 ac_simps)

lemma detachment:
  shows "x ⊓ (x ❙⟶⇩H y) = x ⊓ y" (is ?thesis1)
    and "(x ❙⟶⇩H y) ⊓ x = x ⊓ y" (is ?thesis2)
proof -
  show ?thesis1 by (metis absorb(1) uncurry inf.assoc inf.commute inf.idem inf_iff_le(2))
  then show ?thesis2 by (simp add: ac_simps)
qed

lemma discharge:
  assumes "x' ≤ x"
  shows "x' ⊓ (x ❙⟶⇩H y) = x' ⊓ y" (is ?thesis1)
    and "(x ❙⟶⇩H y) ⊓ x' = y ⊓ x'" (is ?thesis2)
proof -
  from assms show ?thesis1 by (metis curry_conv detachment(2) inf.absorb1)
  then show ?thesis2 by (simp add: ac_simps)
qed

lemma trans:
  shows "(x ❙⟶⇩H y) ⊓ (y ❙⟶⇩H z) ≤ x ❙⟶⇩H z"
by (metis curry detachment(2) swap uncurry inf_le2)

lemma rev_trans:
  shows "(y ❙⟶⇩H z) ⊓ (x ❙⟶⇩H y) ≤ x ❙⟶⇩H z"
by (simp add: inf.commute trans)

lemma discard:
  shows "Q ≤ P ❙⟶⇩H Q"
by (simp add: curry)

lemma infR:
  shows "x ❙⟶⇩H y ⊓ z = (x ❙⟶⇩H y) ⊓ (x ❙⟶⇩H z)"
by (simp add: order_eq_iff curry uncurry detachment le_infI2)

lemma mono:
  assumes "x' ≤ x"
  assumes "y ≤ y'"
  shows "x ❙⟶⇩H y ≤ x' ❙⟶⇩H y'"
using assms by (metis curry detachment(1) uncurry inf_commute inf_absorb2 le_infI1)

lemma strengthen[strg]:
  assumes "st_ord (¬ F) X X'"
  assumes "st_ord F Y Y'"
  shows "st_ord F (X ❙⟶⇩H Y) (X' ❙⟶⇩H Y')"
using assms by (cases F; simp add: heyting.mono)

lemma mono2mono[cont_intro, partial_function_mono]:
  assumes "monotone orda (≥) F"
  assumes "monotone orda (≤) G"
  shows "monotone orda (≤) (λx. F x ❙⟶⇩H G x)"
by (simp add: monotoneI curry discharge le_infI1 monotoneD[OF assms(1)] monotoneD[OF assms(2)])

lemma mp:
  assumes "x ≤ y ❙⟶⇩H z"
  assumes "x ≤ y"
  shows "x ≤ z"
by (meson assms uncurry inf_greatest order.refl order_trans)

lemma botL:
  shows "⊥ ❙⟶⇩H x = ⊤"
by (simp add: heyting top_le)

lemma top_conv:
  shows "x ❙⟶⇩H y = ⊤ ⟷ x ≤ y"
by (metis curry detachment(2) inf_iff_le(1) inf_top.left_neutral)

lemma refl[simp]:
  shows "x ❙⟶⇩H x = ⊤"
by (simp add: top_conv)

lemma topL[simp]:
  shows "⊤ ❙⟶⇩H x = x"
by (metis detachment(1) inf_top_left)

lemma topR[simp]:
  shows "x ❙⟶⇩H ⊤ = ⊤"
by (simp add: top_conv)

lemma K[simp]:
  shows "x ❙⟶⇩H (y ❙⟶⇩H x) = ⊤"
by (simp add: discard top_conv)

subclass distrib_lattice
proof ―‹ \<^citet>‹‹Proposition~1.5.3› in "Esakia:2019"› ›
  have "x ⊓ (y ⊔ z) ≤ x ⊓ y ⊔ x ⊓ z" for x y z :: 'a
    using commute by fastforce
  then have "x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z)" for x y z :: 'a
    by (simp add: order.eq_iff le_infI2)
  then show "x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z)" for x y z :: 'a
    by (rule distrib_imp1)
qed

lemma supL:
  shows "(x ⊔ y) ❙⟶⇩H z = (x ❙⟶⇩H z) ⊓ (y ❙⟶⇩H z)"
by (simp add: order_eq_iff mono curry uncurry inf_sup_distrib1)

subclass (in complete_distrib_lattice) heyting_algebra by standard (rule inf_Sup)

lemma inf_Sup_distrib:
  shows "x ⊓ ⨆Y = (⨆y∈Y. x ⊓ y)"
    and "⨆Y ⊓ x = (⨆y∈Y. x ⊓ y)"
by (simp_all add: inf_Sup_distrib1 inf_commute)

lemma inf_SUP_distrib:
  shows "x ⊓ (⨆i∈I. Y i) = (⨆i∈I. x ⊓ Y i)"
    and "(⨆i∈I. Y i) ⊓ x = (⨆i∈I. Y i ⊓ x)"
by (simp_all add: inf_Sup_distrib image_image ac_simps)

end

lemma eq_boolean_implication: ―‹ the implications coincide in \<^class>‹boolean_algebra›s  ›
  fixes x :: "_::boolean_algebra"
  shows "x ❙⟶⇩H y = x ❙⟶⇩B y"
by (simp add: order.eq_iff boolean_implication_def heyting.detachment heyting.curry flip: shunt1)

lemmas simp_thms =
  heyting.botL
  heyting.topL
  heyting.topR
  heyting.refl

lemma Sup_prime_Sup_irreducible_iff:
  fixes x :: "_::heyting_algebra"
  shows "Sup_prime x ⟷ Sup_irreducible x"
by (fastforce simp: Sup_prime_on_def Sup_irreducible_on_def inf.order_iff heyting.inf_Sup_distrib
             intro: Sup_prime_on_imp_Sup_irreducible_on)

paragraph‹ Logical rules ala HOL ›

lemma bspec:
  fixes P :: "_ ⇒ (_::heyting_algebra)"
  shows "x ∈ X ⟹ (⨅x∈X. P x ❙⟶⇩H Q x) ⊓ P x ≤ Q x" (is "?X ⟹ ?thesis1")
    and "x ∈ X ⟹ P x ⊓ (⨅x∈X. P x ❙⟶⇩H Q x) ≤ Q x" (is "_ ⟹ ?thesis2")
    and "(⨅x. P x ❙⟶⇩H Q x) ⊓ P x ≤ Q x" (is ?thesis3)
    and "P x ⊓ (⨅x. P x ❙⟶⇩H Q x) ≤ Q x" (is ?thesis4)
proof -
  show "?X ⟹ ?thesis1" by (meson INF_lower heyting.uncurry)
  then show "?X ⟹ ?thesis2" by (simp add: inf_commute)
  show ?thesis3 by (simp add: Inf_lower heyting.commute inf_commute)
  then show ?thesis4 by (simp add: inf_commute)
qed

lemma INFL:
  fixes Q :: "_::heyting_algebra"
  shows "(⨅x∈X. P x ❙⟶⇩H Q) = (⨆x∈X. P x) ❙⟶⇩H Q" (is "?lhs = ?rhs")
proof(rule antisym)
  show "?lhs ≤ ?rhs" by (meson INFE SUPE order.refl heyting.commute heyting.uncurry)
  show "?rhs ≤ ?lhs" by (simp add: INFI SupI heyting.mono)
qed

lemmas SUPL = heyting.INFL[symmetric]

lemma INFR:
  fixes P :: "_::heyting_algebra"
  shows "(⨅x∈X. P ❙⟶⇩H Q x) = (P ❙⟶⇩H (⨅x∈X. Q x))" (is "?lhs = ?rhs")
by (simp add: order_eq_iff INFI INF_lower heyting.mono)
   (meson INFI INF_lower heyting.curry heyting.uncurry)

lemmas Inf_simps = ―‹ "Miniscoping: pushing in universal quantifiers." ›
  Inf_inf
  inf_Inf
  INF_inf_const1
  INF_inf_const2
  heyting.INFL
  heyting.INFR

lemma SUPL_le:
  fixes Q :: "_::heyting_algebra"
  shows "(⨆x∈X. P x ❙⟶⇩H Q) ≤ (⨅x∈X. P x) ❙⟶⇩H Q"
by (simp add: INF_lower SUPE heyting.mono)

lemma SUPR_le:
  fixes P :: "_::heyting_algebra"
  shows "(⨆x∈X. P ❙⟶⇩H Q x) ≤ P ❙⟶⇩H (⨆x∈X. Q x)"
by (simp add: SUPE SUP_upper heyting.mono)

lemma SUP_inf:
  fixes Q :: "_::heyting_algebra"
  shows "(⨆x∈X. P x ⊓ Q) = (⨆x∈X. P x) ⊓ Q"
by (simp add: heyting.inf_SUP_distrib(2))

lemma inf_SUP:
  fixes P :: "_::heyting_algebra"
  shows "(⨆x∈X. P ⊓ Q x) =  P ⊓ (⨆x∈X. Q x)"
by (simp add: heyting.inf_SUP_distrib(1))

lemmas Sup_simps = ―‹ "Miniscoping: pushing in universal quantifiers." ›
  sup_SUP
  SUP_sup
  heyting.inf_SUP
  heyting.SUP_inf

lemma mcont2mcont_inf[cont_intro]:
  fixes F :: "_ ⇒ 'a::heyting_algebra"
  fixes G :: "_ ⇒ 'a::heyting_algebra"
  assumes "mcont luba orda Sup (≤) F"
  assumes "mcont luba orda Sup (≤) G"
  shows "mcont luba orda Sup (≤) (λx. F x ⊓ G x)"
proof -
  have mcont_inf1: "mcont Sup (≤) Sup (≤) (λy. x ⊓ y)" for x :: "'a::heyting_algebra"
    by (auto intro!: contI mcontI monotoneI intro: le_infI2 simp flip: heyting.inf_SUP_distrib)
  then have mcont_inf2: "mcont Sup (≤) Sup (≤) (λx. x ⊓ y)" for y :: "'a::heyting_algebra"
    by (subst inf.commute) (rule mcont_inf1)
  from assms mcont_inf1 mcont_inf2 show ?thesis
    by (best intro: ccpo.mcont2mcont'[OF complete_lattice_ccpo] ccpo.mcont_const[OF complete_lattice_ccpo])
qed

lemma closure_imp_distrib_le: ―‹ \<^citet>‹‹Lemma~3.3› in "AbadiPlotkin:1993"›, generalized ›
  fixes P Q :: "_ :: heyting_algebra"
  assumes cl: "closure_axioms (≤) cl"
  assumes cl_inf: "⋀x y. cl x ⊓ cl y ≤ cl (x ⊓ y)"
  shows "P ❙⟶⇩H Q ≤ cl P ❙⟶⇩H cl Q"
proof -
  from cl have "(P ❙⟶⇩H Q) ⊓ cl P ≤ cl (P ❙⟶⇩H Q) ⊓ cl P"
    by (metis (mono_tags) closure_axioms_def inf_mono order.refl)
  also have "… ≤ cl ((P ❙⟶⇩H Q) ⊓ P)"
    by (simp add: cl_inf)
  also from cl have "… ≤ cl Q"
    by (metis (mono_tags) closure_axioms_def order.refl heyting.mono heyting.uncurry)
  finally show ?thesis
    by (simp add: heyting)
qed

setup ‹Sign.parent_path›


paragraph‹ Pseudocomplements ›

definition pseudocomplement :: "'a::heyting_algebra ⇒ 'a" ("❙¬⇩H _" [75] 75) where
  "❙¬⇩Hx = x ❙⟶⇩H ⊥"

lemma pseudocomplementI:
  shows "x ≤ ❙¬⇩Hy ⟷ x ⊓ y ≤ ⊥"
by (simp add: pseudocomplement_def heyting)

setup ‹Sign.mandatory_path "pseudocomplement"›

lemma monotone:
  shows "antimono pseudocomplement"
by (simp add: antimonoI heyting.mono pseudocomplement_def)

lemmas strengthen[strg] = st_monotone[OF pseudocomplement.monotone]
lemmas mono = monotoneD[OF pseudocomplement.monotone]
lemmas mono2mono[cont_intro, partial_function_mono]
   = monotone2monotone[OF pseudocomplement.monotone, simplified, of orda P for orda P]

lemma eq_boolean_negation: ―‹ the negations coincide in \<^class>‹boolean_algebra›s  ›
  fixes x :: "_::{boolean_algebra,heyting_algebra}"
  shows "❙¬⇩Hx = -x"
by (simp add: pseudocomplement_def heyting.eq_boolean_implication)

lemma heyting:
  shows "x ❙⟶⇩H ❙¬⇩Hx = ❙¬⇩Hx"
by (simp add: pseudocomplement_def order_eq_iff heyting heyting.detachment)

lemma Inf:
  shows "x ⊓ ❙¬⇩Hx = ⊥"
    and "❙¬⇩Hx ⊓ x = ⊥"
by (simp_all add: pseudocomplement_def heyting.detachment)

lemma double_le:
  shows "x ≤ ❙¬⇩H❙¬⇩Hx"
by (simp add: pseudocomplement_def heyting.detachment heyting.curry)

interpretation double: closure_complete_lattice_class "pseudocomplement ∘ pseudocomplement"
by standard (simp; meson order.trans pseudocomplement.double_le pseudocomplement.mono)

lemma triple:
  shows "❙¬⇩H❙¬⇩H❙¬⇩Hx = ❙¬⇩Hx"
by (simp add: order_eq_iff pseudocomplement.double_le pseudocomplement.mono)

lemma contrapos_le:
  shows "x ❙⟶⇩H y ≤ ❙¬⇩Hy ❙⟶⇩H ❙¬⇩Hx"
by (simp add: heyting.curry heyting.trans pseudocomplement_def)

lemma sup_inf: ―‹ half of de Morgan ›
  shows "❙¬⇩H(x ⊔ y) = ❙¬⇩Hx ⊓ ❙¬⇩Hy"
by (simp add: pseudocomplement_def heyting.supL)

lemma inf_sup_weak: ―‹ the weakened other half of de Morgan ›
  shows "❙¬⇩H(x ⊓ y) = ❙¬⇩H❙¬⇩H(❙¬⇩Hx ⊔ ❙¬⇩Hy)"
by (metis (no_types, opaque_lifting) pseudocomplement_def heyting.curry_conv heyting.supL inf_commute pseudocomplement.triple)                   

lemma fix_triv:
  assumes "x = ❙¬⇩Hx"
  shows "x = y"
using assms by (metis antisym bot.extremum inf.idem inf_le2 pseudocomplementI)

lemma double_top:
  shows "❙¬⇩H❙¬⇩H(x ⊔ ❙¬⇩Hx) = ⊤"
by (metis pseudocomplement_def heyting.refl pseudocomplement.Inf(1) pseudocomplement.sup_inf)

lemma Inf_inf:
  fixes P :: "_ ⇒ (_::heyting_algebra)"
  shows "(⨅x. P x) ⊓ ❙¬⇩HP x = ⊥"
by (simp add: pseudocomplement_def Inf_lower heyting.discharge(1))

lemma SUP_le: ―‹ half of de Morgan ›
  fixes P :: "_ ⇒ (_::heyting_algebra)"
  shows "(⨆x∈X. P x) ≤ ❙¬⇩H(⨅x∈X. ❙¬⇩HP x)"
by (rule SUP_least) (meson INF_lower order.trans pseudocomplement.double_le pseudocomplement.mono)

lemma SUP_INF_le:
  fixes P :: "_ ⇒ (_::heyting_algebra)"
  shows "(⨆x∈X. ❙¬⇩HP x) ≤ ❙¬⇩H(⨅x∈X. P x)"
by (simp add: INF_lower SUPE pseudocomplement.mono)

lemma SUP:
  fixes P :: "_ ⇒ (_::heyting_algebra)"
  shows "❙¬⇩H(⨆x∈X. P x) = (⨅x∈X. ❙¬⇩HP x)"
by (simp add: order.eq_iff SUP_upper le_INF_iff pseudocomplement.mono)
   (metis inf_commute pseudocomplement.SUP_le pseudocomplementI)

setup ‹Sign.parent_path›


subsection‹ Downwards closure of preorders (downsets) \label{sec:closures-downwards} ›

text‹

A ∗‹downset› (also ∗‹lower set› and ∗‹order ideal›) is a subset of a preorder that is closed under
the order relation. (An ∗‹ideal› is a downset that is \<^const>‹directed›.) Some results require
antisymmetry (a partial order).

References:
 ▪ \<^citet>‹"Vickers:1989"›, early chapters.
 ▪ 🌐‹https://en.wikipedia.org/wiki/Alexandrov_topology›
 ▪ \<^citet>‹‹\S3› in "AbadiPlotkin:1991"›

›

setup ‹Sign.mandatory_path "downwards"›

definition cl :: "'a::preorder set ⇒ 'a set" where
  "cl P = {x |x y. y ∈ P ∧ x ≤ y}"

setup ‹Sign.parent_path›

interpretation downwards: closure_powerset_distributive downwards.cl ―‹ On preorders ›
proof standard
  show "(P ⊆ downwards.cl Q) ⟷ (downwards.cl P ⊆ downwards.cl Q)" for P Q :: "'a set"
    unfolding downwards.cl_def by (auto dest: order_trans)
  show "downwards.cl (⋃X) ⊆ ⋃ (downwards.cl ` X) ∪ downwards.cl {}" for X :: "'a set set"
    unfolding downwards.cl_def by auto
qed

interpretation downwards: closure_powerset_distributive_anti_exchange "(downwards.cl::_::order set ⇒ _)"
  ―‹ On partial orders; see \<^citet>‹"PfaltzSlapal:2013"› ›
by standard (unfold downwards.cl_def; blast intro: anti_exchangeI antisym)

setup ‹Sign.mandatory_path "downwards"›

lemma cl_empty:
  shows "downwards.cl {} = {}"
unfolding downwards.cl_def by simp

lemma closed_empty[iff]:
  shows "{} ∈ downwards.closed"
using downwards.cl_def by fastforce

lemma clI[intro]:
  assumes "y ∈ P"
  assumes "x ≤ y"
  shows "x ∈ downwards.cl P"
unfolding closure.closed_def downwards.cl_def using assms by blast

lemma clE:
  assumes "x ∈ downwards.cl P"
  obtains y where "y ∈ P" and "x ≤ y"
using assms unfolding downwards.cl_def by fast

lemma closed_in:
  assumes "x ∈ P"
  assumes "y ≤ x"
  assumes "P ∈ downwards.closed"
  shows "y ∈ P"
using assms unfolding downwards.cl_def downwards.closed_def by blast

lemma order_embedding: ―‹ On preorders; see \<^citet>‹‹\S1.35› in "DaveyPriestley:2002"› ›
  fixes x :: "_::preorder"
  shows "downwards.cl {x} ⊆ downwards.cl {y} ⟷ x ≤ y"
using downwards.cl by (blast elim: downwards.clE)

text‹

The lattice of downsets of a set ‹X› is always a \<^class>‹heyting_algebra›.

References:
 ▪ \<^citet>‹‹\S7.5› in "Ono:2019"›; uses upsets, points to \<^citet>‹"Stone:1938"› as the origin
 ▪ \<^citet>‹‹\S2.2› in "Esakia:2019"›
 ▪ 🌐‹https://en.wikipedia.org/wiki/Intuitionistic_logic#Heyting_algebra_semantics›

›

definition imp :: "'a::preorder set ⇒ 'a set ⇒ 'a set" where
  "imp P Q = {σ. ∀σ'≤σ. σ' ∈ P ⟶ σ' ∈ Q}"

lemma imp_refl:
  shows "downwards.imp P P = UNIV"
by (simp add: downwards.imp_def)

lemma imp_contained:
  assumes "P ⊆ Q"
  shows "downwards.imp P Q = UNIV"
unfolding downwards.imp_def using assms by fast

lemma heyting_imp:
  assumes "P ∈ downwards.closed"
  shows "P ⊆ downwards.imp Q R ⟷ P ∩ Q ⊆ R"
using assms unfolding downwards.imp_def downwards.closed_def by blast

lemma imp_mp':
  assumes "σ ∈ downwards.imp P Q"
  assumes "σ ∈ P"
  shows "σ ∈ Q"
using assms by (simp add: downwards.imp_def)

lemma imp_mp:
  shows "P ∩ downwards.imp P Q ⊆ Q"
    and "downwards.imp P Q ∩ P ⊆ Q"
by (meson IntD1 IntD2 downwards.imp_mp' subsetI)+

lemma imp_contains:
  assumes "X ⊆ Q"
  assumes "X ∈ downwards.closed"
  shows "X ⊆ downwards.imp P Q"
using assms by (auto simp: downwards.imp_def elim: downwards.closed_in)

lemma imp_downwards:
  assumes "y ∈ downwards.imp P Q"
  assumes "x ≤ y"
  shows "x ∈ downwards.imp P Q"
using assms order_trans by (force simp: downwards.imp_def)

lemma closed_imp:
  shows "downwards.imp P Q ∈ downwards.closed"
by (meson downwards.clE downwards.closedI downwards.imp_downwards)

text‹

The set ‹downwards.imp P Q› is the greatest downset contained in the Boolean implication
‹P ❙⟶⇩B Q›, i.e., ‹downwards.imp› is the ∗‹kernel› of ‹(❙⟶⇩B)› \<^citep>‹"Zwiers:1989"›.
Note that ``kernel'' is a choice or interior function.

›

lemma imp_boolean_implication_subseteq:
  shows "downwards.imp P Q ⊆ P ❙⟶⇩B Q"
unfolding downwards.imp_def boolean_implication.set_alt_def by blast

lemma downwards_closed_imp_greatest:
  assumes "R ⊆ P ❙⟶⇩B Q"
  assumes "R ∈ downwards.closed"
  shows "R ⊆ downwards.imp P Q"
using assms unfolding boolean_implication.set_alt_def downwards.imp_def downwards.closed_def by blast

definition kernel :: "'a::order set ⇒ 'a set" where
  "kernel X = ⨆{Q ∈ downwards.closed. Q ⊆ X}"

lemma kernel_def2:
  shows "downwards.kernel X = {σ. ∀σ'≤σ. σ' ∈ X}" (is "?lhs = ?rhs")
proof(rule antisym)
  show "?lhs ⊆ ?rhs"
    unfolding downwards.kernel_def using downwards.closed_conv by blast
next
  have "x ∈ ?lhs" if "x ∈ ?rhs" for x
    unfolding downwards.kernel_def using that
    by (auto elim: downwards.clE intro: exI[where x="downwards.cl {x}"])
  then show "?rhs ⊆ ?lhs" by blast
qed

lemma kernel_contractive:
  shows "downwards.kernel X ⊆ X"
unfolding downwards.kernel_def by blast

lemma kernel_idempotent:
  shows "downwards.kernel (downwards.kernel X) = downwards.kernel X"
unfolding downwards.kernel_def by blast

lemma kernel_monotone:
  shows "mono downwards.kernel"
unfolding downwards.kernel_def by (rule monotoneI) blast

lemma closed_kernel_conv:
  shows "X ∈ downwards.closed ⟷ downwards.kernel X = X"
unfolding downwards.kernel_def2 downwards.closed_def by (blast elim: downwards.clE)

lemma closed_kernel:
  shows "downwards.kernel X ∈ downwards.closed"
by (simp add: downwards.closed_kernel_conv downwards.kernel_idempotent)

lemma kernel_cl:
  shows "downwards.kernel (downwards.cl X) = downwards.cl X"
using downwards.closed_kernel_conv by blast

lemma cl_kernel:
  shows "downwards.cl (downwards.kernel X) = downwards.kernel X"
by (simp flip: downwards.closed_conv add: downwards.closed_kernel)

lemma kernel_boolean_implication:
  fixes P :: "_::order"
  shows "downwards.kernel (P ❙⟶⇩B Q) = downwards.imp P Q"
unfolding downwards.kernel_def2 boolean_implication.set_alt_def downwards.imp_def by blast

setup ‹Sign.parent_path›
(*<*)

end
(*>*)