# Theory topo_frontier_algebra

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

section ‹Frontier 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. In this section we explore the first variant by drawing on the notion
of a frontier algebra, defined in an analogous fashion as the well-known closure and interior algebras.}›

text‹\noindent{Declares a primitive (unconstrained) frontier (aka. boundary) operation and defines others from it.}›
consts ℱ::"σ⇒σ"
abbreviation "ℐ ≡ ℐ⇩F ℱ" ―‹ interior ›
abbreviation "𝒞 ≡ 𝒞⇩F ℱ" ―‹ closure ›
abbreviation "ℬ ≡ ℬ⇩F ℱ" ―‹ border ›

subsection ‹Basic properties›

text‹\noindent{Verifies minimal conditions under which operators resulting from conversion functions coincide.}›
lemma ICdual: "Fr_2 ℱ ⟹ ℐ ❙≡ 𝒞⇧d" by (simp add: Cl_fr_def Fr_2_def Int_fr_def dual_def equal_op_def conn)
lemma ICdual': "Fr_2 ℱ ⟹ 𝒞 ❙≡ ℐ⇧d" by (simp add: Cl_fr_def Fr_2_def Int_fr_def dual_def equal_op_def conn)
lemma BI_rel: "ℬ ❙≡ ℬ⇩I ℐ" using Br_fr_def Br_int_def Int_fr_def unfolding equal_op_def conn by auto
lemma IB_rel: "ℐ ❙≡ ℐ⇩B ℬ" using Br_fr_def Int_br_def Int_fr_def unfolding equal_op_def conn by auto
lemma BC_rel: "Fr_2 ℱ ⟹ ℬ ❙≡ ℬ⇩C 𝒞"  using BI_BC_rel BI_rel ICdual' eq_ext' by fastforce
lemma CB_rel: "Fr_2 ℱ ⟹ 𝒞 ❙≡ 𝒞⇩B ℬ" using Br_fr_def Cl_br_def Cl_fr_def Fr_2_def unfolding equal_op_def conn by auto
lemma FI_rel: "Fr_2 ℱ ⟹ ℱ ❙≡ ℱ⇩I ℐ" by (smt Cl_fr_def Fr_int_def ICdual' Int_fr_def compl_def diff_def equal_op_def join_def meet_def)
lemma FC_rel: "Fr_2 ℱ ⟹ ℱ ❙≡ ℱ⇩C 𝒞" by (metis (mono_tags, lifting) FI_rel Fr_2_def Fr_cl_def Fr_int_def ICdual' dual_def eq_ext' equal_op_def)
lemma FB_rel: "Fr_2 ℱ ⟹ ℱ ❙≡ ℱ⇩B ℬ" by (smt Br_fr_def CB_rel Cl_br_def FC_rel Fr_br_def Fr_cl_def equal_op_def join_def meet_def)

text‹\noindent{Fixed-point and other operators are interestingly related.}›
lemma fp1: "ℐ⇧f⇧p ❙≡ ℬ⇧c" using Br_fr_def Int_fr_def unfolding equal_op_def conn by auto
lemma fp2: "ℬ⇧f⇧p ❙≡ ℐ⇧c" using Br_fr_def Int_fr_def unfolding equal_op_def conn by auto
lemma fp3: "Fr_2 ℱ ⟹ 𝒞⇧f⇧p ❙≡ ℬ⇧d" using Br_fr_def Cl_fr_def Fr_2_def dual_def equal_op_def conn by fastforce
lemma fp4: "Fr_2 ℱ ⟹ (ℬ⇧d)⇧f⇧p ❙≡ 𝒞" by (smt dimp_def equal_op_def fp3)
lemma fp5: "ℱ⇧f⇧p ❙≡ ℬ ❙⊔ (𝒞⇧c)" using Br_fr_def Cl_fr_def unfolding equal_op_def conn by auto

text‹\noindent{Different inter-relations (some redundant ones are kept to help the provers).}›
lemma monI: "Fr_1b ℱ ⟹ MONO(ℐ)" by (simp add: IF1a MONO_MULTa)
lemma monC: "Fr_6 ℱ ⟹ MONO(𝒞)" by (simp add: Cl_fr_def Fr_6_def MONO_def conn)
lemma pB1: "∀A. ℬ A ❙≈ A ❙↼ ℐ A" using Br_fr_def fp1 unfolding conn equal_op_def by metis
lemma pB2: "∀A. ℬ A ❙≈ A ❙∧ ℱ A" by (simp add: Br_fr_def)
lemma pB3: "Fr_2 ℱ ⟹ ∀A. ℬ(❙─A) ❙≈ ❙─A ❙∧ ℱ A" by (simp add: Fr_2_def pB2 conn)
lemma pB4: "Fr_2 ℱ ⟹ ∀A. ℬ(❙─A) ❙≈ ❙─A ❙∧ 𝒞 A" using CB_rel Cl_br_def pB3 unfolding conn equal_op_def by metis
lemma pB5: "Fr_1b ℱ ⟹ Fr_2 ℱ ⟹ ∀A. ℬ(𝒞 A) ❙≼ (ℬ A) ❙∨ ℬ(❙─A)"  by (smt BC_rel Br_cl_def Cl_fr_def Fr_6_def PF6 equal_op_def conn)
lemma pF1: "∀A. ℱ A ❙≈ 𝒞 A ❙↼ ℐ A"  using Cl_fr_def Int_fr_def conn by auto
lemma pF2: "Fr_2 ℱ ⟹ ∀A. ℱ A ❙≈ 𝒞 A ❙∧ 𝒞(❙─A)" using Cl_fr_def Fr_2_def conn by auto
lemma pF3: "Fr_2 ℱ ⟹ ∀A. ℱ A ❙≈ ℬ A ❙∨ ℬ(❙─A)" using Br_fr_def Fr_2_def conn by auto
lemma pF4: "Fr_1 ℱ ⟹ Fr_2 ℱ ⟹ Fr_4(ℱ) ⟹ ∀A. ℱ(ℐ A) ❙≼ ℱ A" by (smt IDEMa_def IF2 IF4 Int_fr_def MONO_def PF1 PF6 PI4 diff_def monC pF1)
lemma pF5: "Fr_1 ℱ ⟹ Fr_2 ℱ ⟹ Fr_4 ℱ ⟹ ∀A. ℱ(𝒞 A) ❙≼ ℱ A" by (metis Br_fr_def CF4 Cl_fr_def IDEM_def PF1 join_def meet_def pB5 pF3)
lemma pA1: "∀A. A ❙≈ ℐ A ❙∨ ℬ A" using Br_fr_def Int_fr_def unfolding conn by auto
lemma pA2: "Fr_2 ℱ ⟹ ∀A. A ❙≈ 𝒞 A ❙↼ ℬ(❙─A)" using pB1 dual_def fp3 unfolding equal_op_def conn by smt
lemma pC1: "Fr_2 ℱ ⟹ ∀A. 𝒞 A ❙≈ A ❙∨ ℬ(❙─A)" using Cl_fr_def pB4 conn by auto
lemma pC2: "∀A. 𝒞 A ❙≈ A ❙∨ ℱ A" using Cl_fr_def by auto
lemma pI1: "∀A. ℐ A ❙≈ A ❙↼ ℬ A" using pA1 pB1 conn by auto
lemma pI2: "∀A. ℐ A ❙≈ A ❙↼ ℱ A" by (simp add: Int_fr_def)

lemma IC_imp: "Fr_1 ℱ ⟹ Fr_2 ℱ ⟹ Fr_3 ℱ ⟹ ∀A B. ℐ(A ❙→ B) ❙≼ 𝒞 A ❙→ 𝒞 B" proof -
assume fr1: "Fr_1 ℱ" and fr2: "Fr_2 ℱ" and fr3: "Fr_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 fr3 IF3 dNOR_def fr2 by auto
moreover have "let A=(a ❙→ b) ❙∧ ❙─b; B=❙─a in ℐ(A ❙→ B) ❙≼ ℐ(A) ❙→ ℐ(B)" using fr1 IF1 PI7 Int_7_def by metis
ultimately have "ℐ((a ❙→ b) ❙∧ ❙─b) ❙→ ℐ(❙─a) ❙≈ ❙⊤" unfolding conn by simp
moreover have "let A=a ❙→ b; B=❙─b in ℐ(A ❙∧ B) ❙≈ ℐ(A) ❙∧ ℐ(B)" using fr1 IF1 MULT_def by simp
ultimately have "ℐ(a ❙→ b) ❙∧ ℐ(❙─b) ❙→ ℐ(❙─a) ❙≈ ❙⊤" unfolding conn by simp
moreover have "∀A. ℐ(❙─A) ❙≈ ❙─𝒞(A)" using Cl_fr_def Fr_2_def Int_fr_def fr2  unfolding conn by auto
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{Defines 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: "Fr_1a ℱ ⟹ Fr_2 ℱ ⟹ Fr_4 ℱ ⟹ ∀A. Op(ℐ A)" using IF4 IDEM_def by blast
lemma Cl_Closed: "Fr_1a ℱ ⟹ Fr_2 ℱ ⟹ Fr_4 ℱ ⟹ ∀A. Cl(𝒞 A)" using CF4 IDEM_def by blast
lemma Br_Border: "Fr_1b ℱ ⟹ ∀A. Br(ℬ A)" using Br_fr_def Fr_1b_def conn by auto
text‹\noindent{In contrast, there is no analogous fixed-point result for frontier:}›
lemma "𝔉 ℱ ⟹ ∀A. Fr(ℱ A)" nitpick oops (*counterexample even if assuming all frontier conditions*)

lemma OpCldual: "Fr_2 ℱ ⟹ ∀A. Cl A ⟷ Op(❙─A)" using Cl_fr_def Fr_2_def Int_fr_def conn by auto
lemma ClOpdual: "Fr_2 ℱ ⟹ ∀A. Op A ⟷ Cl(❙─A)" using ICdual dual_def unfolding equal_op_def conn by auto
lemma Fr_ClBr: "∀A. Fr(A) = (Cl(A) ∧ Br(A))" using Br_fr_def Cl_fr_def join_def meet_def by auto
lemma Cl_F: "Fr_4 ℱ ⟹ ∀A. Cl(ℱ A)" using Cl_fr_def Fr_4_def conn 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 frontier operation as primitive).}›
lemma Cl_Bzero: "Fr_2 ℱ ⟹ ∀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: "Fr_2 ℱ ⟹ ∀A. Br(A) ⟷ ℐ A ❙≈ ❙⊥" by (metis Br_fr_def Int_fr_def bottom_def diff_def meet_def)
lemma Fr_nowhereDense: "Fr_2 ℱ ⟹ ∀A. Fr(A) ⟶ ℐ(𝒞 A) ❙≈ ❙⊥" using Fr_ClBr Br_boundary eq_ext by metis
lemma Cl_FB: "∀A. Cl A ⟷ ℱ A ❙≈ ℬ A" using Br_fr_def Cl_fr_def unfolding conn by auto
lemma Op_FB: "Fr_2 ℱ ⟹ ∀A. Op A ⟷ ℱ A ❙≈ ℬ(❙─A)" using Br_fr_def Fr_2_def Int_fr_def unfolding conn by auto
lemma Clopen_Fzero: "∀A. Cl A ∧ Op A ⟷ ℱ A ❙≈ ❙⊥" using Cl_fr_def Int_fr_def unfolding conn by auto

lemma Int_sup_closed: "Fr_1b ℱ ⟹ supremum_closed (λA. Op A)" by (smt IF1a Int_fr_def MONO_def MONO_MULTa sup_char conn)
lemma Int_meet_closed: "Fr_1a ℱ ⟹ meet_closed (λA. Op A)" using Fr_1a_def Int_fr_def unfolding conn by metis
lemma Int_inf_closed: "Fr_inf ℱ ⟹ infimum_closed (λA. Op A)" by (simp add: fp_IF_inf_closed)
lemma Cl_inf_closed: "Fr_6 ℱ ⟹ infimum_closed (λA. Cl A)" by (smt Cl_fr_def Fr_6_def infimum_def join_def)
lemma Cl_join_closed: "Fr_1a ℱ ⟹ Fr_2 ℱ ⟹ join_closed (λA. Cl A)" using ADDI_a_def CF1a CF2 EXP_def unfolding conn by metis
lemma Cl_sup_closed: "Fr_2 ℱ ⟹ Fr_inf ℱ ⟹ supremum_closed (λA. Cl A)" by (simp add: fp_CF_sup_closed)
lemma Br_inf_closed: "Fr_1b ℱ ⟹ infimum_closed (λA. Br A)" by (smt BI_rel Br_int_def IF1a MONO_iMULTa MONO_MULTa Ra_restr_all eq_ext' iMULT_a_def inf_char diff_def)
lemma Fr_inf_closed: "Fr_1b ℱ ⟹ Fr_2 ℱ ⟹ infimum_closed (λA. Fr A)" by (metis (full_types) Br_fr_def Br_inf_closed PF6 Cl_fr_def Cl_inf_closed meet_def join_def)
lemma Br_Fr_join: "Fr_1 ℱ ⟹ Fr_2 ℱ ⟹ Fr_4 ℱ ⟹ ∀A B. Br A ∧ Fr B ⟶ Br(A ❙∨ B)" proof -
assume fr1: "Fr_1 ℱ" and fr2: "Fr_2 ℱ" and fr4: "Fr_4 ℱ"
{ fix A B
{ assume bra: "Br A" and frb: "Fr B"
from bra have "ℐ A ❙≈ ❙⊥" using Br_boundary fr2 by auto
hence 1: "𝒞(❙─A) ❙≈ ❙⊤" by (metis ICdual bottom_def compl_def dual_def eq_ext' fr2 top_def)
from frb have "ℐ(𝒞 B) ❙≈ ❙⊥" by (simp add: Fr_nowhereDense fr2)
hence 2: "𝒞(❙─(𝒞 B)) ❙≈ ❙⊤" by (metis ICdual bottom_def compl_def dual_def eq_ext' fr2 top_def)
from fr1 fr2 have "𝒞(❙─A) ❙↼ 𝒞 B ❙≼ 𝒞((❙─A) ❙↼ B)" using CF1 Cl_6_def PC6 by metis
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 fr1 fr2 fr4 have 4: "let M=❙─(𝒞 B); N=❙─(A ❙∨ B) in  M ❙≼ 𝒞 N ⟶ 𝒞 M ❙≼ 𝒞 N" using PC9 CF4 Cl_9_def PF1 CF1b by fastforce
from 3 4 have "𝒞(❙─(𝒞 B)) ❙≼ 𝒞(❙─(A ❙∨ B))" by simp
hence "❙⊤ ❙≈ 𝒞(❙─(A ❙∨ B))" using 2 unfolding top_def by simp
hence "❙⊥ ❙≈ ℐ(A ❙∨ B)" using fr2 ICdual dual_def eq_ext' conn by metis
hence "Br (A ❙∨ B)" using fr2 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: "Fr_1 ℱ ⟹ Fr_2 ℱ ⟹ Fr_4 ℱ ⟹ join_closed (λA. Fr A)" by (smt Br_Fr_join ADDI_a_def CF1a Cl_fr_def PF1 diff_def join_def meet_def pB2 pF1)

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: Int_fr_def conn)
lemma Disj_B: "∀A. Disj (ℬ A) (ℬ(❙─A))" using Br_fr_def unfolding conn by auto
lemma Disj_I: "∀A. Disj (ℐ A) (❙─A)" by (simp add: Int_fr_def conn)
lemma Disj_BCI: "Fr_2 ℱ ⟹ ∀A. Disj (ℬ(𝒞 A)) (ℐ(❙─A))" using Br_fr_def Cl_fr_def Fr_2_def Int_fr_def conn by metis
lemma Disj_CBI: "Fr_6 ℱ ⟹ Fr_4 ℱ ⟹ ∀A. Disj (𝒞(ℬ(❙─A))) (ℐ(❙─A))" by (metis Br_fr_def Cl_F IB_rel Int_br_def MONO_MULTa MULT_a_def eq_ext' monC conn)

text‹\noindent{Introduces 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 Cl_fr_def Sep_def conn by fastforce
lemma Sep_I: "Fr_1(ℱ) ⟹ Fr_2(ℱ) ⟹ Fr_4(ℱ) ⟹ ∀A. Sep (ℐ A) (ℐ (❙─A))" using Cl_fr_def pF4 Fr_2_def Int_fr_def unfolding Sep_def conn by metis
lemma Sep_sub: "Fr_6 ℱ  ⟹ ∀A B C D. Sep A B ∧ C ❙≼ A ∧ D ❙≼ B ⟶ Sep C D" using MONO_def monC unfolding Sep_def conn by smt
lemma Sep_Cl_diff: "Fr_6 ℱ ⟹ ∀A B. Cl(A) ∧ Cl(B) ⟶ Sep (A ❙↼ B) (B ❙↼ A)" using Fr_6_def pC2 unfolding Sep_def conn by smt
lemma Sep_Op_diff: "Fr_1b ℱ ⟹ Fr_2 ℱ ⟹ ∀A B. Op(A) ∧ Op(B) ⟶ Sep (A ❙↼ B) (B ❙↼ A)" proof -
assume fr1b:"Fr_1b ℱ" and fr2:"Fr_2 ℱ"
{ fix A B
from fr1b fr2 have aux: "let M=❙─A ; N=❙─B in (Cl(M) ∧ Cl(N) ⟶ Sep (M ❙↼ N) (N ❙↼ M))" using PF6 Sep_Cl_diff by simp
{ assume "Op(A) ∧ Op(B)"
hence "Cl(❙─A) ∧ Cl(❙─B)" using fr2 ClOpdual by simp
hence "Sep (❙─A ❙↼ ❙─B) (❙─B ❙↼ ❙─A)" using fr1b fr2 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: "Fr_1b ℱ ⟹ Fr_2 ℱ  ⟹ ∀A B. Op(A) ∧ Op(B) ∧ Disj A B ⟶ Sep A B" proof -
assume fr1b:"Fr_1b ℱ" and fr2:"Fr_2 ℱ"
{ fix A B
from fr1b fr2 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 "Fr_1a ℱ ⟹ Fr_2 ℱ ⟹ ∀A B C. Sep A B ∧ Sep A C ⟶ Sep A (B ❙∨ C)" using CF1a ADDI_a_def unfolding Sep_def conn by metis

text‹\noindent{Verifies a neighborhood-based definition of closure.}›
definition "nbhd A p ≡ ∃E. E ❙≼ A ∧ Op(E) ∧ (E p)"
lemma nbhd_def2: "Fr_1 ℱ ⟹ Fr_2 ℱ ⟹ Fr_4 ℱ ⟹ ∀A p. (nbhd A p) = (ℐ A p)" using pF4 MONO_def PF1 monI pI2 unfolding nbhd_def conn by smt

lemma C_def_lr: "Fr_1b ℱ ⟹ Fr_2 ℱ ⟹ Fr_4 ℱ ⟹ ∀A p. (𝒞 A p) ⟶ (∀E. (nbhd E p) ⟶ ¬(Disj E A))" using Cl_fr_def Fr_2_def Fr_6_def PF6 pF1 unfolding nbhd_def conn by smt
lemma C_def_rl: "Fr_1 ℱ ⟹ Fr_2 ℱ ⟹ Fr_4 ℱ ⟹ ∀A p. (𝒞 A p) ⟵ (∀E. (nbhd E p) ⟶ ¬(Disj E A))" using Cl_fr_def pF5 pA1 pB4 unfolding nbhd_def conn by smt
lemma C_def: "Fr_1 ℱ ⟹ Fr_2 ℱ ⟹ Fr_4 ℱ ⟹ ∀A p. (𝒞 A p) ⟷ (∀E. (nbhd E p) ⟶ ¬(Disj E A))" using C_def_lr C_def_rl PF1 by blast

text‹\noindent{Explore the Barcan and converse Barcan formulas.}›
lemma Barcan_I: "Fr_inf ℱ ⟹ ∀P. (❙∀x. ℐ(P x)) ❙≼ ℐ(❙∀x. P x)" using IF_inf Barcan1 by auto
lemma Barcan_C: "Fr_2 ℱ ⟹ Fr_inf ℱ ⟹ ∀P. 𝒞(❙∃x. P x) ❙≼ (❙∃x. 𝒞(P x))" using Fr_2_def CF_inf Barcan2 by metis
lemma CBarcan_I: "Fr_1b ℱ ⟹ ∀P. ℐ(❙∀x. P x)  ❙≼ (❙∀x. ℐ(P x))" by (metis (mono_tags, lifting) MONO_def monI)
lemma CBarcan_C: "Fr_6 ℱ ⟹ ∀P. (❙∃x. 𝒞(P x)) ❙≼ 𝒞(❙∃x. P x)"  by (metis (mono_tags, lifting) MONO_def monC)

end