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 ℬ fp c" using Br_5b_def Int_br_def PB5b unfolding equal_op_def conn by fastforce
lemma fp2: "Br_1 ℬ fp c" using Br_5b_def Int_br_def PB5b conn equal_op_def by fastforce 
lemma fp3: "Br_1 ℬ  𝒞fp d" using Br_5c_def Cl_br_def PB5c dual_def unfolding equal_op_def conn by fastforce
lemma fp4: "Br_1 ℬ  (d)fp  𝒞" by (smt dimp_def equal_op_def fp3)
lemma fp5: "Br_1 ℬ fp  (𝒞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  fpA"
abbreviation closedset ("Cl") where "Cl A  fp 𝒞 A"
abbreviation borderset ("Br") where "Br A  fpA"
abbreviation frontierset ("Fr") where "Fr A  fpA"

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