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 ("(_¯)" [1000] 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σ)σ" ("_" [55]56) where "π  λw. X. (π X) w"
abbreviation mexists::"('tσ)σ" ("_" [55]56) where "π  λw. X. (π X) w"
text‹\noindent{To improve readability, we introduce for them an useful binder notation.}›
abbreviation mforallB (binder""[55]56) where "X. π X  π"
abbreviation mexistsB (binder""[55]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::"('tbool)('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σ)('tbool)(σ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] = RDπ" by (metis (full_types) pfunRange_restr_def infimum_def)
lemma Ra_restr_ex:  "Ra[π|D] = RDπ" 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: "(πγ) = RRa γ π" by (metis comp_apply pfunRange_def)
lemma Ra_ex_comp1:  "(πγ) = [π|Ra γ]N" by (metis comp_apply pfunRange_def)
lemma Ra_ex_comp2:  "(πγ) = RRa γ π" 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