Theory CDCL.CDCL_W_Merge

(* Title: Merging some rules of Weidenbach's CDCL
    Author: Mathias Fleury <mathias.fleury@mpi-inf.mpg.de>
*)

section Merging backjump rules

theory CDCL_W_Merge
imports CDCL_W
begin

text Before showing that Weidenbach's CDCL is included in NOT's CDCL, we need to work on a variant
  of Weidenbach's calculus: NOT's backjump assumes the existence of a clause that is suitable to
  backjump. This clause is obtained in W's CDCL by applying:
     @{term conflict_driven_clause_learningW.conflict} to find the conflict
     the conflict is analysed by repetitive application of
      @{term conflict_driven_clause_learningW.resolve} and
      @{term conflict_driven_clause_learningW.skip},
     finally @{term conflict_driven_clause_learningW.backtrack} is used to backtrack.

  We show that this new calculus has the same final states than Weidenbach's CDCL if the calculus
  starts in a state such that the invariant holds and no conflict has been found yet. The latter
  condition holds for initial states.

subsection Inclusion of the States

context conflict_driven_clause_learningW
begin

declare cdclW_restart.intros[intro] cdclW_bj.intros[intro] cdclW_o.intros[intro]
state_prop [simp del]

lemma backtrack_no_cdclW_bj:
  assumes cdcl: "cdclW_bj T U"
  shows "¬backtrack V T"
  using cdcl
  apply (induction rule: cdclW_bj.induct)
    apply (elim skipE, force elim!: backtrackE simp: cdclW_M_level_inv_def)
   apply (elim resolveE, force elim!: backtrackE simp: cdclW_M_level_inv_def)
  apply standard
  apply (elim backtrackE)
  apply (force simp add: cdclW_M_level_inv_decomp)
  done

text @{term skip_or_resolve} corresponds to the analyze function in the code of MiniSAT.
inductive skip_or_resolve :: "'st  'st  bool" where
s_or_r_skip[intro]: "skip S T  skip_or_resolve S T" |
s_or_r_resolve[intro]: "resolve S T  skip_or_resolve S T"

lemma rtranclp_cdclW_bj_skip_or_resolve_backtrack:
  assumes "cdclW_bj** S U"
  shows "skip_or_resolve** S U  (T. skip_or_resolve** S T  backtrack T U)"
  using assms
proof induction
  case base
  then show ?case by simp
next
  case (step U V) note st = this(1) and bj = this(2) and IH = this(3)
  consider
      (SU) "S = U"
    | (SUp) "cdclW_bj++ S U"
    using st unfolding rtranclp_unfold by blast
  then show ?case
  proof cases
    case SUp
    have "T. skip_or_resolve** S T  cdclW_restart** S T"
      using mono_rtranclp[of skip_or_resolve cdclW_restart]
      by (blast intro: skip_or_resolve.cases)
    then have "skip_or_resolve** S U"
      using bj IH backtrack_no_cdclW_bj by meson
    then show ?thesis
      using bj by (auto simp: cdclW_bj.simps dest!: skip_or_resolve.intros)
  next
    case SU
    then show ?thesis
      using bj by (auto simp: cdclW_bj.simps dest!: skip_or_resolve.intros)
  qed
qed

lemma rtranclp_skip_or_resolve_rtranclp_cdclW_restart:
  "skip_or_resolve** S T  cdclW_restart** S T"
  by (induction rule: rtranclp_induct)
    (auto dest!: cdclW_bj.intros cdclW_restart.intros cdclW_o.intros simp: skip_or_resolve.simps)

definition backjump_l_cond :: "'v clause  'v clause  'v literal  'st  'st  bool" where
"backjump_l_cond  λC C' L S T. True"

lemma wf_skip_or_resolve:
  "wf {(T, S). skip_or_resolve S T}"
proof -
  have "skip_or_resolve x y  length (trail y) < length (trail x)" for x y
    by (auto simp: skip_or_resolve.simps elim!: skipE resolveE)
  then show ?thesis
    using wfP_if_measure[of "λ_. True" skip_or_resolve "λS. length (trail S)"]
    by meson
qed

definition invNOT :: "'st  bool" where
"invNOT  λS. no_dup (trail S)"

declare invNOT_def[simp]
end

context conflict_driven_clause_learningW
begin

subsection More lemmas about Conflict, Propagate and Backjumping

subsubsection Termination

lemma cdclW_bj_measure:
  assumes "cdclW_bj S T"
  shows "length (trail S) + (if conflicting S = None then 0 else 1)
    > length (trail T) + (if conflicting T = None then 0 else 1)"
  using assms by (induction rule: cdclW_bj.induct) (force elim!: backtrackE skipE resolveE)+

lemma wf_cdclW_bj:
  "wf {(b,a). cdclW_bj a b}"
  apply (rule wfP_if_measure[of "λ_. True"
      _ "λT. length (trail T) + (if conflicting T = None then 0 else 1)", simplified])
  using cdclW_bj_measure by simp

lemma cdclW_bj_exists_normal_form:
  shows "T. full cdclW_bj S T"
  using wf_exists_normal_form_full[OF wf_cdclW_bj] .

lemma rtranclp_skip_state_decomp:
  assumes "skip** S T"
  shows
    "M. trail S = M @ trail T  (mset M. ¬is_decided m)"
    "init_clss S = init_clss T"
    "learned_clss S = learned_clss T"
    "backtrack_lvl S = backtrack_lvl T"
    "conflicting S = conflicting T"
  using assms by (induction rule: rtranclp_induct) (auto elim!: skipE)


subsubsection Analysing is confluent

lemma backtrack_reduce_trail_to_state_eq:
  assumes
    V_T: V  tl_trail T and
    decomp: (Decided K # M1, M2)  set (get_all_ann_decomposition (trail V))
  shows reduce_trail_to M1 (add_learned_cls E (update_conflicting None V))
     reduce_trail_to M1 (add_learned_cls E (update_conflicting None T))
proof -
  let ?f = λT. add_learned_cls E (update_conflicting None T)
  have [simp]: length (trail T)  length M1 trail T  []
    using decomp V_T by (cases trail T; auto)+
  have reduce_trail_to M1 (?f V)  reduce_trail_to M1 (?f (tl_trail T))
    apply (rule reduce_trail_to_state_eq)
    using V_T by (simp_all add: add_learned_cls_state_eq update_conflicting_state_eq)
  moreover {
    have add_learned_cls E (update_conflicting None (tl_trail T)) 
      tl_trail (add_learned_cls E (update_conflicting None T))
      apply (rule state_eq_trans[OF state_eq_sym[THEN iffD1], of
            add_learned_cls E (tl_trail (update_conflicting None T))])
       apply (auto simp: tl_trail_update_conflicting tl_trail_add_learned_cls_commute
          update_conflicting_state_eq add_learned_cls_state_eq tl_trail_state_eq; fail)[]
      apply (rule state_eq_trans[OF state_eq_sym[THEN iffD1], of
            add_learned_cls E (tl_trail (update_conflicting None T))])
       apply (auto simp: tl_trail_update_conflicting tl_trail_add_learned_cls_commute
          update_conflicting_state_eq add_learned_cls_state_eq tl_trail_state_eq; fail)[]
      apply (rule state_eq_trans[OF state_eq_sym[THEN iffD1], of
            tl_trail (add_learned_cls E (update_conflicting None T))])
       apply (auto simp: tl_trail_update_conflicting tl_trail_add_learned_cls_commute
          update_conflicting_state_eq add_learned_cls_state_eq tl_trail_state_eq)
      done
    note _ = reduce_trail_to_state_eq[OF this, of M1 M1]}
  ultimately show reduce_trail_to M1 (?f V)  reduce_trail_to M1 (?f T)
    by (subst (2) reduce_trail_to.simps)
      (auto simp: tl_trail_update_conflicting tl_trail_add_learned_cls_commute intro: state_eq_trans)
qed

lemma rtranclp_skip_backtrack_reduce_trail_to_state_eq:
  assumes
    V_T: skip** T V and
    decomp: (Decided K # M1, M2)  set (get_all_ann_decomposition (trail V))
  shows reduce_trail_to M1 (add_learned_cls E (update_conflicting None T))
     reduce_trail_to M1 (add_learned_cls E (update_conflicting None V))
  using V_T decomp
proof (induction arbitrary: M2 rule: rtranclp_induct)
  case base
  then show ?case by auto
next
  case (step U V) note st = this(1) and skip = this(2) and IH = this(3) and decomp = this(4)
  obtain M2' where
    decomp': (Decided K # M1, M2')  set (get_all_ann_decomposition (trail U))
    using get_all_ann_decomposition_exists_prepend[OF decomp] skip
    by atomize (auto elim!: rulesE simp del: get_all_ann_decomposition.simps
        simp: Decided_cons_in_get_all_ann_decomposition_append_Decided_cons
        append_Cons[symmetric] append_assoc[symmetric]
        simp del: append_Cons append_assoc)
  show ?case
    using backtrack_reduce_trail_to_state_eq[OF _ decomp, of U E] skip IH[OF decomp']
    by (auto elim!: skipE simp del: get_all_ann_decomposition.simps intro: state_eq_trans')
qed

paragraph Backjumping after skipping or jump directly
lemma rtranclp_skip_backtrack_backtrack:
  assumes
    "skip** S T" and
    "backtrack T W" and
    "cdclW_all_struct_inv S"
  shows "backtrack S W"
  using assms
proof induction
  case base
  then show ?case by simp
next
  case (step T V) note st = this(1) and skip = this(2) and IH = this(3) and bt = this(4) and
    inv = this(5)
  have "skip** S V"
    using st skip by auto
  then have "cdclW_all_struct_inv V"
    using rtranclp_mono[of skip cdclW_restart] assms(3) rtranclp_cdclW_all_struct_inv_inv mono_rtranclp
    by (auto dest!: bj other cdclW_bj.skip)
  then have "cdclW_M_level_inv V"
    unfolding cdclW_all_struct_inv_def by auto
  then obtain K i M1 M2 L D D' where
    conf: "conflicting V = Some (add_mset L D)" and
    decomp: "(Decided K # M1, M2)  set (get_all_ann_decomposition (trail V))" and
    lev_L: "get_level (trail V) L = backtrack_lvl V" and
    max: "get_level (trail V) L = get_maximum_level (trail V) (add_mset L D')" and
    max_D: "get_maximum_level (trail V) D'  i" and
    lev_k: "get_level (trail V) K = Suc i" and
    W: "W  cons_trail (Propagated L (add_mset L D'))
                (reduce_trail_to M1
                  (add_learned_cls (add_mset L D')
                    (update_conflicting None V)))" and
    D_D': D' ⊆# D and
    NU_D': clauses V ⊨pm add_mset L D'
    using bt inv by (elim backtrackE) metis
  obtain L' C' M E where
    tr: "trail T = Propagated L' C' # M" and
    raw: "conflicting T = Some E" and
    LE: "-L' ∉# E" and
    E: "E  {#}" and
    V: "V  tl_trail T"
    using skip by (elim skipE) metis
  let ?M = "Propagated L' C' # M"
  have tr_M: "trail T = ?M"
    using tr V by auto
  have MT: "M = tl (trail T)" and MV: "M = trail V"
    using tr V by auto
  have DE[simp]: "E = add_mset L D"
    using V conf raw by auto
  have "cdclW_restart** S T"
    using bj cdclW_bj.skip mono_rtranclp[of skip cdclW_restart S T] other st by meson
  then have inv': "cdclW_all_struct_inv T"
    using rtranclp_cdclW_all_struct_inv_inv inv by blast
  have M_lev: "cdclW_M_level_inv T" using inv' unfolding cdclW_all_struct_inv_def by auto
  then have n_d': "no_dup ?M"
    using tr_M unfolding cdclW_M_level_inv_def by auto
  let ?k = "backtrack_lvl T"
  have [simp]:
    "backtrack_lvl V = ?k"
    using V tr_M by simp
  have "?k > 0"
    using decomp M_lev V tr unfolding cdclW_M_level_inv_def by auto
  then have "atm_of L  atm_of ` lits_of_l (trail V)"
    using lev_L get_level_ge_0_atm_of_in[of 0 "trail V" L] by auto
  then have L_L': "atm_of L  atm_of L'"
    using n_d' unfolding lits_of_def MV by (auto simp: defined_lit_map)
  have L'_M: "undefined_lit M L'"
    using n_d' unfolding lits_of_def by auto
  have "?M ⊨as CNot D"
    using inv' raw unfolding cdclW_conflicting_def cdclW_all_struct_inv_def tr_M by auto
  then have "L' ∉# D"
    using L_L' L'_M unfolding true_annots_true_cls true_clss_def
    by (auto simp: uminus_lit_swap atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set defined_lit_map
      lits_of_def dest!: in_diffD)
  have [simp]: "trail (reduce_trail_to M1 T) = M1"
    using decomp tr W V by auto
  have "skip** S V"
    using st skip by auto
  have "no_dup (trail S)"
    using inv unfolding cdclW_all_struct_inv_def cdclW_M_level_inv_def by auto
  then have [simp]: "init_clss S = init_clss V" and [simp]: "learned_clss S = learned_clss V"
    using rtranclp_skip_state_decomp[OF skip** S V] V by auto
  have V_T: V  tl_trail T
    using skip by (auto elim: rulesE)
  have
    W_S: "W  cons_trail (Propagated L (add_mset L D')) (reduce_trail_to M1
     (add_learned_cls (add_mset L D') (update_conflicting None T)))"
    apply (rule state_eq_trans[OF W])
    unfolding DE
    apply (rule cons_trail_state_eq)
    apply (rule backtrack_reduce_trail_to_state_eq)
    using V decomp by auto
  have atm_of_L'_D': "atm_of L'  atms_of D'"
    by (metis DE LE D' ⊆# D L' ∉# D atm_of_in_atm_of_set_in_uminus atms_of_def insert_iff
        mset_subset_eqD set_mset_add_mset_insert)

  obtain M2' where
    decomp': "(Decided K # M1, M2')  set (get_all_ann_decomposition (trail T))"
    using decomp V unfolding tr_M MV by (cases "hd (get_all_ann_decomposition (trail V))",
      cases "get_all_ann_decomposition (trail V)") auto
  moreover from L_L' have "get_level ?M L = ?k"
      using lev_L V tr_M by (auto split: if_split_asm)
  moreover have "get_level ?M L = get_maximum_level ?M (add_mset L D')"
    using count_decided_ge_get_maximum_level[of trail V D'] calculation(2) lev_L max MV atm_of_L'_D'
    unfolding get_maximum_level_add_mset
    by auto
  moreover have "i = get_maximum_level ?M D'"
    using max_D MV atm_of_L'_D' by auto
  moreover have "atm_of L'  atm_of K"
    using inv' get_all_ann_decomposition_exists_prepend[OF decomp]
    unfolding cdclW_all_struct_inv_def cdclW_M_level_inv_def tr MV by (auto simp: defined_lit_map)
  ultimately have "backtrack T W"
    apply -
    apply (rule backtrack_rule[of T L D K M1 M2' D' i])
    unfolding tr_M[symmetric]
    subgoal using raw by (simp; fail)
    subgoal by (simp; fail)
    subgoal by (simp; fail)
    subgoal by (simp; fail)
    subgoal by (simp; fail)
    subgoal using lev_k tr unfolding MV[symmetric] by (auto; fail)[]
    subgoal using D_D' by (simp; fail)
    subgoal using NU_D' V_T by (simp; fail)
    subgoal using W_S lev_k by (auto; fail)[]
    done
  then show ?thesis using IH inv by blast
qed


text See also theorem @{thm [source] rtranclp_skip_backtrack_backtrack}
lemma rtranclp_skip_backtrack_backtrack_end:
  assumes
    skip: "skip** S T" and
    bt: "backtrack S W" and
    inv: "cdclW_all_struct_inv S"
  shows "backtrack T W"
  using assms
proof -
  have M_lev: "cdclW_M_level_inv S "
    using bt inv unfolding cdclW_all_struct_inv_def by (auto elim!: backtrackE)
  then obtain K i M1 M2 L D D' where
    S: "conflicting S = Some (add_mset L D)" and
    decomp: "(Decided K # M1, M2)  set (get_all_ann_decomposition (trail S))" and
    lev_l: "get_level (trail S) L = backtrack_lvl S" and
    lev_l_D: "get_level (trail S) L = get_maximum_level (trail S) (add_mset L D')" and
    i: "get_maximum_level (trail S) D'  i" and
    lev_K: "get_level (trail S) K = Suc i" and
    W: "W  cons_trail (Propagated L (add_mset L D'))
                (reduce_trail_to M1
                  (add_learned_cls (add_mset L D')
                    (update_conflicting None S)))" and
    D_D': D' ⊆# D and
    NU_D': clauses S ⊨pm add_mset L D'
    using bt by (elim backtrackE) metis
  let ?D = "add_mset L D"
  let ?D' = "add_mset L D'"

  have [simp]: "no_dup (trail S)"
    using M_lev by (auto simp: cdclW_M_level_inv_decomp)
  have "cdclW_all_struct_inv T"
    using mono_rtranclp[of skip cdclW_restart] by (smt bj cdclW_bj.skip inv local.skip other
      rtranclp_cdclW_all_struct_inv_inv)
  then have [simp]: "no_dup (trail T)"
    unfolding cdclW_all_struct_inv_def cdclW_M_level_inv_def by auto
  (* MT is a proxy to allow auto to unfold T*)
  obtain MS MT where M: "trail S = MS @ MT" and MT: "MT = trail T" and nm: "mset MS. ¬is_decided m"
    using rtranclp_skip_state_decomp(1)[OF skip] S by auto
  have T: "state_butlast T = (MT, init_clss S, learned_clss S, Some (add_mset L D))" and
    bt_S_T: "backtrack_lvl S = backtrack_lvl T" and
    clss_S_T: clauses S = clauses T
    using MT rtranclp_skip_state_decomp[of S T] skip S by (auto simp: clauses_def)

  have "cdclW_all_struct_inv T"
    apply (rule rtranclp_cdclW_all_struct_inv_inv[OF _ inv])
    using bj cdclW_bj.skip local.skip other rtranclp_mono[of skip cdclW_restart] by blast
  then have "MT ⊨as CNot ?D"
    unfolding cdclW_all_struct_inv_def cdclW_conflicting_def using T by auto
  then have "L'∈#?D. defined_lit MT L'"
    using Decided_Propagated_in_iff_in_lits_of_l
    by (auto dest: true_annots_CNot_definedD)
  moreover have "no_dup (trail S)"
    using inv unfolding cdclW_all_struct_inv_def cdclW_M_level_inv_def by auto
  ultimately have undef_D: "L'∈#?D. undefined_lit MS L'"
    unfolding M by (auto dest: defined_lit_no_dupD)
  then have H: "L'. L'∈# D  get_level (trail S) L' = get_level MT L'"
     "get_level (trail S) L = get_level MT L"
    unfolding M by (auto simp: lits_of_def)
  have [simp]: "get_maximum_level (trail S) D = get_maximum_level MT D"
    using MT ⊨as CNot (add_mset L D) M nm undef_D by (auto simp: get_maximum_level_skip_beginning)

  have lev_l': "get_level MT L = backtrack_lvl S"
    using lev_l nm by (auto simp: H)
  have [simp]: "trail (reduce_trail_to M1 T) = M1"
    by (metis (no_types) M MT append_assoc get_all_ann_decomposition_exists_prepend[OF decomp] nm
        reduce_trail_to_trail_tl_trail_decomp beginning_not_decided_invert)
  obtain c where c: MT = c @ Decided K # M1
    using nm decomp by (auto dest!: get_all_ann_decomposition_exists_prepend
        simp: MT[symmetric] M append_assoc[symmetric]
        simp del: append_assoc
        dest!: beginning_not_decided_invert)
  obtain c'' where
    c'': (Decided K # M1, c'')  set (get_all_ann_decomposition (c @ Decided K # M1))
    using Decided_cons_in_get_all_ann_decomposition_append_Decided_cons[of K M1]  by blast
  have W: "W  cons_trail (Propagated L (add_mset L D')) (reduce_trail_to M1
    (add_learned_cls (add_mset L D') (update_conflicting None T)))"
    apply (rule state_eq_trans[OF W])
    apply (rule cons_trail_state_eq)
    apply (rule rtranclp_skip_backtrack_reduce_trail_to_state_eq[of _ _ K M1])
    using skip apply (simp; fail)
    using c'' by (auto simp: MT[symmetric] M c)
  have max_trail_S_MT_L_D': get_maximum_level (trail S) ?D' = get_maximum_level MT ?D'
    by (rule get_maximum_level_cong) (use H D_D' in auto)
  then have lev_l_D': "get_level MT L = get_maximum_level MT ?D'"
    using lev_l_D H by auto
  have i': "i = get_maximum_level MT D'"
    unfolding i[symmetric]
    by (rule get_maximum_level_cong) (use H D_D' in auto)
  have "Decided K # M1  set (map fst (get_all_ann_decomposition (trail S)))"
    using Set.imageI[OF decomp, of fst] by auto
  then have "Decided K # M1  set (map fst (get_all_ann_decomposition MT))"
    using fst_get_all_ann_decomposition_prepend_not_decided[OF nm] unfolding M by auto
  then obtain M2' where decomp': "(Decided K # M1, M2')  set (get_all_ann_decomposition MT)"
    by auto
  moreover {
    have "undefined_lit MS K"
      using no_dup (trail S) decomp' unfolding M MT
      by (auto simp: lits_of_def defined_lit_map no_dup_def)
    then have "get_level (trail T) K = get_level (trail S) K"
      unfolding M MT by auto }
  ultimately show "backtrack T W"
    apply -
    apply (rule backtrack.intros[of T L D K M1 M2' D' i])
    subgoal using T by auto
    subgoal using T by auto
    subgoal using T lev_l' lev_l_D' bt_S_T by auto
    subgoal using T lev_l_D' bt_S_T by auto
    subgoal using i' W lev_K unfolding MT[symmetric] clss_S_T by auto
    subgoal using lev_K unfolding MT[symmetric] clss_S_T by auto
    subgoal using D_D' .
    subgoal using NU_D' unfolding clss_S_T .
    subgoal using W unfolding i'[symmetric] by auto
    done
qed

lemma cdclW_bj_decomp_resolve_skip_and_bj:
  assumes "cdclW_bj** S T"
  shows "(skip_or_resolve** S T
     (U. skip_or_resolve** S U  backtrack U T))"
  using assms
proof induction
  case base
  then show ?case by simp
next
  case (step T U) note st = this(1) and bj = this(2) and IH = this(3)
  have IH: "skip_or_resolve** S T"
  proof -
    { assume "U. skip_or_resolve** S U  backtrack U T"
      then obtain V where
        bt: "backtrack V T" and
        "skip_or_resolve** S V"
        by blast
      then have "cdclW_restart** S V"
        using rtranclp_skip_or_resolve_rtranclp_cdclW_restart by blast
      with bj bt have False using backtrack_no_cdclW_bj by simp
    }
    then show ?thesis using IH by blast
  qed
  show ?case
    using bj
    proof (cases rule: cdclW_bj.cases)
      case backtrack
      then show ?thesis using IH by blast
    qed (metis (no_types, lifting) IH rtranclp.simps skip_or_resolve.simps)+
qed


subsection CDCL with Merging

inductive cdclW_merge_restart :: "'st  'st  bool" where
fw_r_propagate: "propagate S S'  cdclW_merge_restart S S'" |
fw_r_conflict: "conflict S T  full cdclW_bj T U  cdclW_merge_restart S U" |
fw_r_decide: "decide S S'  cdclW_merge_restart S S'"|
fw_r_rf: "cdclW_rf S S'  cdclW_merge_restart S S'"

lemma rtranclp_cdclW_bj_rtranclp_cdclW_restart:
  "cdclW_bj** S T  cdclW_restart** S T"
  using mono_rtranclp[of cdclW_bj cdclW_restart] by blast

lemma cdclW_merge_restart_cdclW_restart:
  assumes "cdclW_merge_restart S T"
  shows "cdclW_restart** S T"
  using assms
proof induction
  case (fw_r_conflict S T U) note confl = this(1) and bj = this(2)
  have "cdclW_restart S T" using confl by (simp add: cdclW_restart.intros r_into_rtranclp)
  moreover
    have "cdclW_bj** T U" using bj unfolding full_def by auto
    then have "cdclW_restart** T U" using rtranclp_cdclW_bj_rtranclp_cdclW_restart by blast
  ultimately show ?case by auto
qed (simp_all add: cdclW_o.intros cdclW_restart.intros r_into_rtranclp)

lemma cdclW_merge_restart_conflicting_true_or_no_step:
  assumes "cdclW_merge_restart S T"
  shows "conflicting T = None  no_step cdclW_restart T"
  using assms
proof induction
  case (fw_r_conflict S T U) note confl = this(1) and n_s = this(2)
  { fix D V
    assume "cdclW_restart U V" and "conflicting U = Some D"
    then have False
      using n_s unfolding full_def
      by (induction rule: cdclW_restart_all_rules_induct)
        (auto dest!: cdclW_bj.intros elim: decideE propagateE conflictE forgetE restartE)
  }
  then show ?case by (cases "conflicting U") fastforce+
qed (auto simp add: cdclW_rf.simps elim: propagateE decideE restartE forgetE)

inductive cdclW_merge :: "'st  'st  bool" where
fw_propagate: "propagate S S'  cdclW_merge S S'" |
fw_conflict: "conflict S T  full cdclW_bj T U  cdclW_merge S U" |
fw_decide: "decide S S'  cdclW_merge S S'"|
fw_forget: "forget S S'  cdclW_merge S S'"

lemma cdclW_merge_cdclW_merge_restart:
  "cdclW_merge S T  cdclW_merge_restart S T"
  by (meson cdclW_merge.cases cdclW_merge_restart.simps forget)

lemma rtranclp_cdclW_merge_tranclp_cdclW_merge_restart:
  "cdclW_merge** S T  cdclW_merge_restart** S T"
  using rtranclp_mono[of cdclW_merge cdclW_merge_restart] cdclW_merge_cdclW_merge_restart by blast

lemma cdclW_merge_rtranclp_cdclW_restart:
  "cdclW_merge S T  cdclW_restart** S T"
  using cdclW_merge_cdclW_merge_restart cdclW_merge_restart_cdclW_restart by blast

lemma rtranclp_cdclW_merge_rtranclp_cdclW_restart:
  "cdclW_merge** S T  cdclW_restart** S T"
  using rtranclp_mono[of cdclW_merge "cdclW_restart**"] cdclW_merge_rtranclp_cdclW_restart by auto

lemma cdclW_all_struct_inv_tranclp_cdclW_merge_tranclp_cdclW_merge_cdclW_all_struct_inv:
  assumes
    inv: "cdclW_all_struct_inv b"
    "cdclW_merge++ b a"
  shows "(λS T. cdclW_all_struct_inv S  cdclW_merge S T)++ b a"
  using assms(2)
proof induction
  case base
  then show ?case using inv by auto
next
  case (step c d) note st = this(1) and fw = this(2) and IH = this(3)
  have "cdclW_all_struct_inv c"
    using tranclp_into_rtranclp[OF st] cdclW_merge_rtranclp_cdclW_restart assms(1)
    rtranclp_cdclW_all_struct_inv_inv rtranclp_mono[of cdclW_merge "cdclW_restart**"] by fastforce
  then have "(λS T. cdclW_all_struct_inv S  cdclW_merge S T)++ c d"
    using fw by auto
  then show ?case using IH by auto
qed

lemma backtrack_is_full1_cdclW_bj:
  assumes bt: "backtrack S T"
  shows "full1 cdclW_bj S T"
  using bt backtrack_no_cdclW_bj unfolding full1_def by blast

lemma rtrancl_cdclW_conflicting_true_cdclW_merge_restart:
  assumes "cdclW_restart** S V" and inv: "cdclW_M_level_inv S" and "conflicting S = None"
  shows "(cdclW_merge_restart** S V  conflicting V = None)
     (T U. cdclW_merge_restart** S T  conflicting V  None  conflict T U  cdclW_bj** U V)"
  using assms
proof induction
  case base
  then show ?case by simp
next
  case (step U V) note st = this(1) and cdclW_restart = this(2) and IH = this(3)[OF this(4-)] and
    confl[simp] = this(5) and inv = this(4)
  from cdclW_restart
  show ?case
  proof cases
    case propagate
    moreover have "conflicting U = None" and "conflicting V = None"
      using propagate propagate by (auto elim: propagateE)
    ultimately show ?thesis using IH cdclW_merge_restart.fw_r_propagate[of U V] by auto
  next
    case conflict
    moreover have "conflicting U = None" and "conflicting V  None"
      using conflict by (auto elim!: conflictE)
    ultimately show ?thesis using IH by auto
  next
    case other
    then show ?thesis
    proof cases
      case decide
      then show ?thesis using IH cdclW_merge_restart.fw_r_decide[of U V] by (auto elim: decideE)
    next
      case bj
      then consider
        (s_or_r) "skip_or_resolve U V" |
        (bt) "backtrack U V"
        by (auto simp: cdclW_bj.simps)
      then show ?thesis
      proof cases
        case s_or_r
        have f1: "cdclW_bj++ U V"
          by (simp add: local.bj tranclp.r_into_trancl)
        obtain T T' :: 'st where
          f2: "cdclW_merge_restart** S U
                 cdclW_merge_restart** S T  conflicting U  None
                   conflict T T'  cdclW_bj** T' U"
          using IH confl by blast
        have "conflicting V  None  conflicting U  None"
          using skip_or_resolve U V
          by (auto simp: skip_or_resolve.simps elim!: skipE resolveE)
        then show ?thesis
          by (metis (full_types) IH f1 rtranclp_trans tranclp_into_rtranclp)
      next
        case bt
        then have "conflicting U  None" by (auto elim: backtrackE)
        then obtain T T' where
          "cdclW_merge_restart** S T" and
          "conflicting U  None" and
          "conflict T T'" and
          "cdclW_bj** T' U"
          using IH confl by meson
        have invU: "cdclW_M_level_inv U"
          using inv rtranclp_cdclW_restart_consistent_inv step.hyps(1) by blast
        then have "conflicting V = None"
          using backtrack U V inv by (auto elim: backtrackE simp: cdclW_M_level_inv_decomp)
        have "full cdclW_bj T' V"
          apply (rule rtranclp_fullI[of cdclW_bj T' U V])
          using cdclW_bj** T' U apply fast
          using backtrack U V backtrack_is_full1_cdclW_bj invU unfolding full1_def full_def
          by blast
        then show ?thesis
          using cdclW_merge_restart.fw_r_conflict[of T T' V] conflict T T'
            cdclW_merge_restart** S T conflicting V = None by auto
      qed
    qed
  next
    case rf
    moreover have "conflicting U = None" and "conflicting V = None"
      using rf by (auto simp: cdclW_rf.simps elim: restartE forgetE)
    ultimately show ?thesis using IH cdclW_merge_restart.fw_r_rf[of U V] by auto
  qed
qed

lemma no_step_cdclW_restart_no_step_cdclW_merge_restart:
  "no_step cdclW_restart S  no_step cdclW_merge_restart S"
  by (auto simp: cdclW_restart.simps cdclW_merge_restart.simps cdclW_o.simps cdclW_bj.simps)

lemma no_step_cdclW_merge_restart_no_step_cdclW_restart:
  assumes
    "conflicting S = None" and
    "cdclW_M_level_inv S" and
    "no_step cdclW_merge_restart S"
  shows "no_step cdclW_restart S"
proof -
  { fix S'
    assume "conflict S S'"
    then have "cdclW_restart S S'" using cdclW_restart.conflict by auto
    then have "cdclW_M_level_inv S'"
      using assms(2) cdclW_restart_consistent_inv by blast
    then obtain S'' where "full cdclW_bj S' S''"
      using cdclW_bj_exists_normal_form[of S'] by auto
    then have False
      using conflict S S' assms(3) fw_r_conflict by blast
  }
  then show ?thesis
    using assms unfolding cdclW_restart.simps cdclW_merge_restart.simps cdclW_o.simps cdclW_bj.simps
    by (auto elim: skipE resolveE backtrackE conflictE decideE restartE)
qed

lemma cdclW_merge_restart_no_step_cdclW_bj:
  assumes
    "cdclW_merge_restart S T"
  shows "no_step cdclW_bj T"
  using assms
  by (induction rule: cdclW_merge_restart.induct)
   (force simp: cdclW_bj.simps cdclW_rf.simps cdclW_merge_restart.simps full_def
     elim!: rulesE)+

lemma rtranclp_cdclW_merge_restart_no_step_cdclW_bj:
  assumes
    "cdclW_merge_restart** S T" and
    "conflicting S = None"
  shows "no_step cdclW_bj T"
  using assms unfolding rtranclp_unfold
  apply (elim disjE)
   apply (force simp: cdclW_bj.simps cdclW_rf.simps elim!: rulesE)
  by (auto simp: tranclp_unfold_end simp: cdclW_merge_restart_no_step_cdclW_bj)

text If @{term "conflicting S  None"}, we cannot say anything.

  Remark that this theorem does not say anything about well-foundedness: even if you know that one
  relation is well-founded, it only states that the normal forms are shared.
  
lemma conflicting_true_full_cdclW_restart_iff_full_cdclW_merge:
  assumes confl: "conflicting S = None" and lev: "cdclW_M_level_inv S"
  shows "full cdclW_restart S V  full cdclW_merge_restart S V"
proof
  assume full: "full cdclW_merge_restart S V"
  then have st: "cdclW_restart** S V"
    using rtranclp_mono[of cdclW_merge_restart "cdclW_restart**"] cdclW_merge_restart_cdclW_restart
    unfolding full_def by auto

  have n_s: "no_step cdclW_merge_restart V"
    using full unfolding full_def by auto
  have n_s_bj: "no_step cdclW_bj V"
    using rtranclp_cdclW_merge_restart_no_step_cdclW_bj confl full unfolding full_def by auto
  have "S'. conflict V S'  cdclW_M_level_inv S'"
    using cdclW_restart.conflict cdclW_restart_consistent_inv lev rtranclp_cdclW_restart_consistent_inv st by blast
  then have "S'. conflict V S'  False"
    using n_s n_s_bj cdclW_bj_exists_normal_form cdclW_merge_restart.simps by meson
  then have n_s_cdclW_restart: "no_step cdclW_restart V"
    using n_s n_s_bj by (auto simp: cdclW_restart.simps cdclW_o.simps cdclW_merge_restart.simps)
  then show "full cdclW_restart S V" using st unfolding full_def by auto
next
  assume full: "full cdclW_restart S V"
  have "no_step cdclW_merge_restart V"
    using full no_step_cdclW_restart_no_step_cdclW_merge_restart unfolding full_def by blast
  moreover {
    consider
      (fw) "cdclW_merge_restart** S V" and "conflicting V = None" |
      (bj) T U where
        "cdclW_merge_restart** S T" and
        "conflicting V  None" and
        "conflict T U" and
        "cdclW_bj** U V"
      using full rtrancl_cdclW_conflicting_true_cdclW_merge_restart confl lev unfolding full_def
      by meson
    then have "cdclW_merge_restart** S V"
    proof cases
      case fw
      then show ?thesis by fast
    next
      case (bj T U)
      have "no_step cdclW_bj V"
        using full unfolding full_def by (meson cdclW_o.bj other)
      then have "full cdclW_bj U V"
        using  cdclW_bj** U V unfolding full_def by auto
      then have "cdclW_merge_restart T V"
        using conflict T U cdclW_merge_restart.fw_r_conflict by blast
      then show ?thesis using cdclW_merge_restart** S T by auto
    qed }
  ultimately show "full cdclW_merge_restart S V" unfolding full_def by fast
qed

lemma init_state_true_full_cdclW_restart_iff_full_cdclW_merge:
  shows "full cdclW_restart (init_state N) V  full cdclW_merge_restart (init_state N) V"
  by (rule conflicting_true_full_cdclW_restart_iff_full_cdclW_merge) auto


subsection CDCL with Merge and Strategy

subsubsection The intermediate step

inductive cdclW_s' :: "'st  'st  bool" for S :: 'st where
conflict': "conflict S S'  cdclW_s' S S'" |
propagate': "propagate S S'  cdclW_s' S S'" |
decide': "no_step conflict S  no_step propagate S  decide S S'  cdclW_s' S S'" |
bj': "full1 cdclW_bj S S'  cdclW_s' S S'"

inductive_cases cdclW_s'E: "cdclW_s' S T"

lemma rtranclp_cdclW_bj_full1_cdclp_cdclW_stgy:
  "cdclW_bj** S S'  cdclW_stgy** S S'"
proof (induction rule: converse_rtranclp_induct)
  case base
  then show ?case by simp
next
  case (step T U) note st = this(2) and bj = this(1) and IH = this(3)
  have n_s: "no_step conflict T" "no_step propagate T"
    using bj by (auto simp add: cdclW_bj.simps elim!: rulesE)
  consider
      (U) "U = S'"
    | (U') U' where "cdclW_bj U U'" and "cdclW_bj** U' S'"
    using st by (metis converse_rtranclpE)
  then show ?case
  proof cases
    case U
    then show ?thesis
      using n_s cdclW_o.bj local.bj other' by (meson r_into_rtranclp)
  next
    case U' note U' = this(1)
    have "no_step conflict U" "no_step propagate U"
      using U' by (fastforce simp: cdclW_bj.simps elim!: rulesE)+
    then have "cdclW_stgy T U"
      using n_s cdclW_stgy.simps local.bj cdclW_o.bj by meson
    then show ?thesis using IH by auto
  qed
qed

lemma cdclW_s'_is_rtranclp_cdclW_stgy:
  "cdclW_s' S T  cdclW_stgy** S T"
  by (induction rule: cdclW_s'.induct)
    (auto simp: full1_def
     dest: tranclp_into_rtranclp rtranclp_cdclW_bj_full1_cdclp_cdclW_stgy cdclW_stgy.intros)

lemma cdclW_stgy_cdclW_s'_no_step:
  assumes "cdclW_stgy S U" and "cdclW_all_struct_inv S" and "no_step cdclW_bj U"
  shows "cdclW_s' S U"
  using assms apply (cases rule: cdclW_stgy.cases)
  using bj'[of S U] by (auto intro: cdclW_s'.intros simp: cdclW_o.simps full1_def)

lemma rtranclp_cdclW_stgy_connected_to_rtranclp_cdclW_s':
  assumes "cdclW_stgy** S U" and inv: "cdclW_M_level_inv S"
  shows "cdclW_s'** S U  (T. cdclW_s'** S T  cdclW_bj++ T U  conflicting U  None)"
  using assms(1)
proof induction
  case base
  then show ?case by simp
next
  case (step T V) note st = this(1) and o = this(2) and IH = this(3)
  from o show ?case
  proof cases
    case conflict'
    then have "cdclW_s'** S T"
      using IH by (auto elim: conflictE)
    moreover have f2: "cdclW_s'** T V"
      using cdclW_s'.conflict' conflict' by blast
    ultimately show ?thesis by auto
  next
    case propagate'
    then have "cdclW_s'** S T"
      using IH by (auto elim: propagateE)
    moreover have f2: "cdclW_s'** T V"
      using cdclW_s'.propagate' propagate' by blast
    ultimately show ?thesis by auto
  next
    case other' note o = this(3) and n_s = this(1,2) and full = this(3)
    then show ?thesis
      using o
    proof (cases rule: cdclW_o_rule_cases)
      case decide
      then have "cdclW_s'** S T"
        using IH by (auto elim: rulesE)
      then show ?thesis
        by (meson decide decide' full n_s rtranclp.rtrancl_into_rtrancl)
    next
      case backtrack
      consider
        (s') "cdclW_s'** S T" |
        (bj) S' where "cdclW_s'** S S'" and "cdclW_bj++ S' T" and "conflicting T  None"
        using IH by blast
      then show ?thesis
      proof cases
        case s'
        moreover {
          have "cdclW_M_level_inv T"
            using inv local.step(1) rtranclp_cdclW_stgy_consistent_inv by auto
          then have "full1 cdclW_bj T V"
            using backtrack_is_full1_cdclW_bj backtrack by blast
          then have "cdclW_s' T V"
            using full bj' n_s by blast }
        ultimately show ?thesis by auto
      next
        case (bj S') note S_S' = this(1) and bj_T = this(2)
        moreover {
          have "cdclW_M_level_inv T"
            using inv local.step(1) rtranclp_cdclW_stgy_consistent_inv by auto
          then have "full1 cdclW_bj T V"
            using backtrack_is_full1_cdclW_bj backtrack by blast
          then have "full1 cdclW_bj S' V"
            using bj_T unfolding full1_def by fastforce }
        ultimately have "cdclW_s' S' V" by (simp add: cdclW_s'.bj')
        then show ?thesis using S_S' by auto
      qed
    next
      case skip
      then have confl_V: "conflicting V  None"
        using skip by (auto elim: rulesE)
      have "cdclW_bj T V"
        using local.skip by blast
      then show ?thesis
        using confl_V step.IH by auto
    next
      case resolve
      have confl_V: "conflicting V  None"
        using resolve by (auto elim!: rulesE)
      have "cdclW_bj T V"
        using local.resolve by blast
      then show ?thesis
        using confl_V step.IH by auto
    qed
  qed
qed

lemma n_step_cdclW_stgy_iff_no_step_cdclW_restart_cl_cdclW_o:
  assumes inv: "cdclW_all_struct_inv S"
  shows "no_step cdclW_s' S  no_step cdclW_stgy S" (is "?S' S  ?C S")
proof
  assume "?C S"
  then show "?S' S"
    by (auto simp: cdclW_s'.simps full1_def tranclp_unfold_begin cdclW_stgy.simps)
next
  assume n_s: "?S' S"
  then show "?C S"
    by (metis bj' cdclW_bj_exists_normal_form cdclW_o.cases cdclW_s'.intros
      cdclW_stgy.cases decide' full_unfold)
qed

lemma cdclW_s'_tranclp_cdclW_restart:
   assumes "cdclW_s' S S'" shows "cdclW_restart++ S S'"
   using assms
proof (cases rule: cdclW_s'.cases)
  case conflict'
  then show ?thesis by blast
next
  case propagate'
  then show ?thesis by blast
next
  case decide'
  then show ?thesis
    using cdclW_stgy.simps cdclW_stgy_tranclp_cdclW_restart by (meson cdclW_o.simps)
next
  case bj'
  then show ?thesis
    by (metis cdclW_s'.bj' cdclW_s'_is_rtranclp_cdclW_stgy full1_def
      rtranclp_cdclW_stgy_rtranclp_cdclW_restart rtranclp_unfold tranclp_unfold_begin)
qed

lemma tranclp_cdclW_s'_tranclp_cdclW_restart:
  "cdclW_s'++ S S'  cdclW_restart++ S S'"
  apply (induct rule: tranclp.induct)
   using cdclW_s'_tranclp_cdclW_restart apply blast
  by (meson cdclW_s'_tranclp_cdclW_restart tranclp_trans)

lemma rtranclp_cdclW_s'_rtranclp_cdclW_restart:
   "cdclW_s'** S S'  cdclW_restart** S S'"
  using rtranclp_unfold[of cdclW_s' S S'] tranclp_cdclW_s'_tranclp_cdclW_restart[of S S'] by auto

lemma full_cdclW_stgy_iff_full_cdclW_s':
  assumes inv: "cdclW_all_struct_inv S"
  shows "full cdclW_stgy S T  full cdclW_s' S T" (is "?S  ?S'")
proof
  assume ?S'
  then have "cdclW_restart** S T"
    using rtranclp_cdclW_s'_rtranclp_cdclW_restart[of S T] unfolding full_def by blast
  then have inv': "cdclW_all_struct_inv T"
    using rtranclp_cdclW_all_struct_inv_inv inv by blast
  have "cdclW_stgy** S T"
    using ?S' unfolding full_def
      using cdclW_s'_is_rtranclp_cdclW_stgy rtranclp_mono[of cdclW_s' "cdclW_stgy**"] by auto
  then show ?S
    using ?S' inv' n_step_cdclW_stgy_iff_no_step_cdclW_restart_cl_cdclW_o unfolding full_def
    by blast
next
  assume ?S
  then have inv_T: "cdclW_all_struct_inv T"
    by (metis assms full_def rtranclp_cdclW_all_struct_inv_inv
      rtranclp_cdclW_stgy_rtranclp_cdclW_restart)
  consider
    (s') "cdclW_s'** S T" |
    (st) S' where "cdclW_s'** S S'" and "cdclW_bj++ S' T" and "conflicting T  None"
    using rtranclp_cdclW_stgy_connected_to_rtranclp_cdclW_s'[of S T] inv ?S
    unfolding full_def cdclW_all_struct_inv_def
    by blast
  then show ?S'
  proof cases
    case s'
    then show ?thesis
      using full cdclW_stgy S T unfolding full_def
      by (metis inv_T n_step_cdclW_stgy_iff_no_step_cdclW_restart_cl_cdclW_o)
  next
    case (st S') note st = this(1) and bj = this(2) and confl = this(3)
    have "no_step cdclW_bj T"
      using ?S cdclW_stgy.conflict' cdclW_stgy.intros(2) other' unfolding full_def by blast
    then have "full1 cdclW_bj S' T"
      using bj unfolding full1_def by blast
    then have "cdclW_s' S' T"
      using cdclW_s'.bj'[of S' T] by blast
    then have "cdclW_s'** S T"
      using st(1) by auto
    moreover have "no_step cdclW_s' T"
      using inv_T full cdclW_stgy S T n_step_cdclW_stgy_iff_no_step_cdclW_restart_cl_cdclW_o
      unfolding full_def by blast
    ultimately show ?thesis
      unfolding full_def by blast
  qed
qed

end

end