Theory CDCL_W_Partial_Encoding

theory CDCL_W_Partial_Encoding
  imports CDCL_W_Optimal_Model
begin

(*TODO Move*)
lemma consistent_interp_unionI:
  ‹consistent_interp A ⟹ consistent_interp B ⟹ (⋀a. a ∈ A ⟹ -a ∉ B) ⟹ (⋀a. a ∈ B ⟹ -a ∉ A) ⟹
    consistent_interp (A ∪ B)›
  by (auto simp: consistent_interp_def)

lemma consistent_interp_poss: ‹consistent_interp (Pos ` A)› and
  consistent_interp_negs: ‹consistent_interp (Neg ` A)›
  by (auto simp: consistent_interp_def)

lemma Neg_in_lits_of_l_definedD:
  ‹Neg A ∈ lits_of_l M ⟹ defined_lit M (Pos A)›
  by (simp add: Decided_Propagated_in_iff_in_lits_of_l)


subsection ‹Encoding of partial SAT into total SAT›

text ‹As a way to make sure we don't reuse theorems names:›
interpretation test: conflict_driven_clause_learningW_optimal_weight where
  state_eq = ‹(=)› and
  state = id and
  trail = ‹λ(M, N, U, D, W). M› and
  init_clss = ‹λ(M, N, U, D, W). N› and
  learned_clss = ‹λ(M, N, U, D, W). U› and
  conflicting = ‹λ(M, N, U, D, W). D› and
  cons_trail = ‹λK (M, N, U, D, W). (K # M, N, U, D, W)› and
  tl_trail = ‹λ(M, N, U, D, W). (tl M, N, U, D, W)› and
  add_learned_cls = ‹λC (M, N, U, D, W). (M, N, add_mset C U, D, W)› and
  remove_cls = ‹λC (M, N, U, D, W). (M, removeAll_mset C N, removeAll_mset C U, D, W)› and
  update_conflicting = ‹λC (M, N, U, _, W). (M, N, U, C, W)› and
  init_state = ‹λN. ([], N, {#}, None, None, ())› and
  ρ = ‹λ_. 0› and
  update_additional_info = ‹λW (M, N, U, D, _, _). (M, N, U, D, W)›
  by unfold_locales (auto simp: stateW_ops.additional_info_def)

text ‹
  We here formalise the encoding from a formula to another formula from which we will use to derive the
  optimal partial model.

  While the proofs are still inspired by Dominic Zimmer's upcoming bachelor thesis, we now use the dual
  rail encoding, which is more elegant that the solution found by Christoph to solve the problem.

  The intended meaning is the following:
  ▪ term‹Σ› is the set of all variables
  ▪ term‹ΔΣ› is the set of all variables with a (possibly non-zero) weight: These are the variable that needs
    to be replaced during encoding, but it does not matter if the weight 0.
›
locale optimal_encoding_opt_ops = 
  fixes Σ ΔΣ :: ‹'v set› and
    new_vars :: ‹'v ⇒ 'v × 'v›
begin

abbreviation replacement_pos :: ‹'v ⇒ 'v› (‹(_)↦1› 100) where
  ‹replacement_pos A ≡ fst (new_vars A)›

abbreviation replacement_neg :: ‹'v ⇒ 'v› (‹(_)↦0› 100) where
  ‹replacement_neg A ≡ snd (new_vars A)›


fun encode_lit where
  ‹encode_lit (Pos A) = (if A ∈ ΔΣ then Pos (replacement_pos A) else Pos A)› |
  ‹encode_lit (Neg A) = (if A ∈ ΔΣ then Pos (replacement_neg A) else Neg A)›

lemma encode_lit_alt_def:
  ‹encode_lit A = (if atm_of A ∈ ΔΣ
    then Pos (if is_pos A then replacement_pos (atm_of A) else replacement_neg (atm_of A))
    else A)›
  by (cases A) auto

definition encode_clause :: ‹'v clause ⇒ 'v clause› where
  ‹encode_clause C = encode_lit `# C›

lemma encode_clause_simp[simp]:
  ‹encode_clause {#} = {#}›
  ‹encode_clause (add_mset A C) = add_mset (encode_lit A) (encode_clause C)›
  ‹encode_clause (C + D) = encode_clause C + encode_clause D›
  by (auto simp: encode_clause_def)

definition encode_clauses :: ‹'v clauses ⇒ 'v clauses› where
  ‹encode_clauses C = encode_clause `# C›

lemma encode_clauses_simp[simp]:
  ‹encode_clauses {#} = {#}›
  ‹encode_clauses (add_mset A C) = add_mset (encode_clause A) (encode_clauses C)›
  ‹encode_clauses (C + D) = encode_clauses C + encode_clauses D›
  by (auto simp: encode_clauses_def)

definition additional_constraint :: ‹'v ⇒ 'v clauses› where
  ‹additional_constraint A =
     {#{#Neg (A↦1), Neg (A↦0)#}#}›

definition additional_constraints :: ‹'v clauses› where
  ‹additional_constraints = ∑#(additional_constraint `# (mset_set ΔΣ))›

definition penc :: ‹'v clauses ⇒ 'v clauses› where
  ‹penc N = encode_clauses N + additional_constraints›

lemma size_encode_clauses[simp]: ‹size (encode_clauses N) = size N›
  by (auto simp: encode_clauses_def)

lemma size_penc:
  ‹size (penc N) = size N + card ΔΣ›
  by (auto simp: penc_def additional_constraints_def
      additional_constraint_def size_Union_mset_image_mset)

lemma atms_of_mm_additional_constraints: ‹finite ΔΣ ⟹
   atms_of_mm additional_constraints = replacement_pos ` ΔΣ ∪ replacement_neg ` ΔΣ›
  by (auto simp: additional_constraints_def additional_constraint_def atms_of_ms_def)

lemma atms_of_mm_encode_clause_subset:
  ‹atms_of_mm (encode_clauses N) ⊆ (atms_of_mm N - ΔΣ) ∪ replacement_pos ` {A ∈ ΔΣ. A ∈ atms_of_mm N}
    ∪ replacement_neg ` {A ∈ ΔΣ. A ∈ atms_of_mm N}›
  by (auto simp: encode_clauses_def encode_lit_alt_def atms_of_ms_def atms_of_def
      encode_clause_def split: if_splits
      dest!: multi_member_split[of _ N])

text ‹In every meaningful application of the theorem below, we have ‹ΔΣ ⊆ atms_of_mm N›.›
lemma atms_of_mm_penc_subset: ‹finite ΔΣ ⟹
  atms_of_mm (penc N) ⊆ atms_of_mm N ∪ replacement_pos ` ΔΣ
      ∪ replacement_neg ` ΔΣ ∪ ΔΣ›
  using atms_of_mm_encode_clause_subset[of N]
  by (auto simp: penc_def atms_of_mm_additional_constraints)

lemma atms_of_mm_encode_clause_subset2: ‹finite ΔΣ ⟹ ΔΣ ⊆ atms_of_mm N ⟹
  atms_of_mm N ⊆ atms_of_mm (encode_clauses N) ∪ ΔΣ›
  by (auto simp: encode_clauses_def encode_lit_alt_def atms_of_ms_def atms_of_def
      encode_clause_def split: if_splits
      dest!: multi_member_split[of _ N])

lemma atms_of_mm_penc_subset2: ‹finite ΔΣ ⟹ ΔΣ ⊆ atms_of_mm N ⟹
  atms_of_mm (penc N) = (atms_of_mm N - ΔΣ) ∪ replacement_pos ` ΔΣ ∪ replacement_neg ` ΔΣ›
  using atms_of_mm_encode_clause_subset[of N] atms_of_mm_encode_clause_subset2[of N]
  by (auto simp: penc_def atms_of_mm_additional_constraints)

theorem card_atms_of_mm_penc:
  assumes ‹finite ΔΣ› and  ‹ΔΣ ⊆ atms_of_mm N›
  shows ‹card (atms_of_mm (penc N)) ≤ card (atms_of_mm N - ΔΣ) + 2 * card ΔΣ› (is ‹?A ≤ ?B›)
proof -
  have ‹?A = card
     ((atms_of_mm N - ΔΣ) ∪ replacement_pos ` ΔΣ ∪
      replacement_neg ` ΔΣ)› (is ‹_ = card (?W ∪ ?X ∪ ?Y)›)
    using arg_cong[OF atms_of_mm_penc_subset2[of N], of card] assms card_Un_le
    by auto
  also have ‹... ≤ card (?W ∪ ?X) + card ?Y›
    using card_Un_le[of ‹?W ∪ ?X› ?Y] by auto
  also have ‹... ≤ card ?W + card ?X + card ?Y›
    using card_Un_le[of ‹?W› ?X] by auto
  also have ‹... ≤  card (atms_of_mm N - ΔΣ) + 2 * card ΔΣ›
    using card_mono[of ‹atms_of_mm N› ‹ΔΣ›] assms
      card_image_le[of ΔΣ replacement_pos] card_image_le[of ΔΣ replacement_neg]
    by auto
  finally show ?thesis .
qed

definition postp :: ‹'v partial_interp ⇒ 'v partial_interp› where
  ‹postp I =
     {A ∈ I. atm_of A ∉ ΔΣ ∧ atm_of A ∈ Σ} ∪ Pos ` {A. A ∈ ΔΣ ∧ Pos (replacement_pos A) ∈ I}
       ∪ Neg ` {A. A ∈ ΔΣ ∧ Pos (replacement_neg A) ∈ I ∧ Pos (replacement_pos A) ∉ I}›

lemma preprocess_clss_model_additional_variables2:
  assumes
    ‹atm_of A ∈ Σ - ΔΣ›
  shows
    ‹A ∈ postp I ⟷ A ∈ I› (is ?A)
proof -
  show ?A
    using assms
    by (auto simp: postp_def)
qed

lemma encode_clause_iff:
  assumes
    ‹⋀A. A ∈ ΔΣ ⟹ Pos A ∈ I ⟷ Pos (replacement_pos A) ∈ I›
    ‹⋀A. A ∈ ΔΣ ⟹ Neg A ∈ I ⟷ Pos (replacement_neg A) ∈ I›
  shows ‹I ⊨ encode_clause C ⟷ I ⊨ C›
  using assms
  apply (induction C)
  subgoal by auto
  subgoal for A C
    by (cases A)
      (auto simp: encode_clause_def encode_lit_alt_def split: if_splits)
  done

lemma encode_clauses_iff:
  assumes
    ‹⋀A. A ∈ ΔΣ ⟹ Pos A ∈ I ⟷ Pos (replacement_pos A) ∈ I›
    ‹⋀A. A ∈ ΔΣ ⟹ Neg A ∈ I ⟷ Pos (replacement_neg A) ∈ I›
  shows ‹I ⊨m encode_clauses C ⟷ I ⊨m C›
  using encode_clause_iff[OF assms]
  by (auto simp: encode_clauses_def true_cls_mset_def)


definition Σadd where
  ‹Σadd = replacement_pos ` ΔΣ ∪ replacement_neg ` ΔΣ›


definition upostp :: ‹'v partial_interp ⇒ 'v partial_interp› where
  ‹upostp I =
     Neg ` {A ∈ Σ. A ∉ ΔΣ ∧ Pos A ∉ I ∧ Neg A ∉ I}
     ∪ {A ∈ I. atm_of A ∈ Σ ∧ atm_of A ∉ ΔΣ}
     ∪ Pos ` replacement_pos ` {A ∈ ΔΣ. Pos A ∈ I}
     ∪ Neg ` replacement_pos ` {A ∈ ΔΣ. Pos A ∉ I}
     ∪ Pos ` replacement_neg ` {A ∈ ΔΣ. Neg A ∈ I}
     ∪ Neg ` replacement_neg ` {A ∈ ΔΣ. Neg A ∉ I}›

lemma atm_of_upostp_subset:
  ‹atm_of ` (upostp I) ⊆
    (atm_of ` I - ΔΣ) ∪ replacement_pos ` ΔΣ ∪
    replacement_neg ` ΔΣ ∪ Σ›
  by (auto simp: upostp_def image_Un)

end


locale optimal_encoding_opt = conflict_driven_clause_learningW_optimal_weight
    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 ρ
     update_additional_info +
  optimal_encoding_opt_ops Σ ΔΣ new_vars
  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
    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
  ‹conflicting S = None› and
  ‹undefined_lit (trail S) L› and
  ‹atm_of L ∈ atms_of_mm (init_clss S)› and
  ‹T ∼ cons_trail (Decided L) S› and
  ‹atm_of L ∈ Σ - ΔΣ› |
  odecide_replacement_pos: ‹odecide S T›
if
  ‹conflicting S = None› and
  ‹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
  ‹conflicting S = None› and
  ‹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›

definition no_new_lonely_clause :: ‹'v clause ⇒ bool› where
  ‹no_new_lonely_clause C ⟷
    (∀L ∈ ΔΣ. L ∈ atms_of C ⟶
      Neg (replacement_pos L) ∈# C ∨ Neg (replacement_neg L) ∈# C ∨ C ∈# additional_constraint L)›

definition lonely_weighted_lit_decided where
  ‹lonely_weighted_lit_decided S ⟷
    (∀L ∈ ΔΣ. Decided (Pos L) ∉ set (trail S) ∧ Decided (Neg L) ∉ set (trail S))›

end

locale optimal_encoding_ops = optimal_encoding_opt_ops
    Σ ΔΣ
    new_vars +
  ocdcl_weight ρ
  for
    Σ ΔΣ :: ‹'v set› and
    new_vars :: ‹'v ⇒ 'v × 'v› and
    ρ :: ‹'v clause ⇒ 'a :: {linorder}› +
  assumes
    finite_Σ:
    ‹finite ΔΣ› and
    ΔΣ_Σ:
    ‹ΔΣ ⊆ Σ› and
    new_vars_pos:
    ‹A ∈ ΔΣ ⟹ replacement_pos A ∉ Σ› and
    new_vars_neg:
    ‹A ∈ ΔΣ ⟹ replacement_neg A ∉ Σ› and
    new_vars_dist:
    ‹inj_on replacement_pos ΔΣ›
    ‹inj_on replacement_neg ΔΣ›
    ‹replacement_pos ` ΔΣ ∩ replacement_neg ` ΔΣ = {}› and
    Σ_no_weight:
      ‹atm_of C ∈ Σ - ΔΣ ⟹ ρ (add_mset C M) = ρ M›
begin

lemma new_vars_dist2:
  ‹A ∈ ΔΣ ⟹ B ∈ ΔΣ ⟹ A ≠ B ⟹ replacement_pos A ≠ replacement_pos B›
  ‹A ∈ ΔΣ ⟹ B ∈ ΔΣ ⟹ A ≠ B ⟹ replacement_neg A ≠ replacement_neg B›
  ‹A ∈ ΔΣ ⟹ B ∈ ΔΣ ⟹ replacement_neg A ≠ replacement_pos B›
  using new_vars_dist unfolding inj_on_def apply blast
  using new_vars_dist unfolding inj_on_def apply blast
  using new_vars_dist unfolding inj_on_def apply blast
  done

lemma consistent_interp_postp:
  ‹consistent_interp I ⟹ consistent_interp (postp I)›
  by (auto simp: consistent_interp_def postp_def uminus_lit_swap)

text ‹The reverse of the previous theorem does not hold due to the filtering on the variables of
  term‹ΔΣ›. One example of version that holds:›
lemma
  assumes ‹A ∈ ΔΣ›
  shows ‹consistent_interp (postp {Pos A , Neg A})› and
    ‹¬consistent_interp {Pos A, Neg A}›
  using assms ΔΣ_Σ
  by (auto simp: consistent_interp_def postp_def uminus_lit_swap)

text ‹Some more restricted version of the reverse hold, like:›
lemma consistent_interp_postp_iff:
  ‹atm_of ` I ⊆ Σ - ΔΣ ⟹ consistent_interp I ⟷ consistent_interp (postp I)›
  by (auto simp: consistent_interp_def postp_def uminus_lit_swap)

lemma new_vars_different_iff[simp]:
  ‹A ≠ x↦1›
  ‹A ≠ x↦0›
  ‹x↦1 ≠ A›
  ‹x↦0 ≠ A›
  ‹A↦0 ≠ x↦1›
  ‹A↦1 ≠ x↦0›
  ‹A↦0 = x↦0 ⟷ A = x›
  ‹A↦1 = x↦1 ⟷ A = x›
  ‹(A↦1) ∉ Σ›
  ‹(A↦0) ∉ Σ›
  ‹(A↦1) ∉ ΔΣ›
  ‹(A↦0) ∉ ΔΣ›if ‹A ∈ ΔΣ›  ‹x ∈ ΔΣ› for A x
  using ΔΣ_Σ new_vars_pos[of x] new_vars_pos[of A]  new_vars_neg[of x] new_vars_neg[of A]
    new_vars_neg new_vars_dist2[of A x] new_vars_dist2[of x A] that
  by (cases ‹A = x›; fastforce simp: comp_def; fail)+

lemma consistent_interp_upostp:
  ‹consistent_interp I ⟹ consistent_interp (upostp I)›
  using ΔΣ_Σ
  by (auto simp: consistent_interp_def upostp_def uminus_lit_swap)


lemma atm_of_upostp_subset2:
  ‹atm_of ` I ⊆ Σ ⟹ replacement_pos ` ΔΣ ∪
    replacement_neg ` ΔΣ ∪ (Σ - ΔΣ) ⊆ atm_of ` (upostp I)›
  apply (auto simp: upostp_def image_Un image_image)
   apply (metis (mono_tags, lifting) imageI literal.sel(1) mem_Collect_eq)
  apply (metis (mono_tags, lifting) imageI literal.sel(2) mem_Collect_eq)
  done


lemma ΔΣ_notin_upost[simp]:
   ‹y ∈ ΔΣ ⟹ Neg y ∉ upostp I›
   ‹y ∈ ΔΣ ⟹ Pos y ∉ upostp I›
  using ΔΣ_Σ by (auto simp: upostp_def)

lemma penc_ent_upostp: (* \htmllink{ocdcl-enc-upostp-model} *)
  assumes Σ: ‹atms_of_mm N = Σ› and
    sat: ‹I ⊨sm N› and
    cons: ‹consistent_interp I› and
    atm: ‹atm_of ` I ⊆ atms_of_mm N›
  shows ‹upostp I ⊨m penc N›
proof -
  have [iff]: ‹Pos (A↦0) ∉ I› ‹Pos (A↦1) ∉ I›
    ‹Neg (A↦0) ∉ I› ‹Neg (A↦1) ∉ I›  if ‹A ∈ ΔΣ› for A
    using atm new_vars_neg[of A] new_vars_pos[of A] that
    unfolding Σ by force+
  have enc: ‹upostp I ⊨m encode_clauses N›
    unfolding true_cls_mset_def
  proof
    fix C
    assume ‹C ∈# encode_clauses N›
    then obtain C' where
      ‹C' ∈# N› and
      ‹C = encode_clause C'›
      by (auto simp: encode_clauses_def)
    then obtain A where
      ‹A ∈# C'› and
      ‹A ∈ I›
      using sat
      by (auto simp: true_cls_def
          dest!: multi_member_split[of _ N])
    moreover have ‹atm_of A ∈ Σ - ΔΣ ∨ atm_of A ∈ ΔΣ›
      using atm ‹A ∈ I› unfolding Σ by blast
    ultimately have ‹encode_lit A ∈ upostp I›
      by (auto simp: encode_lit_alt_def upostp_def)
    then show ‹upostp I ⊨ C›
      using ‹A ∈# C'›
      unfolding ‹C = encode_clause C'›
      by (auto simp: encode_clause_def dest: multi_member_split)
  qed
  have [iff]: ‹Pos (y↦1) ∉ upostp I ⟷ Neg (y↦1) ∈ upostp I›
    ‹Pos (y↦0) ∉ upostp I ⟷ Neg (y↦0) ∈ upostp I›
    if ‹y ∈ ΔΣ› for y
    using that
    by (cases ‹Pos y ∈ I›; auto simp: upostp_def image_image; fail)+
  have H:
    ‹Neg (y↦0) ∉ upostp I ⟹ Neg (y↦1) ∈ upostp I›
    if ‹y ∈ ΔΣ› for y
    using that cons ΔΣ_Σ unfolding upostp_def consistent_interp_def
    by (cases ‹Pos y ∈ I›) (auto simp:  image_image)
  have [dest]: ‹Neg A ∈ upostp I ⟹ Pos A ∉ upostp I›
    ‹Pos A ∈ upostp I ⟹ Neg A ∉ upostp I› for A
    using consistent_interp_upostp[OF cons]
    by (auto simp: consistent_interp_def)

  have add: ‹upostp I ⊨m additional_constraints›
    using finite_Σ H
    by (auto simp: additional_constraints_def true_cls_mset_def additional_constraint_def)

  show ‹upostp I ⊨m penc N›
    using enc add unfolding penc_def by auto
qed

lemma penc_ent_postp: (*  \htmllink{ocdcl-enc-postp-model} *)
  assumes Σ: ‹atms_of_mm N = Σ› and
    sat: ‹I ⊨sm penc N› and
    cons: ‹consistent_interp I›
  shows ‹postp I ⊨m N›
proof -
  have enc: ‹I ⊨m encode_clauses N› and ‹I ⊨m additional_constraints›
    using sat unfolding penc_def
    by auto
  have [dest]: ‹Pos (x2↦0) ∈ I ⟹ Neg (x2↦1) ∈ I› if ‹x2 ∈ ΔΣ› for x2
    using ‹I ⊨m additional_constraints› that cons
    multi_member_split[of x2 ‹mset_set ΔΣ›] finite_Σ
    unfolding additional_constraints_def additional_constraint_def
      consistent_interp_def
    by (auto simp: true_cls_mset_def)
  have [dest]: ‹Pos (x2↦0) ∈ I ⟹ Pos (x2↦1) ∉ I› if ‹x2 ∈ ΔΣ› for x2
    using that cons
    unfolding consistent_interp_def
    by auto

  show ‹postp I ⊨m N›
    unfolding true_cls_mset_def
  proof
    fix C
    assume ‹C ∈# N›
    then have ‹I ⊨ encode_clause C›
      using enc by (auto dest!: multi_member_split)
    then show ‹postp I ⊨ C›
      unfolding true_cls_def
      using cons finite_Σ sat
        preprocess_clss_model_additional_variables2[of _ I]
        Σ ‹C ∈# N› in_m_in_literals
      apply (auto simp: encode_clause_def postp_def encode_lit_alt_def
          split: if_splits
          dest!: multi_member_split[of _ C])
          using image_iff apply fastforce
          apply (case_tac xa; auto)
          apply auto
          done
       (*TODO proof*)
  qed
qed

lemma satisfiable_penc_satisfiable:
  assumes Σ: ‹atms_of_mm N = Σ› and
    sat: ‹satisfiable (set_mset (penc N))›
  shows ‹satisfiable (set_mset N)›
  using assms apply (subst (asm) satisfiable_def)
  apply clarify
  subgoal for I
    using penc_ent_postp[OF Σ, of I] consistent_interp_postp[of I]
    by auto
  done

lemma satisfiable_penc:
  assumes Σ: ‹atms_of_mm N = Σ› and
    sat: ‹satisfiable (set_mset N)›
  shows ‹satisfiable (set_mset (penc N))›
  using assms
  apply (subst (asm) satisfiable_def_min)
  apply clarify
  subgoal for I
    using penc_ent_upostp[of N I] consistent_interp_upostp[of I]
    by auto
  done

lemma satisfiable_penc_iff:
  assumes Σ: ‹atms_of_mm N = Σ›
  shows ‹satisfiable (set_mset (penc N)) ⟷ satisfiable (set_mset N)›
  using assms satisfiable_penc satisfiable_penc_satisfiable by blast


abbreviation ρe_filter :: ‹'v literal multiset ⇒ 'v literal multiset› where
  ‹ρe_filter M ≡ {#L ∈# poss (mset_set ΔΣ). Pos (atm_of L↦1) ∈# M#} +
     {#L ∈# negs (mset_set ΔΣ). Pos (atm_of L↦0) ∈# M#}›

lemma finite_upostp: ‹finite I  ⟹ finite Σ ⟹ finite (upostp I)›
  using finite_Σ ΔΣ_Σ
  by (auto simp: upostp_def)

declare finite_Σ[simp]

lemma encode_lit_eq_iff:
  ‹atm_of x ∈ Σ ⟹ atm_of y ∈ Σ ⟹ encode_lit x = encode_lit y ⟷ x = y›
  by (cases x; cases y) (auto simp: encode_lit_alt_def atm_of_eq_atm_of)

lemma distinct_mset_encode_clause_iff:
  ‹atms_of N ⊆ Σ ⟹ distinct_mset (encode_clause N) ⟷ distinct_mset N›
  by (induction N)
    (auto simp: encode_clause_def encode_lit_eq_iff
      dest!: multi_member_split)

lemma distinct_mset_encodes_clause_iff:
  ‹atms_of_mm N ⊆ Σ ⟹ distinct_mset_mset (encode_clauses N) ⟷ distinct_mset_mset N›
  by (induction N)
    (auto simp: encode_clauses_def distinct_mset_encode_clause_iff)

lemma distinct_additional_constraints[simp]:
  ‹distinct_mset_mset additional_constraints›
  by (auto simp: additional_constraints_def additional_constraint_def
      distinct_mset_set_def)

lemma distinct_mset_penc:
  ‹atms_of_mm N ⊆ Σ ⟹ distinct_mset_mset (penc N) ⟷ distinct_mset_mset N›
  by (auto simp: penc_def
      distinct_mset_encodes_clause_iff)

lemma finite_postp: ‹finite I ⟹ finite (postp I)›
  by (auto simp: postp_def)

lemma total_entails_iff_no_conflict:
  assumes ‹atms_of_mm N ⊆ atm_of ` I› and ‹consistent_interp I›
  shows ‹I ⊨sm N ⟷ (∀C ∈# N. ¬I ⊨s CNot C)›
  apply rule
  subgoal
    using assms by (auto dest!: multi_member_split
        simp: consistent_CNot_not)
  subgoal
    by (smt assms(1) atms_of_atms_of_ms_mono atms_of_ms_CNot_atms_of
        atms_of_ms_insert atms_of_ms_mono atms_of_s_def empty_iff
        subset_iff sup.orderE total_not_true_cls_true_clss_CNot
        total_over_m_alt_def true_clss_def)
  done

definition ρe :: ‹'v literal multiset ⇒ 'a :: {linorder}› where
  ‹ρe M = ρ (ρe_filter M)›

lemma Σ_no_weight_ρe: ‹atm_of C ∈ Σ - ΔΣ ⟹ ρe (add_mset C M) = ρe M›
  using Σ_no_weight[of C ‹ρe_filter M›]
  apply (auto simp: ρe_def finite_Σ image_mset_mset_set inj_on_Neg inj_on_Pos)
  by (smt Collect_cong image_iff literal.sel(1) literal.sel(2) new_vars_neg new_vars_pos)

lemma ρ_cancel_notin_ΔΣ:
  ‹(⋀x. x ∈# M ⟹ atm_of x ∈ Σ - ΔΣ) ⟹ ρ (M + M') = ρ M'›
  by (induction M) (auto simp: Σ_no_weight)

lemma ρ_mono2:
  ‹consistent_interp (set_mset M') ⟹ distinct_mset M' ⟹
   (⋀A. A ∈# M ⟹ atm_of A ∈ Σ) ⟹ (⋀A. A ∈# M' ⟹ atm_of A ∈ Σ) ⟹
     {#A ∈# M. atm_of A ∈ ΔΣ#} ⊆# {#A ∈# M'. atm_of A ∈ ΔΣ#} ⟹ ρ M ≤ ρ M'›
  apply (subst (2) multiset_partition[of _ ‹λA. atm_of A ∉ ΔΣ›])
  apply (subst multiset_partition[of _ ‹λA. atm_of A ∉ ΔΣ›])
  apply (subst ρ_cancel_notin_ΔΣ)
  subgoal by auto
  apply (subst ρ_cancel_notin_ΔΣ)
  subgoal by auto
  by (auto intro!: ρ_mono intro: consistent_interp_subset intro!: distinct_mset_mono[of _ M'])

lemma ρe_mono: ‹distinct_mset B ⟹ A ⊆# B ⟹ ρe A ≤ ρe B›
  unfolding ρe_def
  apply (rule ρ_mono)
  subgoal
    by (subst distinct_mset_add)
      (auto simp: distinct_image_mset_inj distinct_mset_filter distinct_mset_mset_set inj_on_Pos
        mset_inter_empty_set_mset image_mset_mset_set inj_on_Neg)
  subgoal
    by (rule subset_mset.add_mono; rule filter_mset_mono_subset) auto
  done


lemma ρe_upostp_ρ:
  assumes [simp]: ‹finite Σ› and
    ‹finite I› and
    cons: ‹consistent_interp I› and
    I_Σ: ‹atm_of ` I ⊆ Σ›
  shows ‹ρe (mset_set (upostp I)) = ρ (mset_set I)› (is ‹?A = ?B›)
proof -
  have [simp]: ‹finite I›
    using assms by auto
  have [simp]: ‹mset_set
        {x ∈ I.
         atm_of x ∈ Σ ∧
         atm_of x ∉ replacement_pos ` ΔΣ ∧
         atm_of x ∉ replacement_neg ` ΔΣ} = mset_set I›
    using I_Σ by auto
  have [simp]: ‹finite {A ∈ ΔΣ. P A}› for P
    by (rule finite_subset[of _ ΔΣ])
      (use ΔΣ_Σ finite_Σ in auto)
  have [dest]: ‹xa ∈ ΔΣ ⟹ Pos (xa↦1) ∈ upostp I ⟹ Pos (xa↦0) ∈ upostp I ⟹ False› for xa
    using cons unfolding penc_def
    by (auto simp: additional_constraint_def additional_constraints_def
      true_cls_mset_def consistent_interp_def upostp_def)
  have ‹?A ≤ ?B›
    using assms ΔΣ_Σ apply -
    unfolding ρe_def filter_filter_mset
    apply (rule ρ_mono2)
    subgoal using cons by auto
    subgoal using distinct_mset_mset_set by auto
    subgoal by auto
    subgoal by auto
    apply (rule filter_mset_mono_subset)
    subgoal
      by (subst distinct_subseteq_iff[symmetric])
        (auto simp: upostp_def simp: image_mset_mset_set inj_on_Neg inj_on_Pos
           distinct_mset_add mset_inter_empty_set_mset distinct_mset_mset_set)
    subgoal for x
      by (cases ‹x ∈ I›; cases x) (auto simp: upostp_def)
    done
  moreover have ‹?B ≤ ?A›
    using assms ΔΣ_Σ apply -
    unfolding ρe_def filter_filter_mset
    apply (rule ρ_mono2)
    subgoal using cons by (auto intro:
      intro: consistent_interp_subset[of _ ‹Pos ` ΔΣ›]
      intro: consistent_interp_subset[of _ ‹Neg ` ΔΣ›]
      intro!: consistent_interp_unionI
      simp: consistent_interp_upostp finite_upostp consistent_interp_poss
        consistent_interp_negs)
    subgoal by (auto
      simp: distinct_mset_mset_set distinct_mset_add image_mset_mset_set inj_on_Pos inj_on_Neg
        mset_inter_empty_set_mset)
    subgoal by auto
    subgoal by auto (*TODO Proof *)
    apply (auto simp: image_mset_mset_set inj_on_Neg inj_on_Pos)
      apply (subst distinct_subseteq_iff[symmetric])
      apply (auto simp: distinct_mset_mset_set distinct_mset_add image_mset_mset_set inj_on_Pos inj_on_Neg
        mset_inter_empty_set_mset finite_upostp)
        apply (metis image_eqI literal.exhaust_sel)
    apply (auto simp: upostp_def image_image)
    apply (metis (mono_tags, lifting) imageI literal.collapse(1) literal.collapse(2) mem_Collect_eq)
    apply (metis (mono_tags, lifting) imageI literal.collapse(1) literal.collapse(2) mem_Collect_eq)
    apply (metis (mono_tags, lifting) imageI literal.collapse(1) literal.collapse(2) mem_Collect_eq)
    done
  ultimately show ?thesis
    by simp
qed

end

locale optimal_encoding = optimal_encoding_opt
    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
    update_additional_info
    Σ ΔΣ
    ρ
    new_vars +
    optimal_encoding_ops
    Σ ΔΣ
    new_vars ρ
  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}› and
    update_additional_info :: ‹'v clause option × 'b ⇒ 'st ⇒ 'st› and
    Σ ΔΣ :: ‹'v set› and
    new_vars :: ‹'v ⇒ 'v × 'v› 
begin


interpretation enc_weight_opt: conflict_driven_clause_learningW_optimal_weight 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 and
  ρ = ρe and
  update_additional_info = update_additional_info
  apply unfold_locales
  subgoal by (rule ρe_mono)
  subgoal using update_additional_info by fast
  subgoal using weight_init_state by fast
  done

theorem full_encoding_OCDCL_correctness: (* \htmllink{ocdcl-partial-enc-correctness} *)
  assumes
    st: ‹full enc_weight_opt.cdcl_bnb_stgy (init_state (penc N)) T› and
    dist: ‹distinct_mset_mset N› and
    atms: ‹atms_of_mm N = Σ›
  shows
    ‹weight T = None ⟹ unsatisfiable (set_mset N)› and
    ‹weight T ≠ None ⟹ postp (set_mset (the (weight T))) ⊨sm N›
    ‹weight T ≠ None ⟹ distinct_mset I ⟹ consistent_interp (set_mset I) ⟹
      atms_of I ⊆ atms_of_mm N ⟹ set_mset I ⊨sm N ⟹
      ρ I ≥ ρ (mset_set (postp (set_mset (the (weight T)))))›
    ‹weight T ≠ None ⟹ ρe (the (enc_weight_opt.weight T)) =
      ρ (mset_set (postp (set_mset (the (enc_weight_opt.weight T)))))›
proof -
  let ?N = ‹penc N›
  have ‹distinct_mset_mset (penc N)›
    by (subst distinct_mset_penc)
      (use dist atms in auto)
  then have
    unsat: ‹weight T = None ⟹ unsatisfiable (set_mset ?N)› and
    model: ‹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 ∧
       distinct_mset (the (weight T))› and
    opt: ‹distinct_mset I ⟹ consistent_interp (set_mset I) ⟹ atms_of I = atms_of_mm ?N ⟹
      set_mset I ⊨sm ?N ⟹ Found (ρe I) ≥ enc_weight_opt.ρ' (weight T)›
    for I
    using enc_weight_opt.full_cdcl_bnb_stgy_no_conflicting_clause_from_init_state[of
        ‹penc N› T, OF st]
    by fast+

  show ‹unsatisfiable (set_mset N)› if ‹weight T = None›
    using unsat[OF that] satisfiable_penc[OF atms] by blast
  let ?K = ‹postp (set_mset (the (weight T)))›
  show ‹?K ⊨sm N› if ‹weight T ≠ None›
    using penc_ent_postp[OF atms, of ‹set_mset (the (weight T))›] model[OF that]
    by auto

  assume Some: ‹weight T ≠ None›
  have Some': ‹enc_weight_opt.weight T ≠ None›
    using Some by auto
  have cons_K: ‹consistent_interp ?K›
    using model Some by (auto simp: consistent_interp_postp)
  define J where ‹J = the (weight T)›
  then have [simp]: ‹weight T = Some J› ‹enc_weight_opt.weight T = Some J›
    using Some by auto
  have ‹set_mset J ⊨sm additional_constraints›
    using model by (auto simp: penc_def)
  then have H: ‹x ∈ ΔΣ ⟹ Neg (replacement_pos x) ∈# J ∨ Neg (replacement_neg x) ∈# J› and
    [dest]: ‹Pos (xa↦1) ∈# J ⟹ Pos (xa↦0) ∈# J ⟹ xa ∈ ΔΣ ⟹ False›  for x xa
    using model
    apply (auto simp: additional_constraints_def additional_constraint_def true_clss_def
      consistent_interp_def)
      by (metis uminus_Pos)
  have cons_f: ‹consistent_interp (set_mset (ρe_filter (the (weight T))))›
    using model
    by (auto simp: postp_def ρe_def Σadd_def conj_disj_distribR
        consistent_interp_poss
        consistent_interp_negs
        mset_set_Union intro!: consistent_interp_unionI
        intro: consistent_interp_subset distinct_mset_mset_set
        consistent_interp_subset[of _ ‹Pos ` ΔΣ›]
        consistent_interp_subset[of _ ‹Neg ` ΔΣ›])
  have dist_f: ‹distinct_mset ((ρe_filter (the (weight T))))›
    using model
    by  (auto simp: postp_def simp: image_mset_mset_set inj_on_Neg inj_on_Pos
           distinct_mset_add mset_inter_empty_set_mset distinct_mset_mset_set)

  have ‹enc_weight_opt.ρ' (weight T) ≤ Found (ρ (mset_set ?K))›
    using Some'
    apply auto
    unfolding ρe_def
    apply (rule ρ_mono2)
    subgoal
      using model Some' by (auto simp: finite_postp consistent_interp_postp)
    subgoal by (auto simp: distinct_mset_mset_set)
    subgoal using atms dist model[OF Some] atms ΔΣ_Σ by (auto simp: postp_def)
    subgoal using atms dist model[OF Some] atms ΔΣ_Σ by (auto simp: postp_def)
    subgoal
      apply (subst distinct_subseteq_iff[symmetric])
      using dist model[OF Some] H
      by (force simp: filter_filter_mset consistent_interp_def postp_def
              image_mset_mset_set inj_on_Neg inj_on_Pos finite_postp
              distinct_mset_add mset_inter_empty_set_mset distinct_mset_mset_set
            intro: distinct_mset_mono[of _ ‹the (enc_weight_opt.weight T)›])+
    done
  moreover {
    have ‹ρ (mset_set ?K) ≤ ρe (the (weight T))›
      unfolding ρe_def
      apply (rule ρ_mono2)
      subgoal by (rule cons_f)
      subgoal by (rule dist_f)
      subgoal using atms dist model[OF Some] atms ΔΣ_Σ by (auto simp: postp_def)
      subgoal using atms dist model[OF Some] atms ΔΣ_Σ by (auto simp: postp_def)
      subgoal
        by (subst distinct_subseteq_iff[symmetric])
        (auto simp: postp_def simp: image_mset_mset_set inj_on_Neg inj_on_Pos
           distinct_mset_add mset_inter_empty_set_mset distinct_mset_mset_set)
      done
    then have ‹Found (ρ (mset_set ?K)) ≤ enc_weight_opt.ρ' (weight T)›
      using Some by auto
    } note le =this
  ultimately show ‹ρe (the (weight T)) = (ρ (mset_set ?K))›
    using Some' by auto

  show ‹ρ I ≥ ρ (mset_set ?K)›
    if dist: ‹distinct_mset I› and
      cons: ‹consistent_interp (set_mset I)› and
      atm: ‹atms_of I ⊆ atms_of_mm N› and
      I_N: ‹set_mset I ⊨sm N›
  proof -
    let ?I = ‹mset_set (upostp (set_mset I))›
    have [simp]: ‹finite (upostp (set_mset I))›
      by (rule finite_upostp)
        (use atms in auto)
    then have I: ‹set_mset ?I = upostp (set_mset I)›
      by auto
    have ‹set_mset ?I ⊨m ?N›
      unfolding I
      by (rule penc_ent_upostp[OF atms I_N cons])
        (use atm in ‹auto dest: multi_member_split›)
    moreover have ‹distinct_mset ?I›
      by (rule distinct_mset_mset_set)
    moreover {
      have A: ‹atms_of (mset_set (upostp (set_mset I))) = atm_of ` (upostp (set_mset I))›
        ‹atm_of ` set_mset I = atms_of I›
        by (auto simp: atms_of_def)
      have ‹atms_of ?I = atms_of_mm ?N›
        apply (subst atms_of_mm_penc_subset2[OF finite_Σ])
        subgoal using ΔΣ_Σ atms by auto
        subgoal
          using atm_of_upostp_subset[of ‹set_mset I›] atm_of_upostp_subset2[of ‹set_mset I›] atm
          unfolding atms A
          by (auto simp: upostp_def)
        done
    }
    moreover have cons': ‹consistent_interp (set_mset ?I)›
      using cons unfolding I by (rule consistent_interp_upostp)
    ultimately have ‹Found (ρe ?I) ≥ enc_weight_opt.ρ' (weight T)›
      using opt[of ?I] by auto
    moreover {
      have ‹ρe ?I = ρ (mset_set (set_mset I))›
        by (rule ρe_upostp_ρ)
          (use ΔΣ_Σ atms atm cons in ‹auto dest: multi_member_split›)
      then have ‹ρe ?I = ρ I›
        by (subst (asm) distinct_mset_set_mset_ident)
          (use atms dist in auto)
    }
    ultimately have ‹Found (ρ I) ≥ enc_weight_opt.ρ' (weight T)›
      using Some'
      by auto
    moreover {
      have ‹ρe (mset_set ?K) ≤ ρe (mset_set (set_mset (the (weight T))))›
        unfolding ρe_def
        apply (rule ρ_mono2)
        subgoal using cons_f by auto
        subgoal using dist_f by auto
        subgoal using atms dist model[OF Some] atms ΔΣ_Σ by (auto simp: postp_def)
        subgoal using atms dist model[OF Some] atms ΔΣ_Σ by (auto simp: postp_def)
        subgoal
          by (subst distinct_subseteq_iff[symmetric])
          (auto simp: postp_def simp: image_mset_mset_set inj_on_Neg inj_on_Pos
             distinct_mset_add mset_inter_empty_set_mset distinct_mset_mset_set)
        done
      then have ‹Found (ρe (mset_set ?K)) ≤ enc_weight_opt.ρ' (weight T)›
        apply (subst (asm) distinct_mset_set_mset_ident)
         apply (use atms dist model[OF Some] in auto; fail)[]
        using Some' by auto
    }
    moreover have ‹ρe (mset_set ?K) ≤ ρ (mset_set ?K)›
      unfolding ρe_def
      apply (rule ρ_mono2)
      subgoal
        using model Some' by (auto simp: finite_postp consistent_interp_postp)
      subgoal by (auto simp: distinct_mset_mset_set)
      subgoal using atms dist model[OF Some] atms ΔΣ_Σ by (auto simp: postp_def)
      subgoal using atms dist model[OF Some] atms ΔΣ_Σ by (auto simp: postp_def)
      subgoal
        by (subst distinct_subseteq_iff[symmetric])
          (auto simp: postp_def simp: image_mset_mset_set inj_on_Neg inj_on_Pos
              distinct_mset_add mset_inter_empty_set_mset distinct_mset_mset_set)
      done
    ultimately show ?thesis
      using Some' le by auto
  qed
qed

theorem full_encoding_OCDCL_complexity: (* \htmllink{ocdcl-partial-enc-complexity} *)
  assumes
    st: ‹full enc_weight_opt.cdcl_bnb_stgy (init_state (penc N)) T› and
    dist: ‹distinct_mset_mset N› and
    atms: ‹atms_of_mm N = Σ›
  shows ‹size (learned_clss T) ≤ 2 ^ (card (atms_of_mm N - ΔΣ)) * 4^(card ΔΣ)›
proof -
  have [simp]: ‹finite Σ›
    unfolding atms[symmetric]
    by auto
  have [simp]: ‹card (atms_of_mm N - ΔΣ ∪ replacement_pos ` ΔΣ ∪ replacement_neg ` ΔΣ) =
    card (atms_of_mm N - ΔΣ) + card ( replacement_pos ` ΔΣ) + card (replacement_neg ` ΔΣ)›
    by (subst card_Un_disjoint; auto simp: atms)+
  have [simp]: ‹card (replacement_pos ` ΔΣ) = card ΔΣ›  ‹card (replacement_neg ` ΔΣ) = card ΔΣ›
    by (auto intro!: card_image simp: inj_on_def)

  show ?thesis
    apply (rule order_trans[OF enc_weight_opt.cdcl_bnb_pow2_n_learned_clauses[of ‹penc N›]])
    using assms ΔΣ_Σ monoid_mult_class.power_mult[of ‹2 :: nat› ‹2 :: nat› ‹card ΔΣ›, unfolded mult_2]
    by (auto simp: full_def distinct_mset_penc monoid_mult_class.power_add
       enc_weight_opt.rtranclp_cdcl_bnb_stgy_cdcl_bnb atms_of_mm_penc_subset2)
qed

inductive ocdclW_o_r :: ‹'st ⇒ 'st ⇒ bool› for S :: 'st where
  decide: ‹odecide S S' ⟹ ocdclW_o_r S S'› |
  bj: ‹enc_weight_opt.cdcl_bnb_bj S S' ⟹ ocdclW_o_r S S'›

inductive cdcl_bnb_r :: ‹'st ⇒ 'st ⇒ bool› for S :: 'st where
  cdcl_conflict: ‹conflict S S' ⟹ cdcl_bnb_r S S'› |
  cdcl_propagate: ‹propagate S S' ⟹ cdcl_bnb_r S S'› |
  cdcl_improve: ‹enc_weight_opt.improvep S S' ⟹ cdcl_bnb_r S S'› |
  cdcl_conflict_opt: ‹enc_weight_opt.conflict_opt S S' ⟹ cdcl_bnb_r S S'› |
  cdcl_o': ‹ocdclW_o_r S S' ⟹ cdcl_bnb_r S S'›

inductive cdcl_bnb_r_stgy :: ‹'st ⇒ 'st ⇒ bool› for S :: 'st where
  cdcl_bnb_r_conflict: ‹conflict S S' ⟹ cdcl_bnb_r_stgy S S'› |
  cdcl_bnb_r_propagate: ‹propagate S S' ⟹ cdcl_bnb_r_stgy S S'› |
  cdcl_bnb_r_improve: ‹enc_weight_opt.improvep S S' ⟹ cdcl_bnb_r_stgy S S'› |
  cdcl_bnb_r_conflict_opt: ‹enc_weight_opt.conflict_opt S S' ⟹ cdcl_bnb_r_stgy S S'› |
  cdcl_bnb_r_other': ‹ocdclW_o_r S S' ⟹ no_confl_prop_impr S ⟹ cdcl_bnb_r_stgy S S'›

lemma ocdclW_o_r_cases[consumes 1, case_names odecode obacktrack skip resolve]:
  assumes
    ‹ocdclW_o_r S T›
    ‹odecide S T ⟹ P T›
    ‹enc_weight_opt.obacktrack S T ⟹ P T›
    ‹skip S T ⟹ P T›
    ‹resolve S T ⟹ P T›
  shows ‹P T›
  using assms by (auto simp: ocdclW_o_r.simps enc_weight_opt.cdcl_bnb_bj.simps)

context
  fixes S :: 'st
  assumes S_Σ: ‹atms_of_mm (init_clss S) = (Σ - ΔΣ) ∪ replacement_pos ` ΔΣ
     ∪ replacement_neg ` ΔΣ›
begin

lemma odecide_decide:
  ‹odecide S T ⟹ decide S T›
  apply (elim odecideE)
  subgoal for L
    by (rule decide.intros[of S ‹L›]) auto
  subgoal for L
    by (rule decide.intros[of S ‹Pos (L↦1)›]) (use S_Σ ΔΣ_Σ in auto)
  subgoal for L
    by (rule decide.intros[of S ‹Pos (L↦0)›]) (use S_Σ ΔΣ_Σ in auto)
  done

lemma ocdclW_o_r_ocdclW_o:
  ‹ocdclW_o_r S T ⟹ enc_weight_opt.ocdclW_o S T›
  using S_Σ by (auto simp: ocdclW_o_r.simps enc_weight_opt.ocdclW_o.simps
      dest: odecide_decide)

lemma cdcl_bnb_r_cdcl_bnb:
  ‹cdcl_bnb_r S T ⟹ enc_weight_opt.cdcl_bnb S T›
  using S_Σ by (auto simp: cdcl_bnb_r.simps enc_weight_opt.cdcl_bnb.simps
      dest: ocdclW_o_r_ocdclW_o)

lemma cdcl_bnb_r_stgy_cdcl_bnb_stgy:
  ‹cdcl_bnb_r_stgy S T ⟹ enc_weight_opt.cdcl_bnb_stgy S T›
  using S_Σ by (auto simp: cdcl_bnb_r_stgy.simps enc_weight_opt.cdcl_bnb_stgy.simps
      dest: ocdclW_o_r_ocdclW_o)

end


context
  fixes S :: 'st
  assumes S_Σ: ‹atms_of_mm (init_clss S) = (Σ - ΔΣ) ∪ replacement_pos ` ΔΣ
     ∪ replacement_neg ` ΔΣ›
begin

lemma rtranclp_cdcl_bnb_r_cdcl_bnb:
  ‹cdcl_bnb_r** S T ⟹ enc_weight_opt.cdcl_bnb** S T›
  apply (induction rule: rtranclp_induct)
  subgoal by auto
  subgoal for T U
    using S_Σ enc_weight_opt.rtranclp_cdcl_bnb_no_more_init_clss[of S T]
    by(auto dest: cdcl_bnb_r_cdcl_bnb)
  done


lemma rtranclp_cdcl_bnb_r_stgy_cdcl_bnb_stgy:
  ‹cdcl_bnb_r_stgy** S T ⟹ enc_weight_opt.cdcl_bnb_stgy** S T›
  apply (induction rule: rtranclp_induct)
  subgoal by auto
  subgoal for T U
    using S_Σ
      enc_weight_opt.rtranclp_cdcl_bnb_no_more_init_clss[of S T,
        OF enc_weight_opt.rtranclp_cdcl_bnb_stgy_cdcl_bnb]
    by (auto dest: cdcl_bnb_r_stgy_cdcl_bnb_stgy)
  done


lemma rtranclp_cdcl_bnb_r_all_struct_inv:
  ‹cdcl_bnb_r** S T ⟹
    cdclW_restart_mset.cdclW_all_struct_inv (enc_weight_opt.abs_state S) ⟹
    cdclW_restart_mset.cdclW_all_struct_inv (enc_weight_opt.abs_state T)›
  using rtranclp_cdcl_bnb_r_cdcl_bnb[of T]
   enc_weight_opt.rtranclp_cdcl_bnb_stgy_all_struct_inv by blast

lemma rtranclp_cdcl_bnb_r_stgy_all_struct_inv:
  ‹cdcl_bnb_r_stgy** S T ⟹
    cdclW_restart_mset.cdclW_all_struct_inv (enc_weight_opt.abs_state S) ⟹
    cdclW_restart_mset.cdclW_all_struct_inv (enc_weight_opt.abs_state T)›
  using rtranclp_cdcl_bnb_r_stgy_cdcl_bnb_stgy[of T]
    enc_weight_opt.rtranclp_cdcl_bnb_stgy_all_struct_inv[of S T]
    enc_weight_opt.rtranclp_cdcl_bnb_stgy_cdcl_bnb[of S T]
  by auto

end

lemma no_step_cdcl_bnb_r_stgy_no_step_cdcl_bnb_stgy:
  assumes
    N: ‹init_clss S = penc N› and
    Σ: ‹atms_of_mm N = Σ› and
    n_d: ‹no_dup (trail S)› and
    tr_alien: ‹atm_of ` lits_of_l (trail S) ⊆ Σ ∪ replacement_pos ` ΔΣ ∪ replacement_neg ` ΔΣ›
  shows
    ‹no_step cdcl_bnb_r_stgy S ⟷ no_step enc_weight_opt.cdcl_bnb_stgy S› (is ‹?A ⟷ ?B›)
proof
  assume ?B
  then show ‹?A›
    using N cdcl_bnb_r_stgy_cdcl_bnb_stgy[of S] atms_of_mm_encode_clause_subset[of N]
      atms_of_mm_encode_clause_subset2[of N] finite_Σ ΔΣ_Σ
      atms_of_mm_penc_subset2[of N]
    by (auto simp: Σ)
next
  assume ?A
  then have
    nsd: ‹no_step odecide S› and
    nsp: ‹no_step propagate S› and
    nsc: ‹no_step conflict S› and
    nsi: ‹no_step enc_weight_opt.improvep S› and
    nsco: ‹no_step enc_weight_opt.conflict_opt S›
    by (auto simp: cdcl_bnb_r_stgy.simps ocdclW_o_r.simps)
  have
    nsi': ‹⋀M'. conflicting S = None ⟹ ¬enc_weight_opt.is_improving (trail S) M' S› and
    nsco': ‹conflicting S = None ⟹ negate_ann_lits (trail S) ∉# enc_weight_opt.conflicting_clss S›
    using nsi nsco unfolding enc_weight_opt.improvep.simps enc_weight_opt.conflict_opt.simps
    by auto
  have N_Σ: ‹atms_of_mm (penc N) =
    (Σ - ΔΣ) ∪ replacement_pos ` ΔΣ ∪ replacement_neg ` ΔΣ›
    using N Σ cdcl_bnb_r_stgy_cdcl_bnb_stgy[of S] atms_of_mm_encode_clause_subset[of N]
      atms_of_mm_encode_clause_subset2[of N] finite_Σ ΔΣ_Σ
      atms_of_mm_penc_subset2[of N]
    by auto
  have False if dec: ‹decide S T› for T
  proof -
    obtain L where
      [simp]: ‹conflicting S = None› and
      undef: ‹undefined_lit (trail S) L› and
      L: ‹atm_of L ∈ atms_of_mm (init_clss S)› and
      T: ‹T ∼ cons_trail (Decided L) S›
      using dec unfolding decide.simps
      by auto
    have 1: ‹atm_of L ∉ Σ - ΔΣ›
      using nsd L undef by (fastforce simp: odecide.simps N Σ)
    have 2: False if L: ‹atm_of L ∈ replacement_pos ` ΔΣ ∪
       replacement_neg ` ΔΣ›
    proof -
      obtain A where
        ‹A ∈ ΔΣ› and
        ‹atm_of L = replacement_pos A ∨ atm_of L = replacement_neg A› and
        ‹A ∈ Σ›
        using L ΔΣ_Σ by auto
      then show False
        using nsd L undef T N_Σ
        using odecide.intros(2-)[of S ‹A›]
        unfolding N Σ
        by (cases L) (auto 6 5 simp: defined_lit_Neg_Pos_iff Σ)
    qed
    have defined_replacement_pos: ‹defined_lit (trail S) (Pos (replacement_pos L))›
      if ‹L ∈ ΔΣ› for L
      using nsd that ΔΣ_Σ odecide.intros(2-)[of S ‹L›] by (auto simp: N Σ N_Σ)
    have defined_all: ‹defined_lit (trail S) L›
      if ‹atm_of L ∈ Σ - ΔΣ› for L
      using nsd that ΔΣ_Σ odecide.intros(1)[of S ‹L›] by (force simp: N Σ N_Σ)
    have defined_replacement_neg: ‹defined_lit (trail S) (Pos (replacement_neg L))›
      if ‹L ∈ ΔΣ› for L
      using nsd that ΔΣ_Σ odecide.intros(2-)[of S ‹L›] by (force simp: N Σ N_Σ)
    have [simp]: ‹{A ∈ ΔΣ. A ∈ Σ} = ΔΣ›
      using ΔΣ_Σ by auto
    have atms_tr': ‹Σ - ΔΣ ∪ replacement_pos ` ΔΣ ∪ replacement_neg ` ΔΣ ⊆
       atm_of ` (lits_of_l (trail S))›
      using N Σ cdcl_bnb_r_stgy_cdcl_bnb_stgy[of S] atms_of_mm_encode_clause_subset[of N]
        atms_of_mm_encode_clause_subset2[of N] finite_Σ ΔΣ_Σ
        defined_replacement_pos defined_replacement_neg defined_all
      unfolding N Σ N_Σ (*TODO proof*)
      apply (auto simp: Decided_Propagated_in_iff_in_lits_of_l)
        apply (metis image_eqI literal.sel(1) literal.sel(2) uminus_Pos)
       apply (metis image_eqI literal.sel(1) literal.sel(2))
      apply (metis image_eqI literal.sel(1) literal.sel(2))
      done
    then have atms_tr: ‹atms_of_mm (encode_clauses N) ⊆ atm_of ` (lits_of_l (trail S))›
      using N atms_of_mm_encode_clause_subset[of N]
        atms_of_mm_encode_clause_subset2[of N, OF finite_Σ] ΔΣ_Σ
      unfolding N Σ N_Σ ‹{A ∈ ΔΣ. A ∈ Σ} = ΔΣ›
      by (meson order_trans)
    show False
      by (metis L N N_Σ atm_lit_of_set_lits_of_l
        atms_tr' defined_lit_map subsetCE undef)
  qed
  then show ?B
    using ‹?A›
    by (auto simp: cdcl_bnb_r_stgy.simps enc_weight_opt.cdcl_bnb_stgy.simps
        ocdclW_o_r.simps enc_weight_opt.ocdclW_o.simps)
qed

lemma cdcl_bnb_r_stgy_init_clss:
  ‹cdcl_bnb_r_stgy S T ⟹ init_clss S = init_clss T›
  by (auto simp: cdcl_bnb_r_stgy.simps ocdclW_o_r.simps  enc_weight_opt.cdcl_bnb_bj.simps
      elim: conflictE propagateE enc_weight_opt.improveE enc_weight_opt.conflict_optE
      odecideE skipE resolveE enc_weight_opt.obacktrackE)

lemma rtranclp_cdcl_bnb_r_stgy_init_clss:
  ‹cdcl_bnb_r_stgy** S T ⟹ init_clss S = init_clss T›
  by  (induction rule: rtranclp_induct)(auto simp:  dest: cdcl_bnb_r_stgy_init_clss)

lemma [simp]:
  ‹enc_weight_opt.abs_state (init_state N) = abs_state (init_state N)›
  by (auto simp: enc_weight_opt.abs_state_def abs_state_def)

corollary
  assumes
    Σ: ‹atms_of_mm N = Σ› and dist: ‹distinct_mset_mset N› and
    ‹full cdcl_bnb_r_stgy (init_state (penc N)) T›
  shows
    ‹full enc_weight_opt.cdcl_bnb_stgy (init_state (penc N)) T›
proof -
  have [simp]: ‹atms_of_mm (CDCL_W_Abstract_State.init_clss (enc_weight_opt.abs_state T)) =
    atms_of_mm (init_clss T)›
    by (auto simp: enc_weight_opt.abs_state_def init_clss.simps)
  let ?S = ‹init_state (penc N)›
  have
    st: ‹cdcl_bnb_r_stgy** ?S T› and
    ns: ‹no_step cdcl_bnb_r_stgy T›
    using assms unfolding full_def by metis+
  have st': ‹enc_weight_opt.cdcl_bnb_stgy** ?S T›
    by (rule rtranclp_cdcl_bnb_r_stgy_cdcl_bnb_stgy[OF _ st])
      (use atms_of_mm_penc_subset2[of N] finite_Σ ΔΣ_Σ Σ in auto)
  have [simp]:
    ‹CDCL_W_Abstract_State.init_clss (abs_state (init_state (penc N))) =
      (penc N)›
    by (auto simp: abs_state_def init_clss.simps)
  have [iff]: ‹cdclW_restart_mset.cdclW_all_struct_inv (abs_state ?S)›
    using dist distinct_mset_penc[of N]
    by (auto simp: cdclW_restart_mset.cdclW_all_struct_inv_def
        cdclW_restart_mset.distinct_cdclW_state_def Σ
        cdclW_restart_mset.cdclW_learned_clause_alt_def)
  have ‹cdclW_restart_mset.cdclW_all_struct_inv (enc_weight_opt.abs_state T)›
    using enc_weight_opt.rtranclp_cdcl_bnb_stgy_all_struct_inv[of ?S T]
      enc_weight_opt.rtranclp_cdcl_bnb_stgy_cdcl_bnb[OF st']
    by auto
  then have alien: ‹cdclW_restart_mset.no_strange_atm (enc_weight_opt.abs_state T)› and
    lev: ‹cdclW_restart_mset.cdclW_M_level_inv (enc_weight_opt.abs_state T)›
    unfolding cdclW_restart_mset.cdclW_all_struct_inv_def
    by fast+
  have [simp]: ‹init_clss T = penc N›
    using rtranclp_cdcl_bnb_r_stgy_init_clss[OF st] by auto

  have ‹no_step enc_weight_opt.cdcl_bnb_stgy T›
    by (rule no_step_cdcl_bnb_r_stgy_no_step_cdcl_bnb_stgy[THEN iffD1, of _ N, OF _ _ _ _ ns])
      (use  alien atms_of_mm_penc_subset2[of N] finite_Σ ΔΣ_Σ lev
        in ‹auto simp: cdclW_restart_mset.no_strange_atm_def Σ
            cdclW_restart_mset.cdclW_M_level_inv_def›)
  then show ‹full enc_weight_opt.cdcl_bnb_stgy (init_state (penc N)) T›
    using st' unfolding full_def
    by auto
qed

lemma propagation_one_lit_of_same_lvl:
  assumes
    ‹cdclW_restart_mset.cdclW_all_struct_inv (abs_state S)› and
    ‹no_smaller_propa S› and
    ‹Propagated L E ∈ set (trail S)› and
    rea: ‹reasons_in_clauses S› and
    nempty: ‹E - {#L#} ≠ {#}›
  shows
    ‹∃L' ∈# E - {#L#}. get_level (trail S) L = get_level (trail S) L'›
proof (rule ccontr)
  assume H: ‹¬?thesis›
  have ns: ‹⋀M K M' D L.
       trail S = M' @ Decided K # M ⟹
       D + {#L#} ∈# clauses S ⟹ undefined_lit M L ⟹ ¬ M ⊨as CNot D› and
    n_d: ‹no_dup (trail S)›
    using assms unfolding no_smaller_propa_def
      cdclW_restart_mset.cdclW_all_struct_inv_def
      cdclW_restart_mset.cdclW_M_level_inv_def
    by auto
  obtain M1 M2 where M2: ‹trail S = M2 @ Propagated L E # M1›
    using assms by (auto dest!: split_list)

  have ‹⋀L mark a b.
         a @ Propagated L mark # b = trail S ⟹
         b ⊨as CNot (remove1_mset L mark) ∧ L ∈# mark› and
    ‹set (get_all_mark_of_propagated (trail S)) ⊆ set_mset (clauses S)›
    using assms unfolding cdclW_restart_mset.cdclW_all_struct_inv_def
      cdclW_restart_mset.cdclW_conflicting_def
      reasons_in_clauses_def
    by auto
  from this(1)[OF M2[symmetric]] this(2)
  have ‹M1 ⊨as CNot (remove1_mset L E)› and ‹L ∈# E› and ‹E ∈# clauses S›
    by (auto simp: M2)
  then have lev_le:
    ‹L' ∈# E - {#L#} ⟹ get_level (trail S) L > get_level (trail S) L'› and
    ‹trail S ⊨as CNot (remove1_mset L E)› for L'
    using H n_d defined_lit_no_dupD(1)[of M1 _ M2]
      count_decided_ge_get_level[of M1 L']
    by (auto simp: M2 get_level_append_if get_level_cons_if
        Decided_Propagated_in_iff_in_lits_of_l atm_of_eq_atm_of
        true_annots_append_l
        dest!: multi_member_split)
  define i where ‹i = get_level (trail S) L - 1›
  have ‹i < local.backtrack_lvl S› and ‹get_level (trail S) L ≥ 1›
    ‹get_level (trail S) L > i› and
    i2: ‹get_level (trail S) L = Suc i›
    using lev_le nempty count_decided_ge_get_level[of ‹trail S› L] i_def
    by (cases ‹E - {#L#}›; force)+
  from backtrack_ex_decomp[OF n_d this(1)] obtain M3 M4 K where
    decomp: ‹(Decided K # M3, M4) ∈ set (get_all_ann_decomposition (trail S))› and
    lev_K: ‹get_level (trail S) K = Suc i›
    by blast
  then obtain M5 where
    tr: ‹trail S = (M5 @ M4) @ Decided K # M3›
    by auto
  define M4' where ‹M4' = M5 @ M4›
  have ‹undefined_lit M3 L›
    using n_d ‹get_level (trail S) L > i› lev_K
      count_decided_ge_get_level[of M3 L] unfolding tr M4'_def[symmetric]
    by (auto simp: get_level_append_if get_level_cons_if
        atm_of_eq_atm_of
        split: if_splits dest: defined_lit_no_dupD)
  moreover have ‹M3 ⊨as CNot (remove1_mset L E)›
    using ‹trail S ⊨as CNot (remove1_mset L E)› lev_K n_d
    unfolding true_annots_def true_annot_def
    apply clarsimp
    subgoal for L'
      using lev_le[of ‹-L'›] lev_le[of ‹L'›] lev_K
      unfolding i2
      unfolding  tr M4'_def[symmetric]
      by (auto simp: get_level_append_if get_level_cons_if
          atm_of_eq_atm_of if_distrib if_distribR Decided_Propagated_in_iff_in_lits_of_l
          split: if_splits dest: defined_lit_no_dupD
          dest!: multi_member_split)
    done
  ultimately show False
    using ns[OF tr, of ‹remove1_mset L E› L] ‹E ∈# clauses S› ‹L ∈# E›
    by auto
qed


lemma simple_backtrack_obacktrack:
  ‹simple_backtrack S T ⟹ cdclW_restart_mset.cdclW_all_struct_inv (enc_weight_opt.abs_state S) ⟹
    enc_weight_opt.obacktrack S T›
  unfolding cdclW_restart_mset.cdclW_all_struct_inv_def
    cdclW_restart_mset.cdclW_conflicting_def
    cdclW_restart_mset.cdclW_learned_clause_alt_def
  apply (auto simp: simple_backtrack.simps
      enc_weight_opt.obacktrack.simps)
  apply (rule_tac x=L in exI)
  apply (rule_tac x=D in exI)
  apply auto
  apply (rule_tac x=K in exI)
  apply (rule_tac x=M1 in exI)
  apply auto
  apply (rule_tac x=D in exI)
  apply (auto simp:)
  done

end

interpretation test_real: optimal_encoding_opt where
  state_eq = ‹(=)› and
  state = id and
  trail = ‹λ(M, N, U, D, W). M› and
  init_clss = ‹λ(M, N, U, D, W). N› and
  learned_clss = ‹λ(M, N, U, D, W). U› and
  conflicting = ‹λ(M, N, U, D, W). D› and
  cons_trail = ‹λK (M, N, U, D, W). (K # M, N, U, D, W)› and
  tl_trail = ‹λ(M, N, U, D, W). (tl M, N, U, D, W)› and
  add_learned_cls = ‹λC (M, N, U, D, W). (M, N, add_mset C U, D, W)› and
  remove_cls = ‹λC (M, N, U, D, W). (M, removeAll_mset C N, removeAll_mset C U, D, W)› and
  update_conflicting = ‹λC (M, N, U, _, W). (M, N, U, C, W)› and
  init_state = ‹λN. ([], N, {#}, None, None, ())› and
  ρ = ‹λ_. (0::real)› and
  update_additional_info = ‹λW (M, N, U, D, _, _). (M, N, U, D, W)› and
  Σ = ‹{1..(100::nat)}› and
  ΔΣ = ‹{1..(50::nat)}› and
  new_vars = ‹λn. (200 + 2*n, 200 + 2*n+1)›
  by unfold_locales

lemma mult3_inj:
  ‹2 * A = Suc (2 * Aa) ⟷ False› for A Aa::nat
  by presburger+

interpretation test_real: optimal_encoding where
  state_eq = ‹(=)› and
  state = id and
  trail = ‹λ(M, N, U, D, W). M› and
  init_clss = ‹λ(M, N, U, D, W). N› and
  learned_clss = ‹λ(M, N, U, D, W). U› and
  conflicting = ‹λ(M, N, U, D, W). D› and
  cons_trail = ‹λK (M, N, U, D, W). (K # M, N, U, D, W)› and
  tl_trail = ‹λ(M, N, U, D, W). (tl M, N, U, D, W)› and
  add_learned_cls = ‹λC (M, N, U, D, W). (M, N, add_mset C U, D, W)› and
  remove_cls = ‹λC (M, N, U, D, W). (M, removeAll_mset C N, removeAll_mset C U, D, W)› and
  update_conflicting = ‹λC (M, N, U, _, W). (M, N, U, C, W)› and
  init_state = ‹λN. ([], N, {#}, None, None, ())› and
  ρ = ‹λ_. (0::real)› and
  update_additional_info = ‹λW (M, N, U, D, _, _). (M, N, U, D, W)› and
  Σ = ‹{1..(100::nat)}› and
  ΔΣ = ‹{1..(50::nat)}› and
  new_vars = ‹λn. (200 + 2*n, 200 + 2*n+1)›
  by unfold_locales (auto simp: inj_on_def mult3_inj)

interpretation test_nat: optimal_encoding_opt where
  state_eq = ‹(=)› and
  state = id and
  trail = ‹λ(M, N, U, D, W). M› and
  init_clss = ‹λ(M, N, U, D, W). N› and
  learned_clss = ‹λ(M, N, U, D, W). U› and
  conflicting = ‹λ(M, N, U, D, W). D› and
  cons_trail = ‹λK (M, N, U, D, W). (K # M, N, U, D, W)› and
  tl_trail = ‹λ(M, N, U, D, W). (tl M, N, U, D, W)› and
  add_learned_cls = ‹λC (M, N, U, D, W). (M, N, add_mset C U, D, W)› and
  remove_cls = ‹λC (M, N, U, D, W). (M, removeAll_mset C N, removeAll_mset C U, D, W)› and
  update_conflicting = ‹λC (M, N, U, _, W). (M, N, U, C, W)› and
  init_state = ‹λN. ([], N, {#}, None, None, ())› and
  ρ = ‹λ_. (0::nat)› and
  update_additional_info = ‹λW (M, N, U, D, _, _). (M, N, U, D, W)› and
  Σ = ‹{1..(100::nat)}› and
  ΔΣ = ‹{1..(50::nat)}› and
  new_vars = ‹λn. (200 + 2*n, 200 + 2*n+1)›
  by unfold_locales

interpretation test_nat: optimal_encoding where
  state_eq = ‹(=)› and
  state = id and
  trail = ‹λ(M, N, U, D, W). M› and
  init_clss = ‹λ(M, N, U, D, W). N› and
  learned_clss = ‹λ(M, N, U, D, W). U› and
  conflicting = ‹λ(M, N, U, D, W). D› and
  cons_trail = ‹λK (M, N, U, D, W). (K # M, N, U, D, W)› and
  tl_trail = ‹λ(M, N, U, D, W). (tl M, N, U, D, W)› and
  add_learned_cls = ‹λC (M, N, U, D, W). (M, N, add_mset C U, D, W)› and
  remove_cls = ‹λC (M, N, U, D, W). (M, removeAll_mset C N, removeAll_mset C U, D, W)› and
  update_conflicting = ‹λC (M, N, U, _, W). (M, N, U, C, W)› and
  init_state = ‹λN. ([], N, {#}, None, None, ())› and
  ρ = ‹λ_. (0::nat)› and
  update_additional_info = ‹λW (M, N, U, D, _, _). (M, N, U, D, W)› and
  Σ = ‹{1..(100::nat)}› and
  ΔΣ = ‹{1..(50::nat)}› and
  new_vars = ‹λn. (200 + 2*n, 200 + 2*n+1)›
  by unfold_locales (auto simp: inj_on_def mult3_inj)


end