Theory Watched_Literals_All_Literals

theory Watched_Literals_All_Literals
imports Watched_Literals_Clauses
begin

chapter ‹Set of all literals›

type_synonym ann_lits_l = ‹(nat, nat) ann_lits›
type_synonym clauses_to_update_ll = ‹nat list›


section ‹Refinement›

subsection ‹Set of all literals of the problem›

definition all_lits_of_mm :: ‹'a clauses ⇒ 'a literal multiset› where
‹all_lits_of_mm Ls = Pos `# (atm_of `# (∑⇩# Ls)) + Neg `# (atm_of `# (∑⇩# Ls))›

lemma all_lits_of_mm_empty[simp]: ‹all_lits_of_mm {#} = {#}›
  by (auto simp: all_lits_of_mm_def)
lemma in_all_lits_of_mm_ain_atms_of_iff:
  ‹L ∈# all_lits_of_mm N ⟷ atm_of L ∈ atms_of_mm N›
  by (cases L) (auto simp: all_lits_of_mm_def atms_of_ms_def atms_of_def)

lemma all_lits_of_mm_union:
  ‹all_lits_of_mm (M + N) = all_lits_of_mm M + all_lits_of_mm N›
  unfolding all_lits_of_mm_def by auto

definition all_lits_of_m :: ‹'a clause ⇒ 'a literal multiset› where
  ‹all_lits_of_m Ls = Pos `# (atm_of `# Ls) + Neg `# (atm_of `# Ls)›

lemma all_lits_of_m_empty[simp]: ‹all_lits_of_m {#} = {#}›
  by (auto simp: all_lits_of_m_def)

lemma all_lits_of_m_empty_iff[iff]: ‹all_lits_of_m A = {#} ⟷ A = {#}›
  by (cases A) (auto simp: all_lits_of_m_def)

lemma in_all_lits_of_m_ain_atms_of_iff: ‹L ∈# all_lits_of_m N ⟷ atm_of L ∈ atms_of N›
  by (cases L) (auto simp: all_lits_of_m_def atms_of_ms_def atms_of_def)

lemma in_clause_in_all_lits_of_m: ‹x ∈# C ⟹ x ∈# all_lits_of_m C›
  using atm_of_lit_in_atms_of in_all_lits_of_m_ain_atms_of_iff by blast

lemma all_lits_of_mm_add_mset:
  ‹all_lits_of_mm (add_mset C N) = (all_lits_of_m C) + (all_lits_of_mm N)›
  by (auto simp: all_lits_of_mm_def all_lits_of_m_def)

lemma all_lits_of_m_add_mset:
  ‹all_lits_of_m (add_mset L C) = add_mset L (add_mset (-L) (all_lits_of_m C))›
  by (cases L) (auto simp: all_lits_of_m_def)

lemma all_lits_of_m_union:
  ‹all_lits_of_m (A + B) = all_lits_of_m A + all_lits_of_m B›
  by (auto simp: all_lits_of_m_def)

lemma all_lits_of_m_mono:
  ‹D ⊆# D' ⟹ all_lits_of_m D ⊆# all_lits_of_m D'›
  by (auto elim!: mset_le_addE simp: all_lits_of_m_union)

lemma all_lits_of_m_diffD: ‹x ∈# all_lits_of_m (D - D') ⟹ x ∈# all_lits_of_m D›
  by (auto simp: all_lits_of_m_def dest: in_diffD)


lemma in_all_lits_of_mm_uminusD: ‹x2 ∈# all_lits_of_mm N ⟹ -x2 ∈# all_lits_of_mm N›
  by (auto simp: all_lits_of_mm_def)

lemma in_all_lits_of_mm_uminus_iff: ‹-x2 ∈# all_lits_of_mm N ⟷ x2 ∈# all_lits_of_mm N›
  by (cases x2) (auto simp: all_lits_of_mm_def)

lemma all_lits_of_mm_diffD:
  ‹L ∈# all_lits_of_mm (A - B) ⟹ L ∈# all_lits_of_mm A›
  apply (induction A arbitrary: B)
  subgoal by auto
  subgoal for a A' B
    by (cases ‹a ∈# B›)
      (fastforce dest!: multi_member_split[of a B] simp: all_lits_of_mm_add_mset)+
  done

lemma all_lits_of_mm_mono:
  ‹set_mset A ⊆ set_mset B ⟹ set_mset (all_lits_of_mm A) ⊆ set_mset (all_lits_of_mm B)›
  by (auto simp: all_lits_of_mm_def)


section ‹Conversion from set of atoms to set of literals›

text ‹We start in a context where we have an initial set of atoms. We later extend the locale to
  include a bound on the largest atom (in order to generate more efficient code).
›
context
  fixes 𝒜⇩i⇩n :: ‹'v multiset›
begin

text ‹This is the ∗‹completion› of \<^term>‹𝒜⇩i⇩n›, containing the positive and the negation of every
  literal of \<^term>‹𝒜⇩i⇩n›:›
definition ℒ⇩a⇩l⇩l where ‹ℒ⇩a⇩l⇩l = poss 𝒜⇩i⇩n + negs 𝒜⇩i⇩n›

lemma atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n: ‹atms_of ℒ⇩a⇩l⇩l = set_mset 𝒜⇩i⇩n›
  unfolding ℒ⇩a⇩l⇩l_def by (auto simp: atms_of_def image_Un image_image)

definition is_ℒ⇩a⇩l⇩l :: ‹'v literal multiset ⇒ bool› where
  ‹is_ℒ⇩a⇩l⇩l S ⟷ set_mset ℒ⇩a⇩l⇩l = set_mset S›

definition literals_are_in_ℒ⇩i⇩n :: ‹'v clause ⇒ bool› where
  ‹literals_are_in_ℒ⇩i⇩n C ⟷ set_mset (all_lits_of_m C) ⊆ set_mset ℒ⇩a⇩l⇩l›

lemma literals_are_in_ℒ⇩i⇩n_empty[simp]: ‹literals_are_in_ℒ⇩i⇩n {#}›
  by (auto simp: literals_are_in_ℒ⇩i⇩n_def)

lemma in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff: ‹x ∈# ℒ⇩a⇩l⇩l ⟷ atm_of x ∈ atms_of ℒ⇩a⇩l⇩l›
  by (cases x) (auto simp: ℒ⇩a⇩l⇩l_def atms_of_def atm_of_eq_atm_of image_Un image_image)

lemma literals_are_in_ℒ⇩i⇩n_add_mset:
  ‹literals_are_in_ℒ⇩i⇩n (add_mset L A) ⟷ literals_are_in_ℒ⇩i⇩n A ∧ L ∈# ℒ⇩a⇩l⇩l›
  by (auto simp: literals_are_in_ℒ⇩i⇩n_def all_lits_of_m_add_mset in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff)

lemma literals_are_in_ℒ⇩i⇩n_mono:
  assumes N: ‹literals_are_in_ℒ⇩i⇩n D'› and D: ‹D ⊆# D'›
  shows ‹literals_are_in_ℒ⇩i⇩n D›
proof -
  have ‹set_mset (all_lits_of_m D) ⊆ set_mset (all_lits_of_m D')›
    using D by (auto simp: in_all_lits_of_m_ain_atms_of_iff atm_iff_pos_or_neg_lit)
  then show ?thesis
     using N unfolding literals_are_in_ℒ⇩i⇩n_def by fast
qed

lemma literals_are_in_ℒ⇩i⇩n_sub:
  ‹literals_are_in_ℒ⇩i⇩n y ⟹ literals_are_in_ℒ⇩i⇩n (y - z)›
  using literals_are_in_ℒ⇩i⇩n_mono[of y ‹y - z›] by auto

lemma all_lits_of_m_subset_all_lits_of_mmD:
  ‹a ∈# b ⟹ set_mset (all_lits_of_m a) ⊆ set_mset (all_lits_of_mm b)›
  by (auto simp: all_lits_of_m_def all_lits_of_mm_def)

lemma all_lits_of_m_remdups_mset:
  ‹set_mset (all_lits_of_m (remdups_mset N)) = set_mset (all_lits_of_m N)›
  by (auto simp: all_lits_of_m_def)

lemma literals_are_in_ℒ⇩i⇩n_remdups[simp]:
  ‹literals_are_in_ℒ⇩i⇩n (remdups_mset N) = literals_are_in_ℒ⇩i⇩n N›
  by (auto simp: literals_are_in_ℒ⇩i⇩n_def all_lits_of_m_remdups_mset)

lemma uminus_𝒜⇩i⇩n_iff: ‹- L ∈# ℒ⇩a⇩l⇩l ⟷ L ∈# ℒ⇩a⇩l⇩l›
  by (simp add: in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff)

definition literals_are_in_ℒ⇩i⇩n_mm :: ‹'v clauses ⇒ bool› where
  ‹literals_are_in_ℒ⇩i⇩n_mm C ⟷ set_mset (all_lits_of_mm C) ⊆ set_mset ℒ⇩a⇩l⇩l›

lemma literals_are_in_ℒ⇩i⇩n_mm_add_msetD:
  ‹literals_are_in_ℒ⇩i⇩n_mm (add_mset C N) ⟹ L ∈# C ⟹ L ∈# ℒ⇩a⇩l⇩l›
  by (auto simp: literals_are_in_ℒ⇩i⇩n_mm_def all_lits_of_mm_add_mset
      all_lits_of_m_add_mset
    dest!: multi_member_split)

lemma literals_are_in_ℒ⇩i⇩n_mm_add_mset:
  ‹literals_are_in_ℒ⇩i⇩n_mm (add_mset C N) ⟷
    literals_are_in_ℒ⇩i⇩n_mm N ∧ literals_are_in_ℒ⇩i⇩n C›
  unfolding literals_are_in_ℒ⇩i⇩n_mm_def  literals_are_in_ℒ⇩i⇩n_def
  by (auto simp: all_lits_of_mm_add_mset)

definition literals_are_in_ℒ⇩i⇩n_trail :: ‹('v, 'mark) ann_lits ⇒ bool› where
  ‹literals_are_in_ℒ⇩i⇩n_trail M ⟷ set_mset (lit_of `# mset M) ⊆ set_mset ℒ⇩a⇩l⇩l›

lemma literals_are_in_ℒ⇩i⇩n_trail_in_lits_of_l:
  ‹literals_are_in_ℒ⇩i⇩n_trail M ⟹ a ∈ lits_of_l M ⟹ a ∈# ℒ⇩a⇩l⇩l›
  by (auto simp: literals_are_in_ℒ⇩i⇩n_trail_def lits_of_def)

lemma literals_are_in_ℒ⇩i⇩n_trail_uminus_in_lits_of_l:
  ‹literals_are_in_ℒ⇩i⇩n_trail M ⟹ -a ∈ lits_of_l M ⟹ a ∈# ℒ⇩a⇩l⇩l›
  by (auto simp: literals_are_in_ℒ⇩i⇩n_trail_def lits_of_def uminus_lit_swap uminus_𝒜⇩i⇩n_iff)

lemma literals_are_in_ℒ⇩i⇩n_trail_uminus_in_lits_of_l_atms:
  ‹literals_are_in_ℒ⇩i⇩n_trail M ⟹ -a ∈ lits_of_l M ⟹ atm_of a ∈# 𝒜⇩i⇩n›
  using literals_are_in_ℒ⇩i⇩n_trail_uminus_in_lits_of_l[of M a]
  unfolding in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff[symmetric] atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n[symmetric]
  .
end

lemma isasat_input_ops_ℒ⇩a⇩l⇩l_empty[simp]:
  ‹ℒ⇩a⇩l⇩l {#} = {#}›
  unfolding ℒ⇩a⇩l⇩l_def
  by auto

lemma ℒ⇩a⇩l⇩l_atm_of_all_lits_of_mm: ‹set_mset (ℒ⇩a⇩l⇩l (atm_of `#  all_lits_of_mm A)) = set_mset (all_lits_of_mm A)›
  apply (auto simp: ℒ⇩a⇩l⇩l_def in_all_lits_of_mm_ain_atms_of_iff)
  by (metis (no_types, lifting) image_iff in_all_lits_of_mm_ain_atms_of_iff literal.exhaust_sel)


definition all_lits :: ‹('a, 'v literal list × 'b) fmap ⇒ 'v literal multiset multiset ⇒
   'v literal multiset› where
  ‹all_lits S NUE = all_lits_of_mm ((λC. mset (fst C)) `# ran_m S + NUE)›

lemma all_lits_alt_def:
  ‹all_lits S NUE = all_lits_of_mm (mset `# ran_mf S + NUE)›
  unfolding all_lits_def
  by auto

lemma all_lits_alt_def2:
  ‹all_lits S (NUE + NUS + N0S) = all_lits_of_mm (mset `# ran_mf S + NUE + NUS + N0S)›
  ‹all_lits S (NUE + NUS + N0S) = all_lits_of_mm ((λC. mset (fst C)) `# ran_m S + NUE + NUS + N0S)›
  unfolding all_lits_def
  by (auto simp: ac_simps)

lemma literals_are_in_ℒ⇩i⇩n_mm_in_ℒ⇩a⇩l⇩l:
  assumes
    N1: ‹literals_are_in_ℒ⇩i⇩n_mm 𝒜 (mset `# ran_mf xs)› and
    i_xs: ‹i ∈# dom_m xs› and j_xs: ‹j < length (xs ∝ i)›
  shows ‹xs ∝ i ! j ∈# ℒ⇩a⇩l⇩l 𝒜›
proof -
  have ‹xs ∝ i ∈# ran_mf xs›
    using i_xs by auto
  then have ‹xs ∝ i ! j ∈ set_mset (all_lits_of_mm (mset `# ran_mf xs))›
    using j_xs by (auto simp: in_all_lits_of_mm_ain_atms_of_iff atms_of_ms_def Bex_def
      intro!: exI[of _ ‹xs ∝ i›])
  then show ?thesis
    using N1 unfolding literals_are_in_ℒ⇩i⇩n_mm_def by blast
qed


lemma literals_are_in_ℒ⇩i⇩n_trail_in_lits_of_l_atms:
  ‹literals_are_in_ℒ⇩i⇩n_trail 𝒜⇩i⇩n M ⟹ a ∈ lits_of_l M ⟹ atm_of a ∈# 𝒜⇩i⇩n›
  using literals_are_in_ℒ⇩i⇩n_trail_in_lits_of_l[of 𝒜⇩i⇩n M a]
  unfolding in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff[symmetric] atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n[symmetric]
  .

lemma literals_are_in_ℒ⇩i⇩n_trail_Cons:
  ‹literals_are_in_ℒ⇩i⇩n_trail 𝒜⇩i⇩n (L # M) ⟷
      literals_are_in_ℒ⇩i⇩n_trail 𝒜⇩i⇩n M ∧ lit_of L ∈# ℒ⇩a⇩l⇩l 𝒜⇩i⇩n›
  by (auto simp: literals_are_in_ℒ⇩i⇩n_trail_def)

lemma literals_are_in_ℒ⇩i⇩n_trail_empty[simp]:
  ‹literals_are_in_ℒ⇩i⇩n_trail 𝒜 []›
  by (auto simp: literals_are_in_ℒ⇩i⇩n_trail_def)

lemma literals_are_in_ℒ⇩i⇩n_trail_lit_of_mset:
  ‹literals_are_in_ℒ⇩i⇩n_trail 𝒜 M = literals_are_in_ℒ⇩i⇩n 𝒜 (lit_of `# mset M)›
  by (induction M) (auto simp: literals_are_in_ℒ⇩i⇩n_add_mset literals_are_in_ℒ⇩i⇩n_trail_Cons)

lemma literals_are_in_ℒ⇩i⇩n_in_mset_ℒ⇩a⇩l⇩l:
  ‹literals_are_in_ℒ⇩i⇩n 𝒜 C ⟹ L ∈# C ⟹ L ∈# ℒ⇩a⇩l⇩l 𝒜›
  unfolding literals_are_in_ℒ⇩i⇩n_def
  by (auto dest!: multi_member_split simp: all_lits_of_m_add_mset)

lemma literals_are_in_ℒ⇩i⇩n_in_ℒ⇩a⇩l⇩l:
  assumes
    N1: ‹literals_are_in_ℒ⇩i⇩n 𝒜 (mset xs)› and
    i_xs: ‹i < length xs›
  shows ‹xs ! i ∈# ℒ⇩a⇩l⇩l 𝒜›
  using literals_are_in_ℒ⇩i⇩n_in_mset_ℒ⇩a⇩l⇩l[of 𝒜 ‹mset xs› ‹xs!i›] assms by auto

lemma is_ℒ⇩a⇩l⇩l_ℒ⇩a⇩l⇩l_rewrite[simp]:
  ‹is_ℒ⇩a⇩l⇩l 𝒜 (all_lits_of_mm 𝒜') ⟹
    set_mset (ℒ⇩a⇩l⇩l (atm_of `# all_lits_of_mm 𝒜')) = set_mset (ℒ⇩a⇩l⇩l 𝒜)›
  using in_all_lits_of_mm_ain_atms_of_iff
  unfolding set_mset_set_mset_eq_iff is_ℒ⇩a⇩l⇩l_def Ball_def in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff
    in_all_lits_of_mm_ain_atms_of_iff atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n
  by (auto simp: in_all_lits_of_mm_ain_atms_of_iff)

lemma is_ℒ⇩a⇩l⇩l_alt_def: ‹is_ℒ⇩a⇩l⇩l 𝒜 (all_lits_of_mm A) ⟷ atms_of (ℒ⇩a⇩l⇩l 𝒜) = atms_of_mm A›
  unfolding set_mset_set_mset_eq_iff is_ℒ⇩a⇩l⇩l_def Ball_def in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff
    in_all_lits_of_mm_ain_atms_of_iff
  by auto (metis literal.sel(2))+

lemma in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n: ‹L ∈# ℒ⇩a⇩l⇩l 𝒜⇩i⇩n ⟷ atm_of L ∈# 𝒜⇩i⇩n›
  by (cases L) (auto simp: ℒ⇩a⇩l⇩l_def)

lemma literals_are_in_ℒ⇩i⇩n_alt_def:
  ‹literals_are_in_ℒ⇩i⇩n 𝒜 S ⟷ atms_of S ⊆ atms_of (ℒ⇩a⇩l⇩l 𝒜)›
  apply (auto simp: literals_are_in_ℒ⇩i⇩n_def all_lits_of_mm_union lits_of_def
       in_all_lits_of_m_ain_atms_of_iff in_all_lits_of_mm_ain_atms_of_iff atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n
       atm_of_eq_atm_of uminus_𝒜⇩i⇩n_iff subset_iff in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n)
  apply (auto simp: atms_of_def)
  done

lemma literals_are_in_ℒ⇩i⇩n_trail_atm_of:
  ‹literals_are_in_ℒ⇩i⇩n_trail 𝒜⇩i⇩n M ⟷ atm_of ` lits_of_l M ⊆ set_mset 𝒜⇩i⇩n›
  apply (rule iffI)
  subgoal by (auto dest: literals_are_in_ℒ⇩i⇩n_trail_in_lits_of_l_atms)
  subgoal by (fastforce simp: literals_are_in_ℒ⇩i⇩n_trail_def lits_of_def in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n)
  done

lemma literals_are_in_ℒ⇩i⇩n_poss_remdups_mset:
  ‹literals_are_in_ℒ⇩i⇩n 𝒜⇩i⇩n (poss (remdups_mset (atm_of `# C))) ⟷ literals_are_in_ℒ⇩i⇩n 𝒜⇩i⇩n C›
  by (induction C)
    (auto simp: literals_are_in_ℒ⇩i⇩n_add_mset in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff atm_of_eq_atm_of
      dest!: multi_member_split)

lemma literals_are_in_ℒ⇩i⇩n_negs_remdups_mset:
  ‹literals_are_in_ℒ⇩i⇩n 𝒜⇩i⇩n (negs (remdups_mset (atm_of `# C))) ⟷ literals_are_in_ℒ⇩i⇩n 𝒜⇩i⇩n C›
  by (induction C)
    (auto simp: literals_are_in_ℒ⇩i⇩n_add_mset in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff atm_of_eq_atm_of
      dest!: multi_member_split)

lemma ℒ⇩a⇩l⇩l_atm_of_all_lits_of_m:
   ‹set_mset (ℒ⇩a⇩l⇩l (atm_of `# all_lits_of_m C)) = set_mset C ∪ uminus ` set_mset C›
  supply lit_eq_Neg_Pos_iff[iff]
  by (auto simp: ℒ⇩a⇩l⇩l_def all_lits_of_m_def image_iff dest!: multi_member_split)

lemma atm_of_all_lits_of_mm:
  ‹set_mset (atm_of `# all_lits_of_mm bw) = atms_of_mm bw›
  ‹atm_of ` set_mset (all_lits_of_mm bw) = atms_of_mm bw›
  using in_all_lits_of_mm_ain_atms_of_iff apply (auto simp: image_iff)
  by (metis (full_types) image_eqI literal.sel(1))+

lemma ℒ⇩a⇩l⇩l_union:
   ‹set_mset (ℒ⇩a⇩l⇩l (A + B)) = set_mset (ℒ⇩a⇩l⇩l  A) ∪ set_mset (ℒ⇩a⇩l⇩l  B)›
  by (auto simp: ℒ⇩a⇩l⇩l_def)

lemma ℒ⇩a⇩l⇩l_cong:
  ‹set_mset A = set_mset B ⟹ set_mset (ℒ⇩a⇩l⇩l A) = set_mset (ℒ⇩a⇩l⇩l B)›
  by (auto simp: ℒ⇩a⇩l⇩l_def)

lemma atms_of_ℒ⇩a⇩l⇩l_cong:
  ‹set_mset 𝒜 = set_mset ℬ ⟹ atms_of (ℒ⇩a⇩l⇩l 𝒜) = atms_of (ℒ⇩a⇩l⇩l ℬ)›
  unfolding ℒ⇩a⇩l⇩l_def
  by auto

lemma is_ℒ⇩a⇩l⇩l_cong:
  ‹set_mset 𝒜 = set_mset ℬ ⟹ is_ℒ⇩a⇩l⇩l 𝒜 =  is_ℒ⇩a⇩l⇩l ℬ›
  unfolding ℒ⇩a⇩l⇩l_def is_ℒ⇩a⇩l⇩l_def
  by auto


text ‹The definition is here to be shared later.›
definition get_propagation_reason :: ‹('v, 'mark) ann_lits ⇒ 'v literal ⇒ 'mark option nres› where
  ‹get_propagation_reason M L = SPEC(λC. C ≠ None ⟶ Propagated L (the C) ∈ set M)›


end