SSL Closures.thy

(*<*)
theory Closures
imports
  More_Lattices
begin

(*>*)
section‹ Closure operators\label{sec:closures} ›

text‹

  semantic spaces are modelled as lattices arising from the fixed
  of various closure operators. We attempt to reduce our proof
  by defining a locale for Kuratowski's closure axioms,
  we do not requre strictness (i.e., it need not be the case that
  closure maps ‹⊥› to
 ‹⊥›). 🍋‹‹\S2.33› in
 DaveyPriestley:2002"› term these 🪙‹topped
  structures›; see also
 🍋‹"PfaltzSlapal:2013"› for additional useful
 .

 ›

locale closure =
  ordering "(\<le>)" "(<)" ―‹ We use a partial order as a preorder does not ensure that the closure is idempotent ›
  for less_eq :: "'a ==> 'a ==> bool" (infix ‹\≤› 50)
     and less :: "'a ==> 'a ==> bool" (infix ‹<› 50)
+ fixes cl :: "'a ==> 'a"
  assumes cl: "x \<le> cl y ⟷ cl x \<le> cl y" ―‹ All-in-one non-strict Kuratowski axiom ›
begin

definition closed :: "'a set" where ―‹ These pre fixed points form a complete lattice ala Tarski/Knaster ›
  "closed = {x. cl x \<le> x}"

lemma closed_clI:
  assumes "cl x \<le> x"
  shows "x ∈ closed"
unfolding closed_def using assms by simp

lemma expansive:
  shows "x \<le> cl x"
by (simp add: cl refl)

lemma idempotent[simp]:
  shows "cl (cl x) = cl x"
    and "cl ∘ cl = cl"
using cl antisym by (auto iff: expansive)

lemma monotone_cl:
  shows "monotone (\<le>) (\<le>) cl"
by (rule monotoneI) (meson cl expansive trans)

lemmas strengthen_cl[strg] = st_monotone[OF monotone_cl]
lemmas mono_cl[trans] = monotoneD[OF monotone_cl]

lemma least:
  assumes "x \<le> y"
  assumes "y ∈ closed"
  shows "cl x \<le> y"
using assms cl closed_def trans by (blast intro: expansive)

lemma least_conv:
  assumes "y ∈ closed"
  shows "cl x \<le> y ⟷ x \<le> y"
using assms expansive least trans by blast

lemma closed[iff]:
  shows "cl x ∈ closed"
unfolding closed_def by (simp add: refl)

lemma le_closedE:
  assumes "x \<le> cl y"
  assumes "y ∈ closed"
  shows "x \<le> y"
using assms closed_def trans by blast

lemma closed_conv: ―‹ Typically used to manifest the closure using ‹subst› ›
  assumes "X ∈ closed"
  shows "X = cl X"
using assms unfolding closed_def by (blast intro: antisym expansive)

end

lemma (in ordering) closure_axioms_alt_def: ―‹ Equivalence with the Kuratowski closure axioms ›
  shows "closure_axioms (\<le>) cl ⟷ (∀x. x \<le> cl x) ∧ monotone (\<le>) (\<le>) cl ∧ (∀x. cl (cl x) = cl x)"
unfolding closure_axioms_def monotone_def by (metis antisym trans refl)

lemma (in ordering) closureI:
  assumes "∧x. x \<le> cl x"
  assumes "monotone (\<le>) (\<le>) cl"
  assumes "∧x. cl (cl x) = cl x"
  shows "closure (\<le>) (<) cl"
by (blast intro: assms closure.intro[OF ordering_axioms, unfolded closure_axioms_alt_def])

lemma closure_inf_closure:
  fixes cl₁ :: "'a::semilattice_inf ==> 'a"
  assumes "closure_axioms (≤) cl₁"
  assumes "closure_axioms (≤) cl₂"
  shows "closure_axioms (≤) (λX. cl₁ X ⊓ cl₂ X)"
using assms unfolding closure_axioms_def by (meson order.trans inf_mono le_inf_iff order_refl)


subsection‹ Complete lattices and algebraic closures\label{sec:closures-lattices} ›

locale closure_complete_lattice =
  complete_lattice "\<Sqinter>" "\<Squnion>" "(\<sqinter>)" "(\<le>)" "(<)" "(\<squnion>)" "\<bottom>" "\<top>"
+ closure "(\<le>)" "(<)" cl
    for less_eqa :: "'a ==> 'a ==> bool" (infix ‹\≤› 50)
    and lessa (infix ‹<› 50)
    and infa (infixl ‹\⊓› 70)
    and supa (infixl ‹\⊔› 65)
    and bota (‹\⊥›)
    and topa (‹\⊤›)
    and Inf (‹\⊓›)
    and Sup (‹\⊔›)
    and cl :: "'a ==> 'a"
begin

lemma cl_bot_least:
  shows "cl \<bottom> \<le> cl X"
using cl by auto

lemma cl_Inf_closed:
  shows "cl x = \<Sqinter>{y ∈ closed. x \<le> y}"
by (blast intro: sym[OF Inf_eqI] least expansive)

lemma cl_top:
  shows "cl \<top> = \<top>"
by (simp add: top_le expansive)

lemma closed_top[iff]:
  shows "\<top> ∈ closed"
unfolding closed_def by simp

lemma Sup_cl_le:
  shows "\<Squnion>(cl ` X) \<le> cl (\<Squnion>X)"
by (meson cl expansive SUP_least Sup_le_iff)

lemma sup_cl_le:
  shows "cl x \<squnion> cl y \<le> cl (x \<squnion> y)"
using Sup_cl_le[where X="{x, y}"] by simp

lemma cl_Inf_le:
  shows "cl (\<Sqinter>X) \<le> \<Sqinter>(cl ` X)"
by (meson cl expansive INF_greatest Inf_lower2)

lemma cl_inf_le:
  shows "cl (x \<sqinter> y) \<le> cl x \<sqinter> cl y"
using cl_Inf_le[where X="{x, y}"] by simp

lemma closed_Inf:
  assumes "X ⊆ closed"
  shows "\<Sqinter>X ∈ closed"
unfolding closed_def using assms by (simp add: least Inf_greatest Inf_lower subset_eq)

lemmas closed_Inf'[intro] = closed_Inf[OF subsetI]

lemma closed_inf[intro]:
  assumes "P ∈ closed"
  assumes "Q ∈ closed"
  shows "P \<sqinter> Q ∈ closed"
using assms closed_Inf[where X="{P, Q}"] by simp

lemmas mono2mono[cont_intro, partial_function_mono] = monotone2monotone[OF monotone_cl, simplified]

definition dense :: "'a set" where
  "dense = {x. cl x = \<top>}"

lemma dense_top:
  shows "\<top> ∈ dense"
by (simp add: dense_def cl_top)

lemma dense_Sup:
  assumes "X ⊆ dense"
  assumes "X ≠ {}"
  shows "\<Squnion>X ∈ dense"
using assms by (fastforce simp: dense_def order.eq_iff intro: order.trans[OF _ Sup_cl_le] elim: SUP_upper2)

lemma dense_sup:
  assumes "P ∈ dense"
  assumes "Q ∈ dense"
  shows "P \<squnion> Q ∈ dense"
using assms dense_def top_le sup_cl_le by auto

lemma dense_le:
  assumes "P ∈ dense"
  assumes "P \<le> Q"
  shows "Q ∈ dense"
using assms dense_def top_le mono_cl by auto

lemma dense_inf_closed:
  shows "dense ∩ closed = {\<top>}"
using dense_def closed_conv closed_top by fastforce

end

locale closure_complete_lattice_class =
  closure_complete_lattice "(≤)" "(<)" "(⊓)" "(⊔)" "⊥ :: _ :: complete_lattice" "⊤" "Inf" "Sup"

text‹

  closures for logical purposes are taken to be ``algebraic'', aka ``consequence operators''
 🍋‹‹Definition~7.12› in "DaveyPriestley:2002"›, where 🪙‹compactness› does the work
  the finite/singleton sets.

 ›

locale closure_complete_lattice_algebraic = ―‹ 🍋‹‹Definition~7.12› in "DaveyPriestley:2002"› ›
  closure_complete_lattice
+ assumes algebraic_le: "cl x \<le> \<Squnion>(cl ` ({y. y \<le> x} ∩ compact_points))" ―‹ The converse is given by monotonicity ›
begin

lemma algebraic:
  shows "cl x = \<Squnion>(cl ` ({y. y \<le> x} ∩ compact_points))"
by (clarsimp simp: order.eq_iff Sup_le_iff algebraic_le expansive simp flip: cl elim!: order.trans)

lemma cont_cl: ―‹ Equivalent to @{thm [source] algebraic_le} 🍋‹‹Theorem~7.14› in "DaveyPriestley:2002"› ›
  shows "cont \<Squnion> (\<le>) \<Squnion> (\<le>) cl"
proof(rule contI)
  fix X :: "'a set"
  assume X: "Complete_Partial_Order.chain (\<le>) X" "X ≠ {}"
  show "cl (\<Squnion>X) = \<Squnion>(cl ` X)" (is "?lhs = ?rhs")
  proof(rule order.antisym[OF _ Sup_cl_le])
    have "?lhs = \<Squnion>(cl ` ({y. y \<le> \<Squnion>X} ∩ compact_points))" by (subst algebraic) simp
    also from X have "… \<le> \<Squnion>(cl ` ({Y |Y x. Y \<le> x ∧ x ∈ X} ∩ compact_points))"
      by (auto dest: chain_directed compact_points_directedD intro: SUP_upper simp: Sup_le_iff)
    also have "… \<le> ?rhs"
      by (clarsimp simp: Sup_le_iff SUP_upper2 monotoneD[OF monotone_cl])
    finally show "?lhs \<le> ?rhs" .
  qed
qed

lemma mcont_cl:
  shows "mcont \<Squnion> (\<le>) \<Squnion> (\<le>) cl"
by (simp add: mcontI[OF _ cont_cl])

lemma mcont2mcont_cl[cont_intro]:
  assumes "mcont luba orda \<Squnion> (\<le>) P"
  shows "mcont luba orda \<Squnion> (\<le>) (λx. cl (P x))"
using assms ccpo.mcont2mcont[OF complete_lattice_ccpo] mcont_cl by blast

end

locale closure_complete_lattice_algebraic_class =
  closure_complete_lattice_algebraic "(≤)" "(<)" "(⊓)" "(⊔)" "⊥ :: _ :: complete_lattice" "⊤" "Inf" "Sup"

text‹

  closures often satisfy the stronger condition of 🪙‹distributivity› (see
 🍋‹‹\S2› in "Scott:1980"›).

 ›

locale closure_complete_lattice_distributive =
  closure_complete_lattice
+ assumes cl_Sup_le: "cl (\<Squnion>X) \<le> \<Squnion>(cl ` X) \<squnion> cl \<bottom>"
begin

lemma cl_Sup:
  shows "cl (\<Squnion>X) = \<Squnion>(cl ` X) \<squnion> cl \<bottom>"
by (simp add: order.eq_iff Sup_cl_le cl_Sup_le cl_bot_least)

lemma cl_Sup_not_empty:
  assumes "X ≠ {}"
  shows "cl (\<Squnion>X) = \<Squnion>(cl ` X)"
by (metis assms cl_Sup cl_bot_least SUP_eq_const SUP_upper2 sup.orderE)

lemma cl_sup:
  shows "cl (X \<squnion> Y) = cl X \<squnion> cl Y"
using cl_Sup[where X="{X, Y}"] by (simp add: sup_absorb1 cl_bot_least le_supI2)

lemma closed_sup[intro]:
  assumes "P ∈ closed"
  assumes "Q ∈ closed"
  shows "P \<squnion> Q ∈ closed"
by (metis assms cl_sup closed_conv closed)

lemma closed_Sup: ―‹ Alexandrov: 🪙‹https://en.wikipedia.org/wiki/Alexandrov_topology› ›
  assumes "X ⊆ closed"
  shows "\<Squnion>X \<squnion> cl \<bottom> ∈ closed"
using assms by (fastforce simp: cl_Sup cl_sup Sup_le_iff simp flip: closed_conv intro: closed_clI Sup_upper le_supI1)

lemmas closed_Sup'[intro] = closed_Sup[OF subsetI]

lemma cont_cl:
  shows "cont \<Squnion> (\<le>) \<Squnion> (\<le>) cl"
by (simp add: cl_Sup_not_empty contI)

lemma mcont_cl:
  shows "mcont \<Squnion> (\<le>) \<Squnion> (\<le>) cl"
by (simp add: mcontI[OF _ cont_cl])

lemma mcont2mcont_cl[cont_intro]:
  assumes "mcont luba orda \<Squnion> (\<le>) F"
  shows "mcont luba orda \<Squnion> (\<le>) (λx. cl (F x))"
using assms ccpo.mcont2mcont[OF complete_lattice_ccpo] mcont_cl by blast

lemma closure_sup_irreducible_on: ―‹ converse requires the closure to be T0 ›
  assumes "sup_irreducible_on closed (cl x)"
  shows "sup_irreducible_on closed x"
using assms sup_irreducible_on_def closed_conv closed_sup by auto

end

locale closure_complete_lattice_distributive_class =
  closure_complete_lattice_distributive "(≤)" "(<)" "(⊓)" "(⊔)" "⊥ :: _ :: complete_lattice" "⊤" "Inf" "Sup"

locale closure_complete_distrib_lattice_distributive_class =
  closure_complete_lattice_distributive "(≤)" "(<)" "(⊓)" "(⊔)" "⊥ :: _ :: complete_distrib_lattice" "⊤" "Inf" "Sup"
begin

text‹

  lattice arising from the closed elements for a distributive closure is completely distributive,
 .e., ‹Inf› and ‹Sup› distribute. See 🍋‹‹Section~10.23› in "DaveyPriestley:2002"›.

 ›

lemma closed_complete_distrib_lattice_axiomI':
  assumes "∀A∈A. ∀x∈A. x ∈ closed"
  shows "(⊓X∈A. ⊔X ⊔ cl ⊥)
           ≤ ⊔(Inf ` {f ` A |f. (∀X⊆closed. f X ∈ closed) ∧ (∀Y ∈ A. f Y ∈ Y)}) ⊔ cl ⊥"
proof -
  from assms
  have "∃f'. f ` A = f' ` A ∧ (∀X⊆closed. f' X ∈ closed) ∧ (∀Y∈A. f' Y ∈ Y)"
    if "∀Y∈A. f Y ∈ Y" for f
    using that by (fastforce intro!: exI[where x="λx. if f x ∈ closed then f x else cl ⊥"])
  then show ?thesis
    by (clarsimp simp: Inf_Sup Sup_le_iff simp flip: INF_sup intro!: le_supI1 Sup_upper)
qed

lemma closed_complete_distrib_lattice_axiomI[intro]:
  assumes "∀A∈A. ∀x∈A. x ∈ closed"
  shows "(⊓X∈A. ⊔X ⊔ cl ⊥)
           ≤ ⊔(Inf ` {B. (∃f. (∀x. (∀x∈x. x ∈ closed) ⟶ f x ∈ closed)
                         ∧ B = f ` A ∧ (∀Y∈A. f Y ∈ Y)) ∧ (∀x∈B. x ∈ closed)})
               ⊔ cl ⊥"
by (rule order.trans[OF closed_complete_distrib_lattice_axiomI'[OF assms]])
   (use assms in ‹clarsimp simp: Sup_le_iff ac_simps›; fast intro!: exI imageI Sup_upper le_supI2)

lemma closed_strict_complete_distrib_lattice_axiomI[intro]:
  assumes "cl ⊥ = ⊥"
  assumes "∀A∈A. ∀x∈A. x ∈ closed"
  shows "(⊓X∈A. ⊔X)
           ≤ ⊔(Inf ` {x. (∃f. (∀x. (∀x∈x. x ∈ closed) ⟶ f x ∈ closed)
                         ∧ x = f ` A ∧ (∀Y∈A. f Y ∈ Y)) ∧ (∀x∈x. x ∈ closed)})"
using closed_complete_distrib_lattice_axiomI[simplified assms(1), simplified, OF assms(2)] .

end


subsection‹ Closures over powersets\label{sec:closures-powersets} ›

locale closure_powerset =
  closure_complete_lattice_class cl for cl :: "'a set ==> 'a set"
begin

lemmas expansive' = subsetD[OF expansive]

lemma closedI[intro]:
  assumes "∧x. x ∈ cl X ==> x ∈ X"
  shows "X ∈ closed"
unfolding closed_def using assms by blast

lemma closedE:
  assumes "x ∈ cl Y"
  assumes "Y ∈ closed"
  shows "x ∈ Y"
using assms closed_def by auto

lemma cl_mono:
  assumes "x ∈ cl X"
  assumes "X ⊆ Y"
  shows "x ∈ cl Y"
using assms by (rule subsetD[OF monotoneD[OF monotone_cl], rotated])

lemma cl_bind_le:
  shows "X 🍋 cl ∘ f ≤ cl (X 🍋 f)"
by (metis bind_UNION bind_image Sup_cl_le)

lemma pointwise_distributive_iff:
  shows "(∀X. cl (∪X) = ∪(cl ` X) ∪ cl {}) ⟷ (∀X. cl X = (∪x∈X. cl {x}) ∪ cl {})" (is "?lhs ⟷ ?rhs")
proof(rule iffI)
  show "?lhs ==> ?rhs" by (metis UN_singleton image_image)
next
  assume ?rhs
  note distributive = ‹?rhs›[rule_format]
  have cl_union: "cl (X ∪ Y) = cl X ∪ cl Y" (is "?lhs1 = ?rhs1") for X Y
  proof(rule antisym[OF _ sup_cl_le])
    from cl expansive' show "?lhs1 ⊆ ?rhs1" by (subst distributive) auto
  qed
  have cl_insert: "cl (insert x X) = cl {x} ∪ cl X" for x X
    by (metis cl_union insert_is_Un)
  show ?lhs
  proof(intro allI antisym)
    show "cl (∪ X) ⊆ ∪ (cl ` X) ∪ cl {}" for X
      by (subst distributive) (clarsimp; metis UnCI cl_insert insert_Diff)
  qed (simp add: cl_bot_least Sup_cl_le)
qed

lemma Sup_prime_on_singleton:
  shows "Sup_prime_on closed (cl {x})"
unfolding Sup_prime_on_def by (meson UnionE expansive' insert_subsetI least bot_least singletonI subsetD)

end

locale closure_powerset_algebraic =
  closure_powerset
+ closure_complete_lattice_algebraic_class

locale closure_powerset_distributive =
  closure_powerset
+ closure_complete_distrib_lattice_distributive_class
begin

lemmas distributive = pointwise_distributive_iff[THEN iffD1, rule_format, OF cl_Sup]

(* don't use \<open>sublocale\<close> as it yields name clashes *)
lemma algebraic_axiom: ―‹ 🍋‹‹Theorem~7.14› in "DaveyPriestley:2002"› ›
  shows "cl x ⊆ ∪ (cl ` ({y. y ⊆ x} ∩ local.compact_points))"
unfolding compact_points_def complete_lattice_class.compact_points_def[symmetric]
by (metis Int_iff algebraic cl_Sup_not_empty complete_lattice_class.compact_pointsI emptyE
          finite.intros(1) mem_Collect_eq order_bot_class.bot_least order.refl)

lemma cl_insert:
  shows "cl (insert x X) = cl {x} ∪ cl X"
by (metis cl_sup insert_is_Un)

lemma cl_UNION:
  shows "cl (∪i∈I. f i) = (∪i∈I. cl (f i)) ∪ cl {}"
by (auto simp add: cl_Sup SUP_upper)

lemma closed_UNION:
  assumes "∧i. i ∈ I ==> f i ∈ closed"
  shows "(∪i∈I. f i) ∪ cl {} ∈ closed"
using assms closed_def by (auto simp: cl_Sup cl_sup)

lemma sort_of_inverse: ― ‹ 🍋‹‹Proposition~2.5› in "PfaltzSlapal:2013"› ›
  assumes "y ∈ cl X - cl {}"
  shows "∃x∈X. y ∈ cl {x}"
using assms by (subst (asm) distributive) blast

lemma cl_diff_le:
  shows "cl x - cl y ⊆ cl (x - y)"
by (metis Diff_subset_conv Un_Diff_cancel Un_upper2 cl_sup)

lemma cl_bind:
  shows "cl (X 🍋 f) = (X 🍋 cl ∘ f) ∪ cl {}"
by (simp add: bind_UNION cl_Sup)

lemma sup_irreducible_on_singleton:
  shows "sup_irreducible_on closed (cl {a})"
by (rule sup_irreducible_onI)
   (metis Un_iff sup_bot.right_neutral expansive insert_subset least antisym local.sup.commute sup_ge2)

end


subsection‹ Matroids and antimatroids\label{sec:closures-matroids} ›

text‹

  🪙‹exchange› axiom characterises 🪙‹matroids› (see, for instance,
 S\ref{sec:galois-concrete}), while the 🪙‹anti-exchange› axiom characterises
 {emph ‹antimatroids›} (see e.g. \S\ref{sec:closures-downwards}).

 :
 ▪ 🍋‹"PfaltzSlapal:2013"› provide an overview of these concepts
 ▪ 🪙‹https://en.wikipedia.org/wiki/Antimatroid›

 ›

definition anti_exchange :: "('a set ==> 'a set) ==> bool" where
  "anti_exchange cl ⟷ (∀X x y. x ≠ y ∧ y ∈ cl (insert x X) - cl X ⟶ x ∉ cl (insert y X) - cl X)"

definition exchange :: "('a set ==> 'a set) ==> bool" where
  "exchange cl ⟷ (∀X x y. y ∈ cl (insert x X) - cl X ⟶ x ∈ cl (insert y X) - cl X)"

lemmas anti_exchangeI = iffD2[OF anti_exchange_def, rule_format]
lemmas exchangeI = iffD2[OF exchange_def, rule_format]

lemma anti_exchangeD:
  assumes "y ∈ cl (insert x X) - cl X"
  assumes "x ≠ y"
  assumes "anti_exchange cl"
  shows "x ∉ cl (insert y X) - cl X"
using assms unfolding anti_exchange_def by blast

lemma exchange_Image: ―‹ Some matroids arise from equivalence relations. Note ‹sym r ∧ trans r ⟶ Refl r› ›
  shows "exchange (Image r) ⟷ sym r ∧ trans r"
by (auto 6 0 simp: exchange_def sym_def intro!: transI elim: transE)

locale closure_powerset_distributive_exchange =
  closure_powerset_distributive
+ assumes exchange: "exchange cl"
begin

lemma exchange_exchange:
  assumes "x ∈ cl {y}"
  assumes "x ∉ cl {}"
  shows "y ∈ cl {x}"
using assms exchange unfolding exchange_def by blast

lemma exchange_closed_inter:
  assumes "Q ∈ closed"
  shows "cl P ∩ Q = cl (P ∩ Q)" (is "?lhs = ?rhs")
    and "Q ∩ cl P = cl (P ∩ Q)" (is ?thesis1)
proof -
  show "?lhs = ?rhs"
  proof(rule antisym)
    have "((∪x∈P. cl {x}) ∪ cl {}) ∩ Q ⊆ (∪x∈P ∩ cl Q. cl {x}) ∪ cl {}"
      by clarsimp (metis IntI UnCI cl_insert exchange_exchange mk_disjoint_insert)
    then show "?lhs ⊆ ?rhs"
      by (simp flip: distributive closed_conv[OF assms])
    from assms show "?rhs ⊆ ?lhs"
      using cl_inf_le closed_conv by blast
  qed
  then show ?thesis1 by blast
qed

lemma exchange_both_closed_inter:
  assumes "P ∈ closed"
  assumes "Q ∈ closed"
  shows "cl (P ∩ Q) = P ∩ Q"
using assms closed_conv closed_inf by force

end

lemma anti_exchange_Image: ―‹ when ‹r› is asymmetric on distinct points ›
  shows "anti_exchange (Image r) ⟷ (∀x y. x ≠ y ∧ (x, y) ∈ r ⟶ (y, x) ∉ r)"
by (auto simp: anti_exchange_def)

locale closure_powerset_distributive_anti_exchange =
  closure_powerset_distributive
+ assumes anti_exchange: "anti_exchange cl"


subsection‹ Composition \label{sec:closures-composition} ›

text‹

  under which composing two closures yields a closure.
  also 🍋‹"PfaltzSlapal:2013"›.

 ›

lemma closure_comp:
  assumes "closure lesseqa lessa cl₁"
  assumes "closure lesseqa lessa cl₂"
  assumes "∧X. cl₁ (cl₂ X) = cl₂ (cl₁ X)"
  shows "closure lesseqa lessa (λX. cl₁ (cl₂ X))"
using assms by (clarsimp simp: closure_def closure_axioms_def) metis

lemma closure_complete_lattice_comp:
  assumes "closure_complete_lattice Infa Supa infa lesseqa lessa supa bota topa cl₁"
  assumes "closure_complete_lattice Infa Supa infa lesseqa lessa supa bota topa cl₂"
  assumes "∧X. cl₁ (cl₂ X) = cl₂ (cl₁ X)"
  shows "closure_complete_lattice Infa Supa infa lesseqa lessa supa bota topa (λX. cl₁ (cl₂ X))"
using assms(1)[unfolded closure_complete_lattice_def]
      closure_comp[OF closure_complete_lattice.axioms(2)[OF assms(1)]
      closure_complete_lattice.axioms(2)[OF assms(2)]]
      assms(3)
by (blast intro: closure_complete_lattice.intro)

lemma closure_powerset_comp:
  assumes "closure_powerset cl₁"
  assumes "closure_powerset cl₂"
  assumes "∧X. cl₁ (cl₂ X) = cl₂ (cl₁ X)"
  shows "closure_powerset (λX. cl₁ (cl₂ X))"
using assms by (simp add: closure_complete_lattice_class_def closure_complete_lattice_comp closure_powerset_def)

lemma closure_powerset_distributive_comp:
  assumes "closure_powerset_distributive cl₁"
  assumes "closure_powerset_distributive cl₂"
  assumes "∧X. cl₁ (cl₂ X) = cl₂ (cl₁ X)"
  shows "closure_powerset_distributive (λX. cl₁ (cl₂ X))"
proof -
  have "cl₁ (cl₂ (∪ X)) ⊆ (∪X∈X. cl₁ (cl₂ X)) ∪ cl₁ (cl₂ {})" for X
    apply (subst (1 2 3) closure_powerset_distributive.distributive[OF assms(1)])
    apply (subst (1 2 3) closure_powerset_distributive.distributive[OF assms(2)])
    apply fast
    done
  moreover
  from assms have "closure_axioms (⊆) (λX. cl₁ (cl₂ X))"
    by (metis closure_powerset_distributive_def closure_complete_lattice_class_def closure_def
              closure_powerset.axioms closure_powerset_comp  closure_complete_lattice.axioms(2))
  ultimately show ?thesis
    by (intro_locales; blast intro: closure_complete_lattice_distributive_axioms.intro)
qed


subsection‹ Path independence ›

text‹

 🍋‹‹Prop 1.1› in "PfaltzSlapal:2013"›: ``an expansive operator is a closure operator iff it
  path independent.''

 :
 ▪ 🍋‹$AFP/Stable_Matching/Choice_Functions.thy›

 ›

context semilattice_sup
begin

definition path_independent :: "('a ==> 'a) ==> bool" where
  "path_independent f ⟷ (∀x y. f (x ⊔ y) = f (f x ⊔ f y))"

lemma cl_path_independent:
  shows "closure (≤) (<) cl ⟷ path_independent cl ∧ (∀x. x ≤ cl x)" (is "?lhs ⟷ ?rhs")
proof(rule iffI)
  show "?lhs ==> ?rhs"
    by (auto 5 0 simp: closure_def closure_axioms_def path_independent_def order.eq_iff
                 elim: le_supE)
  show "?rhs ==> ?lhs"
    by unfold_locales (metis path_independent_def le_sup_iff sup.absorb_iff2 sup.idem)
qed

end


subsection‹ Some closures ›

interpretation id_cl: closure_powerset_distributive id
by standard auto


subsubsection‹ Reflexive, symmetric and transitive closures ›

text‹

  reflexive closure const‹reflcl› is very well behaved. Note the new bottom is @{const ‹Id›}.
  reflexive transitive closure @{const ‹rtrancl›} and transitive closure @{const ‹trancl›} are clearly not distributive.

 const‹rtrancl› is neither matroidal nor antimatroidal.

 ›

interpretation reflcl_cl: closure_powerset_distributive_exchange reflcl
by standard (auto simp: exchange_def)

interpretation symcl_cl: closure_powerset_distributive_exchange "λX. X ∪ X^-1"
by standard (auto simp: exchange_def)

interpretation trancl_cl: closure_powerset trancl
by standard (metis r_into_trancl' subsetI trancl_id trancl_mono trans_trancl)

interpretation rtrancl_cl: closure_powerset rtrancl
by standard (use rtrancl_subset_rtrancl in blast)

lemma rtrancl_closed_Id:
  shows "Id ∈ rtrancl_cl.closed"
using rtrancl_cl.idempotent rtrancl_empty by fastforce

lemma rtrancl_closed_reflcl_closed:
  shows "rtrancl_cl.closed ⊆ reflcl_cl.closed"
using rtrancl_cl.closed_conv by fast


subsubsection‹ Relation image ›

lemma idempotent_Image:
  assumes "r ⊆ Y × Y"
  assumes "refl_on Y r"
  assumes "trans r"
  assumes "X ⊆ Y"
  shows "r `` r `` X = r `` X"
  using assms
  by (auto elim: transE intro: refl_onD refl_onD)

lemmas distributive_Image = Image_eq_UN

lemma closure_powerset_distributive_ImageI:
  assumes "cl = Image r"
  assumes "refl r"
  assumes "trans r"
  shows "closure_powerset_distributive cl"
proof -
  have "closure_axioms (⊆) cl"
    unfolding order.closure_axioms_alt_def
  proof (intro conjI)
    show "∀x. x ⊆ cl x"
      unfolding ‹cl = Image r›
      using ‹refl r›
      by (metis subset_refl Image_Id refl_alt_def[of r] Image_mono[of Id r])
  next
    show "mono cl"
      unfolding ‹cl = Image r›
      using mono_Image .
  next
    show "∀x. cl (cl x) = cl x"
      unfolding ‹cl = Image r›
      using ‹refl r› ‹trans r›
      by (metis top_greatest top_greatest[of r] UNIV_Times_UNIV idempotent_Image[of r UNIV])
  qed
  with ‹cl = Image r› show ?thesis
    by - (intro_locales; auto simp: closure_complete_lattice_distributive_axioms_def)
qed

lemma closure_powerset_distributive_exchange_ImageI:
  assumes "cl = Image r"
  assumes "equiv UNIV r" ―‹ symmetric, transitive and universal domain ›
  shows "closure_powerset_distributive_exchange cl"
using closure_powerset_distributive_ImageI[OF assms(1)] exchange_Image[of r] assms
unfolding closure_powerset_distributive_exchange_def closure_powerset_distributive_exchange_axioms_def
by (metis equivE)

interpretation Image_rtrancl: closure_powerset_distributive "Image (r^*)"
by (rule closure_powerset_distributive_ImageI) auto


subsubsection‹ Kleene closure\label{sec:closures-kleene} ›

text‹

  define Kleene closure in the traditional way with respect to some
  that our various lattices satisfy. As trace models are not
  to validate ‹x ∙ ⊥ = ⊥›
 🍋‹‹Axiom~13› in "Kozen:1994"›, we
  reuse existing developments of Kleene Algebra (and Concurrent
  Algebra
 🍋‹"HoareMoellerStruthWehrman:2011"›). In general
  is not distributive.

 ›

locale weak_kleene =
  fixes unit :: "'a::complete_lattice" (‹ε›)
  fixes comp :: "'a ==> 'a ==> 'a" (infixl ‹∙› 60)
  assumes comp_assoc: "(x ∙ y) ∙ z = x ∙ (y ∙ z)"
  assumes weak_comp_unitL: "ε ≤ x ==> ε ∙ x = x"
  assumes comp_unitR: "x ∙ ε = x"
  assumes comp_supL: "(x ⊔ y) ∙ z = (x ∙ z) ⊔ (y ∙ z)"
  assumes comp_supR: "x ∙ (y ⊔ z) = (x ∙ y) ⊔ (x ∙ z)"
  assumes mcont_compL: "mcont Sup (≤) Sup (≤) (λx. x ∙ y)"
  assumes mcont_compR: "mcont Sup (≤) Sup (≤) (λy. x ∙ y)"
  assumes comp_botL: "⊥ ∙ x = ⊥"
begin

lemma mcont2mcont_comp:
  assumes "mcont Supa orda Sup (≤) f"
  assumes "mcont Supa orda Sup (≤) g"
  shows "mcont Supa orda Sup (≤) (λx. f x ∙ g x)"
by (simp add: ccpo.mcont2mcont'[OF complete_lattice_ccpo mcont_compL _ assms(1)]
              ccpo.mcont2mcont'[OF complete_lattice_ccpo mcont_compR _ assms(2)])

lemma mono2mono_comp:
  assumes "monotone orda (≤) f"
  assumes "monotone orda (≤) g"
  shows "monotone orda (≤) (λx. f x ∙ g x)"
using mcont_mono[OF mcont_compL] mcont_mono[OF mcont_compR] assms
by (clarsimp simp: monotone_def) (meson order.trans)

context
  notes mcont2mcont_comp[cont_intro]
  notes mono2mono_comp[cont_intro, partial_function_mono]
  notes st_monotone[OF mcont_mono[OF mcont_compL], strg]
  notes st_monotone[OF mcont_mono[OF mcont_compR], strg]
begin

context
  notes [[function_internals]] ―‹ Exposes the induction rules we need ›
begin

partial_function (lfp) star :: "'a ==> 'a" where
  "star x = (x ∙ star x) ⊔ ε"

partial_function (lfp) rev_star :: "'a ==> 'a" where
  "rev_star x = (rev_star x ∙ x) ⊔ ε"

end

lemmas parallel_star_induct_1_1 =
  parallel_fixp_induct_1_1[OF
    complete_lattice_partial_function_definitions complete_lattice_partial_function_definitions
    star.mono star.mono star_def star_def]

lemma star_bot:
  shows "star ⊥ = ε"
by (subst star.simps) (simp add: comp_botL)

lemma epsilon_star_le:
  shows "ε ≤ star P"
by (subst star.simps) simp

lemma monotone_star:
  shows "mono star"
proof(rule monotoneI)
  fix x y :: "'a"
  assume "x ≤ y" show "star x ≤ star y"
  proof(induct rule: star.fixp_induct[case_names adm bot step])
    case (step R) show ?case
      apply (strengthen ord_to_strengthen(1)[OF ‹x ≤ y›])
      apply (strengthen ord_to_strengthen(1)[OF step])
      apply (rule order.refl)
      done
  qed simp_all
qed

lemma expansive_star:
  shows "x ≤ star x"
by (subst star.simps, subst star.simps)
   (simp add: comp_supL comp_supR comp_unitR le_supI1 flip: sup.assoc)

lemma star_comp_star:
  shows "star x ∙ star x = star x" (is "?lhs = ?rhs")
proof(rule antisym)
  show "?lhs ≤ ?rhs"
  proof(induct rule: star.fixp_induct[where P="λR. R x ∙ star x ≤ star x", case_names adm bot step])
    case (step R) show ?case
      apply (simp add: comp_supL weak_comp_unitL[OF epsilon_star_le] comp_assoc)
      apply (strengthen ord_to_strengthen(1)[OF step])
      apply (subst (2) star.simps)
      apply simp
      done
  qed (simp_all add: comp_botL)
  show "?rhs ≤ ?lhs"
    by (strengthen ord_to_strengthen(2)[OF epsilon_star_le])
       (simp add: weak_comp_unitL[OF epsilon_star_le])
qed

lemma idempotent_star:
  shows "star (star x) = star x" (is "?lhs = ?rhs")
proof(rule antisym)
  show "?lhs ≤ ?rhs"
  proof(induct rule: star.fixp_induct[where P="λR. R (star x) ≤ ?rhs", case_names adm bot step])
  next
    case (step R) then show ?case
      by (metis comp_supR epsilon_star_le le_iff_sup le_sup_iff star_comp_star)
  qed simp_all
  show "?rhs ≤ ?lhs"
    by (simp add: expansive_star)
qed

interpretation star: closure_complete_lattice_class star
by standard (metis order.trans expansive_star idempotent_star monotoneD[OF monotone_star])

lemma star_epsilon:
  shows "star ε = ε"
by (metis idempotent_star star_bot)

lemma epsilon_rev_star_le:
  shows "ε ≤ rev_star P"
by (subst rev_star.simps) simp

lemma rev_star_comp_rev_star:
  shows "rev_star x ∙ rev_star x = rev_star x" (is "?lhs = ?rhs")
proof(rule antisym)
  show "?lhs ≤ ?rhs"
  proof(induct rule: rev_star.fixp_induct[where P="λR. rev_star x ∙ R x ≤ rev_star x", case_names adm bot step])
    case bot show ?case
      by (subst (2) rev_star.simps) (simp add: le_supI1 mcont_monoD[OF mcont_compR])
  next
    case (step R) then show ?case
      by (simp add: comp_supR epsilon_rev_star_le comp_unitR flip: comp_assoc)
         (metis comp_supL le_iff_sup le_supI1 rev_star.simps)
  qed simp
  show "?rhs ≤ ?lhs"
    by (metis comp_supR comp_unitR epsilon_rev_star_le le_iff_sup)
qed

lemma star_rev_star:
  shows "star = rev_star" (is "?lhs = ?rhs")
proof(intro fun_eqI antisym)
  show "?lhs P ≤ ?rhs P" for P
  proof(induct rule: star.fixp_induct[case_names adm bot step])
    case (step R)
    have expansive: "x ≤ rev_star x" for x
      apply (subst rev_star.simps)
      apply (subst rev_star.simps)
      apply (simp add: comp_supL sup_assoc)
      apply (metis comp_supR comp_unitR sup_ge2 le_supI2 sup_commute weak_comp_unitL)
      done
    show ?case
      by (strengthen ord_to_strengthen(1)[OF step])
         (metis comp_supL epsilon_rev_star_le expansive rev_star_comp_rev_star le_sup_iff sup.absorb_iff2)
  qed simp_all
  show "?rhs P ≤ ?lhs P" for P
  proof(induct rule: rev_star.fixp_induct[case_names adm bot step])
    case (step R) show ?case
      by (strengthen ord_to_strengthen(1)[OF step])
         (metis epsilon_star_le expansive_star mcont_monoD[OF mcont_compR] le_supI star_comp_star)
  qed simp_all
qed

lemmas star_fixp_rev_induct = rev_star.fixp_induct[folded star_rev_star]

interpretation rev_star: closure_complete_lattice_class rev_star
by (rule star.closure_complete_lattice_class_axioms[unfolded star_rev_star])

lemma rev_star_bot:
  shows "rev_star ⊥ = ε"
by (simp add: star_bot flip: star_rev_star)

lemma rev_star_epsilon:
  shows "rev_star ε = ε"
by (simp add: star_epsilon flip: star_rev_star)

lemmas star_unfoldL = star.simps

lemma star_unfoldR:
  shows "star x = (star x ∙ x) ⊔ ε"
by (subst (1 2) star_rev_star) (simp flip: rev_star.simps)

lemmas rev_star_unfoldR = rev_star.simps

lemma rev_star_unfoldL:
  shows "rev_star x = (x ∙ rev_star x) ⊔ ε"
by (simp flip: star_rev_star star_unfoldL)

lemma fold_starL:
  shows "x ∙ star x ≤ star x"
by (subst (2) star.simps) simp

lemma fold_starR:
  shows "star x ∙ x ≤ star x"
by (metis inf_sup_ord(3) star_unfoldR)

lemma fold_rev_starL:
  shows "x ∙ rev_star x ≤ rev_star x"
by (simp add: fold_starL flip: star_rev_star)

lemma fold_rev_starR:
  shows "rev_star x ∙ x ≤ rev_star x"
by (simp add: fold_starR flip: star_rev_star)

declare star.strengthen_cl[strg] rev_star.strengthen_cl[strg]

end

end

locale kleene = weak_kleene +
  assumes comp_unitL: "ε ∙ x = x" ―‹ satisfied by ‹('a, 's, 'v) prog› but not ‹('a, 's, 'v) spec› ›
(*<*)

end
(*>*)