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_learning⇩W.conflict} to find the conflict
▸ the conflict is analysed by repetitive application of
@{term conflict_driven_clause_learning⇩W.resolve} and
@{term conflict_driven_clause_learning⇩W.skip},
▸ finally @{term conflict_driven_clause_learning⇩W.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_learning⇩W
begin
declare cdcl⇩W_restart.intros[intro] cdcl⇩W_bj.intros[intro] cdcl⇩W_o.intros[intro]
state_prop [simp del]
lemma backtrack_no_cdcl⇩W_bj:
assumes cdcl: "cdcl⇩W_bj T U"
shows "¬backtrack V T"
using cdcl
apply (induction rule: cdcl⇩W_bj.induct)
apply (elim skipE, force elim!: backtrackE simp: cdcl⇩W_M_level_inv_def)
apply (elim resolveE, force elim!: backtrackE simp: cdcl⇩W_M_level_inv_def)
apply standard
apply (elim backtrackE)
apply (force simp add: cdcl⇩W_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_cdcl⇩W_bj_skip_or_resolve_backtrack:
assumes "cdcl⇩W_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) "cdcl⇩W_bj⇧+⇧+ S U"
using st unfolding rtranclp_unfold by blast
then show ?case
proof cases
case SUp
have "⋀T. skip_or_resolve⇧*⇧* S T ⟹ cdcl⇩W_restart⇧*⇧* S T"
using mono_rtranclp[of skip_or_resolve cdcl⇩W_restart]
by (blast intro: skip_or_resolve.cases)
then have "skip_or_resolve⇧*⇧* S U"
using bj IH backtrack_no_cdcl⇩W_bj by meson
then show ?thesis
using bj by (auto simp: cdcl⇩W_bj.simps dest!: skip_or_resolve.intros)
next
case SU
then show ?thesis
using bj by (auto simp: cdcl⇩W_bj.simps dest!: skip_or_resolve.intros)
qed
qed
lemma rtranclp_skip_or_resolve_rtranclp_cdcl⇩W_restart:
"skip_or_resolve⇧*⇧* S T ⟹ cdcl⇩W_restart⇧*⇧* S T"
by (induction rule: rtranclp_induct)
(auto dest!: cdcl⇩W_bj.intros cdcl⇩W_restart.intros cdcl⇩W_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 inv⇩N⇩O⇩T :: "'st ⇒ bool" where
"inv⇩N⇩O⇩T ≡ λS. no_dup (trail S)"
declare inv⇩N⇩O⇩T_def[simp]
end
context conflict_driven_clause_learning⇩W
begin
subsection ‹More lemmas about Conflict, Propagate and Backjumping›
subsubsection ‹Termination›
lemma cdcl⇩W_bj_measure:
assumes "cdcl⇩W_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: cdcl⇩W_bj.induct) (force elim!: backtrackE skipE resolveE)+
lemma wf_cdcl⇩W_bj:
"wf {(b,a). cdcl⇩W_bj a b}"
apply (rule wfP_if_measure[of "λ_. True"
_ "λT. length (trail T) + (if conflicting T = None then 0 else 1)", simplified])
using cdcl⇩W_bj_measure by simp
lemma cdcl⇩W_bj_exists_normal_form:
shows "∃T. full cdcl⇩W_bj S T"
using wf_exists_normal_form_full[OF wf_cdcl⇩W_bj] .
lemma rtranclp_skip_state_decomp:
assumes "skip⇧*⇧* S T"
shows
"∃M. trail S = M @ trail T ∧ (∀m∈set 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
"cdcl⇩W_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 "cdcl⇩W_all_struct_inv V"
using rtranclp_mono[of skip cdcl⇩W_restart] assms(3) rtranclp_cdcl⇩W_all_struct_inv_inv mono_rtranclp
by (auto dest!: bj other cdcl⇩W_bj.skip)
then have "cdcl⇩W_M_level_inv V"
unfolding cdcl⇩W_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 "cdcl⇩W_restart⇧*⇧* S T"
using bj cdcl⇩W_bj.skip mono_rtranclp[of skip cdcl⇩W_restart S T] other st by meson
then have inv': "cdcl⇩W_all_struct_inv T"
using rtranclp_cdcl⇩W_all_struct_inv_inv inv by blast
have M_lev: "cdcl⇩W_M_level_inv T" using inv' unfolding cdcl⇩W_all_struct_inv_def by auto
then have n_d': "no_dup ?M"
using tr_M unfolding cdcl⇩W_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 cdcl⇩W_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 cdcl⇩W_conflicting_def cdcl⇩W_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 cdcl⇩W_all_struct_inv_def cdcl⇩W_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 cdcl⇩W_all_struct_inv_def cdcl⇩W_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: "cdcl⇩W_all_struct_inv S"
shows "backtrack T W"
using assms
proof -
have M_lev: "cdcl⇩W_M_level_inv S "
using bt inv unfolding cdcl⇩W_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: cdcl⇩W_M_level_inv_decomp)
have "cdcl⇩W_all_struct_inv T"
using mono_rtranclp[of skip cdcl⇩W_restart] by (smt bj cdcl⇩W_bj.skip inv local.skip other
rtranclp_cdcl⇩W_all_struct_inv_inv)
then have [simp]: "no_dup (trail T)"
unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_M_level_inv_def by auto
obtain MS M⇩T where M: "trail S = MS @ M⇩T" and M⇩T: "M⇩T = trail T" and nm: "∀m∈set MS. ¬is_decided m"
using rtranclp_skip_state_decomp(1)[OF skip] S by auto
have T: "state_butlast T = (M⇩T, 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 M⇩T rtranclp_skip_state_decomp[of S T] skip S by (auto simp: clauses_def)
have "cdcl⇩W_all_struct_inv T"
apply (rule rtranclp_cdcl⇩W_all_struct_inv_inv[OF _ inv])
using bj cdcl⇩W_bj.skip local.skip other rtranclp_mono[of skip cdcl⇩W_restart] by blast
then have "M⇩T ⊨as CNot ?D"
unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_conflicting_def using T by auto
then have "∀L'∈#?D. defined_lit M⇩T 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 cdcl⇩W_all_struct_inv_def cdcl⇩W_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 M⇩T L'"
"get_level (trail S) L = get_level M⇩T L"
unfolding M by (auto simp: lits_of_def)
have [simp]: "get_maximum_level (trail S) D = get_maximum_level M⇩T D"
using ‹M⇩T ⊨as CNot (add_mset L D)› M nm undef_D by (auto simp: get_maximum_level_skip_beginning)
have lev_l': "get_level M⇩T 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 M⇩T 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: ‹M⇩T = c @ Decided K # M1›
using nm decomp by (auto dest!: get_all_ann_decomposition_exists_prepend
simp: M⇩T[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: M⇩T[symmetric] M c)
have max_trail_S_MT_L_D': ‹get_maximum_level (trail S) ?D' = get_maximum_level M⇩T ?D'›
by (rule get_maximum_level_cong) (use H D_D' in auto)
then have lev_l_D': "get_level M⇩T L = get_maximum_level M⇩T ?D'"
using lev_l_D H by auto
have i': "i = get_maximum_level M⇩T 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 M⇩T))"
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 M⇩T)"
by auto
moreover {
have "undefined_lit MS K"
using ‹no_dup (trail S)› decomp' unfolding M M⇩T
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 M⇩T 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 M⇩T[symmetric] clss_S_T by auto
subgoal using lev_K unfolding M⇩T[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 cdcl⇩W_bj_decomp_resolve_skip_and_bj:
assumes "cdcl⇩W_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 "cdcl⇩W_restart⇧*⇧* S V"
using rtranclp_skip_or_resolve_rtranclp_cdcl⇩W_restart by blast
with bj bt have False using backtrack_no_cdcl⇩W_bj by simp
}
then show ?thesis using IH by blast
qed
show ?case
using bj
proof (cases rule: cdcl⇩W_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 cdcl⇩W_merge_restart :: "'st ⇒ 'st ⇒ bool" where
fw_r_propagate: "propagate S S' ⟹ cdcl⇩W_merge_restart S S'" |
fw_r_conflict: "conflict S T ⟹ full cdcl⇩W_bj T U ⟹ cdcl⇩W_merge_restart S U" |
fw_r_decide: "decide S S' ⟹ cdcl⇩W_merge_restart S S'"|
fw_r_rf: "cdcl⇩W_rf S S' ⟹ cdcl⇩W_merge_restart S S'"
lemma rtranclp_cdcl⇩W_bj_rtranclp_cdcl⇩W_restart:
"cdcl⇩W_bj⇧*⇧* S T ⟹ cdcl⇩W_restart⇧*⇧* S T"
using mono_rtranclp[of cdcl⇩W_bj cdcl⇩W_restart] by blast
lemma cdcl⇩W_merge_restart_cdcl⇩W_restart:
assumes "cdcl⇩W_merge_restart S T"
shows "cdcl⇩W_restart⇧*⇧* S T"
using assms
proof induction
case (fw_r_conflict S T U) note confl = this(1) and bj = this(2)
have "cdcl⇩W_restart S T" using confl by (simp add: cdcl⇩W_restart.intros r_into_rtranclp)
moreover
have "cdcl⇩W_bj⇧*⇧* T U" using bj unfolding full_def by auto
then have "cdcl⇩W_restart⇧*⇧* T U" using rtranclp_cdcl⇩W_bj_rtranclp_cdcl⇩W_restart by blast
ultimately show ?case by auto
qed (simp_all add: cdcl⇩W_o.intros cdcl⇩W_restart.intros r_into_rtranclp)
lemma cdcl⇩W_merge_restart_conflicting_true_or_no_step:
assumes "cdcl⇩W_merge_restart S T"
shows "conflicting T = None ∨ no_step cdcl⇩W_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 "cdcl⇩W_restart U V" and "conflicting U = Some D"
then have False
using n_s unfolding full_def
by (induction rule: cdcl⇩W_restart_all_rules_induct)
(auto dest!: cdcl⇩W_bj.intros elim: decideE propagateE conflictE forgetE restartE)
}
then show ?case by (cases "conflicting U") fastforce+
qed (auto simp add: cdcl⇩W_rf.simps elim: propagateE decideE restartE forgetE)
inductive cdcl⇩W_merge :: "'st ⇒ 'st ⇒ bool" where
fw_propagate: "propagate S S' ⟹ cdcl⇩W_merge S S'" |
fw_conflict: "conflict S T ⟹ full cdcl⇩W_bj T U ⟹ cdcl⇩W_merge S U" |
fw_decide: "decide S S' ⟹ cdcl⇩W_merge S S'"|
fw_forget: "forget S S' ⟹ cdcl⇩W_merge S S'"
lemma cdcl⇩W_merge_cdcl⇩W_merge_restart:
"cdcl⇩W_merge S T ⟹ cdcl⇩W_merge_restart S T"
by (meson cdcl⇩W_merge.cases cdcl⇩W_merge_restart.simps forget)
lemma rtranclp_cdcl⇩W_merge_tranclp_cdcl⇩W_merge_restart:
"cdcl⇩W_merge⇧*⇧* S T ⟹ cdcl⇩W_merge_restart⇧*⇧* S T"
using rtranclp_mono[of cdcl⇩W_merge cdcl⇩W_merge_restart] cdcl⇩W_merge_cdcl⇩W_merge_restart by blast
lemma cdcl⇩W_merge_rtranclp_cdcl⇩W_restart:
"cdcl⇩W_merge S T ⟹ cdcl⇩W_restart⇧*⇧* S T"
using cdcl⇩W_merge_cdcl⇩W_merge_restart cdcl⇩W_merge_restart_cdcl⇩W_restart by blast
lemma rtranclp_cdcl⇩W_merge_rtranclp_cdcl⇩W_restart:
"cdcl⇩W_merge⇧*⇧* S T ⟹ cdcl⇩W_restart⇧*⇧* S T"
using rtranclp_mono[of cdcl⇩W_merge "cdcl⇩W_restart⇧*⇧*"] cdcl⇩W_merge_rtranclp_cdcl⇩W_restart by auto
lemma cdcl⇩W_all_struct_inv_tranclp_cdcl⇩W_merge_tranclp_cdcl⇩W_merge_cdcl⇩W_all_struct_inv:
assumes
inv: "cdcl⇩W_all_struct_inv b"
"cdcl⇩W_merge⇧+⇧+ b a"
shows "(λS T. cdcl⇩W_all_struct_inv S ∧ cdcl⇩W_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 "cdcl⇩W_all_struct_inv c"
using tranclp_into_rtranclp[OF st] cdcl⇩W_merge_rtranclp_cdcl⇩W_restart assms(1)
rtranclp_cdcl⇩W_all_struct_inv_inv rtranclp_mono[of cdcl⇩W_merge "cdcl⇩W_restart⇧*⇧*"] by fastforce
then have "(λS T. cdcl⇩W_all_struct_inv S ∧ cdcl⇩W_merge S T)⇧+⇧+ c d"
using fw by auto
then show ?case using IH by auto
qed
lemma backtrack_is_full1_cdcl⇩W_bj:
assumes bt: "backtrack S T"
shows "full1 cdcl⇩W_bj S T"
using bt backtrack_no_cdcl⇩W_bj unfolding full1_def by blast
lemma rtrancl_cdcl⇩W_conflicting_true_cdcl⇩W_merge_restart:
assumes "cdcl⇩W_restart⇧*⇧* S V" and inv: "cdcl⇩W_M_level_inv S" and "conflicting S = None"
shows "(cdcl⇩W_merge_restart⇧*⇧* S V ∧ conflicting V = None)
∨ (∃T U. cdcl⇩W_merge_restart⇧*⇧* S T ∧ conflicting V ≠ None ∧ conflict T U ∧ cdcl⇩W_bj⇧*⇧* U V)"
using assms
proof induction
case base
then show ?case by simp
next
case (step U V) note st = this(1) and cdcl⇩W_restart = this(2) and IH = this(3)[OF this(4-)] and
confl[simp] = this(5) and inv = this(4)
from cdcl⇩W_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 cdcl⇩W_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 cdcl⇩W_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: cdcl⇩W_bj.simps)
then show ?thesis
proof cases
case s_or_r
have f1: "cdcl⇩W_bj⇧+⇧+ U V"
by (simp add: local.bj tranclp.r_into_trancl)
obtain T T' :: 'st where
f2: "cdcl⇩W_merge_restart⇧*⇧* S U
∨ cdcl⇩W_merge_restart⇧*⇧* S T ∧ conflicting U ≠ None
∧ conflict T T' ∧ cdcl⇩W_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
"cdcl⇩W_merge_restart⇧*⇧* S T" and
"conflicting U ≠ None" and
"conflict T T'" and
"cdcl⇩W_bj⇧*⇧* T' U"
using IH confl by meson
have invU: "cdcl⇩W_M_level_inv U"
using inv rtranclp_cdcl⇩W_restart_consistent_inv step.hyps(1) by blast
then have "conflicting V = None"
using ‹backtrack U V› inv by (auto elim: backtrackE simp: cdcl⇩W_M_level_inv_decomp)
have "full cdcl⇩W_bj T' V"
apply (rule rtranclp_fullI[of cdcl⇩W_bj T' U V])
using ‹cdcl⇩W_bj⇧*⇧* T' U› apply fast
using ‹backtrack U V› backtrack_is_full1_cdcl⇩W_bj invU unfolding full1_def full_def
by blast
then show ?thesis
using cdcl⇩W_merge_restart.fw_r_conflict[of T T' V] ‹conflict T T'›
‹cdcl⇩W_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: cdcl⇩W_rf.simps elim: restartE forgetE)
ultimately show ?thesis using IH cdcl⇩W_merge_restart.fw_r_rf[of U V] by auto
qed
qed
lemma no_step_cdcl⇩W_restart_no_step_cdcl⇩W_merge_restart:
"no_step cdcl⇩W_restart S ⟹ no_step cdcl⇩W_merge_restart S"
by (auto simp: cdcl⇩W_restart.simps cdcl⇩W_merge_restart.simps cdcl⇩W_o.simps cdcl⇩W_bj.simps)
lemma no_step_cdcl⇩W_merge_restart_no_step_cdcl⇩W_restart:
assumes
"conflicting S = None" and
"cdcl⇩W_M_level_inv S" and
"no_step cdcl⇩W_merge_restart S"
shows "no_step cdcl⇩W_restart S"
proof -
{ fix S'
assume "conflict S S'"
then have "cdcl⇩W_restart S S'" using cdcl⇩W_restart.conflict by auto
then have "cdcl⇩W_M_level_inv S'"
using assms(2) cdcl⇩W_restart_consistent_inv by blast
then obtain S'' where "full cdcl⇩W_bj S' S''"
using cdcl⇩W_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 cdcl⇩W_restart.simps cdcl⇩W_merge_restart.simps cdcl⇩W_o.simps cdcl⇩W_bj.simps
by (auto elim: skipE resolveE backtrackE conflictE decideE restartE)
qed
lemma cdcl⇩W_merge_restart_no_step_cdcl⇩W_bj:
assumes
"cdcl⇩W_merge_restart S T"
shows "no_step cdcl⇩W_bj T"
using assms
by (induction rule: cdcl⇩W_merge_restart.induct)
(force simp: cdcl⇩W_bj.simps cdcl⇩W_rf.simps cdcl⇩W_merge_restart.simps full_def
elim!: rulesE)+
lemma rtranclp_cdcl⇩W_merge_restart_no_step_cdcl⇩W_bj:
assumes
"cdcl⇩W_merge_restart⇧*⇧* S T" and
"conflicting S = None"
shows "no_step cdcl⇩W_bj T"
using assms unfolding rtranclp_unfold
apply (elim disjE)
apply (force simp: cdcl⇩W_bj.simps cdcl⇩W_rf.simps elim!: rulesE)
by (auto simp: tranclp_unfold_end simp: cdcl⇩W_merge_restart_no_step_cdcl⇩W_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_cdcl⇩W_restart_iff_full_cdcl⇩W_merge:
assumes confl: "conflicting S = None" and lev: "cdcl⇩W_M_level_inv S"
shows "full cdcl⇩W_restart S V ⟷ full cdcl⇩W_merge_restart S V"
proof
assume full: "full cdcl⇩W_merge_restart S V"
then have st: "cdcl⇩W_restart⇧*⇧* S V"
using rtranclp_mono[of cdcl⇩W_merge_restart "cdcl⇩W_restart⇧*⇧*"] cdcl⇩W_merge_restart_cdcl⇩W_restart
unfolding full_def by auto
have n_s: "no_step cdcl⇩W_merge_restart V"
using full unfolding full_def by auto
have n_s_bj: "no_step cdcl⇩W_bj V"
using rtranclp_cdcl⇩W_merge_restart_no_step_cdcl⇩W_bj confl full unfolding full_def by auto
have "⋀S'. conflict V S' ⟹ cdcl⇩W_M_level_inv S'"
using cdcl⇩W_restart.conflict cdcl⇩W_restart_consistent_inv lev rtranclp_cdcl⇩W_restart_consistent_inv st by blast
then have "⋀S'. conflict V S' ⟹ False"
using n_s n_s_bj cdcl⇩W_bj_exists_normal_form cdcl⇩W_merge_restart.simps by meson
then have n_s_cdcl⇩W_restart: "no_step cdcl⇩W_restart V"
using n_s n_s_bj by (auto simp: cdcl⇩W_restart.simps cdcl⇩W_o.simps cdcl⇩W_merge_restart.simps)
then show "full cdcl⇩W_restart S V" using st unfolding full_def by auto
next
assume full: "full cdcl⇩W_restart S V"
have "no_step cdcl⇩W_merge_restart V"
using full no_step_cdcl⇩W_restart_no_step_cdcl⇩W_merge_restart unfolding full_def by blast
moreover {
consider
(fw) "cdcl⇩W_merge_restart⇧*⇧* S V" and "conflicting V = None" |
(bj) T U where
"cdcl⇩W_merge_restart⇧*⇧* S T" and
"conflicting V ≠ None" and
"conflict T U" and
"cdcl⇩W_bj⇧*⇧* U V"
using full rtrancl_cdcl⇩W_conflicting_true_cdcl⇩W_merge_restart confl lev unfolding full_def
by meson
then have "cdcl⇩W_merge_restart⇧*⇧* S V"
proof cases
case fw
then show ?thesis by fast
next
case (bj T U)
have "no_step cdcl⇩W_bj V"
using full unfolding full_def by (meson cdcl⇩W_o.bj other)
then have "full cdcl⇩W_bj U V"
using ‹ cdcl⇩W_bj⇧*⇧* U V› unfolding full_def by auto
then have "cdcl⇩W_merge_restart T V"
using ‹conflict T U› cdcl⇩W_merge_restart.fw_r_conflict by blast
then show ?thesis using ‹cdcl⇩W_merge_restart⇧*⇧* S T› by auto
qed }
ultimately show "full cdcl⇩W_merge_restart S V" unfolding full_def by fast
qed
lemma init_state_true_full_cdcl⇩W_restart_iff_full_cdcl⇩W_merge:
shows "full cdcl⇩W_restart (init_state N) V ⟷ full cdcl⇩W_merge_restart (init_state N) V"
by (rule conflicting_true_full_cdcl⇩W_restart_iff_full_cdcl⇩W_merge) auto
subsection ‹CDCL with Merge and Strategy›
subsubsection ‹The intermediate step›
inductive cdcl⇩W_s' :: "'st ⇒ 'st ⇒ bool" for S :: 'st where
conflict': "conflict S S' ⟹ cdcl⇩W_s' S S'" |
propagate': "propagate S S' ⟹ cdcl⇩W_s' S S'" |
decide': "no_step conflict S ⟹ no_step propagate S ⟹ decide S S' ⟹ cdcl⇩W_s' S S'" |
bj': "full1 cdcl⇩W_bj S S' ⟹ cdcl⇩W_s' S S'"
inductive_cases cdcl⇩W_s'E: "cdcl⇩W_s' S T"
lemma rtranclp_cdcl⇩W_bj_full1_cdclp_cdcl⇩W_stgy:
"cdcl⇩W_bj⇧*⇧* S S' ⟹ cdcl⇩W_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: cdcl⇩W_bj.simps elim!: rulesE)
consider
(U) "U = S'"
| (U') U' where "cdcl⇩W_bj U U'" and "cdcl⇩W_bj⇧*⇧* U' S'"
using st by (metis converse_rtranclpE)
then show ?case
proof cases
case U
then show ?thesis
using n_s cdcl⇩W_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: cdcl⇩W_bj.simps elim!: rulesE)+
then have "cdcl⇩W_stgy T U"
using n_s cdcl⇩W_stgy.simps local.bj cdcl⇩W_o.bj by meson
then show ?thesis using IH by auto
qed
qed
lemma cdcl⇩W_s'_is_rtranclp_cdcl⇩W_stgy:
"cdcl⇩W_s' S T ⟹ cdcl⇩W_stgy⇧*⇧* S T"
by (induction rule: cdcl⇩W_s'.induct)
(auto simp: full1_def
dest: tranclp_into_rtranclp rtranclp_cdcl⇩W_bj_full1_cdclp_cdcl⇩W_stgy cdcl⇩W_stgy.intros)
lemma cdcl⇩W_stgy_cdcl⇩W_s'_no_step:
assumes "cdcl⇩W_stgy S U" and "cdcl⇩W_all_struct_inv S" and "no_step cdcl⇩W_bj U"
shows "cdcl⇩W_s' S U"
using assms apply (cases rule: cdcl⇩W_stgy.cases)
using bj'[of S U] by (auto intro: cdcl⇩W_s'.intros simp: cdcl⇩W_o.simps full1_def)
lemma rtranclp_cdcl⇩W_stgy_connected_to_rtranclp_cdcl⇩W_s':
assumes "cdcl⇩W_stgy⇧*⇧* S U" and inv: "cdcl⇩W_M_level_inv S"
shows "cdcl⇩W_s'⇧*⇧* S U ∨ (∃T. cdcl⇩W_s'⇧*⇧* S T ∧ cdcl⇩W_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 "cdcl⇩W_s'⇧*⇧* S T"
using IH by (auto elim: conflictE)
moreover have f2: "cdcl⇩W_s'⇧*⇧* T V"
using cdcl⇩W_s'.conflict' conflict' by blast
ultimately show ?thesis by auto
next
case propagate'
then have "cdcl⇩W_s'⇧*⇧* S T"
using IH by (auto elim: propagateE)
moreover have f2: "cdcl⇩W_s'⇧*⇧* T V"
using cdcl⇩W_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: cdcl⇩W_o_rule_cases)
case decide
then have "cdcl⇩W_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') "cdcl⇩W_s'⇧*⇧* S T" |
(bj) S' where "cdcl⇩W_s'⇧*⇧* S S'" and "cdcl⇩W_bj⇧+⇧+ S' T" and "conflicting T ≠ None"
using IH by blast
then show ?thesis
proof cases
case s'
moreover {
have "cdcl⇩W_M_level_inv T"
using inv local.step(1) rtranclp_cdcl⇩W_stgy_consistent_inv by auto
then have "full1 cdcl⇩W_bj T V"
using backtrack_is_full1_cdcl⇩W_bj backtrack by blast
then have "cdcl⇩W_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 "cdcl⇩W_M_level_inv T"
using inv local.step(1) rtranclp_cdcl⇩W_stgy_consistent_inv by auto
then have "full1 cdcl⇩W_bj T V"
using backtrack_is_full1_cdcl⇩W_bj backtrack by blast
then have "full1 cdcl⇩W_bj S' V"
using bj_T unfolding full1_def by fastforce }
ultimately have "cdcl⇩W_s' S' V" by (simp add: cdcl⇩W_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 "cdcl⇩W_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 "cdcl⇩W_bj T V"
using local.resolve by blast
then show ?thesis
using confl_V step.IH by auto
qed
qed
qed
lemma n_step_cdcl⇩W_stgy_iff_no_step_cdcl⇩W_restart_cl_cdcl⇩W_o:
assumes inv: "cdcl⇩W_all_struct_inv S"
shows "no_step cdcl⇩W_s' S ⟷ no_step cdcl⇩W_stgy S" (is "?S' S ⟷ ?C S")
proof
assume "?C S"
then show "?S' S"
by (auto simp: cdcl⇩W_s'.simps full1_def tranclp_unfold_begin cdcl⇩W_stgy.simps)
next
assume n_s: "?S' S"
then show "?C S"
by (metis bj' cdcl⇩W_bj_exists_normal_form cdcl⇩W_o.cases cdcl⇩W_s'.intros
cdcl⇩W_stgy.cases decide' full_unfold)
qed
lemma cdcl⇩W_s'_tranclp_cdcl⇩W_restart:
assumes "cdcl⇩W_s' S S'" shows "cdcl⇩W_restart⇧+⇧+ S S'"
using assms
proof (cases rule: cdcl⇩W_s'.cases)
case conflict'
then show ?thesis by blast
next
case propagate'
then show ?thesis by blast
next
case decide'
then show ?thesis
using cdcl⇩W_stgy.simps cdcl⇩W_stgy_tranclp_cdcl⇩W_restart by (meson cdcl⇩W_o.simps)
next
case bj'
then show ?thesis
by (metis cdcl⇩W_s'.bj' cdcl⇩W_s'_is_rtranclp_cdcl⇩W_stgy full1_def
rtranclp_cdcl⇩W_stgy_rtranclp_cdcl⇩W_restart rtranclp_unfold tranclp_unfold_begin)
qed
lemma tranclp_cdcl⇩W_s'_tranclp_cdcl⇩W_restart:
"cdcl⇩W_s'⇧+⇧+ S S' ⟹ cdcl⇩W_restart⇧+⇧+ S S'"
apply (induct rule: tranclp.induct)
using cdcl⇩W_s'_tranclp_cdcl⇩W_restart apply blast
by (meson cdcl⇩W_s'_tranclp_cdcl⇩W_restart tranclp_trans)
lemma rtranclp_cdcl⇩W_s'_rtranclp_cdcl⇩W_restart:
"cdcl⇩W_s'⇧*⇧* S S' ⟹ cdcl⇩W_restart⇧*⇧* S S'"
using rtranclp_unfold[of cdcl⇩W_s' S S'] tranclp_cdcl⇩W_s'_tranclp_cdcl⇩W_restart[of S S'] by auto
lemma full_cdcl⇩W_stgy_iff_full_cdcl⇩W_s':
assumes inv: "cdcl⇩W_all_struct_inv S"
shows "full cdcl⇩W_stgy S T ⟷ full cdcl⇩W_s' S T" (is "?S ⟷ ?S'")
proof
assume ?S'
then have "cdcl⇩W_restart⇧*⇧* S T"
using rtranclp_cdcl⇩W_s'_rtranclp_cdcl⇩W_restart[of S T] unfolding full_def by blast
then have inv': "cdcl⇩W_all_struct_inv T"
using rtranclp_cdcl⇩W_all_struct_inv_inv inv by blast
have "cdcl⇩W_stgy⇧*⇧* S T"
using ‹?S'› unfolding full_def
using cdcl⇩W_s'_is_rtranclp_cdcl⇩W_stgy rtranclp_mono[of cdcl⇩W_s' "cdcl⇩W_stgy⇧*⇧*"] by auto
then show ?S
using ‹?S'› inv' n_step_cdcl⇩W_stgy_iff_no_step_cdcl⇩W_restart_cl_cdcl⇩W_o unfolding full_def
by blast
next
assume ?S
then have inv_T: "cdcl⇩W_all_struct_inv T"
by (metis assms full_def rtranclp_cdcl⇩W_all_struct_inv_inv
rtranclp_cdcl⇩W_stgy_rtranclp_cdcl⇩W_restart)
consider
(s') "cdcl⇩W_s'⇧*⇧* S T" |
(st) S' where "cdcl⇩W_s'⇧*⇧* S S'" and "cdcl⇩W_bj⇧+⇧+ S' T" and "conflicting T ≠ None"
using rtranclp_cdcl⇩W_stgy_connected_to_rtranclp_cdcl⇩W_s'[of S T] inv ‹?S›
unfolding full_def cdcl⇩W_all_struct_inv_def
by blast
then show ?S'
proof cases
case s'
then show ?thesis
using ‹full cdcl⇩W_stgy S T› unfolding full_def
by (metis inv_T n_step_cdcl⇩W_stgy_iff_no_step_cdcl⇩W_restart_cl_cdcl⇩W_o)
next
case (st S') note st = this(1) and bj = this(2) and confl = this(3)
have "no_step cdcl⇩W_bj T"
using ‹?S› cdcl⇩W_stgy.conflict' cdcl⇩W_stgy.intros(2) other' unfolding full_def by blast
then have "full1 cdcl⇩W_bj S' T"
using bj unfolding full1_def by blast
then have "cdcl⇩W_s' S' T"
using cdcl⇩W_s'.bj'[of S' T] by blast
then have "cdcl⇩W_s'⇧*⇧* S T"
using st(1) by auto
moreover have "no_step cdcl⇩W_s' T"
using inv_T ‹full cdcl⇩W_stgy S T› n_step_cdcl⇩W_stgy_iff_no_step_cdcl⇩W_restart_cl_cdcl⇩W_o
unfolding full_def by blast
ultimately show ?thesis
unfolding full_def by blast
qed
qed
end
end