Theory topo_operators_derivative

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


subsection ‹Derivative and coherence›

text‹\noindent{In this section we investigate two related operators, namely the `derivative' (or `derived set')
and the (Cantorian) `coherence' of a set. The derivative of a set is the set of its accumulation (aka. limit)
points. The coherence of a set A is the set formed by those limit points of A belonging to A.
For the derivative operator we draw upon the works by Kuratowski @{cite Kuratowski1} and
(in more detail) by Zarycki @{cite Zarycki3}; cf.~also McKinsey \& Tarski @{cite AOT}.
For the (Cantorian) coherence operator we follow the treatment given by Zarycki in @{cite Zarycki2}.}›

subsubsection ‹Derivative conditions›

text‹\noindent{The derivative conditions overlap partly with Kuratowski closure conditions @{cite Kuratowski1}.
We try to make both notations coincide when possible.}›

abbreviation "Der_1 φ   Cl_1 φ"
abbreviation "Der_1a φ  Cl_1a φ"
abbreviation "Der_1b φ  Cl_1b φ"
abbreviation "Der_2 φ   Cl_5 φ" ―‹ follows from Cl-2 ›
abbreviation "Der_3 φ   Cl_3 φ"
abbreviation "Der_4 φ   Cl_4' φ"
definition   "Der_4e φ  A. φ(φ A)  (φ A  A)"
definition   "Der_5 φ  A. (φ A  A)  (A  φd A)  (A    A  )"

text‹\noindent{Some remarks:
Condition Der-2 basically says (when assuming other derivative axioms) that the space is dense-in-itself,
i.e. that all points are accumulation points (no point is isolated) w.r.t the whole space.
Der-4 is a weakened (left-to-right) variant of Cl-4.
Condition Der-4e corresponds to a (weaker) condition than Der-4 and is used in more recent literature
(in particular in the works of Leo Esakia @{cite Esakia}).
When other derivative axioms are assumed, Der-5 above as used by Zarycki @{cite Zarycki3} says that
the only clopen sets in the space are the top and bottom elements (empty set and universe, resp.).
We verify some properties:}›

lemma Der4e_rel: "Der_4 φ  Der_4e φ" by (simp add: IDEMb_def Der_4e_def conn)
lemma PD1: "Der_1b φ  A B. A  B  φ A  φ B" using MONO_def MONO_ADDIb by auto
lemma PD2: "Der_1b φ  A B. A  B  φd A  φd B" using CI1b MONO_def MONO_MULTa dual_def by fastforce
lemma PD3: "Der_1b φ  A B. φ(A  B)  φ A  φ B" unfolding conn by (metis (no_types, lifting) PD1)
lemma PD4: "Der_1 φ  A B. (φ A  φ B)  φ(A  B)" using Cl_6_def PC6 by metis
lemma PD5: "Der_4 φ  A. φ(φ((φ A)))  φ((φ A))" unfolding IDEMb_def by blast
text‹\noindent{Observe that the lemmas below require Der-2 as premise:}›
lemma PD6: "Der_1 φ  Der_2 φ  A. φd A  φ A" unfolding ADDI_def dNOR_def dual_def conn by fastforce
lemma PD7: "Der_1 φ  Der_2 φ  A. φ(φd A)  φ(φ A)" by (metis (mono_tags, lifting) PC1 PD1 PD6)
lemma PD8: "Der_1 φ  Der_2 φ  Der_4 φ  A. φ(φd A)  φ A" by (meson IDEMb_def PD7)
lemma PD9: "Der_1 φ  Der_2 φ  Der_4 φ  A. φd A  φd(φ A)" by (metis CI4' IDEMa_def PC1 PD2 PD6)
lemma PD10: "Der_1 φ  Der_2 φ  Der_4 φ  A. φd A  φ(φd A)" using CI4' IDEMa_def PD6 by metis
lemma PD11: "Der_1 φ  Der_2 φ  Der_4 φ  A. (φ A)  φ((φ A))" using IDEMb_def PD6 dual_def unfolding conn by metis
lemma PD12: "Der_1 φ  Der_2 φ  Der_4 φ  A. (φd A)  (φ A)  φd(A  (φ A))" proof -
 assume der1: "Der_1 φ" and der2: "Der_2 φ" and der4: "Der_4 φ"
  { fix A 
    from der1 have "let M=A ; N=(φ A) in φ(M  N)  (φ M)  (φ N)" unfolding ADDI_def by simp
    hence aux: "(φ(A)  φ((φ A)))  (φ (A  (φ A)))" unfolding dual_def conn by simp
    have "(φd A  φ A) = (φd A  φd(φ A))" using PD6 PD9 der1 der2 der4 unfolding conn by metis
    also have "... = (φ(A)  φ((φ A)))" unfolding dual_def conn by simp
    also from aux have "... = (φ (A  (φ A)))" unfolding dual_def by blast
    also have "... = φd(A  (φ A))" unfolding dual_def conn by simp
    finally have "(φd A)  (φ A)  φd(A  (φ A))" by simp
 } thus ?thesis by simp
qed

text‹\noindent{The conditions below can serve to axiomatize a derivative operator. Different authors consider different
sets of conditions. We define below some corresponding to Zarycki @{cite Zarycki3}, Kuratowski @{cite Kuratowski1}
@{cite Zarycki2}, McKinsey \& Tarski @{cite AOT}, and Esakia @{cite Esakia}, respectively.}›
abbreviation "𝔇z φ   Der_1 φ  Der_2 φ  Der_3 φ  Der_4 φ  Der_5 φ"
abbreviation "𝔇k φ   Der_1 φ  Der_2 φ  Der_3 φ  Der_4 φ"
abbreviation "𝔇mt φ  Der_1 φ            Der_3 φ  Der_4 φ"
abbreviation "𝔇e φ   Der_1 φ            Der_3 φ  Der_4e φ"

text‹\noindent{Our `default' derivative operator will coincide with @{text "𝔇k"} from Kuratowski (also Zarycki).
However, for proving theorems we will employ the weaker variant Der-4e instead of Der-4 whenever possible.
We start by defining a dual operator and verifying some dualities; we then define conversion operators.
Observe that conditions Der-2 and  Der-5 are not used in the rest of this subsection.
Der-2 will be required later when working with the coherence operator.}›
abbreviation "𝔇 φ  𝔇k φ"
abbreviation "Σ φ  Int_1 φ  Int_3 φ  Int_4' φ  Int_5 φ" ―‹ 'dual-derivative' operator ›

lemma SD_dual1: (φ)  𝔇(φd)" using IC1 IC4' IC3 IC5 by simp
lemma SD_dual2: (φd)  𝔇(φ)" using IC1 IC4' IC3 IC5 dual_symm by metis
lemma DS_dual1: "𝔇(φ)  Σ(φd)" using CI1 CI4' CI3 CI5 by simp
lemma DS_dual2: "𝔇(φd)  Σ(φ)" using CI1 CI4' CI3 CI5 dual_symm by metis
lemma DS_dual: "𝔇(φ) = Σ(φd)"  using SD_dual2 DS_dual1 by smt

text‹\noindent{Closure operator as derived from derivative.}›
definition Cl_der::"(σσ)(σσ)" ("𝒞D") where  "𝒞D 𝒟  λA. A  𝒟(A)"
text‹\noindent{Verify properties:}›
lemma CD1a: "Der_1a 𝒟  Cl_1a (𝒞D 𝒟)" unfolding Cl_der_def ADDI_a_def conn by auto
lemma CD1b: "Der_1b 𝒟  Cl_1b (𝒞D 𝒟)" unfolding Cl_der_def ADDI_b_def conn by auto
lemma CD1 : "Der_1 𝒟  Cl_1 (𝒞D 𝒟)" unfolding Cl_der_def ADDI_def conn by blast
lemma CD2: "Cl_2 (𝒞D 𝒟)" unfolding Cl_der_def EXP_def conn by simp
lemma CD3: "Der_3 𝒟  Der_3 (𝒞D 𝒟)" unfolding Cl_der_def NOR_def conn by simp
lemma CD4a: "Der_1a 𝒟  Der_4e 𝒟  Cl_4 (𝒞D 𝒟)" unfolding Cl_der_def by (smt ADDI_a_def Der_4e_def IDEM_def join_def)
lemma "Der_1b 𝒟  Der_4 𝒟  Cl_4 (𝒞D 𝒟)" nitpick oops (*countermodel*)
lemma CD4: "Der_1 𝒟  Der_4e 𝒟  Cl_4 (𝒞D 𝒟)" unfolding Cl_der_def by (metis (no_types, lifting) CD4a Cl_der_def IDEM_def PC1)

text‹\noindent{Interior operator as derived from (dual) derivative.}›
definition Int_der::"(σσ)(σσ)" ("D") where "D 𝒟  λA. A  𝒟d(A)" 
text‹\noindent{Verify definition:}›
lemma Int_der_def2: "D 𝒟 = (λφ. φ  𝒟(φ))" unfolding Int_der_def dual_def conn by simp 
lemma dual_der1: "𝒞D 𝒟  (D 𝒟)d" unfolding Cl_der_def Int_der_def dual_def conn by simp
lemma dual_der2: "D 𝒟  (𝒞D 𝒟)d" unfolding Cl_der_def Int_der_def dual_def conn by simp
text‹\noindent{Verify properties:}›
lemma ID1: "Der_1 𝒟  Int_1 (D 𝒟)" using Int_der_def MULT_def ADDI_def CI1 unfolding conn by auto
lemma ID1a: "Der_1a 𝒟  Int_1b (D 𝒟)" by (simp add: CI1a dual_der2 CD1a)
lemma ID1b: "Der_1b 𝒟  Int_1a (D 𝒟)" by (simp add: CI1b dual_der2 CD1b)
lemma ID2: "Int_2 (D 𝒟)" unfolding Int_der_def dEXP_def conn by simp
lemma ID3: "Der_3 𝒟  Int_3 (D 𝒟)" by (simp add: CI3 CD3 dual_der2)
lemma ID4: "Der_1 𝒟  Der_4e 𝒟  Int_4 (D 𝒟)" using CI4 CD4 dual_der2 by simp
lemma ID4a: "Der_1a 𝒟  Der_4e 𝒟  Int_4 (D 𝒟)" by (simp add: CI4 dual_der2 CD4a)
lemma "Der_1b 𝒟  Der_4 𝒟  Int_4 (D 𝒟)" nitpick oops (*countermodel*)

text‹\noindent{Border operator as derived from (dual) derivative.}›
definition Br_der::"(σσ)(σσ)" ("D") where "D 𝒟  λA. A  𝒟d(A)"
text‹\noindent{Verify definition:}›
lemma Br_der_def2: "D 𝒟 = (λA. A  𝒟(A))" unfolding Br_der_def dual_def conn by simp 
text‹\noindent{Verify properties:}›
lemma BD1: "Der_1 𝒟  Br_1 (D 𝒟)" using Br_der_def Br_1_def CI1 MULT_def conn by auto 
lemma BD2: "Der_3 𝒟  Br_2 (D 𝒟)" using Br_der_def Br_2_def CI3 dNOR_def unfolding conn by auto
lemma BD3: "Der_1b 𝒟  Der_4e 𝒟  Br_3 (D 𝒟)" using dual_def Der_4e_def MONO_ADDIb MONO_def  unfolding Br_der_def Br_3_def conn by smt

text‹\noindent{Frontier operator as derived from derivative.}›
definition Fr_der::"(σσ)(σσ)" ("D") where "D 𝒟  λA. (A  𝒟d(A))  (𝒟(A)  A)"
text‹\noindent{Verify definition:}›
lemma Fr_der_def2: "D 𝒟 = (λA. (A  𝒟(A))  (A  𝒟(A)))" unfolding Fr_der_def dual_def conn by auto  
text‹\noindent{Verify properties:}›
lemma FD1a: "Der_1a 𝒟  Fr_1a(D 𝒟)" unfolding Fr_1a_def Fr_der_def using CI1a MULT_b_def conn by auto
lemma FD1b: "Der_1b 𝒟  Fr_1b(D 𝒟)" unfolding Fr_1b_def Fr_der_def using CI1b MULT_a_def conn by smt
lemma FD1: "Der_1 𝒟  Fr_1(D 𝒟)" unfolding Fr_1_def Fr_der_def using CI1 MULT_def conn by auto
lemma FD2: "Fr_2(D 𝒟)" using dual_def dual_symm unfolding Fr_2_def Fr_der_def conn by metis
lemma FD3: "Der_3 𝒟  Fr_3(D 𝒟)" by (simp add: NOR_def Fr_der_def conn)
lemma FD4: "Der_1 𝒟  Der_4e 𝒟  Fr_4(D 𝒟)" by (metis CD1b CD2 CD4 Cl_8_def Cl_der_def Fr_4_def Fr_der_def2 PC1 PC8 meet_def)

text‹\noindent{Note that the derivative operation cannot be obtained from interior, closure, border, nor frontier.
In this respect the derivative is a fundamental operation.}›

subsubsection ‹Infinitary conditions›

text‹\noindent{The corresponding infinitary condition on derivative operators is inherited from the one for closure.}›
abbreviation "Der_inf φ  Cl_inf(φ)"

lemma CD_inf: "Der_inf φ  Cl_inf(𝒞D φ)" unfolding iADDI_a_def by (smt Cl_der_def Fr_2_def Ra_restr_ex compl_def dom_compl_def2 iDM_b join_def meet_def supremum_def)
lemma ID_inf: "Der_inf φ  Int_inf(D φ)" by (simp add: CD_inf dual_der2 iADDI_MULT_dual1)

text‹\noindent{This condition is indeed strong enough as to entail closure of some fixed-point predicates under infimum/supremum.}›
lemma fp_ID_inf_closed: "Der_inf φ  infimum_closed (fp (D φ))" by (metis (full_types) ID2 ID_inf Ra_restr_all dEXP_def iMULT_b_def inf_char)
lemma fp_CD_sup_closed: "Der_inf φ  supremum_closed (fp (𝒞D φ))" by (metis (full_types) CD_inf Cl_der_def Ra_restr_ex iADDI_a_def join_def supremum_def)


subsubsection ‹Coherence conditions›
text‹\noindent{We finish this section by introducing the `coherence' operator (Cantor's `Koherenz') as discussed
by Zarycki in @{cite Zarycki2}. As happens with the derivative operator, the coherence operator cannot
be derived from interior, closure, border, nor frontier.}›

definition "Kh_1 φ  ADDI_b φ"
definition "Kh_2 φ  dEXP φ"
definition "Kh_3 φ  A. φ(φd A)  φd(φ A)"

lemma PK1: "Kh_1 φ  MONO φ" using ADDI_b_def Kh_1_def MONO_ADDIb by auto
lemma PK2: "Kh_1 φ  A B. φ(A  B)  (φ A)  (φ B)" using MULT_a_def MONO_MULTa PK1 by auto
lemma PK3: "Kh_2 φ  φ   " using Kh_2_def dEXP_def unfolding conn by auto
lemma PK4: "Kh_1 φ   Kh_3 φ  φ   " using MONO_def PK1 dual_def unfolding Kh_3_def conn by metis
lemma PK5: "Kh_2 φ   A. φ(A)  (φ A)" unfolding Kh_2_def dEXP_def conn by metis
lemma PK6: "Kh_1 φ  Kh_2 φ   A B. φ(A  B)  (φ A)  (φ B)" unfolding conn by (metis (no_types, lifting) Kh_2_def dEXP_def MONO_def PK1)
lemma PK7: "Kh_3 φ   A. φ(φ((φ A)))  φ((φ(φd A)))" proof -
 assume kh3: "Kh_3 φ"
  { fix A
    from kh3 have "φ(φd A) = φd(φ A)" using Kh_3_def by auto
    hence "φ((φ(φd A)))  φ(φ((φ A)))" unfolding dual_def conn by simp   
  } thus ?thesis by simp
qed
lemma PK8: "Kh_3 φ   A. φ((φ(φ A)))  φd(φ((φ A)))" proof -
 assume kh3: "Kh_3 φ"
  { fix A
    from kh3 have aux: "φd(φ A)  φ(φd A)" using Kh_3_def by simp
    have "let A=(φ A) in (φd(φ A)  φ(φd A))" using Kh_3_def kh3 by auto
    hence "φ((φ(φ A)))  φd(φ((φ A)))" unfolding dual_def conn by simp
  } thus ?thesis  by simp
qed

text‹\noindent{Coherence operator as derived from derivative (requires conditions Der-2 and Der-4).}›
definition Kh_der::"(σσ)(σσ)" ("𝒦D") where "𝒦D 𝒟  λA. A  (𝒟 A)"
text‹\noindent{Verify properties:}›
lemma KD1: "Der_1 φ  Kh_1 (𝒦D φ)" using PC1 PD3 PK2 ADDI_def Kh_der_def unfolding conn by (metis (full_types))  
lemma KD2: "Kh_2 (𝒦D φ)" by (simp add: Kh_2_def dEXP_def Kh_der_def conn) 
lemma KD3: "Der_1 φ  Der_2 φ  Der_4 φ   Kh_3 (𝒦D φ)" proof -
 assume der1: "Der_1 φ" and der2: "Der_2 φ" and der4: "Der_4 φ"
  { fix A 
    from der1 have aux1: "let M=A ; N=(φd A) in φ(M  N)  (φ M  φ N)" unfolding ADDI_def by simp
    from der1 der2 der4 have aux2: "(φd A)  (φ A)  φd(A  φ A)" using PD12 by simp
    have "(𝒦D φ)((𝒦D φ)d A) = ((A  φ (A))  φ ((A  φ (A))))" unfolding Kh_der_def dual_def by simp
    also have "... = (A  φd A)  φ(A  φd A)" unfolding dual_def conn by simp
    also from aux1 have "... = (A  φd A)  (φ A  φ(φd A))" unfolding conn by meson
    also have "... = (A  φ A)  φd A" using PD6 PD8 der1 der2 der4 unfolding conn by blast
    also have "... = (A  φ A)  (φd A  φ A)" using PD6 der1 der2 unfolding conn by blast
    also have "... = (A  φd A)  (φ A)" unfolding conn by auto
    also from aux2 have "... = (A  φ A)  φd(A  φ A)" unfolding dual_def conn by meson
    also have "... = ((A  φ A)  φ ((A  φ A)))" unfolding dual_def conn by simp
    also have "... = (𝒦D φ)d((𝒦D φ) A)" unfolding Kh_der_def dual_def by simp
    finally have "(𝒦D φ)((𝒦D φ)d A)  (𝒦D φ)d((𝒦D φ) A)" by simp
 } thus ?thesis unfolding Kh_3_def by simp
qed

end