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