Theory topo_closure_algebra

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

section ‹Closure algebra›
text‹\noindent{We define a topological Boolean algebra with a primitive closure operator and verify a few properties.}›

text‹\noindent{Declares a primitive (unconstrained) closure operation and defines others from it.}›
consts 𝒞::σ"
abbreviation "  𝒞d" ―‹ interior ›
abbreviation "  C 𝒞" ―‹ border ›
abbreviation "  C 𝒞" ―‹ 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: "Cl_2 𝒞  B ℬ" using Br_cl_def EXP_dual1 Int_br_def compl_def dEXP_def diff_def dual_def equal_op_def meet_def by fastforce
lemma IF_rel: "Cl_2 𝒞  F ℱ" by (smt EXP_def Fr_cl_def Int_fr_def compl_def diff_def dual_def equal_op_def meet_def) 
lemma CB_rel: "Cl_2 𝒞  𝒞  𝒞B ℬ" by (smt Cl_br_def EXP_def IB_rel Int_br_def compl_def diff_def dual_def dual_symm eq_ext' equal_op_def join_def)
lemma CF_rel: "Cl_2 𝒞  𝒞  𝒞F ℱ" by (smt Br_cl_def CB_rel Cl_br_def Cl_fr_def Fr_cl_def equal_op_def join_def meet_def)
lemma BI_rel: "ℬ  I ℐ" using BI_BC_rel dual_symm equal_op_def by metis
lemma BF_rel: "Cl_2 𝒞  F ℱ" by (smt Br_cl_def Br_fr_def EXP_def Fr_cl_def equal_op_def meet_def)
lemma FI_rel: "ℱ  I ℐ" by (metis FI2 Fr_2_def Fr_cl_def Fr_int_def ICdual' dual_def eq_ext' equal_op_def)
lemma FB_rel: "Cl_2 𝒞  B ℬ" by (smt BF_rel Br_fr_def CB_rel Cl_br_def Fr_br_def Fr_cl_def equal_op_def join_def meet_def)

text‹\noindent{Fixed-point and other operators are interestingly related.}›
lemma fp1: "Cl_2 𝒞 fp c" by (smt BI_rel Br_int_def IB_rel Int_br_def compl_def diff_def dimp_def equal_op_def)
lemma fp2: "Cl_2 𝒞 fp c" using fp1 by (smt compl_def dimp_def equal_op_def)
lemma fp3: "Cl_2 𝒞  𝒞fp d" by (smt BI_rel Br_int_def CB_rel Cl_br_def compl_def diff_def dimp_def dual_def equal_op_def join_def)
lemma fp4: "Cl_2 𝒞  (d)fp  𝒞" by (smt dimp_def equal_op_def fp3)
lemma fp5: "Cl_2 𝒞 fp  (𝒞c)" by (smt Br_cl_def CF_rel Cl_fr_def FC2 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: "Cl_4 𝒞  A. Op(A)" using IC4 IDEM_def by blast
lemma Cl_Closed: "Cl_4 𝒞  A. Cl(𝒞 A)" by (simp add: IDEM_def)
lemma Br_Border: "Cl_1b 𝒞  A. Br(A)" by (metis BI_rel Br_cl_def Br_int_def CI1b MULT_a_def diff_def eq_ext' meet_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 closure conditions*)

lemma OpCldual: "A. Cl A  Op(A)" by (simp add: compl_def dual_def)
lemma ClOpdual: "A. Op A  Cl(A)" by (simp add: fp_d)
lemma Fr_ClBr: "Cl_2 𝒞  A. Fr(A) = (Cl(A)  Br(A))" using BF_rel by (metis Br_fr_def CF_rel Cl_fr_def eq_ext' join_def meet_def)
lemma Cl_F: "Cl_1b 𝒞  Cl_2 𝒞  Cl_4 𝒞  A. Cl(A)" using Cl_8_def Fr_cl_def PC8 by auto