Theory Galois

(*<*)
theory Galois
imports
  Closures
begin

(*>*)
section‹ Galois connections\label{sec:galois} ›

text‹

Here we collect some classical results for Galois connections. These are drawn from
\<^citet>‹ "Backhouse:2000" and "DaveyPriestley:2002" and
"MeltonSchmidtStrecker:1985" and "MuellerOlm:1997"› amongst others.
The canonical reference is likely \<^citet>‹"GierzEtAl:2003"›.

Our focus is on constructing closures (\S\ref{sec:closures}) conveniently; we are less
interested in the fixed-point story. Many of these results hold for preorders; we simply
work with partial orders (via the \<^locale>‹ordering› locale).
Similarly ∗‹conditionally complete lattices› are often sufficient, but for convenience we
just assume (unconditional) completeness.

›

(* This is less general than we might hope as ‹ordering› already quantifies over the entire type.
   Therefore it cannot handle lattices where we hoist the bottom up a bit, like the ‹prog› lattice.
   Generalising is probably be too much hassle. *)
locale galois =
  orda: ordering less_eqa lessa
+ ordb: ordering less_eqb lessb
    for less_eqa (infix "≤⇩a" 50)
    and lessa (infix "<⇩a" 50)
    and less_eqb (infix "≤⇩b" 50)
    and lessb (infix "<⇩b" 50)
+ fixes lower :: "'a ⇒ 'b"
  fixes upper :: "'b ⇒ 'a"
  assumes galois: "lower x ≤⇩b y ⟷ x ≤⇩a upper y"
begin

lemma monotone_lower:
  shows "monotone (≤⇩a) (≤⇩b) lower"
by (rule monotoneI) (use galois orda.trans ordb.refl in blast)

lemma monotone_upper:
  shows "monotone (≤⇩b) (≤⇩a) upper"
by (rule monotoneI) (use galois ordb.trans orda.refl in blast)

lemmas strengthen_lower[strg] = st_monotone[OF monotone_lower]
lemmas strengthen_upper[strg] = st_monotone[OF monotone_upper]

lemma upper_lower_expansive:
  shows "x ≤⇩a upper (lower x)"
using galois ordb.refl by blast

lemma lower_upper_contractive:
  shows "lower (upper x) ≤⇩b x"
using galois orda.refl by blast

lemma comp_galois: ―‹ \<^citet>‹‹Lemma~19› in "Backhouse:2000"›. Observe that the roles of upper and lower have swapped. ›
  fixes less_eqc :: "'c ⇒ 'c ⇒ bool" (infix "≤⇩c" 50)
  fixes lessc :: "'c ⇒ 'c ⇒ bool" (infix "<⇩c" 50)
  fixes h :: "'a ⇒ 'c"
  fixes k :: "'b ⇒ 'c"
  assumes "partial_preordering (≤⇩c)"
  assumes "monotone (≤⇩a) (≤⇩c) h"
  assumes "monotone (≤⇩b) (≤⇩c) k"
  shows "(∀x. h (upper x) ≤⇩c k x)  ⟷ (∀x. h x ≤⇩c k (lower x))"
using assms(1) monotoneD[OF assms(2)] monotoneD[OF assms(3)]
by (meson lower_upper_contractive partial_preordering.trans upper_lower_expansive)

lemma lower_upper_le_iff: ―‹ \<^citet>‹‹Lemma~23› in "Backhouse:2000"› ›
  assumes "∀x y. lower' x ≤⇩b y ⟷ x ≤⇩a upper' y"
  shows "(∀x. lower' x ≤⇩b lower x) ⟷ (∀y. upper y ≤⇩a upper' y)"
using assms by (meson lower_upper_contractive orda.trans ordb.trans upper_lower_expansive)

lemma lower_upper_unique: ―‹ \<^citet>‹‹Lemma~24› in "Backhouse:2000"› ›
  assumes "∀x y. lower' x ≤⇩b y ⟷ x ≤⇩a upper' y"
  shows "lower' = lower ⟷ upper' = upper"
using assms galois lower_upper_contractive orda.eq_iff ordb.eq_iff upper_lower_expansive by blast

lemma upper_lower_idem:
  shows "upper (lower (upper (lower x))) = upper (lower x)"
by (meson galois lower_upper_contractive orda.antisym ordb.trans upper_lower_expansive)

lemma lower_upper_idem:
  shows "lower (upper (lower (upper x))) = lower (upper x)"
by (metis galois ordb.antisym upper_lower_expansive upper_lower_idem)

lemma lower_upper_lower: ―‹ \<^citet>‹‹Proposition~1.2(2)› in "MeltonSchmidtStrecker:1985"› ›
  shows "lower ∘ upper ∘ lower = lower"
    and "lower (upper (lower x)) = lower x"
using galois lower_upper_contractive ordb.antisym upper_lower_expansive upper_lower_idem by auto

lemma upper_lower_upper:  ―‹ \<^citet>‹‹Proposition~1.2(2)› in "MeltonSchmidtStrecker:1985"› ›
  shows "upper ∘ lower ∘ upper = upper"
    and "upper (lower (upper x)) = upper x"
by (simp_all add: fun_eq_iff)
   (metis galois monotone_upper monotoneD orda.antisym orda.refl upper_lower_expansive)+

definition cl :: "'a ⇒ 'a" where ―‹ The opposite composition yields a kernel operator ›
  "cl x = upper (lower x)"

lemma cl_axiom:
  shows "(x ≤⇩a cl y) = (cl x ≤⇩a cl y)"
by (metis cl_def galois lower_upper_lower(2))

sublocale closure "(≤⇩a)" "(<⇩a)" cl ―‹ incorporates definitions and lemmas into this namespace ›
by standard (rule cl_axiom)

lemma cl_upper:
  shows "cl (upper P) = upper P"
by (simp add: cl_def upper_lower_upper)

lemma closed_upper:
  shows "upper P ∈ closed"
by (simp add: closed_def cl_upper orda.refl)

lemma inj_lower_iff_surj_upper:
  shows "inj lower ⟷ surj upper"
by (metis inj_def surj_def lower_upper_lower(2) upper_lower_upper(2))

lemma inj_lower_iff_upper_lower_id:
  shows "inj lower ⟷ upper ∘ lower = id"
by (metis fun.map_comp id_comp inj_iff inj_on_id inj_on_imageI2 lower_upper_lower(1))

lemma upper_inj_iff_surj_lower:
  shows "inj upper ⟷ surj lower"
by (metis inj_def surj_def lower_upper_lower(2) upper_lower_upper(2))

lemma inj_upper_iff_lower_upper_id:
  shows "inj upper ⟷ lower ∘ upper = id"
by (metis fun.map_comp id_comp inj_iff inj_on_id inj_on_imageI2 upper_lower_upper(1))

lemma lower_downset_upper: ―‹ \<^citet>‹‹Lemma~7.32› in "DaveyPriestley:2002"›: inverse image of lower on a downset is the downset of upper ›
  shows "lower -` {a. a ≤⇩b y} = {a. a ≤⇩a upper y}"
by (simp add: galois)

lemma lower_downset: ―‹ \<^citet>‹‹Lemma~7.32› in "DaveyPriestley:2002"›; equivalent to the Galois axiom ›
  shows "∃!x. lower -` {a. a ≤⇩b y} = {a. a ≤⇩a x}"
by (metis lower_downset_upper mem_Collect_eq orda.antisym orda.refl)

end

setup ‹Sign.mandatory_path "galois"›

lemma axioms_alt:
  fixes less_eqa (infix "≤⇩a" 50)
  fixes less_eqb (infix "≤⇩b" 50)
  fixes lower :: "'a ⇒ 'b"
  fixes upper :: "'b ⇒ 'a"
  assumes oa: "ordering less_eqa lessa"
  assumes ob: "ordering less_eqb lessb"
  assumes ul: "∀x. x ≤⇩a upper (lower x)"
  assumes lu: "∀x. lower (upper x) ≤⇩b x"
  assumes ml: "monotone (≤⇩a) (≤⇩b) lower"
  assumes mu: "monotone (≤⇩b) (≤⇩a) upper"
  shows "lower x ≤⇩b y ⟷ x ≤⇩a upper y"
by (metis lu ml monotoneD mu oa ob ordering.axioms(1) partial_preordering.trans ul)

lemma compose:
  fixes lower⇩1 :: "'b ⇒ 'c"
  fixes lower⇩2 :: "'a ⇒ 'b"
  fixes less_eqa :: "'a ⇒ 'a ⇒ bool"
  assumes "galois less_eqb lessb less_eqc lessc lower⇩1 upper⇩1"
  assumes "galois less_eqa lessa less_eqb lessb lower⇩2 upper⇩2"
  shows "galois less_eqa lessa less_eqc lessc (lower⇩1 ∘ lower⇩2) (upper⇩2 ∘ upper⇩1)"
using assms unfolding galois_def galois_axioms_def by simp

locale complete_lattice =
  cla: complete_lattice "Inf⇩a" "Sup⇩a" "(⊓⇩a)" "(≤⇩a)" "(<⇩a)" "(⊔⇩a)" "⊥⇩a" "⊤⇩a"
+ clb: complete_lattice "Inf⇩b" "Sup⇩b" "(⊓⇩b)" "(≤⇩b)" "(<⇩b)" "(⊔⇩b)" "⊥⇩b" "⊤⇩b"
+ galois "(≤⇩a)" "(<⇩a)" "(≤⇩b)" "(<⇩b)" lower upper
    for less_eqa :: "'a ⇒ 'a ⇒ bool" (infix "≤⇩a" 50)
    and lessa (infix "<⇩a" 50)
    and infa (infixl "⊓⇩a" 70)
    and supa (infixl "⊔⇩a" 65)
    and bota ("⊥⇩a")
    and topa ("⊤⇩a")
    and Inf⇩a Sup⇩a
    and less_eqb :: "'b ⇒ 'b ⇒ bool" (infix "≤⇩b" 50)
    and lessb (infix "<⇩b" 50)
    and infb (infixl "⊓⇩b" 70)
    and supb (infixl "⊔⇩b" 65)
    and botb ("⊥⇩b")
    and topb ("⊤⇩b")
    and Inf⇩b Sup⇩b
    and lower :: "'a ⇒ 'b"
    and upper :: "'b ⇒ 'a"
begin

lemma lower_bot:
  shows "lower ⊥⇩a = ⊥⇩b"
by (simp add: clb.le_bot galois)

lemmas mono2mono_lower[cont_intro, partial_function_mono] = monotone2monotone[OF monotone_lower, simplified]

lemma lower_Sup: ―‹ \<^citet>‹‹Proposition~1.2(6)› in "MeltonSchmidtStrecker:1985"›: \<^term>‹lower› is always a distributive operation ›
  shows "lower (Sup⇩a X) = Sup⇩b (lower ` X)" (is "?lhs = ?rhs")
proof(rule clb.order.antisym)
  show "?lhs ≤⇩b ?rhs" by (meson cla.Sup_least clb.SUP_upper galois)
  show "?rhs ≤⇩b ?lhs" by (meson cla.Sup_le_iff clb.SUP_le_iff galois upper_lower_expansive)
qed

lemma lower_SUP:
  shows "lower (Sup⇩a (f ` X)) = Sup⇩b ((λx. lower (f x)) ` X)"
by (simp add: lower_Sup image_image)

lemma lower_sup:
  shows "lower (X ⊔⇩a Y) = lower X ⊔⇩b lower Y"
using lower_Sup[where X="{X, Y}"] by simp

lemma lower_Inf_le:
  shows "lower (Inf⇩a X) ≤⇩b Inf⇩b (lower ` X)"
by (simp add: cla.Inf_lower2 clb.le_INF_iff galois upper_lower_expansive)

lemma lower_INF_le:
  shows "lower (Inf⇩a (f ` X)) ≤⇩b Inf⇩b ((λx. lower (f x)) ` X)"
by (simp add: clb.order.trans[OF lower_Inf_le] image_image)

lemma lower_inf_le:
  shows "lower (x ⊓⇩a y) ≤⇩b lower x ⊓⇩b lower y"
using lower_Inf_le[where X="{x, y}"] by simp

lemma mcont_lower: ―‹ \<^citet>‹"Backhouse:2000"›: fixed point theory based on Galois connections is less general than using countable chains ›
  shows "mcont Sup⇩a (≤⇩a) Sup⇩b (≤⇩b) lower"
by (meson contI lower_Sup mcontI monotone_lower)

lemma mcont2mcont_lower[cont_intro]:
  assumes "mcont luba orda Sup⇩a (≤⇩a) P"
  shows "mcont luba orda Sup⇩b (≤⇩b) (λx. lower (P x))"
using assms mcont_lower
      partial_function_definitions.mcont2mcont[OF clb.complete_lattice_partial_function_definitions]
by blast

lemma upper_top:
  shows "upper ⊤⇩b = ⊤⇩a"
by (simp add: cla.top_le flip: galois)

lemma Sup_upper_le:
  shows "Sup⇩a (upper ` X) ≤⇩a upper (Sup⇩b X)"
by (meson cla.SUP_le_iff clb.Sup_upper2 galois lower_upper_contractive)

lemma sup_upper_le:
  shows "upper x ⊔⇩a upper y ≤⇩a upper (x ⊔⇩b y)"
using Sup_upper_le[where X="{x, y}"] by simp

lemma upper_Inf: ―‹ \<^citet>‹‹Proposition~1.2(6)› in "MeltonSchmidtStrecker:1985"› ›
  shows "upper (Inf⇩b X) = Inf⇩a (upper ` X)" (is "?lhs = ?rhs")
proof(rule cla.order.antisym)
  show "?lhs ≤⇩a ?rhs" by (meson cla.INF_greatest clb.le_Inf_iff galois lower_upper_contractive)
  show "?rhs ≤⇩a ?lhs" by (meson cla.INF_lower clb.le_Inf_iff galois)
qed

lemma upper_INF:
  shows "upper (Inf⇩b (f ` X)) = Inf⇩a ((λx. upper (f x)) ` X)"
by (simp add: image_image upper_Inf)

lemma upper_inf:
  shows "upper (X ⊓⇩b Y) = upper X ⊓⇩a upper Y"
using upper_Inf[where X="{X, Y}"] by simp

text‹

In a complete lattice ‹lower› is determined by ‹upper› and vice-versa.

›

lemma lower_Inf_upper:
  shows "lower X = Inf⇩b {Y. X ≤⇩a upper Y}"
by (auto simp flip: galois intro: clb.Inf_eqI[symmetric])

lemma upper_Sup_lower:
  shows "upper X = Sup⇩a {Y. lower Y ≤⇩b X}"
by (auto simp: galois intro: cla.Sup_eqI[symmetric])

lemma upper_downwards_closure_lower: ―‹ \<^citet>‹‹Lemma~2.1› in "MeltonSchmidtStrecker:1985"› ›
  shows "upper x = Sup⇩a (lower -` {y. y ≤⇩b x})"
by (simp add: upper_Sup_lower)

sublocale closure_complete_lattice "(≤⇩a)" "(<⇩a)" "(⊓⇩a)" "(⊔⇩a)" "⊥⇩a" "⊤⇩a" "Inf⇩a" "Sup⇩a" cl
by (rule closure_complete_lattice.intro[OF cla.complete_lattice_axioms closure_axioms])

end

locale complete_lattice_distributive =
  galois.complete_lattice
+ assumes upper_Sup_le: "upper (Sup⇩b X) ≤⇩a Sup⇩a (upper ` X)" ―‹ Stronger than Scott continuity, which only asks for this for chain or directed ‹X›. ›
begin

lemma upper_Sup:
  shows "upper (Sup⇩b X) = Sup⇩a (upper ` X)"
by (simp add: Sup_upper_le cla.dual_order.antisym upper_Sup_le)

lemma upper_bot:
  shows "upper ⊥⇩b = ⊥⇩a"
using upper_Sup[where X="{}"] by simp

lemma upper_sup:
  shows "upper (x ⊔⇩b y) = upper x ⊔⇩a upper y"
by (rule upper_Sup[where X="{x, y}", simplified])

lemmas mono2mono_upper[cont_intro, partial_function_mono] = monotone2monotone[OF monotone_upper, simplified]

lemma mcont_upper:
  shows "mcont Sup⇩b (≤⇩b) Sup⇩a (≤⇩a) upper"
by (meson contI upper_Sup mcontI monotone_upper)

lemma mcont2mcont_upper[cont_intro]:
  assumes "mcont luba orda Sup⇩b (≤⇩b) P"
  shows "mcont luba orda Sup⇩a (≤⇩a) (λx. upper (P x))"
by (simp add: ccpo.mcont2mcont'[OF cla.complete_lattice_ccpo mcont_upper _ assms])

sublocale closure_complete_lattice_distributive "(≤⇩a)" "(<⇩a)" "(⊓⇩a)" "(⊔⇩a)" "⊥⇩a" "⊤⇩a" "Inf⇩a" "Sup⇩a" cl
by standard (simp add: cl_def upper_Sup lower_Sup image_image)

lemma cl_bot:
  shows "cl ⊥⇩a = ⊥⇩a"
by (simp add: cl_def lower_bot upper_bot)

lemma closed_bot[iff]:
  shows "⊥⇩a ∈ closed"
by (simp add: cl_bot closed_clI)

end

locale complete_lattice_class =
  galois.complete_lattice
    "(≤)" "(<)" "(⊓)" "(⊔)" "⊥ :: _ :: complete_lattice" "⊤" "Inf" "Sup"
    "(≤)" "(<)" "(⊓)" "(⊔)" "⊥ :: _ :: complete_lattice" "⊤" "Inf" "Sup"
begin

sublocale closure_complete_lattice_class cl ..

end

locale complete_lattice_distributive_class =
  galois.complete_lattice_distributive
    "(≤)" "(<)" "(⊓)" "(⊔)" "⊥ :: _ :: complete_lattice" "⊤" "Inf" "Sup"
    "(≤)" "(<)" "(⊓)" "(⊔)" "⊥ :: _ :: complete_lattice" "⊤" "Inf" "Sup"
begin

sublocale galois.complete_lattice_class ..
sublocale closure_complete_lattice_distributive_class cl ..

end

lemma existence_lower_preserves_Sup: ―‹ \<^citet>‹‹p8 of Oxford TR PRG-44› in "HoareHe:1987"› amongst others ›
  fixes lower :: "_::complete_lattice ⇒ _::complete_lattice"
  assumes "mono lower"
  shows "(∀x y. lower x ≤ y ⟷ x ≤ ⨆{Y. lower Y ≤ y}) ⟷ (∀X. lower (⨆X) ≤ ⨆(lower ` X))" (is "?lhs ⟷ ?rhs")
proof(rule iffI)
  show "?lhs ⟹ ?rhs"
    by (metis SUP_upper Sup_least)
  show "?rhs ⟹ ?lhs"
    by (fastforce intro: Sup_upper SUP_least order.trans elim: order.trans[OF monoD[OF assms]])
qed

lemma lower_preserves_SupI:
  assumes "mono lower"
  assumes "⋀X. lower (⨆X) ≤ ⨆(lower ` X)"
  assumes "⋀x. upper x = ⨆{X. lower X ≤ x}"
  shows "galois.complete_lattice_class lower upper"
by standard (metis assms galois.existence_lower_preserves_Sup)

lemma existence_upper_preserves_Inf:
  fixes upper :: "_::complete_lattice ⇒ _::complete_lattice"
  assumes "mono upper"
  shows "(∀x y.  ⨅{Y. x ≤ upper Y} ≤ y ⟷ x ≤ upper y) ⟷ (∀X. ⨅(upper ` X) ≤ upper (⨅X))" (is "?lhs ⟷ ?rhs")
proof(rule iffI)
  assume ?lhs
  interpret gcl: galois.complete_lattice_class "λx. ⨅{Y. x ≤ upper Y}" upper
    by standard (use ‹?lhs› in blast)
  from gcl.upper_Inf show ?rhs by simp
next
  show "?rhs ⟹ ?lhs"
    by (auto intro: Inf_lower order.trans[rotated] INF_greatest order.trans[OF _ monoD[OF assms], rotated])
qed

lemma upper_preserves_InfI:
  assumes "mono upper"
  assumes "⋀X. ⨅(upper ` X) ≤ upper (⨅X)"
  assumes "⋀x. lower x = ⨅{X. x ≤ upper X}"
  shows "galois.complete_lattice_class lower upper"
by standard (metis assms galois.existence_upper_preserves_Inf)

locale powerset =
  galois.complete_lattice_class lower upper
for lower :: "'a set ⇒ 'b set"
and upper :: "'b set ⇒ 'a set"
begin

lemma lower_insert:
  shows "lower (insert x X) = lower {x} ∪ lower X"
by (metis insert_is_Un lower_sup)

lemma lower_distributive:
  shows "lower X = (⋃x∈X. lower {x})"
using lower_Sup[where X="{{x} |x. x ∈ X}"] by (auto simp: Union_singleton)

sublocale closure_powerset cl ..

end

locale powerset_distributive =
  galois.powerset
+ galois.complete_lattice_distributive_class
begin

lemma upper_insert:
  shows "upper (insert x X) = upper {x} ∪ upper X"
by (metis insert_is_Un upper_sup)

lemma cl_distributive_axiom:
  shows "cl (⋃ X) ⊆ ⋃ (cl ` X)"
by (simp add: cl_def lower_Sup upper_Sup)

sublocale closure_powerset_distributive cl
by standard (simp add: cl_distributive_axiom cla.le_supI1)

end

text‹

\<^citet>‹‹Theorems~3.3.1, 3.3.2› in "MuellerOlm:1997"›: relation image forms a Galois connection.
See also \<^citet>‹‹Exercise~7.18› in "DaveyPriestley:2002"›.

›

definition lower⇩R :: "('a × 'b) set ⇒ 'a set ⇒ 'b set" where
  "lower⇩R R A = R `` A"

definition upper⇩R :: "('a × 'b) set ⇒ 'b set ⇒ 'a set" where
  "upper⇩R R B = {a. ∀b. (a, b) ∈ R ⟶ b ∈ B}"

interpretation relation: galois.powerset "galois.lower⇩R R" "galois.upper⇩R R"
unfolding galois.lower⇩R_def galois.upper⇩R_def by standard blast

context galois.powerset
begin

lemma relations_galois:
  defines "R ≡ {(a, b). b ∈ lower {a}}"
  shows "lower = galois.lower⇩R R"
    and "upper = galois.upper⇩R R"
proof -
  show "lower = galois.lower⇩R R"
  proof(rule HOL.ext)
    fix X
    have "lower X = (⋃x∈X. lower {x})" by (rule lower_distributive)
    also have "… = (⋃x∈X. galois.lower⇩R R {x})" by (simp add: galois.lower⇩R_def R_def)
    also have "… = galois.lower⇩R R X" unfolding galois.lower⇩R_def R_def by blast
    finally show "lower X = galois.lower⇩R R X" .
  qed
  then show "upper = galois.upper⇩R R"
    using galois galois.relation.lower_upper_unique by blast
qed

end

setup ‹Sign.parent_path›


subsection‹ Some Galois connections\label{sec:galois-concrete} ›

setup ‹Sign.mandatory_path "galois"›

locale complete_lattice_class_monomorphic
  = galois.complete_lattice_class upper lower
      for upper :: "'a::complete_lattice ⇒ 'a" and lower :: "'a ⇒ 'a"  ―‹ Avoid ‹'a itself› parameters ›

interpretation conj_imp: galois.complete_lattice_class "(⊓) x" "(❙⟶⇩B) x" for x :: "_::boolean_algebra" ―‹ Classic example ›
by standard (simp add: boolean_implication.conv_sup inf_commute shunt1)

text‹

There are very well-behaved Galois connections arising from the image
(and inverse image) of sets under a function; stuttering is one
instance (\S\ref{sec:safety_logic-stuttering}).

›

locale image_vimage =
  fixes f :: "'a ⇒ 'b"
begin

definition lower :: "'a set ⇒ 'b set" where
  "lower X = f ` X"

definition upper :: "'b set ⇒ 'a set" where
  "upper X = f -` X"

lemma upper_empty[iff]:
  shows "upper {} = {}"
unfolding upper_def by simp

sublocale galois.powerset_distributive lower upper
unfolding lower_def upper_def by standard (simp_all add: image_subset_iff_subset_vimage vimage_Union)

abbreviation equivalent :: "'a relp" where
  "equivalent x y ≡ f x = f y"

lemma equiv:
  shows "Equiv_Relations.equivp equivalent"
by (simp add: equivpI reflpI symp_def transp_def)

lemma equiv_cl_singleton:
  assumes "equivalent x y"
  shows "cl {x} = cl {y}"
using assms by (simp add: cl_def galois.image_vimage.lower_def)

lemma cl_alt_def:
  shows "cl X = {(x, y). equivalent x y} `` X"
by (simp add: cl_def lower_def upper_def vimage_image_eq)

sublocale closure_powerset_distributive_exchange cl
by standard (auto simp: cl_alt_def intro: exchangeI)

lemma closed_in:
  assumes "x ∈ P"
  assumes "equivalent x y"
  assumes P: "P ∈ closed"
  shows "y ∈ P"
using assms(1-2) closed_conv[OF P] unfolding cl_alt_def by blast

lemma clE:
  assumes "x ∈ cl P"
  obtains y where "equivalent y x" and "y ∈ P"
using assms unfolding cl_alt_def by blast

lemma clI[intro]:
  assumes "x ∈ P"
  assumes "equivalent x y"
  shows "y ∈ cl P"
unfolding cl_alt_def using assms by blast

lemma closed_diff[intro]:
  assumes "X ∈ closed"
  assumes "Y ∈ closed"
  shows "X - Y ∈ closed"
by (rule closedI) (metis Diff_iff assms clE closed_in)

lemma closed_uminus[intro]:
  assumes "X ∈ closed"
  shows "-X ∈ closed"
using closed_diff[where X=UNIV, OF _ assms] by fastforce

end

locale image_vimage_monomorphic
  = galois.image_vimage f
      for f :: "'a ⇒ 'a" ―‹ Avoid ‹'a itself› parameters ›

locale image_vimage_idempotent
  = galois.image_vimage_monomorphic +
    assumes f_idempotent: "⋀x. f (f x) = f x"
begin

lemma f_idempotent_comp:
  shows "f ∘ f = f"
by (simp add: comp_def f_idempotent)

lemma idemI:
  assumes "f x ∈ P"
  shows "x ∈ cl P"
using assms f_idempotent by (auto simp: cl_alt_def)

lemma f_cl:
  shows "f x ∈ cl P ⟷ x ∈ cl P"
by (simp add: cl_alt_def f_idempotent)

lemma f_closed:
  assumes "P ∈ closed"
  shows "f x ∈ P ⟷ x ∈ P"
by (metis assms closed_conv f_cl)

lemmas f_closedI = iffD1[OF f_closed]

end

setup ‹Sign.parent_path›
(*<*)

end
(*>*)