Theory Propositional_Proof_Systems.CNF_Sema

theory CNF_Sema
imports CNF
begin

(* 'a ⇒ bool is a valuation, but I do not want to include Sema just for that… *)
primrec lit_semantics :: "('a ⇒ bool) ⇒ 'a literal ⇒ bool" where
"lit_semantics 𝒜 (k⇧+) = 𝒜 k" |
"lit_semantics 𝒜 (k¯) = (¬𝒜 k)"
case_of_simps lit_semantics_cases: lit_semantics.simps
definition clause_semantics where
  "clause_semantics 𝒜 C ≡ ∃L ∈ C. lit_semantics 𝒜 L"
definition cnf_semantics where
  "cnf_semantics 𝒜 S ≡ ∀C ∈ S. clause_semantics 𝒜 C"


end