Theory sse_operation_negative_quantification

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

subsection ‹Definitions and interrelations (infinitary case)›

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

text‹\noindent{iDM: infinitary De Morgan laws.}›
abbreviation riDM1 ("iDM1⇧_ _") where "iDM1⇧S η  η(S)  Ra[η|S]"
abbreviation riDM2 ("iDM2⇧_ _") where "iDM2⇧S η  Ra[η|S]  η(S)"
abbreviation riDM3 ("iDM3⇧_ _") where "iDM3⇧S η  η(S)  Ra[η|S]"
abbreviation riDM4 ("iDM4⇧_ _") where "iDM4⇧S η  Ra[η|S]  η(S)"
definition "iDM1 η  S. iDM1⇧S η"
definition "iDM2 η  S. iDM2⇧S η"
definition "iDM3 η  S. iDM3⇧S η"
definition "iDM4 η  S. iDM4⇧S η"
declare iDM1_def[Defs] iDM2_def[Defs] iDM3_def[Defs] iDM4_def[Defs]

lemma CoPw_iDM1: "CoPw η  iDM1 η" unfolding Defs by (smt Ra_restr_all sup_char) 
lemma CoPw_iDM2: "CoPw η  iDM2 η" unfolding Defs by (smt Ra_restr_ex inf_char)
lemma CoP2_iDM3: "CoP2 η  iDM3 η" by (smt CoP2_def Ra_restr_ex iDM3_def inf_char)
lemma CoP1_iDM4: "CoP1 η  iDM4 η" by (smt CoP1_def Ra_restr_all iDM4_def sup_char)
lemma "XCoP η  iDM3 η" nitpick oops
lemma "XCoP η  iDM4 η" nitpick oops

text‹\noindent{DM1, DM2, iDM1, iDM2 and CoPw are equivalent.}›
lemma iDM1_rel: "iDM1 η  DM1 η" proof -
  assume idm1: "iDM1 η" 
   { fix a::"σ" and b::"σ"
     let ?S="λZ. Z=a  Z=b"
     have "Ra[η|?S] = R?S η" using Ra_restr_all by blast
     moreover have "R?S η = (η a)  (η b)" using meet_def by auto
     ultimately have "Ra[η|?S] = (η a)  (η b)" by simp
     moreover have "?S = a  b" using supremum_def join_def by auto
     moreover from idm1 have "η(?S)  Ra[η|?S]" by (simp add: iDM1_def)
     ultimately have "η(a  b)  (η a)  (η b)" by simp
   } thus ?thesis by (simp add: DM1_def)
 qed
lemma iDM2_rel: "iDM2 η  DM2 η" proof -
  assume idm2: "iDM2 η" 
   { fix a::"σ" and b::"σ"
     let ?S="λZ. Z=a  Z=b"
     have "Ra[η|?S] = R?S η" using Ra_restr_ex by blast
     moreover have "R?S η = (η a)  (η b)" using join_def by auto
     ultimately have "Ra[η|?S] = (η a)  (η b)" by simp
     moreover have "?S = a  b" using infimum_def meet_def by auto
     moreover from idm2 have "Ra[η|?S]  η(?S)" by (simp add: iDM2_def)
     ultimately have "(η a)  (η b)  η(a  b)" by auto
   } thus ?thesis by (simp add: DM2_def)
qed
lemma "DM1 η = iDM1 η" using CoPw_iDM1 DM1_CoPw iDM1_rel by blast
lemma "DM2 η = iDM2 η" using CoPw_iDM2 DM2_CoPw iDM2_rel by blast
lemma "iDM1 η = iDM2 η" using CoPw_iDM1 CoPw_iDM2 DM1_CoPw DM2_CoPw iDM1_rel iDM2_rel by blast

text‹\noindent{iDM3/4 entail their finitary variants but not the other way round.}›
lemma iDM3_rel: "iDM3 η  DM3 η" proof -
  assume idm3: "iDM3 η" 
   { fix a::"σ" and b::"σ"
     let ?S="λZ. Z=a  Z=b"
     have "Ra[η|?S] = R?S η" using Ra_restr_ex by blast
     moreover have "R?S η = (η a)  (η b)" using join_def by auto
     ultimately have "Ra[η|?S] = (η a)  (η b)" by simp
     moreover have "?S = a  b" using infimum_def meet_def by auto
     moreover from idm3 have "η(?S)  Ra[η|?S]" by (simp add: iDM3_def)
     ultimately have "η(a  b)  (η a)  (η b)" by auto
   } thus ?thesis by (simp add: DM3_def)
qed
lemma iDM4_rel: "iDM4 η  DM4 η" proof -
  assume idm4: "iDM4 η" 
   { fix a::"σ" and b::"σ"
     let ?S="λZ. Z=a  Z=b"
     have "Ra[η|?S] = R?S η" using Ra_restr_all by blast
     moreover have "R?S η = (η a)  (η b)" using meet_def by auto
     ultimately have "Ra[η|?S] = (η a)  (η b)" by simp
     moreover have "?S = a  b" using supremum_def join_def by auto
     moreover from idm4 have "Ra[η|?S]  η(?S)" by (simp add: iDM4_def)
     ultimately have "(η a)  (η b)  η(a  b)" by simp
   } thus ?thesis by (simp add: DM4_def)
 qed
lemma "DM3 η  iDM3 η" nitpick oops
lemma "DM4 η  iDM4 η" nitpick oops

text‹\noindent{Indeed the previous characterization of the infinitary De Morgan laws is fairly general and entails
the traditional version employing quantifiers (though not the other way round).}›
text‹\noindent{The first two variants DM1/2 follow easily from DM1/2, iDM1/2 or CoPw (all of them equivalent).}›
lemma iDM1_trad: "iDM1 η  π. η(x. π x)    (x. η(π x))" by (metis (mono_tags, lifting) CoPw_def DM1_CoPw iDM1_rel)
lemma iDM2_trad: "iDM2 η  π. (x. η(π x))  η(x. π x)" by (metis (mono_tags, lifting) CoPw_def DM2_CoPw iDM2_rel)

text‹\noindent{An analogous relationship holds for variants DM3/4, though the proof is less trivial.
To see how let us first consider an intermediate version of the De Morgan laws, obtained as a
particular case of the general variant above, with S as the range of a propositional function.}›
abbreviation "piDM1 π η  η(Ra(π))  Ra[η|Ra(π)]"
abbreviation "piDM2 π η  Ra[η|Ra(π)]  η(Ra(π))"
abbreviation "piDM3 π η  η(Ra(π))  Ra[η|Ra(π)]"
abbreviation "piDM4 π η  Ra[η|Ra(π)]  η(Ra(π))"

text‹\noindent{They are entailed (unidirectionally) by the general De Morgan laws.}›
lemma "iDM1 η  π. piDM1 π η" by (simp add: iDM1_def)
lemma "iDM2 η  π. piDM2 π η" by (simp add: iDM2_def)
lemma "iDM3 η  π. piDM3 π η" by (simp add: iDM3_def)
lemma "iDM4 η  π. piDM4 π η" by (simp add: iDM4_def)

text‹\noindent{Drawing upon the relationships shown previously we can rewrite the latter two as:}›
lemma iDM3_aux: "piDM3 π η  η(π)  [η|Ra π]N" unfolding Ra_all Ra_ex_restr by simp
lemma iDM4_aux: "piDM4 π η  [η|Ra π]P  η(π)" unfolding Ra_ex Ra_all_restr by simp

text‹\noindent{and thus finally obtain the desired formulas.}›
lemma iDM3_trad: "iDM3 η  π. η(x. π x)    (x. η(π x))" by (metis Ra_ex_comp2 iDM3_def iDM3_aux comp_apply)
lemma iDM4_trad: "iDM4 η  π. (x. η(π x))  η(x. π x)" by (metis Ra_all_comp1 iDM4_def iDM4_aux comp_apply)

end