Theory boolean_algebra_infinitary
theory boolean_algebra_infinitary
imports boolean_algebra_operators
begin
subsection ‹Encoding infinitary Boolean operations›
text‹Our aim is to encode complete Boolean algebras (of sets) which we can later be used to
interpret quantified formulas (somewhat in the spirit of Boolean-valued models for set theory).›
text‹We start by defining infinite meet (infimum) and infinite join (supremum) operations.›
definition infimum:: "('w σ)σ ⇒ 'w σ" ("❙⋀_")
where "❙⋀S ≡ λw. ∀X. S X ⟶ X w"
definition supremum::"('w σ)σ ⇒ 'w σ" ("❙⋁_")
where "❙⋁S ≡ λw. ∃X. S X ∧ X w"
declare infimum_def[conn] supremum_def[conn]
text‹Infimum and supremum satisfy an infinite variant of the De Morgan laws.›
lemma iDM_a: "❙─(❙⋀S) ❙= ❙⋁(S⇧d⇧-)" unfolding order conn conn2 by force
lemma iDM_b:" ❙─(❙⋁S) ❙= ❙⋀(S⇧d⇧-)" unfolding order conn conn2 by force
text‹We show that our encoded Boolean algebras are lattice-complete.
The functions below return the set of upper-/lower-bounds of a set of sets S (wrt. domain D).›
definition upper_bounds::"('w σ)σ ⇒ ('w σ)σ" ("ub")
where "ub S ≡ λU. ∀X. S X ⟶ X ❙≤ U"
definition upper_bounds_restr::"('w σ)σ ⇒ ('w σ)σ ⇒ ('w σ)σ" ("ub⇧_")
where "ub⇧D S ≡ λU. D U ∧ (∀X. S X ⟶ X ❙≤ U)"
definition lower_bounds::"('w σ)σ ⇒ ('w σ)σ" ("lb")
where "lb S ≡ λL. ∀X. S X ⟶ L ❙≤ X"
definition lower_bounds_restr::"('w σ)σ ⇒ ('w σ)σ ⇒ ('w σ)σ" ("lb⇧_")
where "lb⇧D S ≡ λL. D L ∧ (∀X. S X ⟶ L ❙≤ X)"
lemma ub_char: "ub S = (let D=❙⊤ in ub⇧D S) " by (simp add: top_def upper_bounds_def upper_bounds_restr_def)
lemma lb_char: "lb S = (let D=❙⊤ in lb⇧D S) " by (simp add: top_def lower_bounds_def lower_bounds_restr_def)
text‹Similarly, the functions below return the set of least/greatest upper-/lower-bounds for S (wrt. D).›
definition lub::"('w σ)σ ⇒ ('w σ)σ" ("lub")
where "lub S ≡ λU. ub S U ∧ (∀X. ub S X ⟶ U ❙≤ X)"
definition lub_restr::"('w σ)σ ⇒ ('w σ)σ ⇒ ('w σ)σ" ("lub⇧_")
where "lub⇧D S ≡ λU. ub⇧D S U ∧ (∀X. ub⇧D S X ⟶ U ❙≤ X)"
definition glb::"('w σ)σ ⇒ ('w σ)σ" ("glb")
where "glb S ≡ λL. lb S L ∧ (∀X. lb S X ⟶ X ❙≤ L)"
definition glb_restr::"('w σ)σ ⇒ ('w σ)σ ⇒ ('w σ)σ" ("glb⇧_")
where "glb⇧D S ≡ λL. lb⇧D S L ∧ (∀X. lb⇧D S X ⟶ X ❙≤ L)"
text‹Both pairs of definitions above are suitably related.
(Note that the term @{text "⊤"} below denotes the top element in the algebra of sets of sets (i.e. the powerset).)›
lemma lub_char: "lub S = (let D=❙⊤ in lub⇧D S) " by (simp add: lub_def lub_restr_def ub_char)
lemma glb_char: "glb S = (let D=❙⊤ in glb⇧D S) " by (simp add: glb_def glb_restr_def lb_char)
text‹Clearly, the notions of infimum/supremum correspond to least/greatest upper-/lower-bound.›
lemma sup_lub: "lub S ❙⋁S" unfolding lub_def upper_bounds_def supremum_def subset_def by blast
lemma sup_exist_unique: "∀S. ∃!X. lub S X" by (meson lub_def setequ_char setequ_ext sup_lub)
lemma inf_glb: "glb S ❙⋀S" unfolding glb_def lower_bounds_def infimum_def subset_def by blast
lemma inf_exist_unique: "∀S. ∃!X. glb S X" by (meson glb_def inf_glb setequ_char setequ_ext)
text‹The property of being closed under arbitrary (resp. nonempty) supremum/infimum.›
definition infimum_closed :: "('w σ)σ ⇒ bool"
where "infimum_closed S ≡ ∀D. D ❙≤ S ⟶ S(❙⋀D)"
definition supremum_closed :: "('w σ)σ ⇒ bool"
where "supremum_closed S ≡ ∀D. D ❙≤ S ⟶ S(❙⋁D)"
definition infimum_closed' :: "('w σ)σ ⇒ bool"
where"infimum_closed' S ≡ ∀D. nonEmpty D ∧ D ❙≤ S ⟶ S(❙⋀D)"
definition supremum_closed' :: "('w σ)σ ⇒ bool"
where "supremum_closed' S ≡ ∀D. nonEmpty D ∧ D ❙≤ S ⟶ S(❙⋁D)"
lemma inf_empty: "isEmpty S ⟹ ❙⋀S ❙= ❙⊤" unfolding order conn by simp
lemma sup_empty: "isEmpty S ⟹ ❙⋁S ❙= ❙⊥" unfolding order conn by simp
text‹Note that arbitrary infimum- (resp. supremum-) closed sets include the top (resp. bottom) element.›
lemma "infimum_closed S ⟹ S ❙⊤" unfolding infimum_closed_def conn order by force
lemma "supremum_closed S ⟹ S ❙⊥" unfolding supremum_closed_def conn order by force
text‹However, the above does not hold for non-empty infimum- (resp. supremum-) closed sets.›
lemma "infimum_closed' S ⟹ S ❙⊤" nitpick oops
lemma "supremum_closed' S ⟹ S ❙⊥" nitpick oops
text‹We have in fact the following characterizations for the notions above.›
lemma inf_closed_char: "infimum_closed S = (infimum_closed' S ∧ S ❙⊤)"
unfolding infimum_closed'_def infimum_closed_def by (metis bottom_def infimum_closed_def infimum_def setequ_char setequ_ext subset_def top_def)
lemma sup_closed_char: "supremum_closed S = (supremum_closed' S ∧ S ❙⊥)"
unfolding supremum_closed'_def supremum_closed_def by (metis (no_types, opaque_lifting) L14 L9 bottom_def setequ_ext subset_def supremum_def)
lemma inf_sup_closed_dc: "infimum_closed S = supremum_closed S⇧d⇧-" by (smt (verit) BA_dn iDM_a iDM_b infimum_closed_def setequ_ext sdfun_dcompl_def subset_def supremum_closed_def)
lemma inf_sup_closed_dc': "infimum_closed' S = supremum_closed' S⇧d⇧-" by (smt (verit) dualcompl_invol iDM_a infimum_closed'_def sdfun_dcompl_def setequ_ext subset_def supremum_closed'_def)
text‹We check some further properties.›
lemma fp_inf_sup_closed_dual: "infimum_closed (fp φ) = supremum_closed (fp φ⇧d)"
by (simp add: fp_dual inf_sup_closed_dc)
lemma fp_inf_sup_closed_dual': "infimum_closed' (fp φ) = supremum_closed' (fp φ⇧d)"
by (simp add: fp_dual inf_sup_closed_dc')
text‹We verify that being infimum-closed' (resp. supremum-closed') entails being meet-closed (resp. join-closed).›
lemma inf_meet_closed: "∀S. infimum_closed' S ⟶ meet_closed S" proof -
{ fix S::"'w σ ⇒ bool"
{ assume inf_closed: "infimum_closed' S"
hence "meet_closed S" proof -
{ fix X::"'w σ" and Y::"'w σ"
let ?D="λZ. Z=X ∨ Z=Y"
{ assume "S X ∧ S Y"
hence "?D ❙≤ S" using subset_def by blast
moreover have "nonEmpty ?D" by auto
ultimately have "S(❙⋀?D)" using inf_closed infimum_closed'_def by (smt (z3))
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 unfolding meet_closed_def 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::"'w σ ⇒ bool"
{ assume sup_closed: "supremum_closed' S"
hence "join_closed S" proof -
{ fix X::"'w σ" and Y::"'w σ"
let ?D="λZ. Z=X ∨ Z=Y"
{ assume "S X ∧ S Y"
hence "?D ❙≤ S" using subset_def by blast
moreover have "nonEmpty ?D" by auto
ultimately have "S(❙⋁?D)" using sup_closed supremum_closed'_def by (smt (z3))
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 unfolding join_closed_def by simp qed
} hence "supremum_closed' S ⟶ join_closed S" by simp
} thus ?thesis by (rule allI)
qed
end