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