Theory Watched_Literals_Clauses

theory Watched_Literals_Clauses
imports More_Sepref.WB_More_Refinement_List Watched_Literals_Transition_System
begin

type_synonym 'v clause_l = ‹'v literal list›
type_synonym 'v clauses_l = ‹(nat, ('v clause_l × bool)) fmap›

abbreviation watched_l :: ‹'a clause_l ⇒ 'a clause_l› where
  ‹watched_l l ≡ take 2 l›

abbreviation unwatched_l :: ‹'a clause_l ⇒ 'a clause_l›  where
  ‹unwatched_l l ≡ drop 2 l›

fun twl_clause_of :: ‹'a clause_l ⇒ 'a clause twl_clause› where
  ‹twl_clause_of l = TWL_Clause (mset (watched_l l)) (mset (unwatched_l l))›

abbreviation clause_in :: ‹'v clauses_l ⇒ nat ⇒ 'v clause_l› (infix "∝" 101) where
  ‹N ∝ i ≡ fst (the (fmlookup N i))›

abbreviation clause_upd :: ‹'v clauses_l ⇒ nat ⇒ 'v clause_l ⇒ 'v clauses_l›  where
  ‹clause_upd N i C ≡ fmupd i (C, snd (the (fmlookup N i))) N›

text ‹Taken from \<^term>‹fun_upd›.›
nonterminal updclsss and updclss

syntax
  "_updclss" :: "'a clauses_l ⇒ 'a ⇒ updclss"             ("(2_ ↪/ _)")
  ""         :: "updbind ⇒ updbinds"             ("_")
  "_updclsss":: "updclss ⇒ updclsss ⇒ updclsss" ("_,/ _")
  "_Updateclss"  :: "'a ⇒ updclss ⇒ 'a"            ("_/'((_)')" [1000, 0] 900)

translations
  "_Updateclss f (_updclsss b bs)" ⇌ "_Updateclss (_Updateclss f b) bs"
  "f(x ↪ y)" ⇌ "CONST clause_upd f x y"


abbreviation ran_mf :: ‹'v clauses_l ⇒ 'v clause_l multiset› where
  ‹ran_mf N ≡ fst `# ran_m N›

abbreviation learned_clss_l :: ‹'v clauses_l ⇒ ('v clause_l × bool) multiset› where
  ‹learned_clss_l N ≡ {#C ∈# ran_m N. ¬snd C#}›

abbreviation learned_clss_lf :: ‹'v clauses_l ⇒ 'v clause_l multiset› where
  ‹learned_clss_lf N ≡ fst `# learned_clss_l N›

abbreviation init_clss_l :: ‹'v clauses_l ⇒ ('v clause_l × bool) multiset› where
  ‹init_clss_l N ≡ {#C ∈# ran_m N. snd C#}›

abbreviation init_clss_lf :: ‹'v clauses_l ⇒ 'v clause_l multiset› where
  ‹init_clss_lf N ≡ fst `# init_clss_l N›

abbreviation all_clss_l :: ‹'v clauses_l ⇒ ('v clause_l × bool) multiset› where
  ‹all_clss_l N ≡ init_clss_l N + learned_clss_l N›

lemma all_clss_l_ran_m[simp]:
  ‹all_clss_l N = ran_m N›
  by (metis multiset_partition)

abbreviation all_clss_lf :: ‹'v clauses_l ⇒ 'v clause_l multiset› where
  ‹all_clss_lf N ≡ init_clss_lf N + learned_clss_lf N›

lemma all_clss_lf_ran_m: ‹all_clss_lf N = fst `# ran_m N›
  by (metis (no_types) image_mset_union multiset_partition)

abbreviation irred :: ‹'v clauses_l ⇒ nat ⇒ bool› where
  ‹irred N C ≡ snd (the (fmlookup N C))›

definition irred' where ‹irred' = irred›

lemma ran_m_ran: ‹fset_mset (ran_m N) = fmran N›
  unfolding ran_m_def ran_def
  apply (auto simp: fmlookup_ran_iff dom_m_def elim!: fmdomE)
   apply (metis fmdomE notin_fset option.sel)
  by (metis (no_types, lifting) fmdomI fmember.rep_eq image_iff option.sel)

lemma ran_m_clause_upd:
  assumes
    NC: ‹C ∈# dom_m N›
  shows ‹ran_m (N(C ↪ C')) =
         add_mset (C', irred N C) (remove1_mset (N ∝ C, irred N C) (ran_m N))›
proof -
  define N' where
    ‹N' = fmdrop C N›
  have N_N': ‹dom_m N = add_mset C (dom_m N')›
    using NC unfolding N'_def by auto
  have ‹C ∉# dom_m N'›
    using NC distinct_mset_dom[of N] unfolding N_N' by auto
  then show ?thesis
    by (auto simp: N_N' ran_m_def mset_set.insert_remove image_mset_remove1_mset_if
      intro!: image_mset_cong)
qed

lemma ran_m_mapsto_upd:
  assumes
    NC: ‹C ∈# dom_m N›
  shows ‹ran_m (fmupd C C' N) =
         add_mset C' (remove1_mset (N ∝ C, irred N C) (ran_m N))›
proof -
  define N' where
    ‹N' = fmdrop C N›
  have N_N': ‹dom_m N = add_mset C (dom_m N')›
    using NC unfolding N'_def by auto
  have ‹C ∉# dom_m N'›
    using NC distinct_mset_dom[of N] unfolding N_N' by auto
  then show ?thesis
    by (auto simp: N_N' ran_m_def mset_set.insert_remove image_mset_remove1_mset_if
      intro!: image_mset_cong)
qed

lemma ran_m_mapsto_upd_notin:
  assumes
    NC: ‹C ∉# dom_m N›
  shows ‹ran_m (fmupd C C' N) = add_mset C' (ran_m N)›
  using NC
  by (auto simp: ran_m_def mset_set.insert_remove image_mset_remove1_mset_if
      intro!: image_mset_cong split: if_splits)

lemma learned_clss_l_update[simp]:
  ‹bh ∈# dom_m ax ⟹ size (learned_clss_l (ax(bh ↪ C))) = size (learned_clss_l ax)›
  by (auto simp: ran_m_clause_upd size_Diff_singleton_if dest!: multi_member_split)
     (auto simp: ran_m_def)

lemma Ball_ran_m_dom:
  ‹(∀x∈#ran_m N. P (fst x)) ⟷ (∀x∈#dom_m N. P (N ∝ x))›
  by (auto simp: ran_m_def)

lemma Ball_ran_m_dom_struct_wf:
  ‹(∀x∈#ran_m N. struct_wf_twl_cls (twl_clause_of (fst x))) ⟷
     (∀x∈# dom_m N. struct_wf_twl_cls (twl_clause_of (N ∝ x)))›
  by (rule Ball_ran_m_dom)

lemma init_clss_lf_fmdrop[simp]:
  ‹irred N C ⟹ C ∈# dom_m N ⟹ init_clss_lf (fmdrop C N) = remove1_mset (N∝C) (init_clss_lf N)›
  using distinct_mset_dom[of N]
  by (auto simp: ran_m_def image_mset_If_eq_notin[of C _ the] dest!: multi_member_split)

lemma init_clss_lf_fmdrop_irrelev[simp]:
  ‹¬irred N C ⟹ init_clss_lf (fmdrop C N) = init_clss_lf N›
  using distinct_mset_dom[of N]
  apply (cases ‹C ∈# dom_m N›)
  by (auto simp: ran_m_def image_mset_If_eq_notin[of C _ the] dest!: multi_member_split)

lemma learned_clss_lf_lf_fmdrop[simp]:
  ‹¬irred N C ⟹ C ∈# dom_m N ⟹ learned_clss_lf (fmdrop C N) = remove1_mset (N∝C) (learned_clss_lf N)›
  using distinct_mset_dom[of N]
  apply (cases ‹C ∈# dom_m N›)
  by (auto simp: ran_m_def image_mset_If_eq_notin[of C _ the] dest!: multi_member_split)

lemma learned_clss_l_l_fmdrop: ‹¬ irred N C ⟹ C ∈# dom_m N ⟹
  learned_clss_l (fmdrop C N) = remove1_mset (the (fmlookup N C)) (learned_clss_l N)›
  using distinct_mset_dom[of N]
  apply (cases ‹C ∈# dom_m N›)
  by (auto simp: ran_m_def image_mset_If_eq_notin[of C _ the] dest!: multi_member_split)

lemma learned_clss_lf_lf_fmdrop_irrelev[simp]:
  ‹irred N C ⟹ learned_clss_lf (fmdrop C N) = learned_clss_lf N›
  using distinct_mset_dom[of N]
  apply (cases ‹C ∈# dom_m N›)
  by (auto simp: ran_m_def image_mset_If_eq_notin[of C _ the] dest!: multi_member_split)

lemma ran_mf_lf_fmdrop[simp]:
  ‹C ∈# dom_m N ⟹  ran_mf (fmdrop C N) = remove1_mset (N∝C) (ran_mf N)›
  using distinct_mset_dom[of N]
  by (auto simp: ran_m_def image_mset_If_eq_notin[of C _ ‹λx. fst (the x)›] dest!: multi_member_split)

lemma ran_mf_lf_fmdrop_notin[simp]:
  ‹C ∉# dom_m N ⟹  ran_mf (fmdrop C N) = ran_mf N›
  using distinct_mset_dom[of N]
  by (auto simp: ran_m_def image_mset_If_eq_notin[of C _ ‹λx. fst (the x)›] dest!: multi_member_split)

lemma lookup_None_notin_dom_m[simp]:
  ‹fmlookup N i = None ⟷ i ∉# dom_m N›
  by (auto simp: dom_m_def fmlookup_dom_iff fmember.rep_eq[symmetric])

text ‹While it is tempting to mark the two following theorems as [simp], this would break more
  simplifications since \<^term>‹ran_mf› is only an abbreviation for \<^term>‹ran_m›.
›
lemma ran_m_fmdrop:
  ‹C ∈# dom_m N ⟹  ran_m (fmdrop C N) = remove1_mset (N ∝ C, irred N C) (ran_m N)›
  using distinct_mset_dom[of N]
  by (cases ‹fmlookup N C›)
    (auto simp: ran_m_def image_mset_If_eq_notin[of C _ ‹λx. fst (the x)›]
     dest!: multi_member_split
    intro!: filter_mset_cong2 image_mset_cong2)

lemma ran_m_fmdrop_notin:
  ‹C ∉# dom_m N ⟹ ran_m (fmdrop C N) = ran_m N›
  using distinct_mset_dom[of N]
  by (auto simp: ran_m_def image_mset_If_eq_notin[of C _ ‹λx. fst (the x)›]
    dest!: multi_member_split
    intro!: filter_mset_cong2 image_mset_cong2)

lemma init_clss_l_fmdrop_irrelev:
  ‹¬irred N C ⟹ init_clss_l (fmdrop C N) = init_clss_l N›
  using distinct_mset_dom[of N]
  apply (cases ‹C ∈# dom_m N›)
  by (auto simp: ran_m_def image_mset_If_eq_notin[of C _ the] dest!: multi_member_split)

lemma init_clss_l_fmdrop:
  ‹irred N C ⟹ C ∈# dom_m N ⟹ init_clss_l (fmdrop C N) = remove1_mset (the (fmlookup N C)) (init_clss_l N)›
  using distinct_mset_dom[of N]
  by (auto simp: ran_m_def image_mset_If_eq_notin[of C _ the] dest!: multi_member_split)

lemma ran_m_lf_fmdrop:
  ‹C ∈# dom_m N ⟹ ran_m (fmdrop C N) = remove1_mset (the (fmlookup N C)) (ran_m N)›
  using distinct_mset_dom[of N]
  by (auto simp: ran_m_def image_mset_If_eq_notin[of C _ ‹λx. fst (the x)›] dest!: multi_member_split
    intro!: image_mset_cong)
lemma set_clauses_simp[simp]:
  ‹f ` {a. a ∈# ran_m N ∧ ¬ snd a} ∪ f ` {a. a ∈# ran_m N ∧ snd a} ∪ A =
   f ` {a. a ∈# ran_m N} ∪ A›
  by auto

lemma init_clss_l_clause_upd:
  ‹C ∈# dom_m N ⟹ irred N C ⟹
    init_clss_l (N(C ↪ C')) =
     add_mset (C', irred N C) (remove1_mset (N ∝ C, irred N C) (init_clss_l N))›
  by (auto simp: ran_m_mapsto_upd)

lemma init_clss_l_mapsto_upd:
  ‹C ∈# dom_m N ⟹ irred N C ⟹
   init_clss_l (fmupd C (C', True) N) =
     add_mset (C', irred N C) (remove1_mset (N ∝ C, irred N C) (init_clss_l N))›
  by (auto simp: ran_m_mapsto_upd)

lemma learned_clss_l_mapsto_upd:
  ‹C ∈# dom_m N ⟹ ¬irred N C ⟹
   learned_clss_l (fmupd C (C', False) N) =
      add_mset (C', irred N C) (remove1_mset (N ∝ C, irred N C) (learned_clss_l N))›
  by (auto simp: ran_m_mapsto_upd)

lemma init_clss_l_mapsto_upd_irrel: ‹C ∈# dom_m N ⟹ ¬irred N C ⟹
  init_clss_l (fmupd C (C', False) N) = init_clss_l N›
  by (auto simp: ran_m_mapsto_upd)

lemma init_clss_l_mapsto_upd_irrel_notin: ‹C ∉# dom_m N ⟹
  init_clss_l (fmupd C (C', False) N) = init_clss_l N›
  by (auto simp: ran_m_mapsto_upd_notin)

lemma learned_clss_l_mapsto_upd_irrel: ‹C ∈# dom_m N ⟹ irred N C ⟹
  learned_clss_l (fmupd C (C', True) N) = learned_clss_l N›
  by (auto simp: ran_m_mapsto_upd)

lemma learned_clss_l_mapsto_upd_notin: ‹C ∉# dom_m N ⟹
  learned_clss_l (fmupd C  (C', False) N) = add_mset (C', False) (learned_clss_l N)›
  by (auto simp: ran_m_mapsto_upd_notin)

lemma in_ran_mf_clause_inI[intro]:
  ‹C ∈# dom_m N ⟹ i = irred N C ⟹ (N ∝ C, i) ∈# ran_m N›
  by (auto simp: ran_m_def dom_m_def)

lemma init_clss_l_mapsto_upd_notin:
  ‹C ∉# dom_m N ⟹ init_clss_l (fmupd C (C', True) N) =
     add_mset (C', True) (init_clss_l N)›
  by (auto simp: ran_m_mapsto_upd_notin)

lemma learned_clss_l_mapsto_upd_notin_irrelev: ‹C ∉# dom_m N ⟹
  learned_clss_l (fmupd C  (C', True) N) = learned_clss_l N›
  by (auto simp: ran_m_mapsto_upd_notin)

lemma clause_twl_clause_of:  ‹clause (twl_clause_of C) = mset C› for C
    by (cases C; cases ‹tl C›) auto

lemma learned_clss_l_l_fmdrop_irrelev: ‹irred N C ⟹
  learned_clss_l (fmdrop C N) = learned_clss_l N›
  using distinct_mset_dom[of N]
  apply (cases ‹C ∈# dom_m N›)
  by (auto simp: ran_m_def image_mset_If_eq_notin[of C _ the] dest!: multi_member_split)

lemma init_clss_l_fmdrop_if:
  ‹C ∈# dom_m N ⟹ init_clss_l (fmdrop C N) = (if irred N C then remove1_mset (the (fmlookup N C)) (init_clss_l N)
    else init_clss_l N)›
  by (auto simp: init_clss_l_fmdrop init_clss_l_fmdrop_irrelev)

lemma init_clss_l_fmupd_if:
  ‹C' ∉# dom_m new ⟹ init_clss_l (fmupd C' D new) = (if snd D then add_mset D (init_clss_l new) else init_clss_l new)›
  by (cases D) (auto simp: init_clss_l_mapsto_upd_irrel_notin init_clss_l_mapsto_upd_notin)

lemma learned_clss_l_fmdrop_if:
  ‹C ∈# dom_m N ⟹ learned_clss_l (fmdrop C N) = (if ¬irred N C then remove1_mset (the (fmlookup N C)) (learned_clss_l N)
    else learned_clss_l N)›
  by (auto simp: learned_clss_l_l_fmdrop learned_clss_l_l_fmdrop_irrelev)

lemma learned_clss_l_fmupd_if:
  ‹C' ∉# dom_m new ⟹ learned_clss_l (fmupd C' D new) = (if ¬snd D then add_mset D (learned_clss_l new) else learned_clss_l new)›
  by (cases D) (auto simp: learned_clss_l_mapsto_upd_notin_irrelev
    learned_clss_l_mapsto_upd_notin)



definition op_clauses_at :: ‹'v clauses_l ⇒ nat ⇒ nat ⇒ 'v literal› where
‹op_clauses_at N C i = N ∝ C ! i›

definition mop_clauses_at :: ‹'v clauses_l ⇒ nat ⇒ nat ⇒ 'v literal nres› where
‹mop_clauses_at N C i = do {
   ASSERT(C ∈# dom_m N);
   ASSERT(i < length (N ∝ C));
   RETURN (N ∝ C ! i)
}›

lemma mop_clauses_at:
   ‹(uncurry2 mop_clauses_at, uncurry2 (RETURN ooo op_clauses_at)) ∈
   [λ((N, C), i). C ∈# dom_m N ∧ i < length (N ∝ C)]⇩f
   Id ×⇩f Id ×⇩f Id → ⟨Id⟩nres_rel›
  by (auto simp: mop_clauses_at_def op_clauses_at_def intro!: frefI nres_relI)

definition mop_clauses_swap :: ‹'v clauses_l ⇒ nat ⇒ nat ⇒ nat ⇒ 'v clauses_l nres› where
‹mop_clauses_swap N C i j = do {
   ASSERT(C ∈# dom_m N);
   ASSERT(i < length (N ∝ C));
   ASSERT(j < length (N ∝ C));
   RETURN (N(C ↪ (swap (N ∝ C) i j)))
}›

definition op_clauses_swap :: ‹'v clauses_l ⇒ nat ⇒ nat ⇒ nat ⇒ 'v clauses_l› where
‹op_clauses_swap N C i j = (N(C ↪ (swap (N ∝ C) i j)))›

lemma mop_clauses_swap:
   ‹(uncurry3 mop_clauses_swap, uncurry3 (RETURN oooo op_clauses_swap)) ∈
   [λ(((N, C), i), j). C ∈# dom_m N ∧ i < length (N ∝ C) ∧ j < length (N ∝ C)]⇩f
   Id ×⇩f Id ×⇩f Id ×⇩f Id → ⟨Id⟩nres_rel›
  by (auto simp: mop_clauses_swap_def op_clauses_swap_def intro!: frefI nres_relI)


lemma mop_clauses_at_itself:
  ‹(uncurry2 mop_clauses_at, uncurry2 mop_clauses_at) ∈ Id ×⇩f Id ×⇩f Id →⇩f ⟨Id⟩nres_rel›
  by (auto intro!: frefI nres_relI)

lemma mop_clauses_at_itself_spec:
  ‹((N, C, i), (N', C', i')) ∈ Id ⟹
     mop_clauses_at N C i ≤ ⇓ {(L, L'). L = L' ∧ L = N ∝ C ! i} (mop_clauses_at N' C' i')›
  by (auto intro!: frefI nres_relI ASSERT_refine_right simp: mop_clauses_at_def)

lemma mop_clauses_at_itself_spec2:
  ‹((N, C, i), (N', C', i')) ∈ Id ⟹
     mop_clauses_at N C i ≤ ⇓ {(L, L'). L = L' ∧ L = N ∝ C ! i ∧ C ∈# dom_m N ∧ i < length (N ∝ C)}
      (mop_clauses_at N' C' i')›
  by (auto intro!: frefI nres_relI ASSERT_refine_right simp: mop_clauses_at_def)

lemma mop_clauses_at_op_clauses_at_spec2:
  ‹((N, C, i), (N', C', i')) ∈ Id ⟹ C ∈# dom_m N ∧ i < length (N ∝ C) ⟹
     mop_clauses_at N C i ≤ ⇓ {(L, L'). L = L' ∧ L = N ∝ C ! i}
      (RETURN (op_clauses_at N' C' i'))›
  by (auto intro!: frefI nres_relI ASSERT_refine_right
   simp: mop_clauses_at_def op_clauses_at_def)

lemma mop_clauses_swap_itself:
  ‹(uncurry3 mop_clauses_swap, uncurry3 mop_clauses_swap) ∈ Id ×⇩f Id ×⇩f Id ×⇩f Id →⇩f ⟨Id⟩nres_rel›
  by (auto intro!: frefI nres_relI)

lemma mop_clauses_swap_itself_spec:
  ‹((N, C, i, j), (N', C', i', j')) ∈ Id ⟹
     mop_clauses_swap N C i j ≤ ⇓ {(L, L'). L = L' ∧ L = op_clauses_swap N' C' i' j' ∧ C' ∈# dom_m N} (mop_clauses_swap N' C' i' j')›
  by (auto intro!: frefI nres_relI ASSERT_refine_right simp: mop_clauses_swap_def
    op_clauses_swap_def)

lemma mop_clauses_swap_itself_spec2:
  ‹((N, C, i, j), (N', C', i', j')) ∈ Id ⟹
     mop_clauses_swap N C i j ≤ ⇓ {(L, L'). L = L' ∧ L = op_clauses_swap N' C' i' j' ∧ C' ∈# dom_m N ∧
       i < length (N ∝ C) ∧ j < length (N ∝ C)} (mop_clauses_swap N' C' i' j')›
  by (auto intro!: frefI nres_relI ASSERT_refine_right simp: mop_clauses_swap_def
    op_clauses_swap_def)


end