theory topo_derivative_algebra imports topo_operators_derivative begin nitpick_params[assms=true, user_axioms=true, show_all, expect=genuine, format=3] (*default Nitpick settings*) section βΉDerivative 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. We explore the second variant by drawing on the notion of derivative algebra.}βΊ textβΉ\noindent{Declares a primitive (unconstrained) derivative (aka. derived-set) operation and defines others from it.}βΊ consts π::"ΟβΟ" abbreviation "β β‘ ββ©_{D}π" ββΉ interior βΊ abbreviation "π β‘ πβ©_{D}π" ββΉ closure βΊ abbreviation "β¬ β‘ β¬β©_{D}π" ββΉ border βΊ abbreviation "β± β‘ β±β©_{D}π" ββΉ frontier βΊ abbreviation "π¦ β‘ π¦β©_{D}π" ββΉ coherence βΊ subsection βΉBasic propertiesβΊ textβΉ\noindent{Verifies minimal conditions under which operators resulting from conversion functions coincide.}βΊ lemma ICdual: "β ββ‘πβ§^{d}" by (simp add: dual_der2 equal_op_def) lemma ICdual': "π ββ‘ββ§^{d}" by (simp add: dual_der1 equal_op_def) lemma BI_rel: "β¬ ββ‘β¬β©_{I}β" using Br_der_def Br_int_def Int_der_def unfolding equal_op_def conn by auto lemma IB_rel: "β ββ‘ββ©_{B}β¬" using Br_der_def Int_br_def Int_der_def unfolding equal_op_def conn by auto lemma BC_rel: "β¬ ββ‘β¬β©_{C}π" using BI_BC_rel BI_rel dual_der1 by auto lemma CB_rel: "π ββ‘πβ©_{B}β¬" using Br_der_def2 Cl_br_def Int_der_def2 dual_def dual_der1 unfolding equal_op_def conn by auto lemma FI_rel: "β± ββ‘β±β©_{I}β" by (metis Cl_der_def FI2 Fr_2_def Fr_der_def2 Fr_int_def ICdual' dual_def eq_ext' equal_op_def) lemma FC_rel: "β± ββ‘β±β©_{C}π" by (simp add: Cl_der_def Fr_cl_def Fr_der_def2 equal_op_def) lemma FB_rel: "β± ββ‘β±β©_{B}β¬" by (smt Br_der_def CB_rel Cl_br_def Cl_der_def Fr_br_def Fr_der_def Fr_der_def2 equal_op_def conn) textβΉ\noindent{Recall that derivative and coherence operations cannot be obtained from either interior, closure, border nor frontier. The derivative operation can indeed be seen as being more fundamental than the other ones.}βΊ textβΉ\noindent{Fixed-point and other operators are interestingly related.}βΊ lemma fp1: "ββ§^{f}β§^{p}ββ‘β¬β§^{c}" by (smt BI_rel Br_int_def IB_rel Int_br_def equal_op_def conn) lemma fp2: "β¬β§^{f}β§^{p}ββ‘ββ§^{c}" using Br_der_def Int_der_def unfolding equal_op_def conn by auto lemma fp3: "πβ§^{f}β§^{p}ββ‘β¬β§^{d}" by (smt BI_rel Br_int_def CB_rel Cl_br_def dual_def equal_op_def conn) lemma fp4: "(β¬β§^{d})β§^{f}β§^{p}ββ‘π" by (smt dimp_def equal_op_def fp3) lemma fp5: "β±β§^{f}β§^{p}ββ‘β¬ ββ(πβ§^{c})" using Br_der_def Cl_der_def Fr_der_def unfolding equal_op_def conn by auto lemma fp6: "πβ§^{f}β§^{p}ββ‘π¦ ββ(πβ§^{c})" using Cl_der_def Kh_der_def equal_op_def conn by fastforce textβΉ\noindent{Different inter-relations (some redundant ones are kept to help the provers).}βΊ lemma monI: "Der_1b π βΉ MONO β" by (simp add: ID1b MONO_MULTa) lemma monC: "Der_1b π βΉ MONO π" by (simp add: CD1b MONO_ADDIb) lemma pB1: "βA. β¬ A ββA ββΌβ A" using BI_rel Br_int_def eq_ext' by fastforce lemma pB2: "βA. β¬ A ββA ββ§β± A" using Br_der_def Fr_der_def conn by auto lemma pB3: "βA. β¬(ββA) ββββA ββ§β± A" using FD2 Fr_2_def meet_def pB2 by auto lemma pB4: "βA. β¬(ββA) ββββA ββ§π A" by (simp add: dual_def dual_der1 pB1 conn) lemma pB5: "Der_1b π βΉ βA. β¬(π A) ββΌ(β¬ A) ββ¨β¬(ββA)" using ADDI_b_def Cl_der_def MONO_ADDIb monI pB1 pB4 unfolding conn by auto lemma pF1: "βA. β± A ββπ A ββΌβ A" using Cl_der_def Fr_der_def Int_der_def conn by auto lemma pF2: "βA. β± A ββπ A ββ§π(ββA)" by (simp add: Cl_der_def Fr_der_def2) lemma pF3: "βA. β± A βββ¬ A ββ¨β¬(ββA)" by (smt Br_der_def Cl_der_def dual_def dual_der1 dual_der2 pF2 conn) lemma pF4: "Der_1 π βΉ Der_4e π βΉ βA. β±(β A) ββΌβ± A" by (metis CD1 CD2 CD4a ICdual ID4 IDEM_def PC1 PC4 PC5 PD8 diff_def eq_ext' pF1) lemma pF5: "Der_1 π βΉ Der_4e π βΉ βA. β±(π A) ββΌβ± A" by (metis FD2 Fr_2_def ICdual' dual_def eq_ext' pF4) lemma pA1: "βA. A βββ A ββ¨β¬ A" using Br_der_def2 Int_der_def2 conn by auto lemma pA2: "βA. A ββπ A ββΌβ¬(ββA)" using Cl_der_def pB4 conn by auto lemma pC1: "βA. π A ββA ββ¨β¬(ββA)" using CB_rel Cl_br_def eq_ext' by fastforce lemma pC2: "βA. π A ββA ββ¨β± A" using Cl_der_def Fr_der_def2 conn by auto lemma pI1: "βA. β A ββA ββΌβ¬ A" using pA1 pB1 conn by auto lemma pI2: "βA. β A ββA ββΌβ± A" using Br_der_def Fr_der_def pI1 conn by auto lemma IC_imp: "Der_1 π βΉ Der_3 π βΉ βA B. β(A ββB) ββΌπ A ββπ B" proof - assume der1: "Der_1 π" and der3: "Der_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 der3 dNOR_def using ID3 by auto moreover have "let A=(a ββb) ββ§ββb; B=ββa in β(A ββB) ββΌβ(A) βββ(B)" using ID1 Int_7_def PI7 der1 by auto ultimately have "β((a ββb) ββ§ββb) βββ(ββa) ββββ€" unfolding conn by simp moreover have "let A=a ββb; B=ββb in β(A ββ§B) βββ(A) ββ§β(B)" using ID1 MULT_def der1 by auto ultimately have "β(a ββb) ββ§β(ββb) βββ(ββa) ββββ€" unfolding conn by simp moreover have "βA. β(ββA) ββββπ(A)" by (simp add: dual_def dual_der1 conn) 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{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: "Der_1a π βΉ Der_4e π βΉ βA. Op(β A)" using ID4a IDEM_def by blast lemma Cl_Closed: "Der_1a π βΉ Der_4e π βΉ βA. Cl(π A)" using CD4a IDEM_def by blast lemma Br_Border: "Der_1b π βΉ βA. Br(β¬ A)" by (smt Br_der_def CI1b IC1_dual PD1 conn) textβΉ\noindent{In contrast, there is no analogous fixed-point result for frontier:}βΊ lemma "π π βΉ βA. Fr(β± A)" nitpick oops (*counterexample even if assuming all derivative conditions*) lemma OpCldual: "βA. Cl A β· Op(ββA)" using dual_def dual_der1 conn by auto lemma ClOpdual: "βA. Op A β· Cl(ββA)" by (simp add: dual_def dual_der1 conn) lemma Fr_ClBr: "βA. Fr(A) = (Cl(A) β§ Br(A))" using join_def meet_def pB2 pC2 by auto lemma Cl_F: "Der_1 π βΉ Der_4e π βΉ βA. Cl(β± A)" using FD4 Fr_4_def join_def pC2 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 derivative operation as primitive).}βΊ lemma Cl_Bzero: "β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: "βA. Br(A) β· β A ββββ₯" using Br_der_def2 Int_der_def2 unfolding conn by metis lemma Fr_nowhereDense: "βA. Fr(A) βΆ β(π A) ββββ₯" using Fr_ClBr Br_boundary eq_ext by metis lemma Cl_FB: "βA. Cl A β· β± A βββ¬ A" using Br_der_def2 pA2 pF1 pF3 unfolding conn by metis lemma Op_FB: "βA. Op A β· β± A βββ¬(ββA)" using pA1 pA2 pF3 pI2 unfolding conn by metis lemma Clopen_Fzero: "βA. Cl A β§ Op A β· β± A ββββ₯" using Cl_der_def Int_der_def Fr_der_def unfolding conn by smt lemma Int_sup_closed: "Der_1b π βΉ supremum_closed (Ξ»A. Op A)" by (smt IC1_dual ID1b Int_der_def2 PD1 sup_char diff_def) lemma Int_meet_closed: "Der_1a π βΉ meet_closed (Ξ»A. Op A)" by (metis ID1a Int_der_def MULT_b_def meet_def) lemma Int_inf_closed: "Der_inf π βΉ infimum_closed (Ξ»A. Op A)" by (simp add: fp_ID_inf_closed) lemma Cl_inf_closed: "Der_1b π βΉ infimum_closed (Ξ»A. Cl A)" by (smt Cl_der_def IC1_dual ID1b PD2 dual_der1 inf_char join_def) lemma Cl_join_closed: "Der_1a π βΉ join_closed (Ξ»A. Cl A)" using ADDI_a_def Cl_der_def join_def by fastforce lemma Cl_sup_closed: "Der_inf π βΉ supremum_closed (Ξ»A. Cl A)" by (simp add: fp_CD_sup_closed) lemma Br_inf_closed: "Der_1b π βΉ infimum_closed (Ξ»A. Br A)" by (smt Br_der_def CI1b IC1_dual PD1 inf_char diff_def) lemma Fr_inf_closed: "Der_1b π βΉ infimum_closed (Ξ»A. Fr A)" by (metis (full_types) Br_der_def Br_inf_closed Cl_der_def Cl_inf_closed Fr_der_def join_def diff_def) lemma Br_Fr_join: "Der_1 π βΉ Der_4e π βΉ βA B. Br A β§ Fr B βΆ Br(A ββ¨B)" proof - assume der1: "Der_1 π" and der4: "Der_4e π" { fix A B { assume bra: "Br A" and frb: "Fr B" from bra have "β A ββββ₯" using Br_boundary by auto hence 1: "π(ββA) ββββ€" by (metis ICdual bottom_def compl_def dual_def eq_ext' top_def) from frb have "β(π B) ββββ₯" by (simp add: Fr_nowhereDense) hence 2: "π(ββ(π B)) ββββ€" by (metis ICdual bottom_def compl_def dual_def eq_ext' top_def) from der1 have "π(ββA) ββΌπ B ββΌπ((ββA) ββΌB)" by (simp add: CD1 PD4) 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 der1 der4 have 4: "let M=ββ(π B); N=ββ(A ββ¨B) in M ββΌπ N βΆ π M ββΌπ N" by (smt CD1b Cl_Closed PC1 PD1) from 3 4 have "π(ββ(π B)) ββΌπ(ββ(A ββ¨B))" by simp hence "ββ€ββπ(ββ(A ββ¨B))" using 2 unfolding top_def by simp hence "ββ₯βββ(A ββ¨B)" using ICdual dual_def eq_ext' conn by metis hence "Br (A ββ¨B)" using 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: "Der_1 π βΉ Der_4e π βΉ join_closed (Ξ»A. Fr A)" by (simp add: Br_Fr_join Cl_join_closed Fr_ClBr PC1) 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: Cl_der_def Fr_der_def2 dual_def dual_der2 conn) lemma Disj_B: "βA. Disj (β¬ A) (β¬(ββA))" by (simp add: Br_der_def2 conn) lemma Disj_I: "βA. Disj (β A) (ββA)" by (simp add: Int_der_def conn) lemma Disj_BCI: "βA. Disj (β¬(π A)) (β(ββA))" by (simp add: Br_der_def2 dual_def dual_der1 conn) lemma Disj_CBI: "Der_1b π βΉ Der_4e π βΉ βA. Disj (π(β¬(ββA))) (β(ββA))" by (smt Br_der_def2 Der_4e_def Cl_der_def Int_der_def2 PD3 conn) textβΉ\noindent{Introduce 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 CD2 EXP_def Sep_def conn by auto lemma Sep_I: "Der_1 π βΉ Der_4e π βΉ βA. Sep (β A) (β (ββA))" unfolding Sep_def by (smt CD2 CD4 IC1 ID1 PC4 PC5 PD8 dual_def dual_der1 dual_der2 conn) lemma Sep_sub: "Der_1b π βΉ βA B C D. Sep A B β§ C ββΌA β§ D ββΌB βΆ Sep C D" using MONO_ADDIb PD2 dual_der1 monI unfolding Sep_def conn by metis lemma Sep_Cl_diff: "Der_1b π βΉ βA B. Cl(A) β§ Cl(B) βΆ Sep (A ββΌB) (B ββΌA)" unfolding Sep_def using CD1b PD1 bottom_def diff_def meet_def by smt lemma Sep_Op_diff: "Der_1b π βΉ βA B. Op(A) β§ Op(B) βΆ Sep (A ββΌB) (B ββΌA)" proof - assume der1b:"Der_1b π" { fix A B from der1b have aux: "let M=ββA ; N=ββB in (Cl(M) β§ Cl(N) βΆ Sep (M ββΌN) (N ββΌM))" using Sep_Cl_diff by simp { assume "Op(A) β§ Op(B)" hence "Cl(ββA) β§ Cl(ββB)" using der1b ClOpdual by simp hence "Sep (ββA ββΌββB) (ββB ββΌββA)" using der1b 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: "Der_1b π βΉ βA B. Op(A) β§ Op(B) β§ Disj A B βΆ Sep A B" proof - assume der1b:"Der_1b π" { fix A B from der1b 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 "Der_1a π βΉ βA B C. Sep A B β§ Sep A C βΆ Sep A (B ββ¨C)" using ADDI_a_def CD1a unfolding Sep_def conn by metis textβΉ\noindent{Verifies a neighborhood-based definition of interior.}βΊ definition "nbhd A p β‘ βE. E ββΌA β§ Op(E) β§ (E p)" lemma nbhd_def2: "Der_1 π βΉ Der_4e π βΉ βA p. (nbhd A p) = (β A p)" unfolding nbhd_def by (smt Int_Open MONO_def PC1 monI pI2 conn) lemma I_def'_lr': "βA p. (β A p) βΆ (βE. (β E p) β§ E ββΌA)" by blast lemma I_def'_rl': "Der_1b π βΉ βA p. (β A p) β΅ (βE. (β E p) β§ E ββΌA)" using MONO_def monI by metis lemma I_def': "Der_1b π βΉ βA p. (β A p) β· (βE. (β E p) β§ E ββΌA)" using MONO_def monI by metis textβΉ\noindent{Explore the Barcan and converse Barcan formulas.}βΊ lemma Barcan_I: "Der_inf π βΉ βP. (ββx. β(P x)) ββΌβ(ββx. P x)" using ID_inf Barcan1 by auto lemma Barcan_C: "Der_inf π βΉ βP. π(ββx. P x) ββΌ(ββx. π(P x))" using CD_inf Barcan2 by metis lemma CBarcan_I: "Der_1b π βΉ βP. β(ββx. P x) ββΌ(ββx. β(P x))" by (metis (mono_tags, lifting) MONO_def monI) lemma CBarcan_C: "Der_1b π βΉ βP. (ββx. π(P x)) ββΌπ(ββx. P x)" by (metis (mono_tags, lifting) MONO_def monC) end