Theory CDCL.CDCL_W_Level

theory CDCL_W_Level
imports
  Entailment_Definition.Partial_Annotated_Herbrand_Interpretation
begin


subsubsection ‹Level of literals and clauses›
text ‹Getting the level of a variable, implies that the list has to be reversed. Here is the
  function ∗‹after› reversing.›

definition count_decided :: "('v, 'b, 'm) annotated_lit list ⇒ nat" where
"count_decided l = length (filter is_decided l)"

definition get_level :: "('v, 'm) ann_lits ⇒ 'v literal ⇒ nat" where
"get_level S L = length (filter is_decided (dropWhile (λS. atm_of (lit_of S) ≠ atm_of L) S))"

lemma get_level_uminus[simp]: ‹get_level M (-L) = get_level M L›
  by (auto simp: get_level_def)

lemma get_level_Neg_Pos: ‹get_level M (Neg L) = get_level M (Pos L)›
  unfolding get_level_def by auto

lemma count_decided_0_iff:
  ‹count_decided M = 0 ⟷ (∀L ∈ set M. ¬is_decided L)›
  by (auto simp: count_decided_def filter_empty_conv)

lemma
  shows
    count_decided_nil[simp]: ‹count_decided [] = 0› and
    count_decided_cons[simp]:
      ‹count_decided (a # M) = (if is_decided a then Suc (count_decided M) else count_decided M)› and
    count_decided_append[simp]:
      ‹count_decided (M @ M') = count_decided M + count_decided M'›
  by (auto simp: count_decided_def)

lemma atm_of_notin_get_level_eq_0[simp]:
  assumes "undefined_lit M L"
  shows "get_level M L = 0"
  using assms by (induct M rule: ann_lit_list_induct) (auto simp: get_level_def defined_lit_map)

lemma get_level_ge_0_atm_of_in:
  assumes "get_level M L > n"
  shows "atm_of L ∈ atm_of ` lits_of_l M"
  using atm_of_notin_get_level_eq_0[of M L] assms unfolding defined_lit_map
  by (auto simp: lits_of_def simp del: atm_of_notin_get_level_eq_0)

text ‹In @{const get_level} (resp. @{const get_level}), the beginning (resp. the end) can be
  skipped if the literal is not in the beginning (resp. the end).›
lemma get_level_skip[simp]:
  assumes "undefined_lit M L"
  shows "get_level (M @ M') L = get_level M' L"
  using assms by (induct M rule: ann_lit_list_induct) (auto simp: get_level_def defined_lit_map)

text ‹If the literal is at the beginning, then the end can be skipped›
lemma get_level_skip_end[simp]:
  assumes "defined_lit M L"
  shows "get_level (M @ M') L = get_level M L + count_decided M'"
  using assms by (induct M' rule: ann_lit_list_induct)
    (auto simp: lits_of_def get_level_def count_decided_def defined_lit_map)

lemma get_level_skip_beginning[simp]:
  assumes "atm_of L' ≠ atm_of (lit_of K)"
  shows "get_level (K # M) L' = get_level M L'"
  using assms by (auto simp: get_level_def)

lemma get_level_take_beginning[simp]:
  assumes "atm_of L' = atm_of (lit_of K)"
  shows "get_level (K # M) L' = count_decided (K # M)"
  using assms by (auto simp: get_level_def count_decided_def)

lemma get_level_cons_if:
  ‹get_level (K # M) L' =
    (if atm_of L' = atm_of (lit_of K) then count_decided (K # M) else get_level M L')›
  by auto

lemma get_level_skip_beginning_not_decided[simp]:
  assumes "undefined_lit S L"
  and "∀s∈set S. ¬is_decided s"
  shows "get_level (M @ S) L = get_level M L"
  using assms apply (induction S rule: ann_lit_list_induct)
    apply auto[2]
  apply (case_tac "atm_of L ∈ atm_of ` lits_of_l M")
   apply (auto simp: image_iff lits_of_def filter_empty_conv count_decided_def defined_lit_map
      dest: set_dropWhileD)
  done

lemma get_level_skip_all_not_decided[simp]:
  fixes M
  assumes "∀m∈set M. ¬ is_decided m"
  shows "get_level M L = 0"
  using assms by (auto simp: filter_empty_conv get_level_def dest: set_dropWhileD)

text ‹the @{term "{#0#}"} is there to ensures that the set is not empty.›
definition get_maximum_level :: "('a, 'b) ann_lits ⇒ 'a clause ⇒ nat"
  where
"get_maximum_level M D = Max_mset ({#0#} + image_mset (get_level M) D)"

lemma get_maximum_level_ge_get_level:
  "L ∈# D ⟹ get_maximum_level M D ≥ get_level M L"
  unfolding get_maximum_level_def by auto

lemma get_maximum_level_empty[simp]:
  "get_maximum_level M {#} = 0"
  unfolding get_maximum_level_def by auto

lemma get_maximum_level_exists_lit_of_max_level:
  "D ≠ {#} ⟹ ∃L∈# D. get_level M L = get_maximum_level M D"
  unfolding get_maximum_level_def
  apply (induct D)
   apply simp
  by (rename_tac x D, case_tac "D = {#}") (auto simp add: max_def)

lemma get_maximum_level_empty_list[simp]:
  "get_maximum_level [] D = 0"
  unfolding get_maximum_level_def by (simp add: image_constant_conv)

lemma get_maximum_level_add_mset:
  "get_maximum_level M (add_mset L D) = max (get_level M L) (get_maximum_level M D)"
  unfolding get_maximum_level_def by simp

lemma get_level_append_if:
  ‹get_level (M @ M') L = (if defined_lit M L then get_level M L + count_decided M'
            else get_level M' L)›
  by (auto)

text ‹Do mot activate as [simp] rules. It breaks everything.›
lemma get_maximum_level_single:
  ‹get_maximum_level M {#x#} = get_level M x›
  by (auto simp: get_maximum_level_add_mset)

lemma get_maximum_level_plus:
  "get_maximum_level M (D + D') = max (get_maximum_level M D) (get_maximum_level M D')"
  by (induction D) (simp_all add: get_maximum_level_add_mset)

lemma get_maximum_level_cong:
  assumes ‹∀L ∈# D. get_level M L = get_level M' L›
  shows ‹get_maximum_level M D = get_maximum_level M' D›
  using assms by (induction D) (auto simp: get_maximum_level_add_mset)

lemma get_maximum_level_exists_lit:
  assumes n: "n > 0"
  and max: "get_maximum_level M D = n"
  shows "∃L ∈#D. get_level M L = n"
proof -
  have f: "finite (insert 0 ((λL. get_level M L) ` set_mset D))" by auto
  then have "n ∈ ((λL. get_level M L) ` set_mset D)"
    using n max Max_in[OF f] unfolding get_maximum_level_def by simp
  then show "∃L ∈# D. get_level M L = n" by auto
qed

lemma get_maximum_level_skip_first[simp]:
  assumes "atm_of (lit_of K) ∉ atms_of D"
  shows "get_maximum_level (K # M) D = get_maximum_level M D"
  using assms unfolding get_maximum_level_def atms_of_def
    atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set
  by (smt atm_of_in_atm_of_set_in_uminus get_level_skip_beginning image_iff lit_of.simps(2)
      multiset.map_cong0)

lemma get_maximum_level_skip_beginning:
  assumes DH: "∀x ∈# D. undefined_lit c x"
  shows "get_maximum_level (c @ H) D = get_maximum_level H D"
proof -
  have "(get_level (c @ H)) ` set_mset D = (get_level H) ` set_mset D"
    apply (rule image_cong)
     apply (simp; fail)
    using DH unfolding atms_of_def by auto
  then show ?thesis using DH unfolding get_maximum_level_def by auto
qed

lemma get_maximum_level_D_single_propagated:
  "get_maximum_level [Propagated x21 x22] D = 0"
  unfolding get_maximum_level_def by (simp add: image_constant_conv)

lemma get_maximum_level_union_mset:
  "get_maximum_level M (A ∪# B) = get_maximum_level M (A + B)"
  unfolding get_maximum_level_def by (auto simp: image_Un)

lemma count_decided_rev[simp]:
  "count_decided (rev M) = count_decided M"
  by (auto simp: count_decided_def rev_filter[symmetric])

lemma count_decided_ge_get_level:
  "count_decided M ≥ get_level M L"
  by (induct M rule: ann_lit_list_induct)
    (auto simp add: count_decided_def le_max_iff_disj get_level_def)

lemma count_decided_ge_get_maximum_level:
  "count_decided M ≥ get_maximum_level M D"
  using get_maximum_level_exists_lit_of_max_level unfolding Bex_def
  by (metis get_maximum_level_empty count_decided_ge_get_level le0)

lemma get_level_last_decided_ge:
   ‹defined_lit (c @ [Decided K]) L' ⟹ 0 < get_level (c @ [Decided K]) L'›
  by (induction c) (auto simp: defined_lit_cons get_level_cons_if)

lemma get_maximum_level_mono:
  ‹D ⊆# D' ⟹ get_maximum_level M D ≤ get_maximum_level M D'›
  unfolding get_maximum_level_def by auto

fun get_all_mark_of_propagated where
"get_all_mark_of_propagated [] = []" |
"get_all_mark_of_propagated (Decided _ # L) = get_all_mark_of_propagated L" |
"get_all_mark_of_propagated (Propagated _ mark # L) = mark # get_all_mark_of_propagated L"

lemma get_all_mark_of_propagated_append[simp]:
  "get_all_mark_of_propagated (A @ B) = get_all_mark_of_propagated A @ get_all_mark_of_propagated B"
  by (induct A rule: ann_lit_list_induct) auto

lemma get_all_mark_of_propagated_tl_proped:
  ‹M ≠ [] ⟹ is_proped (hd M) ⟹ get_all_mark_of_propagated (tl M) = tl (get_all_mark_of_propagated M)›
  by (induction M rule: ann_lit_list_induct) auto


subsubsection ‹Properties about the levels›

lemma atm_lit_of_set_lits_of_l:
  "(λl. atm_of (lit_of l)) ` set xs = atm_of ` lits_of_l xs"
  unfolding lits_of_def by auto

text ‹Before I try yet another time to prove that I can remove the assumption \<^term>‹no_dup M›:
  It does not work. The problem is that \<^term>‹get_level M K = Suc i› peaks the first occurrence
  of the literal \<^term>‹K›. This is for example an issue for the trail \<^term>‹replicate n (Decided K)›.
  An explicit counter-example is below.
›
lemma le_count_decided_decomp:
  assumes ‹no_dup M›
  shows ‹i < count_decided M ⟷ (∃c K c'. M = c @ Decided K # c' ∧ get_level M K = Suc i)›
    (is "?A ⟷ ?B")
proof
  assume ?B
  then obtain c K c' where
    "M = c @ Decided K # c'" and "get_level M K = Suc i"
    by blast
  then show ?A using count_decided_ge_get_level[of M K] by auto
next
  assume ?A
  then show ?B
    using ‹no_dup M›
  proof (induction M rule: ann_lit_list_induct)
    case Nil
    then show ?case by simp
  next
    case (Decided L M) note IH = this(1) and i = this(2) and n_d = this(3)
    then have n_d_M: "no_dup M" by simp
    show ?case
    proof (cases "i < count_decided M")
      case True
      then obtain c K c' where
	M: "M = c @ Decided K # c'" and lev_K: "get_level M K = Suc i"
	using IH n_d_M by blast
      show ?thesis
	apply (rule exI[of _ "Decided L # c"])
	apply (rule exI[of _ K])
	apply (rule exI[of _ c'])
	using lev_K n_d unfolding M by (auto simp: get_level_def defined_lit_map)
    next
      case False
      show ?thesis
	apply (rule exI[of _ "[]"])
	apply (rule exI[of _ L])
	apply (rule exI[of _ M])
	using False i by (auto simp: get_level_def count_decided_def)
    qed
    next
      case (Propagated L mark' M) note i = this(2) and IH = this(1) and n_d = this(3)
      then obtain c K c' where
	M: "M = c @ Decided K # c'" and lev_K: "get_level M K = Suc i"
	by (auto simp: count_decided_def)
      show ?case
	apply (rule exI[of _ "Propagated L mark' # c"])
	apply (rule exI[of _ "K"])
	apply (rule exI[of _ "c'"])
	using lev_K n_d unfolding M by (auto simp: atm_lit_of_set_lits_of_l get_level_def
	  defined_lit_map)
    qed
qed

text ‹The counter-example if the assumption \<^term>‹no_dup M›.›
lemma
  fixes K
  defines ‹M ≡ replicate 3 (Decided K)›
  defines ‹i ≡ 1›
  assumes ‹i < count_decided M ⟷ (∃c K c'. M = c @ Decided K # c' ∧ get_level M K = Suc i)›
  shows False
  using assms(3-) unfolding M_def i_def numeral_3_eq_3
  by (auto simp: Cons_eq_append_conv)

lemma Suc_count_decided_gt_get_level:
  ‹get_level M L < Suc (count_decided M)›
  by (induction M rule: ann_lit_list_induct) (auto simp: get_level_cons_if)

lemma get_level_neq_Suc_count_decided[simp]:
  ‹get_level M L ≠ Suc (count_decided M)›
  using Suc_count_decided_gt_get_level[of M L] by auto

lemma length_get_all_ann_decomposition: ‹length (get_all_ann_decomposition M) = 1+count_decided M›
  by (induction M rule: ann_lit_list_induct) auto

lemma get_maximum_level_remove_non_max_lvl:
   ‹get_level M a < get_maximum_level M D ⟹
  get_maximum_level M (remove1_mset a D) = get_maximum_level M D›
  by (cases ‹a ∈# D›)
    (auto dest!: multi_member_split simp: get_maximum_level_add_mset)

lemma exists_lit_max_level_in_negate_ann_lits:
  ‹negate_ann_lits M ≠ {#} ⟹ ∃L∈#negate_ann_lits M. get_level M L = count_decided M›
  by (cases ‹M›) (auto simp: negate_ann_lits_def)
lemma get_maximum_level_eq_count_decided_iff:
  ‹ya ≠ {#} ⟹ get_maximum_level xa ya = count_decided xa ⟷ (∃L ∈# ya. get_level xa L = count_decided xa)›
  apply (rule iffI)
  defer
  subgoal
    using count_decided_ge_get_maximum_level[of xa]
    apply (auto dest!: multi_member_split dest: le_antisym simp: get_maximum_level_add_mset max_def)
    using le_antisym by blast
  subgoal
    using get_maximum_level_exists_lit_of_max_level[of ya xa]
    by auto
  done

definition card_max_lvl where
  ‹card_max_lvl M C ≡ size (filter_mset (λL. get_level M L = count_decided M) C)›

lemma card_max_lvl_add_mset: ‹card_max_lvl M (add_mset L C) =
  (if get_level M L = count_decided M then 1 else 0) +
    card_max_lvl M C›
  by (auto simp: card_max_lvl_def)

lemma card_max_lvl_empty[simp]: ‹card_max_lvl M {#} = 0›
  by (auto simp: card_max_lvl_def)

lemma card_max_lvl_all_poss:
   ‹card_max_lvl M C = card_max_lvl M (poss (atm_of `# C))›
  unfolding card_max_lvl_def
  apply (induction C)
  subgoal by auto
  subgoal for L C
    using get_level_uminus[of M L]
    by (cases L) (auto)
  done

lemma card_max_lvl_distinct_cong:
  assumes
    ‹⋀L. get_level M (Pos L) = count_decided M ⟹ (L ∈ atms_of C) ⟹ (L ∈ atms_of C')› and
    ‹⋀L. get_level M (Pos L) = count_decided M ⟹ (L ∈ atms_of C') ⟹ (L ∈ atms_of C)› and
    ‹distinct_mset C› ‹¬tautology C› and
    ‹distinct_mset C'› ‹¬tautology C'›
  shows ‹card_max_lvl M C = card_max_lvl M C'›
proof -
  have [simp]: ‹NO_MATCH (Pos x) L ⟹ get_level M L = get_level M (Pos (atm_of L))› for x L
    by (simp add: get_level_def)
  have [simp]: ‹atm_of L ∉ atms_of C' ⟷ L ∉# C' ∧ -L ∉# C'› for L C'
    by (cases L) (auto simp: atm_iff_pos_or_neg_lit)
  then have [iff]: ‹atm_of L ∈ atms_of C' ⟷ L ∈# C' ∨ -L ∈# C'› for L C'
    by blast
  have H: ‹distinct_mset {#L ∈# poss (atm_of `# C). get_level M L = count_decided M#}›
    if ‹distinct_mset C› ‹¬tautology C› for C
    using that by (induction C) (auto simp: tautology_add_mset atm_of_eq_atm_of)
  show ?thesis
    apply (subst card_max_lvl_all_poss)
    apply (subst (2) card_max_lvl_all_poss)
    unfolding card_max_lvl_def
    apply (rule arg_cong[of _ _ size])
    apply (rule distinct_set_mset_eq)
    subgoal by (rule H) (use assms in fast)+
    subgoal by (rule H) (use assms in fast)+
    subgoal using assms by (auto simp: atms_of_def imageI image_iff) blast+
    done
qed

lemma get_maximum_level_card_max_lvl_ge1:
  ‹count_decided xa > 0 ⟹ get_maximum_level xa ya = count_decided xa ⟷ card_max_lvl xa ya > 0›
  apply (cases ‹ya = {#}›)
  subgoal by auto
  subgoal
    by (auto simp: card_max_lvl_def get_maximum_level_eq_count_decided_iff dest: multi_member_split
      dest!: multi_nonempty_split[of ‹filter_mset _ _›] filter_mset_eq_add_msetD
      simp flip: nonempty_has_size)
  done

lemma card_max_lvl_remove_hd_trail_iff:
  ‹xa ≠ [] ⟹ - lit_of (hd xa) ∈# ya ⟹ 0 < card_max_lvl xa (remove1_mset (- lit_of (hd xa)) ya) ⟷ Suc 0 < card_max_lvl xa ya›
  by (cases xa)
    (auto dest!: multi_member_split simp: card_max_lvl_add_mset)

lemma card_max_lvl_Cons:
  assumes ‹no_dup (L # a)› ‹distinct_mset y›‹¬tautology y› ‹¬is_decided L›
  shows ‹card_max_lvl (L # a) y =
    (if (lit_of L ∈# y ∨ -lit_of L ∈# y) ∧ count_decided a ≠ 0 then card_max_lvl a y + 1
    else card_max_lvl a y)›
proof -
  have [simp]: ‹count_decided a = 0 ⟹ get_level a L = 0› for L
    by (simp add: count_decided_0_iff)
  have [simp]: ‹lit_of L ∉# A ⟹
         - lit_of L ∉# A ⟹
          {#La ∈# A. La ≠ lit_of L ∧ La ≠ - lit_of L ⟶ get_level a La = b#} =
          {#La ∈# A. get_level a La = b#}› for A b
    apply (rule filter_mset_cong)
     apply (rule refl)
    by auto
  show ?thesis
    using assms by (auto simp: card_max_lvl_def get_level_cons_if tautology_add_mset
        atm_of_eq_atm_of
        dest!: multi_member_split)
qed

lemma card_max_lvl_tl:
  assumes ‹a ≠ []› ‹distinct_mset y›‹¬tautology y› ‹¬is_decided (hd a)› ‹no_dup a›
   ‹count_decided a ≠ 0›
  shows ‹card_max_lvl (tl a) y =
      (if (lit_of(hd a) ∈# y ∨ -lit_of(hd a) ∈# y)
        then card_max_lvl a y - 1 else card_max_lvl a y)›
  using assms by (cases a) (auto simp: card_max_lvl_Cons)

end