Theory DPLL_W_Partial_Encoding

theory DPLL_W_Partial_Encoding
imports
  DPLL_W_Optimal_Model
  CDCL_W_Partial_Encoding
begin

context optimal_encoding_ops
begin

text ‹

We use the following list to generate an upper bound of the derived
trails by ODPLL: using lists makes it possible to use recursion. Using
text‹inductive_set› does not work, because it is not possible to
recurse on the arguments of a predicate.


The idea is similar to an earlier definition of term‹simple_clss›,
although in that case, we went for recursion over the set of literals
directly, via a choice in the recursive call.

›
definition list_new_vars :: ‹'v list› where
‹list_new_vars = (SOME v. set v = ΔΣ ∧ distinct v)›

lemma
  set_list_new_vars: ‹set list_new_vars = ΔΣ› and
  distinct_list_new_vars: ‹distinct list_new_vars› and
  length_list_new_vars: ‹length list_new_vars = card ΔΣ›
  using someI[of ‹λv. set v = ΔΣ ∧ distinct v›]
  unfolding list_new_vars_def[symmetric]
  using finite_Σ finite_distinct_list apply blast
  using someI[of ‹λv. set v = ΔΣ ∧ distinct v›]
  unfolding list_new_vars_def[symmetric]
  using finite_Σ finite_distinct_list apply blast
  using someI[of ‹λv. set v = ΔΣ ∧ distinct v›]
  unfolding list_new_vars_def[symmetric]
  by (metis distinct_card finite_Σ finite_distinct_list)

fun all_sound_trails where
  ‹all_sound_trails [] = simple_clss (Σ - ΔΣ)› |
  ‹all_sound_trails (L # M) =
     all_sound_trails M ∪ add_mset (Pos (replacement_pos L)) ` all_sound_trails M
      ∪ add_mset (Pos (replacement_neg L)) ` all_sound_trails M›

lemma all_sound_trails_atms:
  ‹set xs ⊆ ΔΣ ⟹
   C ∈ all_sound_trails xs ⟹
     atms_of C ⊆ Σ - ΔΣ ∪ replacement_pos ` set xs ∪ replacement_neg ` set xs›
  apply (induction xs arbitrary: C)
  subgoal by (auto simp: simple_clss_def)
  subgoal for x xs C
    apply (auto simp: tautology_add_mset)
    apply blast+
    done
  done

lemma all_sound_trails_distinct_mset:
  ‹set xs ⊆ ΔΣ ⟹ distinct xs ⟹
   C ∈ all_sound_trails xs ⟹
     distinct_mset C›
  using all_sound_trails_atms[of xs C]
  apply (induction xs arbitrary: C)
  subgoal by (auto simp: simple_clss_def)
  subgoal for x xs C
    apply clarsimp
    apply (auto simp: tautology_add_mset)
    apply (simp add: all_sound_trails_atms; fail)+
    apply (frule all_sound_trails_atms, assumption)
    apply (auto dest!: multi_member_split simp: subsetD)
    apply (simp add: all_sound_trails_atms; fail)+
    apply (frule all_sound_trails_atms, assumption)
    apply (auto dest!: multi_member_split simp: subsetD)
    apply (simp add: all_sound_trails_atms; fail)+
    done
  done

lemma all_sound_trails_tautology:
  ‹set xs ⊆ ΔΣ ⟹ distinct xs ⟹
   C ∈ all_sound_trails xs ⟹
     ¬tautology C›
  using all_sound_trails_atms[of xs C]
  apply (induction xs arbitrary: C)
  subgoal by (auto simp: simple_clss_def)
  subgoal for x xs C
    apply clarsimp
    apply (auto simp: tautology_add_mset)
    apply (simp add: all_sound_trails_atms; fail)+
    apply (frule all_sound_trails_atms, assumption)
    apply (auto dest!: multi_member_split simp: subsetD)
    apply (simp add: all_sound_trails_atms; fail)+
    apply (frule all_sound_trails_atms, assumption)
    apply (auto dest!: multi_member_split simp: subsetD)
    done
  done

lemma all_sound_trails_simple_clss:
  ‹set xs ⊆ ΔΣ ⟹ distinct xs ⟹
   all_sound_trails xs ⊆ simple_clss (Σ - ΔΣ ∪ replacement_pos ` set xs ∪ replacement_neg ` set xs)›
   using all_sound_trails_tautology[of xs]
     all_sound_trails_distinct_mset[of xs]
     all_sound_trails_atms[of xs]
   by (fastforce simp: simple_clss_def)

lemma in_all_sound_trails_inD:
  ‹set xs ⊆ ΔΣ ⟹ distinct xs ⟹ a ∈ ΔΣ ⟹
   add_mset (Pos (a↦0)) xa ∈ all_sound_trails xs ⟹ a ∈ set xs›
  using all_sound_trails_simple_clss[of xs]
  apply (auto simp: simple_clss_def)
  apply (rotate_tac 3)
  apply (frule set_mp, assumption)
  apply auto
  done

lemma in_all_sound_trails_inD':
  ‹set xs ⊆ ΔΣ ⟹ distinct xs ⟹ a ∈ ΔΣ ⟹
   add_mset (Pos (a↦1)) xa ∈ all_sound_trails xs ⟹ a ∈ set xs›
  using all_sound_trails_simple_clss[of xs]
  apply (auto simp: simple_clss_def)
  apply (rotate_tac 3)
  apply (frule set_mp, assumption)
  apply auto
  done

context
  assumes [simp]: ‹finite Σ›
begin

lemma all_sound_trails_finite[simp]:
  ‹finite (all_sound_trails xs)›
  by (induction xs)
    (auto intro!: simple_clss_finite finite_Σ)

lemma card_all_sound_trails:
  assumes ‹set xs ⊆ ΔΣ› and ‹distinct xs›
  shows ‹card (all_sound_trails xs) = card (simple_clss (Σ - ΔΣ)) * 3 ^ (length xs)›
  using assms
  apply (induction xs)
  apply auto
  apply (subst card_Un_disjoint)
  apply (auto simp: add_mset_eq_add_mset dest: in_all_sound_trails_inD)
  apply (subst card_Un_disjoint)
  apply (auto simp: add_mset_eq_add_mset dest: in_all_sound_trails_inD')
  apply (subst card_image)
  apply (auto simp: inj_on_def)
  apply (subst card_image)
  apply (auto simp: inj_on_def)
  done

end

lemma simple_clss_all_sound_trails: ‹simple_clss (Σ - ΔΣ) ⊆ all_sound_trails ys›
  apply (induction ys)
  apply auto
  done

lemma all_sound_trails_decomp_in:
  assumes
    ‹C ⊆ ΔΣ›  ‹C' ⊆ ΔΣ›  ‹C ∩ C' = {}› ‹C ∪ C' ⊆ set xs›
    ‹D ∈ simple_clss (Σ - ΔΣ)›
  shows
    ‹(Pos o replacement_pos) `# mset_set C + (Pos o replacement_neg) `# mset_set C' + D ∈ all_sound_trails xs›
  using assms
  apply (induction xs arbitrary: C C' D)
  subgoal
    using simple_clss_all_sound_trails[of ‹[]›]
    by auto
  subgoal premises p for a xs C C' D
    apply (cases ‹a ∈# mset_set C›)
    subgoal
      using p(1)[of ‹C - {a}› C' D] p(2-)
      finite_subset[OF p(3)]
      apply -
      apply (subgoal_tac ‹finite C ∧ C - {a} ⊆ ΔΣ ∧ C' ⊆ ΔΣ ∧ (C - {a}) ∩ C' = {} ∧ C - {a} ∪ C' ⊆ set xs›)
      defer
      apply (auto simp: disjoint_iff_not_equal finite_subset)[]
      apply (auto dest!: multi_member_split)
      by (simp add: mset_set.remove)
    apply (cases ‹a ∈# mset_set C'›)
    subgoal
      using p(1)[of C ‹C' - {a}› D] p(2-)
        finite_subset[OF p(3)]
      apply -
      apply (subgoal_tac ‹finite C ∧ C ⊆ ΔΣ ∧ C'- {a} ⊆ ΔΣ ∧ (C) ∩ (C'- {a}) = {} ∧ C ∪ C'- {a} ⊆ set xs ∧
         C ⊆ set xs ∧ C' - {a} ⊆ set xs›)
      defer
      apply (auto simp: disjoint_iff_not_equal finite_subset)[]
      apply (auto dest!: multi_member_split)
      by (simp add: mset_set.remove)
    subgoal
      using p(1)[of C C' D] p(2-)
        finite_subset[OF p(3)]
      apply -
      apply (subgoal_tac ‹finite C ∧ C ⊆ ΔΣ ∧ C' ⊆ ΔΣ ∧ (C) ∩ (C') = {} ∧ C ∪ C' ⊆ set xs ∧
         C ⊆ set xs ∧ C' ⊆ set xs›)
      defer
      apply (auto simp: disjoint_iff_not_equal finite_subset)[]
      by (auto dest!: multi_member_split)
    done
  done

lemma (in -)image_union_subset_decomp:
  ‹f ` (C) ⊆ A ∪ B ⟷ (∃A' B'. f ` A' ⊆ A ∧ f ` B' ⊆ B ∧ C = A' ∪ B' ∧ A' ∩ B' = {})›
  apply (rule iffI)
  apply (rule exI[of _ ‹{x ∈ C. f x ∈ A}›])
  apply (rule exI[of _ ‹{x ∈ C. f x ∈ B ∧ f x ∉ A}›])
  apply auto
  done

lemma in_all_sound_trails:
  assumes
    ‹⋀L. L ∈ ΔΣ ⟹ Neg (replacement_pos L) ∉# C›
    ‹⋀L. L ∈ ΔΣ ⟹ Neg (replacement_neg L) ∉# C›
    ‹⋀L. L ∈ ΔΣ ⟹ Pos (replacement_pos L) ∈# C ⟹ Pos (replacement_neg L) ∉# C›
    ‹C ∈ simple_clss (Σ - ΔΣ ∪ replacement_pos ` set xs ∪ replacement_neg ` set xs)› and
    xs: ‹set xs ⊆ ΔΣ›
  shows
    ‹C ∈ all_sound_trails xs›
proof -
  have
    atms: ‹atms_of C ⊆ (Σ - ΔΣ ∪ replacement_pos ` set xs ∪ replacement_neg ` set xs)› and
    taut: ‹¬tautology C› and
    dist: ‹distinct_mset C›
    using assms unfolding simple_clss_def
    by blast+

  obtain A' B' A'a B'' where
    A'a: ‹atm_of ` A'a ⊆ Σ - ΔΣ› and
    B'': ‹atm_of ` B'' ⊆ replacement_pos ` set xs› and
    ‹A' = A'a ∪ B''› and
    B': ‹atm_of ` B' ⊆ replacement_neg ` set xs› and
    C: ‹set_mset C = A'a ∪ B'' ∪ B'› and
    inter:
      ‹B'' ∩ B' = {}›
      ‹A'a ∩ B' = {}›
      ‹A'a ∩ B'' = {}›
    using atms unfolding atms_of_def
    apply (subst (asm)image_union_subset_decomp)
    apply (subst (asm)image_union_subset_decomp)
    by (auto simp: Int_Un_distrib2)

  have H: ‹f ` A ⊆ B ⟹ x ∈ A ⟹ f x ∈ B› for x A B f
    by auto
  have [simp]: ‹finite A'a› ‹finite B''› ‹finite B'›
    by (metis C finite_Un finite_set_mset)+
  obtain CB'' CB' where
    CB: ‹CB' ⊆ set xs› ‹CB'' ⊆ set xs› and
    decomp:
      ‹atm_of ` B'' = replacement_pos ` CB''›
      ‹atm_of ` B' = replacement_neg ` CB'›
    using B' B'' by (auto simp: subset_image_iff)
  have C: ‹C =mset_set B'' + mset_set B' + mset_set A'a›
    using inter
    apply (subst distinct_set_mset_eq_iff[symmetric, OF dist])
    apply (auto simp: C distinct_mset_mset_set simp flip: mset_set_Union)
    apply (subst mset_set_Union[symmetric])
    using inter
    apply auto
    done
  have B'': ‹B'' = (Pos) ` (atm_of ` B'')›
    using assms(1-3) B'' xs A'a B'' unfolding C
    apply (auto simp: )
    apply (frule H, assumption)
    apply (case_tac x)
    apply auto
    apply (rule_tac x = ‹replacement_pos A› in imageI)
    apply (auto simp add: rev_image_eqI)
    apply (frule H, assumption)
    apply (case_tac xb)
    apply auto
    done
  have B': ‹B' = (Pos) ` (atm_of ` B')›
    using assms(1-3) B' xs A'a B' unfolding C
    apply (auto simp: )
    apply (frule H, assumption)
    apply (case_tac x)
    apply auto
    apply (rule_tac x = ‹replacement_neg A› in imageI)
    apply (auto simp add: rev_image_eqI)
    apply (frule H, assumption)
    apply (case_tac xb)
    apply auto
    done

  have simple: ‹mset_set A'a ∈ simple_clss (Σ - ΔΣ)›
    using assms A'a
    by (auto simp: simple_clss_def C atms_of_def image_Un tautology_decomp distinct_mset_mset_set)

  have [simp]: ‹finite (Pos ` replacement_pos ` CB'')›  ‹finite (Pos ` replacement_neg ` CB')›
    using B'' ‹finite B''› decomp ‹finite B'› B' apply auto
    by (meson CB(1) finite_Σ finite_imageI finite_subset xs)
  show ?thesis
    unfolding C
    apply (subst B'', subst B')
    unfolding decomp image_image
    apply (subst image_mset_mset_set[symmetric])
    subgoal
      using decomp xs B' B'' inter CB
      by (auto simp: C inj_on_def subset_iff)
    apply (subst image_mset_mset_set[symmetric])
    subgoal
      using decomp xs B' B'' inter CB
      by (auto simp: C inj_on_def subset_iff)
    apply (rule all_sound_trails_decomp_in[unfolded comp_def])
      using decomp xs B' B'' inter CB assms(3) simple
      unfolding C
      apply (auto simp: image_image)
      subgoal for x
        apply (subgoal_tac ‹x ∈ ΔΣ›)
        using assms(3)[of x]
        apply auto
        by (metis (mono_tags, lifting) B' ‹finite (Pos ` replacement_neg ` CB')› ‹finite B''› decomp(2)
         finite_set_mset_mset_set image_iff)
    done
qed

end


locale dpll_optimal_encoding_opt =
  dpllW_state_optimal_weight trail clauses
    tl_trail cons_trail state_eq state ρ update_additional_info +
  optimal_encoding_opt_ops Σ ΔΣ new_vars
  for
    trail :: ‹'st ⇒ 'v  dpllW_ann_lits› and
    clauses :: ‹'st ⇒ 'v clauses› and
    tl_trail :: ‹'st ⇒ 'st› and
    cons_trail :: ‹'v  dpllW_ann_lit ⇒ 'st ⇒ 'st› and
    state_eq  :: ‹'st ⇒ 'st ⇒ bool› (infix ‹∼› 50) and
    state :: ‹'st ⇒ 'v  dpllW_ann_lits × 'v clauses × 'v clause option × 'b› and
    update_additional_info :: ‹'v clause option × 'b ⇒ 'st ⇒ 'st› and
    Σ ΔΣ :: ‹'v set› and
    ρ :: ‹'v clause ⇒ 'a :: {linorder}› and
    new_vars :: ‹'v ⇒ 'v × 'v›
begin

end


locale dpll_optimal_encoding =
  dpll_optimal_encoding_opt trail clauses
    tl_trail cons_trail state_eq state
    update_additional_info Σ ΔΣ ρ new_vars  +
  optimal_encoding_ops
    Σ ΔΣ
    new_vars ρ
  for
    trail :: ‹'st ⇒ 'v  dpllW_ann_lits› and
    clauses :: ‹'st ⇒ 'v clauses› and
    tl_trail :: ‹'st ⇒ 'st› and
    cons_trail :: ‹'v  dpllW_ann_lit ⇒ 'st ⇒ 'st› and
    state_eq  :: ‹'st ⇒ 'st ⇒ bool› (infix ‹∼› 50) and
    state :: ‹'st ⇒ 'v  dpllW_ann_lits × 'v clauses × 'v clause option × 'b› and
    update_additional_info :: ‹'v clause option × 'b ⇒ 'st ⇒ 'st› and
    Σ ΔΣ :: ‹'v set› and
    ρ :: ‹'v clause ⇒ 'a :: {linorder}› and
    new_vars :: ‹'v ⇒ 'v × 'v›
begin


inductive odecide :: ‹'st ⇒ 'st ⇒ bool› where
  odecide_noweight: ‹odecide S T›
if
  ‹undefined_lit (trail S) L› and
  ‹atm_of L ∈ atms_of_mm (clauses S)› and
  ‹T ∼ cons_trail (Decided L) S› and
  ‹atm_of L ∈ Σ - ΔΣ› |
  odecide_replacement_pos: ‹odecide S T›
if
  ‹undefined_lit (trail S) (Pos (replacement_pos L))› and
  ‹T ∼ cons_trail (Decided (Pos (replacement_pos L))) S› and
  ‹L ∈ ΔΣ› |
  odecide_replacement_neg: ‹odecide S T›
if
  ‹undefined_lit (trail S) (Pos (replacement_neg L))› and
  ‹T ∼ cons_trail (Decided (Pos (replacement_neg L))) S› and
  ‹L ∈ ΔΣ›

inductive_cases odecideE: ‹odecide S T›

inductive dpll_conflict :: ‹'st ⇒ 'st ⇒ bool› where
‹dpll_conflict S S›
if ‹C ∈# clauses S› and
  ‹trail S ⊨as CNot C›

inductive odpllW_core_stgy :: ‹'st ⇒ 'st ⇒ bool› for S T where
propagate: ‹dpll_propagate S T ⟹ odpllW_core_stgy S T› |
decided: ‹odecide S T ⟹ no_step dpll_propagate S  ⟹ odpllW_core_stgy S T › |
backtrack: ‹dpll_backtrack S T ⟹ odpllW_core_stgy S T› |
backtrack_opt: ‹bnb.backtrack_opt S T ⟹ odpllW_core_stgy S T›

lemma odpllW_core_stgy_clauses:
  ‹odpllW_core_stgy S T ⟹ clauses T = clauses S›
  by (induction rule: odpllW_core_stgy.induct)
   (auto simp: dpll_propagate.simps odecide.simps dpll_backtrack.simps
      bnb.backtrack_opt.simps)

lemma rtranclp_odpllW_core_stgy_clauses:
  ‹odpllW_core_stgy** S T ⟹ clauses T = clauses S›
  by (induction rule: rtranclp_induct)
    (auto dest: odpllW_core_stgy_clauses)


inductive odpllW_bnb_stgy :: ‹'st ⇒ 'st ⇒ bool› for S T :: 'st where
dpll:
  ‹odpllW_bnb_stgy S T›
  if ‹odpllW_core_stgy S T› |
bnb:
  ‹odpllW_bnb_stgy S T›
  if ‹bnb.dpllW_bound S T›

lemma odpllW_bnb_stgy_clauses:
  ‹odpllW_bnb_stgy S T ⟹ clauses T = clauses S›
  by (induction rule: odpllW_bnb_stgy.induct)
   (auto simp: bnb.dpllW_bound.simps dest: odpllW_core_stgy_clauses)

lemma rtranclp_odpllW_bnb_stgy_clauses:
  ‹odpllW_bnb_stgy** S T ⟹ clauses T = clauses S›
  by (induction rule: rtranclp_induct)
    (auto dest: odpllW_bnb_stgy_clauses)

lemma odecide_dpll_decide_iff:
  assumes ‹clauses S = penc N› ‹atms_of_mm N = Σ›
  shows ‹odecide S T ⟹ dpll_decide S T›
    ‹dpll_decide S T ⟹ Ex(odecide S)›
  using assms atms_of_mm_penc_subset2[of N] ΔΣ_Σ
  unfolding odecide.simps dpll_decide.simps
  apply (auto simp: odecide.simps dpll_decide.simps)
  apply (metis defined_lit_Pos_atm_iff state_eq_ref)+
  done

lemma
  assumes ‹clauses S = penc N› ‹atms_of_mm N = Σ›
  shows
    odpllW_core_stgy_dpllW_core_stgy: ‹odpllW_core_stgy S T ⟹ bnb.dpllW_core_stgy S T›
  using odecide_dpll_decide_iff[OF assms]
  by (auto simp: odpllW_core_stgy.simps bnb.dpllW_core_stgy.simps)

lemma
  assumes ‹clauses S = penc N› ‹atms_of_mm N = Σ›
  shows
    odpllW_bnb_stgy_dpllW_bnb_stgy: ‹odpllW_bnb_stgy S T ⟹ bnb.dpllW_bnb S T›
  using odecide_dpll_decide_iff[OF assms]
  by (auto simp: odpllW_bnb_stgy.simps bnb.dpllW_bnb.simps dest: odpllW_core_stgy_dpllW_core_stgy[OF assms]
    bnb.dpllW_core_stgy_dpllW_core)

lemma
  assumes ‹clauses S = penc N› and [simp]: ‹atms_of_mm N = Σ›
  shows
    rtranclp_odpllW_bnb_stgy_dpllW_bnb_stgy: ‹odpllW_bnb_stgy** S T ⟹ bnb.dpllW_bnb** S T›
  using assms(1) apply -
  apply (induction rule: rtranclp_induct)
  subgoal by auto
  subgoal for T U
    using odpllW_bnb_stgy_dpllW_bnb_stgy[of T N U] rtranclp_odpllW_bnb_stgy_clauses[of S T]
    by auto
  done

lemma no_step_odpllW_core_stgy_no_step_dpllW_core_stgy:
  assumes ‹clauses S = penc N› and [simp]:‹atms_of_mm N = Σ›
  shows
    ‹no_step odpllW_core_stgy S ⟷ no_step bnb.dpllW_core_stgy S›
  using odecide_dpll_decide_iff[of S, OF assms]
  by (auto simp: odpllW_core_stgy.simps bnb.dpllW_core_stgy.simps)

lemma no_step_odpllW_bnb_stgy_no_step_dpllW_bnb:
  assumes ‹clauses S = penc N› and [simp]:‹atms_of_mm N = Σ›
  shows
    ‹no_step odpllW_bnb_stgy S ⟷ no_step bnb.dpllW_bnb S›
  using no_step_odpllW_core_stgy_no_step_dpllW_core_stgy[of S, OF assms] bnb.no_step_stgy_iff
  by (auto simp: odpllW_bnb_stgy.simps bnb.dpllW_bnb.simps dest: odpllW_core_stgy_dpllW_core_stgy[OF assms]
    bnb.dpllW_core_stgy_dpllW_core)

lemma full_odpllW_core_stgy_full_dpllW_core_stgy:
  assumes ‹clauses S = penc N› and [simp]:‹atms_of_mm N = Σ›
  shows
    ‹full odpllW_bnb_stgy S T ⟹ full bnb.dpllW_bnb S T›
  using no_step_odpllW_bnb_stgy_no_step_dpllW_bnb[of T, OF _ assms(2)]
    rtranclp_odpllW_bnb_stgy_clauses[of S T, symmetric, unfolded assms]
    rtranclp_odpllW_bnb_stgy_dpllW_bnb_stgy[of S N T, OF assms]
   by (auto simp: full_def)


lemma decided_cons_eq_append_decide_cons:
  "Decided L # Ms = M' @ Decided K # M ⟷
    (L = K ∧ Ms = M ∧ M' = []) ∨
    (hd M' = Decided L ∧ Ms = tl M' @ Decided K # M ∧ M' ≠ [])"
  by (cases M')
   auto

lemma no_step_dpll_backtrack_iff:
  ‹no_step dpll_backtrack S ⟷ (count_decided (trail S) = 0 ∨ (∀C ∈# clauses S. ¬trail S ⊨as CNot C))›
  using backtrack_snd_empty_not_decided[of ‹trail S›] backtrack_split_list_eq[of ‹trail S›, symmetric]
  apply (cases ‹backtrack_split (trail S)›; cases ‹snd(backtrack_split (trail S))›)
  by (auto simp: dpll_backtrack.simps count_decided_0_iff)

lemma no_step_dpll_conflict:
  ‹no_step dpll_conflict S ⟷ (∀C ∈# clauses S. ¬trail S ⊨as CNot C)›
  by (auto simp: dpll_conflict.simps)

definition no_smaller_propa :: ‹'st ⇒ bool› where
"no_smaller_propa (S ::'st) ⟷
  (∀M K M' D L. trail S = M' @ Decided K # M ⟶ add_mset L D ∈# clauses S ⟶ undefined_lit M L ⟶ ¬M ⊨as CNot D)"

lemma [simp]: ‹T ∼ S ⟹ no_smaller_propa T = no_smaller_propa S›
  by (auto simp: no_smaller_propa_def)

lemma no_smaller_propa_cons_trail[simp]:
  ‹no_smaller_propa (cons_trail (Propagated L C) S) ⟷ no_smaller_propa S›
  ‹no_smaller_propa (update_weight_information M' S) ⟷ no_smaller_propa S›
  by (force simp: no_smaller_propa_def cdclW_restart_mset.propagated_cons_eq_append_decide_cons)+

lemma no_smaller_propa_cons_trail_decided[simp]:
  ‹no_smaller_propa S ⟹ no_smaller_propa (cons_trail (Decided L) S) ⟷ (∀L C. add_mset L C ∈# clauses S ⟶ undefined_lit (trail S)L ⟶ ¬trail S ⊨as CNot C)›
  by (auto simp: no_smaller_propa_def cdclW_restart_mset.propagated_cons_eq_append_decide_cons
    decided_cons_eq_append_decide_cons)

lemma no_step_dpll_propagate_iff:
  ‹no_step dpll_propagate S ⟷ (∀L C. add_mset L C ∈# clauses S ⟶ undefined_lit (trail S)L ⟶ ¬trail S ⊨as CNot C)›
  by (auto simp: dpll_propagate.simps)

lemma count_decided_0_no_smaller_propa: ‹count_decided (trail S) = 0 ⟹ no_smaller_propa S›
  by (auto simp: no_smaller_propa_def)

lemma no_smaller_propa_backtrack_split:
  ‹no_smaller_propa S ⟹
       backtrack_split (trail S) = (M', L # M) ⟹
       no_smaller_propa (reduce_trail_to M S)›
  using backtrack_split_list_eq[of ‹trail S›, symmetric]
  by (auto simp: no_smaller_propa_def)

lemma odpllW_core_stgy_no_smaller_propa:
  ‹odpllW_core_stgy S T ⟹ no_smaller_propa S ⟹ no_smaller_propa T›
  using no_step_dpll_backtrack_iff[of S] apply -
  by (induction rule: odpllW_core_stgy.induct)
   (auto 5 5 simp: cdclW_restart_mset.propagated_cons_eq_append_decide_cons count_decided_0_no_smaller_propa
      dpll_propagate.simps dpll_decide.simps odecide.simps decided_cons_eq_append_decide_cons
      bnb.backtrack_opt.simps dpll_backtrack.simps no_step_dpll_conflict no_smaller_propa_backtrack_split)

lemma odpllW_bound_stgy_no_smaller_propa: ‹bnb.dpllW_bound S T ⟹ no_smaller_propa S ⟹ no_smaller_propa T›
  by (auto simp: cdclW_restart_mset.propagated_cons_eq_append_decide_cons count_decided_0_no_smaller_propa
      dpll_propagate.simps dpll_decide.simps odecide.simps decided_cons_eq_append_decide_cons bnb.dpllW_bound.simps
      bnb.backtrack_opt.simps dpll_backtrack.simps no_step_dpll_conflict no_smaller_propa_backtrack_split)

lemma odpllW_bnb_stgy_no_smaller_propa:
  ‹odpllW_bnb_stgy S T ⟹ no_smaller_propa S ⟹ no_smaller_propa T›
  by (induction rule: odpllW_bnb_stgy.induct)
    (auto simp: odpllW_core_stgy_no_smaller_propa odpllW_bound_stgy_no_smaller_propa)


lemma filter_disjount_union:
  ‹(⋀x. x ∈ set xs ⟹ P x ⟹ ¬Q x) ⟹
   length (filter P xs) + length (filter Q xs) =
     length (filter (λx. P x ∨ Q x) xs)›
  by (induction xs) auto

lemma Collect_req_remove1:
  ‹{a ∈ A. a ≠ b ∧ P a} = (if P b then Set.remove b {a ∈ A. P a} else {a ∈ A. P a})› and
  Collect_req_remove2:
  ‹{a ∈ A. b ≠ a ∧ P a} = (if P b then Set.remove b {a ∈ A. P a} else {a ∈ A. P a})›
  by auto

lemma card_remove:
  ‹card (Set.remove a A) = (if a ∈ A then card A - 1 else card A)›
  by (auto simp: Set.remove_def)

lemma isabelle_should_do_that_automatically: ‹Suc (a - Suc 0) = a ⟷ a ≥ 1›
  by auto
lemma distinct_count_list_if: ‹distinct xs ⟹ count_list xs x = (if x ∈ set xs then 1 else 0)›
  by (induction xs) auto

abbreviation (input) cut_and_complete_trail :: ‹'st ⇒ _› where
‹cut_and_complete_trail S ≡ trail S›


(*TODO prove that favouring conflict over propagate works [this is obvious, but still]...*)
inductive odpllW_core_stgy_count :: ‹'st × _ ⇒ 'st × _ ⇒ bool› where
propagate: ‹dpll_propagate S T ⟹ odpllW_core_stgy_count (S, C) (T, C)› |
decided: ‹odecide S T ⟹ no_step dpll_propagate S  ⟹ odpllW_core_stgy_count (S, C) (T, C) › |
backtrack: ‹dpll_backtrack S T ⟹ odpllW_core_stgy_count (S, C) (T, add_mset (cut_and_complete_trail S) C)› |
backtrack_opt: ‹bnb.backtrack_opt S T ⟹ odpllW_core_stgy_count (S, C) (T, add_mset (cut_and_complete_trail S) C)›


inductive odpllW_bnb_stgy_count :: ‹'st × _ ⇒ 'st × _ ⇒ bool› where
dpll:
  ‹odpllW_bnb_stgy_count S T›
  if ‹odpllW_core_stgy_count S T› |
bnb:
  ‹odpllW_bnb_stgy_count (S, C) (T, C)›
  if ‹bnb.dpllW_bound S T›


lemma odpllW_core_stgy_countD:
  ‹odpllW_core_stgy_count S T ⟹ odpllW_core_stgy (fst S) (fst T)›
  ‹odpllW_core_stgy_count S T ⟹ snd S ⊆# snd T›
  by (induction rule: odpllW_core_stgy_count.induct; auto intro: odpllW_core_stgy.intros)+

lemma odpllW_bnb_stgy_countD:
  ‹odpllW_bnb_stgy_count S T ⟹ odpllW_bnb_stgy (fst S) (fst T)›
  ‹odpllW_bnb_stgy_count S T ⟹ snd S ⊆# snd T›
  by (induction rule: odpllW_bnb_stgy_count.induct; auto dest: odpllW_core_stgy_countD intro: odpllW_bnb_stgy.intros)+

lemma rtranclp_odpllW_bnb_stgy_countD:
  ‹odpllW_bnb_stgy_count** S T ⟹ odpllW_bnb_stgy** (fst S) (fst T)›
  ‹odpllW_bnb_stgy_count** S T ⟹ snd S ⊆# snd T›
  by (induction rule: rtranclp_induct; auto dest: odpllW_bnb_stgy_countD)+

lemmas odpllW_core_stgy_count_induct = odpllW_core_stgy_count.induct[of ‹(S, n)› ‹(T, m)› for S n T m, split_format(complete), OF dpll_optimal_encoding_axioms,
   consumes 1]


definition conflict_clauses_are_entailed :: ‹'st × _ ⇒ bool› where
‹conflict_clauses_are_entailed =
  (λ(S, Cs). ∀C ∈# Cs. (∃M' K M M''. trail S = M' @ Propagated K () # M ∧ C = M'' @ Decided (-K) # M))›

definition conflict_clauses_are_entailed2 :: ‹'st × ('v literal, 'v literal, unit) annotated_lits multiset ⇒ bool› where
‹conflict_clauses_are_entailed2 =
  (λ(S, Cs). ∀C ∈# Cs. ∀C' ∈# remove1_mset C Cs. (∃L. Decided L ∈ set C ∧ Propagated (-L) () ∈ set C') ∨
    (∃L.  Propagated (L) () ∈ set C ∧ Decided (-L) ∈ set C'))›

lemma propagated_cons_eq_append_propagated_cons:
 ‹Propagated L () # M = M' @ Propagated K () # Ma ⟷
  (M' = [] ∧ K = L ∧ M = Ma) ∨
  (M' ≠ [] ∧ hd M' = Propagated L () ∧ M = tl M' @ Propagated K () # Ma)›
  by (cases M')
    auto


lemma odpllW_core_stgy_count_conflict_clauses_are_entailed:
  assumes
    ‹odpllW_core_stgy_count S T› and
    ‹conflict_clauses_are_entailed S›
  shows
    ‹conflict_clauses_are_entailed T›
  using assms
  apply (induction rule: odpllW_core_stgy_count.induct)
  subgoal
    apply (auto simp: dpll_propagate.simps conflict_clauses_are_entailed_def
      cdclW_restart_mset.propagated_cons_eq_append_decide_cons)
    by (metis append_Cons)
  subgoal for S T
    apply (auto simp: odecide.simps conflict_clauses_are_entailed_def
      dest!: multi_member_split intro: exI[of _ ‹Decided _ # _›])
    by (metis append_Cons)+
  subgoal for S T C
    using backtrack_split_list_eq[of ‹trail S›, symmetric]
      backtrack_split_snd_hd_decided[of ‹trail S›]
    apply (auto simp: dpll_backtrack.simps conflict_clauses_are_entailed_def
        propagated_cons_eq_append_propagated_cons is_decided_def append_eq_append_conv2
        eq_commute[of _ ‹Propagated _ () # _›] conj_disj_distribR ex_disj_distrib
      cdclW_restart_mset.propagated_cons_eq_append_decide_cons dpllW_all_inv_def
      dest!: multi_member_split
      simp del: backtrack_split_list_eq
     )
     apply (case_tac us)
     by force+
  subgoal for S T C
    using backtrack_split_list_eq[of ‹trail S›, symmetric]
      backtrack_split_snd_hd_decided[of ‹trail S›]
    apply (auto simp: bnb.backtrack_opt.simps conflict_clauses_are_entailed_def
        propagated_cons_eq_append_propagated_cons is_decided_def append_eq_append_conv2
        eq_commute[of _ ‹Propagated _ () # _›] conj_disj_distribR ex_disj_distrib
      cdclW_restart_mset.propagated_cons_eq_append_decide_cons
      dpllW_all_inv_def
      dest!: multi_member_split
      simp del: backtrack_split_list_eq
     )
     apply (case_tac us)
     by force+
  done


lemma odpllW_bnb_stgy_count_conflict_clauses_are_entailed:
  assumes
    ‹odpllW_bnb_stgy_count S T› and
    ‹conflict_clauses_are_entailed S›
  shows
    ‹conflict_clauses_are_entailed T›
  using assms odpllW_core_stgy_count_conflict_clauses_are_entailed[of S T]
  apply (auto simp: odpllW_bnb_stgy_count.simps)
  apply (auto simp: conflict_clauses_are_entailed_def
    bnb.dpllW_bound.simps)
  done

lemma odpllW_core_stgy_count_no_dup_clss:
  assumes
    ‹odpllW_core_stgy_count S T› and
    ‹∀C ∈# snd S. no_dup C› and
    invs: ‹dpllW_all_inv (bnb.abs_state (fst S))›
  shows
    ‹∀C ∈# snd T. no_dup C›
  using assms
  by (induction rule: odpllW_core_stgy_count.induct)
    (auto simp: dpllW_all_inv_def)

lemma odpllW_bnb_stgy_count_no_dup_clss:
  assumes
    ‹odpllW_bnb_stgy_count S T› and
    ‹∀C ∈# snd S. no_dup C› and
    invs: ‹dpllW_all_inv (bnb.abs_state (fst S))›
  shows
    ‹∀C ∈# snd T. no_dup C›
  using assms
  by (induction rule: odpllW_bnb_stgy_count.induct)
    (auto simp: dpllW_all_inv_def 
      bnb.dpllW_bound.simps dest!: odpllW_core_stgy_count_no_dup_clss)

lemma backtrack_split_conflict_clauses_are_entailed_itself:
  assumes
    ‹backtrack_split (trail S) = (M', L # M)› and
    invs: ‹dpllW_all_inv (bnb.abs_state S)›
  shows ‹¬ conflict_clauses_are_entailed
            (S, add_mset (trail S) C)› (is ‹¬ ?A›)
proof
  assume ?A
  then obtain M' K Ma where
    tr: ‹trail S = M' @ Propagated K () # Ma› and
    ‹add_mset (- K) (lit_of `# mset Ma) ⊆#
       add_mset (lit_of L) (lit_of `# mset M)›
    by (clarsimp simp: conflict_clauses_are_entailed_def)

  then have ‹-K ∈# add_mset (lit_of L) (lit_of `# mset M)›
    by (meson member_add_mset mset_subset_eqD)
  then have ‹-K ∈# lit_of `# mset (trail S)›
    using backtrack_split_list_eq[of ‹trail S›, symmetric] assms(1)
    by auto
  moreover have ‹K ∈# lit_of `# mset (trail S)›
    by (auto simp: tr)
  ultimately show False using invs unfolding dpllW_all_inv_def
    by (auto simp add: no_dup_cannot_not_lit_and_uminus uminus_lit_swap)
qed



lemma odpllW_core_stgy_count_distinct_mset:
  assumes
    ‹odpllW_core_stgy_count S T› and
    ‹conflict_clauses_are_entailed S› and
    ‹distinct_mset (snd S)› and
    invs: ‹dpllW_all_inv (bnb.abs_state (fst S))›
  shows
    ‹distinct_mset (snd T)›
  using assms(1,2,3,4) odpllW_core_stgy_count_conflict_clauses_are_entailed[OF assms(1,2)]
  apply (induction rule: odpllW_core_stgy_count.induct)
  subgoal
    by (auto simp: dpll_propagate.simps conflict_clauses_are_entailed_def
      cdclW_restart_mset.propagated_cons_eq_append_decide_cons)
  subgoal
    by (auto simp:)
  subgoal for S T C
    by (clarsimp simp: dpll_backtrack.simps backtrack_split_conflict_clauses_are_entailed_itself
      dest!: multi_member_split)
  subgoal for S T C
    by (clarsimp simp: bnb.backtrack_opt.simps backtrack_split_conflict_clauses_are_entailed_itself
      dest!: multi_member_split)
  done

lemma odpllW_bnb_stgy_count_distinct_mset:
  assumes
    ‹odpllW_bnb_stgy_count S T› and
    ‹conflict_clauses_are_entailed S› and
    ‹distinct_mset (snd S)› and
    invs: ‹dpllW_all_inv (bnb.abs_state (fst S))›
  shows
    ‹distinct_mset (snd T)›
  using assms odpllW_core_stgy_count_distinct_mset[OF _ assms(2-), of T]
  by (auto simp: odpllW_bnb_stgy_count.simps)


lemma odpllW_core_stgy_count_conflict_clauses_are_entailed2:
  assumes
    ‹odpllW_core_stgy_count S T› and
    ‹conflict_clauses_are_entailed S› and
    ‹conflict_clauses_are_entailed2 S› and
    ‹distinct_mset (snd S)› and
    invs: ‹dpllW_all_inv (bnb.abs_state (fst S))›
  shows
      ‹conflict_clauses_are_entailed2 T›
  using assms
proof (induction rule: odpllW_core_stgy_count.induct)
  case (propagate S T C)
  then show ?case
    by (auto simp: dpll_propagate.simps conflict_clauses_are_entailed2_def)
next
  case (decided S T C)
  then show ?case
    by (auto simp: dpll_decide.simps conflict_clauses_are_entailed2_def)
next
  case (backtrack S T C) note bt = this(1) and ent = this(2) and ent2 = this(3) and dist = this(4)
    and invs = this(5)
  let ?M = ‹(cut_and_complete_trail S)›
  have ‹conflict_clauses_are_entailed (T, add_mset ?M C)› and
    dist': ‹distinct_mset (add_mset ?M C)›
    using odpllW_core_stgy_count_conflict_clauses_are_entailed[OF _ ent, of ‹(T, add_mset ?M C)›]
    odpllW_core_stgy_count_distinct_mset[OF _ ent dist invs, of ‹(T, add_mset ?M C)›]
      bt by (auto dest!: odpllW_core_stgy_count.intros(3)[of S T C])

  obtain M1 K M2 where
    spl: ‹backtrack_split (trail S) = (M2, Decided K # M1)›
    using bt backtrack_split_snd_hd_decided[of ‹trail S›]
    by (cases ‹hd (snd (backtrack_split (trail S)))›) (auto simp: dpll_backtrack.simps)
  have has_dec: ‹∃l∈set (trail S). is_decided l›
    using bt apply (auto simp: dpll_backtrack.simps)
    using bt count_decided_0_iff no_step_dpll_backtrack_iff by blast

  let ?P = ‹λCa C'.
          (∃L. Decided L ∈ set Ca ∧ Propagated (- L) () ∈ set C') ∨
          (∃L. Propagated L () ∈ set Ca ∧ Decided (- L)  ∈ set C')›
  have ‹∀C'∈#remove1_mset ?M C. ?P ?M C'›
  proof
    fix C'
    assume ‹C'∈#remove1_mset ?M C›
    then have ‹C' ∈# C› and ‹C' ≠ ?M›
      using dist' by auto
    then obtain M' L M M'' where
      ‹trail S = M' @ Propagated L () # M› and
      ‹C' = M'' @ Decided (- L) # M›
      using ent unfolding conflict_clauses_are_entailed_def
      by auto
    then show ‹?P ?M C'›
      using backtrack_split_some_is_decided_then_snd_has_hd[of ‹trail S›, OF has_dec]
        spl backtrack_split_list_eq[of ‹trail S›, symmetric]
      by (clarsimp simp: conj_disj_distribR ex_disj_distrib  decided_cons_eq_append_decide_cons
        cdclW_restart_mset.propagated_cons_eq_append_decide_cons propagated_cons_eq_append_propagated_cons
        append_eq_append_conv2)
  qed
  moreover have H: ‹?case ⟷ (∀Ca∈#add_mset ?M C.
       ∀C'∈#remove1_mset Ca C. ?P Ca C')›
    unfolding conflict_clauses_are_entailed2_def prod.case
    apply (intro conjI iffI impI ballI)
    subgoal for Ca C'
      by (auto dest: multi_member_split dest: in_diffD)
    subgoal for Ca C'
      using dist'
      by (auto 5 3 dest!: multi_member_split[of Ca] dest: in_diffD)
    done
  moreover have ‹(∀Ca∈#C. ∀C'∈#remove1_mset Ca C. ?P Ca C')›
    using ent2 unfolding conflict_clauses_are_entailed2_def
    by auto
  ultimately show ?case
    unfolding H
    by auto
next
  case (backtrack_opt S T C) note bt = this(1) and ent = this(2) and ent2 = this(3) and dist = this(4)
    and invs = this(5)
  let ?M = ‹(cut_and_complete_trail S)›
  have ‹conflict_clauses_are_entailed (T, add_mset ?M C)› and
    dist': ‹distinct_mset (add_mset ?M C)›
    using odpllW_core_stgy_count_conflict_clauses_are_entailed[OF _ ent, of ‹(T, add_mset ?M C)›]
    odpllW_core_stgy_count_distinct_mset[OF _ ent dist invs, of ‹(T, add_mset ?M C)›]
      bt by (auto dest!: odpllW_core_stgy_count.intros(4)[of S T C])

  obtain M1 K M2 where
    spl: ‹backtrack_split (trail S) = (M2, Decided K # M1)›
    using bt backtrack_split_snd_hd_decided[of ‹trail S›]
    by (cases ‹hd (snd (backtrack_split (trail S)))›) (auto simp: bnb.backtrack_opt.simps)
  have has_dec: ‹∃l∈set (trail S). is_decided l›
    using bt apply (auto simp: bnb.backtrack_opt.simps)
    by (metis annotated_lit.disc(1) backtrack_split_list_eq in_set_conv_decomp snd_conv spl)

  let ?P = ‹λCa C'.
          (∃L. Decided L ∈ set Ca ∧ Propagated (- L) () ∈ set C') ∨
          (∃L. Propagated L () ∈ set Ca ∧ Decided (- L)  ∈ set C')›
  have ‹∀C'∈#remove1_mset ?M C. ?P ?M C'›
  proof
    fix C'
    assume ‹C'∈#remove1_mset ?M C›
    then have ‹C' ∈# C› and ‹C' ≠ ?M›
      using dist' by auto
    then obtain M' L M M'' where
      ‹trail S = M' @ Propagated L () # M› and
      ‹C' = M'' @ Decided (- L) # M›
      using ent unfolding conflict_clauses_are_entailed_def
      by auto
    then show ‹?P ?M C'›
      using backtrack_split_some_is_decided_then_snd_has_hd[of ‹trail S›, OF has_dec]
        spl backtrack_split_list_eq[of ‹trail S›, symmetric]
      by (clarsimp simp: conj_disj_distribR ex_disj_distrib  decided_cons_eq_append_decide_cons
        cdclW_restart_mset.propagated_cons_eq_append_decide_cons propagated_cons_eq_append_propagated_cons
        append_eq_append_conv2)
  qed
  moreover have H: ‹?case ⟷ (∀Ca∈#add_mset ?M C.
       ∀C'∈#remove1_mset Ca C. ?P Ca C')›
    unfolding conflict_clauses_are_entailed2_def prod.case
    apply (intro conjI iffI impI ballI)
    subgoal for Ca C'
      by (auto dest: multi_member_split dest: in_diffD)
    subgoal for Ca C'
      using dist'
      by (auto 5 3 dest!: multi_member_split[of Ca] dest: in_diffD)
    done
  moreover have ‹(∀Ca∈#C. ∀C'∈#remove1_mset Ca C. ?P Ca C')›
    using ent2 unfolding conflict_clauses_are_entailed2_def
    by auto
  ultimately show ?case
    unfolding H
    by auto
qed


lemma odpllW_bnb_stgy_count_conflict_clauses_are_entailed2:
  assumes
    ‹odpllW_bnb_stgy_count S T› and
    ‹conflict_clauses_are_entailed S› and
    ‹conflict_clauses_are_entailed2 S› and
    ‹distinct_mset (snd S)› and
    invs: ‹dpllW_all_inv (bnb.abs_state (fst S))›
  shows
    ‹conflict_clauses_are_entailed2 T›
  using assms odpllW_core_stgy_count_conflict_clauses_are_entailed2[of S T]
  apply (auto simp: odpllW_bnb_stgy_count.simps)
  apply (auto simp: conflict_clauses_are_entailed2_def
    bnb.dpllW_bound.simps)
  done

definition no_complement_set_lit :: ‹'v dpllW_ann_lits ⇒ bool› where
  ‹no_complement_set_lit M ⟷
    (∀L ∈ ΔΣ. Decided (Pos (replacement_pos L)) ∈ set M ⟶ Decided (Pos (replacement_neg L)) ∉ set M) ∧
    (∀L ∈ ΔΣ. Decided (Neg (replacement_pos L)) ∉ set M) ∧
    (∀L ∈ ΔΣ. Decided (Neg (replacement_neg L)) ∉ set M) ∧
    atm_of ` lits_of_l M ⊆ Σ - ΔΣ ∪ replacement_pos ` ΔΣ ∪ replacement_neg ` ΔΣ›

definition no_complement_set_lit_st :: ‹'st × 'v dpllW_ann_lits multiset ⇒ bool› where
  ‹no_complement_set_lit_st = (λ(S, Cs). (∀C∈#Cs. no_complement_set_lit C) ∧ no_complement_set_lit (trail S))›

lemma backtrack_no_complement_set_lit: ‹no_complement_set_lit (trail S) ⟹
       backtrack_split (trail S) = (M', L # M) ⟹
       no_complement_set_lit (Propagated (- lit_of L) () # M)›
  using backtrack_split_list_eq[of ‹trail S›, symmetric]
  by (auto simp: no_complement_set_lit_def)

lemma odpllW_core_stgy_count_no_complement_set_lit_st:
  assumes
    ‹odpllW_core_stgy_count S T› and
    ‹conflict_clauses_are_entailed S› and
    ‹conflict_clauses_are_entailed2 S› and
    ‹distinct_mset (snd S)› and
    invs: ‹dpllW_all_inv (bnb.abs_state (fst S))› and
    ‹no_complement_set_lit_st S› and
    atms: ‹clauses (fst S) = penc N› ‹atms_of_mm N = Σ› and
    ‹no_smaller_propa (fst S)›
  shows
      ‹no_complement_set_lit_st T›
  using assms
proof (induction rule: odpllW_core_stgy_count.induct)
  case (propagate S T C)
  then show ?case
    using atms_of_mm_penc_subset2[of N] ΔΣ_Σ
    apply (auto simp: dpll_propagate.simps no_complement_set_lit_st_def no_complement_set_lit_def
      dpllW_all_inv_def dest!: multi_member_split)
    apply blast
    apply blast
    apply auto
    done
next
  case (decided S T C)
  have H1: False if ‹Decided (Pos (L↦0)) ∈ set (trail S)›
    ‹undefined_lit (trail S) (Pos (L↦1))› ‹L ∈ ΔΣ› for L
  proof -
    have ‹{#Neg (L↦0), Neg (L↦1)#} ∈# clauses S›
      using decided that
      by (fastforce simp: penc_def additional_constraints_def additional_constraint_def)
    then show False
      using decided(2) that
      apply (auto 7 4 simp: dpll_propagate.simps add_mset_eq_add_mset all_conj_distrib
          imp_conjR imp_conjL remove1_mset_empty_iff defined_lit_Neg_Pos_iff lits_of_def
        dest!: multi_member_split dest: in_lits_of_l_defined_litD)
      apply (metis (full_types) image_iff lit_of.simps(1))
      apply auto
      apply (metis (full_types) image_iff lit_of.simps(1))
      done
  qed
  have H2: False if ‹Decided (Pos (L↦1)) ∈ set (trail S)›
    ‹undefined_lit (trail S) (Pos (L↦0))› ‹L ∈ ΔΣ› for L
  proof -
    have ‹{#Neg (L↦0), Neg (L↦1)#} ∈# clauses S›
      using decided that
      by (fastforce simp: penc_def additional_constraints_def additional_constraint_def)
    then show False
      using decided(2) that
      apply (auto 7 4 simp: dpll_propagate.simps add_mset_eq_add_mset all_conj_distrib
          imp_conjR imp_conjL remove1_mset_empty_iff defined_lit_Neg_Pos_iff lits_of_def
        dest!: multi_member_split dest: in_lits_of_l_defined_litD)
      apply (metis (full_types) image_iff lit_of.simps(1))
      apply auto
      apply (metis (full_types) image_iff lit_of.simps(1))
      done
  qed
  have ‹?case ⟷ no_complement_set_lit (trail T)›
    using decided(1,7) unfolding no_complement_set_lit_st_def
    by (auto simp: odecide.simps)
  moreover have ‹no_complement_set_lit (trail T)›
  proof -
    have H: ‹L ∈ ΔΣ ⟹
        Decided (Pos (L↦1)) ∈ set (trail S) ⟹
        Decided (Pos (L↦0)) ∈ set (trail S) ⟹ False›
      ‹L ∈ ΔΣ ⟹ Decided (Neg (L↦1)) ∈ set (trail S) ⟹ False› 
      ‹L ∈ ΔΣ ⟹ Decided (Neg (L↦0)) ∈ set (trail S) ⟹ False›
      ‹atm_of ` lits_of_l (trail S) ⊆ Σ - ΔΣ ∪ replacement_pos ` ΔΣ ∪ replacement_neg ` ΔΣ›
      for L
      using decided(7) unfolding no_complement_set_lit_st_def no_complement_set_lit_def
      by blast+
    have ‹L ∈ ΔΣ ⟹
        Decided (Pos (L↦1)) ∈ set (trail T) ⟹
        Decided (Pos (L↦0)) ∈ set (trail T) ⟹ False› for L
      using decided(1) H(1)[of L] H1[of L] H2[of L]
      by (auto simp: odecide.simps no_complement_set_lit_def)
    moreover have ‹L ∈ ΔΣ ⟹ Decided (Neg (L↦1)) ∈ set (trail T) ⟹ False› for L
      using decided(1) H(2)[of L]
      by (auto simp: odecide.simps no_complement_set_lit_def)
    moreover have ‹L ∈ ΔΣ ⟹ Decided (Neg (L↦0)) ∈ set (trail T) ⟹ False› for L
      using decided(1) H(3)[of L]
      by (auto simp: odecide.simps no_complement_set_lit_def)
    moreover have ‹atm_of ` lits_of_l (trail T) ⊆ Σ - ΔΣ ∪ replacement_pos ` ΔΣ ∪ replacement_neg ` ΔΣ›
      using decided(1) H(4)
      by (auto 5 3 simp: odecide.simps no_complement_set_lit_def lits_of_def image_image)

    ultimately show ?thesis
      by (auto simp: no_complement_set_lit_def)
  qed
  ultimately show ?case
     by fast

next
  case (backtrack S T C) note bt = this(1) and ent = this(2) and ent2 = this(3) and dist = this(4)
    and invs = this(6)
  show ?case
    using bt invs
    by (auto simp: dpll_backtrack.simps no_complement_set_lit_st_def
      backtrack_no_complement_set_lit)

next
  case (backtrack_opt S T C) note bt = this(1) and ent = this(2) and ent2 = this(3) and dist = this(4)
    and invs = this(6)
  show ?case
    using bt invs
    by (auto simp: bnb.backtrack_opt.simps no_complement_set_lit_st_def
      backtrack_no_complement_set_lit)
qed

lemma odpllW_bnb_stgy_count_no_complement_set_lit_st:
  assumes
    ‹odpllW_bnb_stgy_count S T› and
    ‹conflict_clauses_are_entailed S› and
    ‹conflict_clauses_are_entailed2 S› and
    ‹distinct_mset (snd S)› and
    invs: ‹dpllW_all_inv (bnb.abs_state (fst S))› and
    ‹no_complement_set_lit_st S› and
    atms: ‹clauses (fst S) = penc N› ‹atms_of_mm N = Σ› and
    ‹no_smaller_propa (fst S)›
  shows
      ‹no_complement_set_lit_st T›
  using odpllW_core_stgy_count_no_complement_set_lit_st[of S T, OF _ assms(2-)] assms(1,6)
  by (auto simp: odpllW_bnb_stgy_count.simps no_complement_set_lit_st_def
    bnb.dpllW_bound.simps)

definition stgy_invs :: ‹'v clauses ⇒ 'st × _ ⇒ bool› where
  ‹stgy_invs N S ⟷
    no_smaller_propa (fst S) ∧
    conflict_clauses_are_entailed S ∧
    conflict_clauses_are_entailed2 S ∧
    distinct_mset (snd S) ∧
    (∀C ∈# snd S. no_dup C) ∧
    dpllW_all_inv (bnb.abs_state (fst S)) ∧
    no_complement_set_lit_st S ∧
    clauses (fst S) = penc N ∧
    atms_of_mm N = Σ
    ›

lemma odpllW_bnb_stgy_count_stgy_invs:
  assumes
    ‹odpllW_bnb_stgy_count S T› and
    ‹stgy_invs N S›
  shows ‹stgy_invs N T›
  using odpllW_bnb_stgy_count_conflict_clauses_are_entailed2[of S T]
    odpllW_bnb_stgy_count_conflict_clauses_are_entailed[of S T]
    odpllW_bnb_stgy_no_smaller_propa[of ‹fst S› ‹fst T›]
    odpllW_bnb_stgy_countD[of S T]
    odpllW_bnb_stgy_clauses[of ‹fst S› ‹fst T›]
    odpllW_core_stgy_count_distinct_mset[of S T]
    odpllW_bnb_stgy_count_no_dup_clss[of S T]
    odpllW_bnb_stgy_count_distinct_mset[of S T]
    assms
    odpllW_bnb_stgy_dpllW_bnb_stgy[of ‹fst S› N ‹fst T›]
    odpllW_bnb_stgy_count_no_complement_set_lit_st[of S T]
  using local.bnb.dpllW_bnb_abs_state_all_inv
  unfolding stgy_invs_def
  by auto

lemma stgy_invs_size_le:
  assumes ‹stgy_invs N S›
  shows ‹size (snd S) ≤ 3 ^ (card Σ)›
proof -
  have ‹no_smaller_propa (fst S)› and
    ‹conflict_clauses_are_entailed S› and
    ent2: ‹conflict_clauses_are_entailed2 S› and
    dist: ‹distinct_mset (snd S)› and
    n_d: ‹(∀C ∈# snd S. no_dup C)› and
    ‹dpllW_all_inv (bnb.abs_state (fst S))› and
    nc: ‹no_complement_set_lit_st S› and
    Σ: ‹atms_of_mm N = Σ›
    using assms unfolding stgy_invs_def by fast+

  let ?f = ‹(filter_mset is_decided o mset)›
  have ‹distinct_mset (?f `# (snd S))›
    apply (subst distinct_image_mset_inj)
    subgoal
      using ent2 n_d
      apply (auto simp: conflict_clauses_are_entailed2_def
        inj_on_def add_mset_eq_add_mset dest!: multi_member_split split_list)
      using n_d apply auto
      apply (metis defined_lit_def multiset_partition set_mset_mset union_iff union_single_eq_member)+
      done
    subgoal
      using dist by auto
    done
  have H: ‹lit_of `# ?f C ∈ all_sound_trails list_new_vars› if ‹C ∈# (snd S)› for C
  proof -
    have nc: ‹no_complement_set_lit C› and n_d: ‹no_dup C›
      using nc that n_d unfolding no_complement_set_lit_st_def
      by (auto dest!: multi_member_split)
    have taut: ‹¬tautology (lit_of `#  mset C)›
      using n_d no_dup_not_tautology by blast
    have taut: ‹¬tautology (lit_of `# ?f C)›
      apply (rule not_tautology_mono[OF _ taut])
      by (simp add: image_mset_subseteq_mono)
    have dist: ‹distinct_mset (lit_of `#  mset C)›
      using n_d no_dup_distinct by blast
    have dist: ‹distinct_mset (lit_of `# ?f C)›
      apply (rule distinct_mset_mono[OF _ dist])
      by (simp add: image_mset_subseteq_mono)

    show ?thesis
      apply (rule in_all_sound_trails)
      subgoal
        using nc unfolding no_complement_set_lit_def
        by (auto dest!: multi_member_split simp: is_decided_def)
      subgoal
        using nc unfolding no_complement_set_lit_def
        by (auto dest!: multi_member_split simp: is_decided_def)
      subgoal
        using nc unfolding no_complement_set_lit_def
        by (auto dest!: multi_member_split simp: is_decided_def)
      subgoal
        using nc n_d taut dist unfolding no_complement_set_lit_def set_list_new_vars
        by (auto dest!: multi_member_split simp: set_list_new_vars
          is_decided_def simple_clss_def atms_of_def lits_of_def
          image_image dest!: split_list)
      subgoal
        by (auto simp: set_list_new_vars)
      done
  qed
  then have incl: ‹set_mset ((image_mset lit_of o ?f) `# (snd S)) ⊆ all_sound_trails list_new_vars›
    by auto
  have K: ‹xs ≠ [] ⟹ ∃y ys. xs = y # ys› for xs
    by (cases xs) auto
  have K2: ‹Decided La # zsb = us @ Propagated (L) () # zsa ⟷
    (us ≠ [] ∧ hd us = Decided La ∧ zsb = tl us @ Propagated (L) () # zsa)› for La zsb us L zsa
    apply (cases us)
    apply auto
    done
  have inj: ‹inj_on ((`#) lit_of ∘ (filter_mset is_decided ∘ mset))
     (set_mset (snd S))›
     unfolding inj_on_def
  proof (intro ballI impI, rule ccontr)
    fix x y
    assume x: ‹x ∈# snd S› and
      y: ‹y ∈# snd S› and
      eq: ‹((`#) lit_of ∘ (filter_mset is_decided ∘ mset)) x =
         ((`#) lit_of ∘ (filter_mset is_decided ∘ mset)) y› and
      neq: ‹x ≠ y›
    consider
      L where ‹Decided L ∈ set x› ‹Propagated (- L) () ∈ set y› |
      L where ‹Decided L ∈ set y› ‹Propagated (- L) () ∈ set x›
      using ent2 n_d x y unfolding conflict_clauses_are_entailed2_def
      by (auto  dest!: multi_member_split simp: add_mset_eq_add_mset neq)
    then show False
    proof cases
      case 1
      show False
        using eq 1(1) multi_member_split[of ‹Decided L› ‹mset x›]
        apply auto
        by (smt 1(2) lit_of.simps(2) msed_map_invR multiset_partition n_d
          no_dup_cannot_not_lit_and_uminus set_mset_mset union_mset_add_mset_left union_single_eq_member y)
    next
      case 2
      show False
        using eq 2 multi_member_split[of ‹Decided L› ‹mset y›]
        apply auto
        by (smt lit_of.simps(2) msed_map_invR multiset_partition n_d
          no_dup_cannot_not_lit_and_uminus set_mset_mset union_mset_add_mset_left union_single_eq_member x)
    qed
  qed

  have [simp]: ‹finite Σ›
    unfolding Σ[symmetric]
    by auto
  have [simp]: ‹Σ ∪ ΔΣ = Σ›
    using ΔΣ_Σ by blast
  have ‹size (snd S) = size (((image_mset lit_of o ?f) `# (snd S)))›
    by auto
  also have ‹... = card (set_mset ((image_mset lit_of o ?f) `# (snd S)))›
    supply [[goals_limit=1]]
    apply (subst distinct_mset_size_eq_card)
    apply (subst distinct_image_mset_inj[OF inj])
    using dist by auto
  also have ‹... ≤ card (all_sound_trails list_new_vars)›
    by (rule card_mono[OF _ incl]) simp
  also have ‹... ≤ card (simple_clss (Σ - ΔΣ)) * 3 ^ card ΔΣ›
    using card_all_sound_trails[of list_new_vars]
    by (auto simp: set_list_new_vars distinct_list_new_vars
      length_list_new_vars)
  also have ‹... ≤ 3 ^ card (Σ - ΔΣ) * 3 ^ card ΔΣ›
    using simple_clss_card[of ‹Σ - ΔΣ›]
    unfolding set_list_new_vars distinct_list_new_vars
      length_list_new_vars
    by (auto simp: set_list_new_vars distinct_list_new_vars
      length_list_new_vars)
  also have ‹... = (3 :: nat) ^ (card Σ)›
    unfolding comm_semiring_1_class.semiring_normalization_rules(26)
    by (subst card_Un_disjoint[symmetric])
      auto
  finally show ‹size (snd S) ≤ 3 ^ card Σ›
    .
qed

lemma rtranclp_odpllW_bnb_stgy_count_stgy_invs: ‹odpllW_bnb_stgy_count** S T ⟹ stgy_invs N S ⟹ stgy_invs N T›
  apply (induction rule: rtranclp_induct)
  apply (auto dest!: odpllW_bnb_stgy_count_stgy_invs)
  done

theorem (* \htmllink{ODPLL-complexity} *)
  assumes ‹clauses S = penc N› ‹atms_of_mm N = Σ› and
    ‹odpllW_bnb_stgy_count** (S, {#}) (T, D)› and
    tr: ‹trail S = []›
  shows ‹size D ≤ 3 ^ (card Σ)›
proof -
  have i: ‹stgy_invs N (S, {#})›
    using tr unfolding no_smaller_propa_def
      stgy_invs_def conflict_clauses_are_entailed_def
      conflict_clauses_are_entailed2_def assms(1,2)
      no_complement_set_lit_st_def no_complement_set_lit_def
      dpllW_all_inv_def
    by (auto simp: assms(1))
  show ?thesis
    using rtranclp_odpllW_bnb_stgy_count_stgy_invs[OF assms(3) i]
      stgy_invs_size_le[of N ‹(T, D)›]
    by auto
qed

end

end