Theory Clauses

theory Clauses imports
  Main
  Containers.Containers
begin

type_synonym literal = "nat × bool"
type_synonym clause = "literal set"
type_synonym cnf = "clause set"

datatype bexp
  = Var nat
  | not bexp
  | Or bexp bexp (infixl ‹or› 110)
  | And bexp bexp (infixl ‹and› 120)

declare [[coercion Var]] [[coercion_enabled]]

declare SUP_cong_simp[fundef_cong del]
function cnf :: "bexp ⇒ cnf"
where
  "cnf v = {{(v, True)}}"
| "cnf (b and b') = cnf b ∪ cnf b'"
| "cnf (b or b') = (⋃c ∈ cnf b. (λc'. c ∪ c') ` cnf b')"
| "cnf (not v) = {{(v, False)}}"
| "cnf (not (not b)) = cnf b"
| "cnf (not (b and b')) = cnf (not b or not b')"
| "cnf (not (b or b')) = cnf (not b and not b')"
by pat_completeness simp_all
termination by(relation "measure (rec_bexp (λ_. 1) (λ_ n. 3 * n + 1) (λ_ _ n m. n + m + 1) (λ_ _ n m. n + m + 1))") simp_all
declare SUP_cong_simp[fundef_cong]

definition test 
where 
  "test = 
  (1 and 2) or (not 1 and not 2) or
  (3 and 4) or (not 3 and not 4) or
  (5 and 6) or (not 5 and not 6) or
  (7 and 8) or (not 7 and not 8) or
  (9 and 10) or (not 9 and not 10) or
  (11 and 12) or (not 11 and not 12) or
  (1 and 2) or (3 and 4) or
  (1 and 3) or (2 and 4)"

value "cnf test = {}"

text ‹Sanity check for correctness›

type_synonym env = "nat ⇒ bool"

primrec eval_bexp :: "env ⇒ bexp ⇒ bool" (‹_ ⊨ _› [100, 100] 70)
where
  "Φ ⊨ v ⟷ Φ v"
| "Φ ⊨ not b ⟷ ¬ Φ ⊨ b"
| "Φ ⊨ b and b' ⟷ Φ ⊨ b ∧ Φ ⊨ b'"
| "Φ ⊨ b or b' ⟷ Φ ⊨ b ∨ Φ ⊨ b'"

definition eval_cnf :: "env ⇒ cnf ⇒ bool" (‹_ ⊢ _› [100, 100] 70)
where "Φ ⊢ F ⟷ (∀C ∈ F. ∃(n, b) ∈ C. Φ n = b)"

lemma cnf_correct: "Φ ⊢ cnf b ⟷ Φ ⊨ b"
proof(rule sym, induction b rule: cnf.induct)
  case 2 show ?case by(simp add: "2.IH")(auto simp add: eval_cnf_def)
next
  case 3 then show ?case
    by (auto simp add: "3.IH" eval_cnf_def split_beta) blast+
qed(auto simp add: eval_cnf_def)

end