Theory conditions_negative_infinitary

theory conditions_negative_infinitary
  imports conditions_negative conditions_positive_infinitary
begin

subsection ‹Infinitary Negative Conditions›

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

text‹Anti-distribution over infinite joins (suprema) or infinite anti-additivity (inADDI).›
definition inADDI::"('w σ ⇒ 'w σ) ⇒ bool" ("inADDI")
  where "inADDI φ  ≡ ∀S. φ(❙⋁S) ❙= ❙⋀⟦φ S⟧" 
definition inADDI_a::"('w σ ⇒ 'w σ) ⇒ bool" ("inADDI⇧^a")
  where "inADDI⇧^a φ ≡ ∀S. ❙⋀⟦φ S⟧ ❙≤ φ(❙⋁S)  " 
definition inADDI_b::"('w σ ⇒ 'w σ) ⇒ bool" ("inADDI⇧^b")
  where "inADDI⇧^b φ ≡ ∀S. φ(❙⋁S) ❙≤ ❙⋀⟦φ S⟧"

text‹Anti-distribution over infinite meets (infima) or infinite anti-multiplicativity (inMULT).›
definition inMULT::"('w σ ⇒ 'w σ) ⇒ bool" ("inMULT")
  where "inMULT φ  ≡ ∀S. φ(❙⋀S) ❙= ❙⋁⟦φ S⟧" 
definition inMULT_a::"('w σ ⇒ 'w σ) ⇒ bool" ("inMULT⇧^a")
  where "inMULT⇧^a φ ≡ ∀S. ❙⋁⟦φ S⟧ ❙≤ φ(❙⋀S)"
definition inMULT_b::"('w σ ⇒ 'w σ) ⇒ bool" ("inMULT⇧^b")
  where "inMULT⇧^b φ ≡ ∀S. φ(❙⋀S) ❙≤ ❙⋁⟦φ S⟧"

declare inADDI_def[cond] inADDI_a_def[cond] inADDI_b_def[cond]
        inMULT_def[cond] inMULT_a_def[cond] inMULT_b_def[cond]

lemma inADDI_char: "inADDI φ = (inADDI⇧^a φ ∧ inADDI⇧^b φ)" unfolding cond using setequ_char by blast
lemma inMULT_char: "inMULT φ = (inMULT⇧^a φ ∧ inMULT⇧^b φ)" unfolding cond using setequ_char by blast

text‹nADDI-b and inADDI-b are in fact equivalent.›
lemma inADDIb_equ: "inADDI⇧^b φ = nADDI⇧^b φ" proof -
  have lr: "inADDI⇧^b φ ⟹ nADDI⇧^b φ" proof - (*prove as a one-liner by instantiating inADDI_b_def with S=(λZ. Z=A ∨ Z=B)*)
  assume inaddib: "inADDI⇧^b φ"
  { fix A::"'a σ" and B::"'a σ" (* for some reason Isabelle doesn't like other letters as type variable. Why?*)
    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 infimum_def meet_def by auto
    have "φ(❙⋁?S) ❙≤ ❙⋀⟦φ ?S⟧" using inaddib inADDI_b_def by blast
    hence "φ(A ❙∨ B) ❙≤ (φ A) ❙∧ (φ B)" using p1 p2 by simp
  } thus ?thesis by (simp add: nADDI_b_def) qed
  have rl: "nADDI⇧^b φ ⟹ inADDI⇧^b φ" unfolding inADDI_b_def ANTI_nADDIb ANTI_def image_def
    by (smt (verit) glb_def inf_glb lower_bounds_def lub_def sup_lub upper_bounds_def)
  from lr rl show ?thesis by auto
qed
text‹nMULT-a and inMULT-a are also equivalent.›
lemma inMULTa_equ: "inMULT⇧^a φ = nMULT⇧^a φ" proof -
  have lr: "inMULT⇧^a φ ⟹ nMULT⇧^a φ" proof - (*prove as a one-liner by instantiating inMULT_a_def with S=(λZ. Z=A ∨ Z=B)*)
  assume inmulta: "inMULT⇧^a φ"
  { fix A::"'a σ" and B::"'a σ"
    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 supremum_def join_def by auto
    have "❙⋁⟦φ ?S⟧ ❙≤ φ(❙⋀?S)" using inmulta inMULT_a_def by blast    
    hence "(φ A) ❙∨ (φ B) ❙≤ φ(A ❙∧ B)" using p1 p2 by simp
  } thus ?thesis by (simp add: nMULT_a_def) qed
  have rl: "nMULT⇧^a φ ⟹ inMULT⇧^a φ" unfolding inMULT_a_def ANTI_nMULTa ANTI_def image_def
    by (smt (verit) glb_def inf_glb lower_bounds_def lub_def sup_lub upper_bounds_def)
  from lr rl show ?thesis by blast
qed

text‹Thus we have that ANTI, nADDI-b/inADDI-b and nMULT-a/inMULT-a are all equivalent.›
lemma ANTI_inADDIb: "inADDI⇧^b φ = ANTI φ" unfolding ANTI_nADDIb inADDIb_equ by simp
lemma ANTI_inMULTa: "inMULT⇧^a φ = ANTI φ" unfolding ANTI_nMULTa inMULTa_equ by simp


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

text‹Duality between inMULT-a and inADDI-b (an easy corollary from the previous equivalence).›
lemma inMULTa_inADDIb_dual1: "inMULT⇧^a φ = inADDI⇧^b φ⇧^d" by (simp add: nMULTa_nADDIb_dual1 inADDIb_equ inMULTa_equ)
lemma inMULTa_inADDIb_dual2: "inADDI⇧^b φ = inMULT⇧^a φ⇧^d" by (simp add: nMULTa_nADDIb_dual2 inADDIb_equ inMULTa_equ)
text‹Duality between inADDI-a and inMULT-b.›
lemma inADDIa_inMULTb_dual1: "inADDI⇧^a φ = inMULT⇧^b φ⇧^d" by (smt (z3) BA_cmpl_equ BA_cp dualcompl_invol inADDI_a_def iDM_a inMULT_b_def im_prop1 op_dual_def setequ_ext)
lemma inADDIa_inMULTb_dual2: "inMULT⇧^b φ = inADDI⇧^a φ⇧^d" by (simp add: dual_invol inADDIa_inMULTb_dual1)
text‹Duality between inADDI and inMULT.›
lemma inADDI_inMULT_dual1: "inADDI φ = inMULT φ⇧^d" using inADDI_char inADDIa_inMULTb_dual1 inMULT_char inMULTa_inADDIb_dual2 by blast
lemma inADDI_inMULT_dual2: "inMULT φ = inADDI φ⇧^d" by (simp add: dual_invol inADDI_inMULT_dual1)

text‹inADDI and inMULT are the 'complements' of iADDI and iMULT respectively.›
lemma inADDIa_compl: "iADDI⇧^a φ = inADDI⇧^a φ⇧^-" by (metis BA_cmpl_equ BA_cp iADDI_a_def iDM_a im_prop2 inADDI_a_def setequ_ext svfun_compl_def)
lemma inADDIb_compl: "iADDI⇧^b φ = inADDI⇧^b φ⇧^-" by (simp add: ANTI_MONO ANTI_inADDIb MONO_iADDIb)
lemma inADDI_compl: "iADDI φ = inADDI φ⇧^-" by (simp add: iADDI_char inADDI_char inADDIa_compl inADDIb_compl)
lemma inMULTa_compl: "iMULT⇧^a φ = inMULT⇧^a φ⇧^-" by (simp add: ANTI_MONO ANTI_inMULTa MONO_iMULTa)
lemma inMULTb_compl: "iMULT⇧^b φ = inMULT⇧^b φ⇧^-" by (metis dual_compl_char1 dual_compl_char2 iADDIa_iMULTb_dual2 inADDIa_compl inADDIa_inMULTb_dual2)
lemma inMULT_compl: "iMULT φ = inMULT φ⇧^-" by (simp add: iMULT_char inMULT_char inMULTa_compl inMULTb_compl)

text‹In fact, infinite anti-additivity (anti-multiplicativity) entails (dual) anti-normality:›
lemma inADDI_nNORM: "inADDI φ ⟶ nNORM φ" by (metis bottom_def inADDI_def inf_empty image_def nNORM_def setequ_ext sup_empty)
lemma inMULT_nDNRM: "inMULT φ ⟶ nDNRM φ" by (simp add: inADDI_inMULT_dual2 inADDI_nNORM nNOR_dual2)

end