# Theory sse_boolean_algebra_quantification

theory sse_boolean_algebra_quantification
imports sse_boolean_algebra
begin
hide_const(open) List.list.Nil no_notation List.list.Nil ("[]")  (*We have no use for lists... *)
hide_const(open) Relation.converse no_notation Relation.converse ("(_¯)"  999) (*..nor for relations in this work*)
nitpick_params[assms=true, user_axioms=true, show_all, expect=genuine, format=3] (*default Nitpick settings*)

subsection ‹Obtaining a complete Boolean Algebra›

text‹\noindent{Our aim is to obtain a complete Boolean algebra which we can use to interpret
quantified formulas (in the spirit of Boolean-valued models for set theory).}›

text‹\noindent{We start by defining infinite meet (infimum) and infinite join (supremum) operations,}›
definition infimum:: "(σ⇒bool)⇒σ" ("❙⋀_") where "❙⋀S ≡ λw. ∀X. S X ⟶ X w"
definition supremum::"(σ⇒bool)⇒σ" ("❙⋁_") where "❙⋁S ≡ λw. ∃X. S X  ∧  X w"

text‹\noindent{and show that the corresponding lattice is complete.}›
abbreviation "upper_bound U S ≡ ∀X. (S X) ⟶ X ❙≼ U"
abbreviation "lower_bound L S ≡ ∀X. (S X) ⟶ L ❙≼ X"
abbreviation "is_supremum U S ≡ upper_bound U S ∧ (∀X. upper_bound X S ⟶ U ❙≼ X)"
abbreviation "is_infimum  L S ≡ lower_bound L S ∧ (∀X. lower_bound X S ⟶ X ❙≼ L)"

lemma sup_char: "is_supremum ❙⋁S S" unfolding supremum_def by auto
lemma sup_ext: "∀S. ∃X. is_supremum X S" by (metis supremum_def)
lemma inf_char: "is_infimum ❙⋀S S" unfolding infimum_def by auto
lemma inf_ext: "∀S. ∃X. is_infimum X S" by (metis infimum_def)

text‹\noindent{We can check that being closed under supremum/infimum entails being closed under join/meet.}›
abbreviation "meet_closed S ≡  ∀X Y. (S X ∧ S Y) ⟶ S(X ❙∧ Y)"
abbreviation "join_closed S ≡  ∀X Y. (S X ∧ S Y) ⟶ S(X ❙∨ Y)"

abbreviation "nonEmpty S ≡ ∃x. S x"
abbreviation "contains S D ≡  ∀X. D X ⟶ S X"
abbreviation "infimum_closed S  ≡ ∀D. nonEmpty D ∧ contains S D ⟶ S(❙⋀D)"
abbreviation "supremum_closed S ≡ ∀D. nonEmpty D ∧ contains S D ⟶ S(❙⋁D)"

lemma inf_meet_closed: "∀S. infimum_closed S ⟶ meet_closed S" proof -
{ fix S
{ assume inf_closed: "infimum_closed S"
hence "meet_closed S" proof -
{ fix X::"σ" and Y::"σ"
let ?D="λZ. Z=X ∨ Z=Y"
{ assume "S X ∧ S Y"
hence "contains S ?D" by simp
moreover have "nonEmpty ?D" by auto
ultimately have "S(❙⋀?D)" using inf_closed by simp
hence "S(λw. ∀Z. (Z=X ∨ Z=Y) ⟶ Z w)" unfolding infimum_def by simp
moreover have "(λw. ∀Z. (Z=X ∨ Z=Y) ⟶ Z w) = (λw. X w ∧ Y w)" by auto
ultimately have "S(λw. X w ∧ Y w)" by simp
} hence "(S X ∧ S Y) ⟶ S(X ❙∧ Y)" unfolding conn by (rule impI)
} thus ?thesis by simp  qed
} hence "infimum_closed S ⟶ meet_closed S" by simp
} thus ?thesis by (rule allI)
qed
lemma sup_join_closed: "∀P. supremum_closed P ⟶ join_closed P" proof -
{ fix S
{ assume sup_closed: "supremum_closed S"
hence "join_closed S" proof -
{ fix X::"σ" and Y::"σ"
let ?D="λZ. Z=X ∨ Z=Y"
{ assume "S X ∧ S Y"
hence "contains S ?D" by simp
moreover have "nonEmpty ?D" by auto
ultimately have "S(❙⋁?D)" using sup_closed by simp
hence "S(λw. ∃Z. (Z=X ∨ Z=Y) ∧ Z w)" unfolding supremum_def by simp
moreover have "(λw. ∃Z. (Z=X ∨ Z=Y) ∧ Z w) = (λw. X w ∨ Y w)" by auto
ultimately have "S(λw. X w ∨ Y w)" by simp
} hence "(S X ∧ S Y) ⟶ S(X ❙∨ Y)" unfolding conn by (rule impI)
} thus ?thesis by simp qed
} hence "supremum_closed S ⟶ join_closed S" by simp
} thus ?thesis by (rule allI)
qed

subsection ‹Adding quantifiers (restricted and unrestricted)›

text‹\noindent{We can harness HOL to define quantification over individuals of arbitrary type (using polymorphism).
These (unrestricted) quantifiers take a propositional function and give a proposition.}›
abbreviation mforall::"('t⇒σ)⇒σ" ("❙∀_" 56) where "❙∀π ≡ λw. ∀X. (π X) w"
abbreviation mexists::"('t⇒σ)⇒σ" ("❙∃_" 56) where "❙∃π ≡ λw. ∃X. (π X) w"
text‹\noindent{To improve readability, we introduce for them an useful binder notation.}›
abbreviation mforallB (binder"❙∀"56) where "❙∀X. π X ≡ ❙∀π"
abbreviation mexistsB (binder"❙∃"56) where "❙∃X. π X ≡ ❙∃π"

(*TODO: is it possible to also add binder notation to the ones below?*)
text‹\noindent{Moreover, we define restricted quantifiers which take a 'functional domain' as additional parameter.
The latter is a propositional function that maps each element 'e' to the proposition 'e exists'.}›
abbreviation mforall_restr::"('t⇒σ)⇒('t⇒σ)⇒σ" ("❙∀⇧R(_)_") where "❙∀⇧R(δ)π ≡ λw.∀X. (δ X) w ⟶ (π X) w"
abbreviation mexists_restr::"('t⇒σ)⇒('t⇒σ)⇒σ" ("❙∃⇧R(_)_") where "❙∃⇧R(δ)π ≡ λw.∃X. (δ X) w  ∧  (π X) w"

subsection ‹Relating quantifiers with further operators›

text‹\noindent{The following 'type-lifting' function is useful for converting sets into 'rigid' propositional functions.}›
abbreviation lift_conv::"('t⇒bool)⇒('t⇒σ)" ("⦇_⦈") where "⦇S⦈ ≡ λX. λw. S X"

text‹\noindent{We introduce an useful operator: the range of a propositional function (resp. restricted over a domain),}›
definition pfunRange::"('t⇒σ)⇒(σ⇒bool)" ("Ra(_)") where "Ra(π) ≡ λY. ∃x. (π x) = Y"
definition pfunRange_restr::"('t⇒σ)⇒('t⇒bool)⇒(σ⇒bool)" ("Ra[_|_]") where "Ra[π|D] ≡ λY. ∃x. (D x) ∧ (π x) = Y"

text‹\noindent{and check that taking infinite joins/meets (suprema/infima) over the range of a propositional function
can be equivalently codified by using quantifiers. This is a quite useful simplifying relationship.}›
lemma Ra_all: "❙⋀Ra(π) = ❙∀π" by (metis (full_types) infimum_def pfunRange_def)
lemma Ra_ex:  "❙⋁Ra(π) = ❙∃π" by (metis (full_types) pfunRange_def supremum_def)
lemma Ra_restr_all: "❙⋀Ra[π|D] = ❙∀⇧R⦇D⦈π" by (metis (full_types) pfunRange_restr_def infimum_def)
lemma Ra_restr_ex:  "❙⋁Ra[π|D] = ❙∃⇧R⦇D⦈π" by (metis pfunRange_restr_def supremum_def)

text‹\noindent{We further introduce the positive (negative) restriction of a propositional function wrt. a domain,}›
abbreviation pfunRestr_pos::"('t⇒σ)⇒('t⇒σ)⇒('t⇒σ)" ("[_|_]⇧P") where "[π|δ]⇧P ≡ λX. λw. (δ X) w ⟶ (π X) w"
abbreviation pfunRestr_neg::"('t⇒σ)⇒('t⇒σ)⇒('t⇒σ)" ("[_|_]⇧N") where "[π|δ]⇧N ≡ λX. λw. (δ X) w  ∧  (π X) w"

text‹\noindent{and check that some additional simplifying relationships obtain.}›
lemma all_restr: "❙∀⇧R(δ)π = ❙∀[π|δ]⇧P" by simp
lemma ex_restr:  "❙∃⇧R(δ)π = ❙∃[π|δ]⇧N" by simp
lemma Ra_all_restr: "❙⋀Ra[π|D] = ❙∀[π|⦇D⦈]⇧P" using Ra_restr_all by blast
lemma Ra_ex_restr:  "❙⋁Ra[π|D] = ❙∃[π|⦇D⦈]⇧N" by (simp add: Ra_restr_ex)

text‹\noindent{Observe that using these operators has the advantage of allowing for binder notation,}›
lemma "❙∀X. [π|δ]⇧P X = ❙∀[π|δ]⇧P" by simp
lemma "❙∃X. [π|δ]⇧N X = ❙∃[π|δ]⇧N" by simp

text‹\noindent{noting that extra care should be taken when working with complements or negations;
always remember to switch P/N (positive/negative restriction) accordingly.}›
lemma "❙∀⇧R(δ)π  = ❙∀X.  [π|δ]⇧P X" by simp
lemma "❙∀⇧R(δ)π⇧c = ❙∀X. ❙─[π|δ]⇧N X" by (simp add: compl_def)
lemma "❙∃⇧R(δ)π  = ❙∃X.  [π|δ]⇧N X" by simp
lemma "❙∃⇧R(δ)π⇧c = ❙∃X. ❙─[π|δ]⇧P X" by (simp add: compl_def)

text‹\noindent{The previous definitions allow us to nicely characterize the interaction
between function composition and (restricted) quantification:}›
lemma Ra_all_comp1: "❙∀(π∘γ) = ❙∀[π|⦇Ra γ⦈]⇧P" by (metis comp_apply pfunRange_def)
lemma Ra_all_comp2: "❙∀(π∘γ) = ❙∀⇧R⦇Ra γ⦈ π" by (metis comp_apply pfunRange_def)
lemma Ra_ex_comp1:  "❙∃(π∘γ) = ❙∃[π|⦇Ra γ⦈]⇧N" by (metis comp_apply pfunRange_def)
lemma Ra_ex_comp2:  "❙∃(π∘γ) = ❙∃⇧R⦇Ra γ⦈ π" by (metis comp_apply pfunRange_def)

text‹\noindent{This useful operator returns for a given domain of propositions the domain of their complements:}›
definition dom_compl::"(σ⇒bool)⇒(σ⇒bool)" ("(_¯)") where "D¯ ≡ λX. ∃Y. (D Y) ∧ (X = ❙─Y)"
lemma dom_compl_def2: "D¯ = (λX. D(❙─X))" unfolding dom_compl_def by (metis comp_symm fun_upd_same)
lemma dom_compl_invol: "D = (D¯)¯" unfolding dom_compl_def by (metis comp_symm fun_upd_same)

text‹\noindent{We can now check an infinite variant of the De Morgan laws,}›
lemma iDM_a: "❙─(❙⋀S) = ❙⋁S¯" unfolding dom_compl_def2 infimum_def supremum_def using compl_def by force
lemma iDM_b:" ❙─(❙⋁S) = ❙⋀S¯" unfolding dom_compl_def2 infimum_def supremum_def using compl_def by force

text‹\noindent{and some useful dualities regarding the range of propositional functions (restricted wrt. a domain).}›
lemma Ra_compl: "Ra[π⇧c|D]  = Ra[π|D]¯" unfolding pfunRange_restr_def dom_compl_def by auto
lemma Ra_dual1: "Ra[π⇧d|D]  = Ra[π|D¯]¯" unfolding pfunRange_restr_def dom_compl_def using dual_def by auto
lemma Ra_dual2: "Ra[π⇧d|D]  = Ra[π⇧c|D¯]" unfolding pfunRange_restr_def dom_compl_def using dual_def by auto
lemma Ra_dual3: "Ra[π⇧d|D]¯ = Ra[π|D¯]" unfolding pfunRange_restr_def dom_compl_def using dual_def comp_symm by metis
lemma Ra_dual4: "Ra[π⇧d|D¯] = Ra[π|D]¯" using Ra_dual3 dual_symm by metis

text‹\noindent{Finally, we check some facts concerning duality for quantifiers.}›
lemma "❙∃π⇧c = ❙─(❙∀π)" using compl_def by auto
lemma "❙∀π⇧c = ❙─(❙∃π)" using compl_def by auto
lemma "❙∃X. ❙─π X = ❙─(❙∀X. π X)" using compl_def by auto
lemma "❙∀X. ❙─π X = ❙─(❙∃X. π X)" using compl_def by auto

lemma "❙∃⇧R(δ)π⇧c = ❙─(❙∀⇧R(δ)π)" using compl_def by auto
lemma "❙∀⇧R(δ)π⇧c = ❙─(❙∃⇧R(δ)π)" using compl_def by auto
lemma "❙∃X. ❙─[π|δ]⇧P X = ❙─(❙∀X. [π|δ]⇧P X)" using compl_def by auto
lemma "❙∀X. ❙─[π|δ]⇧P X = ❙─(❙∃X. [π|δ]⇧P X)" using compl_def by auto
lemma "❙∃X. ❙─[π|δ]⇧N X = ❙─(❙∀X. [π|δ]⇧N X)" using compl_def by auto
lemma "❙∀X. ❙─[π|δ]⇧N X = ❙─(❙∃X. [π|δ]⇧N X)" using compl_def by auto

text‹\noindent{Warning: Do not switch P and N when passing to the dual form.}›
lemma "❙∀X. [π|δ]⇧P X = ❙─(❙∃X. ❙─[π|δ]⇧N X)" nitpick oops ―‹ wrong: counterexample ›
lemma "❙∀X. [π|δ]⇧P X = ❙─(❙∃X. ❙─[π|δ]⇧P X)" using compl_def by auto ―‹ correct ›

end