Theory SAT_Basic

(* Taken from Lammich's GRAT tool, and slightly adapted to use positive nats as variables *)
section ‹Basics of Boolean Formulas in CNF›
theory SAT_Basic
imports Main
begin
  datatype 'a literal = is_pos: Pos 'a | Neg 'a

  type_synonym 'a clause = "'a literal set"

  type_synonym 'a cnf = "'a clause set"

  type_synonym 'a valuation = "'a ⇒ bool"

  fun sem_lit :: "'a literal ⇒ 'a valuation ⇒ bool" where
    "sem_lit (Pos x) σ = σ x"
  | "sem_lit (Neg x) σ = (¬ σ x)"

  lemma sem_lit_alt: "sem_lit l σ = (case l of Pos x ⇒ σ x | Neg x ⇒ ¬σ x)"
    by (auto split: literal.split)

  definition sem_clause :: "'a clause ⇒ 'a valuation ⇒ bool" where
    "sem_clause C σ ≡ ∃l∈C. sem_lit l σ"

  definition sem_cnf :: "'a cnf ⇒ 'a valuation ⇒ bool" where
    "sem_cnf F σ ≡ ∀C∈F. sem_clause C σ"

  definition sat :: "'a cnf ⇒ bool" where
    "sat F ≡ ∃σ. sem_cnf F σ"

  definition models :: "'a cnf ⇒ 'a valuation set" where
    "models F ≡ {σ. sem_cnf F σ}"
    
  lemma sat_iff_has_models: 
    "sat F ⟷ models F ≠ {}" 
    unfolding sat_def models_def by auto
    
  fun neg_lit where
    "neg_lit (Pos x) = Neg x" | "neg_lit (Neg x) = Pos x"

  lemma neg_neg_lit[simp]: "neg_lit (neg_lit l) = l" by (cases l) auto  
  lemma neg_lit_neq[simp]: 
    "neg_lit l ≠ l" 
    "l ≠ neg_lit l" 
    by (cases l; auto)+

  lemma neg_lit_inj_simp[simp]: "neg_lit l = neg_lit l' ⟷ l=l'" by (cases l; cases l') auto

  lemma neg_lit_eq_inv[simp]:
    "neg_lit l = Neg v ⟷ l = Pos v"  
    "Neg v = neg_lit l ⟷ l = Pos v"  
    "neg_lit l = Pos v ⟷ l = Neg v"  
    "Pos v = neg_lit l ⟷ l = Neg v"  
    by (cases l; auto; fail)+
  
  
  definition mk_lit where "mk_lit p x ≡ if p then Pos x else Neg x"  

  lemma is_pos_mk_lit[simp]: "is_pos (mk_lit p x) ⟷ p"
    unfolding mk_lit_def by auto

  lemma sem_clause_empty[simp]: "sem_clause {} σ = False"  
    unfolding sem_clause_def by auto

  lemma sem_clause_insert[simp]: "sem_clause (insert l C) σ ⟷ sem_lit l σ ∨ sem_clause C σ"  
    by (auto simp: sem_clause_def)

  lemma sem_clause_union[simp]: "sem_clause (C⇩1∪C⇩2) σ ⟷ sem_clause C⇩1 σ ∨ sem_clause C⇩2 σ"  
    by (auto simp: sem_clause_def)

  lemma sem_cnf_empty[simp]: "sem_cnf {} σ" by (auto simp: sem_cnf_def)
  lemma sem_cnf_insert[simp]: "sem_cnf (insert C F) σ ⟷ sem_clause C σ ∧ sem_cnf F σ"
    by (auto simp: sem_cnf_def)
  lemma sem_cnf_union[simp]: "sem_cnf (F⇩1 ∪ F⇩2) σ ⟷ sem_cnf F⇩1 σ ∧ sem_cnf F⇩2 σ"
    by (auto simp: sem_cnf_def)

  lemma sem_clauseI: "⟦l∈C; sem_lit l σ⟧ ⟹ sem_clause C σ"
    by (auto simp: sem_clause_def)

  lemma sem_cnfI: "⟦⋀C. C∈F ⟹ sem_clause C σ⟧ ⟹ sem_cnf F σ"    
    by (auto simp: sem_cnf_def)

  lemma sem_neg_lit[simp]: "sem_lit (neg_lit l) σ ⟷ ¬sem_lit l σ"  
    by (cases l) auto

  lemma unsat_empty_clause: "{}∈F ⟹ ¬sat F"  
    unfolding sat_def sem_cnf_def
    by fastforce

  lemma sat_empty[simp, intro!]: "sat {}"  
    unfolding sat_def sem_cnf_def by auto

  lemma unsat_emptyc[simp, intro!]: "¬sat {{}}"
    by (simp add: unsat_empty_clause)


  subsection ‹Used Variables›
  fun var_of_lit :: "'a literal ⇒ 'a" where
    "var_of_lit (Pos x) = x" | "var_of_lit (Neg x) = x"
  lemma var_of_lit_alt: "var_of_lit l = (case l of Pos x ⇒ x | Neg x ⇒ x)"
    by (cases l) auto
  definition vars_of_clause :: "'a clause ⇒ 'a set" 
    where "vars_of_clause C = var_of_lit ` C"
  definition vars_of_cnf :: "'a cnf ⇒ 'a set" where "vars_of_cnf F ≡ ⋃(vars_of_clause`F)"

  lemma vars_of_clause_simps[simp]:
    "vars_of_clause {} = {}"
    "vars_of_clause (insert l C) = insert (var_of_lit l) (vars_of_clause C)"
    "vars_of_clause (C⇩1 ∪ C⇩2) = vars_of_clause C⇩1 ∪ vars_of_clause C⇩2"
    by (auto simp: vars_of_clause_def)

  lemma vars_of_cnf_simps[simp]: 
    "vars_of_cnf {} = {}"
    "vars_of_cnf (insert C F) = vars_of_clause C ∪ vars_of_cnf F"
    "vars_of_cnf (F⇩1∪F⇩2) = vars_of_cnf F⇩1 ∪ vars_of_cnf F⇩2"
    by (auto simp: vars_of_cnf_def)

  lemma vars_of_clause_empty_iff[simp]: "vars_of_clause C = {} ⟷ C={}"  
    by (auto simp: vars_of_clause_def)

  lemma vars_of_cnf_empty_iff[simp]: "vars_of_cnf F = {} ⟷ (F={} ∨ F={{}})"
    by (auto simp: vars_of_cnf_def)
    
  lemma var_of_lit_neg_eq[simp]: "var_of_lit (neg_lit l) = var_of_lit l" by (cases l) auto
  

  lemma syn_indep_lit: "x≠var_of_lit l ⟹ sem_lit l (σ(x:=v)) = sem_lit l σ"
    by (cases l) auto

  lemma syn_indep_clause: "x∉vars_of_clause C ⟹ sem_clause C (σ(x:=v)) = sem_clause C σ"
    unfolding sem_clause_def vars_of_clause_def 
    by (force simp: syn_indep_lit)

  lemma syn_indep_cnf: "x∉vars_of_cnf F ⟹ sem_cnf F (σ(x:=v)) = sem_cnf F σ"
    unfolding sem_cnf_def vars_of_cnf_def
    by (auto simp: syn_indep_clause)


  subsection ‹Assigning Valuations›  
  definition "set_lit F l ≡ { C - {neg_lit l} | C. C∈F ∧ l ∉ C }"

  lemma sem_clause_set: "sem_clause C (σ(var_of_lit l := is_pos l)) 
    ⟷ l∈C ∨ sem_clause (C - {neg_lit l}) σ"
    unfolding sem_clause_def 
    apply (cases l)
    apply safe
    apply (auto simp: sem_lit_alt split: literal.splits if_split_asm)
    done

  lemma sem_cnf_set: "sem_cnf F (σ(var_of_lit l := is_pos l)) ⟷ sem_cnf (set_lit F l) σ"
    unfolding sem_cnf_def set_lit_def mk_lit_def
    by (auto simp: sem_clause_set)

  lemma upd_sigma_true[simp]: "σ x ⟹ σ(x:=True) = σ" by (auto simp: fun_upd_def)
  lemma upd_sigma_false[simp]: "¬σ x ⟹ σ(x:=False) = σ" by (auto simp: fun_upd_def)
    
  lemma set_lit_no_var: "var_of_lit l ∉ vars_of_cnf (set_lit F l)"  
    unfolding set_lit_def vars_of_cnf_def
    by (auto simp: vars_of_clause_def var_of_lit_alt split: literal.splits)

  lemmas indep_set_lit = syn_indep_cnf[OF set_lit_no_var]

end