Theory topo_closure_algebra

theory topo_closure_algebra
  imports topo_operators_basic
begin
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 𝒞 ⟹ ℐ⇧f⇧p ❙≡ ℬ⇧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 𝒞 ⟹ ℬ⇧f⇧p ❙≡ ℐ⇧c" using fp1 by (smt compl_def dimp_def equal_op_def)
lemma fp3: "Cl_2 𝒞 ⟹ 𝒞⇧f⇧p ❙≡ ℬ⇧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)⇧f⇧p ❙≡ 𝒞" by (smt dimp_def equal_op_def fp3)
lemma fp5: "Cl_2 𝒞 ⟹ ℱ⇧f⇧p ❙≡ ℬ ❙⊔ (𝒞⇧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 ≡ 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: "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

end