Theory CDCL_W_Optimal_Model

theory CDCL_W_Optimal_Model
  imports CDCL_W_BnB "HOL-Library.Extended_Nat"
begin

subsubsection ‹OCDCL›

text ‹
  The following datatype is equivalent to \<^typ>‹'a option›. Howover, it has the opposite
  ordering. Therefore, I decided to use a different type instead of have a second order
  which conflicts with 🗏‹~~/src/HOL/Library/Option_ord.thy›.
›
datatype 'a optimal_model = Not_Found | is_found: Found (the_optimal: 'a)

instantiation optimal_model :: (ord) ord
begin
  fun less_optimal_model  :: ‹'a :: ord optimal_model ⇒ 'a optimal_model ⇒ bool› where
  ‹less_optimal_model Not_Found _ = False›
| ‹less_optimal_model (Found _) Not_Found ⟷ True›
| ‹less_optimal_model (Found a) (Found b) ⟷ a < b›

fun less_eq_optimal_model  :: ‹'a :: ord optimal_model ⇒ 'a optimal_model ⇒ bool› where
  ‹less_eq_optimal_model Not_Found Not_Found = True›
| ‹less_eq_optimal_model Not_Found (Found _) = False›
| ‹less_eq_optimal_model (Found _) Not_Found ⟷ True›
| ‹less_eq_optimal_model (Found a) (Found b) ⟷ a ≤ b›

instance
  by standard

end

instance optimal_model :: (preorder) preorder
  apply standard
  subgoal for a b
    by (cases a; cases b) (auto simp: less_le_not_le)
  subgoal for a
    by (cases a) auto
  subgoal for a b c
    by (cases a; cases b; cases c) (auto dest: order_trans)
  done

instance optimal_model :: (order) order
  apply standard
  subgoal for a b
    by (cases a; cases b) (auto simp: less_le_not_le)
  done

instance optimal_model :: (linorder) linorder
  apply standard
  subgoal for a b
    by (cases a; cases b) (auto simp: less_le_not_le)
  done

instantiation optimal_model :: (wellorder) wellorder
begin

lemma wf_less_optimal_model: ‹wf {(M :: 'a optimal_model, N). M < N}›
proof -
  have 1: ‹{(M :: 'a optimal_model, N). M < N} =
    map_prod Found Found ` {(M :: 'a, N). M < N} ∪
    {(a, b). a ≠ Not_Found ∧ b = Not_Found}› (is ‹?A = ?B ∪ ?C›)
    apply (auto simp: image_iff)
    apply (case_tac a; case_tac b)
    apply auto
    apply (case_tac a)
    apply auto
    done
  have [simp]: ‹inj Found›
    by (auto simp:inj_on_def)
  have ‹wf ?B›
    by (rule wf_map_prod_image) (auto intro: wf)
  moreover have ‹wf ?C›
    by (rule wfI_pf) auto
  ultimately show ‹wf (?A)›
    unfolding 1
    by (rule wf_Un) (auto)
qed

instance by standard (metis CollectI split_conv wf_def wf_less_optimal_model)

end


text ‹This locales includes only the assumption we make on the weight function.›
locale ocdcl_weight =
  fixes
    ρ :: ‹'v clause ⇒ 'a :: {linorder}›
  assumes
    ρ_mono: ‹distinct_mset B ⟹ A ⊆# B ⟹ ρ A ≤ ρ B›
begin

lemma ρ_empty_simp[simp]:
  assumes ‹consistent_interp (set_mset A)› ‹distinct_mset A›
  shows ‹ρ A ≥ ρ {#}› ‹¬ρ A < ρ {#}›  ‹ρ A ≤ ρ {#} ⟷ ρ A = ρ {#}›
  using ρ_mono[of A ‹{#}›] assms
  by auto

abbreviation ρ' :: ‹'v clause option ⇒ 'a optimal_model› where
  ‹ρ' w ≡ (case w of None ⇒ Not_Found | Some w ⇒ Found (ρ w))›

definition is_improving_int
  :: "('v literal, 'v literal, 'b) annotated_lits ⇒ ('v literal, 'v literal, 'b) annotated_lits ⇒ 'v clauses ⇒
    'v clause option ⇒ bool"
where
  ‹is_improving_int M M' N w ⟷ Found (ρ (lit_of `# mset M')) < ρ' w ∧
    M' ⊨asm N ∧ no_dup M' ∧
    lit_of `# mset M' ∈ simple_clss (atms_of_mm N) ∧
    total_over_m (lits_of_l M') (set_mset N) ∧
    (∀M'. total_over_m (lits_of_l M') (set_mset N) ⟶ mset M ⊆# mset M' ⟶
      lit_of `# mset M' ∈ simple_clss (atms_of_mm N) ⟶
      ρ (lit_of `# mset M') = ρ (lit_of `# mset M))›

definition too_heavy_clauses
  :: ‹'v clauses ⇒ 'v clause option ⇒ 'v clauses›
where
  ‹too_heavy_clauses M w =
     {#pNeg C | C ∈# mset_set (simple_clss (atms_of_mm M)). ρ' w ≤ Found (ρ C)#}›

definition conflicting_clauses
  :: ‹'v clauses ⇒ 'v clause option ⇒ 'v clauses›
where
  ‹conflicting_clauses N w =
    {#C ∈# mset_set (simple_clss (atms_of_mm N)). too_heavy_clauses N w ⊨pm C#}›

lemma too_heavy_clauses_conflicting_clauses:
  ‹C ∈# too_heavy_clauses M w ⟹ C ∈# conflicting_clauses M w›
  by (auto simp: conflicting_clauses_def too_heavy_clauses_def simple_clss_finite)

lemma too_heavy_clauses_contains_itself:
  ‹M ∈ simple_clss (atms_of_mm N) ⟹ pNeg M ∈# too_heavy_clauses N (Some M)›
  by (auto simp: too_heavy_clauses_def simple_clss_finite)

lemma too_heavy_clause_None[simp]: ‹too_heavy_clauses M None = {#}›
  by (auto simp: too_heavy_clauses_def)

lemma atms_of_mm_too_heavy_clauses_le:
  ‹atms_of_mm (too_heavy_clauses M I) ⊆ atms_of_mm M›
  by (auto simp: too_heavy_clauses_def atms_of_ms_def simple_clss_finite dest: simple_clssE)

lemma
  atms_too_heavy_clauses_None:
    ‹atms_of_mm (too_heavy_clauses M None) = {}› and
  atms_too_heavy_clauses_Some:
    ‹atms_of w ⊆ atms_of_mm M  ⟹ distinct_mset w ⟹ ¬tautology w ⟹
      atms_of_mm (too_heavy_clauses M (Some w)) = atms_of_mm M›
proof -
  show ‹atms_of_mm (too_heavy_clauses M None) = {}›
    by (auto simp: too_heavy_clauses_def)
  assume atms: ‹atms_of w ⊆ atms_of_mm M› and
    dist: ‹distinct_mset w› and
    taut: ‹¬tautology w›
  have ‹atms_of_mm (too_heavy_clauses M (Some w)) ⊆ atms_of_mm M›
    by (auto simp: too_heavy_clauses_def atms_of_ms_def simple_clss_finite)
      (auto simp: simple_clss_def)
  let ?w = ‹w + Neg `# {#x ∈# mset_set (atms_of_mm M). x ∉ atms_of w#}›
  have [simp]: ‹inj_on Neg A› for A
    by (auto simp: inj_on_def)
  have dist: ‹distinct_mset ?w›
    using dist
    by (auto simp: distinct_mset_add distinct_image_mset_inj distinct_mset_mset_set uminus_lit_swap
      disjunct_not_in dest: multi_member_split)
  moreover have not_tauto: ‹¬tautology ?w›
    by (auto simp: tautology_union taut uminus_lit_swap dest: multi_member_split)
  ultimately have ‹?w ∈ (simple_clss (atms_of_mm M))›
    using atms by (auto simp: simple_clss_def)
  moreover have ‹ρ ?w ≥ ρ w›
    by (rule ρ_mono) (use dist not_tauto in ‹auto simp: consistent_interp_tuatology_mset_set tautology_decomp›)
  ultimately have ‹pNeg ?w ∈# too_heavy_clauses M (Some w)›
    by (auto simp: too_heavy_clauses_def simple_clss_finite)
  then have ‹atms_of_mm M ⊆ atms_of_mm (too_heavy_clauses M (Some w))›
    by (auto dest!: multi_member_split)
  then show ‹atms_of_mm (too_heavy_clauses M (Some w)) = atms_of_mm M›
    using ‹atms_of_mm (too_heavy_clauses M (Some w)) ⊆ atms_of_mm M› by blast
qed

lemma entails_too_heavy_clauses_too_heavy_clauses: (* \htmllink{ocdcl-entails-conflicting} *)
  assumes
    ‹consistent_interp I› and
    tot: ‹total_over_m I (set_mset (too_heavy_clauses M w))› and
    ‹I ⊨m too_heavy_clauses M w› and
    w: ‹w ≠ None ⟹ atms_of (the w) ⊆ atms_of_mm M›
      ‹w ≠ None ⟹ ¬tautology (the w)›
      ‹w ≠ None ⟹ distinct_mset (the w)›
  shows ‹I ⊨m conflicting_clauses M w›
proof (cases w)
  case None
  have [simp]: ‹{x ∈ simple_clss (atms_of_mm M). tautology x} = {}›
    by (auto dest: simple_clssE)
  show ?thesis
    using None by (auto simp: conflicting_clauses_def true_clss_cls_tautology_iff
      simple_clss_finite)
next
  case w': (Some w')
  have ‹x ∈# mset_set (simple_clss (atms_of_mm M)) ⟹ total_over_set I (atms_of x)› for x
    using tot w atms_too_heavy_clauses_Some[of w' M] unfolding w'
    by (auto simp: total_over_m_def simple_clss_finite total_over_set_alt_def
      dest!: simple_clssE)
  then show ?thesis
    using assms
    by (subst true_cls_mset_def)
      (auto simp: conflicting_clauses_def true_clss_cls_def
        dest!: spec[of _ I])
qed

lemma not_entailed_too_heavy_clauses_ge:
  ‹C ∈ simple_clss (atms_of_mm N) ⟹ ¬ too_heavy_clauses N w ⊨pm pNeg C ⟹ ¬Found (ρ C) ≥ ρ' w›
  using true_clss_cls_in[of ‹pNeg C› ‹set_mset (too_heavy_clauses N w)›]
    too_heavy_clauses_contains_itself
  by (auto simp: too_heavy_clauses_def simple_clss_finite
        image_iff)

lemma conflicting_clss_incl_init_clauses:
  ‹atms_of_mm (conflicting_clauses N w) ⊆ atms_of_mm (N)›
  unfolding conflicting_clauses_def
  apply (auto simp: simple_clss_finite)
  by (auto simp: simple_clss_def atms_of_ms_def split: if_splits)

lemma distinct_mset_mset_conflicting_clss2: ‹distinct_mset_mset (conflicting_clauses N w)›
  unfolding conflicting_clauses_def distinct_mset_set_def
  apply (auto simp: simple_clss_finite)
  by (auto simp: simple_clss_def)

lemma too_heavy_clauses_mono:
  ‹ρ a > ρ (lit_of `# mset M) ⟹ too_heavy_clauses N (Some a) ⊆#
       too_heavy_clauses N (Some (lit_of `# mset M))›
  by (auto simp: too_heavy_clauses_def multiset_filter_mono2
    intro!: multiset_filter_mono image_mset_subseteq_mono)

lemma is_improving_conflicting_clss_update_weight_information: ‹is_improving_int M M' N w ⟹
       conflicting_clauses N w ⊆# conflicting_clauses N (Some (lit_of `# mset M'))›
  using too_heavy_clauses_mono[of M' ‹the w› ‹N›]
  by (cases ‹w›)
    (auto simp: is_improving_int_def  conflicting_clauses_def multiset_filter_mono2
      intro!: image_mset_subseteq_mono
      intro: true_clss_cls_subset
      dest: simple_clssE)

lemma conflicting_clss_update_weight_information_in2:
  assumes ‹is_improving_int M M' N w›
  shows ‹negate_ann_lits M' ∈# conflicting_clauses N (Some (lit_of `# mset M'))›
  using assms apply (auto simp: simple_clss_finite
    conflicting_clauses_def is_improving_int_def)
  by (auto simp: is_improving_int_def conflicting_clauses_def  multiset_filter_mono2 simple_clss_def
       lits_of_def negate_ann_lits_pNeg_lit_of image_iff dest: total_over_m_atms_incl
      intro!: true_clss_cls_in too_heavy_clauses_contains_itself)

lemma atms_of_init_clss_conflicting_clauses'[simp]:
  ‹atms_of_mm N ∪ atms_of_mm (conflicting_clauses N S) = atms_of_mm N›
  using conflicting_clss_incl_init_clauses[of N] by blast

lemma entails_too_heavy_clauses_if_le:
  assumes
    dist: ‹distinct_mset I› and
    cons: ‹consistent_interp (set_mset I)› and
    tot: ‹atms_of I = atms_of_mm N› and
    le: ‹Found (ρ I) < ρ' (Some M')›
  shows
    ‹set_mset I ⊨m too_heavy_clauses N (Some M')›
proof -
  show ‹set_mset I ⊨m too_heavy_clauses N (Some M')›
    unfolding true_cls_mset_def
  proof
    fix C
    assume ‹C ∈# too_heavy_clauses N (Some M')›
    then obtain x where
      [simp]: ‹C = pNeg x› and
      x: ‹x ∈ simple_clss (atms_of_mm N)› and
      we: ‹ρ M' ≤ ρ x›
      unfolding too_heavy_clauses_def
      by (auto simp: simple_clss_finite)
    then have ‹x ≠ I›
      using le by auto
    then have ‹set_mset x ≠ set_mset I›
      using distinct_set_mset_eq_iff[of x I] x dist
      by (auto simp: simple_clss_def)
    then have ‹∃a. ((a ∈# x ∧ a ∉# I) ∨ (a ∈# I ∧ a ∉# x))›
      by auto
    moreover have not_incl: ‹¬set_mset x ⊆ set_mset I›
      using ρ_mono[of I ‹x›] we le distinct_set_mset_eq_iff[of x I] simple_clssE[OF x]
        dist cons
      by auto
    moreover have ‹x ≠ {#}›
      using we le cons dist not_incl by auto
    ultimately obtain L where
      L_x: ‹L ∈# x› and
      ‹L ∉# I›
      by auto
    moreover have ‹atms_of x ⊆ atms_of I›
      using simple_clssE[OF x] tot atm_iff_pos_or_neg_lit[of a I] atm_iff_pos_or_neg_lit[of a x]
      by (auto dest!: multi_member_split)
    ultimately have ‹-L ∈# I›
      using tot simple_clssE[OF x] atm_of_notin_atms_of_iff by auto
    then show ‹set_mset I ⊨ C›
      using L_x by (auto simp: simple_clss_finite pNeg_def dest!: multi_member_split)
  qed
qed

lemma entails_conflicting_clauses_if_le:
  fixes M''
  defines ‹M' ≡ lit_of `# mset M''›
  assumes
    dist: ‹distinct_mset I› and
    cons: ‹consistent_interp (set_mset I)› and
    tot: ‹atms_of I = atms_of_mm N› and
    le: ‹Found (ρ I) < ρ' (Some M')› and
    ‹is_improving_int M M'' N w›
  shows
    ‹set_mset I ⊨m conflicting_clauses N (Some (lit_of `# mset M''))›
  apply (rule entails_too_heavy_clauses_too_heavy_clauses[OF cons])
  subgoal
    using assms unfolding is_improving_int_def
    by (auto simp: total_over_m_alt_def M'_def atms_of_def lit_in_set_iff_atm
          atms_too_heavy_clauses_Some eq_commute[of _ ‹atms_of_mm N›]
        dest: multi_member_split dest!: simple_clssE)
  by (use assms  entails_too_heavy_clauses_if_le[OF assms(2-5)] in
    ‹auto simp: M'_def lits_of_def image_image is_improving_int_def dest!: simple_clssE›)

end


locale conflict_driven_clause_learning⇩W_optimal_weight =
  conflict_driven_clause_learning⇩W
    state_eq
    state
    ― ‹functions for the state:›
      ― ‹access functions:›
    trail init_clss learned_clss conflicting
      ― ‹changing state:›
    cons_trail tl_trail add_learned_cls remove_cls
    update_conflicting
      ― ‹get state:›
    init_state +
  ocdcl_weight ρ
  for
    state_eq :: ‹'st ⇒ 'st ⇒ bool› (infix ‹∼› 50) and
    state :: "'st ⇒ ('v, 'v clause) ann_lits × 'v clauses × 'v clauses × 'v clause option ×
      'v clause option × 'b" and
    trail :: ‹'st ⇒ ('v, 'v clause) ann_lits› and
    init_clss :: ‹'st ⇒ 'v clauses› and
    learned_clss :: ‹'st ⇒ 'v clauses› and
    conflicting :: ‹'st ⇒ 'v clause option› and

    cons_trail :: ‹('v, 'v clause) ann_lit ⇒ 'st ⇒ 'st› and
    tl_trail :: ‹'st ⇒ 'st› and
    add_learned_cls :: ‹'v clause ⇒ 'st ⇒ 'st› and
    remove_cls :: ‹'v clause ⇒ 'st ⇒ 'st› and
    update_conflicting :: ‹'v clause option ⇒ 'st ⇒ 'st› and
    init_state :: ‹'v clauses ⇒ 'st› and
    ρ :: ‹'v clause ⇒ 'a :: {linorder}›  +
  fixes
    update_additional_info :: ‹'v clause option × 'b ⇒ 'st ⇒ 'st›
  assumes
    update_additional_info:
      ‹state S = (M, N, U, C, K) ⟹ state (update_additional_info K' S) = (M, N, U, C, K')› and
    weight_init_state:
      ‹⋀N :: 'v clauses. fst (additional_info (init_state N)) = None›
begin

definition update_weight_information :: ‹('v, 'v clause) ann_lits ⇒ 'st ⇒ 'st› where
  ‹update_weight_information M S =
    update_additional_info (Some (lit_of `# mset M), snd (additional_info S)) S›

lemma
  trail_update_additional_info[simp]: ‹trail (update_additional_info w S) = trail S› and
  init_clss_update_additional_info[simp]:
    ‹init_clss (update_additional_info w S) = init_clss S› and
  learned_clss_update_additional_info[simp]:
    ‹learned_clss (update_additional_info w S) = learned_clss S› and
  backtrack_lvl_update_additional_info[simp]:
    ‹backtrack_lvl (update_additional_info w S) = backtrack_lvl S› and
  conflicting_update_additional_info[simp]:
    ‹conflicting (update_additional_info w S) = conflicting S› and
  clauses_update_additional_info[simp]:
    ‹clauses (update_additional_info w S) = clauses S›
  using update_additional_info[of S] unfolding clauses_def
  by (subst (asm) state_prop; subst (asm) state_prop; auto; fail)+

lemma
  trail_update_weight_information[simp]:
    ‹trail (update_weight_information w S) = trail S› and
  init_clss_update_weight_information[simp]:
    ‹init_clss (update_weight_information w S) = init_clss S› and
  learned_clss_update_weight_information[simp]:
    ‹learned_clss (update_weight_information w S) = learned_clss S› and
  backtrack_lvl_update_weight_information[simp]:
    ‹backtrack_lvl (update_weight_information w S) = backtrack_lvl S› and
  conflicting_update_weight_information[simp]:
    ‹conflicting (update_weight_information w S) = conflicting S› and
  clauses_update_weight_information[simp]:
    ‹clauses (update_weight_information w S) = clauses S›
  using update_additional_info[of S] unfolding update_weight_information_def by auto

definition weight :: ‹'st ⇒ 'v clause option› where
  ‹weight S = fst (additional_info S)›

lemma
  additional_info_update_additional_info[simp]:
  ‹additional_info (update_additional_info w S) = w›
  unfolding additional_info_def using update_additional_info[of S]
  by (cases ‹state S›; auto; fail)+

lemma
  weight_cons_trail2[simp]: ‹weight (cons_trail L S) = weight S› and
  clss_tl_trail2[simp]: ‹weight (tl_trail S) = weight S› and
  weight_add_learned_cls_unfolded:
    ‹weight (add_learned_cls U S) = weight S›
    and
  weight_update_conflicting2[simp]: ‹weight (update_conflicting D S) = weight S› and
  weight_remove_cls2[simp]:
    ‹weight (remove_cls C S) = weight S› and
  weight_add_learned_cls2[simp]:
    ‹weight (add_learned_cls C S) = weight S› and
  weight_update_weight_information2[simp]:
    ‹weight (update_weight_information M S) = Some (lit_of `# mset M)›
  by (auto simp: update_weight_information_def weight_def)


sublocale conflict_driven_clause_learning_with_adding_init_clause_bnb⇩W_no_state
  where
    state = state and
    trail = trail and
    init_clss = init_clss and
    learned_clss = learned_clss and
    conflicting = conflicting and
    cons_trail = cons_trail and
    tl_trail = tl_trail and
    add_learned_cls = add_learned_cls and
    remove_cls = remove_cls and
    update_conflicting = update_conflicting and
    init_state = init_state and
    weight = weight and
    update_weight_information = update_weight_information and
    is_improving_int = is_improving_int and
    conflicting_clauses = conflicting_clauses
  by unfold_locales

lemma state_additional_info':
  ‹state S = (trail S, init_clss S, learned_clss S, conflicting S, weight S, additional_info' S)›
  unfolding additional_info'_def by (cases ‹state S›; auto simp: state_prop weight_def)

lemma state_update_weight_information:
  ‹state S = (M, N, U, C, w, other) ⟹
    ∃w'. state (update_weight_information T S) = (M, N, U, C, w', other)›
  unfolding update_weight_information_def by (cases ‹state S›; auto simp: state_prop weight_def)

lemma atms_of_init_clss_conflicting_clauses[simp]:
  ‹atms_of_mm (init_clss S) ∪ atms_of_mm (conflicting_clss S) = atms_of_mm (init_clss S)›
  using conflicting_clss_incl_init_clauses[of ‹(init_clss S)›] unfolding conflicting_clss_def by blast

lemma lit_of_trail_in_simple_clss: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S) ⟹
         lit_of `# mset (trail S) ∈ simple_clss (atms_of_mm (init_clss S))›
  unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def abs_state_def
  cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def cdcl⇩W_restart_mset.no_strange_atm_def
  by (auto simp: simple_clss_def cdcl⇩W_restart_mset_state atms_of_def pNeg_def lits_of_def
      dest: no_dup_not_tautology no_dup_distinct)

lemma pNeg_lit_of_trail_in_simple_clss: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S) ⟹
         pNeg (lit_of `# mset (trail S)) ∈ simple_clss (atms_of_mm (init_clss S))›
  unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def abs_state_def
  cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def cdcl⇩W_restart_mset.no_strange_atm_def
  by (auto simp: simple_clss_def cdcl⇩W_restart_mset_state atms_of_def pNeg_def lits_of_def
      dest: no_dup_not_tautology_uminus no_dup_distinct_uminus)

lemma conflict_clss_update_weight_no_alien:
  ‹atms_of_mm (conflicting_clss (update_weight_information M S))
    ⊆ atms_of_mm (init_clss S)›
  by (auto simp: conflicting_clss_def conflicting_clauses_def atms_of_ms_def
      cdcl⇩W_restart_mset_state simple_clss_finite
    dest: simple_clssE)

sublocale state⇩W_no_state
  where
    state = state and
    trail = trail and
    init_clss = init_clss and
    learned_clss = learned_clss and
    conflicting = conflicting and
    cons_trail = cons_trail and
    tl_trail = tl_trail and
    add_learned_cls = add_learned_cls and
    remove_cls = remove_cls and
    update_conflicting = update_conflicting and
    init_state = init_state
  by unfold_locales

sublocale state⇩W_no_state
  where
    state_eq = state_eq and
    state = state and
    trail = trail and
    init_clss = init_clss and
    learned_clss = learned_clss and
    conflicting = conflicting and
    cons_trail = cons_trail and
    tl_trail = tl_trail and
    add_learned_cls = add_learned_cls and
    remove_cls = remove_cls and
    update_conflicting = update_conflicting and
    init_state = init_state
  by unfold_locales

sublocale conflict_driven_clause_learning⇩W
  where
    state_eq = state_eq and
    state = state and
    trail = trail and
    init_clss = init_clss and
    learned_clss = learned_clss and
    conflicting = conflicting and
    cons_trail = cons_trail and
    tl_trail = tl_trail and
    add_learned_cls = add_learned_cls and
    remove_cls = remove_cls and
    update_conflicting = update_conflicting and
    init_state = init_state
  by unfold_locales

lemma is_improving_conflicting_clss_update_weight_information': ‹is_improving M M' S ⟹
       conflicting_clss S ⊆# conflicting_clss (update_weight_information M' S)›
  using is_improving_conflicting_clss_update_weight_information[of M M' ‹init_clss S› ‹weight S›]
  unfolding conflicting_clss_def
  by auto

lemma conflicting_clss_update_weight_information_in2':
  assumes ‹is_improving M M' S›
  shows ‹negate_ann_lits M' ∈# conflicting_clss (update_weight_information M' S)›
  using conflicting_clss_update_weight_information_in2[of M M' ‹init_clss S› ‹weight S›] assms
  unfolding conflicting_clss_def
  by auto

sublocale conflict_driven_clause_learning_with_adding_init_clause_bnb⇩W_ops
  where
    state = state and
    trail = trail and
    init_clss = init_clss and
    learned_clss = learned_clss and
    conflicting = conflicting and
    cons_trail = cons_trail and
    tl_trail = tl_trail and
    add_learned_cls = add_learned_cls and
    remove_cls = remove_cls and
    update_conflicting = update_conflicting and
    init_state = init_state and
    weight = weight and
    update_weight_information = update_weight_information and
    is_improving_int = is_improving_int and
    conflicting_clauses = conflicting_clauses
  apply unfold_locales
  subgoal by (rule state_additional_info')
  subgoal by (rule state_update_weight_information)
  subgoal unfolding conflicting_clss_def by (rule conflicting_clss_incl_init_clauses)
  subgoal unfolding conflicting_clss_def by (rule distinct_mset_mset_conflicting_clss2)
  subgoal by (rule is_improving_conflicting_clss_update_weight_information')
  subgoal by (rule conflicting_clss_update_weight_information_in2'; assumption)
  done

lemma wf_cdcl_bnb_fixed:
   ‹wf {(T, S). cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S) ∧ cdcl_bnb S T
      ∧ init_clss S = N}›
  apply (rule wf_cdcl_bnb[of N id ‹{(I', I). I' ≠ None ∧
     (the I') ∈ simple_clss (atms_of_mm N) ∧ (ρ' I', ρ' I) ∈ {(j, i). j < i}}›])
  subgoal for S T
    by (cases ‹weight S›; cases ‹weight T›)
      (auto simp: improvep.simps is_improving_int_def split: enat.splits)
  subgoal
    apply (rule wf_finite_segments)
    subgoal by (auto simp: irrefl_def)
    subgoal
      apply (auto simp: irrefl_def trans_def intro: less_trans[of ‹Found _› ‹Found _›])
      apply (rule less_trans[of ‹Found _› ‹Found _›])
      apply auto
      done
    subgoal for x
      by (subgoal_tac ‹{y. (y, x)
         ∈ {(I', I). I' ≠ None ∧ the I' ∈ simple_clss (atms_of_mm N) ∧
            (ρ' I', ρ' I) ∈ {(j, i). j < i}}} =
        Some ` {y. (y, x) ∈ {(I', I).
             I' ∈ simple_clss (atms_of_mm N) ∧
            (ρ' (Some I'), ρ' I) ∈ {(j, i). j < i}}}›)
       (auto simp: finite_image_iff intro: finite_subset[OF _ simple_clss_finite[of ‹atms_of_mm N›]])
    done
  done

lemma wf_cdcl_bnb2:
  ‹wf {(T, S). cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)
     ∧ cdcl_bnb S T}›
  by (subst wf_cdcl_bnb_fixed_iff[symmetric]) (intro allI, rule wf_cdcl_bnb_fixed)

lemma can_always_improve:
  assumes
    ent: ‹trail S ⊨asm clauses S› and
    total: ‹total_over_m (lits_of_l (trail S)) (set_mset (clauses S))› and
    n_s: ‹no_step conflict_opt S› and
    confl[simp]: ‹conflicting S = None› and
    all_struct: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
   shows ‹Ex (improvep S)›
proof -
  have H: ‹(lit_of `# mset (trail S)) ∈# mset_set (simple_clss (atms_of_mm (init_clss S)))›
    ‹(lit_of `# mset (trail S)) ∈ simple_clss (atms_of_mm (init_clss S))›
    ‹no_dup (trail S)›
    apply (subst finite_set_mset_mset_set[OF simple_clss_finite])
    using all_struct by (auto simp: simple_clss_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
        no_strange_atm_def atms_of_def lits_of_def image_image
        cdcl⇩W_M_level_inv_def clauses_def
      dest: no_dup_not_tautology no_dup_distinct)
  then have le: ‹Found (ρ (lit_of `# mset (trail S))) < ρ' (weight S)›
    using n_s total
    by (auto simp: conflict_opt.simps conflicting_clss_def lits_of_def
         conflicting_clauses_def clauses_def negate_ann_lits_pNeg_lit_of simple_clss_finite
       dest: not_entailed_too_heavy_clauses_ge)
  have tr: ‹trail S ⊨asm init_clss S›
    using ent by (auto simp: clauses_def)
  have tot': ‹total_over_m (lits_of_l (trail S)) (set_mset (init_clss S))›
    using total all_struct by (auto simp: total_over_m_def total_over_set_def
       cdcl⇩W_all_struct_inv_def clauses_def no_strange_atm_def)
  have M': ‹ρ (lit_of `# mset M') = ρ (lit_of `# mset (trail S))›
      if ‹total_over_m (lits_of_l M') (set_mset (init_clss S))› and
        incl: ‹mset (trail S) ⊆# mset M'› and
        ‹lit_of `# mset M' ∈ simple_clss (atms_of_mm (init_clss S))›
      for M'
    proof -
      have [simp]: ‹lits_of_l M' = set_mset (lit_of `# mset M')›
        by (auto simp: lits_of_def)
      obtain A where A: ‹mset M' = A + mset (trail S)›
        using incl by (auto simp: mset_subset_eq_exists_conv)
      have M': ‹lits_of_l M' = lit_of ` set_mset A ∪ lits_of_l (trail S)›
        unfolding lits_of_def
        by (metis A image_Un set_mset_mset set_mset_union)
      have ‹mset M' = mset (trail S)›
        using that tot' total unfolding A total_over_m_alt_def
        apply (case_tac A)
        apply (auto simp: A simple_clss_def distinct_mset_add M' image_Un
            tautology_union mset_inter_empty_set_mset atms_of_def atms_of_s_def
            atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set image_image
            tautology_add_mset)
        by (metis (no_types, lifting) atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set
           subsetCE lits_of_def)
      then show ?thesis
        using total by auto
    qed
  have ‹is_improving (trail S) (trail S) S›
    if ‹Found (ρ (lit_of `# mset (trail S))) < ρ' (weight S)›
    using that total H confl tr tot' M' unfolding is_improving_int_def lits_of_def by fast
  then show ‹Ex (improvep S)›
    using improvep.intros[of S ‹trail S› ‹update_weight_information (trail S) S›] le confl by fast
qed

lemma no_step_cdcl_bnb_stgy_empty_conflict2:
  assumes
    n_s: ‹no_step cdcl_bnb S› and
    all_struct: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)› and
    stgy_inv: ‹cdcl_bnb_stgy_inv S›
  shows ‹conflicting S = Some {#}›
  by (rule no_step_cdcl_bnb_stgy_empty_conflict[OF can_always_improve assms])


lemma cdcl_bnb_larger_still_larger:
  assumes
    ‹cdcl_bnb S T›
  shows ‹ρ' (weight S) ≥ ρ' (weight T)›
  using assms apply (cases rule: cdcl_bnb.cases)
  by (auto simp: improvep.simps is_improving_int_def conflict_opt.simps ocdcl⇩W_o.simps
      cdcl_bnb_bj.simps skip.simps resolve.simps obacktrack.simps elim: rulesE)

lemma obacktrack_model_still_model:
  assumes
    ‹obacktrack S T› and
    all_struct: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)› and
    ent: ‹set_mset I ⊨sm clauses S› ‹set_mset I ⊨sm conflicting_clss S› and
    dist: ‹distinct_mset I› and
    cons: ‹consistent_interp (set_mset I)› and
    tot: ‹atms_of I = atms_of_mm (init_clss S)› and
    opt_struct: ‹cdcl_bnb_struct_invs S› and
    le: ‹Found (ρ I) < ρ' (weight T)›
  shows
    ‹set_mset I ⊨sm clauses T ∧ set_mset I ⊨sm conflicting_clss T›
  using assms(1)
proof (cases rule: obacktrack.cases)
  case (obacktrack_rule L D K M1 M2 D' i) note confl = this(1) and DD' = this(7) and
    clss_L_D' = this(8) and T = this(9)
  have H: ‹total_over_m I (set_mset (clauses S + conflicting_clss S) ∪ {add_mset L D'}) ⟹
      consistent_interp I ⟹
      I ⊨sm clauses S + conflicting_clss S ⟹ I ⊨ add_mset L D'› for I
    using clss_L_D'
    unfolding true_clss_cls_def
    by blast
  have alien: ‹cdcl⇩W_restart_mset.no_strange_atm (abs_state S)›
    using all_struct unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
    by fast+
  have ‹total_over_m (set_mset I) (set_mset (init_clss S))›
    using tot[symmetric]
    by (auto simp: total_over_m_def total_over_set_def atm_iff_pos_or_neg_lit)

  then have 1: ‹total_over_m (set_mset I) (set_mset (clauses S + conflicting_clss S) ∪
       {add_mset L D'})›
    using alien T confl tot DD' opt_struct
    unfolding cdcl⇩W_restart_mset.no_strange_atm_def total_over_m_def total_over_set_def
    apply (auto simp: cdcl⇩W_restart_mset_state abs_state_def atms_of_def clauses_def
      cdcl_bnb_struct_invs_def dest: multi_member_split)
    by blast
  have 2: ‹set_mset I ⊨sm conflicting_clss S›
    using tot cons ent(2) by auto
  have ‹set_mset I ⊨ add_mset L D'›
    using H[OF 1 cons] 2 ent by auto
  then show ?thesis
    using ent obacktrack_rule 2 by auto
qed


lemma entails_conflicting_clauses_if_le':
  fixes M''
  defines ‹M' ≡ lit_of `# mset M''›
  assumes
    dist: ‹distinct_mset I› and
    cons: ‹consistent_interp (set_mset I)› and
    tot: ‹atms_of I = atms_of_mm (init_clss S)› and
    le: ‹Found (ρ I) < ρ' (Some M')› and
    ‹is_improving M M'' S› and
    ‹N = init_clss S›
  shows
    ‹set_mset I ⊨m conflicting_clauses N (weight (update_weight_information M'' S))›
  using entails_conflicting_clauses_if_le[OF assms(2-6)[unfolded M'_def]] assms(7)
  unfolding conflicting_clss_def by auto

lemma improve_model_still_model:
  assumes
    ‹improvep S T› and
    all_struct: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)› and
    ent: ‹set_mset I ⊨sm clauses S›  ‹set_mset I ⊨sm conflicting_clss S› and
    dist: ‹distinct_mset I› and
    cons: ‹consistent_interp (set_mset I)› and
    tot: ‹atms_of I = atms_of_mm (init_clss S)› and
    opt_struct: ‹cdcl_bnb_struct_invs S› and
    le: ‹Found (ρ I) < ρ' (weight T)›
  shows
    ‹set_mset I ⊨sm clauses T ∧ set_mset I ⊨sm conflicting_clss T›
  using assms(1)
proof (cases rule: improvep.cases)
  case (improve_rule M') note imp = this(1) and confl = this(2) and T = this(3)
  have alien: ‹cdcl⇩W_restart_mset.no_strange_atm (abs_state S)› and
    lev: ‹cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv (abs_state S)›
    using all_struct unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
    by fast+
  then have atm_trail: ‹atms_of (lit_of `# mset (trail S)) ⊆ atms_of_mm (init_clss S)›
    using alien by (auto simp: no_strange_atm_def lits_of_def atms_of_def)
  have dist2: ‹distinct_mset (lit_of `# mset (trail S))› and
    taut2: ‹¬ tautology (lit_of `# mset (trail S))›
    using lev unfolding cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
    by (auto dest: no_dup_distinct no_dup_not_tautology)
  have tot2: ‹total_over_m (set_mset I) (set_mset (init_clss S))›
    using tot[symmetric]
    by (auto simp: total_over_m_def total_over_set_def atm_iff_pos_or_neg_lit)
  have atm_trail: ‹atms_of (lit_of `# mset M') ⊆ atms_of_mm (init_clss S)› and
    dist2: ‹distinct_mset (lit_of `# mset M')› and
    taut2: ‹¬ tautology (lit_of `# mset M')›
    using imp by (auto simp: no_strange_atm_def lits_of_def atms_of_def is_improving_int_def
      simple_clss_def)

  have tot2: ‹total_over_m (set_mset I) (set_mset (init_clss S))›
    using tot[symmetric]
    by (auto simp: total_over_m_def total_over_set_def atm_iff_pos_or_neg_lit)
  have
      ‹set_mset I ⊨m conflicting_clauses (init_clss S) (weight (update_weight_information M' S))›
    apply (rule entails_conflicting_clauses_if_le'[unfolded conflicting_clss_def])
    using T dist cons tot le imp by (auto intro!: )
  then have ‹set_mset I ⊨m conflicting_clss (update_weight_information M' S)›
    by (auto simp: update_weight_information_def conflicting_clss_def)
  then show ?thesis
    using ent improve_rule T by auto
qed

lemma cdcl_bnb_still_model:
  assumes
    ‹cdcl_bnb S T› and
    all_struct: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)› and
    ent: ‹set_mset I ⊨sm clauses S› ‹set_mset I ⊨sm conflicting_clss S› and
    dist: ‹distinct_mset I› and
    cons: ‹consistent_interp (set_mset I)› and
    tot: ‹atms_of I = atms_of_mm (init_clss S)› and
    opt_struct: ‹cdcl_bnb_struct_invs S›
  shows
    ‹(set_mset I ⊨sm clauses T ∧ set_mset I ⊨sm conflicting_clss T) ∨ Found (ρ I) ≥ ρ' (weight T)›
  using assms
proof (cases rule: cdcl_bnb.cases)
  case cdcl_improve
  from improve_model_still_model[OF this all_struct ent dist cons tot opt_struct]
  show ?thesis
    by (auto simp: improvep.simps)
next
  case cdcl_other'
  then show ?thesis
  proof (induction rule: ocdcl⇩W_o_all_rules_induct)
    case (backtrack T)
    from obacktrack_model_still_model[OF this all_struct ent dist cons tot opt_struct]
    show ?case
      by auto
  qed (use ent in ‹auto elim: rulesE›)
qed (auto simp: conflict_opt.simps elim: rulesE)

lemma rtranclp_cdcl_bnb_still_model:
  assumes
    st: ‹cdcl_bnb⇧*⇧* S T› and
    all_struct: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)› and
    ent: ‹(set_mset I ⊨sm clauses S ∧ set_mset I ⊨sm conflicting_clss S) ∨ Found (ρ I) ≥ ρ' (weight S)› and
    dist: ‹distinct_mset I› and
    cons: ‹consistent_interp (set_mset I)› and
    tot: ‹atms_of I = atms_of_mm (init_clss S)› and
    opt_struct: ‹cdcl_bnb_struct_invs S›
  shows
    ‹(set_mset I ⊨sm clauses T ∧ set_mset I ⊨sm conflicting_clss T) ∨ Found (ρ I) ≥ ρ' (weight T)›
  using st
proof (induction rule: rtranclp_induct)
  case base
  then show ?case
    using ent by auto
next
  case (step T U) note star = this(1) and st = this(2) and IH = this(3)
  have 1: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state T)›
    using rtranclp_cdcl_bnb_stgy_all_struct_inv[OF star all_struct] .

  have 2: ‹cdcl_bnb_struct_invs T›
    using rtranclp_cdcl_bnb_cdcl_bnb_struct_invs[OF star opt_struct] .
  have 3: ‹atms_of I = atms_of_mm (init_clss T)›
    using tot rtranclp_cdcl_bnb_no_more_init_clss[OF star] by auto
  show ?case
    using cdcl_bnb_still_model[OF st 1 _ _ dist cons 3 2] IH
      cdcl_bnb_larger_still_larger[OF st]
    using dual_order.trans by blast
qed

lemma full_cdcl_bnb_stgy_larger_or_equal_weight:
  assumes
    st: ‹full cdcl_bnb_stgy S T› and
    all_struct: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)› and
    ent: ‹(set_mset I ⊨sm clauses S ∧ set_mset I ⊨sm conflicting_clss S) ∨ Found (ρ I) ≥ ρ' (weight S)› and
    dist: ‹distinct_mset I› and
    cons: ‹consistent_interp (set_mset I)› and
    tot: ‹atms_of I = atms_of_mm (init_clss S)› and
    opt_struct: ‹cdcl_bnb_struct_invs S› and
    stgy_inv: ‹cdcl_bnb_stgy_inv S›
  shows
    ‹Found (ρ I) ≥ ρ' (weight T)› and
    ‹unsatisfiable (set_mset (clauses T + conflicting_clss T))›
proof -
  have ns: ‹no_step cdcl_bnb_stgy T› and
    st: ‹cdcl_bnb_stgy⇧*⇧* S T› and
    st': ‹cdcl_bnb⇧*⇧* S T›
    using st unfolding full_def by (auto intro: rtranclp_cdcl_bnb_stgy_cdcl_bnb)
  have ns': ‹no_step cdcl_bnb T›
    by (meson cdcl_bnb.cases cdcl_bnb_stgy.simps no_confl_prop_impr.elims(3) ns)
  have struct_T: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state T)›
    using rtranclp_cdcl_bnb_stgy_all_struct_inv[OF st' all_struct] .
  have stgy_T: ‹cdcl_bnb_stgy_inv T›
    using rtranclp_cdcl_bnb_stgy_stgy_inv[OF st all_struct stgy_inv] .
  have confl: ‹conflicting T = Some {#}›
    using no_step_cdcl_bnb_stgy_empty_conflict2[OF ns' struct_T stgy_T] .

  have ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clause (abs_state T)› and
    alien: ‹cdcl⇩W_restart_mset.no_strange_atm (abs_state T)›
    using struct_T unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def by fast+
  then have ent': ‹set_mset (clauses T + conflicting_clss T) ⊨p {#}›
    using confl unfolding cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def
    by auto
  have atms_eq: ‹atms_of I ∪ atms_of_mm (conflicting_clss T) = atms_of_mm (init_clss T)›
    using tot[symmetric] atms_of_conflicting_clss[of T] alien
    unfolding rtranclp_cdcl_bnb_no_more_init_clss[OF st'] cdcl⇩W_restart_mset.no_strange_atm_def
    by (auto simp: clauses_def total_over_m_def total_over_set_def atm_iff_pos_or_neg_lit
      abs_state_def cdcl⇩W_restart_mset_state)

  have ‹¬ (set_mset I ⊨sm clauses T + conflicting_clss T)›
  proof
    assume ent'': ‹set_mset I ⊨sm clauses T + conflicting_clss T›
    moreover have ‹total_over_m (set_mset I) (set_mset (clauses T + conflicting_clss T))›
      using tot[symmetric] atms_of_conflicting_clss[of T] alien
      unfolding rtranclp_cdcl_bnb_no_more_init_clss[OF st'] cdcl⇩W_restart_mset.no_strange_atm_def
      by (auto simp: clauses_def total_over_m_def total_over_set_def atm_iff_pos_or_neg_lit
              abs_state_def cdcl⇩W_restart_mset_state atms_eq)
    then show False
      using ent' cons ent'' unfolding true_clss_cls_def by auto
  qed
  then show ‹ρ' (weight T) ≤ Found (ρ I)›
    using rtranclp_cdcl_bnb_still_model[OF st' all_struct ent dist cons tot opt_struct]
    by auto

  show ‹unsatisfiable (set_mset (clauses T + conflicting_clss T))›
  proof
    assume ‹satisfiable (set_mset (clauses T + conflicting_clss T))›
    then obtain I where
      ent'': ‹I ⊨sm clauses T + conflicting_clss T› and
      tot: ‹total_over_m I (set_mset (clauses T + conflicting_clss T))› and
      ‹consistent_interp I›
      unfolding satisfiable_def
      by blast
    then show ‹False›
      using ent' cons unfolding true_clss_cls_def by auto
  qed
qed


lemma full_cdcl_bnb_stgy_unsat2:
  assumes
    st: ‹full cdcl_bnb_stgy S T› and
    all_struct: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)› and
    opt_struct: ‹cdcl_bnb_struct_invs S› and
    stgy_inv: ‹cdcl_bnb_stgy_inv S›
  shows
    ‹unsatisfiable (set_mset (clauses T + conflicting_clss T))›
proof -
  have ns: ‹no_step cdcl_bnb_stgy T› and
    st: ‹cdcl_bnb_stgy⇧*⇧* S T› and
    st': ‹cdcl_bnb⇧*⇧* S T›
    using st unfolding full_def by (auto intro: rtranclp_cdcl_bnb_stgy_cdcl_bnb)
  have ns': ‹no_step cdcl_bnb T›
    by (meson cdcl_bnb.cases cdcl_bnb_stgy.simps no_confl_prop_impr.elims(3) ns)
  have struct_T: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state T)›
    using rtranclp_cdcl_bnb_stgy_all_struct_inv[OF st' all_struct] .
  have stgy_T: ‹cdcl_bnb_stgy_inv T›
    using rtranclp_cdcl_bnb_stgy_stgy_inv[OF st all_struct stgy_inv] .
  have confl: ‹conflicting T = Some {#}›
    using no_step_cdcl_bnb_stgy_empty_conflict2[OF ns' struct_T stgy_T] .

  have ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clause (abs_state T)› and
    alien: ‹cdcl⇩W_restart_mset.no_strange_atm (abs_state T)›
    using struct_T unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def by fast+
  then have ent': ‹set_mset (clauses T + conflicting_clss T) ⊨p {#}›
    using confl unfolding cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def
    by auto

  show ‹unsatisfiable (set_mset (clauses T + conflicting_clss T))›
  proof
    assume ‹satisfiable (set_mset (clauses T + conflicting_clss T))›
    then obtain I where
      ent'': ‹I ⊨sm clauses T + conflicting_clss T› and
      tot: ‹total_over_m I (set_mset (clauses T + conflicting_clss T))› and
      ‹consistent_interp I›
      unfolding satisfiable_def
      by blast
    then show ‹False›
      using ent' unfolding true_clss_cls_def by auto
  qed
qed

lemma weight_init_state2[simp]: ‹weight (init_state S) = None› and
  conflicting_clss_init_state[simp]:
    ‹conflicting_clss (init_state N) = {#}›
  unfolding weight_def conflicting_clss_def conflicting_clauses_def
  by (auto simp: weight_init_state true_clss_cls_tautology_iff simple_clss_finite
    filter_mset_empty_conv mset_set_empty_iff dest: simple_clssE)

text ‹First part of \cwref{theo:prop:cdclmmcorrect}{Theorem 2.15.6}›
lemma full_cdcl_bnb_stgy_no_conflicting_clause_unsat:
  assumes
    st: ‹full cdcl_bnb_stgy S T› and
    all_struct: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)› and
    opt_struct: ‹cdcl_bnb_struct_invs S› and
    stgy_inv: ‹cdcl_bnb_stgy_inv S› and
    [simp]: ‹weight T = None› and
    ent: ‹cdcl⇩W_learned_clauses_entailed_by_init S›
  shows ‹unsatisfiable (set_mset (init_clss S))›
proof -
  have ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (abs_state S)› and
    ‹conflicting_clss T = {#}›
    using ent by (auto simp: cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init_def
      cdcl⇩W_learned_clauses_entailed_by_init_def abs_state_def cdcl⇩W_restart_mset_state
      conflicting_clss_def conflicting_clauses_def true_clss_cls_tautology_iff simple_clss_finite
      filter_mset_empty_conv mset_set_empty_iff dest: simple_clssE)
  then show ?thesis
    using full_cdcl_bnb_stgy_no_conflicting_clss_unsat[OF _ st all_struct
     stgy_inv] by (auto simp: can_always_improve)
qed

definition annotation_is_model where
  ‹annotation_is_model S ⟷
     (weight S ≠ None ⟶ (set_mset (the (weight S)) ⊨sm init_clss S ∧
       consistent_interp (set_mset (the (weight S))) ∧
       atms_of (the (weight S)) ⊆ atms_of_mm (init_clss S) ∧
       total_over_m (set_mset (the (weight S))) (set_mset (init_clss S)) ∧
       distinct_mset (the (weight S))))›

lemma cdcl_bnb_annotation_is_model:
  assumes
    ‹cdcl_bnb S T› and
    ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)› and
    ‹annotation_is_model S›
  shows ‹annotation_is_model T›
proof -
  have [simp]: ‹atms_of (lit_of `# mset M) = atm_of ` lit_of ` set M› for M
    by (auto simp: atms_of_def)
  have ‹consistent_interp (lits_of_l (trail S)) ∧
       atm_of ` (lits_of_l (trail S)) ⊆ atms_of_mm (init_clss S) ∧
       distinct_mset (lit_of `# mset (trail S))›
    using assms(2) by (auto simp: cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
      abs_state_def cdcl⇩W_restart_mset_state cdcl⇩W_restart_mset.no_strange_atm_def
      cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
      dest: no_dup_distinct)
  with assms(1,3)
  show ?thesis
    apply (cases rule: cdcl_bnb.cases)
    subgoal
      by (auto simp: conflict.simps annotation_is_model_def)
    subgoal
      by (auto simp: propagate.simps annotation_is_model_def)
    subgoal
      by (force simp: annotation_is_model_def true_annots_true_cls lits_of_def
             improvep.simps is_improving_int_def image_Un image_image simple_clss_def
             consistent_interp_tuatology_mset_set
           dest!: consistent_interp_unionD intro: distinct_mset_union2)
    subgoal
      by (auto simp: annotation_is_model_def conflict_opt.simps)
    subgoal
      by (auto simp: annotation_is_model_def
              ocdcl⇩W_o.simps cdcl_bnb_bj.simps obacktrack.simps
              skip.simps resolve.simps decide.simps)
    done
qed

lemma rtranclp_cdcl_bnb_annotation_is_model:
  ‹cdcl_bnb⇧*⇧* S T ⟹ cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S) ⟹
     annotation_is_model S ⟹ annotation_is_model T›
  by (induction rule: rtranclp_induct)
    (auto simp: cdcl_bnb_annotation_is_model rtranclp_cdcl_bnb_stgy_all_struct_inv)


text ‹\cwref{theo:prop:cdclmmcorrect}{Theorem 2.15.6}›
theorem full_cdcl_bnb_stgy_no_conflicting_clause_from_init_state:
  assumes
    st: ‹full cdcl_bnb_stgy (init_state N) T› and
    dist: ‹distinct_mset_mset N›
  shows
    ‹weight T = None ⟹ unsatisfiable (set_mset N)› (is ‹?B ⟹ ?A›) and
    ‹weight T ≠ None ⟹ consistent_interp (set_mset (the (weight T))) ∧
       atms_of (the (weight T)) ⊆ atms_of_mm N ∧ set_mset (the (weight T)) ⊨sm N ∧
       total_over_m (set_mset (the (weight T))) (set_mset N) ∧
       distinct_mset (the (weight T))› and
    ‹distinct_mset I ⟹ consistent_interp (set_mset I) ⟹ atms_of I = atms_of_mm N ⟹
      set_mset I ⊨sm N ⟹ Found (ρ I) ≥ ρ' (weight T)›
proof -
  let ?S = ‹init_state N›
  have ‹distinct_mset C› if ‹C ∈# N› for C
    using dist that by (auto simp: distinct_mset_set_def dest: multi_member_split)
  then have dist: ‹distinct_mset_mset N›
    by (auto simp: distinct_mset_set_def)
  then have [simp]: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv ([], N, {#}, None)›
    unfolding init_state.simps[symmetric]
    by (auto simp: cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def)
  moreover have [iff]: ‹cdcl_bnb_struct_invs ?S› and [simp]: ‹cdcl_bnb_stgy_inv ?S›
    by (auto simp: cdcl_bnb_struct_invs_def conflict_is_false_with_level_def cdcl_bnb_stgy_inv_def)
  moreover have ent: ‹cdcl⇩W_learned_clauses_entailed_by_init ?S›
    by (auto simp: cdcl⇩W_learned_clauses_entailed_by_init_def)
  moreover have [simp]: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state (init_state N))›
    unfolding CDCL_W_Abstract_State.init_state.simps abs_state_def
    by auto
  ultimately show ‹weight T = None ⟹ unsatisfiable (set_mset N)›
    using full_cdcl_bnb_stgy_no_conflicting_clause_unsat[OF st]
    by auto
  have ‹annotation_is_model ?S›
    by (auto simp: annotation_is_model_def)
  then have ‹annotation_is_model T›
    using rtranclp_cdcl_bnb_annotation_is_model[of ?S T] st
    unfolding full_def by (auto dest: rtranclp_cdcl_bnb_stgy_cdcl_bnb)
  moreover have ‹init_clss T = N›
    using rtranclp_cdcl_bnb_no_more_init_clss[of ?S T] st
    unfolding full_def by (auto dest: rtranclp_cdcl_bnb_stgy_cdcl_bnb)
  ultimately show ‹weight T ≠ None ⟹ consistent_interp (set_mset (the (weight T))) ∧
       atms_of (the (weight T)) ⊆ atms_of_mm N ∧ set_mset (the (weight T)) ⊨sm N ∧
       total_over_m (set_mset (the (weight T))) (set_mset N) ∧
       distinct_mset (the (weight T))›
    by (auto simp: annotation_is_model_def)

  show ‹distinct_mset I ⟹ consistent_interp (set_mset I) ⟹ atms_of I = atms_of_mm N ⟹
      set_mset I ⊨sm N ⟹ Found (ρ I) ≥ ρ' (weight T)›
    using full_cdcl_bnb_stgy_larger_or_equal_weight[of ?S T I] st unfolding full_def
    by auto
qed

lemma pruned_clause_in_conflicting_clss:
  assumes
    ge: ‹⋀M'. total_over_m (set_mset (mset (M @ M'))) (set_mset (init_clss S)) ⟹
      distinct_mset (atm_of `# mset (M @ M')) ⟹
      consistent_interp (set_mset (mset (M @ M'))) ⟹
      Found (ρ (mset (M @ M'))) ≥ ρ' (weight S)› and
    atm: ‹atms_of (mset M) ⊆ atms_of_mm (init_clss S)› and
    dist: ‹distinct M› and
    cons: ‹consistent_interp (set M)›
  shows ‹pNeg (mset M) ∈# conflicting_clss S›
proof -
  have 0: ‹(pNeg o mset o ((@) M))` {M'.
      distinct_mset (atm_of `# mset (M @ M')) ∧ consistent_interp (set_mset (mset (M @ M'))) ∧
      atms_of_s (set (M @ M')) ⊆ (atms_of_mm (init_clss S)) ∧
      card (atms_of_mm (init_clss S)) = n + card (atms_of (mset (M @ M')))} ⊆
    set_mset (conflicting_clss S)› (is ‹_ ` ?A n ⊆ ?H›)for n
  proof (induction n)
    case 0
    show ?case
    proof clarify
      fix x :: ‹'v literal multiset› and xa :: ‹'v literal multiset› and
        xb :: ‹'v literal list› and xc :: ‹'v literal list›
      assume
        dist: ‹distinct_mset (atm_of `# mset (M @ xc))› and
        cons: ‹consistent_interp (set_mset (mset (M @ xc)))› and
        atm': ‹atms_of_s (set (M @ xc)) ⊆ atms_of_mm (init_clss S)› and
        0: ‹card (atms_of_mm (init_clss S)) = 0 + card (atms_of (mset (M @ xc)))›
      have D[dest]:
        ‹A ∈ set M ⟹ A ∉ set xc› ‹A ∈ set M ⟹ -A ∉ set xc›
        for A
        using dist multi_member_split[of A ‹mset M›] multi_member_split[of ‹-A› ‹mset xc›]
          multi_member_split[of ‹-A› ‹mset M›] multi_member_split[of ‹A› ‹mset xc›]
        by (auto simp: atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set)
      have dist2: ‹distinct xc› ‹distinct_mset (atm_of `# mset xc)›
        ‹distinct_mset (mset M + mset xc)›
        using dist distinct_mset_atm_ofD[OF dist]
        unfolding mset_append[symmetric] distinct_mset_mset_distinct
        by (auto dest: distinct_mset_union2 distinct_mset_atm_ofD)
      have eq: ‹card (atms_of_s (set M) ∪ atms_of_s (set xc)) =
        card (atms_of_s (set M)) + card (atms_of_s (set xc))›
              by (subst card_Un_Int) auto
      let ?M = ‹M @ xc›

      have H1: ‹atms_of_s (set ?M) = atms_of_mm (init_clss S)›
        using eq atm card_mono[OF _ atm'] card_subset_eq[OF _ atm'] 0
        by (auto simp: atms_of_s_def image_Un)
      moreover have tot2: ‹total_over_m (set ?M) (set_mset (init_clss S))›
        using H1 by (auto simp: total_over_m_def total_over_set_def lit_in_set_iff_atm)
      moreover have ‹¬tautology (mset ?M)›
        using cons unfolding consistent_interp_tautology[symmetric]
        by auto
      ultimately have ‹mset ?M ∈ simple_clss (atms_of_mm (init_clss S))›
        using dist atm cons H1 dist2
        by (auto simp: simple_clss_def consistent_interp_tautology atms_of_s_def)
      moreover have tot2: ‹total_over_m (set ?M) (set_mset (init_clss S))›
        using H1 by (auto simp: total_over_m_def total_over_set_def lit_in_set_iff_atm)
      ultimately show ‹(pNeg ∘ mset ∘ (@) M) xc ∈# conflicting_clss S›
        using ge[of ‹xc›] dist 0 cons card_mono[OF _ atm] tot2 cons
        by (auto simp: conflicting_clss_def too_heavy_clauses_def simple_clss_finite
            intro!: too_heavy_clauses_conflicting_clauses imageI)
    qed
  next
    case (Suc n) note IH = this(1)
    let ?H = ‹?A n›
    show ?case
    proof clarify
      fix x :: ‹'v literal multiset› and xa :: ‹'v literal multiset› and
        xb :: ‹'v literal list› and xc :: ‹'v literal list›
      assume
        dist: ‹distinct_mset (atm_of `# mset (M @ xc))› and
        cons: ‹consistent_interp (set_mset (mset (M @ xc)))› and
        atm': ‹atms_of_s (set (M @ xc)) ⊆ atms_of_mm (init_clss S)› and
        0: ‹card (atms_of_mm (init_clss S)) = Suc n + card (atms_of (mset (M @ xc)))›
      then obtain a where
        a: ‹a ∈ atms_of_mm (init_clss S)› and
        a_notin: ‹a ∉ atms_of_s (set (M @ xc))›
        by (metis Suc_n_not_le_n add_Suc_shift atms_of_mmltiset atms_of_s_def le_add2
            subsetI subset_antisym)
      have dist2: ‹distinct xc› ‹distinct_mset (atm_of `# mset xc)›
        ‹distinct_mset (mset M + mset xc)›
        using dist distinct_mset_atm_ofD[OF dist]
        unfolding mset_append[symmetric] distinct_mset_mset_distinct
        by (auto dest: distinct_mset_union2 distinct_mset_atm_ofD)
      let ?xc1 = ‹Pos a # xc›
      let ?xc2 = ‹Neg a # xc›
      have ‹?xc1 ∈ ?H›
        using dist cons atm' 0 dist2 a_notin a
        by (auto simp: distinct_mset_add mset_inter_empty_set_mset
            lit_in_set_iff_atm card_insert_if)
      from set_mp[OF IH imageI[OF this]]
      have 1: ‹too_heavy_clauses (init_clss S) (weight S) ⊨pm add_mset (-(Pos a)) (pNeg (mset (M @ xc)))›
        unfolding conflicting_clss_def unfolding conflicting_clauses_def
        by (auto simp: pNeg_simps)
      have ‹?xc2 ∈ ?H›
        using dist cons atm' 0 dist2 a_notin a
        by (auto simp: distinct_mset_add mset_inter_empty_set_mset
            lit_in_set_iff_atm card_insert_if)
      from set_mp[OF IH imageI[OF this]]
      have 2: ‹too_heavy_clauses (init_clss S) (weight S) ⊨pm add_mset (Pos a) (pNeg (mset (M @ xc)))›
        unfolding conflicting_clss_def unfolding conflicting_clauses_def
        by (auto simp: pNeg_simps)

      have ‹¬tautology (mset (M @ xc))›
        using cons unfolding consistent_interp_tautology[symmetric]
        by auto
      then have ‹¬tautology (pNeg (mset M) + pNeg (mset xc))›
        unfolding mset_append[symmetric] pNeg_simps[symmetric]
        by (auto simp del: mset_append)
      then have ‹pNeg (mset M) + pNeg (mset xc) ∈ simple_clss (atms_of_mm (init_clss S))›
        using atm' dist2 by (auto simp: simple_clss_def atms_of_s_def simp flip: pNeg_simps)
      then show ‹(pNeg ∘ mset ∘ (@) M) xc ∈# conflicting_clss S›
        using true_clss_cls_or_true_clss_cls_or_not_true_clss_cls_or[OF 1 2] apply -
        unfolding conflicting_clss_def conflicting_clauses_def
        by (subst (asm) true_clss_cls_remdups_mset[symmetric])
          (auto simp: simple_clss_finite pNeg_simps intro: true_clss_cls_cong_set_mset
            simp del: true_clss_cls_remdups_mset)
    qed
  qed
  have ‹[] ∈ {M'.
     distinct_mset (atm_of `# mset (M @ M')) ∧
     consistent_interp (set_mset (mset (M @ M'))) ∧
     atms_of_s (set (M @ M')) ⊆ atms_of_mm (init_clss S) ∧
     card (atms_of_mm (init_clss S)) =
     card (atms_of_mm (init_clss S)) - card (atms_of (mset M)) +
     card (atms_of (mset (M @ M')))}›
    using card_mono[OF _ assms(2)] assms by (auto dest: card_mono distinct_consistent_distinct_atm)

  from set_mp[OF 0 imageI[OF this]]
  show ‹pNeg (mset M) ∈# conflicting_clss S›
    by auto
qed

end

end