Theory Boolean_Algebra

section ‹Boolean Algebra›

theory Boolean_Algebra
  imports
    "ZFC_in_HOL.ZFC_Typeclasses"
begin

text ‹This theory contains an embedding of two-valued boolean algebra into \<^term>‹V›.›

hide_const (open) List.set

definition bool_to_V :: "bool ⇒ V" where
  "bool_to_V = (SOME f. inj f)"

lemma bool_to_V_injectivity [simp]:
  shows "inj bool_to_V"
  unfolding bool_to_V_def by (fact someI_ex[OF embeddable_class.ex_inj])

definition bool_from_V :: "V ⇒ bool" where
  [simp]: "bool_from_V = inv bool_to_V"

definition top :: V (‹❙T›) where
  [simp]: "❙T = bool_to_V True"

definition bottom :: V (‹❙F›) where
  [simp]: "❙F = bool_to_V False"

definition two_valued_boolean_algebra_universe :: V (‹𝔹›) where
  [simp]: "𝔹 = set {❙T, ❙F}"

definition negation :: "V ⇒ V" (‹∼ _› [141] 141) where
  [simp]: "∼ p = bool_to_V (¬ bool_from_V p)"

definition conjunction :: "V ⇒ V ⇒ V" (infixr ‹❙∧› 136) where
  [simp]: "p ❙∧ q = bool_to_V (bool_from_V p ∧ bool_from_V q)"

definition disjunction :: "V ⇒ V ⇒ V" (infixr ‹❙∨› 131) where
  [simp]: "p ❙∨ q = ∼ (∼ p ❙∧ ∼ q)"

definition implication :: "V ⇒ V ⇒ V" (infixr ‹❙⊃› 121) where
  [simp]: "p ❙⊃ q = ∼ p ❙∨ q"

definition iff :: "V ⇒ V ⇒ V" (infixl ‹❙≡› 150) where
  [simp]: "p ❙≡ q = (p ❙⊃ q) ❙∧ (q ❙⊃ p)"

lemma boolean_algebra_simps [simp]:
  assumes "p ∈ elts 𝔹" and "q ∈ elts 𝔹" and "r ∈ elts 𝔹"
  shows "∼ ∼ p = p"
  and "((∼ p) ❙≡ (∼ q)) = (p ❙≡ q)"
  and "∼ (p ❙≡ q) = (p ❙≡ (∼ q))"
  and "(p ❙∨ ∼ p) = ❙T"
  and "(∼ p ❙∨ p) = ❙T"
  and "(p ❙≡ p) = ❙T"
  and "(∼ p) ≠ p"
  and "p ≠ (∼ p)"
  and "(❙T ❙≡ p) = p"
  and "(p ❙≡ ❙T) = p"
  and "(❙F ❙≡ p) = (∼ p)"
  and "(p ❙≡ ❙F) = (∼ p)"
  and "(❙T ❙⊃ p) = p"
  and "(❙F ❙⊃ p) = ❙T"
  and "(p ❙⊃ ❙T) = ❙T"
  and "(p ❙⊃ p) = ❙T"
  and "(p ❙⊃ ❙F) = (∼ p)"
  and "(p ❙⊃ ∼ p) = (∼ p)"
  and "(p ❙∧ ❙T) = p"
  and "(❙T ❙∧ p) = p"
  and "(p ❙∧ ❙F) = ❙F"
  and "(❙F ❙∧ p) = ❙F"
  and "(p ❙∧ p) = p"
  and "(p ❙∧ (p ❙∧ q)) = (p ❙∧ q)"
  and "(p ❙∧ ∼ p) = ❙F"
  and "(∼ p ❙∧ p) = ❙F"
  and "(p ❙∨ ❙T) = ❙T"
  and "(❙T ❙∨ p) = ❙T"
  and "(p ❙∨ ❙F) = p"
  and "(❙F ❙∨ p) = p"
  and "(p ❙∨ p) = p"
  and "(p ❙∨ (p ❙∨ q)) = (p ❙∨ q)"
  and "p ❙∧ q = q ❙∧ p"
  and "p ❙∧ (q ❙∧ r) = q ❙∧ (p ❙∧ r)"
  and "p ❙∨ q = q ❙∨ p"
  and "p ❙∨ (q ❙∨ r) = q ❙∨ (p ❙∨ r)"
  and "(p ❙∨ q) ❙∨ r = p ❙∨ (q ❙∨ r)"
  and "p ❙∧ (q ❙∨ r) = p ❙∧ q ❙∨ p ❙∧ r"
  and "(p ❙∨ q) ❙∧ r = p ❙∧ r ❙∨ q ❙∧ r"
  and "p ❙∨ (q ❙∧ r) = (p ❙∨ q) ❙∧ (p ❙∨ r)"
  and "(p ❙∧ q) ❙∨ r = (p ❙∨ r) ❙∧ (q ❙∨ r)"
  and "(p ❙⊃ (q ❙∧ r)) = ((p ❙⊃ q) ❙∧ (p ❙⊃ r))"
  and "((p ❙∧ q) ❙⊃ r) = (p ❙⊃ (q ❙⊃ r))"
  and "((p ❙∨ q) ❙⊃ r) = ((p ❙⊃ r) ❙∧ (q ❙⊃ r))"
  and "((p ❙⊃ q) ❙∨ r) = (p ❙⊃ q ❙∨ r)"
  and "(q ❙∨ (p ❙⊃ r)) = (p ❙⊃ q ❙∨ r)"
  and "∼ (p ❙∨ q) = ∼ p ❙∧ ∼ q"
  and "∼ (p ❙∧ q) = ∼ p ❙∨ ∼ q"
  and "∼ (p ❙⊃ q) = p ❙∧ ∼ q"
  and "∼ p ❙∨ q = (p ❙⊃ q)"
  and "p ❙∨ ∼ q = (q ❙⊃ p)"
  and "(p ❙⊃ q) = (∼ p) ❙∨ q"
  and "p ❙∨ q = ∼ p ❙⊃ q"
  and "(p ❙≡ q) = (p ❙⊃ q) ❙∧ (q ❙⊃ p)"
  and "(p ❙⊃ q) ❙∧ (∼ p ❙⊃ q) = q"
  and "p = ❙T ⟹ ¬ (p = ❙F)"
  and "p = ❙F ⟹ ¬ (p = ❙T)"
  and "p = ❙T ∨ p = ❙F"
  using assms by (auto simp add: inj_eq)

lemma tv_cases [consumes 1, case_names top bottom, cases type: V]:
  assumes "p ∈ elts 𝔹"
  and "p = ❙T ⟹ P"
  and "p = ❙F ⟹ P"
  shows P
  using assms by auto

end