# Theory topo_border_algebra

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

section ‹Border algebra›
text‹\noindent{We define a border algebra in an analogous fashion to the well-known closure/interior algebras.
We also verify a few interesting properties.}›

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

subsection ‹Basic properties›

text‹\noindent{Verifies minimal conditions under which operators resulting from conversion functions coincide.}›
lemma ICdual:  "ℐ ❙≡ 𝒞⇧d" by (simp add: Cl_br_def Int_br_def dual_def equal_op_def conn)
lemma ICdual': "𝒞 ❙≡ ℐ⇧d"  by (simp add: Cl_br_def Int_br_def dual_def equal_op_def conn)
lemma FI_rel: "Br_1 ℬ ⟹ ℱ ❙≡ ℱ⇩I ℐ" using Fr_br_def Fr_int_def Int_br_def equal_op_def by (smt Br_5b_def PB5b dual_def conn)
lemma IF_rel: "Br_1 ℬ ⟹ ℐ ❙≡ ℐ⇩F ℱ" using Br_5b_def Fr_br_def Int_br_def Int_fr_def PB5b unfolding equal_op_def conn by fastforce
lemma FC_rel: "Br_1 ℬ ⟹ ℱ ❙≡ ℱ⇩C 𝒞" using Br_5b_def Cl_br_def Fr_br_def Fr_cl_def PB5b unfolding equal_op_def conn by fastforce
lemma CF_rel: "Br_1 ℬ ⟹ 𝒞 ❙≡ 𝒞⇩F ℱ" using Br_5b_def Cl_br_def Cl_fr_def Fr_br_def PB5b unfolding equal_op_def conn by fastforce
lemma BI_rel: "Br_1 ℬ ⟹ ℬ ❙≡ ℬ⇩I ℐ" using Br_5b_def Br_int_def Int_br_def PB5b diff_def equal_op_def by fastforce
lemma BC_rel: "Br_1 ℬ ⟹ ℬ ❙≡ ℬ⇩C 𝒞" using BI_BC_rel BI_rel ICdual' eq_ext' by fastforce
lemma BF_rel: "Br_1 ℬ ⟹ ℬ ❙≡ ℬ⇩F ℱ" by (smt BI_rel Br_fr_def Br_int_def IF_rel Int_fr_def diff_def equal_op_def meet_def)

text‹\noindent{Fixed-point and other operators are interestingly related.}›
lemma fp1: "Br_1 ℬ ⟹ ℐ⇧f⇧p ❙≡ ℬ⇧c" using Br_5b_def Int_br_def PB5b unfolding equal_op_def conn by fastforce
lemma fp2: "Br_1 ℬ ⟹ ℬ⇧f⇧p ❙≡ ℐ⇧c" using Br_5b_def Int_br_def PB5b conn equal_op_def by fastforce
lemma fp3: "Br_1 ℬ ⟹ 𝒞⇧f⇧p ❙≡ ℬ⇧d" using Br_5c_def Cl_br_def PB5c dual_def unfolding equal_op_def conn by fastforce
lemma fp4: "Br_1 ℬ ⟹ (ℬ⇧d)⇧f⇧p ❙≡ 𝒞" by (smt dimp_def equal_op_def fp3)
lemma fp5: "Br_1 ℬ ⟹ ℱ⇧f⇧p ❙≡ ℬ ❙⊔ (𝒞⇧c)" by (smt Br_5b_def Cl_br_def Fr_br_def PB5b equal_op_def conn)

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: "Br_1 ℬ ⟹ Br_3 ℬ ⟹ ∀A. Op(ℐ A)" using IB4 IDEM_def by blast
lemma Cl_Closed: "Br_1 ℬ ⟹ Br_3 ℬ ⟹ ∀A. Cl(𝒞 A)" using CB4 IDEM_def by blast
lemma Br_Border: "Br_1 ℬ ⟹ ∀A. Br(ℬ A)" using IDEM_def PB6 by blast
text‹\noindent{In contrast, there is no analogous fixed-point result for frontier:}›
lemma "𝔅 ℬ ⟹ ∀A. Fr(ℱ A)" nitpick oops (*counterexample even if assuming all border conditions*)

lemma OpCldual: "∀A. Cl A ⟷ Op(❙─A)" using Cl_br_def Int_br_def conn by auto
lemma ClOpdual: "∀A. Op A ⟷ Cl(❙─A)" using Cl_br_def Int_br_def conn by auto
lemma Fr_ClBr: "Br_1 ℬ ⟹ ∀A. Fr(A) = (Cl(A) ∧ Br(A))" by (metis BF_rel Br_fr_def CF_rel Cl_fr_def eq_ext' join_def meet_def)
lemma Cl_F: "Br_1 ℬ ⟹ Br_3 ℬ ⟹ ∀A. Cl(ℱ A)" by (metis CF_rel Cl_fr_def FB4 Fr_4_def eq_ext' join_def)

end