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