Theory boolean_algebra

theory boolean_algebra
  imports Main
begin

(*-----------------------------------*)
text‹Technical configuration›
declare[[smt_timeout=30]]
declare[[show_types]]
(* declare[[syntax_ambiguity_warning=false]] *)
sledgehammer_params[isar_proof=false]
nitpick_params[assms=true, user_axioms=true, show_all, expect=genuine, format=3, atoms=a b c d] (*default Nitpick settings*)
text‹We hide some Isabelle/HOL notation from the libraries (which we don't use) to avoid overloading›
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*)
hide_const(open) Fun.comp no_notation Fun.comp (infixl "∘" 55) (*we redefine function composition below*)
hide_const(open) Groups.plus_class.plus no_notation Groups.plus_class.plus (infixl "+" 65) (*we don't use this*)
hide_const(open) Groups.times_class.times no_notation Groups.times_class.times (infixl "*" 70) (*we don't use this*)
hide_const(open) Groups.minus_class.minus no_notation Groups.minus_class.minus (infixl "-" 65) (*we don't use this*)
hide_const(open) Groups.uminus_class.uminus no_notation Groups.uminus_class.uminus ("- _" [81] 80) (*we don't use this*)
(*-----------------------------------*)

section ‹Shallow semantical embedding of (a logic of) Boolean algebras›

text‹We encode Boolean algebras via their (Stone) representation as algebras of sets ('fields of sets').
This means that each element of (the carrier of) the algebra will be a set of 'points'.
Inspired by the 'propositions as sets of worlds' paradigm from modal logic, we may think of points 
as being 'worlds', and thus of the elements of our Boolean algebras as 'propositions'.
Of course, this is just one among many possible interpretations, and nothing stops us from thinking 
of points as any other kind of object (e.g., they can be sets, functions, sets of functions, etc.).
›

text‹We utilize a particular naming convention: The type parameter 'w is employed for the
domain/universe of 'points'. We conveniently introduce the (parametric) type-alias @{text "('w)σ"} 
as shorthand for @{text "'w⇒bool"}. Hence, the elements of our algebra are objects of type @{text "('w)σ"},
and thus correspond to (characteristic functions of) sets of 'points'.
Set-valued (resp. set-domain) functions are thus functions that have sets as their codomain (resp. domain),
they are basically anything with a (parametric) type @{text "'a⇒('w)σ"} (resp. @{text "('w)σ⇒'a)"}.›

text‹Type for (characteristic functions of) sets (of 'points')›
type_synonym 'w σ = ‹'w ⇒ bool›

text‹In the sequel, we will (try to) enforce the following naming convention:›

text‹(i) Upper-case latin letters (A, B, D, M, P, S, X, etc.) denote arbitrary sets (type @{text "('w)σ"}).
We will employ lower-case letters (p, q, x, w, etc.) to denote variables playing the role of 'points'.
In some contexts, the letters S and D will be employed to denote sets/domains of sets (of 'points').›

text‹(ii) Greek letters denote arbitrary set-valued functions (type @{text "'a⇒('w)σ"}).
We employ the letters @{text "φ, ψ and η"} to denote arbitrary unary operations
(with type @{text "('w)σ⇒('w)σ)"}.›

text‹(iii) Upper-case calligraphic letters @{text "(ℬ, ℐ, 𝒞, ℱ, etc.)"} are reserved for unary operations that are
intended to act as 'topological operators' in the given context.›

subsection ‹Encoding Boolean operations›

text‹Standard inclusion-based order structure on sets.›
definition subset::"'w σ ⇒ 'w σ ⇒ bool" (infixr "❙≤" 45) 
  where "A ❙≤ B ≡ ∀p. A p ⟶ B p"
definition setequ::"'w σ ⇒ 'w σ ⇒ bool" (infixr "❙=" 45) 
  where "A ❙= B ≡ ∀p. A p ⟷ B p"

named_theorems order (*to group together order-related definitions*)
declare setequ_def[order] subset_def[order]

lemma subset_char1: "(A ❙≤ B) = (∀C. B ❙≤ C ⟶ A ❙≤ C)" by (metis subset_def)
lemma subset_char2: "(A ❙≤ B) = (∀C. C ❙≤ A ⟶ C ❙≤ B)" by (metis subset_def)

text‹These (trivial) lemmas are intended to help automated tools.›
lemma setequ_char: "(A ❙= B) = (A ❙≤ B ∧ B ❙≤ A)" unfolding order by blast
lemma setequ_ext: "(A ❙= B) = (A = B)" unfolding order by blast

text‹We now encode connectives for (distributive and complemented) bounded lattices, mostly 
by reusing their counterpart meta-logical HOL connectives.›
definition meet::"'w σ ⇒ 'w σ ⇒ 'w σ" (infixr "❙∧" 54) 
  where "A ❙∧ B ≡ λp. (A p) ∧ (B p)" ―‹ intersection ›
definition join::"'w σ ⇒ 'w σ ⇒ 'w σ" (infixr "❙∨" 53) 
  where "A ❙∨ B ≡ λp. (A p) ∨ (B p)" ―‹ union ›
definition top::"'w σ" ("❙⊤")    
  where "❙⊤ ≡ λw. True"   ―‹ universe ›
definition bottom::"'w σ" ("❙⊥") 
  where "❙⊥ ≡ λw. False"  ―‹ empty-set ›

text‹And introduce further operations to obtain a Boolean algebra (of sets).›
definition compl::"'w σ ⇒ 'w σ" ("❙─_" [57]58)
  where "❙─A  ≡ λp. ¬(A p)" ―‹  (set-)complement ›
definition impl::"'w σ ⇒ 'w σ ⇒ 'w σ" (infixr "❙→" 51)
  where "A ❙→ B ≡ λp. (A p) ⟶ (B p)" ―‹  (set-)implication ›
definition diff::"'w σ ⇒ 'w σ ⇒ 'w σ" (infixr "❙↼" 51) 
  where "A ❙↼ B ≡ λp. (A p) ∧ ¬(B p)" ―‹  (set-)difference ›
definition dimpl::"'w σ ⇒ 'w σ ⇒ 'w σ" (infixr "❙↔" 51)
  where "A ❙↔ B ≡ λp. (A p) = (B p)" ―‹  double implication ›
definition sdiff::"'w σ ⇒ 'w σ ⇒ 'w σ" (infixr "❙△" 51)
  where "A ❙△ B ≡ λp. (A p) ≠ (B p)" ―‹  symmetric difference (aka. xor)  ›

named_theorems conn (*to group together definitions for algebraic connectives*)
declare meet_def[conn] join_def[conn] top_def[conn] bottom_def[conn]
        impl_def[conn] dimpl_def[conn] diff_def[conn] sdiff_def[conn] compl_def[conn]

text‹Verify characterization for some connectives.›
lemma compl_char: "❙─A = A ❙→ ❙⊥" unfolding conn by simp
lemma impl_char: "A ❙→ B = ❙─A ❙∨ B" unfolding conn by simp
lemma dimpl_char: "A ❙↔ B = (A ❙→ B) ❙∧ (B ❙→ A)" unfolding conn by blast
lemma diff_char1: "A ❙↼ B = A ❙∧ ❙─B" unfolding conn by simp
lemma diff_char2: "A ❙↼ B = ❙─(A ❙→ B)" unfolding conn by simp
lemma sdiff_char1: "A ❙△ B = (A ❙↼ B) ❙∨ (B ❙↼ A)" unfolding conn by blast
lemma sdiff_char2: "A ❙△ B = ❙─(A ❙↔ B)" unfolding conn by simp

text‹We can verify that (quite trivially) this algebra satisfies some properties of lattices.›
lemma L1: "A ❙= A ❙∨ A" unfolding conn order by simp
lemma L2: "A ❙= A ❙∧ A" unfolding conn order by simp
lemma L3: "A ❙≤ A ❙∨ B" unfolding conn order by simp
lemma L4: "A ❙∧ B ❙≤ A" unfolding conn order by simp
lemma L5: "(A ❙∧ B) ❙∨ B ❙= B" unfolding setequ_char conn order by simp 
lemma L6: "A ❙∧ (A ❙∨ B) ❙= A" unfolding setequ_char conn order by simp
lemma L7: "A ❙≤ C ∧ B ❙≤ C ⟶ A ❙∨ B ❙≤ C" unfolding conn order by simp 
lemma L8: "C ❙≤ A ∧ C ❙≤ B ⟶ C ❙≤ A ❙∧ B" unfolding conn order by simp
lemma L9:  "A ❙≤ B ⟷ (A ❙∨ B) ❙= B" unfolding setequ_char conn order by simp
lemma L10: "B ❙≤ A ⟷ (A ❙∧ B) ❙= B" unfolding setequ_char conn order by simp
lemma L11: "A ❙≤ B ∧ C ❙≤ D ⟶ A ❙∨ C ❙≤ B ❙∨ D" unfolding conn order by simp
lemma L12: "A ❙≤ B ∧ C ❙≤ D ⟶ A ❙∧ C ❙≤ B ❙∧ D" unfolding conn order by simp
lemma L13: "A ❙∧ ❙⊤ ❙= A" unfolding conn order by simp
lemma L14: "A ❙∨ ❙⊥ ❙= A" unfolding conn order by simp
lemma L15: "A ❙≤ B ⟷ (∀C. C ❙∧ A ❙≤ C ❙∧ B)" by (metis L3 L4 L5 L8 setequ_char subset_char1)
lemma L16: "A ❙≤ B ⟷ (∀C. C ❙∨ A ❙≤ C ❙∨ B)" by (metis L11 L4 L5 setequ_char setequ_ext)

text‹These properties below hold in particular also for Boolean algebras.›
lemma BA_impl: "A ❙≤ B ⟷ A ❙→ B ❙= ❙⊤" unfolding conn order by simp
lemma BA_distr1: "(A ❙∧ (B ❙∨ C)) ❙= ((A ❙∧ B) ❙∨ (A ❙∧ C))" unfolding setequ_char conn order by simp
lemma BA_distr2: "(A ❙∨ (B ❙∧ C)) ❙= ((A ❙∨ B) ❙∧ (A ❙∨ C))" unfolding conn order by blast
lemma BA_cp: "A ❙≤ B ⟷ ❙─B ❙≤ ❙─A" unfolding conn order by blast 
lemma BA_deMorgan1: "❙─(A ❙∨ B) ❙= (❙─A ❙∧ ❙─B)" unfolding conn order by simp
lemma BA_deMorgan2: "❙─(A ❙∧ B) ❙= (❙─A ❙∨ ❙─B)" unfolding conn order by simp
lemma BA_dn: "❙─❙─A ❙= A" unfolding conn order by simp
lemma BA_cmpl_equ: "(❙─A ❙= B) = (A ❙= ❙─B)" unfolding conn order by blast


text‹We conveniently introduce these properties of sets of sets (of points).›
definition meet_closed::"('w σ)σ ⇒ bool"
  where "meet_closed S ≡  ∀X Y. (S X ∧ S Y) ⟶ S(X ❙∧ Y)"
definition join_closed::"('w σ)σ ⇒ bool"
  where "join_closed S ≡  ∀X Y. (S X ∧ S Y) ⟶ S(X ❙∨ Y)"

definition upwards_closed::"('w σ)σ ⇒ bool"
  where "upwards_closed S ≡ ∀X Y. S X ∧ X ❙≤ Y ⟶ S Y"
definition downwards_closed::"('w σ)σ ⇒ bool" 
  where "downwards_closed S ≡ ∀X Y. S X ∧ Y ❙≤ X ⟶ S Y"


subsection ‹Atomicity and primitive equality›

text‹We can verify indeed that the algebra is atomic (in three different ways) by relying on the
presence of primitive equality in HOL.›

lemma atomic1: "∀w. ∃Q. Q w ∧ (∀P. P w ⟶ Q ❙≤ P)" unfolding order using the_sym_eq_trivial by metis

definition "atom A ≡ ¬(A ❙= ❙⊥) ∧ (∀P. A ❙≤ P ∨ A ❙≤ ❙─P)"

lemma atomic2: "∀w. ∃Q. Q w ∧ atom Q" unfolding atom_def order conn using the_sym_eq_trivial by metis
lemma atomic3: "∀P. ¬(P ❙= ❙⊥) ⟶ (∃Q. atom Q ∧ Q ❙≤ P)" unfolding atom_def order conn by fastforce

text‹Now with interactive proof:›
lemma "∀P. ¬(P ❙= ❙⊥) ⟶ (∃Q. atom Q ∧ Q ❙≤ P)"
proof -
  { fix P::"'w σ"
    { assume "¬(P ❙= ❙⊥)"
      hence "∃v. P v" unfolding conn order by simp
      then obtain w where 1:"P w" by (rule exE)
      let ?Q="λv. v = w" ―‹ using HOL primitive equality ›
      have 2: "atom ?Q" unfolding atom_def unfolding conn order by simp
      have "∀v. ?Q v ⟶ P v" using 1 by simp
      hence 3: "?Q ❙≤ P" unfolding order by simp
      from 2 3 have "∃Q. atom Q ∧ Q ❙≤ P" by blast
    } hence "¬(P ❙= ❙⊥) ⟶ (∃Q. atom Q ∧ Q ❙≤ P)" by (rule impI)
  } thus ?thesis by (rule allI)
qed

subsection ‹Miscellaneous notions›

text‹We add some miscellaneous notions that will be useful later.›

abbreviation "isEmpty S ≡ ∀x. ¬S x"
abbreviation "nonEmpty S ≡ ∃x. S x"

text‹Function composition.›
definition fun_comp :: "('b ⇒ 'c) ⇒ ( 'a ⇒ 'b) ⇒ 'a ⇒ 'c" (infixl "∘" 75) 
  where "φ ∘ ψ ≡ λx. φ (ψ x)"

text‹Inverse projection maps a unary function to a 'projected' binary function wrt. its 1st argument.›
abbreviation inv_proj::‹('a ⇒ 'c) ⇒ ('a ⇒ 'b ⇒ 'c)› ("(_)↿")
  where "D↿ ≡ λA B. D A"

text‹Image of a mapping @{text "φ"}, with range as an special case.›
definition image::"('a ⇒ 'b) ⇒ ('a ⇒ bool) ⇒ ('b ⇒ bool)" ("⟦_ _⟧") 
  where "⟦φ S⟧ ≡ λy. ∃x. (S x) ∧ (φ x) = y"
definition range::"('a ⇒ 'b) ⇒ ('b ⇒ bool)" ("⟦_'_⟧") 
  where "⟦φ _⟧ ≡ λY. ∃x. (φ x) = Y"
lemma range_char1: "⟦φ _⟧ = ⟦φ (λx. True)⟧" by (simp add: image_def range_def)
lemma range_char2: "⟦φ _⟧ = (λX. ∃S. ⟦φ S⟧ X)" unfolding range_def image_def by blast

lemma image_comp: "⟦(f ∘ g) S⟧ = ⟦f ⟦g S⟧⟧" unfolding fun_comp_def image_def by metis

end