Theory DPLL_CDCL_W_Implementation

theory DPLL_CDCL_W_Implementation
imports Partial_Annotated_Clausal_Logic
begin

section ‹Simple Implementation of the DPLL and CDCL›
subsection ‹Common Rules›
subsubsection ‹Propagation›
text ‹The following theorem holds:›
lemma lits_of_unfold[iff]:
  "(∀c ∈ set C. -c ∈ lits_of Ms) ⟷ Ms ⊨as CNot (mset C)"
  unfolding true_annots_def Ball_def true_annot_def CNot_def mem_set_multiset_eq by auto
text ‹The right-hand version is written at a high-level, but only the left-hand side is executable.›

definition is_unit_clause :: "'a literal list ⇒ ('a, 'b, 'c) ann_literal list ⇒ 'a literal option"
 where
 "is_unit_clause l M =
   (case List.filter (λa. atm_of a ∉ atm_of ` lits_of M) l of
     a # [] ⇒ if M ⊨as CNot (mset l - {#a#}) then Some a else None
   | _ ⇒ None)"

definition is_unit_clause_code :: "'a literal list ⇒ ('a, 'b, 'c) ann_literal list
  ⇒ 'a literal option" where
 "is_unit_clause_code l M =
   (case List.filter (λa. atm_of a ∉ atm_of ` lits_of M) l of
     a # [] ⇒ if (∀c ∈set (remove1 a l). -c ∈ lits_of M) then Some a else None
   | _ ⇒ None)"

lemma is_unit_clause_is_unit_clause_code[code]:
  "is_unit_clause l M = is_unit_clause_code l M"
proof -
  have 1: "⋀a. (∀c∈set (remove1 a l). - c ∈ lits_of M) ⟷ M ⊨as CNot (mset l - {#a#})"
    using lits_of_unfold[of "remove1 _ l", of _ M] by simp
  thus ?thesis
    unfolding is_unit_clause_code_def is_unit_clause_def 1 by blast
qed

lemma is_unit_clause_some_undef:
  assumes "is_unit_clause l M = Some a"
  shows "undefined_lit M a"
proof -
  have "(case [a←l . atm_of a ∉ atm_of ` lits_of M] of [] ⇒ None
          | [a] ⇒ if M ⊨as CNot (mset l - {#a#}) then Some a else None
          | a # ab # xa ⇒ Map.empty xa) = Some a"
    using assms unfolding is_unit_clause_def .
  hence "a ∈ set [a←l . atm_of a ∉ atm_of ` lits_of M]"
    apply (cases "[a←l . atm_of a ∉ atm_of ` lits_of M]")
      apply simp
    apply (rename_tac aa list; case_tac list) by (auto split: split_if_asm)
  hence "atm_of a ∉ atm_of ` lits_of M" by auto
  thus ?thesis
    by (simp add: Decided_Propagated_in_iff_in_lits_of
      atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set )
qed

lemma is_unit_clause_some_CNot: "is_unit_clause l M = Some a ⟹ M ⊨as CNot (mset l - {#a#})"
  unfolding is_unit_clause_def
proof -
  assume "(case [a←l . atm_of a ∉ atm_of ` lits_of M] of [] ⇒ None
          | [a] ⇒ if M ⊨as CNot (mset l - {#a#}) then Some a else None
          | a # ab # xa ⇒ Map.empty xa) = Some a"
  thus ?thesis
    apply (cases "[a←l . atm_of a ∉ atm_of ` lits_of M]", simp)
      apply simp
    apply (rename_tac aa list, case_tac list) by (auto split: split_if_asm)
qed

lemma is_unit_clause_some_in: "is_unit_clause l M = Some a ⟹ a ∈ set l"
  unfolding is_unit_clause_def
proof -
  assume "(case [a←l . atm_of a ∉ atm_of ` lits_of M] of [] ⇒ None
         | [a] ⇒ if M ⊨as CNot (mset l - {#a#}) then Some a else None
         | a # ab # xa ⇒ Map.empty xa) = Some a"
  thus "a ∈ set l"
    by (cases "[a←l . atm_of a ∉ atm_of ` lits_of M]")
       (fastforce dest: filter_eq_ConsD split: split_if_asm  split: list.splits)+
qed

lemma is_unit_clause_nil[simp]: "is_unit_clause [] M = None"
  unfolding is_unit_clause_def by auto

subsubsection ‹Unit propagation for all clauses›
text ‹Finding the first clause to propagate›
fun find_first_unit_clause :: "'a literal list list ⇒ ('a, 'b, 'c) ann_literal list
  ⇒ ('a literal × 'a literal list) option"  where
"find_first_unit_clause (a # l) M =
  (case is_unit_clause a M of
    None ⇒ find_first_unit_clause l M
  | Some L ⇒ Some (L, a))" |
"find_first_unit_clause [] _ = None"

lemma find_first_unit_clause_some:
  "find_first_unit_clause l M = Some (a, c)
  ⟹ c ∈ set l ∧  M ⊨as CNot (mset c - {#a#}) ∧ undefined_lit M a ∧ a ∈ set c"
  apply (induction l)
    apply simp
  by (auto split: option.splits dest: is_unit_clause_some_in is_unit_clause_some_CNot
         is_unit_clause_some_undef)

lemma propagate_is_unit_clause_not_None:
  assumes dist: "distinct c" and
  M: "M ⊨as CNot (mset c - {#a#})" and
  undef: "undefined_lit M a" and
  ac: "a ∈ set c"
  shows "is_unit_clause c M ≠ None"
proof -
  have "[a←c . atm_of a ∉ atm_of ` lits_of M] = [a]"
    using assms
    proof (induction c)
      case Nil thus ?case by simp
    next
      case (Cons ac c)
      show ?case
        proof (cases "a = ac")
          case True
          thus ?thesis using Cons
            by (auto simp del: lits_of_unfold
                 simp add: lits_of_unfold[symmetric] Decided_Propagated_in_iff_in_lits_of
                   atm_of_eq_atm_of atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set)
        next
          case False
          hence T: "mset c + {#ac#} - {#a#} = mset c - {#a#} + {#ac#}"
            by (auto simp add: multiset_eq_iff)
          show ?thesis using False Cons
            by (auto simp add: T atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set)
        qed
    qed
  thus ?thesis
    using M unfolding is_unit_clause_def by auto
qed

lemma find_first_unit_clause_none:
  "distinct c ⟹ c ∈ set l ⟹  M ⊨as CNot (mset c - {#a#}) ⟹ undefined_lit M a ⟹ a ∈ set c
  ⟹ find_first_unit_clause l M ≠ None"
  by (induction l)
     (auto split: option.split simp add: propagate_is_unit_clause_not_None)

subsubsection ‹Decide›
fun find_first_unused_var :: "'a literal list list ⇒ 'a literal set ⇒ 'a literal option"  where
"find_first_unused_var (a # l) M =
  (case List.find (λlit. lit ∉ M ∧ -lit ∉ M) a of
    None ⇒ find_first_unused_var l M
  | Some a ⇒ Some a)" |
"find_first_unused_var [] _ = None"

lemma find_none[iff]:
  "List.find (λlit. lit ∉ M ∧ -lit ∉ M) a = None ⟷  atm_of ` set a ⊆ atm_of `  M"
  apply (induct a)
  using atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set
    by (force simp add:  atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set)+

lemma find_some: "List.find (λlit. lit ∉ M ∧ -lit ∉ M) a = Some b ⟹ b ∈ set a ∧ b ∉ M ∧ -b ∉ M"
  unfolding find_Some_iff by (metis nth_mem)

lemma find_first_unused_var_None[iff]:
  "find_first_unused_var l M = None ⟷ (∀a ∈ set l. atm_of ` set a ⊆ atm_of `  M)"
  by (induct l)
     (auto split: option.splits dest!: find_some
       simp add: image_subset_iff atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set)

lemma find_first_unused_var_Some_not_all_incl:
  assumes "find_first_unused_var l M = Some c"
  shows " ¬(∀a ∈ set l. atm_of ` set a ⊆ atm_of `  M)"
proof -
  have "find_first_unused_var l M ≠ None"
    using assms by (cases "find_first_unused_var l M") auto
  thus "¬(∀a ∈ set l. atm_of ` set a ⊆ atm_of `  M)" by auto
qed

lemma find_first_unused_var_Some:
  "find_first_unused_var l M = Some a ⟹ (∃m ∈ set l. a ∈ set m ∧ a ∉ M ∧ -a ∉ M)"
  by (induct l) (auto split: option.splits dest: find_some)

lemma find_first_unused_var_undefined:
  "find_first_unused_var l (lits_of Ms) = Some a ⟹ undefined_lit Ms a"
  using find_first_unused_var_Some[of l "lits_of Ms" a] Decided_Propagated_in_iff_in_lits_of
  by blast

end