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]
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