# Theory topo_frontier_algebra

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

section βΉFrontier AlgebraβΊ

textβΉ\noindent{The closure of a set A (@{text "π(A)"}) can be seen as the set A augmented by (i) its boundary points,
or (ii) its accumulation/limit points. In this section we explore the first variant by drawing on the notion
of a frontier algebra, defined in an analogous fashion as the well-known closure and interior algebras.}βΊ

textβΉ\noindent{Declares a primitive (unconstrained) frontier (aka. boundary) operation and defines others from it.}βΊ
consts β±::"ΟβΟ"
abbreviation "β β‘ ββ©F β±" ββΉ interior βΊ
abbreviation "π β‘ πβ©F β±" ββΉ closure βΊ
abbreviation "β¬ β‘ β¬β©F β±" ββΉ border βΊ

subsection βΉBasic propertiesβΊ

textβΉ\noindent{Verifies minimal conditions under which operators resulting from conversion functions coincide.}βΊ
lemma ICdual: "Fr_2 β± βΉ β ββ‘ πβ§d" by (simp add: Cl_fr_def Fr_2_def Int_fr_def dual_def equal_op_def conn)
lemma ICdual': "Fr_2 β± βΉ π ββ‘ ββ§d" by (simp add: Cl_fr_def Fr_2_def Int_fr_def dual_def equal_op_def conn)
lemma BI_rel: "β¬ ββ‘ β¬β©I β" using Br_fr_def Br_int_def Int_fr_def unfolding equal_op_def conn by auto
lemma IB_rel: "β ββ‘ ββ©B β¬" using Br_fr_def Int_br_def Int_fr_def unfolding equal_op_def conn by auto
lemma BC_rel: "Fr_2 β± βΉ β¬ ββ‘ β¬β©C π"  using BI_BC_rel BI_rel ICdual' eq_ext' by fastforce
lemma CB_rel: "Fr_2 β± βΉ π ββ‘ πβ©B β¬" using Br_fr_def Cl_br_def Cl_fr_def Fr_2_def unfolding equal_op_def conn by auto
lemma FI_rel: "Fr_2 β± βΉ β± ββ‘ β±β©I β" by (smt Cl_fr_def Fr_int_def ICdual' Int_fr_def compl_def diff_def equal_op_def join_def meet_def)
lemma FC_rel: "Fr_2 β± βΉ β± ββ‘ β±β©C π" by (metis (mono_tags, lifting) FI_rel Fr_2_def Fr_cl_def Fr_int_def ICdual' dual_def eq_ext' equal_op_def)
lemma FB_rel: "Fr_2 β± βΉ β± ββ‘ β±β©B β¬" by (smt Br_fr_def CB_rel Cl_br_def FC_rel 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: "ββ§fβ§p ββ‘ β¬β§c" using Br_fr_def Int_fr_def unfolding equal_op_def conn by auto
lemma fp2: "β¬β§fβ§p ββ‘ ββ§c" using Br_fr_def Int_fr_def unfolding equal_op_def conn by auto
lemma fp3: "Fr_2 β± βΉ πβ§fβ§p ββ‘ β¬β§d" using Br_fr_def Cl_fr_def Fr_2_def dual_def equal_op_def conn by fastforce
lemma fp4: "Fr_2 β± βΉ (β¬β§d)β§fβ§p ββ‘ π" by (smt dimp_def equal_op_def fp3)
lemma fp5: "β±β§fβ§p ββ‘ β¬ ββ (πβ§c)" using Br_fr_def Cl_fr_def unfolding equal_op_def conn by auto

textβΉ\noindent{Different inter-relations (some redundant ones are kept to help the provers).}βΊ
lemma monI: "Fr_1b β± βΉ MONO(β)" by (simp add: IF1a MONO_MULTa)
lemma monC: "Fr_6 β± βΉ MONO(π)" by (simp add: Cl_fr_def Fr_6_def MONO_def conn)
lemma pB1: "βA. β¬ A ββ A ββΌ β A" using Br_fr_def fp1 unfolding conn equal_op_def by metis
lemma pB2: "βA. β¬ A ββ A ββ§ β± A" by (simp add: Br_fr_def)
lemma pB3: "Fr_2 β± βΉ βA. β¬(ββA) ββ ββA ββ§ β± A" by (simp add: Fr_2_def pB2 conn)
lemma pB4: "Fr_2 β± βΉ βA. β¬(ββA) ββ ββA ββ§ π A" using CB_rel Cl_br_def pB3 unfolding conn equal_op_def by metis
lemma pB5: "Fr_1b β± βΉ Fr_2 β± βΉ βA. β¬(π A) ββΌ (β¬ A) ββ¨ β¬(ββA)"  by (smt BC_rel Br_cl_def Cl_fr_def Fr_6_def PF6 equal_op_def conn)
lemma pF1: "βA. β± A ββ π A ββΌ β A"  using Cl_fr_def Int_fr_def conn by auto
lemma pF2: "Fr_2 β± βΉ βA. β± A ββ π A ββ§ π(ββA)" using Cl_fr_def Fr_2_def conn by auto
lemma pF3: "Fr_2 β± βΉ βA. β± A ββ β¬ A ββ¨ β¬(ββA)" using Br_fr_def Fr_2_def conn by auto
lemma pF4: "Fr_1 β± βΉ Fr_2 β± βΉ Fr_4(β±) βΉ βA. β±(β A) ββΌ β± A" by (smt IDEMa_def IF2 IF4 Int_fr_def MONO_def PF1 PF6 PI4 diff_def monC pF1)
lemma pF5: "Fr_1 β± βΉ Fr_2 β± βΉ Fr_4 β± βΉ βA. β±(π A) ββΌ β± A" by (metis Br_fr_def CF4 Cl_fr_def IDEM_def PF1 join_def meet_def pB5 pF3)
lemma pA1: "βA. A ββ β A ββ¨ β¬ A" using Br_fr_def Int_fr_def unfolding conn by auto
lemma pA2: "Fr_2 β± βΉ βA. A ββ π A ββΌ β¬(ββA)" using pB1 dual_def fp3 unfolding equal_op_def conn by smt
lemma pC1: "Fr_2 β± βΉ βA. π A ββ A ββ¨ β¬(ββA)" using Cl_fr_def pB4 conn by auto
lemma pC2: "βA. π A ββ A ββ¨ β± A" using Cl_fr_def by auto
lemma pI1: "βA. β A ββ A ββΌ β¬ A" using pA1 pB1 conn by auto
lemma pI2: "βA. β A ββ A ββΌ β± A" by (simp add: Int_fr_def)

lemma IC_imp: "Fr_1 β± βΉ Fr_2 β± βΉ Fr_3 β± βΉ βA B. β(A ββ B) ββΌ π A ββ π B" proof -
assume fr1: "Fr_1 β±" and fr2: "Fr_2 β±" and fr3: "Fr_3 β±"
{ fix a b
have "(a ββ b) ββ§ ββb ββ ββa = ββ€" unfolding conn by auto
hence "β((a ββ b) ββ§ ββb ββ ββa) ββ β(ββ€)" by simp
hence "β((a ββ b) ββ§ ββb ββ ββa) ββ ββ€" using fr3 IF3 dNOR_def fr2 by auto
moreover have "let A=(a ββ b) ββ§ ββb; B=ββa in β(A ββ B) ββΌ β(A) ββ β(B)" using fr1 IF1 PI7 Int_7_def by metis
ultimately have "β((a ββ b) ββ§ ββb) ββ β(ββa) ββ ββ€" unfolding conn by simp
moreover have "let A=a ββ b; B=ββb in β(A ββ§ B) ββ β(A) ββ§ β(B)" using fr1 IF1 MULT_def by simp
ultimately have "β(a ββ b) ββ§ β(ββb) ββ β(ββa) ββ ββ€" unfolding conn by simp
moreover have "βA. β(ββA) ββ ββπ(A)" using Cl_fr_def Fr_2_def Int_fr_def fr2  unfolding conn by auto
ultimately have "β(a ββ b) ββ§ ββπ(b) ββ ββπ(a) ββ ββ€" unfolding conn by simp
hence "β(a ββ b) ββ§ ββπ(b) ββΌ ββπ(a)" unfolding conn by simp
hence "β(a ββ b) ββ§ π a ββΌ π b" unfolding conn by metis
} thus ?thesis unfolding conn by simp
qed

textβΉ\noindent{Defines 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: "Fr_1a β± βΉ Fr_2 β± βΉ Fr_4 β± βΉ βA. Op(β A)" using IF4 IDEM_def by blast
lemma Cl_Closed: "Fr_1a β± βΉ Fr_2 β± βΉ Fr_4 β± βΉ βA. Cl(π A)" using CF4 IDEM_def by blast
lemma Br_Border: "Fr_1b β± βΉ βA. Br(β¬ A)" using Br_fr_def Fr_1b_def conn by auto
textβΉ\noindent{In contrast, there is no analogous fixed-point result for frontier:}βΊ
lemma "π β± βΉ βA. Fr(β± A)" nitpick oops (*counterexample even if assuming all frontier conditions*)

lemma OpCldual: "Fr_2 β± βΉ βA. Cl A β· Op(ββA)" using Cl_fr_def Fr_2_def Int_fr_def conn by auto
lemma ClOpdual: "Fr_2 β± βΉ βA. Op A β· Cl(ββA)" using ICdual dual_def unfolding equal_op_def conn by auto
lemma Fr_ClBr: "βA. Fr(A) = (Cl(A) β§ Br(A))" using Br_fr_def Cl_fr_def join_def meet_def by auto
lemma Cl_F: "Fr_4 β± βΉ βA. Cl(β± A)" using Cl_fr_def Fr_4_def conn by auto

subsection βΉFurther propertiesβΊ

textβΉ\noindent{The definitions and theorems below are well known in the literature (e.g. @{cite Kuratowski2}).
Here we uncover the minimal conditions under which they hold (taking frontier operation as primitive).}βΊ
lemma Cl_Bzero: "Fr_2 β± βΉ βA. Cl A β· β¬(ββA) ββ ββ₯" using pA2 pC1 unfolding conn by metis
lemma Op_Bzero: "βA. Op A β· (β¬ A) ββ ββ₯" using pB1 pI1 unfolding conn by metis
lemma Br_boundary: "Fr_2 β± βΉ βA. Br(A) β· β A ββ ββ₯" by (metis Br_fr_def Int_fr_def bottom_def diff_def meet_def)
lemma Fr_nowhereDense: "Fr_2 β± βΉ βA. Fr(A) βΆ β(π A) ββ ββ₯" using Fr_ClBr Br_boundary eq_ext by metis
lemma Cl_FB: "βA. Cl A β· β± A ββ β¬ A" using Br_fr_def Cl_fr_def unfolding conn by auto
lemma Op_FB: "Fr_2 β± βΉ βA. Op A β· β± A ββ β¬(ββA)" using Br_fr_def Fr_2_def Int_fr_def unfolding conn by auto
lemma Clopen_Fzero: "βA. Cl A β§ Op A β· β± A ββ ββ₯" using Cl_fr_def Int_fr_def unfolding conn by auto

lemma Int_sup_closed: "Fr_1b β± βΉ supremum_closed (Ξ»A. Op A)" by (smt IF1a Int_fr_def MONO_def MONO_MULTa sup_char conn)
lemma Int_meet_closed: "Fr_1a β± βΉ meet_closed (Ξ»A. Op A)" using Fr_1a_def Int_fr_def unfolding conn by metis
lemma Int_inf_closed: "Fr_inf β± βΉ infimum_closed (Ξ»A. Op A)" by (simp add: fp_IF_inf_closed)
lemma Cl_inf_closed: "Fr_6 β± βΉ infimum_closed (Ξ»A. Cl A)" by (smt Cl_fr_def Fr_6_def infimum_def join_def)
lemma Cl_join_closed: "Fr_1a β± βΉ Fr_2 β± βΉ join_closed (Ξ»A. Cl A)" using ADDI_a_def CF1a CF2 EXP_def unfolding conn by metis
lemma Cl_sup_closed: "Fr_2 β± βΉ Fr_inf β± βΉ supremum_closed (Ξ»A. Cl A)" by (simp add: fp_CF_sup_closed)
lemma Br_inf_closed: "Fr_1b β± βΉ infimum_closed (Ξ»A. Br A)" by (smt BI_rel Br_int_def IF1a MONO_iMULTa MONO_MULTa Ra_restr_all eq_ext' iMULT_a_def inf_char diff_def)
lemma Fr_inf_closed: "Fr_1b β± βΉ Fr_2 β± βΉ infimum_closed (Ξ»A. Fr A)" by (metis (full_types) Br_fr_def Br_inf_closed PF6 Cl_fr_def Cl_inf_closed meet_def join_def)
lemma Br_Fr_join: "Fr_1 β± βΉ Fr_2 β± βΉ Fr_4 β± βΉ βA B. Br A β§ Fr B βΆ Br(A ββ¨ B)" proof -
assume fr1: "Fr_1 β±" and fr2: "Fr_2 β±" and fr4: "Fr_4 β±"
{ fix A B
{ assume bra: "Br A" and frb: "Fr B"
from bra have "β A ββ ββ₯" using Br_boundary fr2 by auto
hence 1: "π(ββA) ββ ββ€" by (metis ICdual bottom_def compl_def dual_def eq_ext' fr2 top_def)
from frb have "β(π B) ββ ββ₯" by (simp add: Fr_nowhereDense fr2)
hence 2: "π(ββ(π B)) ββ ββ€" by (metis ICdual bottom_def compl_def dual_def eq_ext' fr2 top_def)
from fr1 fr2 have "π(ββA) ββΌ π B ββΌ π((ββA) ββΌ B)" using CF1 Cl_6_def PC6 by metis
hence "π(ββA) ββΌ π B ββΌ π(ββ(A ββ¨ B))" unfolding conn by simp
hence "ββ€ ββΌ π B ββΌ π(ββ(A ββ¨ B))" using 1 unfolding conn by simp
hence 3: "ββ(π B) ββΌ π(ββ(A ββ¨ B))" unfolding conn by simp
from fr1 fr2 fr4 have 4: "let M=ββ(π B); N=ββ(A ββ¨ B) in  M ββΌ π N βΆ π M ββΌ π N" using PC9 CF4 Cl_9_def PF1 CF1b by fastforce
from 3 4 have "π(ββ(π B)) ββΌ π(ββ(A ββ¨ B))" by simp
hence "ββ€ ββ π(ββ(A ββ¨ B))" using 2 unfolding top_def by simp
hence "ββ₯ ββ β(A ββ¨ B)" using fr2 ICdual dual_def eq_ext' conn by metis
hence "Br (A ββ¨ B)" using fr2 Br_boundary by simp
} hence "Br A β§ Fr B βΆ Br (A ββ¨ B)" by simp
} hence "βA B. Br A β§ Fr B βΆ Br (A ββ¨ B)" by simp
thus ?thesis by simp
qed
lemma Fr_join_closed: "Fr_1 β± βΉ Fr_2 β± βΉ Fr_4 β± βΉ join_closed (Ξ»A. Fr A)" by (smt Br_Fr_join ADDI_a_def CF1a Cl_fr_def PF1 diff_def join_def meet_def pB2 pF1)

textβΉ\noindent{Introduces a predicate for indicating that two sets are disjoint and proves some properties.}βΊ
abbreviation "Disj A B β‘ A ββ§ B ββ ββ₯"

lemma Disj_comm: "βA B. Disj A B βΆ Disj B A" unfolding conn by fastforce
lemma Disj_IF: "βA. Disj (β A) (β± A)" by (simp add: Int_fr_def conn)
lemma Disj_B: "βA. Disj (β¬ A) (β¬(ββA))" using Br_fr_def unfolding conn by auto
lemma Disj_I: "βA. Disj (β A) (ββA)" by (simp add: Int_fr_def conn)
lemma Disj_BCI: "Fr_2 β± βΉ βA. Disj (β¬(π A)) (β(ββA))" using Br_fr_def Cl_fr_def Fr_2_def Int_fr_def conn by metis
lemma Disj_CBI: "Fr_6 β± βΉ Fr_4 β± βΉ βA. Disj (π(β¬(ββA))) (β(ββA))" by (metis Br_fr_def Cl_F IB_rel Int_br_def MONO_MULTa MULT_a_def eq_ext' monC conn)

textβΉ\noindent{Introduces a predicate for indicating that two sets are separated and proves some properties.}βΊ
definition "Sep A B β‘ Disj (π A) B β§ Disj (π B) A"

lemma Sep_comm: "βA B. Sep A B βΆ Sep B A" by (simp add: Sep_def)
lemma Sep_disj: "βA B. Sep A B βΆ Disj A B" using Cl_fr_def Sep_def conn by fastforce
lemma Sep_I: "Fr_1(β±) βΉ Fr_2(β±) βΉ Fr_4(β±) βΉ βA. Sep (β A) (β (ββA))" using Cl_fr_def pF4 Fr_2_def Int_fr_def unfolding Sep_def conn by metis
lemma Sep_sub: "Fr_6 β±  βΉ βA B C D. Sep A B β§ C ββΌ A β§ D ββΌ B βΆ Sep C D" using MONO_def monC unfolding Sep_def conn by smt
lemma Sep_Cl_diff: "Fr_6 β± βΉ βA B. Cl(A) β§ Cl(B) βΆ Sep (A ββΌ B) (B ββΌ A)" using Fr_6_def pC2 unfolding Sep_def conn by smt
lemma Sep_Op_diff: "Fr_1b β± βΉ Fr_2 β± βΉ βA B. Op(A) β§ Op(B) βΆ Sep (A ββΌ B) (B ββΌ A)" proof -
assume fr1b:"Fr_1b β±" and fr2:"Fr_2 β±"
{ fix A B
from fr1b fr2 have aux: "let M=ββA ; N=ββB in (Cl(M) β§ Cl(N) βΆ Sep (M ββΌ N) (N ββΌ M))" using PF6 Sep_Cl_diff by simp
{ assume "Op(A) β§ Op(B)"
hence "Cl(ββA) β§ Cl(ββB)" using fr2 ClOpdual by simp
hence "Sep (ββA ββΌ ββB) (ββB ββΌ ββA)" using fr1b fr2 aux unfolding conn by simp
moreover have "(ββA ββΌ ββB) ββ (B ββΌ A)" unfolding conn by auto
moreover have "(ββB ββΌ ββA) ββ (A ββΌ B)" unfolding conn by auto
ultimately have "Sep (B ββΌ A) (A ββΌ B)" unfolding conn by simp
hence "Sep (A ββΌ B) (B ββΌ A)" using Sep_comm by simp
} hence "Op(A) β§ Op(B) βΆ Sep (A ββΌ B) (B ββΌ A)" by (rule impI)
} thus ?thesis by simp
qed
lemma Sep_Cl: "βA B. Cl(A) β§ Cl(B) β§ Disj A B βΆ Sep A B" unfolding Sep_def conn by blast
lemma Sep_Op: "Fr_1b β± βΉ Fr_2 β±  βΉ βA B. Op(A) β§ Op(B) β§ Disj A B βΆ Sep A B" proof -
assume fr1b:"Fr_1b β±" and fr2:"Fr_2 β±"
{ fix A B
from fr1b fr2 have aux: "Op(A) β§ Op(B) βΆ Sep (A ββΌ B) (B ββΌ A)" using Sep_Op_diff by simp
{ assume op: "Op(A) β§ Op(B)" and disj: "Disj A B"
hence "(A ββΌ B) ββ A β§ (B ββΌ A) ββ B" unfolding conn by blast
hence "Sep A B" using op aux unfolding conn by simp
} hence "Op(A) β§ Op(B) β§ Disj A B βΆ Sep A B" by simp
} thus ?thesis by simp
qed
lemma "Fr_1a β± βΉ Fr_2 β± βΉ βA B C. Sep A B β§ Sep A C βΆ Sep A (B ββ¨ C)" using CF1a ADDI_a_def unfolding Sep_def conn by metis

textβΉ\noindent{Verifies a neighborhood-based definition of closure.}βΊ
definition "nbhd A p β‘ βE. E ββΌ A β§ Op(E) β§ (E p)"
lemma nbhd_def2: "Fr_1 β± βΉ Fr_2 β± βΉ Fr_4 β± βΉ βA p. (nbhd A p) = (β A p)" using pF4 MONO_def PF1 monI pI2 unfolding nbhd_def conn by smt

lemma C_def_lr: "Fr_1b β± βΉ Fr_2 β± βΉ Fr_4 β± βΉ βA p. (π A p) βΆ (βE. (nbhd E p) βΆ Β¬(Disj E A))" using Cl_fr_def Fr_2_def Fr_6_def PF6 pF1 unfolding nbhd_def conn by smt
lemma C_def_rl: "Fr_1 β± βΉ Fr_2 β± βΉ Fr_4 β± βΉ βA p. (π A p) β΅ (βE. (nbhd E p) βΆ Β¬(Disj E A))" using Cl_fr_def pF5 pA1 pB4 unfolding nbhd_def conn by smt
lemma C_def: "Fr_1 β± βΉ Fr_2 β± βΉ Fr_4 β± βΉ βA p. (π A p) β· (βE. (nbhd E p) βΆ Β¬(Disj E A))" using C_def_lr C_def_rl PF1 by blast

textβΉ\noindent{Explore the Barcan and converse Barcan formulas.}βΊ
lemma Barcan_I: "Fr_inf β± βΉ βP. (ββx. β(P x)) ββΌ β(ββx. P x)" using IF_inf Barcan1 by auto
lemma Barcan_C: "Fr_2 β± βΉ Fr_inf β± βΉ βP. π(ββx. P x) ββΌ (ββx. π(P x))" using Fr_2_def CF_inf Barcan2 by metis
lemma CBarcan_I: "Fr_1b β± βΉ βP. β(ββx. P x)  ββΌ (ββx. β(P x))" by (metis (mono_tags, lifting) MONO_def monI)
lemma CBarcan_C: "Fr_6 β± βΉ βP. (ββx. π(P x)) ββΌ π(ββx. P x)"  by (metis (mono_tags, lifting) MONO_def monC)

end