Theory sse_operation_positive_quantification

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


subsection ‹Definitions (infinitary case)›

text‹\noindent{We define and interrelate infinitary variants for some previously introduced ('positive') conditions 
on operations and show how they relate to quantifiers as previously defined.}›

text‹\noindent{Distribution over infinite meets (infima) or infinite multiplicativity (iMULT).}›
definition "iMULT φ   ≡ ∀S. φ(❙⋀S) ❙≈ ❙⋀Ra[φ|S]" 
definition "iMULT_a φ ≡ ∀S. φ(❙⋀S) ❙≼ ❙⋀Ra[φ|S]"
definition "iMULT_b φ ≡ ∀S. φ(❙⋀S) ❙≽ ❙⋀Ra[φ|S]"

text‹\noindent{Distribution over infinite joins (suprema) or infinite additivity (iADDI).}›
definition "iADDI φ   ≡ ∀S. φ(❙⋁S) ❙≈ ❙⋁Ra[φ|S]" 
definition "iADDI_a φ ≡ ∀S. φ(❙⋁S) ❙≼ ❙⋁Ra[φ|S]" 
definition "iADDI_b φ ≡ ∀S. φ(❙⋁S) ❙≽ ❙⋁Ra[φ|S]"


subsection ‹Relations among conditions (infinitary case)›

text‹\noindent{We start by noting that there is a duality between iADDI-a and iMULT-b.}›
lemma iADDI_MULT_dual1: "iADDI_a φ ⟹ iMULT_b φ⇧d" unfolding iADDI_a_def iMULT_b_def by (metis compl_def dual_def iDM_a iDM_b Ra_dual1)
lemma iADDI_MULT_dual2: "iMULT_b φ ⟹ iADDI_a φ⇧d" unfolding iADDI_a_def iMULT_b_def by (metis compl_def dual_def iDM_b Ra_dual3)

text‹\noindent{MULT-a and iMULT-a are equivalent.}›
lemma iMULTa_rel: "iMULT_a φ = MULT_a φ" proof -
  have lr: "iMULT_a φ ⟹ MULT_a φ" proof -
  assume imulta: "iMULT_a φ"
  { fix A::"σ" and B::"σ"
    let ?S="λZ. Z=A ∨ Z=B"
    from imulta have "φ(❙⋀?S) ❙≼ ❙∀⇧R⦇?S⦈ φ" by (simp add: iMULT_a_def Ra_restr_all)
    moreover have "❙⋀?S = A ❙∧ B" using infimum_def meet_def by auto
    moreover have "❙∀⇧R⦇?S⦈ φ = (φ A) ❙∧ (φ B)" using meet_def by auto
    ultimately have "φ(A ❙∧ B) ❙≼ (φ A) ❙∧ (φ B)" by smt
  } thus ?thesis by (simp add: MULT_a_def) qed
  have rl: "MULT_a φ ⟹ iMULT_a φ" by (smt MONO_def MONO_MULTa Ra_restr_all iMULT_a_def inf_char)
  from lr rl show ?thesis by auto
qed
text‹\noindent{ADDI-b and iADDI-b are equivalent.}›
lemma iADDIb_rel: "iADDI_b φ = ADDI_b φ" proof -
  have lr: "iADDI_b φ ⟹ ADDI_b φ" proof -
  assume iaddib: "iADDI_b φ"
  { fix A::"σ" and B::"σ"
    let ?S="λZ. Z=A ∨ Z=B"
    from iaddib have "φ(❙⋁?S) ❙≽ ❙∃⇧R⦇?S⦈(φ)" by (simp add: iADDI_b_def Ra_restr_ex)
    moreover have "❙⋁?S = A ❙∨ B" using supremum_def join_def by auto
    moreover have "❙∃⇧R⦇?S⦈(φ) = (φ A) ❙∨ (φ B)" using join_def by auto
    ultimately have "φ(A ❙∨ B) ❙≽ (φ A) ❙∨ (φ B)" by smt
  } thus ?thesis by (simp add: ADDI_b_def) qed
  have rl: "ADDI_b φ ⟹ iADDI_b φ" by (smt MONO_def MONO_ADDIb Ra_restr_ex iADDI_b_def sup_char)
  from lr rl show ?thesis by auto
qed

text‹\noindent{Thus we have that MONO, MULT-a/iMULT-a and ADDI-b/iADDI-b are all equivalent.}›
lemma MONO_iADDIb: "MONO φ = iADDI_b φ" using MONO_ADDIb iADDIb_rel by simp
lemma MONO_iMULTa: "MONO φ = iMULT_a φ" using MONO_MULTa iMULTa_rel by simp
lemma iADDI_b_iMULTa: "iADDI_b φ = iMULT_a φ" using MONO_iADDIb MONO_iMULTa by auto

lemma PI_imult: "MONO φ ⟹ iMULT_b φ ⟹ iMULT φ" using MONO_MULTa iMULT_a_def iMULT_b_def iMULT_def iMULTa_rel by auto
lemma PC_iaddi: "MONO φ ⟹ iADDI_a φ ⟹ iADDI φ"  using MONO_ADDIb iADDI_a_def iADDI_b_def iADDI_def iADDIb_rel by auto

text‹\noindent{Interestingly, we can show that suitable (infinitary) conditions on an operation can make the set
of its fixed points closed under infinite meets/joins.}›
lemma fp_inf_closed: "MONO φ ⟹ iMULT_b φ ⟹ infimum_closed (fp φ)" by (metis (full_types) PI_imult Ra_restr_all iMULT_def infimum_def)
lemma fp_sup_closed: "MONO φ ⟹ iADDI_a φ ⟹ supremum_closed (fp φ)" by (metis (full_types) PC_iaddi Ra_restr_ex iADDI_def supremum_def) 


subsection ‹Exploring the Barcan formula and its converse›

text‹\noindent{The converse Barcan formula follows readily from monotonicity.}›
lemma CBarcan1: "MONO φ ⟹ ∀π.  φ(❙∀x. π x)  ❙≼ (❙∀x. φ(π x))" by (metis (mono_tags, lifting) MONO_def)
lemma CBarcan2: "MONO φ ⟹ ∀π. (❙∃x. φ(π x)) ❙≼ φ(❙∃x. π x)" by (metis (mono_tags, lifting) MONO_def)

text‹\noindent{However, the Barcan formula requires a stronger assumption (of an infinitary character).}›
lemma Barcan1: "iMULT_b φ ⟹ ∀π. (❙∀x. φ(π x)) ❙≼ φ(❙∀x. π x)" proof -
  assume imultb: "iMULT_b φ"
  { fix π::"'a⇒σ"
    from imultb have "(❙⋀Ra(φ∘π)) ❙≼ φ(❙⋀Ra(π))" unfolding iMULT_b_def by (smt comp_apply infimum_def pfunRange_def pfunRange_restr_def)
    moreover have "❙⋀Ra(π) = (❙∀x. π x)" unfolding Ra_all by simp
    moreover have "❙⋀Ra(φ∘π) = (❙∀x. φ(π x))" unfolding Ra_all by simp
    ultimately have "(❙∀x. φ(π x)) ❙≼ φ(❙∀x. π x)" by simp
  } thus ?thesis by simp
qed
lemma Barcan2: "iADDI_a φ ⟹ ∀π. φ(❙∃x. π x) ❙≼ (❙∃x. φ(π x))" proof -
  assume iaddia: "iADDI_a φ"
  { fix π::"'a⇒σ"
    from iaddia have "φ(❙⋁Ra(π)) ❙≼ (❙⋁Ra(φ∘π))" unfolding iADDI_a_def Ra_restr_ex by (smt fcomp_comp fcomp_def pfunRange_def sup_char)
    moreover have "❙⋁Ra(π) = (❙∃x. π x)" unfolding Ra_ex by simp
    moreover have "❙⋁Ra(φ∘π) = (❙∃x. φ(π x))" unfolding Ra_ex by simp
    ultimately have "φ(❙∃x. π x) ❙≼ (❙∃x. φ(π x))" by simp
  } thus ?thesis by simp
qed

end