Theory topo_operators_basic

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

abbreviation implies_rl::"boolboolbool" (infixl "" 25) where "φ  ψ  ψ  φ" (*for readability*)

section ‹Topological operators›

text‹\noindent{Below we define some conditions on algebraic operations (aka. operators) with type @{text "σ⇒σ"}.
Those operations are aimed at extending a Boolean 'algebra of propositions' towards different
generalizations of topological algebras.
We divide this section into two parts. In the first we define and interrelate the topological operators of 
interior, closure, border and frontier. In the second we introduce the (more fundamental) notion of
derivative (aka. derived set) and its related notion of (Cantorian) coherence, defining both as operators.
We follow the naming conventions introduced originally by Kuratowski @{cite Kuratowski1}
(cf. also @{cite Kuratowski2}) and Zarycki @{cite Zarycki1}.}›

subsection ‹Interior and closure›
text‹\noindent{In this section we examine the traditional notion of topological (closure, resp. interior) algebras
in the spirit of McKinsey \& Tarski @{cite AOT}, but drawing primarily from the works of Zarycki
@{cite Zarycki1} and Kuratowski @{cite Kuratowski1}.
We also explore the less-known notions of border (cf. 'Rand' @{cite Hausdorff}, 'bord' @{cite Zarycki1}) and
frontier (aka. 'boundary'; cf. 'Grenze' @{cite Hausdorff}, 'fronti\`ere' @{cite Zarycki1} @{cite Kuratowski2})
as studied by Zarycki @{cite Zarycki1} and define corresponding operations for them.}›

subsubsection ‹Interior conditions›

abbreviation "Int_1 φ   MULT φ" 
abbreviation "Int_1a φ  MULT_a φ"
abbreviation "Int_1b φ  MULT_b φ" 
abbreviation "Int_2 φ   dEXP φ"
abbreviation "Int_3 φ   dNOR φ"
abbreviation "Int_4 φ   IDEM φ"
abbreviation "Int_4' φ  IDEMa φ"

abbreviation "Int_5 φ   NOR φ"
definition "Int_6 φ   A B. φ(A  B)  φ(A)  φ(B)"
definition "Int_7 φ   A B. φ(A  B)  φ(A)  φ(B)"
definition "Int_8 φ   A B. φ(φ A  φ B)  (φ A)  (φ B)"
definition "Int_9 φ   A B. φ A  B  φ A  φ B"

text‹\noindent{@{text "φ"} is an interior operator (@{text "ℑ(φ)"}) iff it satisfies conditions 1-4 (cf. @{cite Zarycki1}
and also @{cite Kuratowski2}). This characterization is shown consistent by generating a non-trivial model.}›
abbreviation " φ  Int_1 φ  Int_2 φ  Int_3 φ  Int_4 φ"
lemma "ℑ φ" nitpick[satisfy, card w=3] oops (*model found: characterization is consistent*)

text‹\noindent{We verify some properties which will become useful later (also to improve provers' performance).}›
lemma PI1: "Int_1 φ = (Int_1a φ  Int_1b φ)" by (metis MULT_def MULT_a_def MULT_b_def)
lemma PI4: "Int_2 φ  (Int_4 φ = Int_4' φ)" unfolding dEXP_def IDEM_def IDEMa_def by blast
lemma PI5: "Int_2 φ  Int_5 φ" unfolding dEXP_def NOR_def conn by blast
lemma PI6: "Int_1a φ  Int_2 φ  Int_6 φ" by (smt dEXP_def Int_6_def MONO_MULTa MONO_def conn)
lemma PI7: "Int_1 φ  Int_7 φ" proof -
  assume int1: "Int_1 φ"
  { fix a b
    have "a  b = a  (a  b)" unfolding conn by blast
    hence "φ(a  b) = φ(a  (a  b))" by simp
    moreover from int1 have "φ(a  b)  φ a  φ b" by (simp add: MULT_def)
    moreover from int1 have "φ(a  (a  b))  φ a  φ (a  b)" by (simp add: MULT_def)
    ultimately have "φ a  φ (a  b)  φ a  φ b" by simp
    hence "φ a  φ (a  b)  φ a  (φ a  φ b)" unfolding conn by blast
    hence "φ(a  b)  φ a  φ b" unfolding conn by blast
  } thus ?thesis by (simp add: Int_7_def)
qed
lemma PI8: "Int_1a φ  Int_2 φ  Int_4 φ  Int_8 φ" using ADDI_b_def IDEM_def Int_8_def MONO_ADDIb MONO_MULTa dEXP_def join_def by auto
lemma PI9: "Int_1a φ  Int_4 φ  Int_9 φ" using IDEM_def Int_9_def MONO_def MONO_MULTa by simp


subsubsection ‹Closure conditions›

abbreviation "Cl_1 φ  ADDI φ"
abbreviation "Cl_1a φ  ADDI_a φ"
abbreviation "Cl_1b φ  ADDI_b φ"
abbreviation "Cl_2 φ  EXP φ"
abbreviation "Cl_3 φ   NOR φ"
abbreviation "Cl_4 φ  IDEM φ"
abbreviation "Cl_4' φ  IDEMb φ"

abbreviation "Cl_5 φ   dNOR φ"
definition "Cl_6 φ   A B. (φ A)  (φ B)  φ (A  B)"
definition "Cl_7 φ  A B. (φ A)  (φ B)  φ (A  B)"
definition "Cl_8 φ   A B. φ(φ A  φ B)  (φ A)  (φ B)"
definition "Cl_9 φ   A B.  A  φ B  φ A  φ B"

text‹\noindent{@{text "φ"} is a closure operator (@{text "ℭ(φ)"}) iff it satisfies conditions 1-4 (cf. @{cite Kuratowski1}
@{cite Kuratowski2}). This characterization is shown consistent by generating a non-trivial model.}›
abbreviation " φ   Cl_1 φ  Cl_2 φ  Cl_3  φ  Cl_4 φ"
lemma "ℭ φ" nitpick[satisfy, card w=3] oops (*model found: characterization is consistent*)

text‹\noindent{We verify some properties that will become useful later.}›
lemma PC1: "Cl_1 φ = (Cl_1a φ  Cl_1b φ)" unfolding ADDI_def ADDI_a_def ADDI_b_def by blast
lemma PC4: "Cl_2 φ  (Cl_4 φ = Cl_4' φ)" unfolding EXP_def IDEM_def IDEMb_def by smt
lemma PC5: "Cl_2 φ  Cl_5 φ" unfolding EXP_def dNOR_def conn by simp
lemma PC6: "Cl_1 φ  Cl_6 φ" proof -
  assume cl1: "Cl_1 φ"
  { fix a b
    have "a  b = (a  b)  b" unfolding conn by blast
    hence "φ(a  b) = φ((a  b)  b)" by simp
    moreover from cl1 have "φ(a  b)  φ a  φ b" by (simp add: ADDI_def)
    moreover from cl1 have "φ((a  b)  b)  φ (a  b)  (φ b)" by (simp add: ADDI_def)
    ultimately have "φ a  φ b  φ(a  b)  φ b" by simp
    hence "(φ a  φ b)  φ b  φ(a  b)  φ b" unfolding conn by blast
    hence "φ a  φ b  φ (a  b)" unfolding conn by blast
  } thus ?thesis by (simp add: Cl_6_def)
qed
lemma PC7: "Cl_1b φ  Cl_2 φ  Cl_7 φ" by (smt EXP_def Cl_7_def MONO_def PC1 MONO_ADDIb conn)
lemma PC8: "Cl_1b φ  Cl_2 φ  Cl_4 φ  Cl_8 φ" by (smt Cl_8_def EXP_def IDEM_def MONO_ADDIb MONO_MULTa MULT_a_def meet_def)
lemma PC9: "Cl_1b φ  Cl_4 φ  Cl_9 φ" by (smt IDEM_def Cl_9_def MONO_def MONO_ADDIb)


subsubsection ‹Exploring dualities›

lemma IC1_dual: "Int_1a φ = Cl_1b φ" using MONO_ADDIb MONO_MULTa by auto
lemma "Int_1b φ = Cl_1a φ" nitpick oops

lemma IC1a: "Int_1a φ  Cl_1b φd" by (smt MULT_a_def ADDI_b_def MONO_def MONO_MULTa dual_def conn)
lemma IC1b: "Int_1b φ  Cl_1a φd" unfolding MULT_b_def ADDI_a_def dual_def conn by auto
lemma IC1:  "Int_1 φ   Cl_1 φd" unfolding MULT_def ADDI_def dual_def conn by simp
lemma IC2:  "Int_2 φ   Cl_2 φd" unfolding dEXP_def EXP_def dual_def conn by blast
lemma IC3:  "Int_3 φ   Cl_3 φd" unfolding dNOR_def NOR_def dual_def conn by simp
lemma IC4:  "Int_4 φ   Cl_4 φd" unfolding IDEM_def IDEM_def dual_def conn by simp
lemma IC4': "Int_4' φ  Cl_4' φd" unfolding IDEMa_def IDEMb_def dual_def conn by metis
lemma IC5:  "Int_5 φ   Cl_5 φd" unfolding NOR_def dNOR_def dual_def conn by simp

lemma CI1a: "Cl_1a φ   Int_1b φd" proof -
  assume cl1a: "Cl_1a φ" 
  { fix A B
    have "φ((A  B))  φ(A  B)" unfolding conn by simp
    moreover from cl1a have "(φ(A)  φ(B))  φ(A  B)" using ADDI_a_def conn by metis
    ultimately have "(φ(A))  (φ(B))  φ((A  B))" unfolding conn by simp
    hence "(φd A)  (φd B)  (φd (A  B))" unfolding dual_def by simp
  } thus "Int_1b φd" using MULT_b_def by blast
qed
lemma CI1b: "Cl_1b φ  Int_1a φd" by (metis IC1a MONO_ADDIb MONO_MULTa)
lemma CI1:  "Cl_1 φ   Int_1 φd" by (simp add: CI1a CI1b PC1 PI1)
lemma CI2:  "Cl_2 φ   Int_2 φd" unfolding EXP_def dEXP_def dual_def conn by metis
lemma CI3:  "Cl_3 φ   Int_3 φd" unfolding NOR_def dNOR_def dual_def conn by simp
lemma CI4:  "Cl_4 φ   Int_4 φd" unfolding IDEM_def IDEM_def dual_def conn by simp
lemma CI4': "Cl_4' φ  Int_4' φd" unfolding IDEMa_def IDEMb_def dual_def conn by metis
lemma CI5:  "Cl_5 φ   Int_5 φd" unfolding dNOR_def NOR_def dual_def conn by simp


subsection ‹Frontier and border›

subsubsection ‹Frontier conditions›

definition "Fr_1a φ  A B. (A  B)  φ(A  B)  (A  B)  (φ A  φ B)"
definition "Fr_1b φ  A B. (A  B)  φ(A  B)  (A  B)  (φ A  φ B)"
definition "Fr_1 φ   A B. (A  B)  φ(A  B)  (A  B)  (φ A  φ B)"
definition "Fr_2 φ  A. φ A  φ(A)"
abbreviation "Fr_3 φ  NOR φ"
definition "Fr_4 φ  A. φ(φ A)  (φ A)"

definition "Fr_5 φ  A. φ(φ(φ A))  φ(φ A)"
definition "Fr_6 φ  A B. A  B  (φ A  B  φ B)"

text‹\noindent{@{text "φ"} is a topological frontier operator (@{text "𝔉(φ)"}) iff it satisfies conditions 1-4
(cf. @{cite Zarycki1}). This is also shown consistent by generating a non-trivial model.}›
abbreviation "𝔉 φ   Fr_1 φ  Fr_2 φ  Fr_3 φ  Fr_4 φ"
lemma "𝔉 φ" nitpick[satisfy, card w=3] oops (*model found: characterization is consistent*)

text‹\noindent{We now verify some useful properties of the frontier operator.}›
lemma PF1: "Fr_1 φ = (Fr_1a φ  Fr_1b φ)" unfolding Fr_1_def Fr_1a_def Fr_1b_def by meson
lemma PF5: "Fr_1 φ  Fr_4 φ  Fr_5 φ" proof -
  assume fr1: "Fr_1 φ" and fr4: "Fr_4 φ"
  { fix A
    from fr1 have "(φ(φ A)  (φ A))  φ(φ(φ A)  (φ A))  (φ(φ A)  (φ A))  (φ(φ(φ A))  φ(φ A))" by (simp add: Fr_1_def)
    moreover have r1: "φ(φ A)  (φ A)  φ(φ A)" using meet_char Fr_4_def fr4 by simp
    moreover have r2: "φ(φ(φ A))  φ(φ A)  φ(φ A)" using join_char Fr_4_def fr4 by simp
    ultimately have "(φ(φ A)  (φ A))  φ(φ(φ A))  (φ(φ A)  (φ A))  φ(φ A)" unfolding conn by auto
    hence "φ(φ(φ A))  φ(φ A)" using r1 r2 conn by auto
  } thus ?thesis by (simp add: Fr_5_def)
qed
lemma PF6: "Fr_1b φ  Fr_2 φ  Fr_6 φ" proof -
  assume fr1b: "Fr_1b φ" and fr2: "Fr_2 φ"
  { fix A B
    have "φ((A  B))  φ(A  B)" unfolding conn by simp
    hence aux: "φ(A  B)  φ(A  B)" by (metis (mono_tags) Fr_2_def fr2)
    from fr1b have "(A  B)  φ(A  B)  (A  B)  (φ(A)  φ(B))" using Fr_1b_def by metis
    hence "A  B  φ(A  B)  A  B  ((φ A)  (φ B))" using Fr_2_def fr2 conn by auto
    hence "A  B  φ(A  B)  A  B  (φ A)  (φ B)" unfolding conn by blast
    hence "A  B  φ(A  B)  A  B  (φ A)  (φ B)" using aux unfolding conn by blast
    hence "A  B  B  φ(A  B)  B  (φ A)  (φ B)" unfolding conn by auto
    hence "A  B  B  (φ B)  B  (φ A)  (φ B)" using join_char unfolding conn by simp
    hence "A  B  (φ A)  B  (φ B)" unfolding conn by simp
  } thus "Fr_6 φ" by (simp add: Fr_6_def)
qed


subsubsection ‹Border conditions›

definition "Br_1 φ  A B. φ(A  B)  (A  φ B)  (B  φ A)"
definition "Br_2 φ  (φ )  "
definition "Br_3 φ  A. φ(φd A)  A"

definition "Br_4 φ  A B. A  B  A  (φ B)  φ A"
definition "Br_5a φ  A. φ(φd A)  φ A"
definition "Br_5b φ  A. φ A  A"
definition "Br_5c φ  A. A  φd A"
definition "Br_5d φ  A. φd A  φd(φ A)"
abbreviation "Br_6 φ  IDEM φ"
abbreviation "Br_7 φ  ADDI_a φ"
abbreviation "Br_8 φ  MULT_b φ"
definition "Br_9 φ  A B. φ(A  B)  (φ A)  (φ B)"
definition "Br_10 φ  A. φ((φ A)  φd A)  "

text‹\noindent{@{text "φ"} is a topological border operator (@{text "𝔅(φ)"}) iff it satisfies conditions 1-3
(cf. @{cite Zarycki1}). This is also shown consistent.}›
abbreviation "𝔅 φ   Br_1 φ  Br_2 φ  Br_3 φ"
lemma "𝔅 φ" nitpick[satisfy, card w=3] oops (*model found: characterization is consistent*)

text‹\noindent{We now verify some useful properties of the border operator.}›
lemma PB4: "Br_1 φ  Br_4 φ" proof -
  assume br1: "Br_1 φ"
  { fix A B
    have aux: "φ(A  B)  (A  φ B)  (B  φ A)" using br1 Br_1_def by simp
    { assume "A  B"
      hence "φ(A  B)  φ A" using meet_char unfolding conn by simp
      hence "φ A  (A  φ B)  (B  φ A)" using aux by auto
      hence "A  φ B  φ A" unfolding conn by auto
    } hence "A  B  A  φ B  φ A" by (rule impI)
  } thus "Br_4 φ"  by (simp add: Br_4_def)
qed
lemma PB5b: "Br_1 φ  Br_5b φ" proof -
  assume br1: "Br_1 φ"
  { fix A
    from br1 have aux: "φ(A  A)  (A  φ A)  (A  φ A)" unfolding Br_1_def by blast
    hence "φ A  (A  φ A)" unfolding conn by metis
    hence "φ A  A" unfolding conn by blast
  } thus "Br_5b φ" using Br_5b_def by blast 
qed
lemma PB5c: "Br_1 φ  Br_5c φ" using Br_5b_def Br_5c_def PB5b dual_def unfolding conn by force 
lemma PB5a: "Br_1 φ  Br_3 φ  Br_5a φ" proof -
  assume br1: "Br_1 φ" and br3: "Br_3 φ"
  hence br5c: "Br_5c φ" using PB5c by simp
  { fix A
    have "A  φ(φd A)  φ A" by (metis br5c Br_4_def Br_5c_def PB4 br1)
    hence "φ(φd A)  φ A" using Br_3_def br3 unfolding conn by metis
  } thus "Br_5a φ" using Br_5a_def by simp 
qed
lemma PB5d: "Br_1 φ  Br_3 φ  Br_5d φ" proof -
  assume br1: "Br_1 φ" and br3: "Br_3 φ"
  hence br5a: "Br_5a φ" using PB5a by simp
  { fix A
    from br5a have "φ(φd(A))  φ(A)" unfolding Br_5a_def by simp
    hence "φ(A)  φ(φd(A))" unfolding conn by blast
    hence "φd A  φd(φ A)" unfolding dual_def conn by simp
  } thus "Br_5d φ" using Br_5d_def by simp 
qed
lemma PB6: "Br_1 φ  Br_6 φ" by (smt Br_4_def Br_5b_def IDEM_def PB4 PB5b conn)
lemma PB7: "Br_1 φ  Br_7 φ" using Br_4_def Br_5b_def ADDI_a_def PB4 PB5b unfolding conn by smt
lemma PB8: "Br_1 φ  Br_8 φ" using Br_1_def Br_5b_def MULT_b_def PB5b unfolding conn by metis
lemma PB9: "Br_1 φ  Br_9 φ" unfolding Br_1_def Br_9_def conn by simp
lemma PB10: "Br_1 φ  Br_3 φ  Br_10 φ" proof - ―‹ proof automagically generated ›
  assume a1: "Br_3 φ"
  assume a2: "Br_1 φ"
  { fix bb :: "w  bool" and ww :: w
    have "p pa w pb. ((pb p w  pb pa w)  ¬pb (pa  p) w)  ¬Br_9 pb"
      by (metis Br_9_def join_def) (* 20 ms *)
    then have "(φ (((φc)  (φd)) bb) ww)  ( ww)  ¬(φ (((φc)  (φd)) bb) ww)  ¬( ww)"
      using a2 a1 by (metis (no_types) Br_5a_def Br_5b_def Br_5d_def PB5a PB5b PB5d PB9 bottom_def compl_def dual_def meet_def) (* 86 ms *)
  } then show ?thesis unfolding Br_10_def by blast (* 1 ms *)
qed


subsubsection ‹Relation with closure and interior›

text‹\noindent{We define and verify some conversion operators useful to derive border and frontier operators from
closure/interior operators and also between each other.}›

text‹\noindent{Frontier operator as derived from interior.}›
definition Fr_int::"(σσ)(σσ)" ("I") where "I   λA. ( A)  d A" 
lemma FI1: "Int_1 φ  Int_2 φ   Fr_1(I φ)" using EXP_def Fr_1_def Fr_int_def IC2 MULT_def conn by auto
lemma FI2: "Fr_2(I φ)" using Fr_2_def Fr_int_def dual_def dual_symm unfolding conn by smt 
lemma FI3: "Int_3 φ  Fr_3(I φ)" using NOR_def Fr_int_def IC3 unfolding conn by auto  
lemma FI4: "Int_1a φ  Int_2 φ   Int_4 φ  Fr_4(I φ)" unfolding Fr_int_def Fr_4_def dual_def conn by (smt Int_9_def MONO_MULTa PI9)

text‹\noindent{Frontier operator as derived from closure.}›
definition Fr_cl::"(σσ)(σσ)" ("C") where "C 𝒞  λA. (𝒞 A)  𝒞(A)" 
lemma FC1: "Cl_1 φ  Cl_2 φ   Fr_1(C φ)" using CI1 EXP_def Fr_1_def Fr_cl_def MULT_def dual_def unfolding conn by smt
lemma FC2: "Fr_2(C φ)" using Fr_2_def Fr_cl_def dual_def dual_symm unfolding conn by smt
lemma FC3: "Cl_3 φ  Fr_3(C φ)" unfolding NOR_def Fr_cl_def conn by simp 
lemma FC4: "Cl_1b φ  Cl_2 φ  Cl_4 φ  Fr_4(C φ)" using Cl_8_def MONO_ADDIb PC8 unfolding Fr_cl_def Fr_4_def conn by blast
  
text‹\noindent{Frontier operator as derived from border.}›
definition Fr_br::"(σσ)(σσ)" ("B") where "B   λA.  A  (A)"
lemma FB1: "Br_1 φ   Fr_1(B φ)" unfolding Fr_br_def Fr_1_def using Br_1_def Br_5b_def PB5b conn by smt
lemma FB2: "Fr_2(B φ)" unfolding Fr_br_def Fr_2_def conn by auto
lemma FB3: "Br_1 φ  Br_2 φ   Fr_3(B φ)" using Br_2_def Br_5b_def PB5b unfolding Fr_br_def NOR_def conn by force
lemma FB4: "Br_1 φ  Br_3 φ   Fr_4(B φ)" proof -
  assume br1: "Br_1 φ" and br3: "Br_3 φ"
  { fix A 
   have "(B φ) ((B φ) A) = φ(φ A  φ(A))  φ((φ A  φ(A)))" by (simp add: Fr_br_def conn)
   also have "... = φ(φ A  φ(A))  φ((φ A)  φd A)" by (simp add: dual_def conn)
   also from br1 br3 have "... = φ(φ A  φ(A))  " using Br_10_def PB10 by metis
   finally have "(B φ) ((B φ) A)  φ(φ A  φ(A))" unfolding conn by simp
   hence "(B φ) ((B φ) A)  (B φ) A" using Br_5b_def Fr_br_def PB5b br1 by fastforce
  } thus "Fr_4(B φ)" using Fr_4_def by blast
qed

text‹\noindent{Border operator as derived from interior.}›
definition Br_int::"(σσ)(σσ)" ("I") where "I   λA. A  ( A)"
lemma BI1: "Int_1 φ   Br_1 (I φ)" using Br_1_def Br_int_def MULT_def conn by auto
lemma BI2: "Int_3 φ   Br_2 (I φ)" by (simp add: Br_2_def Br_int_def dNOR_def conn)
lemma BI3: "Int_1a φ  Int_4 φ  Br_3 (I φ)" unfolding Br_int_def Br_3_def dual_def by (smt Int_9_def MONO_MULTa PI9 conn)

text‹\noindent{Border operator as derived from closure.}›
definition Br_cl::"(σσ)(σσ)" ("C")  where "C 𝒞  λA. A  𝒞(A)"
lemma BC1: "Cl_1 φ   Br_1(C φ)" using Br_1_def Br_cl_def CI1 MULT_def dual_def unfolding conn by smt
lemma BC2: "Cl_3 φ   Br_2(C φ)" using Br_2_def Br_cl_def CI3 dNOR_def dual_def unfolding conn by auto
lemma BC3: "Cl_1b φ  Cl_4 φ  Br_3 (C φ)" unfolding Br_cl_def Br_3_def dual_def conn by (metis (mono_tags, lifting) Cl_9_def PC9)

text‹\noindent{Note that the previous two conversion functions are related:}›
lemma BI_BC_rel: "(I φ) = C(φd)" by (simp add: Br_cl_def Br_int_def dual_def conn)

text‹\noindent{Border operator as derived from frontier.}›
definition Br_fr::"(σσ)(σσ)" ("F") where "F   λA. A  ( A)"
lemma BF1: "Fr_1 φ  Br_1(F φ)" using Br_1_def Br_fr_def Fr_1_def conn by auto 
lemma BF2: "Fr_2 φ  Fr_3 φ  Br_2(F φ)" using Br_2_def Br_fr_def Fr_2_def NOR_def unfolding conn by fastforce
lemma BF3: "Fr_1b φ  Fr_2 φ  Fr_4 φ  Br_3(F φ)" proof - 
  assume fr1b: "Fr_1b φ" and fr2: "Fr_2 φ" and fr4: "Fr_4 φ"
  { fix A
    from fr1b fr2 have "let M= A  φ A ; N= φ A in M  N  (φ M  N  φ N)" using PF1 PF6 by (simp add: Fr_6_def)
    hence "φ(A  φ A)  φ A  φ(φ A)" unfolding conn by meson
    hence "φ(A  φ A)  φ A" using Fr_4_def fr4 unfolding conn by metis
    hence aux: "φ(A  φ A)  (φ A)  " unfolding conn by blast
    have "(F φ)((F φ)d A) = (A  φ(A))  φ((A  φ(A)))" unfolding Br_fr_def dual_def by simp 
    also have "... = (A  φ A)  φ(A  φ A)" using Fr_2_def fr2 unfolding conn by force
    also have "... = (A  φ(A  φ A))  (φ A  φ(A  φ A))" unfolding conn by auto
    also have "... = (A  φ(A  φ A))" using aux unfolding conn by blast
    finally have "(F φ)((F φ)d A) = A  φ(A  φ A)" unfolding Br_fr_def dual_def conn by simp
  } thus "Br_3(F φ)" unfolding Br_3_def Br_fr_def conn by meson
qed

text‹\noindent{Interior operator as derived from border.}›
definition Int_br::"(σσ)(σσ)" ("B") where "B   λA. A  ( A)"
lemma IB1: "Br_1 φ  Int_1(B φ)" using Br_1_def MULT_def Int_br_def conn by auto 
lemma IB2: "Int_2(B φ)" by (simp add: dEXP_def Int_br_def conn)
lemma IB3: "Br_2 φ  Int_3(B φ)" by (simp add: Br_2_def dNOR_def Int_br_def conn)
lemma IB4: "Br_1 φ  Br_3 φ  Int_4(B φ)" unfolding Int_br_def IDEM_def conn
  using Br_1_def Br_5c_def Br_5d_def PB5c PB5d dual_def unfolding conn by (metis (full_types))

text‹\noindent{Interior operator as derived from frontier.}›
definition Int_fr::"(σσ)(σσ)" ("F") where "F   λA. A  ( A)"
lemma IF1a: "Fr_1b φ  Int_1a(F φ)" using Fr_1b_def MULT_a_def Int_fr_def conn by auto
lemma IF1b: "Fr_1a φ  Int_1b(F φ)" using Fr_1a_def MULT_b_def Int_fr_def conn by auto
lemma IF1: "Fr_1 φ  Int_1(F φ)" by (simp add: IF1a IF1b PF1 PI1)
lemma IF2: "Int_2(F φ)" by (simp add: dEXP_def Int_fr_def conn)
lemma IF3: "Fr_2 φ  Fr_3 φ  Int_3(F φ)" using BF2 Br_2_def Br_fr_def dNOR_def Int_fr_def unfolding conn by auto
lemma IF4: "Fr_1a φ  Fr_2 φ  Fr_4 φ  Int_4(F φ)"
  using Fr_1a_def Fr_2_def Fr_4_def unfolding Int_fr_def IDEM_def conn by metis  

text‹\noindent{Closure operator as derived from border.}›
definition Cl_br::"(σσ)(σσ)" ("𝒞B") where "𝒞B   λA. A  (A)"
lemma CB1: "Br_1 φ  Cl_1(𝒞B φ)" proof -
 assume br1: "Br_1 φ"
  { fix A B
    have "(𝒞B φ) (A  B) = A  B  φ((A  B))" by (simp add: Cl_br_def conn)
    also have "... = A  B  φ(A  B)" unfolding conn by simp
    also have "... = A  B  (A  φ(B))  (B  φ(A))" using Br_1_def br1 unfolding conn by auto
    also have "... = A  φ(A)  B  φ(B)" unfolding conn by auto
    also have "... = (𝒞B φ) A  (𝒞B φ) B" by (simp add: Cl_br_def conn)
    finally have "(𝒞B φ)(A  B) = (𝒞B φ) A  (𝒞B φ) B" unfolding Cl_br_def by blast
  } thus "Cl_1(𝒞B φ)" unfolding ADDI_def Cl_br_def by simp
qed
lemma CB2: "Cl_2(𝒞B φ)" by (simp add: EXP_def Cl_br_def conn) 
lemma CB3: "Br_2 φ  Cl_3(𝒞B φ)" using Br_2_def Cl_br_def IC3 dNOR_def dual_def dual_symm unfolding conn by smt
lemma CB4: "Br_1 φ  Br_3 φ  Cl_4(𝒞B φ)" proof -
 assume br1: "Br_1 φ" and br3: "Br_3 φ"
  { fix A 
   have "(𝒞B φ) ((𝒞B φ) A) = A  φ(A)  φ((A  φ(A)))" by (simp add: Cl_br_def conn)
   also have "... = A  φ(A)  φ(A  φd A)" unfolding dual_def conn by simp
   also have "... = A  φ(A)  (A  φ(φd A))  (A  φ(A))" unfolding dual_def using Br_1_def br1 conn by auto
   also have "... = A  φ(A)" using Br_3_def br3 unfolding conn by metis
   finally have "(𝒞B φ) ((𝒞B φ) A) = (𝒞B φ) A" unfolding Cl_br_def by blast
  } thus "Cl_4(𝒞B φ)" unfolding IDEM_def Cl_br_def by simp
qed

text‹\noindent{Closure operator as derived from frontier.}›
definition Cl_fr::"(σσ)(σσ)" ("𝒞F") where "𝒞F   λA. A  ( A)"
lemma CF1b: "Fr_1b φ  Fr_2 φ  Cl_1b(𝒞F φ)" using Cl_fr_def Fr_6_def MONO_def MONO_ADDIb PF6 unfolding conn by auto
lemma CF1a: "Fr_1a φ  Fr_2 φ  Cl_1a(𝒞F φ)" proof -
  have aux: "Fr_2 φ  (F φ)d = (𝒞F φ)" by (simp add: Cl_fr_def Fr_2_def Int_fr_def dual_def conn)
  hence "Fr_1a φ  Fr_2 φ  Cl_1a(F φ)d" using IC1b IF1b by blast
  thus "Fr_1a φ  Fr_2 φ  Cl_1a(𝒞F φ)" using ADDI_a_def aux unfolding conn by simp
qed
lemma CF1: "Fr_1 φ  Fr_2 φ  Cl_1(𝒞F φ)" by (simp add: CF1a CF1b PC1 PF1)
lemma CF2: "Cl_2(𝒞F φ)" by (simp add: EXP_def Cl_fr_def conn)
lemma CF3: "Fr_3 φ  Cl_3(𝒞F φ)" by (simp add: Cl_fr_def NOR_def conn)
lemma CF4: "Fr_1a φ  Fr_2 φ  Fr_4 φ  Cl_4(𝒞F φ)" proof -
  have aux: "Fr_2 φ  (F φ)d = (𝒞F φ)"  by (simp add: Cl_fr_def Fr_2_def Int_fr_def dual_def conn)
  hence "Fr_1a φ  Fr_2 φ  Fr_4 φ  Cl_4(F φ)d" using IC4 IF4 by blast
  thus "Fr_1a φ  Fr_2 φ  Fr_4 φ  Cl_4(𝒞F φ)" by (simp add: aux)
qed


subsubsection ‹Infinitary conditions›

text‹\noindent{We define the essential infinitary conditions for the closure and interior operators (entailing infinite
additivity and multiplicativity resp.). Observe that the other direction is implied by monotonicity (MONO).}›
abbreviation "Cl_inf φ  iADDI_a(φ)"
abbreviation "Int_inf φ  iMULT_b(φ)"

text‹\noindent{There exists indeed a condition on frontier operators responsible for the infinitary conditions above:}›
definition "Fr_inf φ  S. S  φ(S)  S  Ra[φ|S]"

lemma CF_inf: "Fr_2 φ  Fr_inf φ  Cl_inf(𝒞F φ)" unfolding iADDI_a_def  Fr_inf_def 
  by (smt Cl_fr_def Fr_2_def Ra_restr_ex compl_def dom_compl_def2 iDM_b join_def meet_def supremum_def)
lemma IF_inf: "Fr_inf φ  Int_inf(F φ)" unfolding Fr_inf_def iMULT_b_def Int_fr_def Ra_restr_all
  by (metis (mono_tags, hide_lams) diff_def infimum_def meet_def pfunRange_restr_def supremum_def)

text‹\noindent{This condition is indeed strong enough to entail closure of the fixed-point predicates under infimum/supremum.}›
lemma fp_IF_inf_closed: "Fr_inf φ  infimum_closed (fp (F φ))" by (metis (full_types) IF2 IF_inf Ra_restr_all dEXP_def iMULT_b_def infimum_def)
lemma fp_CF_sup_closed: "Fr_inf φ  Fr_2 φ  supremum_closed (fp (𝒞F φ))" by (metis (full_types) CF2 CF_inf EXP_def Ra_restr_ex iADDI_a_def supremum_def)

end