Theory CDCL_WNOT_Measure

chapter ‹NOT's CDCL and DPLL›

theory CDCL_WNOT_Measure
imports Weidenbach_Book_Base.WB_List_More
begin

text ‹The organisation of the development is the following:
  ▪ @{file CDCL_WNOT_Measure.thy} contains the measure used to show the termination the core of
  CDCL.
  ▪ @{file CDCL_NOT.thy} contains the specification of the rules: the rules are
  defined, and we proof the correctness and termination for some strategies CDCL.
  ▪ @{file DPLL_NOT.thy} contains the DPLL calculus based on the CDCL version.
  ▪ @{file DPLL_W.thy} contains Weidenbach's version of DPLL and the proof of equivalence between
  the two DPLL versions.
›

section ‹Measure›
text ‹This measure show the termination of the core of CDCL: each step improves the number of
  literals we know for sure.

  This measure can also be seen as the increasing lexicographic order: it is an order on bounded
  sequences, when each element is bounded. The proof involves a measure like the one defined here
  (the same?).›
definition μ⇩C :: "nat ⇒ nat ⇒ nat list ⇒ nat" where
"μ⇩C s b M ≡ (∑i=0..<length M. M!i * b^ (s +i - length M))"

lemma μ⇩C_Nil[simp]:
  "μ⇩C s b [] = 0"
  unfolding μ⇩C_def by auto

lemma μ⇩C_single[simp]:
  "μ⇩C s b [L] = L * b ^ (s - Suc 0)"
  unfolding μ⇩C_def by auto

lemma set_sum_atLeastLessThan_add:
  "(∑i=k..<k+(b::nat). f i) = (∑i=0..<b. f (k+ i))"
  by (induction b) auto

lemma set_sum_atLeastLessThan_Suc:
  "(∑i=1..<Suc j. f i) = (∑i=0..<j. f (Suc i))"
  using set_sum_atLeastLessThan_add[of _ 1 j] by force

lemma μ⇩C_cons:
  "μ⇩C s b (L # M) = L * b ^ (s - 1 - length M) + μ⇩C s b M"
proof -
  have "μ⇩C s b (L # M) = (∑i=0..<length (L#M). (L#M)!i * b^ (s +i - length (L#M)))"
    unfolding μ⇩C_def by blast
  also have "… = (∑i=0..<1. (L#M)!i * b^ (s +i - length (L#M)))
                 + (∑i=1..<length (L#M). (L#M)!i * b^ (s +i - length (L#M)))"
     by (rule sum.atLeastLessThan_concat[symmetric]) simp_all
  finally have "μ⇩C s b (L # M)= L * b ^ (s - 1 - length M)
                  + (∑i=1..<length (L#M). (L#M)!i * b^ (s +i - length (L#M)))"
     by auto
  moreover {
    have "(∑i=1..<length (L#M). (L#M)!i * b^ (s +i - length (L#M))) =
           (∑i=0..<length M. (L#M)!(Suc i) * b^ (s + (Suc i) - length (L#M)))"
     unfolding length_Cons set_sum_atLeastLessThan_Suc by blast
    also have "… = (∑i=0..<length M. M!i * b^ (s + i - length M))"
      by auto
    finally have "(∑i=1..<length (L#M). (L#M)!i * b^ (s +i - length (L#M))) = μ⇩C s b M"
      unfolding μ⇩C_def .
    }
  ultimately show ?thesis by presburger
qed

lemma μ⇩C_append:
  assumes "s ≥ length (M@M')"
  shows "μ⇩C s b (M@M') = μ⇩C (s - length M') b M + μ⇩C s b M'"
proof -
  have "μ⇩C s b (M@M') = (∑i=0..<length (M@M'). (M@M')!i * b^ (s +i - length (M@M')))"
    unfolding μ⇩C_def by blast
  moreover then have "… = (∑i=0..< length M. (M@M')!i * b^ (s +i - length (M@M')))
                 + (∑i=length M..<length (M@M'). (M@M')!i * b^ (s +i - length (M@M')))"
    by (auto intro!: sum.atLeastLessThan_concat[symmetric])
  moreover
    have "∀i∈{0..< length M}. (M@M')!i * b^ (s +i - length (M@M')) = M ! i * b ^ (s - length M'
      + i - length M)"
      using ‹s ≥ length (M@M')› by (auto simp add: nth_append ac_simps)
    then have "μ⇩C (s - length M') b M = (∑i=0..< length M. (M@M')!i * b^ (s +i - length (M@M')))"
      unfolding μ⇩C_def by auto
  ultimately have "μ⇩C s b (M@M')= μ⇩C (s - length M') b M
                  + (∑i=length M..<length (M@M'). (M@M')!i * b^ (s +i - length (M@M')))"
     by auto
  moreover {
    have "(∑i=length M..<length (M@M'). (M@M')!i * b^ (s +i - length (M@M'))) =
           (∑i=0..<length M'. M'!i * b^ (s + i - length M'))"
     unfolding length_append set_sum_atLeastLessThan_add by auto
    then have "(∑i=length M..<length (M@M'). (M@M')!i * b^ (s +i - length (M@M'))) = μ⇩C s b M'"
      unfolding μ⇩C_def .
    }
  ultimately show ?thesis by presburger
qed

lemma μ⇩C_cons_non_empty_inf:
  assumes M_ge_1: "∀i∈set M. i ≥ 1" and M: "M ≠ []"
  shows "μ⇩C s b M ≥ b ^ (s - length M)"
  using assms by (cases M) (auto simp: mult_eq_if μ⇩C_cons)

text ‹Copy of @{file "~~/src/HOL/ex/NatSum.thy"} (but generalized to @{term "k≥(0::nat)"})›
lemma sum_of_powers: "0 ≤ k ⟹ (k - 1) * (∑i=0..<n. k^i) = k^n - (1::nat)"
  apply (cases "k = 0")
    apply (cases n; simp)
  by (induct n) (auto simp: Nat.nat_distrib)

text ‹In the degenerated cases, we only have the large inequality holds. In the other cases, the
  following strict inequality holds:›
lemma μ⇩C_bounded_non_degenerated:
  fixes b ::nat
  assumes
    "b > 0" and
    "M ≠ []" and
    M_le: "∀i < length M. M!i < b" and
    "s ≥ length M"
  shows "μ⇩C s b M < b^s"
proof -
  consider (b1) "b= 1" | (b) "b>1" using ‹b>0› by (cases b) auto
  then show ?thesis
    proof cases
      case b1
      then have "∀i < length M. M!i = 0" using M_le by auto
      then have "μ⇩C s b M = 0" unfolding μ⇩C_def by auto
      then show ?thesis using ‹b > 0› by auto
    next
      case b
      have "∀ i ∈ {0..<length M}. M!i * b^ (s +i - length M) ≤ (b-1) * b^ (s +i - length M)"
        using M_le ‹b > 1› by auto
      then have "μ⇩C s b M ≤ (∑i=0..<length M. (b-1) * b^ (s +i - length M))"
         using ‹M≠[]› ‹b>0› unfolding μ⇩C_def by (auto intro: sum_mono)
      also
        have "∀ i ∈ {0..<length M}. (b-1) * b^ (s +i - length M) = (b-1) * b^ i * b^(s - length M)"
          by (metis Nat.add_diff_assoc2 add.commute assms(4) mult.assoc power_add)
        then have "(∑i=0..<length M. (b-1) * b^ (s +i - length M))
          = (∑i=0..<length M. (b-1)* b^ i * b^(s - length M))"
          by (auto simp add: ac_simps)
      also have "… = (∑i=0..<length M. b^ i) * b^(s - length M) * (b-1)"
         by (simp add: sum_distrib_right sum_distrib_left ac_simps)
      finally have "μ⇩C s b M ≤ (∑i=0..<length M. b^ i) * (b-1) * b^(s - length M)"
        by (simp add: ac_simps)

      also
        have "(∑i=0..<length M. b^ i)* (b-1) = b ^ (length M) - 1"
          using sum_of_powers[of b "length M"] ‹b>1›
          by (auto simp add: ac_simps)
      finally have "μ⇩C s b M ≤ (b ^ (length M) - 1) * b ^ (s - length M)"
        by auto
      also have "… < b ^ (length M) * b ^ (s - length M)"
        using ‹b>1› by auto
      also have "… = b ^ s"
        by (metis assms(4) le_add_diff_inverse power_add)
      finally show ?thesis unfolding μ⇩C_def by (auto simp add: ac_simps)
    qed
qed

text ‹In the degenerate case @{term "b=0"}, the list @{term M} is empty (since the list cannot
  contain any element).›
lemma μ⇩C_bounded:
  fixes b :: nat
  assumes
    M_le: "∀i < length M. M!i < b" and
    "s ≥ length M"
    "b > 0"
  shows "μ⇩C s b M < b ^ s"
proof -
  consider (M0) "M = []" | (M) "b > 0" and "M ≠ []"
    using M_le by (cases b, cases M) auto
  then show ?thesis
    proof cases
      case M0
      then show ?thesis using M_le ‹b > 0› by auto
    next
      case M
      show ?thesis using μ⇩C_bounded_non_degenerated[OF M assms(1,2)] by arith
    qed
qed

text ‹When @{term "b=(0::nat)"}, we cannot show that the measure is empty, since @{term "0^0 =
  (1::nat)"}.›
lemma μ⇩C_base_0:
  assumes "length M ≤ s"
  shows "μ⇩C s 0 M ≤ M!0"
proof -
  {
    assume "s = length M"
    moreover {
      fix n
      have "(∑i=0..<n. M ! i * (0::nat) ^ i) ≤ M ! 0"
        apply (induction n rule: nat_induct)
        by simp (rename_tac n, case_tac n, auto)
    }
    ultimately have ?thesis unfolding μ⇩C_def by auto
  }
  moreover
  {
    assume "length M < s"
    then have "μ⇩C s 0 M = 0" unfolding μ⇩C_def by auto}
  ultimately show ?thesis using assms unfolding μ⇩C_def by linarith
qed

lemma finite_bounded_pair_list:
  fixes b :: nat
  shows "finite {(ys, xs). length xs < s ∧ length ys < s ∧
    (∀i< length xs. xs ! i < b) ∧ (∀i< length ys. ys ! i < b)}"
proof -
  have H: "{(ys, xs). length xs < s ∧ length ys < s ∧
    (∀i< length xs. xs ! i < b) ∧ (∀i< length ys. ys ! i < b)}
    ⊆
    {xs. length xs < s ∧ (∀i< length xs. xs ! i < b)} ×
    {xs. length xs < s ∧ (∀i< length xs. xs ! i < b)}"
    by auto
  moreover have "finite {xs. length xs < s ∧ (∀i< length xs. xs ! i < b)}"
    by (rule finite_bounded_list)
  ultimately show ?thesis by (auto simp: finite_subset)
qed

definition νNOT :: "nat ⇒ nat ⇒ (nat list × nat list) set" where
"νNOT s base = {(ys, xs). length xs < s ∧ length ys < s ∧
  (∀i< length xs. xs ! i < base) ∧ (∀i< length ys. ys ! i < base) ∧
  (ys, xs) ∈ lenlex less_than}"

lemma finite_νNOT[simp]:
  "finite (νNOT s base)"
proof -
  have "νNOT s base ⊆ {(ys, xs). length xs < s ∧ length ys < s ∧
    (∀i< length xs. xs ! i < base) ∧ (∀i< length ys. ys ! i < base)}"
    by (auto simp: νNOT_def)
  moreover have "finite {(ys, xs). length xs < s ∧ length ys < s ∧
    (∀i< length xs. xs ! i < base) ∧ (∀i< length ys. ys ! i < base)}"
      by (rule finite_bounded_pair_list)
  ultimately show ?thesis by (auto simp: finite_subset)
qed

lemma acyclic_νNOT: "acyclic (νNOT s base)"
  apply (rule acyclic_subset[of "lenlex less_than" "νNOT s base"])
    apply (rule wf_acyclic)
  by (auto simp: νNOT_def)

lemma wf_νNOT: "wf (νNOT s base)"
  by (rule finite_acyclic_wf) (auto simp: acyclic_νNOT)

end