Quelle  Galois.thy

(*<*)
theory Galois
imports
  Closures
begin

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

text‹

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

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

 ›

(* This is less general than we might hope as \<open>ordering\<close> already quantifies over the entire type.
   Therefore it cannot handle lattices where we hoist the bottom up a bit, like the \<open>prog\<close> 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 ‹<\<^sub>a› 50)
    and less_eqb (infix ‹≤_b› 50)
    and lessb (infix ‹<\<^sub>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: ―‹ 🍋‹‹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 ‹<\<^sub>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: ―‹ 🍋‹‹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: ―‹ 🍋‹‹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: ―‹ 🍋‹‹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:  ―‹ 🍋‹‹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: ―‹ 🍋‹‹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: ―‹ 🍋‹‹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₁ :: "'b ==> 'c"
  fixes lower₂ :: "'a ==> 'b"
  fixes less_eqa :: "'a ==> 'a ==> bool"
  assumes "galois less_eqb lessb less_eqc lessc lower₁ upper₁"
  assumes "galois less_eqa lessa less_eqb lessb lower₂ upper₂"
  shows "galois less_eqa lessa less_eqc lessc (lower₁ ∘ lower₂) (upper₂ ∘ upper₁)"
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 ‹<\<^sub>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 ‹<\<^sub>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: ―‹ 🍋‹‹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<sub>b</sub> ((λ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)) ≤<sub>b</sub> Inf<sub>b</sub> ((λ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: ―‹ 🍋‹"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: ―‹ 🍋‹‹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<sub>a</sub> ((λ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‹

  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: ―‹ 🍋‹‹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: ―‹ 🍋‹‹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‹

 🍋‹‹Theorems~3.3.1, 3.3.2› in "MuellerOlm:1997"›: relation image forms a Galois connection.
  also 🍋‹‹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" "(\<longrightarrow>_B) x" for x :: "_::boolean_algebra" ―‹ Classic example ›
by standard (simp add: boolean_implication.conv_sup inf_commute shunt1)

text‹

  are very well-behaved Galois connections arising from the image
 and inverse image) of sets under a function; stuttering is one
  (\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
(*>*)