Theory topo_interior_algebra

theory topo_interior_algebra
  imports topo_operators_basic
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.}›
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 ℐ fp c" by (smt Br_int_def IB_rel Int_br_def compl_def diff_def dimp_def equal_op_def)
lemma fp2: "Int_2 ℐ fp c" using fp1 unfolding compl_def dimp_def equal_op_def by smt
lemma fp3: "Int_2 ℐ  𝒞fp d" by (metis (no_types) dual_comp eq_ext' fp2 ofp_c ofp_d ofp_invol)
lemma fp4: "Int_2 ℐ  (d)fp  𝒞" by (smt dimp_def equal_op_def fp3)
lemma fp5: "Int_2 ℐ fp  (𝒞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  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: "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)