Theory topo_derivative_algebra

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