# Theory topo_interior_algebra

theory topo_interior_algebra
imports topo_operators_basic
begin
nitpick_params[assms=true, user_axioms=true, show_all, expect=genuine, format=3] (*default Nitpick settings*)

section ‹Interior algebra›
text‹\noindent{We define a topological Boolean algebra taking the interior operator as primitive and verify some properties.}›

text‹\noindent{Declares a primitive (unconstrained) interior operation and defines others from it.}›
consts ℐ::"σ⇒σ"
abbreviation "𝒞 ≡ ℐ⇧d" ―‹ closure ›
abbreviation "ℬ ≡ ℬ⇩I ℐ" ―‹ border ›
abbreviation "ℱ ≡ ℱ⇩I ℐ" ―‹ frontier ›

subsection ‹Basic properties›

text‹\noindent{Verifies minimal conditions under which operators resulting from conversion functions coincide.}›
lemma ICdual:  "ℐ ❙≡ 𝒞⇧d" using dual_symm equal_op_def by auto
lemma IB_rel: "Int_2 ℐ ⟹ ℐ ❙≡ ℐ⇩B ℬ" by (smt Br_int_def Int_br_def dEXP_def diff_def equal_op_def)
lemma IF_rel: "Int_2 ℐ ⟹ ℐ ❙≡ ℐ⇩F ℱ" using EXP_def EXP_dual2 Fr_int_def IB_rel Int_br_def Int_fr_def compl_def diff_def equal_op_def meet_def by fastforce
lemma CB_rel: "Int_2 ℐ ⟹ 𝒞 ❙≡ 𝒞⇩B ℬ" using Br_int_def Cl_br_def EXP_def EXP_dual2 compl_def diff_def dual_def equal_op_def join_def by fastforce
lemma CF_rel: "Int_2 ℐ ⟹ 𝒞 ❙≡ 𝒞⇩F ℱ" by (smt Cl_fr_def EXP_def EXP_dual2 Fr_int_def compl_def dEXP_def equal_op_def join_def meet_def)
lemma BC_rel: "ℬ ❙≡ ℬ⇩C 𝒞" by (simp add: BI_BC_rel equal_op_def)
lemma BF_rel: "Int_2 ℐ ⟹ ℬ ❙≡ ℬ⇩F ℱ" by (smt Br_fr_def Br_int_def IF_rel Int_fr_def diff_def equal_op_def meet_def)
lemma FC_rel: "ℱ ❙≡ ℱ⇩C 𝒞" using Fr_cl_def Fr_int_def compl_def dual_def equal_op_def meet_def by fastforce
lemma FB_rel: "Int_2 ℐ ⟹ ℱ ❙≡ ℱ⇩B ℬ" unfolding Fr_br_def by (smt BC_rel Br_cl_def CB_rel Cl_br_def FC_rel Fr_cl_def equal_op_def join_def meet_def)

text‹\noindent{Fixed-point and other operators are interestingly related.}›
lemma fp1: "Int_2 ℐ ⟹ ℐ⇧f⇧p ❙≡ ℬ⇧c" by (smt Br_int_def IB_rel Int_br_def compl_def diff_def dimp_def equal_op_def)
lemma fp2: "Int_2 ℐ ⟹ ℬ⇧f⇧p ❙≡ ℐ⇧c" using fp1 unfolding compl_def dimp_def equal_op_def by smt
lemma fp3: "Int_2 ℐ ⟹ 𝒞⇧f⇧p ❙≡ ℬ⇧d" by (metis (no_types) dual_comp eq_ext' fp2 ofp_c ofp_d ofp_invol)
lemma fp4: "Int_2 ℐ ⟹ (ℬ⇧d)⇧f⇧p ❙≡ 𝒞" by (smt dimp_def equal_op_def fp3)
lemma fp5: "Int_2 ℐ ⟹ ℱ⇧f⇧p ❙≡ ℬ ❙⊔ (𝒞⇧c)" by (smt BC_rel Br_cl_def CF_rel Cl_fr_def FI2 Fr_2_def compl_def dimp_def eq_ext' equal_op_def join_def meet_def)

text‹\noindent{Define some fixed-point predicates and prove some properties.}›
abbreviation openset ("Op") where "Op A ≡ fp ℐ A"
abbreviation closedset ("Cl") where "Cl A ≡ fp 𝒞 A"
abbreviation borderset ("Br") where "Br A ≡ fp ℬ A"
abbreviation frontierset ("Fr") where "Fr A ≡ fp ℱ A"

lemma Int_Open: "Int_4 ℐ ⟹ ∀A. Op(ℐ A)" by (simp add: IDEM_def)
lemma Cl_Closed: "Int_4 ℐ ⟹ ∀A. Cl(𝒞 A)" using IC4 IDEM_def by blast
lemma Br_Border: "Int_1a ℐ ⟹ ∀A. Br(ℬ A)" by (metis Br_int_def MONO_MULTa MONO_def diff_def)
text‹\noindent{In contrast, there is no analogous fixed-point result for frontier:}›
lemma "ℑ ℐ ⟹ ∀A. Fr(ℱ A)" nitpick oops (*counterexample even if assuming all interior conditions*)

lemma OpCldual: "∀A. Cl A ⟷ Op(❙─A)" by (simp add: fp_d)
lemma ClOpdual: "∀A. Op A ⟷ Cl(❙─A)" by (simp add: compl_def dual_def)
lemma Fr_ClBr: "Int_2 ℐ ⟹ ∀A. Fr(A) = (Cl(A) ∧ Br(A))" using BF_rel Br_fr_def CF_rel Cl_fr_def eq_ext' join_def meet_def by fastforce
lemma Cl_F: "Int_1a ℐ ⟹ Int_2 ℐ ⟹ Int_4 ℐ ⟹ ∀A. Cl(ℱ A)" by (metis CF_rel Cl_fr_def FI4 Fr_4_def eq_ext' join_def)

end