Theory boolean_algebra_operators

theory boolean_algebra_operators
  imports boolean_algebra
begin

subsection ‹Operations on set-valued functions›

text‹Functions with sets in their codomain will be called here 'set-valued functions'.
  We conveniently define some (2nd-order) Boolean operations on them.›

text‹The 'meet' and 'join' of two set-valued functions.›
definition svfun_meet::"('a ⇒ 'w σ) ⇒ ('a ⇒ 'w σ) ⇒ ('a ⇒ 'w σ)" (infixr "❙∧⇧^:" 62) 
  where "φ ❙∧⇧^: ψ ≡ λx. (φ x) ❙∧ (ψ x)"
definition svfun_join::"('a ⇒ 'w σ) ⇒ ('a ⇒ 'w σ) ⇒ ('a ⇒ 'w σ)" (infixr "❙∨⇧^:" 61) 
  where "φ ❙∨⇧^: ψ ≡ λx. (φ x) ❙∨ (ψ x)"
text‹Analogously, we can define an 'implication' and a 'complement'.›
definition svfun_impl::"('a ⇒ 'w σ) ⇒ ('a ⇒ 'w σ) ⇒ ('a ⇒ 'w σ)" (infixr "❙→⇧^:" 61) 
  where "ψ ❙→⇧^: φ ≡ λx. (ψ x) ❙→ (φ x)"
definition svfun_compl::"('a ⇒ 'w σ) ⇒ ('a ⇒ 'w σ)" ("(_⇧^-)") 
  where "φ⇧^- ≡ λx. ❙─(φ x)"
text‹There are two natural 0-ary connectives (aka. constants). ›
definition svfun_top::"'a ⇒ 'w σ" ("❙⊤⇧^:") 
  where "❙⊤⇧^: ≡ λx. ❙⊤"
definition svfun_bot::"'a ⇒ 'w σ" ("❙⊥⇧^:") 
  where "❙⊥⇧^: ≡ λx. ❙⊥"

named_theorems conn2 (*to group together definitions for 2nd-order algebraic connectives*)
declare svfun_meet_def[conn2] svfun_join_def[conn2] svfun_impl_def[conn2]
        svfun_compl_def[conn2] svfun_top_def[conn2] svfun_bot_def[conn2]

text‹And, of course, set-valued functions are naturally ordered in the expected way:›
definition svfun_sub::"('a ⇒ 'w σ) ⇒ ('a ⇒ 'w σ) ⇒ bool" (infixr "❙≤⇧^:" 55) 
  where "ψ ❙≤⇧^: φ ≡ ∀x. (ψ x) ❙≤ (φ x)"
definition svfun_equ::"('a ⇒ 'w σ) ⇒ ('a ⇒ 'w σ) ⇒ bool" (infixr "❙=⇧^:" 55) 
  where "ψ ❙=⇧^: φ ≡ ∀x. (ψ x) ❙= (φ x)"

named_theorems order2 (*to group together definitions for 2nd-order algebraic connectives*)
declare svfun_sub_def[order2] svfun_equ_def[order2]

text‹These (trivial) lemmas are intended to help automated tools.›
lemma svfun_sub_char: "(ψ ❙≤⇧^: φ) = (ψ ❙→⇧^: φ ❙=⇧^: ❙⊤⇧^:)" by (simp add: BA_impl svfun_equ_def svfun_impl_def svfun_sub_def svfun_top_def)
lemma svfun_equ_char: "(ψ ❙=⇧^: φ) = (ψ ❙≤⇧^: φ ∧ φ ❙≤⇧^: ψ)" unfolding order2 setequ_char by blast
lemma svfun_equ_ext: "(ψ ❙=⇧^: φ) = (ψ = φ)" by (meson ext setequ_ext svfun_equ_def)

text‹Clearly, set-valued functions form a Boolean algebra. We can prove some interesting relationships:›
lemma svfun_compl_char: "φ⇧^- = (φ ❙→⇧^: ❙⊥⇧^:)" unfolding conn conn2 by simp
lemma svfun_impl_char1: "(ψ ❙→⇧^: φ) = (ψ⇧^- ❙∨⇧^: φ)" unfolding conn conn2 by simp
lemma svfun_impl_char2: "(ψ ❙→⇧^: φ) = (ψ ❙∧⇧^: (φ⇧^-))⇧^-" unfolding conn conn2 by simp
lemma svfun_deMorgan1: "(ψ ❙∧⇧^: φ)⇧^- = (ψ⇧^-) ❙∨⇧^: (φ⇧^-)" unfolding conn conn2 by simp
lemma svfun_deMorgan2: "(ψ ❙∨⇧^: φ)⇧^- = (ψ⇧^-) ❙∧⇧^: (φ⇧^-)" unfolding conn conn2 by simp


subsection ‹Operators and their transformations›

text‹Dual to set-valued functions we can have set-domain functions. For them we can define the 'dual-complement'.›
definition sdfun_dcompl::"('w σ ⇒ 'a) ⇒ ('w σ ⇒ 'a)" ("(_⇧^d⇧^-)") 
  where "φ⇧^d⇧^- ≡ λX. φ(❙─X)"
lemma sdfun_dcompl_char: "φ⇧^d⇧^- = (λX. ∃Y. (φ Y) ∧ (X = ❙─Y))" by (metis BA_dn setequ_ext sdfun_dcompl_def)

text‹Operators are a particularly important kind of functions. They are both set-valued and set-domain.
Thus our algebra of operators inherits the connectives defined above plus the ones below. ›

text‹We conveniently define the 'dual' of an operator.›
definition op_dual::"('w σ ⇒ 'w σ) ⇒ ('w σ ⇒ 'w σ)" ("(_⇧^d)") 
  where "φ⇧^d ≡ λX. ❙─(φ(❙─X))"

text‹The following two 0-ary connectives (i.e. operator 'constants') exist already (but somehow implicitly).
  We just make them explicit by introducing some convenient notation.›
definition id_op::"'w σ ⇒ 'w σ" ("❙e") 
  where "❙e ≡ λX. X" (*introduces notation to refer to 'identity' operator*)
definition compl_op::"'w σ ⇒ 'w σ" ("❙n") 
  where "❙n ≡ λX. ❙─X" (*to refer to 'complement' operator*)

declare sdfun_dcompl_def[conn2] op_dual_def[conn2] id_op_def[conn2] compl_op_def[conn2]

text‹We now prove some lemmas (some of them might help provers in their hard work).›
lemma dual_compl_char1: "φ⇧^d⇧^- = (φ⇧^d)⇧^-" unfolding conn2 conn order by simp
lemma dual_compl_char2: "φ⇧^d⇧^- = (φ⇧^-)⇧^d" unfolding conn2 conn order by simp
lemma sfun_compl_invol: "φ⇧^-⇧^- = φ" unfolding conn2 conn order by simp
lemma dual_invol: "φ⇧^d⇧^d = φ" unfolding conn2 conn order by simp
lemma dualcompl_invol: "(φ⇧^d⇧^-)⇧^d⇧^- = φ" unfolding conn2 conn order by simp

lemma op_prop1: "❙e⇧^d = ❙e" unfolding conn2 conn by simp
lemma op_prop2: "❙n⇧^d = ❙n" unfolding conn2 conn by simp
lemma op_prop3: "❙e⇧^- = ❙n" unfolding conn2 conn by simp
lemma op_prop4: "(φ ❙∨⇧^: ψ)⇧^d = (φ⇧^d) ❙∧⇧^: (ψ⇧^d)" unfolding conn2 conn by simp
lemma op_prop5: "(φ ❙∨⇧^: ψ)⇧^- = (φ⇧^-) ❙∧⇧^: (ψ⇧^-)" unfolding conn2 conn by simp
lemma op_prop6: "(φ ❙∧⇧^: ψ)⇧^d = (φ⇧^d) ❙∨⇧^: (ψ⇧^d)" unfolding conn2 conn by simp
lemma op_prop7: "(φ ❙∧⇧^: ψ)⇧^- = (φ⇧^-) ❙∨⇧^: (ψ⇧^-)" unfolding conn2 conn by simp
lemma op_prop8: "❙⊤⇧^: = ❙n ❙∨⇧^: ❙e" unfolding conn2 conn by simp
lemma op_prop9: "❙⊥⇧^: = ❙n ❙∧⇧^: ❙e" unfolding conn2 conn by simp

text‹The notion of a fixed-point is fundamental. We speak of sets being fixed-points of operators.
We define a function that given an operator returns the set of all its fixed-points.›
definition fixpoints::"('w σ ⇒ 'w σ) ⇒ ('w σ)σ" ("fp") 
  where "fp φ ≡ λX. (φ X) ❙= X"
text‹We can in fact 'operationalize' the function above, thus obtaining a 'fixed-point operation'.›
definition op_fixpoint::"('w σ ⇒ 'w σ) ⇒ ('w σ ⇒ 'w σ)" ("(_⇧^f⇧^p)")
  where "φ⇧^f⇧^p ≡ λX. (φ X) ❙↔ X"

declare fixpoints_def[conn2] op_fixpoint_def[conn2]

text‹Interestingly, the fixed-point operation (or transformation) is definable in terms of the others.›
lemma op_fixpoint_char: "φ⇧^f⇧^p = (φ ❙∧⇧^: ❙e) ❙∨⇧^: (φ⇧^- ❙∧⇧^: ❙n)" unfolding conn2 order conn by blast

text‹Given an operator @{text "φ"} the fixed-points of it's dual is the set of complements of @{text "φ's"} fixed-points.›
lemma fp_dual: "fp φ⇧^d = (fp φ)⇧^d⇧^-" unfolding order conn conn2 by blast
text‹The fixed-points of @{text "φ's"} complement is the set of complements of the fixed-points of @{text "φ's"} dual-complement.›
lemma fp_compl: "fp φ⇧^- = (fp (φ⇧^d⇧^-))⇧^d⇧^-" by (simp add: dual_compl_char2 dualcompl_invol fp_dual)
text‹The fixed-points of @{text "φ's"} dual-complement is the set of complements of the fixed-points of @{text "φ's"} complement.›
lemma fp_dcompl: "fp (φ⇧^d⇧^-) = (fp φ⇧^-)⇧^d⇧^-" by (simp add: dualcompl_invol fp_compl)

text‹The fixed-points function and the fixed-point operation are essentially related.›
lemma fp_rel: "fp φ A ⟷ (φ⇧^f⇧^p A) ❙= ❙⊤" unfolding conn2 order conn by simp
lemma fp_d_rel:  "fp φ⇧^d A ⟷ φ⇧^f⇧^p(❙─A) ❙= ❙⊤" unfolding conn2 order conn by blast
lemma fp_c_rel: "fp φ⇧^- A ⟷ φ⇧^f⇧^p A ❙= ❙⊥" unfolding conn2 order conn by blast
lemma fp_dc_rel: "fp (φ⇧^d⇧^-) A ⟷ φ⇧^f⇧^p(❙─A) ❙= ❙⊥" unfolding conn2 order conn by simp

text‹The fixed-point operation is involutive.›
lemma ofp_invol: "(φ⇧^f⇧^p)⇧^f⇧^p = φ" unfolding conn2 order conn by blast
text‹And commutes the dual with the dual-complement operations.›
lemma ofp_comm_dc1: "(φ⇧^d)⇧^f⇧^p = (φ⇧^f⇧^p)⇧^d⇧^-" unfolding conn2 order conn by blast
lemma ofp_comm_dc2:"(φ⇧^d⇧^-)⇧^f⇧^p = (φ⇧^f⇧^p)⇧^d" unfolding conn2 order conn by simp

text‹The fixed-point operation commutes with the complement.›
lemma ofp_comm_compl: "(φ⇧^-)⇧^f⇧^p = (φ⇧^f⇧^p)⇧^-" unfolding conn2 order conn by blast
text‹The above motivates the following alternative definition for a 'complemented-fixed-point' operation.›
lemma ofp_fixpoint_compl_def: "φ⇧^f⇧^p⇧^- = (λX. (φ X) ❙△ X)" unfolding conn2 conn by simp
text‹Analogously, the 'complemented fixed-point' operation is also definable in terms of the others.›
lemma op_fixpoint_compl_char: "φ⇧^f⇧^p⇧^- = (φ ❙∨⇧^: ❙e) ❙∧⇧^: (φ⇧^- ❙∨⇧^: ❙n)" unfolding conn2 conn by blast

text‹In fact, function composition can be seen as an additional binary connective for operators.
  We show below some interesting relationships that hold. ›
lemma op_prop10: "φ = (❙e ∘ φ)" unfolding conn2 fun_comp_def by simp
lemma op_prop11: "φ = (φ ∘ ❙e)" unfolding conn2 fun_comp_def by simp
lemma op_prop12: "❙e = (❙n ∘ ❙n)" unfolding conn2 conn fun_comp_def by simp
lemma op_prop13: "φ⇧^- = (❙n ∘ φ)" unfolding conn2 fun_comp_def by simp
lemma op_prop14: "φ⇧^d⇧^- = (φ ∘ ❙n)" unfolding conn2 fun_comp_def by simp
lemma op_prop15: "φ⇧^d = (❙n ∘ φ ∘ ❙n)" unfolding conn2 fun_comp_def by simp

text‹There are also some useful properties regarding the images of operators.›
lemma im_prop1: "⟦φ D⟧⇧^d⇧^-  = ⟦φ⇧^d D⇧^d⇧^-⟧" unfolding image_def op_dual_def sdfun_dcompl_def by (metis BA_dn setequ_ext)
lemma im_prop2: "⟦φ⇧^- D⟧⇧^d⇧^- = ⟦φ D⟧" unfolding image_def svfun_compl_def sdfun_dcompl_def by (metis BA_dn setequ_ext)
lemma im_prop3: "⟦φ⇧^d D⟧⇧^d⇧^- = ⟦φ D⇧^d⇧^-⟧" unfolding image_def op_dual_def sdfun_dcompl_def by (metis BA_dn setequ_ext)
lemma im_prop4: "⟦φ⇧^d⇧^- D⟧⇧^d⇧^- = ⟦φ⇧^d D⟧" unfolding image_def op_dual_def sdfun_dcompl_def by (metis BA_dn setequ_ext)
lemma im_prop5: "⟦φ⇧^- D⇧^d⇧^-⟧  = ⟦φ⇧^d⇧^- D⟧⇧^d⇧^-" unfolding image_def svfun_compl_def sdfun_dcompl_def by (metis (no_types, opaque_lifting) BA_dn setequ_ext)
lemma im_prop6: "⟦φ⇧^d⇧^- D⇧^d⇧^-⟧  = ⟦φ D⟧" unfolding image_def sdfun_dcompl_def by (metis BA_dn setequ_ext)


text‹Observe that all results obtained by assuming fixed-point predicates extend to their associated operators.›
lemma "φ⇧^f⇧^p(A) ❙∧ Γ(A) ❙≤ Δ(A) ⟶ (fp φ)(A) ⟶ Γ(A) ❙≤ Δ(A)"
  by (simp add: fp_rel meet_def setequ_ext subset_def top_def)
lemma "φ⇧^f⇧^p(A) ❙∧ φ⇧^f⇧^p(B) ❙∧ (Γ A B) ❙≤ (Δ A B) ⟶ (fp φ)(A) ∧ (fp φ)(B) ⟶ (Γ A B) ❙≤ (Δ A B)"
  by (simp add: fp_rel meet_def setequ_ext subset_def top_def)

end