Theory conditions_positive_infinitary

theory conditions_positive_infinitary
  imports conditions_positive boolean_algebra_infinitary
begin

subsection ‹Infinitary Positive Conditions›

text‹We define and interrelate infinitary variants for some previously introduced
 axiomatic conditions on operators.›

text‹Distribution over infinite joins (suprema) or infinite additivity (iADDI).›
definition iADDI::"('w σ ⇒ 'w σ) ⇒ bool" (‹iADDI›)
  where "iADDI φ   ≡ ∀S. φ(❙⋁S) ❙= ❙⋁⟦φ S⟧" 
definition iADDI_a::"('w σ ⇒ 'w σ) ⇒ bool" (‹iADDI⇧a›)
  where "iADDI⇧a φ ≡ ∀S. φ(❙⋁S) ❙≤ ❙⋁⟦φ S⟧" 
definition iADDI_b::"('w σ ⇒ 'w σ) ⇒ bool" (‹iADDI⇧b›)
  where "iADDI⇧b φ ≡ ∀S. ❙⋁⟦φ S⟧ ❙≤ φ(❙⋁S)"
text‹Distribution over infinite meets (infima) or infinite multiplicativity (iMULT).›
definition iMULT::"('w σ ⇒ 'w σ) ⇒ bool" (‹iMULT›)
  where "iMULT φ   ≡ ∀S. φ(❙⋀S) ❙= ❙⋀⟦φ S⟧" 
definition iMULT_a::"('w σ ⇒ 'w σ) ⇒ bool" (‹iMULT⇧a›)
  where "iMULT⇧a φ ≡ ∀S. φ(❙⋀S) ❙≤ ❙⋀⟦φ S⟧"
definition iMULT_b::"('w σ ⇒ 'w σ) ⇒ bool" (‹iMULT⇧b›)
  where "iMULT⇧b φ ≡ ∀S. ❙⋀⟦φ S⟧ ❙≤ φ(❙⋀S)"

declare iADDI_def[cond] iADDI_a_def[cond] iADDI_b_def[cond]
        iMULT_def[cond] iMULT_a_def[cond] iMULT_b_def[cond]

lemma iADDI_char: "iADDI φ = (iADDI⇧a φ ∧ iADDI⇧b φ)" unfolding cond using setequ_char by blast
lemma iMULT_char: "iMULT φ = (iMULT⇧a φ ∧ iMULT⇧b φ)" unfolding cond using setequ_char by blast

text‹ADDI-b and iADDI-b are in fact equivalent.›
lemma iADDIb_equ: "iADDI⇧b φ = ADDI⇧b φ" proof -
  have lr: "iADDI⇧b φ ⟹ ADDI⇧b φ" proof -
  assume iaddib: "iADDI⇧b φ"
  { fix A::"'a σ" and B::"'a σ" (*Isabelle forces us to use 'a as type variable name*)
    let ?S="λZ. Z=A ∨ Z=B"
    have "❙⋁?S = A ❙∨ B" unfolding supremum_def join_def by blast
    hence p1: "φ(❙⋁?S) = φ(A ❙∨ B)" by simp
    have "⟦φ ?S⟧ = (λZ. Z=(φ A) ∨ Z=(φ B))" unfolding image_def by metis
    hence p2: "❙⋁⟦φ ?S⟧ = (φ A) ❙∨ (φ B)" unfolding supremum_def join_def by auto
    have " ❙⋁⟦φ ?S⟧ ❙≤ φ(❙⋁?S)" using iaddib iADDI_b_def by blast    
    hence "(φ A) ❙∨ (φ B) ❙≤ φ(A ❙∨ B)" using p1 p2 by simp
  } thus ?thesis by (simp add: ADDI_b_def) qed
  have rl: "ADDI⇧b φ ⟹ iADDI⇧b φ" unfolding iADDI_b_def by (smt (verit) MONO_ADDIb MONO_def lub_def image_def sup_lub upper_bounds_def) 
  from lr rl show ?thesis by auto
qed
text‹MULT-a and iMULT-a are also equivalent.›
lemma iMULTa_equ: "iMULT⇧a φ = MULT⇧a φ" proof -
  have lr: "iMULT⇧a φ ⟹ MULT⇧a φ" proof -
  assume imulta: "iMULT⇧a φ"
  { fix A::"'a σ" and B::"'a σ" (*Isabelle forces us to use 'a as type variable name*)
    let ?S="λZ. Z=A ∨ Z=B"
    have "❙⋀?S = A ❙∧ B" unfolding infimum_def meet_def by blast
    hence p1: "φ(❙⋀?S) = φ(A ❙∧ B)" by simp
    have "⟦φ ?S⟧ = (λZ. Z=(φ A) ∨ Z=(φ B))" unfolding image_def by metis
    hence p2: "❙⋀⟦φ ?S⟧ = (φ A) ❙∧ (φ B)" unfolding infimum_def meet_def by auto
    have "φ(❙⋀?S) ❙≤ ❙⋀⟦φ ?S⟧" using imulta iMULT_a_def by blast    
    hence "φ(A ❙∧ B) ❙≤ (φ A) ❙∧ (φ B)" using p1 p2 by simp
  } thus ?thesis by (simp add: MULT_a_def) qed
  have rl: "MULT⇧a φ ⟹ iMULT⇧a φ" by (smt (verit) MONO_MULTa MONO_def glb_def iMULT_a_def inf_glb lower_bounds_def image_def)
  from lr rl show ?thesis by blast
qed

text‹Thus we have that MONO, ADDI-b/iADDI-b and MULT-a/iMULT-a are all equivalent.›
lemma MONO_iADDIb: "iADDI⇧b φ = MONO φ" unfolding MONO_ADDIb iADDIb_equ by simp
lemma MONO_iMULTa: "iMULT⇧a φ = MONO φ" unfolding MONO_MULTa iMULTa_equ by simp


text‹Below we prove several duality relationships between iADDI(a/b) and iMULT(a/b).›

text‹Duality between iMULT-a and iADDI-b (an easy corollary from the previous equivalence).›
lemma iMULTa_iADDIb_dual1: "iMULT⇧a φ = iADDI⇧b φ⇧d" by (simp add: MULTa_ADDIb_dual1 iADDIb_equ iMULTa_equ)
lemma iMULTa_iADDIb_dual2: "iADDI⇧b φ = iMULT⇧a φ⇧d" by (simp add: MULTa_ADDIb_dual2 iADDIb_equ iMULTa_equ)
text‹Duality between iADDI-a and iMULT-b.›
lemma iADDIa_iMULTb_dual1: "iADDI⇧a φ = iMULT⇧b φ⇧d" by (smt (z3) BA_cmpl_equ BA_cp dualcompl_invol iADDI_a_def iDM_a iMULT_b_def im_prop1 op_dual_def setequ_ext)
lemma iADDIa_iMULTb_dual2: "iMULT⇧b φ = iADDI⇧a φ⇧d" by (simp add: dual_invol iADDIa_iMULTb_dual1)
text‹Duality between iADDI and iMULT.›
lemma iADDI_iMULT_dual1: "iADDI φ = iMULT φ⇧d" using iADDI_char iADDIa_iMULTb_dual1 iMULT_char iMULTa_iADDIb_dual2 by blast
lemma iADDI_iMULT_dual2: "iMULT φ = iADDI φ⇧d" by (simp add: dual_invol iADDI_iMULT_dual1)

text‹In fact, infinite additivity (multiplicativity) entails (dual) normality:›
lemma iADDI_NORM: "iADDI φ ⟶ NORM φ" unfolding cond by (metis bottom_def image_def setequ_ext sup_empty)
lemma iMULT_DNRM: "iMULT φ ⟶ DNRM φ" by (simp add: NOR_dual2 iADDI_NORM iADDI_iMULT_dual2)

text‹Suitable conditions on an operation can make the set of its fixed-points closed under infinite meets/joins.›

lemma fp_sup_closed_cond1: "iADDI φ ⟶ supremum_closed (fp φ)" unfolding cond order supremum_closed_def fixpoints_def image_def by (smt (verit) supremum_def)
lemma fp_sup_closed_cond2: "iADDI⇧a φ ∧ EXPN φ ⟶ supremum_closed (fp φ)" unfolding cond by (smt (z3) fixpoints_def image_def setequ_char subset_def supremum_closed_def supremum_def)
lemma fp_sup_closed_cond3: "MONO φ ∧ CNTR φ ⟶ supremum_closed (fp φ)" unfolding cond by (smt (verit, del_insts) fixpoints_def lub_def setequ_char setequ_ext subset_def sup_lub supremum_closed_def upper_bounds_def)

lemma fp_inf_closed_cond1: "iMULT φ ⟶ infimum_closed (fp φ)" by (metis fp_dual fp_sup_closed_cond1 iADDI_iMULT_dual2 inf_sup_closed_dc)
lemma fp_inf_closed_cond2: "iMULT⇧b φ ∧ CNTR φ ⟶ infimum_closed (fp φ)" by (metis EXPN_CNTR_dual2 fp_dual fp_sup_closed_cond2 iADDIa_iMULTb_dual2 inf_sup_closed_dc)
lemma fp_inf_closed_cond3: "MONO φ ∧ EXPN φ ⟶ infimum_closed (fp φ)" by (metis EXPN_CNTR_dual1 MONO_dual fp_dual fp_sup_closed_cond3 inf_sup_closed_dc)

text‹OTOH, the converse conjectures have (finite) countermodels. They need additional assumptions.›
lemma "infimum_closed (fp φ) ⟶ iMULT φ" nitpick oops ―‹ countermodel found: needs further assumptions ›
lemma "supremum_closed (fp φ) ⟶ iADDI φ" nitpick oops ―‹ countermodel found: needs further assumptions ›
lemma fp_inf_closed_iMULT: "MONO φ ⟹ CNTR φ ⟹ IDEM⇧b φ ⟹ infimum_closed (fp φ) ⟶ iMULT φ"
proof -
assume mono: "MONO φ" and cntr: "CNTR φ" and idem:"IDEM⇧b φ" {
  assume ic:"infimum_closed (fp φ)" {
    fix S
    from ic have "∀D. D ❙≤ (fp φ) ⟶ (fp φ)(❙⋀D)" unfolding infimum_closed_def by simp
    hence "let D=⟦φ S⟧ in (∀X. D X ⟶ (X ❙= φ X)) ⟶ ❙⋀D ❙= φ ❙⋀D" by (simp add: fixpoints_def setequ_ext subset_def) 
    moreover from idem have "(∀X. ⟦φ S⟧ X ⟶ (X ❙= φ X))" by (metis (mono_tags, lifting) CNTR_def IDEM_b_def cntr image_def setequ_char)
    ultimately have aux: "❙⋀(⟦φ S⟧) ❙= φ(❙⋀⟦φ S⟧)" by meson
    from cntr have "❙⋀⟦φ S⟧ ❙≤ ❙⋀S" by (smt (verit, best) CNTR_def image_def infimum_def subset_def)
    hence "φ(❙⋀⟦φ S⟧) ❙≤ φ(❙⋀S)" using mono by (simp add: MONO_def) 
    from this aux have "❙⋀⟦φ S⟧ ❙≤ φ(❙⋀S)" by (simp add: setequ_ext)
  } hence "infimum_closed (fp φ) ⟶ iMULT φ" by (simp add: MONO_iMULTa iMULT_b_def iMULT_char mono)
} thus ?thesis by simp 
qed
lemma fp_sup_closed_iADDI: "MONO φ ⟹ EXPN φ ⟹ IDEM⇧a φ ⟹ supremum_closed (fp φ) ⟶ iADDI φ" 
  (* by (metis EXPN_CNTR_dual1 IDEM_dual2 MONO_dual dual_invol fp_inf_closed_iMULT fp_inf_sup_closed_dual iADDI_iMULT_dual1) *)
proof -
assume mono: "MONO φ" and expn: "EXPN φ" and idem:"IDEM⇧a φ" {
  assume sc:"supremum_closed (fp φ)" {
    fix S
    from sc have "∀D. D ❙≤ (fp φ) ⟶ (fp φ)(❙⋁D)" unfolding supremum_closed_def by simp
    hence "let D=⟦φ S⟧ in (∀X. D X ⟶ (X ❙= φ X)) ⟶ ❙⋁D ❙= φ ❙⋁D" by (simp add: fixpoints_def setequ_ext subset_def)
    moreover have "(∀X. ⟦φ S⟧ X ⟶ (X ❙= φ X))" by (metis (mono_tags, lifting) EXPN_def IDEM_a_def expn idem image_def setequ_char)
    ultimately have aux: "❙⋁(⟦φ S⟧) ❙= φ(❙⋁⟦φ S⟧)" by meson
    have "❙⋁S ❙≤ ❙⋁⟦φ S⟧" by (metis EXPN_CNTR_dual1 EXPN_def IDEM_dual1 MONO_dual dual_invol expn fp_inf_closed_iMULT fp_inf_sup_closed_dual iADDI_def iADDI_iMULT_dual1 idem mono sc setequ_ext)
    hence "φ(❙⋁S) ❙≤ φ(❙⋁⟦φ S⟧)" using mono by (simp add: MONO_def) 
    from this aux have "φ(❙⋁S) ❙≤ ❙⋁⟦φ S⟧" by (metis setequ_ext)
  } hence "supremum_closed (fp φ) ⟶ iADDI φ" by (simp add: MONO_ADDIb iADDI_a_def iADDI_char iADDIb_equ mono)
} thus ?thesis by simp
qed

section ‹Alexandrov topologies and (generalized) specialization preorders›

text‹A topology is called 'Alexandrov' (after the Russian mathematician Pavel Alexandrov) if the intersection
(resp. union) of any (finite or infinite) family of open (resp. closed) sets is open (resp. closed);
in algebraic terms, this means that the set of fixed points of the interior (closure) operation is closed
under infinite meets (joins). Another common algebraic formulation requires the closure (interior) operation
to satisfy the infinitary variants of additivity (multiplicativity), i.e. iADDI (iMULT) as introduced before.

In the literature, the well-known Kuratowski conditions for the closure (resp. interior) operation are assumed,
namely: ADDI, EXPN, NORM, IDEM (resp. MULT, CNTR, DNRM, IDEM). This makes both formulations equivalent.
However, this is not the case in general if those conditions become negotiable.›

text‹Alexandrov topologies have interesting properties relating them to the semantics of modal logic.
Assuming Kuratowski conditions, Alexandrov topological operations defined on subsets of S are in one-to-one
correspondence with preorders on S; in topological terms, Alexandrov topologies are uniquely determined by
their specialization preorders. Since we do not presuppose any Kuratowski conditions to begin with, the
preorders in question are in general not even transitive. Here we just call them 'reachability relations'.
We will still call (generalized) closure/interior-like operations as such (for lack of a better name).
We explore minimal conditions under which some relevant results for the semantics of modal logic obtain.›

text‹Closure/interior(-like) operators can be derived from an arbitrary relation (as in modal logic).›
definition Cl_rel::"('w ⇒ 'w ⇒ bool) ⇒ ('w σ ⇒ 'w σ)" (‹𝒞[_]›) 
  where "𝒞[R] ≡ λA. λw. ∃v. R w v ∧ A v"
definition Int_rel::"('w ⇒ 'w ⇒ bool) ⇒ ('w σ ⇒ 'w σ)" (‹ℐ[_]›) 
  where "ℐ[R] ≡ λA. λw. ∀v. R w v ⟶ A v"

text‹Duality between interior and closure follows directly:›
lemma dual_CI: "𝒞[R] = ℐ[R]⇧d" by (simp add: Cl_rel_def Int_rel_def compl_def op_dual_def setequ_char)

text‹We explore minimal conditions of the reachability relation under which some operation's conditions obtain.› 
text‹Define some relevant properties of relations: ›
abbreviation "serial R  ≡ ∀x. ∃y. R x y"
abbreviation "reflexive R  ≡ ∀x. R x x"
abbreviation "transitive R ≡ ∀x y z. R x y ∧ R y z ⟶ R x z"
abbreviation "antisymmetric R  ≡ ∀x y. R x y ∧ R y x ⟶ x = y"
abbreviation "symmetric R  ≡ ∀x y. R x y ⟶ R y x"

lemma rC1: "iADDI 𝒞[R]" unfolding iADDI_def Cl_rel_def image_def supremum_def using setequ_def by fastforce
lemma rC2: "reflexive R = EXPN 𝒞[R]" by (metis (full_types) CNTR_def EXPN_CNTR_dual2 Int_rel_def dual_CI subset_def)
lemma rC3: "NORM 𝒞[R]" by (simp add: iADDI_NORM rC1)
lemma rC4: "transitive R = IDEM⇧a 𝒞[R]" proof -
  have l2r: "transitive R ⟶ IDEM⇧a 𝒞[R]"  by (smt (verit, best) Cl_rel_def IDEM_a_def subset_def)
  have r2l: "IDEM⇧a 𝒞[R] ⟶ transitive R" unfolding Cl_rel_def IDEM_a_def subset_def using compl_def by force
  from l2r r2l show ?thesis by blast
qed


text‹A reachability (specialization) relation (preorder) can be derived from a given operation (intended as a closure-like operation).›
definition ℛ::"('w σ ⇒ 'w σ) ⇒ ('w ⇒ 'w ⇒ bool)" (‹ℛ[_]›) 
  where "ℛ[φ] ≡ λw v. φ (λx. x = v) w"

text‹Preorder properties of the reachability relation follow from the corresponding operation's conditions.›
lemma rel_refl: "EXPN φ ⟶ reflexive ℛ[φ]" by (simp add: EXPN_def ℛ_def subset_def)
lemma rel_trans: "MONO φ ∧ IDEM⇧a φ ⟶ transitive ℛ[φ]" by (smt (verit, best) IDEM_a_def MONO_def ℛ_def subset_def)
lemma "IDEM⇧a φ ⟶ transitive ℛ[φ]" nitpick oops ―‹ counterexample ›

(*The converse directions do not hold*)
lemma "reflexive ℛ[φ] ⟶ EXPN φ" nitpick oops ―‹ counterexample ›
lemma "transitive ℛ[φ] ⟶ IDEM⇧a φ" nitpick oops ―‹ counterexample ›
lemma "transitive ℛ[φ] ⟶ MONO φ" nitpick oops ―‹ counterexample ›

text‹However, we can obtain finite countermodels for antisymmetry and symmetry given all relevant conditions.
We will revisit this issue later and examine their relation with the topological separation axioms T0 and T1 resp.›
lemma "iADDI φ ⟹ EXPN φ ⟹ IDEM⇧a φ ⟹ antisymmetric ℛ[φ]" nitpick oops ―‹ counterexample ›
lemma "iADDI φ ⟹ EXPN φ ⟹ IDEM⇧a φ ⟹ symmetric ℛ[φ]" nitpick oops ―‹ counterexample ›

text‹As mentioned previously, Alexandrov closure (and by duality interior) operations correspond to 
specialization orderings (reachability relations).
It is worth mentioning that in Alexandrov topologies every point has a minimal/smallest neighborhood,
namely the set of points related to it by the specialization preorder (reachability relation).
We examine below  minimal conditions under which these relations obtain.›

lemma Cl_rel'_a:   "MONO φ ⟶ (∀A. 𝒞[ℛ[φ]] A ❙≤ φ A)" unfolding Cl_rel_def MONO_def ℛ_def by (smt (verit, ccfv_SIG) subset_def)
lemma Cl_rel'_b: "iADDI⇧a φ ⟶ (∀A. φ A ❙≤ 𝒞[ℛ[φ]] A)" proof -
{ assume iaddia: "iADDI⇧a φ"
  { fix A::"'a σ"
    let ?S="λB. ∃w. A w ∧ B=(λu. u=w)"
    have "A ❙= (❙⋁?S)" unfolding supremum_def setequ_def by auto
    hence "φ(A) ❙= φ(❙⋁?S)" by (simp add: setequ_ext)
    moreover have "❙⋁⟦φ ?S⟧ ❙= 𝒞[ℛ[φ]] A" by (smt (verit) Cl_rel_def ℛ_def image_def setequ_def supremum_def)
    moreover from iaddia have "φ(❙⋁?S) ❙≤ ❙⋁⟦φ ?S⟧" unfolding iADDI_a_def by simp
    ultimately have "φ A ❙≤ 𝒞[ℛ[φ]] A" by (simp add: setequ_ext)
} } thus ?thesis by simp
qed
lemma Cl_rel': "iADDI φ ⟶ φ ❙=⇧: 𝒞[ℛ[φ]]" by (simp add: MONO_iADDIb iADDI_char setequ_char Cl_rel'_a Cl_rel'_b svfun_equ_def)
lemma Cl_rel: "iADDI φ ⟷ φ = 𝒞[ℛ[φ]]" using Cl_rel' by (metis rC1 svfun_equ_ext)

text‹It is instructive to expand the definitions in the above result:›
lemma "iADDI φ ⟷ (∀A. ∀w. (φ A) w ⟷ (∃v. A v ∧ φ (λx. x=v) w))" oops

text‹Closure (interior) operations derived from relations are thus closed under infinite joins (meets).›
lemma "supremum_closed (fp 𝒞[R])" by (simp add: fp_sup_closed_cond1 rC1)
lemma "infimum_closed  (fp ℐ[R])" by (metis dual_CI fp_inf_closed_cond1 iADDI_iMULT_dual2 rC1)


text‹We can now revisit the relationship between (anti)symmetry and the separation axioms T1 and T0.›

text‹T0: any two distinct points in the space can be separated by a closed (or open) set (i.e. containing one point and not the other).›
abbreviation "T0 𝒞 ≡ (∀p q. p ≠ q ⟶ (∃G. (fp 𝒞) G ∧ ¬(G p ⟷ G q)))"
text‹T1: any two distinct points can be separated by (two not necessarily disjoint) closed (or open) sets.›
abbreviation "T1 𝒞 ≡ (∀p q. p ≠ q ⟶ (∃G H. (fp 𝒞) G ∧ (fp 𝒞) H ∧ G p ∧ ¬G q ∧ H q ∧ ¬H p))"

text‹We can (sanity) check that T1 entails T0 but not viceversa.›
lemma "T1 𝒞 ⟹ T0 𝒞" by meson
lemma "T0 𝒞 ⟹ T1 𝒞" nitpick oops ―‹ counterexample ›


text‹Under appropriate conditions, T0-separation corresponds to antisymmetry of the specialization relation (here an ordering).›
lemma "T0 𝒞 ⟷ antisymmetric ℛ[𝒞]" nitpick oops (*counterexample*)
lemma T0_antisymm_a: "MONO 𝒞 ⟹ T0 𝒞 ⟶ antisymmetric ℛ[𝒞]" by (smt (verit, best) Cl_rel'_a Cl_rel_def fixpoints_def setequ_ext subset_def)
lemma T0_antisymm_b: "EXPN 𝒞 ⟹ IDEM⇧a 𝒞 ⟹ antisymmetric ℛ[𝒞] ⟶ T0 𝒞" by (metis EXPN_impl_IDEM_b IDEM_char IDEM_def ℛ_def fixpoints_def rel_refl)
lemma T0_antisymm: "MONO 𝒞 ⟹ EXPN 𝒞 ⟹ IDEM⇧a 𝒞 ⟹ T0 𝒞 = antisymmetric ℛ[𝒞]" using T0_antisymm_a T0_antisymm_b by fastforce

text‹Also, under the appropriate conditions, T1-separation corresponds to symmetry of the specialization relation.›
lemma T1_symm_a: "MONO 𝒞 ⟹ T1 𝒞 ⟶ symmetric ℛ[𝒞]" by (metis (mono_tags, opaque_lifting) Cl_rel'_a Cl_rel_def fixpoints_def setequ_ext subset_def)
lemma T1_symm_b: "MONO 𝒞 ⟹ EXPN 𝒞 ⟹ T0 𝒞 ⟹ symmetric ℛ[𝒞] ⟶ T1 𝒞" by (smt (verit, ccfv_SIG) T0_antisymm_a ℛ_def fixpoints_def rel_refl setequ_def)
lemma T1_symm: "MONO 𝒞 ⟹ EXPN 𝒞 ⟹ T0 𝒞 ⟹ symmetric ℛ[𝒞] = T1 𝒞" using T1_symm_a T1_symm_b by (smt (verit, ccfv_threshold))

end