# 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