Theory logics_operators

theory logics_operators
  imports conditions_positive
begin

subsection ‹Converting between topological operators›

text‹We verify minimal conditions under which operators resulting from conversion functions coincide.›

text‹Conversions between interior, closure and exterior are straightforward and hold without restrictions: 
  Interior and closure are each other duals. Exterior is the complement of closure.
  We focus here on conversions involving the border and frontier operators.›

text‹Interior operator as derived from border.›
definition Int_br::"('w σ⇒'w σ)⇒('w σ⇒'w σ)" ("ℐ⇩B") 
  where "ℐ⇩B ℬ ≡ λA. A ❙↼ (ℬ A)"
text‹Interior operator as derived from frontier.›
definition Int_fr::"('w σ⇒'w σ)⇒('w σ⇒'w σ)" ("ℐ⇩F") 
  where "ℐ⇩F ℱ ≡ λA. A ❙↼ (ℱ A)"
text‹Closure operator as derived from border.›
definition Cl_br::"('w σ⇒'w σ)⇒('w σ⇒'w σ)" ("𝒞⇩B") 
  where "𝒞⇩B ℬ ≡ λA. A ❙∨ ℬ(❙─A)"
text‹Closure operator as derived from frontier.›
definition Cl_fr::"('w σ⇒'w σ)⇒('w σ⇒'w σ)" ("𝒞⇩F") 
  where "𝒞⇩F ℱ ≡ λA. A ❙∨ (ℱ A)"
text‹Frontier operator as derived from interior.›
definition Fr_int::"('w σ⇒'w σ)⇒('w σ⇒'w σ)" ("ℱ⇩I") 
  where "ℱ⇩I ℐ ≡ λA. ❙─(ℐ A ❙∨ ℐ(❙─A))"
text‹Frontier operator as derived from closure.›
definition Fr_cl::"('w σ⇒'w σ)⇒('w σ⇒'w σ)" ("ℱ⇩C") 
  where "ℱ⇩C 𝒞 ≡ λA. (𝒞 A) ❙∧ 𝒞(❙─A)"
text‹Frontier operator as derived from border.›
definition Fr_br::"('w σ⇒'w σ)⇒('w σ⇒'w σ)" ("ℱ⇩B") 
  where "ℱ⇩B ℬ ≡ λA. ℬ A ❙∨ ℬ(❙─A)"
text‹Border operator as derived from interior.›
definition Br_int::"('w σ⇒'w σ)⇒('w σ⇒'w σ)" ("ℬ⇩I") 
  where "ℬ⇩I ℐ ≡ λA. A ❙↼ (ℐ A)"
text‹Border operator as derived from closure.›
definition Br_cl::"('w σ⇒'w σ)⇒('w σ⇒'w σ)" ("ℬ⇩C")  
  where "ℬ⇩C 𝒞 ≡ λA. A ❙∧ 𝒞(❙─A)"
text‹Border operator as derived from frontier.›
definition Br_fr::"('w σ⇒'w σ)⇒('w σ⇒'w σ)" ("ℬ⇩F") 
  where "ℬ⇩F ℱ ≡ λA. A ❙∧ (ℱ A)"

text‹Inter-definitions involving border or frontier do not hold without restrictions.›
lemma "ℬ = ℬ⇩C (𝒞⇩B ℬ)" nitpick oops ―‹ countermodel ›
lemma "ℬ = ℬ⇩I (ℐ⇩B ℬ)" nitpick oops ―‹ countermodel ›
lemma "ℬ = ℬ⇩F (ℱ⇩B ℬ)" nitpick oops ―‹ countermodel ›
lemma "ℱ = ℱ⇩C (𝒞⇩F ℱ)" nitpick oops ―‹ countermodel ›
lemma "ℱ = ℱ⇩I (ℐ⇩F ℱ)" nitpick oops ―‹ countermodel ›
lemma "ℱ = ℱ⇩B (ℬ⇩F ℱ)" nitpick oops ―‹ countermodel ›

lemma "𝒞 = 𝒞⇩B (ℬ⇩C 𝒞)" nitpick oops ―‹ countermodel ›
lemma "𝒞 = 𝒞⇩F (ℱ⇩C 𝒞)" nitpick oops ―‹ countermodel ›
lemma "ℐ = ℐ⇩B (ℬ⇩C ℐ)" nitpick oops ―‹ countermodel ›
lemma "ℐ = ℐ⇩F (ℱ⇩C ℐ)" nitpick oops ―‹ countermodel ›


text‹Inter-definitions involving border or frontier always assume the second Kuratowski condition 
  (or its respective counterpart: C2, I2, B2 or F2).›
abbreviation "C2 φ ≡ EXPN φ"
abbreviation "I2 φ ≡ CNTR φ"
abbreviation "B2 φ ≡ CNTR φ"
abbreviation "F2 φ ≡ ∀A. φ(❙─A) ❙= φ A"

lemma "B2 ℬ ⟹ ℬ = ℬ⇩C (𝒞⇩B ℬ)" unfolding CNTR_def Br_cl_def Cl_br_def conn order by metis
lemma "B2 ℬ ⟹ ℬ = ℬ⇩I (ℐ⇩B ℬ)" unfolding CNTR_def Br_int_def Int_br_def conn order by metis
lemma "B2 ℬ ⟹ ℬ = ℬ⇩F (ℱ⇩B ℬ)" unfolding CNTR_def Br_fr_def Fr_br_def conn order by metis
lemma "F2 ℱ ⟹ ℱ = ℱ⇩C (𝒞⇩F ℱ)" unfolding Cl_fr_def Fr_cl_def conn order by metis
lemma "F2 ℱ ⟹ ℱ = ℱ⇩I (ℐ⇩F ℱ)" unfolding Int_fr_def Fr_int_def conn order by metis
lemma "F2 ℱ ⟹ ℱ = ℱ⇩B (ℬ⇩F ℱ)" unfolding Br_fr_def Fr_br_def conn order by metis

lemma "C2 𝒞 ⟹ 𝒞 = 𝒞⇩B (ℬ⇩C 𝒞)" unfolding EXPN_def Br_cl_def Cl_br_def conn order by metis
lemma "C2 𝒞 ⟹ 𝒞 = 𝒞⇩F (ℱ⇩C 𝒞)" unfolding EXPN_def Fr_cl_def Cl_fr_def conn order by metis
lemma "I2 ℐ ⟹ ℐ = ℐ⇩B (ℬ⇩I ℐ)" unfolding CNTR_def Int_br_def Br_int_def conn order by metis
lemma "I2 ℐ ⟹ ℐ = ℐ⇩F (ℱ⇩I ℐ)" unfolding CNTR_def Int_fr_def Fr_int_def conn order by metis

end