Theory CDCL_Abstract_Clause_Representation

theory CDCL_Abstract_Clause_Representation
imports Entailment_Definition.Partial_Herbrand_Interpretation
begin

type_synonym 'v clause = "'v literal multiset"
type_synonym 'v clauses = "'v clause multiset"


subsection ‹Abstract Clause Representation›

text ‹We will abstract the representation of clause and clauses via two locales. We expect our
  representation to behave like multiset, but the internal representation can be done using list
  or whatever other representation.

  We assume the following:
  ▪ there is an equivalent to adding and removing a literal and to taking the union of clauses.
  ›

locale raw_cls =
   fixes
    mset_cls :: "'cls ⇒ 'v clause"
begin
end

text ‹The two following locales are the ∗‹exact same› locale, but we need two different locales.
  Otherwise, instantiating @{text raw_clss} would lead to duplicate constants.›
locale abstract_with_index =
  fixes
    get_lit :: "'a ⇒ 'it ⇒ 'conc option" and
    convert_to_mset :: "'a ⇒ 'conc multiset"
  assumes
    in_clss_mset_cls[dest]:
      "get_lit Cs a = Some e ⟹ e ∈# convert_to_mset Cs" and
    in_mset_cls_exists_preimage:
      "b ∈# convert_to_mset Cs ⟹ ∃b'. get_lit Cs b' = Some b"

locale abstract_with_index2 =
  fixes
    get_lit :: "'a ⇒ 'it ⇒ 'conc option" and
    convert_to_mset :: "'a ⇒ 'conc multiset"
  assumes
    in_clss_mset_clss[dest]:
      "get_lit Cs a = Some e ⟹ e ∈# convert_to_mset Cs" and
    in_mset_clss_exists_preimage:
      "b ∈# convert_to_mset Cs ⟹ ∃b'. get_lit Cs b' = Some b"

locale raw_clss =
  abstract_with_index get_lit mset_cls +
  abstract_with_index2 get_cls mset_clss
  for
    get_lit :: "'cls ⇒ 'lit ⇒ 'v literal option" and
    mset_cls :: "'cls ⇒ 'v clause" and

    get_cls :: "'clss ⇒ 'cls_it ⇒ 'cls option" and
    mset_clss:: "'clss ⇒ 'cls multiset"
begin

definition cls_lit :: "'cls ⇒ 'lit ⇒ 'v literal" (infix "↓" 49) where
"C ↓ a ≡ the (get_lit C a)"

definition clss_cls :: "'clss ⇒ 'cls_it ⇒ 'cls" (infix "⇓" 49) where
"C ⇓ a ≡ the (get_cls C a)"

definition in_cls :: "'lit ⇒ 'cls ⇒ bool" (infix "∈↓" 49) where
"a ∈↓ Cs ≡ get_lit Cs a ≠ None"

definition in_clss :: "'cls_it ⇒ 'clss ⇒ bool" (infix "∈⇓" 49) where
"a ∈⇓ Cs ≡ get_cls Cs a ≠ None"

definition raw_clss where
"raw_clss S ≡ image_mset mset_cls (mset_clss S)"

end

experiment
begin
  fun safe_nth where
  "safe_nth (x # _) 0 = Some x" |
  "safe_nth (_ # xs) (Suc n) = safe_nth xs n" |
  "safe_nth [] _ = None"

  lemma safe_nth_nth: "n < length l ⟹ safe_nth l n = Some (nth l n)"
    by (induction l n rule: safe_nth.induct) auto

  lemma safe_nth_None: "n ≥ length l ⟹ safe_nth l n = None"
    by (induction l n rule: safe_nth.induct) auto

  lemma safe_nth_Some_iff: "safe_nth l n = Some m ⟷ n < length l ∧ m = nth l n"
    apply (rule iffI)
      defer apply (auto simp: safe_nth_nth)[]
    by (induction l n rule: safe_nth.induct) auto

  lemma safe_nth_None_iff: "safe_nth l n = None ⟷ n ≥ length l"
    apply (rule iffI)
      defer apply (auto simp: safe_nth_None)[]
    by (induction l n rule: safe_nth.induct) auto

  interpretation abstract_with_index
    safe_nth
    mset
    apply unfold_locales
      apply (simp add: safe_nth_Some_iff)
    by (metis in_set_conv_nth safe_nth_nth set_mset_mset)

  interpretation abstract_with_index2
    safe_nth
    mset
    apply unfold_locales
      apply (simp add: safe_nth_Some_iff)
    by (metis in_set_conv_nth safe_nth_nth set_mset_mset)

  interpretation list_cls: raw_clss
    safe_nth mset
    safe_nth mset
    by unfold_locales
end

end