theory CDCL_WNOT
imports CDCL_W_Termination CDCL_NOT
begin
section ‹Link between Weidenbach's and NOT's CDCL›
subsection ‹Inclusion of the states›
declare upt.simps(2)[simp del]
sledgehammer_params[verbose]
context cdcl⇩W
begin
lemma backtrack_levE:
"backtrack S S' ⟹ cdcl⇩W_M_level_inv S ⟹
(⋀D L K M1 M2.
(Decided K (Suc (get_maximum_level (trail S) D)) # M1, M2)
∈ set (get_all_decided_decomposition (trail S)) ⟹
get_level (trail S) L = get_maximum_level (trail S) (D + {#L#}) ⟹
undefined_lit M1 L ⟹
S' ∼ cons_trail (Propagated L (D + {#L#}))
(reduce_trail_to M1 (add_learned_cls (D + {#L#})
(update_backtrack_lvl (get_maximum_level (trail S) D) (update_conflicting None S)))) ⟹
backtrack_lvl S = get_maximum_level (trail S) (D + {#L#}) ⟹
conflicting S = Some (D + {#L#}) ⟹ P) ⟹
P"
using assms by (induction rule: backtrack_induction_lev2) metis
lemma backtrack_no_cdcl⇩W_bj:
assumes cdcl: "cdcl⇩W_bj T U" and inv: "cdcl⇩W_M_level_inv V"
shows "¬backtrack V T"
using cdcl inv
apply (induction rule: cdcl⇩W_bj.induct)
apply (elim skipE, force elim!: backtrack_levE[OF _ inv] simp: cdcl⇩W_M_level_inv_def)
apply (elim resolveE, force elim!: backtrack_levE[OF _ inv] simp: cdcl⇩W_M_level_inv_def)
apply standard
apply (elim backtrack_levE[OF _ inv], elim backtrackE)
apply (force simp del: state_simp simp add: state_eq_conflicting cdcl⇩W_M_level_inv_decomp)
done
abbreviation skip_or_resolve :: "'st ⇒ 'st ⇒ bool" where
"skip_or_resolve ≡ (λS T. skip S T ∨ resolve S T)"
lemma rtranclp_cdcl⇩W_bj_skip_or_resolve_backtrack:
assumes "cdcl⇩W_bj⇧*⇧* S U" and inv: "cdcl⇩W_M_level_inv S"
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)[OF this(4)]
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⇧*⇧* S T"
using mono_rtranclp[of skip_or_resolve cdcl⇩W] other by blast
then have "skip_or_resolve⇧*⇧* S U"
using bj IH inv backtrack_no_cdcl⇩W_bj rtranclp_cdcl⇩W_consistent_inv[OF _ inv] by meson
then show ?thesis
using bj by (metis (no_types, lifting) cdcl⇩W_bj.cases rtranclp.simps)
next
case SU
then show ?thesis
using bj by (metis (no_types, lifting) cdcl⇩W_bj.cases rtranclp.simps)
qed
qed
lemma rtranclp_skip_or_resolve_rtranclp_cdcl⇩W:
"skip_or_resolve⇧*⇧* S T ⟹ cdcl⇩W⇧*⇧* S T"
by (induction rule: rtranclp_induct) (auto dest!: cdcl⇩W_bj.intros cdcl⇩W.intros cdcl⇩W_o.intros)
definition backjump_l_cond :: "'v clause ⇒ 'v clause ⇒ 'v literal ⇒ 'st ⇒ bool" where
"backjump_l_cond ≡ λC C' L' S. True"
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
fun convert_ann_literal_from_W where
"convert_ann_literal_from_W (Propagated L _) = Propagated L ()" |
"convert_ann_literal_from_W (Decided L _) = Decided L ()"
abbreviation convert_trail_from_W ::
"('v, 'lvl, 'a) ann_literal list
⇒ ('v, unit, unit) ann_literal list" where
"convert_trail_from_W ≡ map convert_ann_literal_from_W"
lemma lits_of_convert_trail_from_W[simp]:
"lits_of (convert_trail_from_W M) = lits_of M"
by (induction rule: ann_literal_list_induct) simp_all
lemma lit_of_convert_trail_from_W[simp]:
"lit_of (convert_ann_literal_from_W L) = lit_of L"
by (cases L) auto
lemma no_dup_convert_from_W[simp]:
"no_dup (convert_trail_from_W M) ⟷ no_dup M"
by (auto simp: comp_def)
lemma convert_trail_from_W_true_annots[simp]:
"convert_trail_from_W M ⊨as C ⟷ M ⊨as C"
by (auto simp: true_annots_true_cls)
lemma defined_lit_convert_trail_from_W[simp]:
"defined_lit (convert_trail_from_W S) L ⟷ defined_lit S L"
by (auto simp: defined_lit_map image_comp)
text ‹The values @{term "0::nat"} and @{term "{#}"} are dummy values.›
fun convert_ann_literal_from_NOT
:: "('a, 'e, 'b) ann_literal ⇒ ('a, nat, 'a literal multiset) ann_literal" where
"convert_ann_literal_from_NOT (Propagated L _) = Propagated L {#}" |
"convert_ann_literal_from_NOT (Decided L _) = Decided L 0"
abbreviation convert_trail_from_NOT where
"convert_trail_from_NOT ≡ map convert_ann_literal_from_NOT"
lemma undefined_lit_convert_trail_from_NOT[simp]:
"undefined_lit (convert_trail_from_NOT F) L ⟷ undefined_lit F L"
by (induction F rule: ann_literal_list_induct) (auto simp: defined_lit_map)
lemma lits_of_convert_trail_from_NOT:
"lits_of (convert_trail_from_NOT F) = lits_of F"
by (induction F rule: ann_literal_list_induct) auto
lemma convert_trail_from_W_from_NOT[simp]:
"convert_trail_from_W (convert_trail_from_NOT M) = M"
by (induction rule: ann_literal_list_induct) auto
lemma convert_trail_from_W_convert_lit_from_NOT[simp]:
"convert_ann_literal_from_W (convert_ann_literal_from_NOT L) = L"
by (cases L) auto
abbreviation trail⇩N⇩O⇩T where
"trail⇩N⇩O⇩T S ≡ convert_trail_from_W (fst S)"
lemma undefined_lit_convert_trail_from_W[iff]:
"undefined_lit (convert_trail_from_W M) L ⟷ undefined_lit M L"
by (auto simp: defined_lit_map image_comp)
lemma lit_of_convert_ann_literal_from_NOT[iff]:
"lit_of (convert_ann_literal_from_NOT L) = lit_of L"
by (cases L) auto
sublocale state⇩W ⊆ dpll_state
"λS. convert_trail_from_W (trail S)"
clauses
"λL S. cons_trail (convert_ann_literal_from_NOT L) S"
"λS. tl_trail S"
"λC S. add_learned_cls C S"
"λC S. remove_cls C S"
by unfold_locales (auto simp: map_tl o_def)
context state⇩W
begin
declare state_simp⇩N⇩O⇩T[simp del]
end
sublocale cdcl⇩W ⊆ cdcl⇩N⇩O⇩T_merge_bj_learn_ops
"λS. convert_trail_from_W (trail S)"
clauses
"λL S. cons_trail (convert_ann_literal_from_NOT L) S"
"λS. tl_trail S"
"λC S. add_learned_cls C S"
"λC S. remove_cls C S"
"λ_ _. True"
"λ_ S. conflicting S = None"
"λC C' L' S. backjump_l_cond C C' L' S ∧ distinct_mset (C' + {#L'#}) ∧ ¬tautology (C' + {#L'#})"
by unfold_locales
sublocale cdcl⇩W ⊆ cdcl⇩N⇩O⇩T_merge_bj_learn_proxy
"λS. convert_trail_from_W (trail S)"
clauses
"λL S. cons_trail (convert_ann_literal_from_NOT L) S"
"λS. tl_trail S"
"λC S. add_learned_cls C S"
"λC S. remove_cls C S"
"λ_ _. True"
"λ_ S. conflicting S = None" backjump_l_cond inv⇩N⇩O⇩T
proof (unfold_locales, goal_cases)
case 2
then show ?case using cdcl⇩N⇩O⇩T_merged_bj_learn_no_dup_inv by (auto simp: comp_def)
next
case (1 C' S C F' K F L)
moreover
let ?C' = "remdups_mset C'"
have "L ∉# C'"
using ‹F ⊨as CNot C'› ‹undefined_lit F L› Decided_Propagated_in_iff_in_lits_of
in_CNot_implies_uminus(2) by blast
then have "distinct_mset (?C' + {#L#})"
by (metis count_mset_set(3) distinct_mset_remdups_mset distinct_mset_single_add
less_irrefl_nat mem_set_mset_iff remdups_mset_def)
moreover
have "no_dup F"
using ‹inv⇩N⇩O⇩T S› ‹convert_trail_from_W (trail S) = F' @ Decided K () # F›
unfolding inv⇩N⇩O⇩T_def
by (smt comp_apply distinct.simps(2) distinct_append list.simps(9) map_append
no_dup_convert_from_W)
then have "consistent_interp (lits_of F)"
using distinctconsistent_interp by blast
then have "¬ tautology (C')"
using ‹F ⊨as CNot C'› consistent_CNot_not_tautology true_annots_true_cls by blast
then have "¬ tautology (?C' + {#L#})"
using ‹F ⊨as CNot C'› ‹undefined_lit F L› by (metis CNot_remdups_mset
Decided_Propagated_in_iff_in_lits_of add.commute in_CNot_uminus tautology_add_single
tautology_remdups_mset true_annot_singleton true_annots_def)
show ?case
proof -
have f2: "no_dup (convert_trail_from_W (trail S))"
using ‹inv⇩N⇩O⇩T S› unfolding inv⇩N⇩O⇩T_def by (simp add: o_def)
have f3: "atm_of L ∈ atms_of_msu (clauses S)
∪ atm_of ` lits_of (convert_trail_from_W (trail S))"
using ‹convert_trail_from_W (trail S) = F' @ Decided K () # F›
‹atm_of L ∈ atms_of_msu (clauses S) ∪ atm_of ` lits_of (F' @ Decided K () # F)› by auto
have f4: "clauses S ⊨pm remdups_mset C' + {#L#}"
by (metis (no_types) ‹L ∉# C'› ‹clauses S ⊨pm C' + {#L#}› remdups_mset_singleton_sum(2)
true_clss_cls_remdups_mset union_commute)
have "F ⊨as CNot (remdups_mset C')"
by (simp add: ‹F ⊨as CNot C'›)
then show ?thesis
using f4 f3 f2 ‹¬ tautology (remdups_mset C' + {#L#})›
backjump_l.intros[OF _ f2] calculation(2-5,9)
state_eq⇩N⇩O⇩T_ref unfolding backjump_l_cond_def by blast
qed
qed
sublocale cdcl⇩W ⊆ cdcl⇩N⇩O⇩T_merge_bj_learn_proxy2
"λS. convert_trail_from_W (trail S)"
clauses
"λL S. cons_trail (convert_ann_literal_from_NOT L) S"
"λS. tl_trail S"
"λC S. add_learned_cls C S"
"λC S. remove_cls C S" "λ_ _. True" inv⇩N⇩O⇩T
"λ_ S. conflicting S = None" backjump_l_cond
by unfold_locales
sublocale cdcl⇩W ⊆ cdcl⇩N⇩O⇩T_merge_bj_learn
"λS. convert_trail_from_W (trail S)"
clauses
"λL S. cons_trail (convert_ann_literal_from_NOT L) S"
"λS. tl_trail S"
"λC S. add_learned_cls C S"
"λC S. remove_cls C S" "λ_ _. True" inv⇩N⇩O⇩T
"λ_ S. conflicting S = None" backjump_l_cond
apply unfold_locales
using dpll_bj_no_dup apply (simp add: comp_def)
using cdcl⇩N⇩O⇩T_no_dup by (auto simp add: comp_def cdcl⇩N⇩O⇩T.simps)
context cdcl⇩W
begin
text ‹Notations are lost while proving locale inclusion:›
notation state_eq⇩N⇩O⇩T (infix "∼⇩N⇩O⇩T" 50)
subsection ‹Additional Lemmas between NOT and W states›
lemma trail⇩W_eq_reduce_trail_to⇩N⇩O⇩T_eq:
"trail S = trail T ⟹ trail (reduce_trail_to⇩N⇩O⇩T F S) = trail (reduce_trail_to⇩N⇩O⇩T F T)"
proof (induction F S arbitrary: T rule: reduce_trail_to⇩N⇩O⇩T.induct)
case (1 F S T) note IH = this(1) and tr = this(2)
then have "[] = convert_trail_from_W (trail S)
∨ length F = length (convert_trail_from_W (trail S))
∨ trail (reduce_trail_to⇩N⇩O⇩T F (tl_trail S)) = trail (reduce_trail_to⇩N⇩O⇩T F (tl_trail T))"
using IH by (metis (no_types) trail_tl_trail)
then show "trail (reduce_trail_to⇩N⇩O⇩T F S) = trail (reduce_trail_to⇩N⇩O⇩T F T)"
using tr by (metis (no_types) reduce_trail_to⇩N⇩O⇩T.elims)
qed
lemma trail_reduce_trail_to⇩N⇩O⇩T_add_learned_cls:
"no_dup (trail S) ⟹
trail (reduce_trail_to⇩N⇩O⇩T M (add_learned_cls D S)) = trail (reduce_trail_to⇩N⇩O⇩T M S)"
by (rule trail⇩W_eq_reduce_trail_to⇩N⇩O⇩T_eq) simp
lemma reduce_trail_to⇩N⇩O⇩T_reduce_trail_convert:
"reduce_trail_to⇩N⇩O⇩T C S = reduce_trail_to (convert_trail_from_NOT C) S"
apply (induction C S rule: reduce_trail_to⇩N⇩O⇩T.induct)
apply (subst reduce_trail_to⇩N⇩O⇩T.simps, subst reduce_trail_to.simps)
by auto
lemma reduce_trail_to_length:
"length M = length M' ⟹ reduce_trail_to M S = reduce_trail_to M' S"
apply (induction M S arbitrary: rule: reduce_trail_to.induct)
apply (rename_tac F S; case_tac "trail S ≠ [] "; case_tac "length (trail S) ≠ length M'")
by (simp_all add: reduce_trail_to_length_ne)
subsection ‹More lemmas conflict--propagate and backjumping›
subsubsection ‹Termination›
lemma cdcl⇩W_cp_normalized_element_all_inv:
assumes inv: "cdcl⇩W_all_struct_inv S"
obtains T where "full cdcl⇩W_cp S T"
using assms cdcl⇩W_cp_normalized_element unfolding cdcl⇩W_all_struct_inv_def by blast
thm backtrackE
lemma cdcl⇩W_bj_measure:
assumes "cdcl⇩W_bj S T" and "cdcl⇩W_M_level_inv S"
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 dest:arg_cong[of _ _ length]
intro: get_all_decided_decomposition_exists_prepend
elim!: backtrack_levE
simp: cdcl⇩W_M_level_inv_def)+
lemma wf_cdcl⇩W_bj:
"wf {(b,a). cdcl⇩W_bj a b ∧ cdcl⇩W_M_level_inv a}"
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 blast
lemma cdcl⇩W_bj_exists_normal_form:
assumes lev: "cdcl⇩W_M_level_inv S"
shows "∃T. full cdcl⇩W_bj S T"
proof -
obtain T where T: "full (λa b. cdcl⇩W_bj a b ∧ cdcl⇩W_M_level_inv a) S T"
using wf_exists_normal_form_full[OF wf_cdcl⇩W_bj] by auto
then have "cdcl⇩W_bj⇧*⇧* S T"
by (auto dest: rtranclp_and_rtranclp_left simp: full_def)
moreover
then have "cdcl⇩W⇧*⇧* S T"
using mono_rtranclp[of cdcl⇩W_bj cdcl⇩W] cdcl⇩W.simps by blast
then have "cdcl⇩W_M_level_inv T"
using rtranclp_cdcl⇩W_consistent_inv lev by auto
ultimately show ?thesis using T unfolding full_def by auto
qed
lemma rtranclp_skip_state_decomp:
assumes "skip⇧*⇧* S T" and "no_dup (trail S)"
shows
"∃M. trail S = M @ trail T ∧ (∀m∈set M. ¬is_decided m)" and
"T ∼ delete_trail_and_rebuild (trail T) S"
using assms by (induction rule: rtranclp_induct)
(auto simp del: state_simp simp: state_eq_def state_access_simp)
subsubsection ‹More backjumping›
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] 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 N k M1 M2 K D L U i where
V: "state V = (trail V, N, U, k, Some (D + {#L#}))" and
W: "state W = (Propagated L (D + {#L#}) # M1, N, {#D + {#L#}#} + U,
get_maximum_level (trail V) D, None)" and
decomp: "(Decided K (Suc i) # M1, M2)
∈ set (get_all_decided_decomposition (trail V))" and
"k = get_maximum_level (trail V) (D + {#L#})" and
lev_L: "get_level (trail V) L = k" and
undef: "undefined_lit M1 L" and
"W ∼ cons_trail (Propagated L (D + {#L#}))
(reduce_trail_to M1 (add_learned_cls (D + {#L#})
(update_backtrack_lvl (get_maximum_level (trail V) D) (update_conflicting None V))))"and
lev_l_D: "backtrack_lvl V = get_maximum_level (trail V) (D + {#L#})" and
"conflicting V = Some (D + {#L#})" and
i: "i = get_maximum_level (trail V) D"
using bt by (elim backtrack_levE)
(auto simp: cdcl⇩W_M_level_inv_decomp state_eq_def simp del: state_simp)+
let ?D = "(D + {#L#})"
obtain L' C' where
T: "state T = (Propagated L' C' # trail V, N, U, k, Some ?D)" and
"V ∼ tl_trail T" and
"-L' ∉# ?D" and
"?D ≠ {#}"
using skip V by force
let ?M = "Propagated L' C' # trail V"
have "cdcl⇩W⇧*⇧* S T" using bj cdcl⇩W_bj.skip mono_rtranclp[of skip cdcl⇩W 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 T unfolding cdcl⇩W_M_level_inv_def by auto
have "k > 0"
using decomp M_lev T V unfolding cdcl⇩W_M_level_inv_def by auto
then have "atm_of L ∈ atm_of ` lits_of (trail V)"
using lev_L get_rev_level_ge_0_atm_of_in V by fastforce
then have L_L': "atm_of L ≠ atm_of L'"
using n_d' unfolding lits_of_def by auto
have L'_M: "atm_of L' ∉ atm_of ` lits_of (trail V)"
using n_d' unfolding lits_of_def by auto
have "?M ⊨as CNot ?D"
using inv' T unfolding cdcl⇩W_conflicting_def cdcl⇩W_all_struct_inv_def by auto
then have "L' ∉# ?D"
using L_L' L'_M unfolding true_annots_def by (auto simp add: true_annot_def true_cls_def
atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set Ball_mset_def
split: split_if_asm)
have [simp]: "trail (reduce_trail_to M1 T) = M1"
by (metis (mono_tags, lifting) One_nat_def Pair_inject T ‹V ∼ tl_trail T› decomp
diff_less in_get_all_decided_decomposition_trail_update_trail length_greater_0_conv
length_tl lessI list.distinct(1) reduce_trail_to_length_ne state_eq_trail
trail_reduce_trail_to_length_le trail_tl_trail)
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 = N" and [simp]: "learned_clss S = U"
using rtranclp_skip_state_decomp[OF ‹skip⇧*⇧* S V›] V
by (auto simp del: state_simp simp: state_eq_def state_access_simp)
then have W_S: "W ∼ cons_trail (Propagated L (D + {#L#})) (reduce_trail_to M1
(add_learned_cls (D + {#L#}) (update_backtrack_lvl i (update_conflicting None T))))"
using W i T undef M_lev by (auto simp del: state_simp simp: state_eq_def cdcl⇩W_M_level_inv_def)
obtain M2' where
"(Decided K (i+1) # M1, M2') ∈ set (get_all_decided_decomposition ?M)"
using decomp V by (cases "hd (get_all_decided_decomposition (trail V))",
cases "get_all_decided_decomposition (trail V)") auto
moreover
from L_L' have "get_level ?M L = k"
using lev_L ‹-L' ∉# ?D› V by (auto split: split_if_asm)
moreover
have "atm_of L' ∉ atms_of D"
using ‹L' ∉# ?D› ‹-L' ∉# ?D› by (simp add: atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set
atms_of_def)
then have "get_level ?M L = get_maximum_level ?M (D+{#L#})"
using lev_l_D[symmetric] L_L' V lev_L by simp
moreover have "i = get_maximum_level ?M D"
using i ‹atm_of L' ∉ atms_of D› by auto
moreover
ultimately have "backtrack T W"
using T(1) W_S by blast
then show ?thesis using IH inv by blast
qed
lemma fst_get_all_decided_decomposition_prepend_not_decided:
assumes "∀m∈set MS. ¬ is_decided m"
shows "set (map fst (get_all_decided_decomposition M))
= set (map fst (get_all_decided_decomposition (MS @ M)))"
using assms apply (induction MS rule: ann_literal_list_induct)
apply auto[2]
by (rename_tac L m xs; case_tac "get_all_decided_decomposition (xs @ M)") simp_all
text ‹See also @{thm 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!: backtrack_levE)
then obtain k M M1 M2 K i D L N U where
S: "state S = (M, N, U, k, Some (D + {#L#}))" and
W: "state W = (Propagated L (D + {#L#}) # M1, N, {#D + {#L#}#} + U, get_maximum_level M D,
None)" and
decomp: "(Decided K (i+1) # M1, M2) ∈ set (get_all_decided_decomposition M)" and
lev_l: "get_level M L = k" and
lev_l_D: "get_level M L = get_maximum_level M (D+{#L#})" and
i: "i = get_maximum_level M D" and
undef: "undefined_lit M1 L"
using bt by (elim backtrack_levE)
(simp_all add: cdcl⇩W_M_level_inv_decomp state_eq_def del: state_simp)
let ?D = "(D + {#L#})"
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] 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: "M = 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 M_lev by auto
have T: "state T = (M⇩T, N, U, k, Some ?D)"
using M⇩T rtranclp_skip_state_decomp(2)[of S T] skip S
by (auto simp del: state_simp simp: state_eq_def state_access_simp)
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] by blast
then have "M⇩T ⊨as CNot ?D"
unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_conflicting_def using T by blast
have "∀L∈#?D. atm_of L ∈ atm_of ` lits_of M⇩T"
proof -
have f1: "⋀l. ¬ M⇩T ⊨a {#- l#} ∨ atm_of l ∈ atm_of ` lits_of M⇩T"
by (simp add: atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set in_lit_of_true_annot
lits_of_def)
have "⋀l. l ∉# D ∨ - l ∈ lits_of M⇩T"
using ‹M⇩T ⊨as CNot (D + {#L#})› multi_member_split by fastforce
then show ?thesis
using f1 by (meson ‹M⇩T ⊨as CNot (D + {#L#})› ball_msetI true_annots_CNot_all_atms_defined)
qed
moreover have "no_dup M"
using inv S unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_M_level_inv_def by auto
ultimately have "∀L∈#?D. atm_of L ∉ atm_of ` lits_of MS"
unfolding M unfolding lits_of_def by auto
then have H: "⋀L. L∈#?D ⟹ get_level M L = get_level M⇩T L"
unfolding M by (fastforce simp: lits_of_def)
have [simp]: "get_maximum_level M ?D = get_maximum_level M⇩T ?D"
by (metis ‹M⇩T ⊨as CNot (D + {#L#})› M nm ball_msetI true_annots_CNot_all_atms_defined
get_maximum_level_skip_un_decided_not_present)
have lev_l': "get_level M⇩T L = k"
using lev_l by (auto simp: H)
have [simp]: "trail (reduce_trail_to M1 T) = M1"
using T decomp M nm by (smt M⇩T append_assoc beginning_not_decided_invert
get_all_decided_decomposition_exists_prepend reduce_trail_to_trail_tl_trail_decomp)
have W: "W ∼ cons_trail (Propagated L (D + {#L#})) (reduce_trail_to M1
(add_learned_cls (D + {#L#}) (update_backtrack_lvl i (update_conflicting None T))))"
using W T i decomp undef by (auto simp del: state_simp simp: state_eq_def)
have lev_l_D': "get_level M⇩T L = get_maximum_level M⇩T (D+{#L#})"
using lev_l_D by (auto simp: H)
have [simp]: "get_maximum_level M D = get_maximum_level M⇩T D"
proof -
have "⋀ms m. ¬ (ms::('v, nat, 'v literal multiset) ann_literal list) ⊨as CNot m
∨ (∀l∈#m. atm_of l ∈ atm_of ` lits_of ms)"
by (simp add: atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set in_CNot_implies_uminus(2))
then have "∀l∈#D. atm_of l ∈ atm_of ` lits_of M⇩T"
using ‹M⇩T ⊨as CNot (D + {#L#})› by auto
then show ?thesis
by (metis M get_maximum_level_skip_un_decided_not_present nm)
qed
then have i': "i = get_maximum_level M⇩T D"
using i by auto
have "Decided K (i + 1) # M1 ∈ set (map fst (get_all_decided_decomposition M))"
using Set.imageI[OF decomp, of fst] by auto
then have "Decided K (i + 1) # M1 ∈ set (map fst (get_all_decided_decomposition M⇩T))"
using fst_get_all_decided_decomposition_prepend_not_decided[OF nm] unfolding M by auto
then obtain M2' where decomp':"(Decided K (i+1) # M1, M2') ∈ set (get_all_decided_decomposition M⇩T)"
by auto
then show "backtrack T W"
using backtrack.intros[OF T decomp' lev_l'] lev_l_D' i' W by force
qed
lemma cdcl⇩W_bj_decomp_resolve_skip_and_bj:
assumes "cdcl⇩W_bj⇧*⇧* S T" and inv: "cdcl⇩W_M_level_inv S"
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
have "cdcl⇩W⇧*⇧* S V"
using ‹skip_or_resolve⇧*⇧* S V› rtranclp_skip_or_resolve_rtranclp_cdcl⇩W by blast
then have "cdcl⇩W_M_level_inv V" and "cdcl⇩W_M_level_inv S"
using rtranclp_cdcl⇩W_consistent_inv inv by blast+
with bj bt have False using backtrack_no_cdcl⇩W_bj by simp
}
then show ?thesis using IH inv 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)+
qed
lemma resolve_skip_deterministic:
"resolve S T ⟹ skip S U ⟹ False"
by fastforce
lemma backtrack_unique:
assumes
bt_T: "backtrack S T" and
bt_U: "backtrack S U" and
inv: "cdcl⇩W_all_struct_inv S"
shows "T ∼ U"
proof -
have lev: "cdcl⇩W_M_level_inv S"
using inv unfolding cdcl⇩W_all_struct_inv_def by auto
then obtain M N U' k D L i K M1 M2 where
S: "state S = (M, N, U', k, Some (D + {#L#}))" and
decomp: "(Decided K (i+1) # M1, M2) ∈ set (get_all_decided_decomposition M)" and
"get_level M L = k" and
"get_level M L = get_maximum_level M (D+{#L#})" and
"get_maximum_level M D = i" and
T: "state T = (Propagated L ( (D+{#L#})) # M1 , N, {#D + {#L#}#} + U', i, None)" and
undef: "undefined_lit M1 L"
using bt_T by (elim backtrack_levE)
(force simp: cdcl⇩W_M_level_inv_def state_eq_def simp del: state_simp)+
obtain D' L' i' K' M1' M2' where
S': "state S = (M, N, U', k, Some (D' + {#L'#}))" and
decomp': "(Decided K' (i'+1) # M1', M2') ∈ set (get_all_decided_decomposition M)" and
"get_level M L' = k" and
"get_level M L' = get_maximum_level M (D'+{#L'#})" and
"get_maximum_level M D' = i'" and
U: "state U = (Propagated L' (D'+{#L'#}) # M1', N, {#D' + {#L'#}#} +U', i', None)" and
undef: "undefined_lit M1' L'"
using bt_U lev S by (elim backtrack_levE)
(force simp: cdcl⇩W_M_level_inv_def state_eq_def simp del: state_simp)+
obtain c where M: "M = c @ M2 @ Decided K (i + 1) # M1"
using decomp by auto
obtain c' where M': "M = c' @ M2' @ Decided K' (i' + 1) # M1'"
using decomp' by auto
have decided: "get_all_levels_of_decided M = rev [1..<1+k]"
using inv S unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_M_level_inv_def by auto
then have "i < k"
unfolding M
by (force simp add: rev_swap[symmetric] dest!: arg_cong[of _ _ set])
have [simp]: "L = L'"
proof (rule ccontr)
assume "¬ ?thesis"
then have "L' ∈# D"
using S unfolding S' by (fastforce simp: multiset_eq_iff split: split_if_asm)
then have "get_maximum_level M D ≥ k"
using ‹get_level M L' = k› get_maximum_level_ge_get_level by blast
then show False using ‹get_maximum_level M D = i› ‹i < k› by auto
qed
then have [simp]: "D = D'"
using S S' by auto
have [simp]: "i=i'" using ‹get_maximum_level M D' = i'› ‹get_maximum_level M D = i› by auto
text ‹Automation in a step later...›
have H: "⋀a A B. insert a A = B ⟹ a : B"
by blast
have "get_all_levels_of_decided (c@M2) = rev [i+2..<1+k]" and
"get_all_levels_of_decided (c'@M2') = rev [i+2..<1+k]"
using decided unfolding M
using decided unfolding M'
unfolding rev_swap[symmetric] by (auto dest: append_cons_eq_upt_length_i_end)
from arg_cong[OF this(1), of set] arg_cong[OF this(2), of set]
have
"dropWhile (λL. ¬is_decided L ∨ level_of L ≠ Suc i) (c @ M2) = []" and
"dropWhile (λL. ¬is_decided L ∨ level_of L ≠ Suc i) (c' @ M2') = []"
unfolding dropWhile_eq_Nil_conv Ball_def
by (intro allI; rename_tac x; case_tac x; auto dest!: H simp add: in_set_conv_decomp)+
then have "M1 = M1'"
using arg_cong[OF M, of "dropWhile (λL. ¬is_decided L ∨ level_of L ≠ Suc i)"]
unfolding M' by auto
then show ?thesis using T U by (auto simp del: state_simp simp: state_eq_def)
qed
lemma if_can_apply_backtrack_no_more_resolve:
assumes
skip: "skip⇧*⇧* S U" and
bt: "backtrack S T" and
inv: "cdcl⇩W_all_struct_inv S"
shows "¬resolve U V"
proof (rule ccontr)
assume resolve: "¬¬resolve U V"
obtain L C M N U' k D where
U: "state U = (Propagated L ( (C + {#L#})) # M, N, U', k, Some (D + {#-L#}))"and
"get_maximum_level (Propagated L (C + {#L#}) # M) D = k" and
"state V = (M, N, U', k, Some (D #∪ C))"
using resolve by auto
have "cdcl⇩W_all_struct_inv U"
using mono_rtranclp[of skip cdcl⇩W] by (meson bj cdcl⇩W_bj.skip inv local.skip other
rtranclp_cdcl⇩W_all_struct_inv_inv)
then have [iff]: "no_dup (trail S)" "cdcl⇩W_M_level_inv S" and [iff]: "no_dup (trail U)"
using inv unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_M_level_inv_def by blast+
then have
S: "init_clss S = N"
"learned_clss S = U'"
"backtrack_lvl S = k"
"conflicting S = Some (D + {#-L#})"
using rtranclp_skip_state_decomp(2)[OF skip] U
by (auto simp del: state_simp simp: state_eq_def state_access_simp)
obtain M⇩0 where
tr_S: "trail S = M⇩0 @ trail U" and
nm: "∀m∈set M⇩0. ¬is_decided m"
using rtranclp_skip_state_decomp[OF skip] by blast
obtain M' D' L' i K M1 M2 where
S': "state S = (M', N, U', k, Some (D' + {#L'#}))" and
decomp: "(Decided K (i+1) # M1, M2) ∈ set (get_all_decided_decomposition M')" and
"get_level M' L' = k" and
"get_level M' L' = get_maximum_level M' (D'+{#L'#})" and
"get_maximum_level M' D' = i" and
undef: "undefined_lit M1 L'" and
T: "state T = (Propagated L' (D'+{#L'#}) # M1 , N, {#D' + {#L'#}#}+U', i, None)"
using bt by (elim backtrack_levE) (fastforce simp: S state_eq_def simp del:state_simp)+
obtain c where M: "M' = c @ M2 @ Decided K (i + 1) # M1"
using get_all_decided_decomposition_exists_prepend[OF decomp] by auto
have decided: "get_all_levels_of_decided M' = rev [1..<1+k]"
using inv S' unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_M_level_inv_def by auto
then have "i < k"
unfolding M by (force simp add: rev_swap[symmetric] dest!: arg_cong[of _ _ set])
have DD': "D' + {#L'#} = D + {#-L#}"
using S S' by auto
have [simp]: "L' = -L"
proof (rule ccontr)
assume "¬ ?thesis"
then have "-L ∈# D'"
using DD' by (metis add_diff_cancel_right' diff_single_trivial diff_union_swap
multi_self_add_other_not_self)
moreover
have M': "M' = M⇩0 @ Propagated L ( (C + {#L#})) # M"
using tr_S U S S' by (auto simp: lits_of_def)
have "no_dup M'"
using inv U S' unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_M_level_inv_def by auto
have atm_L_notin_M: "atm_of L ∉ atm_of ` (lits_of M)"
using ‹no_dup M'› M' U S S' by (auto simp: lits_of_def)
have "get_all_levels_of_decided M' = rev [1..<1+k]"
using inv U S' unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_M_level_inv_def by auto
then have "get_all_levels_of_decided M = rev [1..<1+k]"
using nm M' S' U by (simp add: get_all_levels_of_decided_no_decided)
then have get_lev_L:
"get_level(Propagated L (C + {#L#}) # M) L = k"
using get_level_get_rev_level_get_all_levels_of_decided[OF atm_L_notin_M,
of "[Propagated L ((C + {#L#}))]"] by simp
have "atm_of L ∉ atm_of ` (lits_of (rev M⇩0))"
using ‹no_dup M'› M' U S' by (auto simp: lits_of_def)
then have "get_level M' L = k"
using get_rev_level_notin_end[of L "rev M⇩0"
"rev M @ Propagated L (C + {#L#}) # []" 0]
using tr_S get_lev_L M' U S' by (simp add:nm lits_of_def)
ultimately have "get_maximum_level M' D' ≥ k"
by (metis get_maximum_level_ge_get_level get_rev_level_uminus)
then show False
using ‹i < k› unfolding ‹get_maximum_level M' D' = i› by auto
qed
have [simp]: "D = D'" using DD' by auto
have "cdcl⇩W⇧*⇧* S U"
using bj cdcl⇩W_bj.skip local.skip mono_rtranclp[of skip cdcl⇩W S U] other by meson
then have "cdcl⇩W_all_struct_inv U"
using inv rtranclp_cdcl⇩W_all_struct_inv_inv by blast
then have "Propagated L ( (C + {#L#})) # M ⊨as CNot (D' + {#L'#})"
using cdcl⇩W_all_struct_inv_def cdcl⇩W_conflicting_def U by auto
then have "∀L'∈#D. atm_of L' ∈ atm_of ` lits_of (Propagated L ( (C + {#L#})) # M)"
by (metis CNot_plus CNot_singleton Un_insert_right ‹D = D'› true_annots_insert ball_msetI
atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set in_CNot_implies_uminus(2)
sup_bot.comm_neutral)
then have "get_maximum_level M' D = k"
using tr_S nm U S'
get_maximum_level_skip_un_decided_not_present[of D "
Propagated L (C + {#L#}) # M" M⇩0]
unfolding ‹get_maximum_level (Propagated L (C + {#L#}) # M) D = k›
unfolding ‹D = D'›
by simp
then show False
using ‹get_maximum_level M' D' = i› ‹i < k› by auto
qed
lemma if_can_apply_resolve_no_more_backtrack:
assumes
skip: "skip⇧*⇧* S U" and
resolve: "resolve S T" and
inv: "cdcl⇩W_all_struct_inv S"
shows "¬backtrack U V"
using assms
by (meson if_can_apply_backtrack_no_more_resolve rtranclp.rtrancl_refl
rtranclp_skip_backtrack_backtrack)
lemma if_can_apply_backtrack_skip_or_resolve_is_skip:
assumes
bt: "backtrack S T" and
skip: "skip_or_resolve⇧*⇧* S U" and
inv: "cdcl⇩W_all_struct_inv S"
shows "skip⇧*⇧* S U"
using assms(2,3,1)
by induction (simp_all add: if_can_apply_backtrack_no_more_resolve)
lemma cdcl⇩W_bj_bj_decomp:
assumes "cdcl⇩W_bj⇧*⇧* S W" and "cdcl⇩W_all_struct_inv S"
shows
"(∃T U V. (λS T. skip_or_resolve S T ∧ no_step backtrack S)⇧*⇧* S T
∧ (λT U. resolve T U ∧ no_step backtrack T) T U
∧ skip⇧*⇧* U V ∧ backtrack V W)
∨ (∃T U. (λS T. skip_or_resolve S T ∧ no_step backtrack S)⇧*⇧* S T
∧ (λT U. resolve T U ∧ no_step backtrack T) T U ∧ skip⇧*⇧* U W)
∨ (∃T. skip⇧*⇧* S T ∧ backtrack T W)
∨ skip⇧*⇧* S W" (is "?RB S W ∨ ?R S W ∨ ?SB S W ∨ ?S S W")
using assms
proof induction
case base
then show ?case by simp
next
case (step W X) note st = this(1) and bj = this(2) and IH = this(3)[OF this(4)] and inv = this(4)
have "¬?RB S W" and "¬?SB S W"
proof (clarify, goal_cases)
case (1 T U V)
have "skip_or_resolve⇧*⇧* S T"
using 1(1) by (auto dest!: rtranclp_and_rtranclp_left)
then show "False"
by (metis (no_types, lifting) "1"(2) "1"(4) "1"(5) backtrack_no_cdcl⇩W_bj
cdcl⇩W_all_struct_inv_def cdcl⇩W_all_struct_inv_inv cdcl⇩W_o.bj local.bj other
resolve rtranclp_cdcl⇩W_all_struct_inv_inv rtranclp_skip_backtrack_backtrack
rtranclp_skip_or_resolve_rtranclp_cdcl⇩W step.prems)
next
case 2
then show ?case by (meson assms(2) cdcl⇩W_all_struct_inv_def backtrack_no_cdcl⇩W_bj
local.bj rtranclp_skip_backtrack_backtrack)
qed
then have IH: "?R S W ∨ ?S S W" using IH by blast
have "cdcl⇩W⇧*⇧* S W" by (metis cdcl⇩W_o.bj mono_rtranclp other st)
then have inv_W: "cdcl⇩W_all_struct_inv W" by (simp add: rtranclp_cdcl⇩W_all_struct_inv_inv
step.prems)
consider
(BT) X' where "backtrack W X'"
| (skip) "no_step backtrack W" and "skip W X"
| (resolve) "no_step backtrack W" and "resolve W X"
using bj cdcl⇩W_bj.cases by meson
then show ?case
proof cases
case (BT X')
then consider
(bt) "backtrack W X"
| (sk) "skip W X"
using bj if_can_apply_backtrack_no_more_resolve[of W W X' X] inv_W cdcl⇩W_bj.cases by fast
then show ?thesis
proof cases
case bt
then show ?thesis using IH by auto
next
case sk
then show ?thesis using IH by (meson rtranclp_trans r_into_rtranclp)
qed
next
case skip
then show ?thesis using IH by (meson rtranclp.rtrancl_into_rtrancl)
next
case resolve note no_bt = this(1) and res = this(2)
consider
(RS) T U where
"(λS T. skip_or_resolve S T ∧ no_step backtrack S)⇧*⇧* S T" and
"resolve T U" and
"no_step backtrack T" and
"skip⇧*⇧* U W"
| (S) "skip⇧*⇧* S W"
using IH by auto
then show ?thesis
proof cases
case (RS T U)
have "cdcl⇩W⇧*⇧* S T"
using RS(1) cdcl⇩W_bj.resolve cdcl⇩W_o.bj other skip
mono_rtranclp[of " (λS T. skip_or_resolve S T ∧ no_step backtrack S)" cdcl⇩W S T]
by meson
then have "cdcl⇩W_all_struct_inv U"
by (meson RS(2) cdcl⇩W_all_struct_inv_inv cdcl⇩W_bj.resolve cdcl⇩W_o.bj other
rtranclp_cdcl⇩W_all_struct_inv_inv step.prems)
{ fix U'
assume "skip⇧*⇧* U U'" and "skip⇧*⇧* U' W"
have "cdcl⇩W_all_struct_inv U'"
using ‹cdcl⇩W_all_struct_inv U› ‹skip⇧*⇧* U U'› rtranclp_cdcl⇩W_all_struct_inv_inv
cdcl⇩W_o.bj rtranclp_mono[of skip cdcl⇩W] other skip by blast
then have "no_step backtrack U'"
using if_can_apply_backtrack_no_more_resolve[OF ‹skip⇧*⇧* U' W› ] res by blast
}
with ‹skip⇧*⇧* U W›
have "(λS T. skip_or_resolve S T ∧ no_step backtrack S)⇧*⇧* U W"
proof induction
case base
then show ?case by simp
next
case (step V W) note st = this(1) and skip = this(2) and IH = this(3) and H = this(4)
have "⋀U'. skip⇧*⇧* U' V ⟹ skip⇧*⇧* U' W"
using skip by auto
then have "(λS T. skip_or_resolve S T ∧ no_step backtrack S)⇧*⇧* U V"
using IH H by blast
moreover have "(λS T. skip_or_resolve S T ∧ no_step backtrack S)⇧*⇧* V W"
by (simp add: local.skip r_into_rtranclp st step.prems)
ultimately show ?case by simp
qed
then show ?thesis
proof -
have f1: "∀p pa pb pc. ¬ p (pa) pb ∨ ¬ p⇧*⇧* pb pc ∨ p⇧*⇧* pa pc"
by (meson converse_rtranclp_into_rtranclp)
have "skip_or_resolve T U ∧ no_step backtrack T"
using RS(2) RS(3) by force
then have "(λp pa. skip_or_resolve p pa ∧ no_step backtrack p)⇧*⇧* T W"
proof -
have "(∃vr19 vr16 vr17 vr18. vr19 (vr16::'st) vr17 ∧ vr19⇧*⇧* vr17 vr18
∧ ¬ vr19⇧*⇧* vr16 vr18)
∨ ¬ (skip_or_resolve T U ∧ no_step backtrack T)
∨ ¬ (λuu uua. skip_or_resolve uu uua ∧ no_step backtrack uu)⇧*⇧* U W
∨ (λuu uua. skip_or_resolve uu uua ∧ no_step backtrack uu)⇧*⇧* T W"
by force
then show ?thesis
by (metis (no_types) ‹(λS T. skip_or_resolve S T ∧ no_step backtrack S)⇧*⇧* U W›
‹skip_or_resolve T U ∧ no_step backtrack T› f1)
qed
then have "(λp pa. skip_or_resolve p pa ∧ no_step backtrack p)⇧*⇧* S W"
using RS(1) by force
then show ?thesis
using no_bt res by blast
qed
next
case S
{ fix U'
assume "skip⇧*⇧* S U'" and "skip⇧*⇧* U' W"
then have "cdcl⇩W⇧*⇧* S U'"
using mono_rtranclp[of skip cdcl⇩W S U'] by (simp add: cdcl⇩W_o.bj other skip)
then have "cdcl⇩W_all_struct_inv U'"
by (metis (no_types, hide_lams) ‹cdcl⇩W_all_struct_inv S›
rtranclp_cdcl⇩W_all_struct_inv_inv)
then have "no_step backtrack U'"
using if_can_apply_backtrack_no_more_resolve[OF ‹skip⇧*⇧* U' W› ] res by blast
}
with S
have "(λS T. skip_or_resolve S T ∧ no_step backtrack S)⇧*⇧* S W"
proof induction
case base
then show ?case by simp
next
case (step V W) note st = this(1) and skip = this(2) and IH = this(3) and H = this(4)
have "⋀U'. skip⇧*⇧* U' V ⟹ skip⇧*⇧* U' W"
using skip by auto
then have "(λS T. skip_or_resolve S T ∧ no_step backtrack S)⇧*⇧* S V"
using IH H by blast
moreover have "(λS T. skip_or_resolve S T ∧ no_step backtrack S)⇧*⇧* V W"
by (simp add: local.skip r_into_rtranclp st step.prems)
ultimately show ?case by simp
qed
then show ?thesis using res no_bt by blast
qed
qed
qed
text ‹The case distinction is needed, since @{term "T ∼ V"} does not imply that @{term "R⇧*⇧* T V"}.›
lemma cdcl⇩W_bj_strongly_confluent:
assumes
"cdcl⇩W_bj⇧*⇧* S V" and
"cdcl⇩W_bj⇧*⇧* S T" and
n_s: "no_step cdcl⇩W_bj V" and
inv: "cdcl⇩W_all_struct_inv S"
shows "T ∼ V ∨ cdcl⇩W_bj⇧*⇧* T V"
using assms(2)
proof induction
case base
then show ?case by (simp add: assms(1))
next
case (step T U) note st = this(1) and s_o_r = this(2) and IH = this(3)
have "cdcl⇩W⇧*⇧* S T"
using st mono_rtranclp[of cdcl⇩W_bj cdcl⇩W] other by blast
then have lev_T: "cdcl⇩W_M_level_inv T"
using inv rtranclp_cdcl⇩W_consistent_inv[of S T]
unfolding cdcl⇩W_all_struct_inv_def by auto
consider
(TV) "T ∼ V"
| (bj_TV) "cdcl⇩W_bj⇧*⇧* T V"
using IH by blast
then show ?case
proof cases
case TV
have "no_step cdcl⇩W_bj T"
using ‹cdcl⇩W_M_level_inv T› n_s cdcl⇩W_bj_state_eq_compatible[of T _ V] TV by auto
then show ?thesis
using s_o_r by auto
next
case bj_TV
then obtain U' where
T_U': "cdcl⇩W_bj T U'" and
"cdcl⇩W_bj⇧*⇧* U' V"
using IH n_s s_o_r by (metis rtranclp_unfold tranclpD)
have "cdcl⇩W⇧*⇧* S T"
by (metis (no_types, hide_lams) bj mono_rtranclp[of cdcl⇩W_bj cdcl⇩W] other st)
then have inv_T: "cdcl⇩W_all_struct_inv T"
by (metis (no_types, hide_lams) inv rtranclp_cdcl⇩W_all_struct_inv_inv)
have lev_U: "cdcl⇩W_M_level_inv U"
using s_o_r cdcl⇩W_consistent_inv lev_T other by blast
show ?thesis
using s_o_r
proof cases
case backtrack
then obtain V0 where "skip⇧*⇧* T V0" and "backtrack V0 V"
using IH if_can_apply_backtrack_skip_or_resolve_is_skip[OF backtrack _ inv_T]
cdcl⇩W_bj_decomp_resolve_skip_and_bj
by (meson bj_TV cdcl⇩W_bj.backtrack inv_T lev_T n_s
rtranclp_skip_backtrack_backtrack_end)
then have "cdcl⇩W_bj⇧*⇧* T V0" and "cdcl⇩W_bj V0 V"
using rtranclp_mono[of skip cdcl⇩W_bj] by blast+
then show ?thesis
using ‹backtrack V0 V› ‹skip⇧*⇧* T V0› backtrack_unique inv_T local.backtrack
rtranclp_skip_backtrack_backtrack by auto
next
case resolve
then have "U ∼ U'"
by (meson T_U' cdcl⇩W_bj.simps if_can_apply_backtrack_no_more_resolve inv_T
resolve_skip_deterministic resolve_unique rtranclp.rtrancl_refl)
then show ?thesis
using ‹cdcl⇩W_bj⇧*⇧* U' V› unfolding rtranclp_unfold
by (meson T_U' bj cdcl⇩W_consistent_inv lev_T other state_eq_ref state_eq_sym
tranclp_cdcl⇩W_bj_state_eq_compatible)
next
case skip
consider
(sk) "skip T U'"
| (bt) "backtrack T U'"
using T_U' by (meson cdcl⇩W_bj.cases local.skip resolve_skip_deterministic)
then show ?thesis
proof cases
case sk
then show ?thesis
using ‹cdcl⇩W_bj⇧*⇧* U' V› unfolding rtranclp_unfold
by (meson T_U' bj cdcl⇩W_all_inv(3) cdcl⇩W_all_struct_inv_def inv_T local.skip other
tranclp_cdcl⇩W_bj_state_eq_compatible skip_unique state_eq_ref)
next
case bt
have "skip⇧+⇧+ T U"
using local.skip by blast
then show ?thesis
using bt by (metis ‹cdcl⇩W_bj⇧*⇧* U' V› backtrack inv_T tranclp_unfold_begin
rtranclp_skip_backtrack_backtrack_end tranclp_into_rtranclp)
qed
qed
qed
qed
lemma cdcl⇩W_bj_unique_normal_form:
assumes
ST: "cdcl⇩W_bj⇧*⇧* S T" and SU: "cdcl⇩W_bj⇧*⇧* S U" and
n_s_U: "no_step cdcl⇩W_bj U" and
n_s_T: "no_step cdcl⇩W_bj T" and
inv: "cdcl⇩W_all_struct_inv S"
shows "T ∼ U"
proof -
have "T ∼ U ∨ cdcl⇩W_bj⇧*⇧* T U"
using ST SU cdcl⇩W_bj_strongly_confluent inv n_s_U by blast
then show ?thesis
by (metis (no_types) n_s_T rtranclp_unfold state_eq_ref tranclp_unfold_begin)
qed
lemma full_cdcl⇩W_bj_unique_normal_form:
assumes "full cdcl⇩W_bj S T" and "full cdcl⇩W_bj S U" and
inv: "cdcl⇩W_all_struct_inv S"
shows "T ∼ U"
using cdcl⇩W_bj_unique_normal_form assms unfolding full_def by blast
subsection ‹CDCL FW›
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 cdcl⇩W_merge_restart_cdcl⇩W:
assumes "cdcl⇩W_merge_restart S T"
shows "cdcl⇩W⇧*⇧* S T"
using assms
proof induction
case (fw_r_conflict S T U) note confl = this(1) and bj = this(2)
have "cdcl⇩W S T" using confl by (simp add: cdcl⇩W.intros r_into_rtranclp)
moreover
have "cdcl⇩W_bj⇧*⇧* T U" using bj unfolding full_def by auto
then have "cdcl⇩W⇧*⇧* T U" by (metis cdcl⇩W_o.bj mono_rtranclp other)
ultimately show ?case by auto
qed (simp_all add: cdcl⇩W_o.intros cdcl⇩W.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 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 U V" and "conflicting U = Some D"
then have False
using n_s unfolding full_def
by (induction rule: cdcl⇩W_all_rules_induct) (auto dest!: cdcl⇩W_bj.intros )
}
then show ?case by (cases "conflicting U") fastforce+
qed (auto simp add: cdcl⇩W_rf.simps)
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:
"cdcl⇩W_merge S T ⟹ cdcl⇩W⇧*⇧* S T"
using cdcl⇩W_merge_cdcl⇩W_merge_restart cdcl⇩W_merge_restart_cdcl⇩W by blast
lemma rtranclp_cdcl⇩W_merge_rtranclp_cdcl⇩W:
"cdcl⇩W_merge⇧*⇧* S T ⟹ cdcl⇩W⇧*⇧* S T"
using rtranclp_mono[of cdcl⇩W_merge "cdcl⇩W⇧*⇧*"] cdcl⇩W_merge_rtranclp_cdcl⇩W by auto
lemma cdcl⇩W_merge_is_cdcl⇩N⇩O⇩T_merged_bj_learn:
assumes
inv: "cdcl⇩W_all_struct_inv S" and
cdcl⇩W:"cdcl⇩W_merge S T"
shows "cdcl⇩N⇩O⇩T_merged_bj_learn S T
∨ (no_step cdcl⇩W_merge T ∧ conflicting T ≠ None)"
using cdcl⇩W inv
proof induction
case (fw_propagate S T) note propa = this(1)
then obtain M N U k L C where
H: "state S = (M, N, U, k, None)" and
CL: "C + {#L#} ∈# clauses S" and
M_C: "M ⊨as CNot C" and
undef: "undefined_lit (trail S) L" and
T: "T ∼ cons_trail (Propagated L (C + {#L#})) S"
using propa by auto
have "propagate⇩N⇩O⇩T S T"
apply (rule propagate⇩N⇩O⇩T.propagate⇩N⇩O⇩T[of _ C L])
using H CL T undef M_C by (auto simp: state_eq⇩N⇩O⇩T_def state_eq_def clauses_def
simp del: state_simp)
then show ?case
using cdcl⇩N⇩O⇩T_merged_bj_learn.intros(2) by blast
next
case (fw_decide S T) note dec = this(1) and inv = this(2)
then obtain L where
undef_L: "undefined_lit (trail S) L" and
atm_L: "atm_of L ∈ atms_of_msu (init_clss S)" and
T: "T ∼ cons_trail (Decided L (Suc (backtrack_lvl S)))
(update_backtrack_lvl (Suc (backtrack_lvl S)) S)"
by auto
have "decide⇩N⇩O⇩T S T"
apply (rule decide⇩N⇩O⇩T.decide⇩N⇩O⇩T)
using undef_L apply simp
using atm_L inv unfolding cdcl⇩W_all_struct_inv_def no_strange_atm_def clauses_def apply auto[]
using T undef_L unfolding state_eq_def state_eq⇩N⇩O⇩T_def by (auto simp: clauses_def)
then show ?case using cdcl⇩N⇩O⇩T_merged_bj_learn_decide⇩N⇩O⇩T by blast
next
case (fw_forget S T) note rf =this(1) and inv = this(2)
then obtain M N C U k where
S: "state S = (M, N, {#C#} + U, k, None)" and
"¬ M ⊨asm clauses S" and
"C ∉ set (get_all_mark_of_propagated (trail S))" and
C_init: "C ∉# init_clss S" and
C_le: "C ∈# learned_clss S" and
T: "T ∼ remove_cls C S"
by auto
have "init_clss S ⊨pm C"
using inv C_le unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_learned_clause_def
by (meson mem_set_mset_iff true_clss_clss_in_imp_true_clss_cls)
then have S_C: "clauses S - replicate_mset (count (clauses S) C) C ⊨pm C"
using C_init C_le unfolding clauses_def by (simp add: Un_Diff)
moreover have H: "init_clss S + (learned_clss S - replicate_mset (count (learned_clss S) C) C)
= init_clss S + learned_clss S - replicate_mset (count (learned_clss S) C) C"
using C_le C_init by (metis clauses_def clauses_remove_cls diff_zero gr0I
init_clss_remove_cls learned_clss_remove_cls plus_multiset.rep_eq replicate_mset_0
semiring_normalization_rules(5))
have "forget⇩N⇩O⇩T S T"
apply (rule forget⇩N⇩O⇩T.forget⇩N⇩O⇩T)
using S_C apply blast
using S apply simp
using ‹C ∈# learned_clss S› apply (simp add: clauses_def)
using T C_le C_init by (auto
simp: state_eq_def Un_Diff state_eq⇩N⇩O⇩T_def clauses_def ac_simps H
simp del: state_simp)
then show ?case using cdcl⇩N⇩O⇩T_merged_bj_learn_forget⇩N⇩O⇩T by blast
next
case (fw_conflict S T U) note confl = this(1) and bj = this(2) and inv = this(3)
obtain C⇩S where
confl_T: "conflicting T = Some C⇩S" and
C⇩S: "C⇩S ∈# clauses S" and
tr_S_C⇩S: "trail S ⊨as CNot C⇩S"
using confl by auto
have "cdcl⇩W_all_struct_inv T"
using cdcl⇩W.simps cdcl⇩W_all_struct_inv_inv confl inv by blast
then have "cdcl⇩W_M_level_inv T"
unfolding cdcl⇩W_all_struct_inv_def by auto
then consider
(no_bt) "skip_or_resolve⇧*⇧* T U"
| (bt) T' where "skip_or_resolve⇧*⇧* T T'" and "backtrack T' U"
using bj rtranclp_cdcl⇩W_bj_skip_or_resolve_backtrack unfolding full_def by meson
then show ?case
proof cases
case no_bt
then have "conflicting U ≠ None"
using confl by (induction rule: rtranclp_induct) auto
moreover then have "no_step cdcl⇩W_merge U"
by (auto simp: cdcl⇩W_merge.simps)
ultimately show ?thesis by blast
next
case bt note s_or_r = this(1) and bt = this(2)
have "cdcl⇩W⇧*⇧* T T'"
using s_or_r mono_rtranclp[of skip_or_resolve cdcl⇩W] rtranclp_skip_or_resolve_rtranclp_cdcl⇩W
by blast
then have "cdcl⇩W_M_level_inv T'"
using rtranclp_cdcl⇩W_consistent_inv ‹cdcl⇩W_M_level_inv T› by blast
then obtain M1 M2 i D L K where
confl_T': "conflicting T' = Some (D + {#L#})" and
M1_M2:"(Decided K (i+1) # M1, M2) ∈ set (get_all_decided_decomposition (trail T'))" and
"get_level (trail T') L = backtrack_lvl T'" and
"get_level (trail T') L = get_maximum_level (trail T') (D+{#L#})" and
"get_maximum_level (trail T') D = i" and
undef_L: "undefined_lit M1 L" and
U: "U ∼ cons_trail (Propagated L (D+{#L#}))
(reduce_trail_to M1
(add_learned_cls (D + {#L#})
(update_backtrack_lvl i
(update_conflicting None T'))))"
using bt by (auto elim: backtrack_levE)
have [simp]: "clauses S = clauses T"
using confl by auto
have [simp]: "clauses T = clauses T'"
using s_or_r
proof (induction)
case base
then show ?case by simp
next
case (step U V) note st = this(1) and s_o_r = this(2) and IH = this(3)
have "clauses U = clauses V"
using s_o_r by auto
then show ?case using IH by auto
qed
have inv_T: "cdcl⇩W_all_struct_inv T"
by (meson cdcl⇩W_cp.simps confl inv r_into_rtranclp rtranclp_cdcl⇩W_all_struct_inv_inv
rtranclp_cdcl⇩W_cp_rtranclp_cdcl⇩W)
have "cdcl⇩W⇧*⇧* T T'"
using rtranclp_skip_or_resolve_rtranclp_cdcl⇩W s_or_r by blast
have inv_T': "cdcl⇩W_all_struct_inv T'"
using ‹cdcl⇩W⇧*⇧* T T'› inv_T rtranclp_cdcl⇩W_all_struct_inv_inv by blast
have inv_U: "cdcl⇩W_all_struct_inv U"
using cdcl⇩W_merge_restart_cdcl⇩W confl fw_r_conflict inv local.bj
rtranclp_cdcl⇩W_all_struct_inv_inv by blast
have [simp]: "init_clss S = init_clss T'"
using ‹cdcl⇩W⇧*⇧* T T'› cdcl⇩W_init_clss confl cdcl⇩W_all_struct_inv_def conflict inv
by (metis ‹cdcl⇩W_M_level_inv T› rtranclp_cdcl⇩W_init_clss)
then have atm_L: "atm_of L ∈ atms_of_msu (clauses S)"
using inv_T' confl_T' unfolding cdcl⇩W_all_struct_inv_def no_strange_atm_def clauses_def
by auto
obtain M where tr_T: "trail T = M @ trail T'"
using s_or_r by (induction rule: rtranclp_induct) auto
obtain M' where
tr_T': "trail T' = M' @ Decided K (i+1) # tl (trail U)" and
tr_U: "trail U = Propagated L (D + {#L#}) # tl (trail U)"
using U M1_M2 undef_L inv_T' unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_M_level_inv_def
by fastforce
def M'' ≡ "M @ M'"
have tr_T: "trail S = M'' @ Decided K (i+1) # tl (trail U)"
using tr_T tr_T' confl unfolding M''_def by auto
have "init_clss T' + learned_clss S ⊨pm D + {#L#}"
using inv_T' confl_T' unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_learned_clause_def clauses_def
by simp
have "reduce_trail_to (convert_trail_from_NOT (convert_trail_from_W M1)) S =
reduce_trail_to M1 S"
by (rule reduce_trail_to_length) simp
moreover have "trail (reduce_trail_to M1 S) = M1"
apply (rule reduce_trail_to_skip_beginning[of _ "M @ _ @ M2 @ [Decided K (Suc i)]"])
using confl M1_M2 ‹trail T = M @ trail T'›
apply (auto dest!: get_all_decided_decomposition_exists_prepend
elim!: conflictE)
by (rule sym) auto
ultimately have [simp]: "trail (reduce_trail_to⇩N⇩O⇩T (convert_trail_from_W M1) S) = M1"
using M1_M2 confl by (auto simp add: reduce_trail_to⇩N⇩O⇩T_reduce_trail_convert)
have "every_mark_is_a_conflict U"
using inv_U unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_conflicting_def by simp
then have "tl (trail U) ⊨as CNot D"
by (metis add_diff_cancel_left' append_self_conv2 tr_U union_commute)
have "backjump_l S U"
apply (rule backjump_l[of _ _ _ _ _ L])
using tr_T apply simp
using inv unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_M_level_inv_def
apply (simp add: comp_def)
using U M1_M2 confl undef_L M1_M2 inv_T' inv unfolding cdcl⇩W_all_struct_inv_def
cdcl⇩W_M_level_inv_def apply (auto simp: state_eq⇩N⇩O⇩T_def
trail_reduce_trail_to⇩N⇩O⇩T_add_learned_cls)[]
using C⇩S apply simp
using tr_S_C⇩S apply simp
using U undef_L M1_M2 inv_T' inv unfolding cdcl⇩W_all_struct_inv_def
cdcl⇩W_M_level_inv_def apply auto[]
using undef_L atm_L apply (simp add: trail_reduce_trail_to⇩N⇩O⇩T_add_learned_cls)
using ‹init_clss T' + learned_clss S ⊨pm D + {#L#}› unfolding clauses_def apply simp
apply (metis ‹tl (trail U) ⊨as CNot D› convert_trail_from_W_true_annots)
using inv_T' inv_U U confl_T' undef_L M1_M2 unfolding cdcl⇩W_all_struct_inv_def
distinct_cdcl⇩W_state_def by (simp add: cdcl⇩W_M_level_inv_decomp backjump_l_cond_def)
then show ?thesis using cdcl⇩N⇩O⇩T_merged_bj_learn_backjump_l by fast
qed
qed
abbreviation cdcl⇩N⇩O⇩T_restart where
"cdcl⇩N⇩O⇩T_restart ≡ restart_ops.cdcl⇩N⇩O⇩T_raw_restart cdcl⇩N⇩O⇩T restart"
lemma cdcl⇩W_merge_restart_is_cdcl⇩N⇩O⇩T_merged_bj_learn_restart_no_step:
assumes
inv: "cdcl⇩W_all_struct_inv S" and
cdcl⇩W:"cdcl⇩W_merge_restart S T"
shows "cdcl⇩N⇩O⇩T_restart⇧*⇧* S T ∨ (no_step cdcl⇩W_merge T ∧ conflicting T ≠ None)"
proof -
consider
(fw) "cdcl⇩W_merge S T"
| (fw_r) "restart S T"
using cdcl⇩W by (meson cdcl⇩W_merge_restart.simps cdcl⇩W_rf.cases fw_conflict fw_decide fw_forget
fw_propagate)
then show ?thesis
proof cases
case fw
then have IH: "cdcl⇩N⇩O⇩T_merged_bj_learn S T ∨ (no_step cdcl⇩W_merge T ∧ conflicting T ≠ None)"
using inv cdcl⇩W_merge_is_cdcl⇩N⇩O⇩T_merged_bj_learn by blast
have invS: "inv⇩N⇩O⇩T S"
using inv unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_M_level_inv_def by auto
have ff2: "cdcl⇩N⇩O⇩T⇧+⇧+ S T ⟶ cdcl⇩N⇩O⇩T⇧*⇧* S T"
by (meson tranclp_into_rtranclp)
have ff3: "no_dup (convert_trail_from_W (trail S))"
using invS by (simp add: comp_def)
have "cdcl⇩N⇩O⇩T ≤ cdcl⇩N⇩O⇩T_restart"
by (auto simp: restart_ops.cdcl⇩N⇩O⇩T_raw_restart.simps)
then show ?thesis
using ff3 ff2 IH cdcl⇩N⇩O⇩T_merged_bj_learn_is_tranclp_cdcl⇩N⇩O⇩T
rtranclp_mono[of cdcl⇩N⇩O⇩T cdcl⇩N⇩O⇩T_restart] invS predicate2D by blast
next
case fw_r
then show ?thesis by (blast intro: restart_ops.cdcl⇩N⇩O⇩T_raw_restart.intros)
qed
qed
abbreviation μ⇩F⇩W :: "'st ⇒ nat" where
"μ⇩F⇩W S ≡ (if no_step cdcl⇩W_merge S then 0 else 1+μ⇩C⇩D⇩C⇩L'_merged (set_mset (init_clss S)) S)"
lemma cdcl⇩W_merge_μ⇩F⇩W_decreasing:
assumes
inv: "cdcl⇩W_all_struct_inv S" and
fw: "cdcl⇩W_merge S T"
shows "μ⇩F⇩W T < μ⇩F⇩W S"
proof -
let ?A = "init_clss S"
have atm_clauses: "atms_of_msu (clauses S) ⊆ atms_of_msu ?A"
using inv unfolding cdcl⇩W_all_struct_inv_def no_strange_atm_def clauses_def by auto
have atm_trail: "atm_of ` lits_of (trail S) ⊆ atms_of_msu ?A"
using inv unfolding cdcl⇩W_all_struct_inv_def no_strange_atm_def clauses_def by auto
have n_d: "no_dup (trail S)"
using inv unfolding cdcl⇩W_all_struct_inv_def by (auto simp: cdcl⇩W_M_level_inv_decomp)
have [simp]: "¬ no_step cdcl⇩W_merge S"
using fw by auto
have [simp]: "init_clss S = init_clss T"
using cdcl⇩W_merge_restart_cdcl⇩W[of S T] inv rtranclp_cdcl⇩W_init_clss
unfolding cdcl⇩W_all_struct_inv_def
by (meson cdcl⇩W_merge.simps cdcl⇩W_merge_restart.simps cdcl⇩W_rf.simps fw)
consider
(merged) "cdcl⇩N⇩O⇩T_merged_bj_learn S T"
| (n_s) "no_step cdcl⇩W_merge T"
using cdcl⇩W_merge_is_cdcl⇩N⇩O⇩T_merged_bj_learn inv fw by blast
then show ?thesis
proof cases
case merged
then show ?thesis
using cdcl⇩N⇩O⇩T_decreasing_measure'[OF _ _ atm_clauses] atm_trail n_d
by (auto split: split_if simp: comp_def)
next
case n_s
then show ?thesis by simp
qed
qed
lemma wf_cdcl⇩W_merge: "wf {(T, S). cdcl⇩W_all_struct_inv S ∧ cdcl⇩W_merge S T}"
apply (rule wfP_if_measure[of _ _ "μ⇩F⇩W"])
using cdcl⇩W_merge_μ⇩F⇩W_decreasing by blast
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
assms(1) rtranclp_cdcl⇩W_all_struct_inv_inv rtranclp_mono[of cdcl⇩W_merge "cdcl⇩W⇧*⇧*"] 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 wf_tranclp_cdcl⇩W_merge: "wf {(T, S). cdcl⇩W_all_struct_inv S ∧ cdcl⇩W_merge⇧+⇧+ S T}"
using wf_trancl[OF wf_cdcl⇩W_merge]
apply (rule wf_subset)
by (auto simp: trancl_set_tranclp
cdcl⇩W_all_struct_inv_tranclp_cdcl⇩W_merge_tranclp_cdcl⇩W_merge_cdcl⇩W_all_struct_inv)
lemma backtrack_is_full1_cdcl⇩W_bj:
assumes bt: "backtrack S T" and inv: "cdcl⇩W_M_level_inv S"
shows "full1 cdcl⇩W_bj S T"
proof -
have "no_step cdcl⇩W_bj T"
using bt inv backtrack_no_cdcl⇩W_bj by blast
moreover have "cdcl⇩W_bj⇧+⇧+ S T"
using bt by auto
ultimately show ?thesis unfolding full1_def by blast
qed
lemma rtrancl_cdcl⇩W_conflicting_true_cdcl⇩W_merge_restart:
assumes "cdcl⇩W⇧*⇧* 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 = this(2) and IH = this(3)[OF this(4-)] and
confl[simp] = this(5) and inv = this(4)
from cdcl⇩W
show ?case
proof (cases)
case propagate
moreover then have "conflicting U = None"
by auto
moreover have "conflicting V = None"
using propagate by auto
ultimately show ?thesis using IH cdcl⇩W_merge_restart.fw_r_propagate[of U V] by auto
next
case conflict
moreover then have "conflicting U = None"
by auto
moreover have "conflicting V ≠ None"
using conflict by auto
ultimately show ?thesis using IH by auto
next
case other
then show ?thesis
proof cases
case decide
moreover then have "conflicting U = None"
by auto
ultimately show ?thesis using IH cdcl⇩W_merge_restart.fw_r_decide[of U V] by auto
next
case bj
moreover {
assume "skip_or_resolve U V"
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
then have ?thesis
proof -
have "conflicting V ≠ None ∧ conflicting U ≠ None"
using ‹skip_or_resolve U V› by auto
then show ?thesis
by (metis (no_types) IH f1 rtranclp_trans tranclp_into_rtranclp)
qed
}
moreover {
assume "backtrack U V"
then have "conflicting U ≠ None" by auto
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_consistent_inv step.hyps(1) by blast
then have "conflicting V = None"
using ‹backtrack U V› inv by (auto elim: backtrack_levE
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 have ?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
}
ultimately show ?thesis by (auto simp: cdcl⇩W_bj.simps)
qed
next
case rf
moreover then have "conflicting U = None" and "conflicting V = None"
by (auto simp: cdcl⇩W_rf.simps)
ultimately show ?thesis using IH cdcl⇩W_merge_restart.fw_r_rf[of U V] by auto
qed
qed
lemma no_step_cdcl⇩W_no_step_cdcl⇩W_merge_restart: "no_step cdcl⇩W S ⟹ no_step cdcl⇩W_merge_restart S"
by (auto simp: cdcl⇩W.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:
assumes
"conflicting S = None" and
"cdcl⇩W_M_level_inv S" and
"no_step cdcl⇩W_merge_restart S"
shows "no_step cdcl⇩W S"
proof -
{ fix S'
assume "conflict S S'"
then have "cdcl⇩W S S'" using cdcl⇩W.conflict by auto
then have "cdcl⇩W_M_level_inv S'"
using assms(2) cdcl⇩W_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.simps cdcl⇩W_merge_restart.simps cdcl⇩W_o.simps cdcl⇩W_bj.simps
by fastforce
qed
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
apply (induction rule: rtranclp_induct)
apply (fastforce simp: cdcl⇩W_bj.simps cdcl⇩W_rf.simps cdcl⇩W_merge_restart.simps full_def)
apply (fastforce simp: cdcl⇩W_bj.simps cdcl⇩W_rf.simps cdcl⇩W_merge_restart.simps full_def)
done
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_iff_full_cdcl⇩W_merge:
assumes confl: "conflicting S = None" and lev: "cdcl⇩W_M_level_inv S"
shows "full cdcl⇩W S V ⟷ full cdcl⇩W_merge_restart S V"
proof
assume full: "full cdcl⇩W_merge_restart S V"
then have st: "cdcl⇩W⇧*⇧* S V"
using rtranclp_mono[of cdcl⇩W_merge_restart "cdcl⇩W⇧*⇧*"] cdcl⇩W_merge_restart_cdcl⇩W
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.conflict cdcl⇩W_consistent_inv lev rtranclp_cdcl⇩W_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: "no_step cdcl⇩W V"
using n_s n_s_bj by (auto simp: cdcl⇩W.simps cdcl⇩W_o.simps cdcl⇩W_merge_restart.simps)
then show "full cdcl⇩W S V" using st unfolding full_def by auto
next
assume full: "full cdcl⇩W S V"
have "no_step cdcl⇩W_merge_restart V"
using full no_step_cdcl⇩W_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_iff_full_cdcl⇩W_merge:
shows "full cdcl⇩W (init_state N) V ⟷ full cdcl⇩W_merge_restart (init_state N) V"
by (rule conflicting_true_full_cdcl⇩W_iff_full_cdcl⇩W_merge) auto
subsection ‹FW with strategy›
subsubsection ‹The intermediate step›
inductive cdcl⇩W_s' :: "'st ⇒ 'st ⇒ bool" where
conflict': "full1 cdcl⇩W_cp S S' ⟹ cdcl⇩W_s' S S'" |
decide': "decide S S' ⟹ no_step cdcl⇩W_cp S ⟹ full cdcl⇩W_cp S' S'' ⟹ cdcl⇩W_s' S S''" |
bj': "full1 cdcl⇩W_bj S S' ⟹ no_step cdcl⇩W_cp S ⟹ full cdcl⇩W_cp 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' ⟹ full cdcl⇩W_cp S' S'' ⟹ cdcl⇩W_stgy⇧*⇧* S S''"
proof (induction rule: converse_rtranclp_induct)
case base
then show ?case by (metis cdcl⇩W_stgy.conflict' full_unfold rtranclp.simps)
next
case (step T U) note st =this(2) and bj = this(1) and IH = this(3)[OF this(4)]
have "no_step cdcl⇩W_cp T"
using bj by (auto simp add: cdcl⇩W_bj.simps)
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 ‹no_step cdcl⇩W_cp T› cdcl⇩W_o.bj local.bj other' step.prems by (meson r_into_rtranclp)
next
case U' note U' = this(1)
have "no_step cdcl⇩W_cp U"
using U' by (fastforce simp: cdcl⇩W_cp.simps cdcl⇩W_bj.simps)
then have "full cdcl⇩W_cp U U"
by (simp add: full_unfold)
then have "cdcl⇩W_stgy T U"
using ‹no_step cdcl⇩W_cp T› 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"
apply (induction rule: cdcl⇩W_s'.induct)
apply (auto intro: cdcl⇩W_stgy.intros)[]
apply (meson decide other' r_into_rtranclp)
by (metis full1_def rtranclp_cdcl⇩W_bj_full1_cdclp_cdcl⇩W_stgy tranclp_into_rtranclp)
lemma cdcl⇩W_cp_cdcl⇩W_bj_bissimulation:
assumes
"full cdcl⇩W_cp T U" and
"cdcl⇩W_bj⇧*⇧* T T'" and
"cdcl⇩W_all_struct_inv T" and
"no_step cdcl⇩W_bj T'"
shows "full cdcl⇩W_cp T' U
∨ (∃U' U''. full cdcl⇩W_cp T' U'' ∧ full1 cdcl⇩W_bj U U' ∧ full cdcl⇩W_cp U' U'' ∧ cdcl⇩W_s'⇧*⇧* U U'')"
using assms(2,1,3,4)
proof (induction rule: rtranclp_induct)
case base
then show ?case by blast
next
case (step T' T'') note st = this(1) and bj = this(2) and IH = this(3)[OF this(4,5)] and
full = this(4) and inv = this(5)
have "cdcl⇩W⇧*⇧* T T''"
by (metis (no_types, lifting) cdcl⇩W_o.bj local.bj mono_rtranclp[of cdcl⇩W_bj cdcl⇩W T T''] other
st rtranclp.rtrancl_into_rtrancl)
then have inv_T'': "cdcl⇩W_all_struct_inv T''"
using inv rtranclp_cdcl⇩W_all_struct_inv_inv by blast
have "cdcl⇩W_bj⇧+⇧+ T T''"
using local.bj st by auto
have "full1 cdcl⇩W_bj T T''"
by (metis ‹cdcl⇩W_bj⇧+⇧+ T T''› full1_def step.prems(3))
then have "T = U"
proof -
obtain Z where "cdcl⇩W_bj T Z"
by (meson tranclpD ‹cdcl⇩W_bj⇧+⇧+ T T''›)
{ assume "cdcl⇩W_cp⇧+⇧+ T U"
then obtain Z' where "cdcl⇩W_cp T Z'"
by (meson tranclpD)
then have False
using ‹cdcl⇩W_bj T Z› by (fastforce simp: cdcl⇩W_bj.simps cdcl⇩W_cp.simps)
}
then show ?thesis
using full unfolding full_def rtranclp_unfold by blast
qed
obtain U'' where "full cdcl⇩W_cp T'' U''"
using cdcl⇩W_cp_normalized_element_all_inv inv_T'' by blast
moreover then have "cdcl⇩W_stgy⇧*⇧* U U''"
by (metis ‹T = U› ‹cdcl⇩W_bj⇧+⇧+ T T''› rtranclp_cdcl⇩W_bj_full1_cdclp_cdcl⇩W_stgy rtranclp_unfold)
moreover have "cdcl⇩W_s'⇧*⇧* U U''"
proof -
obtain ss :: "'st ⇒ 'st" where
f1: "∀x2. (∃v3. cdcl⇩W_cp x2 v3) = cdcl⇩W_cp x2 (ss x2)"
by moura
have "¬ cdcl⇩W_cp U (ss U)"
by (meson full full_def)
then show ?thesis
using f1 by (metis (no_types) ‹T = U› ‹full1 cdcl⇩W_bj T T''› bj' calculation(1)
r_into_rtranclp)
qed
ultimately show ?case
using ‹full1 cdcl⇩W_bj T T''› ‹full cdcl⇩W_cp T'' U''› unfolding ‹T = U› by blast
qed
lemma cdcl⇩W_cp_cdcl⇩W_bj_bissimulation':
assumes
"full cdcl⇩W_cp T U" and
"cdcl⇩W_bj⇧*⇧* T T'" and
"cdcl⇩W_all_struct_inv T" and
"no_step cdcl⇩W_bj T'"
shows "full cdcl⇩W_cp T' U
∨ (∃U'. full1 cdcl⇩W_bj U U' ∧ (∀U''. full cdcl⇩W_cp U' U'' ⟶ full cdcl⇩W_cp T' U''
∧ cdcl⇩W_s'⇧*⇧* U U''))"
using assms(2,1,3,4)
proof (induction rule: rtranclp_induct)
case base
then show ?case by blast
next
case (step T' T'') note st = this(1) and bj = this(2) and IH = this(3)[OF this(4,5)] and
full = this(4) and inv = this(5)
have "cdcl⇩W⇧*⇧* T T''"
by (metis (no_types, lifting) cdcl⇩W_o.bj local.bj mono_rtranclp[of cdcl⇩W_bj cdcl⇩W T T''] other st
rtranclp.rtrancl_into_rtrancl)
then have inv_T'': "cdcl⇩W_all_struct_inv T''"
using inv rtranclp_cdcl⇩W_all_struct_inv_inv by blast
have "cdcl⇩W_bj⇧+⇧+ T T''"
using local.bj st by auto
have "full1 cdcl⇩W_bj T T''"
by (metis ‹cdcl⇩W_bj⇧+⇧+ T T''› full1_def step.prems(3))
then have "T = U"
proof -
obtain Z where "cdcl⇩W_bj T Z"
by (meson tranclpD ‹cdcl⇩W_bj⇧+⇧+ T T''›)
{ assume "cdcl⇩W_cp⇧+⇧+ T U"
then obtain Z' where "cdcl⇩W_cp T Z'"
by (meson tranclpD)
then have False
using ‹cdcl⇩W_bj T Z› by (fastforce simp: cdcl⇩W_bj.simps cdcl⇩W_cp.simps)
}
then show ?thesis
using full unfolding full_def rtranclp_unfold by blast
qed
{ fix U''
assume "full cdcl⇩W_cp T'' U''"
moreover then have "cdcl⇩W_stgy⇧*⇧* U U''"
by (metis ‹T = U› ‹cdcl⇩W_bj⇧+⇧+ T T''› rtranclp_cdcl⇩W_bj_full1_cdclp_cdcl⇩W_stgy rtranclp_unfold)
moreover have "cdcl⇩W_s'⇧*⇧* U U''"
proof -
obtain ss :: "'st ⇒ 'st" where
f1: "∀x2. (∃v3. cdcl⇩W_cp x2 v3) = cdcl⇩W_cp x2 (ss x2)"
by moura
have "¬ cdcl⇩W_cp U (ss U)"
by (meson assms(1) full_def)
then show ?thesis
using f1 by (metis (no_types) ‹T = U› ‹full1 cdcl⇩W_bj T T''› bj' calculation(1)
r_into_rtranclp)
qed
ultimately have "full1 cdcl⇩W_bj U T''" and " cdcl⇩W_s'⇧*⇧* T'' U''"
using ‹full1 cdcl⇩W_bj T T''› ‹full cdcl⇩W_cp T'' U''› unfolding ‹T = U›
apply blast
by (metis ‹full cdcl⇩W_cp T'' U''› cdcl⇩W_s'.simps full_unfold rtranclp.simps)
}
then show ?case
using ‹full1 cdcl⇩W_bj T T''› full bj' unfolding ‹T = U› full_def by (metis r_into_rtranclp)
qed
lemma cdcl⇩W_stgy_cdcl⇩W_s'_connected:
assumes "cdcl⇩W_stgy S U" and "cdcl⇩W_all_struct_inv S"
shows "cdcl⇩W_s' S U
∨ (∃U'. full1 cdcl⇩W_bj U U' ∧ (∀U''. full cdcl⇩W_cp U' U'' ⟶ cdcl⇩W_s' S U'' ))"
using assms
proof (induction rule: cdcl⇩W_stgy.induct)
case (conflict' T)
then have "cdcl⇩W_s' S T"
using cdcl⇩W_s'.conflict' by blast
then show ?case
by blast
next
case (other' T U) note o = this(1) and n_s = this(2) and full = this(3) and inv = this(4)
show ?case
using o
proof cases
case decide
then show ?thesis using cdcl⇩W_s'.simps full n_s by blast
next
case bj
have inv_T: "cdcl⇩W_all_struct_inv T"
using cdcl⇩W_all_struct_inv_inv o other other'.prems by blast
consider
(cp) "full cdcl⇩W_cp T U" and "no_step cdcl⇩W_bj T"
| (fbj) T' where "full1 cdcl⇩W_bj T T'"
apply (cases "no_step cdcl⇩W_bj T")
using full apply blast
using cdcl⇩W_bj_exists_normal_form[of T] inv_T unfolding cdcl⇩W_all_struct_inv_def
by (metis full_unfold)
then show ?thesis
proof cases
case cp
then show ?thesis
proof -
obtain ss :: "'st ⇒ 'st" where
f1: "∀s sa sb. (¬ full1 cdcl⇩W_bj s sa ∨ cdcl⇩W_cp s (ss s) ∨ ¬ full cdcl⇩W_cp sa sb)
∨ cdcl⇩W_s' s sb"
using bj' by moura
have "full1 cdcl⇩W_bj S T"
by (simp add: cp(2) full1_def local.bj tranclp.r_into_trancl)
then show ?thesis
using f1 full n_s by blast
qed
next
case (fbj U')
then have "full1 cdcl⇩W_bj S U'"
using bj unfolding full1_def by auto
moreover have "no_step cdcl⇩W_cp S"
using n_s by blast
moreover have "T = U"
using full fbj unfolding full1_def full_def rtranclp_unfold
by (force dest!: tranclpD simp:cdcl⇩W_bj.simps)
ultimately show ?thesis using cdcl⇩W_s'.bj'[of S U'] using fbj by blast
qed
qed
qed
lemma cdcl⇩W_stgy_cdcl⇩W_s'_connected':
assumes "cdcl⇩W_stgy S U" and "cdcl⇩W_all_struct_inv S"
shows "cdcl⇩W_s' S U
∨ (∃U' U''. cdcl⇩W_s' S U'' ∧ full1 cdcl⇩W_bj U U' ∧ full cdcl⇩W_cp U' U'')"
using assms
proof (induction rule: cdcl⇩W_stgy.induct)
case (conflict' T)
then have "cdcl⇩W_s' S T"
using cdcl⇩W_s'.conflict' by blast
then show ?case
by blast
next
case (other' T U) note o = this(1) and n_s = this(2) and full = this(3) and inv = this(4)
show ?case
using o
proof cases
case decide
then show ?thesis using cdcl⇩W_s'.simps full n_s by blast
next
case bj
have "cdcl⇩W_all_struct_inv T"
using cdcl⇩W_all_struct_inv_inv o other other'.prems by blast
then obtain T' where T': "full cdcl⇩W_bj T T'"
using cdcl⇩W_bj_exists_normal_form unfolding full_def cdcl⇩W_all_struct_inv_def by metis
then have "full cdcl⇩W_bj S T'"
proof -
have f1: "cdcl⇩W_bj⇧*⇧* T T' ∧ no_step cdcl⇩W_bj T'"
by (metis (no_types) T' full_def)
then have "cdcl⇩W_bj⇧*⇧* S T'"
by (meson converse_rtranclp_into_rtranclp local.bj)
then show ?thesis
using f1 by (simp add: full_def)
qed
have "cdcl⇩W_bj⇧*⇧* T T'"
using T' unfolding full_def by simp
have "cdcl⇩W_all_struct_inv T"
using cdcl⇩W_all_struct_inv_inv o other other'.prems by blast
then consider
(T'U) "full cdcl⇩W_cp T' U"
| (U) U' U'' where
"full cdcl⇩W_cp T' U''" and
"full1 cdcl⇩W_bj U U'" and
"full cdcl⇩W_cp U' U''" and
"cdcl⇩W_s'⇧*⇧* U U''"
using cdcl⇩W_cp_cdcl⇩W_bj_bissimulation[OF full ‹cdcl⇩W_bj⇧*⇧* T T'›] T' unfolding full_def
by blast
then show ?thesis by (metis T' cdcl⇩W_s'.simps full_fullI local.bj n_s)
qed
qed
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 cdcl⇩W_stgy_cdcl⇩W_s'_connected[OF assms(1,2)] assms(3)
by (metis (no_types, lifting) full1_def tranclpD)
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 f2: "cdcl⇩W_s' T V"
using cdcl⇩W_s'.conflict' by blast
obtain ss :: 'st where
f3: "S = T ∨ cdcl⇩W_stgy⇧*⇧* S ss ∧ cdcl⇩W_stgy ss T"
by (metis (full_types) rtranclp.simps st)
obtain ssa :: 'st where
"cdcl⇩W_cp T ssa"
using conflict' by (metis (no_types) full1_def tranclpD)
then have "S = T"
using f3 by (metis (no_types) cdcl⇩W_stgy.simps full_def full1_def)
then show ?thesis
using f2 by blast
next
case (other' U) note o = this(1) and n_s = this(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
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 U"
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)
have "no_step cdcl⇩W_cp S'"
using bj_T by (fastforce simp: cdcl⇩W_cp.simps cdcl⇩W_bj.simps dest!: tranclpD)
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 U"
using backtrack_is_full1_cdcl⇩W_bj backtrack by blast
then have "full1 cdcl⇩W_bj S' U"
using bj_T unfolding full1_def by fastforce
ultimately have "cdcl⇩W_s' S' V" using full by (simp add: bj')
then show ?thesis using S_S' by auto
qed
next
case skip
then have [simp]: "U = V"
using full converse_rtranclpE unfolding full_def by fastforce
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'
have "cdcl⇩W_bj⇧+⇧+ T V"
using skip by force
moreover have "conflicting V ≠ None"
using skip by auto
ultimately show ?thesis using s' by auto
next
case (bj S') note S_S' = this(1) and bj_T = this(2)
have "cdcl⇩W_bj⇧+⇧+ S' V"
using skip bj_T by (metis ‹U = V› cdcl⇩W_bj.skip tranclp.simps)
moreover have "conflicting V ≠ None"
using skip by auto
ultimately show ?thesis using S_S' by auto
qed
next
case resolve
then have [simp]: "U = V"
using full converse_rtranclpE unfolding full_def by fastforce
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'
have "cdcl⇩W_bj⇧+⇧+ T V"
using resolve by force
moreover have "conflicting V ≠ None"
using resolve by auto
ultimately show ?thesis using s' by auto
next
case (bj S') note S_S' = this(1) and bj_T = this(2)
have "cdcl⇩W_bj⇧+⇧+ S' V"
using resolve bj_T by (metis ‹U = V› cdcl⇩W_bj.resolve tranclp.simps)
moreover have "conflicting V ≠ None"
using resolve by auto
ultimately show ?thesis using S_S' by auto
qed
qed
qed
qed
lemma n_step_cdcl⇩W_stgy_iff_no_step_cdcl⇩W_cl_cdcl⇩W_o:
assumes inv: "cdcl⇩W_all_struct_inv S"
shows "no_step cdcl⇩W_s' S ⟷ no_step cdcl⇩W_cp S ∧ no_step cdcl⇩W_o S" (is "?S' S ⟷ ?C S ∧ ?O S")
proof
assume "?C S ∧ ?O S"
then show "?S' S"
by (auto simp: cdcl⇩W_s'.simps full1_def tranclp_unfold_begin)
next
assume n_s: "?S' S"
have "?C S"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain S' where "cdcl⇩W_cp S S'"
by auto
then obtain T where "full1 cdcl⇩W_cp S T"
using cdcl⇩W_cp_normalized_element_all_inv inv by (metis (no_types, lifting) full_unfold)
then show False using n_s cdcl⇩W_s'.conflict' by blast
qed
moreover have "?O S"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain S' where "cdcl⇩W_o S S'"
by auto
then obtain T where "full1 cdcl⇩W_cp S' T"
using cdcl⇩W_cp_normalized_element_all_inv inv
by (meson cdcl⇩W_all_struct_inv_def n_s
cdcl⇩W_stgy_cdcl⇩W_s'_connected' cdcl⇩W_then_exists_cdcl⇩W_stgy_step )
then show False using n_s by (meson ‹cdcl⇩W_o S S'› cdcl⇩W_all_struct_inv_def
cdcl⇩W_stgy_cdcl⇩W_s'_connected' cdcl⇩W_then_exists_cdcl⇩W_stgy_step inv)
qed
ultimately show "?C S ∧ ?O S" by auto
qed
lemma cdcl⇩W_s'_tranclp_cdcl⇩W:
"cdcl⇩W_s' S S' ⟹ cdcl⇩W⇧+⇧+ S S'"
proof (induct rule: cdcl⇩W_s'.induct)
case conflict'
then show ?case
by (simp add: full1_def tranclp_cdcl⇩W_cp_tranclp_cdcl⇩W)
next
case decide'
then show ?case
using cdcl⇩W_stgy.simps cdcl⇩W_stgy_tranclp_cdcl⇩W by (meson cdcl⇩W_o.simps)
next
case (bj' Sa S'a S'') note a2 = this(1) and a1 = this(2) and n_s = this(3)
obtain ss :: "'st ⇒ 'st ⇒ ('st ⇒ 'st ⇒ bool) ⇒ 'st" where
"∀x0 x1 x2. (∃v3. x2 x1 v3 ∧ x2⇧*⇧* v3 x0) = (x2 x1 (ss x0 x1 x2) ∧ x2⇧*⇧* (ss x0 x1 x2) x0)"
by moura
then have f3: "∀p s sa. ¬ p⇧+⇧+ s sa ∨ p s (ss sa s p) ∧ p⇧*⇧* (ss sa s p) sa"
by (metis (full_types) tranclpD)
have "cdcl⇩W_bj⇧+⇧+ Sa S'a ∧ no_step cdcl⇩W_bj S'a"
using a2 by (simp add: full1_def)
then have "cdcl⇩W_bj Sa (ss S'a Sa cdcl⇩W_bj) ∧ cdcl⇩W_bj⇧*⇧* (ss S'a Sa cdcl⇩W_bj) S'a"
using f3 by auto
then show "cdcl⇩W⇧+⇧+ Sa S''"
using a1 n_s by (meson bj other rtranclp_cdcl⇩W_bj_full1_cdclp_cdcl⇩W_stgy
rtranclp_cdcl⇩W_stgy_rtranclp_cdcl⇩W rtranclp_into_tranclp2)
qed
lemma tranclp_cdcl⇩W_s'_tranclp_cdcl⇩W:
"cdcl⇩W_s'⇧+⇧+ S S' ⟹ cdcl⇩W⇧+⇧+ S S'"
apply (induct rule: tranclp.induct)
using cdcl⇩W_s'_tranclp_cdcl⇩W apply blast
by (meson cdcl⇩W_s'_tranclp_cdcl⇩W tranclp_trans)
lemma rtranclp_cdcl⇩W_s'_rtranclp_cdcl⇩W:
"cdcl⇩W_s'⇧*⇧* S S' ⟹ cdcl⇩W⇧*⇧* S S'"
using rtranclp_unfold[of cdcl⇩W_s' S S'] tranclp_cdcl⇩W_s'_tranclp_cdcl⇩W[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⇧*⇧* S T"
using rtranclp_cdcl⇩W_s'_rtranclp_cdcl⇩W[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' cdcl⇩W_stgy_cdcl⇩W_s'_connected' 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)
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
by (metis ‹full cdcl⇩W_stgy S T› inv_T cdcl⇩W_all_struct_inv_def cdcl⇩W_s'.simps
cdcl⇩W_stgy.conflict' cdcl⇩W_then_exists_cdcl⇩W_stgy_step full_def
n_step_cdcl⇩W_stgy_iff_no_step_cdcl⇩W_cl_cdcl⇩W_o)
next
case (st S')
have "full cdcl⇩W_cp T T"
using option_full_cdcl⇩W_cp st(3) by blast
moreover
have n_s: "no_step cdcl⇩W_bj T"
by (metis ‹full cdcl⇩W_stgy S T› bj inv_T cdcl⇩W_all_struct_inv_def
cdcl⇩W_then_exists_cdcl⇩W_stgy_step full_def)
then have "full1 cdcl⇩W_bj S' T"
using st(2) unfolding full1_def by blast
moreover have "no_step cdcl⇩W_cp S'"
using st(2) by (fastforce dest!: tranclpD simp: cdcl⇩W_cp.simps cdcl⇩W_bj.simps)
ultimately have "cdcl⇩W_s' S' T"
using cdcl⇩W_s'.bj'[of S' T 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 by (metis ‹full cdcl⇩W_cp T T› ‹full cdcl⇩W_stgy S T› cdcl⇩W_all_struct_inv_def
cdcl⇩W_then_exists_cdcl⇩W_stgy_step full_def n_step_cdcl⇩W_stgy_iff_no_step_cdcl⇩W_cl_cdcl⇩W_o)
ultimately show ?thesis
unfolding full_def by blast
qed
qed
lemma conflict_step_cdcl⇩W_stgy_step:
assumes
"conflict S T"
"cdcl⇩W_all_struct_inv S"
shows "∃T. cdcl⇩W_stgy S T"
proof -
obtain U where "full cdcl⇩W_cp S U"
using cdcl⇩W_cp_normalized_element_all_inv assms by blast
then have "full1 cdcl⇩W_cp S U"
by (metis cdcl⇩W_cp.conflict' assms(1) full_unfold)
then show ?thesis using cdcl⇩W_stgy.conflict' by blast
qed
lemma decide_step_cdcl⇩W_stgy_step:
assumes
"decide S T"
"cdcl⇩W_all_struct_inv S"
shows "∃T. cdcl⇩W_stgy S T"
proof -
obtain U where "full cdcl⇩W_cp T U"
using cdcl⇩W_cp_normalized_element_all_inv by (meson assms(1) assms(2) cdcl⇩W_all_struct_inv_inv
cdcl⇩W_cp_normalized_element_all_inv decide other)
then show ?thesis
by (metis assms cdcl⇩W_cp_normalized_element_all_inv cdcl⇩W_stgy.conflict' decide full_unfold
other')
qed
lemma rtranclp_cdcl⇩W_cp_conflicting_Some:
"cdcl⇩W_cp⇧*⇧* S T ⟹ conflicting S = Some D ⟹ S = T"
using rtranclpD tranclpD by fastforce
inductive cdcl⇩W_merge_cp :: "'st ⇒ 'st ⇒ bool" where
conflict'[intro]: "conflict S T ⟹ full cdcl⇩W_bj T U ⟹ cdcl⇩W_merge_cp S U" |
propagate'[intro]: "propagate⇧+⇧+ S S' ⟹ cdcl⇩W_merge_cp S S'"
lemma cdcl⇩W_merge_restart_cases[consumes 1, case_names conflict propagate]:
assumes
"cdcl⇩W_merge_cp S U" and
"⋀T. conflict S T ⟹ full cdcl⇩W_bj T U ⟹ P" and
"propagate⇧+⇧+ S U ⟹ P"
shows "P"
using assms unfolding cdcl⇩W_merge_cp.simps by auto
lemma cdcl⇩W_merge_cp_tranclp_cdcl⇩W_merge:
"cdcl⇩W_merge_cp S T ⟹ cdcl⇩W_merge⇧+⇧+ S T"
apply (induction rule: cdcl⇩W_merge_cp.induct)
using cdcl⇩W_merge.simps apply auto[1]
using tranclp_mono[of propagate cdcl⇩W_merge] fw_propagate by blast
lemma rtranclp_cdcl⇩W_merge_cp_rtranclp_cdcl⇩W:
"cdcl⇩W_merge_cp⇧*⇧* S T ⟹ cdcl⇩W⇧*⇧* S T"
apply (induction rule: rtranclp_induct)
apply simp
unfolding cdcl⇩W_merge_cp.simps by (meson cdcl⇩W_merge_restart_cdcl⇩W fw_r_conflict
rtranclp_propagate_is_rtranclp_cdcl⇩W rtranclp_trans tranclp_into_rtranclp)
lemma full1_cdcl⇩W_bj_no_step_cdcl⇩W_bj:
"full1 cdcl⇩W_bj S T ⟹ no_step cdcl⇩W_cp S"
by (metis rtranclp_unfold cdcl⇩W_cp_conflicting_not_empty option.exhaust full1_def
rtranclp_cdcl⇩W_merge_restart_no_step_cdcl⇩W_bj tranclpD)
inductive cdcl⇩W_s'_without_decide where
conflict'_without_decide[intro]: "full1 cdcl⇩W_cp S S' ⟹ cdcl⇩W_s'_without_decide S S'" |
bj'_without_decide[intro]: "full1 cdcl⇩W_bj S S' ⟹ no_step cdcl⇩W_cp S ⟹ full cdcl⇩W_cp S' S''
⟹ cdcl⇩W_s'_without_decide S S''"
lemma rtranclp_cdcl⇩W_s'_without_decide_rtranclp_cdcl⇩W:
"cdcl⇩W_s'_without_decide⇧*⇧* S T ⟹ cdcl⇩W⇧*⇧* S T"
apply (induction rule: rtranclp_induct)
apply simp
by (meson cdcl⇩W_s'.simps cdcl⇩W_s'_tranclp_cdcl⇩W cdcl⇩W_s'_without_decide.simps
rtranclp_tranclp_tranclp tranclp_into_rtranclp)
lemma rtranclp_cdcl⇩W_s'_without_decide_rtranclp_cdcl⇩W_s':
"cdcl⇩W_s'_without_decide⇧*⇧* S T ⟹ cdcl⇩W_s'⇧*⇧* S T"
proof (induction rule: rtranclp_induct)
case base
then show ?case by simp
next
case (step y z) note a2 = this(2) and a1 = this(3)
have "cdcl⇩W_s' y z"
using a2 by (metis (no_types) bj' cdcl⇩W_s'.conflict' cdcl⇩W_s'_without_decide.cases)
then show "cdcl⇩W_s'⇧*⇧* S z"
using a1 by (meson r_into_rtranclp rtranclp_trans)
qed
lemma rtranclp_cdcl⇩W_merge_cp_is_rtranclp_cdcl⇩W_s'_without_decide:
assumes
"cdcl⇩W_merge_cp⇧*⇧* S V"
"conflicting S = None"
shows
"(cdcl⇩W_s'_without_decide⇧*⇧* S V)
∨ (∃T. cdcl⇩W_s'_without_decide⇧*⇧* S T ∧ propagate⇧+⇧+ T V)
∨ (∃T U. cdcl⇩W_s'_without_decide⇧*⇧* S T ∧ full1 cdcl⇩W_bj T U ∧ propagate⇧*⇧* U V)"
using assms
proof (induction rule: rtranclp_induct)
case base
then show ?case by simp
next
case (step U V) note st = this(1) and cp = this(2) and IH = this(3)[OF this(4)]
from cp show ?case
proof (cases rule: cdcl⇩W_merge_restart_cases)
case propagate
then show ?thesis using IH by (meson rtranclp_tranclp_tranclp tranclp_into_rtranclp)
next
case (conflict U') note confl = this(1) and bj = this(2)
have full1_U_U': "full1 cdcl⇩W_cp U U'"
by (simp add: conflict_is_full1_cdcl⇩W_cp local.conflict(1))
consider
(s') "cdcl⇩W_s'_without_decide⇧*⇧* S U"
| (propa) T' where "cdcl⇩W_s'_without_decide⇧*⇧* S T'" and "propagate⇧+⇧+ T' U"
| (bj_prop) T' T'' where
"cdcl⇩W_s'_without_decide⇧*⇧* S T' " and
"full1 cdcl⇩W_bj T' T''" and
"propagate⇧*⇧* T'' U"
using IH by blast
then show ?thesis
proof cases
case s'
have "cdcl⇩W_s'_without_decide U U'"
using full1_U_U' conflict'_without_decide by blast
then have "cdcl⇩W_s'_without_decide⇧*⇧* S U'"
using ‹cdcl⇩W_s'_without_decide⇧*⇧* S U› by auto
moreover have "U' = V ∨ full1 cdcl⇩W_bj U' V"
using bj by (meson full_unfold)
ultimately show ?thesis by blast
next
case propa note s' = this(1) and T'_U = this(2)
have "full1 cdcl⇩W_cp T' U'"
using rtranclp_mono[of propagate cdcl⇩W_cp] T'_U cdcl⇩W_cp.propagate' full1_U_U'
rtranclp_full1I[of cdcl⇩W_cp T'] by (metis (full_types) predicate2D predicate2I
tranclp_into_rtranclp)
have "cdcl⇩W_s'_without_decide⇧*⇧* S U'"
using ‹full1 cdcl⇩W_cp T' U'› conflict'_without_decide s' by force
have "full1 cdcl⇩W_bj U' V ∨ V = U'"
by (metis (lifting) full_unfold local.bj)
then show ?thesis
using ‹cdcl⇩W_s'_without_decide⇧*⇧* S U'› by blast
next
case bj_prop note s' = this(1) and bj_T' = this(2) and T''_U = this(3)
have "no_step cdcl⇩W_cp T'"
using bj_T' full1_cdcl⇩W_bj_no_step_cdcl⇩W_bj by blast
moreover have "full1 cdcl⇩W_cp T'' U'"
using rtranclp_mono[of propagate cdcl⇩W_cp] T''_U cdcl⇩W_cp.propagate' full1_U_U'
rtranclp_full1I[of cdcl⇩W_cp T''] by blast
ultimately have "cdcl⇩W_s'_without_decide T' U'"
using bj'_without_decide[of T' T'' U'] bj_T' by (simp add: full_unfold)
then have "cdcl⇩W_s'_without_decide⇧*⇧* S U'"
using s' rtranclp.intros(2)[of _ S T' U'] by blast
then show ?thesis
by (metis full_unfold local.bj rtranclp.rtrancl_refl)
qed
qed
qed
lemma rtranclp_cdcl⇩W_s'_without_decide_is_rtranclp_cdcl⇩W_merge_cp:
assumes
"cdcl⇩W_s'_without_decide⇧*⇧* S V" and
confl: "conflicting S = None"
shows
"(cdcl⇩W_merge_cp⇧*⇧* S V ∧ conflicting V = None)
∨ (cdcl⇩W_merge_cp⇧*⇧* S V ∧ conflicting V ≠ None ∧ no_step cdcl⇩W_cp V ∧ no_step cdcl⇩W_bj V)
∨ (∃T. cdcl⇩W_merge_cp⇧*⇧* S T ∧ conflict T V)"
using assms(1)
proof (induction)
case base
then show ?case using confl by auto
next
case (step U V) note st = this(1) and s = this(2) and IH = this(3)
from s show ?case
proof (cases rule: cdcl⇩W_s'_without_decide.cases)
case conflict'_without_decide
then have rt: "cdcl⇩W_cp⇧+⇧+ U V" unfolding full1_def by fast
then have "conflicting U = None"
using tranclp_cdcl⇩W_cp_propagate_with_conflict_or_not[of U V]
conflict by (auto dest!: tranclpD simp: rtranclp_unfold)
then have "cdcl⇩W_merge_cp⇧*⇧* S U" using IH by auto
consider
(propa) "propagate⇧+⇧+ U V"
| (confl') "conflict U V"
| (propa_confl') U' where "propagate⇧+⇧+ U U'" "conflict U' V"
using tranclp_cdcl⇩W_cp_propagate_with_conflict_or_not[OF rt] unfolding rtranclp_unfold
by fastforce
then show ?thesis
proof cases
case propa
then have "cdcl⇩W_merge_cp U V"
by auto
moreover have "conflicting V = None"
using propa unfolding tranclp_unfold_end by auto
ultimately show ?thesis using ‹cdcl⇩W_merge_cp⇧*⇧* S U› by force
next
case confl'
then show ?thesis using ‹cdcl⇩W_merge_cp⇧*⇧* S U› by auto
next
case propa_confl' note propa = this(1) and confl' = this(2)
then have "cdcl⇩W_merge_cp U U'" by auto
then have "cdcl⇩W_merge_cp⇧*⇧* S U'" using ‹cdcl⇩W_merge_cp⇧*⇧* S U› by auto
then show ?thesis using ‹cdcl⇩W_merge_cp⇧*⇧* S U› confl' by auto
qed
next
case (bj'_without_decide U') note full_bj = this(1) and cp = this(3)
then have "conflicting U ≠ None"
using full_bj unfolding full1_def by (fastforce dest!: tranclpD simp: cdcl⇩W_bj.simps)
with IH obtain T where
S_T: "cdcl⇩W_merge_cp⇧*⇧* S T" and T_U: "conflict T U"
using full_bj unfolding full1_def by (blast dest: tranclpD)
then have "cdcl⇩W_merge_cp T U'"
using cdcl⇩W_merge_cp.conflict'[of T U U'] full_bj by (simp add: full_unfold)
then have S_U': "cdcl⇩W_merge_cp⇧*⇧* S U'" using S_T by auto
consider
(n_s) "U' = V"
| (propa) "propagate⇧+⇧+ U' V"
| (confl') "conflict U' V"
| (propa_confl') U'' where "propagate⇧+⇧+ U' U''" "conflict U'' V"
using tranclp_cdcl⇩W_cp_propagate_with_conflict_or_not cp
unfolding rtranclp_unfold full_def by metis
then show ?thesis
proof cases
case propa
then have "cdcl⇩W_merge_cp U' V" by auto
moreover have "conflicting V = None"
using propa unfolding tranclp_unfold_end by auto
ultimately show ?thesis using S_U' by force
next
case confl'
then show ?thesis using S_U' by auto
next
case propa_confl' note propa = this(1) and confl = this(2)
have "cdcl⇩W_merge_cp U' U''" using propa by auto
then show ?thesis using S_U' confl by (meson rtranclp.rtrancl_into_rtrancl)
next
case n_s
then show ?thesis
using S_U' apply (cases "conflicting V = None")
using full_bj apply simp
by (metis cp full_def full_unfold full_bj)
qed
qed
qed
lemma no_step_cdcl⇩W_s'_no_ste_cdcl⇩W_merge_cp:
assumes
"cdcl⇩W_all_struct_inv S"
"conflicting S = None"
"no_step cdcl⇩W_s' S"
shows "no_step cdcl⇩W_merge_cp S"
using assms apply (auto simp: cdcl⇩W_s'.simps cdcl⇩W_merge_cp.simps)
using conflict_is_full1_cdcl⇩W_cp apply blast
using cdcl⇩W_cp_normalized_element_all_inv cdcl⇩W_cp.propagate' by (metis cdcl⇩W_cp.propagate'
full_unfold tranclpD)
text ‹The @{term "no_step decide S"} is needed, since @{term "cdcl⇩W_merge_cp"} is
@{term "cdcl⇩W_s'"} without @{term decide}.›
lemma conflicting_true_no_step_cdcl⇩W_merge_cp_no_step_s'_without_decide:
assumes
confl: "conflicting S = None" and
inv: "cdcl⇩W_M_level_inv S" and
n_s: "no_step cdcl⇩W_merge_cp S"
shows "no_step cdcl⇩W_s'_without_decide S"
proof (rule ccontr)
assume "¬ no_step cdcl⇩W_s'_without_decide S"
then obtain T where
cdcl⇩W: "cdcl⇩W_s'_without_decide S T"
by auto
then have inv_T: "cdcl⇩W_M_level_inv T"
using rtranclp_cdcl⇩W_s'_without_decide_rtranclp_cdcl⇩W[of S T]
rtranclp_cdcl⇩W_consistent_inv inv by blast
from cdcl⇩W show False
proof cases
case conflict'_without_decide
have "no_step propagate S"
using n_s by blast
then have "conflict S T"
using local.conflict' tranclp_cdcl⇩W_cp_propagate_with_conflict_or_not[of S T]
unfolding full1_def by (metis full1_def local.conflict'_without_decide rtranclp_unfold
tranclp_unfold_begin)
moreover
then obtain T' where "full cdcl⇩W_bj T T'"
using cdcl⇩W_bj_exists_normal_form inv_T by blast
ultimately show False using cdcl⇩W_merge_cp.conflict' n_s by meson
next
case (bj'_without_decide S')
then show ?thesis
using confl unfolding full1_def by (fastforce simp: cdcl⇩W_bj.simps dest: tranclpD)
qed
qed
lemma conflicting_true_no_step_s'_without_decide_no_step_cdcl⇩W_merge_cp:
assumes
inv: "cdcl⇩W_all_struct_inv S" and
n_s: "no_step cdcl⇩W_s'_without_decide S"
shows "no_step cdcl⇩W_merge_cp S"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain T where "cdcl⇩W_merge_cp S T"
by auto
then show False
proof cases
case (conflict' S')
then show False using n_s conflict'_without_decide conflict_is_full1_cdcl⇩W_cp by blast
next
case propagate'
moreover
have "cdcl⇩W_all_struct_inv T"
using inv by (meson local.propagate' rtranclp_cdcl⇩W_all_struct_inv_inv
rtranclp_propagate_is_rtranclp_cdcl⇩W tranclp_into_rtranclp)
then obtain U where "full cdcl⇩W_cp T U"
using cdcl⇩W_cp_normalized_element_all_inv by auto
ultimately have "full1 cdcl⇩W_cp S U"
using tranclp_full_full1I[of cdcl⇩W_cp S T U] cdcl⇩W_cp.propagate'
tranclp_mono[of propagate cdcl⇩W_cp] by blast
then show False using conflict'_without_decide n_s by blast
qed
qed
lemma no_step_cdcl⇩W_merge_cp_no_step_cdcl⇩W_cp:
"no_step cdcl⇩W_merge_cp S ⟹ cdcl⇩W_M_level_inv S ⟹ no_step cdcl⇩W_cp S"
using cdcl⇩W_bj_exists_normal_form cdcl⇩W_consistent_inv[OF cdcl⇩W.conflict, of S]
by (metis cdcl⇩W_cp.cases cdcl⇩W_merge_cp.simps tranclp.intros(1))
lemma conflicting_not_true_rtranclp_cdcl⇩W_merge_cp_no_step_cdcl⇩W_bj:
assumes
"conflicting S = None" and
"cdcl⇩W_merge_cp⇧*⇧* S T"
shows "no_step cdcl⇩W_bj T"
using assms(2,1) by (induction)
(fastforce simp: cdcl⇩W_merge_cp.simps full_def tranclp_unfold_end cdcl⇩W_bj.simps)+
lemma conflicting_true_full_cdcl⇩W_merge_cp_iff_full_cdcl⇩W_s'_without_decode:
assumes
confl: "conflicting S = None" and
inv: "cdcl⇩W_all_struct_inv S"
shows
"full cdcl⇩W_merge_cp S V ⟷ full cdcl⇩W_s'_without_decide S V" (is "?fw ⟷ ?s'")
proof
assume ?fw
then have st: "cdcl⇩W_merge_cp⇧*⇧* S V" and n_s: "no_step cdcl⇩W_merge_cp V"
unfolding full_def by blast+
have inv_V: "cdcl⇩W_all_struct_inv V"
using rtranclp_cdcl⇩W_merge_cp_rtranclp_cdcl⇩W[of S V] ‹?fw› unfolding full_def
by (simp add: inv rtranclp_cdcl⇩W_all_struct_inv_inv)
consider
(s') "cdcl⇩W_s'_without_decide⇧*⇧* S V"
| (propa) T where "cdcl⇩W_s'_without_decide⇧*⇧* S T" and "propagate⇧+⇧+ T V"
| (bj) T U where "cdcl⇩W_s'_without_decide⇧*⇧* S T" and "full1 cdcl⇩W_bj T U" and "propagate⇧*⇧* U V"
using rtranclp_cdcl⇩W_merge_cp_is_rtranclp_cdcl⇩W_s'_without_decide confl st n_s by metis
then have "cdcl⇩W_s'_without_decide⇧*⇧* S V"
proof cases
case s'
then show ?thesis .
next
case propa note s' = this(1) and propa = this(2)
have "no_step cdcl⇩W_cp V"
using no_step_cdcl⇩W_merge_cp_no_step_cdcl⇩W_cp n_s inv_V
unfolding cdcl⇩W_all_struct_inv_def by blast
then have "full1 cdcl⇩W_cp T V"
using propa tranclp_mono[of propagate cdcl⇩W_cp] "cdcl⇩W_cp.propagate'" unfolding full1_def
by blast
then have "cdcl⇩W_s'_without_decide T V"
using conflict'_without_decide by blast
then show ?thesis using s' by auto
next
case bj note s' = this(1) and bj = this(2) and propa = this(3)
have "no_step cdcl⇩W_cp V"
using no_step_cdcl⇩W_merge_cp_no_step_cdcl⇩W_cp n_s inv_V
unfolding cdcl⇩W_all_struct_inv_def by blast
then have "full cdcl⇩W_cp U V"
using propa rtranclp_mono[of propagate cdcl⇩W_cp] cdcl⇩W_cp.propagate' unfolding full_def
by blast
moreover have "no_step cdcl⇩W_cp T"
using bj unfolding full1_def by (fastforce dest!: tranclpD simp:cdcl⇩W_bj.simps)
ultimately have "cdcl⇩W_s'_without_decide T V"
using bj'_without_decide[of T U V] bj by blast
then show ?thesis using s' by auto
qed
moreover have "no_step cdcl⇩W_s'_without_decide V"
proof (cases "conflicting V = None")
case False
{ fix ss :: 'st
have ff1: "∀s sa. ¬ cdcl⇩W_s' s sa ∨ full1 cdcl⇩W_cp s sa
∨ (∃sb. decide s sb ∧ no_step cdcl⇩W_cp s ∧ full cdcl⇩W_cp sb sa)
∨ (∃sb. full1 cdcl⇩W_bj s sb ∧ no_step cdcl⇩W_cp s ∧ full cdcl⇩W_cp sb sa)"
by (metis cdcl⇩W_s'.cases)
have ff2: "(∀p s sa. ¬ full1 p (s::'st) sa ∨ p⇧+⇧+ s sa ∧ no_step p sa)
∧ (∀p s sa. (¬ p⇧+⇧+ (s::'st) sa ∨ (∃s. p sa s)) ∨ full1 p s sa)"
by (meson full1_def)
obtain ssa :: "('st ⇒ 'st ⇒ bool) ⇒ 'st ⇒ 'st ⇒ 'st" where
ff3: "∀p s sa. ¬ p⇧+⇧+ s sa ∨ p s (ssa p s sa) ∧ p⇧*⇧* (ssa p s sa) sa"
by (metis (no_types) tranclpD)
then have a3: "¬ cdcl⇩W_cp⇧+⇧+ V ss"
using False by (metis option_full_cdcl⇩W_cp full_def)
have "⋀s. ¬ cdcl⇩W_bj⇧+⇧+ V s"
using ff3 False by (metis confl st
conflicting_not_true_rtranclp_cdcl⇩W_merge_cp_no_step_cdcl⇩W_bj)
then have "¬ cdcl⇩W_s'_without_decide V ss"
using ff1 a3 ff2 by (metis cdcl⇩W_s'_without_decide.cases)
}
then show ?thesis
by fastforce
next
case True
then show ?thesis
using conflicting_true_no_step_cdcl⇩W_merge_cp_no_step_s'_without_decide n_s inv_V
unfolding cdcl⇩W_all_struct_inv_def by blast
qed
ultimately show ?s' unfolding full_def by blast
next
assume s': ?s'
then have st: "cdcl⇩W_s'_without_decide⇧*⇧* S V" and n_s: "no_step cdcl⇩W_s'_without_decide V"
unfolding full_def by auto
then have "cdcl⇩W⇧*⇧* S V"
using rtranclp_cdcl⇩W_s'_without_decide_rtranclp_cdcl⇩W st by blast
then have inv_V: "cdcl⇩W_all_struct_inv V" using inv rtranclp_cdcl⇩W_all_struct_inv_inv by blast
then have n_s_cp_V: "no_step cdcl⇩W_cp V"
using cdcl⇩W_cp_normalized_element_all_inv[of V] full_fullI[of cdcl⇩W_cp V] n_s
conflict'_without_decide conflicting_true_no_step_s'_without_decide_no_step_cdcl⇩W_merge_cp
no_step_cdcl⇩W_merge_cp_no_step_cdcl⇩W_cp
unfolding cdcl⇩W_all_struct_inv_def by presburger
have n_s_bj: "no_step cdcl⇩W_bj V"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain W where W: "cdcl⇩W_bj V W" by blast
have "cdcl⇩W_all_struct_inv W"
using W cdcl⇩W.simps cdcl⇩W_all_struct_inv_inv inv_V by blast
then obtain W' where "full1 cdcl⇩W_bj V W'"
using cdcl⇩W_bj_exists_normal_form[of W] full_fullI[of cdcl⇩W_bj V W] W
unfolding cdcl⇩W_all_struct_inv_def
by blast
moreover
then have "cdcl⇩W⇧+⇧+ V W'"
using tranclp_mono[of cdcl⇩W_bj cdcl⇩W] cdcl⇩W.other cdcl⇩W_o.bj unfolding full1_def by blast
then have "cdcl⇩W_all_struct_inv W'"
by (meson inv_V rtranclp_cdcl⇩W_all_struct_inv_inv tranclp_into_rtranclp)
then obtain X where "full cdcl⇩W_cp W' X"
using cdcl⇩W_cp_normalized_element_all_inv by blast
ultimately show False
using bj'_without_decide n_s_cp_V n_s by blast
qed
from s' consider
(cp_true) "cdcl⇩W_merge_cp⇧*⇧* S V" and "conflicting V = None"
| (cp_false) "cdcl⇩W_merge_cp⇧*⇧* S V" and "conflicting V ≠ None" and "no_step cdcl⇩W_cp V" and
"no_step cdcl⇩W_bj V"
| (cp_confl) T where "cdcl⇩W_merge_cp⇧*⇧* S T" "conflict T V"
using rtranclp_cdcl⇩W_s'_without_decide_is_rtranclp_cdcl⇩W_merge_cp[of S V] confl
unfolding full_def by meson
then have "cdcl⇩W_merge_cp⇧*⇧* S V"
proof cases
case cp_confl note S_T = this(1) and conf_V = this(2)
have "full cdcl⇩W_bj V V"
using conf_V n_s_bj unfolding full_def by fast
then have "cdcl⇩W_merge_cp T V"
using cdcl⇩W_merge_cp.conflict' conf_V by auto
then show ?thesis using S_T by auto
qed fast+
moreover
then have "cdcl⇩W⇧*⇧* S V" using rtranclp_cdcl⇩W_merge_cp_rtranclp_cdcl⇩W by blast
then have "cdcl⇩W_all_struct_inv V"
using inv rtranclp_cdcl⇩W_all_struct_inv_inv by blast
then have "no_step cdcl⇩W_merge_cp V"
using conflicting_true_no_step_s'_without_decide_no_step_cdcl⇩W_merge_cp s'
unfolding full_def by blast
ultimately show ?fw unfolding full_def by auto
qed
lemma conflicting_true_full1_cdcl⇩W_merge_cp_iff_full1_cdcl⇩W_s'_without_decode:
assumes
confl: "conflicting S = None" and
inv: "cdcl⇩W_all_struct_inv S"
shows
"full1 cdcl⇩W_merge_cp S V ⟷ full1 cdcl⇩W_s'_without_decide S V"
proof -
have "full cdcl⇩W_merge_cp S V = full cdcl⇩W_s'_without_decide S V"
using confl conflicting_true_full_cdcl⇩W_merge_cp_iff_full_cdcl⇩W_s'_without_decode inv
by blast
then show ?thesis unfolding full_unfold full1_def
by (metis (mono_tags) tranclp_unfold_begin)
qed
lemma conflicting_true_full1_cdcl⇩W_merge_cp_imp_full1_cdcl⇩W_s'_without_decode:
assumes
fw: "full1 cdcl⇩W_merge_cp S V" and
inv: "cdcl⇩W_all_struct_inv S"
shows
"full1 cdcl⇩W_s'_without_decide S V"
proof -
have "conflicting S = None"
using fw unfolding full1_def by (auto dest!: tranclpD simp: cdcl⇩W_merge_cp.simps)
then show ?thesis
using conflicting_true_full1_cdcl⇩W_merge_cp_iff_full1_cdcl⇩W_s'_without_decode fw inv by blast
qed
inductive cdcl⇩W_merge_stgy where
fw_s_cp[intro]: "full1 cdcl⇩W_merge_cp S T ⟹ cdcl⇩W_merge_stgy S T" |
fw_s_decide[intro]: "decide S T ⟹ no_step cdcl⇩W_merge_cp S ⟹ full cdcl⇩W_merge_cp T U
⟹ cdcl⇩W_merge_stgy S U"
lemma cdcl⇩W_merge_stgy_tranclp_cdcl⇩W_merge:
assumes fw: "cdcl⇩W_merge_stgy S T"
shows "cdcl⇩W_merge⇧+⇧+ S T"
proof -
{ fix S T
assume "full1 cdcl⇩W_merge_cp S T"
then have "cdcl⇩W_merge⇧+⇧+ S T"
using tranclp_mono[of cdcl⇩W_merge_cp "cdcl⇩W_merge⇧+⇧+"] cdcl⇩W_merge_cp_tranclp_cdcl⇩W_merge
unfolding full1_def
by auto
} note full1_cdcl⇩W_merge_cp_cdcl⇩W_merge = this
show ?thesis
using fw
apply (induction rule: cdcl⇩W_merge_stgy.induct)
using full1_cdcl⇩W_merge_cp_cdcl⇩W_merge apply simp
unfolding full_unfold by (auto dest!: full1_cdcl⇩W_merge_cp_cdcl⇩W_merge fw_decide)
qed
lemma rtranclp_cdcl⇩W_merge_stgy_rtranclp_cdcl⇩W_merge:
assumes fw: "cdcl⇩W_merge_stgy⇧*⇧* S T"
shows "cdcl⇩W_merge⇧*⇧* S T"
using fw cdcl⇩W_merge_stgy_tranclp_cdcl⇩W_merge rtranclp_mono[of cdcl⇩W_merge_stgy "cdcl⇩W_merge⇧+⇧+"]
unfolding tranclp_rtranclp_rtranclp by blast
lemma cdcl⇩W_merge_stgy_rtranclp_cdcl⇩W:
"cdcl⇩W_merge_stgy S T ⟹ cdcl⇩W⇧*⇧* S T"
apply (induction rule: cdcl⇩W_merge_stgy.induct)
using rtranclp_cdcl⇩W_merge_cp_rtranclp_cdcl⇩W unfolding full1_def
apply (simp add: tranclp_into_rtranclp)
using rtranclp_cdcl⇩W_merge_cp_rtranclp_cdcl⇩W cdcl⇩W_o.decide cdcl⇩W.other unfolding full_def
by (meson r_into_rtranclp rtranclp_trans)
lemma rtranclp_cdcl⇩W_merge_stgy_rtranclp_cdcl⇩W:
"cdcl⇩W_merge_stgy⇧*⇧* S T ⟹ cdcl⇩W⇧*⇧* S T"
using rtranclp_mono[of cdcl⇩W_merge_stgy "cdcl⇩W⇧*⇧*"] cdcl⇩W_merge_stgy_rtranclp_cdcl⇩W by auto
lemma cdcl⇩W_merge_stgy_cases[consumes 1, case_names fw_s_cp fw_s_decide]:
assumes
"cdcl⇩W_merge_stgy S U"
"full1 cdcl⇩W_merge_cp S U ⟹ P"
"⋀T. decide S T ⟹ no_step cdcl⇩W_merge_cp S ⟹ full cdcl⇩W_merge_cp T U ⟹ P"
shows "P"
using assms by (auto simp: cdcl⇩W_merge_stgy.simps)
inductive cdcl⇩W_s'_w :: "'st ⇒ 'st ⇒ bool" where
conflict': "full1 cdcl⇩W_s'_without_decide S S' ⟹ cdcl⇩W_s'_w S S'" |
decide': "decide S S' ⟹ no_step cdcl⇩W_s'_without_decide S ⟹ full cdcl⇩W_s'_without_decide S' S''
⟹ cdcl⇩W_s'_w S S''"
lemma cdcl⇩W_s'_w_rtranclp_cdcl⇩W:
"cdcl⇩W_s'_w S T ⟹ cdcl⇩W⇧*⇧* S T"
apply (induction rule: cdcl⇩W_s'_w.induct)
using rtranclp_cdcl⇩W_s'_without_decide_rtranclp_cdcl⇩W unfolding full1_def
apply (simp add: tranclp_into_rtranclp)
using rtranclp_cdcl⇩W_s'_without_decide_rtranclp_cdcl⇩W unfolding full_def
by (meson decide other rtranclp_into_tranclp2 tranclp_into_rtranclp)
lemma rtranclp_cdcl⇩W_s'_w_rtranclp_cdcl⇩W:
"cdcl⇩W_s'_w⇧*⇧* S T ⟹ cdcl⇩W⇧*⇧* S T"
using rtranclp_mono[of cdcl⇩W_s'_w "cdcl⇩W⇧*⇧*"] cdcl⇩W_s'_w_rtranclp_cdcl⇩W by auto
lemma no_step_cdcl⇩W_cp_no_step_cdcl⇩W_s'_without_decide:
assumes "no_step cdcl⇩W_cp S" and "conflicting S = None" and inv: "cdcl⇩W_M_level_inv S"
shows "no_step cdcl⇩W_s'_without_decide S"
by (metis assms cdcl⇩W_cp.conflict' cdcl⇩W_cp.propagate' cdcl⇩W_merge_restart_cases tranclpD
conflicting_true_no_step_cdcl⇩W_merge_cp_no_step_s'_without_decide)
lemma no_step_cdcl⇩W_cp_no_step_cdcl⇩W_merge_restart:
assumes "no_step cdcl⇩W_cp S" and "conflicting S = None"
shows "no_step cdcl⇩W_merge_cp S"
by (metis assms(1) cdcl⇩W_cp.conflict' cdcl⇩W_cp.propagate' cdcl⇩W_merge_restart_cases tranclpD)
lemma after_cdcl⇩W_s'_without_decide_no_step_cdcl⇩W_cp:
assumes "cdcl⇩W_s'_without_decide S T"
shows "no_step cdcl⇩W_cp T"
using assms by (induction rule: cdcl⇩W_s'_without_decide.induct) (auto simp: full1_def full_def)
lemma no_step_cdcl⇩W_s'_without_decide_no_step_cdcl⇩W_cp:
"cdcl⇩W_all_struct_inv S ⟹ no_step cdcl⇩W_s'_without_decide S ⟹ no_step cdcl⇩W_cp S"
by (simp add: conflicting_true_no_step_s'_without_decide_no_step_cdcl⇩W_merge_cp
no_step_cdcl⇩W_merge_cp_no_step_cdcl⇩W_cp cdcl⇩W_all_struct_inv_def)
lemma after_cdcl⇩W_s'_w_no_step_cdcl⇩W_cp:
assumes "cdcl⇩W_s'_w S T" and "cdcl⇩W_all_struct_inv S"
shows "no_step cdcl⇩W_cp T"
using assms
proof (induction rule: cdcl⇩W_s'_w.induct)
case conflict'
then show ?case
by (auto simp: full1_def tranclp_unfold_end after_cdcl⇩W_s'_without_decide_no_step_cdcl⇩W_cp)
next
case (decide' S T U)
moreover
then have "cdcl⇩W⇧*⇧* S U"
using rtranclp_cdcl⇩W_s'_without_decide_rtranclp_cdcl⇩W[of T U] cdcl⇩W.other[of S T]
cdcl⇩W_o.decide unfolding full_def by auto
then have "cdcl⇩W_all_struct_inv U"
using decide'.prems rtranclp_cdcl⇩W_all_struct_inv_inv by blast
ultimately show ?case
using no_step_cdcl⇩W_s'_without_decide_no_step_cdcl⇩W_cp unfolding full_def by blast
qed
lemma rtranclp_cdcl⇩W_s'_w_no_step_cdcl⇩W_cp_or_eq:
assumes "cdcl⇩W_s'_w⇧*⇧* S T" and "cdcl⇩W_all_struct_inv S"
shows "S = T ∨ no_step cdcl⇩W_cp T"
using assms
proof (induction rule: rtranclp_induct)
case base
then show ?case by simp
next
case (step T U)
moreover have "cdcl⇩W_all_struct_inv T"
using rtranclp_cdcl⇩W_s'_w_rtranclp_cdcl⇩W[of S U] assms(2) rtranclp_cdcl⇩W_all_struct_inv_inv
rtranclp_cdcl⇩W_s'_w_rtranclp_cdcl⇩W step.hyps(1) by blast
ultimately show ?case using after_cdcl⇩W_s'_w_no_step_cdcl⇩W_cp by fast
qed
lemma rtranclp_cdcl⇩W_merge_stgy'_no_step_cdcl⇩W_cp_or_eq:
assumes "cdcl⇩W_merge_stgy⇧*⇧* S T" and inv: "cdcl⇩W_all_struct_inv S"
shows "S = T ∨ no_step cdcl⇩W_cp T"
using assms
proof (induction rule: rtranclp_induct)
case base
then show ?case by simp
next
case (step T U)
moreover have "cdcl⇩W_all_struct_inv T"
using rtranclp_cdcl⇩W_merge_stgy_rtranclp_cdcl⇩W[of S U] assms(2) rtranclp_cdcl⇩W_all_struct_inv_inv
rtranclp_cdcl⇩W_s'_w_rtranclp_cdcl⇩W step.hyps(1)
by (meson rtranclp_cdcl⇩W_merge_stgy_rtranclp_cdcl⇩W)
ultimately show ?case
using after_cdcl⇩W_s'_w_no_step_cdcl⇩W_cp inv unfolding cdcl⇩W_all_struct_inv_def
by (metis cdcl⇩W_all_struct_inv_def cdcl⇩W_merge_stgy.simps full1_def full_def
no_step_cdcl⇩W_merge_cp_no_step_cdcl⇩W_cp rtranclp_cdcl⇩W_all_struct_inv_inv
rtranclp_cdcl⇩W_merge_stgy_rtranclp_cdcl⇩W tranclp.intros(1) tranclp_into_rtranclp)
qed
lemma no_step_cdcl⇩W_s'_without_decide_no_step_cdcl⇩W_bj:
assumes "no_step cdcl⇩W_s'_without_decide S" and inv: "cdcl⇩W_all_struct_inv S"
shows "no_step cdcl⇩W_bj S"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain T where S_T: "cdcl⇩W_bj S T"
by auto
have "cdcl⇩W_all_struct_inv T"
using S_T cdcl⇩W_all_struct_inv_inv inv other by blast
then obtain T' where "full1 cdcl⇩W_bj S T'"
using cdcl⇩W_bj_exists_normal_form[of T] full_fullI S_T unfolding cdcl⇩W_all_struct_inv_def
by metis
moreover
then have "cdcl⇩W⇧*⇧* S T'"
using rtranclp_mono[of cdcl⇩W_bj cdcl⇩W] cdcl⇩W.other cdcl⇩W_o.bj tranclp_into_rtranclp[of cdcl⇩W_bj]
unfolding full1_def by (metis (full_types) predicate2D predicate2I)
then have "cdcl⇩W_all_struct_inv T'"
using inv rtranclp_cdcl⇩W_all_struct_inv_inv by blast
then obtain U where "full cdcl⇩W_cp T' U"
using cdcl⇩W_cp_normalized_element_all_inv by blast
moreover have "no_step cdcl⇩W_cp S"
using S_T by (auto simp: cdcl⇩W_bj.simps)
ultimately show False
using assms cdcl⇩W_s'_without_decide.intros(2)[of S T' U] by fast
qed
lemma cdcl⇩W_s'_w_no_step_cdcl⇩W_bj:
assumes "cdcl⇩W_s'_w S T" and "cdcl⇩W_all_struct_inv S"
shows "no_step cdcl⇩W_bj T"
using assms apply induction
using rtranclp_cdcl⇩W_s'_without_decide_rtranclp_cdcl⇩W rtranclp_cdcl⇩W_all_struct_inv_inv
no_step_cdcl⇩W_s'_without_decide_no_step_cdcl⇩W_bj unfolding full1_def
apply (meson tranclp_into_rtranclp)
using rtranclp_cdcl⇩W_s'_without_decide_rtranclp_cdcl⇩W rtranclp_cdcl⇩W_all_struct_inv_inv
no_step_cdcl⇩W_s'_without_decide_no_step_cdcl⇩W_bj unfolding full_def
by (meson cdcl⇩W_merge_restart_cdcl⇩W fw_r_decide)
lemma rtranclp_cdcl⇩W_s'_w_no_step_cdcl⇩W_bj_or_eq:
assumes "cdcl⇩W_s'_w⇧*⇧* S T" and "cdcl⇩W_all_struct_inv S"
shows "S = T ∨ no_step cdcl⇩W_bj T"
using assms apply induction
apply simp
using rtranclp_cdcl⇩W_s'_w_rtranclp_cdcl⇩W rtranclp_cdcl⇩W_all_struct_inv_inv
cdcl⇩W_s'_w_no_step_cdcl⇩W_bj by meson
lemma rtranclp_cdcl⇩W_s'_no_step_cdcl⇩W_s'_without_decide_decomp_into_cdcl⇩W_merge:
assumes
"cdcl⇩W_s'⇧*⇧* R V" and
"conflicting R = None" and
inv: "cdcl⇩W_all_struct_inv R"
shows "(cdcl⇩W_merge_stgy⇧*⇧* R V ∧ conflicting V = None)
∨ (cdcl⇩W_merge_stgy⇧*⇧* R V ∧ conflicting V ≠ None ∧ no_step cdcl⇩W_bj V)
∨ (∃S T U. cdcl⇩W_merge_stgy⇧*⇧* R S ∧ no_step cdcl⇩W_merge_cp S ∧ decide S T
∧ cdcl⇩W_merge_cp⇧*⇧* T U ∧ conflict U V)
∨ (∃S T. cdcl⇩W_merge_stgy⇧*⇧* R S ∧ no_step cdcl⇩W_merge_cp S ∧ decide S T
∧ cdcl⇩W_merge_cp⇧*⇧* T V
∧ conflicting V = None)
∨ (cdcl⇩W_merge_cp⇧*⇧* R V ∧ conflicting V = None)
∨ (∃U. cdcl⇩W_merge_cp⇧*⇧* R U ∧ conflict U V)"
using assms(1,2)
proof induction
case base
then show ?case by simp
next
case (step V W) note st = this(1) and s' = this(2) and IH = this(3)[OF this(4)] and
n_s_R = this(4)
from s'
show ?case
proof cases
case conflict'
consider
(s') "cdcl⇩W_merge_stgy⇧*⇧* R V"
| (dec_confl) S T U where "cdcl⇩W_merge_stgy⇧*⇧* R S" and "no_step cdcl⇩W_merge_cp S" and
"decide S T" and "cdcl⇩W_merge_cp⇧*⇧* T U" and "conflict U V"
| (dec) S T where "cdcl⇩W_merge_stgy⇧*⇧* R S" and "no_step cdcl⇩W_merge_cp S" and "decide S T"
and "cdcl⇩W_merge_cp⇧*⇧* T V" and "conflicting V = None"
| (cp) "cdcl⇩W_merge_cp⇧*⇧* R V"
| (cp_confl) U where "cdcl⇩W_merge_cp⇧*⇧* R U" and "conflict U V"
using IH by meson
then show ?thesis
proof cases
next
case s'
then have "R = V"
by (metis full1_def inv local.conflict' tranclp_unfold_begin
rtranclp_cdcl⇩W_merge_stgy'_no_step_cdcl⇩W_cp_or_eq)
consider
(V_W) "V = W"
| (propa) "propagate⇧+⇧+ V W" and "conflicting W = None"
| (propa_confl) V' where "propagate⇧*⇧* V V'" and "conflict V' W"
using tranclp_cdcl⇩W_cp_propagate_with_conflict_or_not[of V W] conflict'
unfolding full_unfold full1_def by meson
then show ?thesis
proof cases
case V_W
then show ?thesis using ‹R = V› n_s_R by simp
next
case propa
then show ?thesis using ‹R = V› by auto
next
case propa_confl
moreover
then have "cdcl⇩W_merge_cp⇧*⇧* V V'"
by (metis rtranclp_unfold cdcl⇩W_merge_cp.propagate' r_into_rtranclp)
ultimately show ?thesis using s' ‹R = V› by blast
qed
next
case dec_confl note _ = this(5)
then have False using conflict' unfolding full1_def by (auto dest!: tranclpD)
then show ?thesis by fast
next
case dec note T_V = this(4)
consider
(propa) "propagate⇧+⇧+ V W" and "conflicting W = None"
| (propa_confl) V' where "propagate⇧*⇧* V V'" and "conflict V' W"
using tranclp_cdcl⇩W_cp_propagate_with_conflict_or_not[of V W] conflict'
unfolding full1_def by meson
then show ?thesis
proof cases
case propa
then show ?thesis
by (meson T_V cdcl⇩W_merge_cp.propagate' dec rtranclp.rtrancl_into_rtrancl)
next
case propa_confl
then have "cdcl⇩W_merge_cp⇧*⇧* T V'"
using T_V by (metis rtranclp_unfold cdcl⇩W_merge_cp.propagate' rtranclp.simps)
then show ?thesis using dec propa_confl(2) by metis
qed
next
case cp
consider
(propa) "propagate⇧+⇧+ V W" and "conflicting W = None"
| (propa_confl) V' where "propagate⇧*⇧* V V'" and "conflict V' W"
using tranclp_cdcl⇩W_cp_propagate_with_conflict_or_not[of V W] conflict'
unfolding full1_def by meson
then show ?thesis
proof cases
case propa
then show ?thesis by (meson cdcl⇩W_merge_cp.propagate' cp rtranclp.rtrancl_into_rtrancl)
next
case propa_confl
then show ?thesis
using propa_confl(2) by (metis rtranclp_unfold cdcl⇩W_merge_cp.propagate'
cp rtranclp.rtrancl_into_rtrancl)
qed
next
case cp_confl
then show ?thesis using conflict' unfolding full1_def by (fastforce dest!: tranclpD)
qed
next
case (decide' V')
then have conf_V: "conflicting V = None"
by auto
consider
(s') "cdcl⇩W_merge_stgy⇧*⇧* R V"
| (dec_confl) S T U where "cdcl⇩W_merge_stgy⇧*⇧* R S" and "no_step cdcl⇩W_merge_cp S" and
"decide S T" and "cdcl⇩W_merge_cp⇧*⇧* T U" and "conflict U V"
| (dec) S T where "cdcl⇩W_merge_stgy⇧*⇧* R S" and "no_step cdcl⇩W_merge_cp S" and "decide S T"
and "cdcl⇩W_merge_cp⇧*⇧* T V" and "conflicting V = None"
| (cp) "cdcl⇩W_merge_cp⇧*⇧* R V"
| (cp_confl) U where "cdcl⇩W_merge_cp⇧*⇧* R U" and "conflict U V"
using IH by meson
then show ?thesis
proof cases
case s'
have confl_V': "conflicting V' = None" using decide'(1) by auto
have full: "full1 cdcl⇩W_cp V' W ∨ (V' = W ∧ no_step cdcl⇩W_cp W)"
using decide'(3) unfolding full_unfold by blast
consider
(V'_W) "V' = W"
| (propa) "propagate⇧+⇧+ V' W" and "conflicting W = None"
| (propa_confl) V'' where "propagate⇧*⇧* V' V''" and "conflict V'' W"
using tranclp_cdcl⇩W_cp_propagate_with_conflict_or_not[of V W] decide'
by (metis ‹full1 cdcl⇩W_cp V' W ∨ V' = W ∧ no_step cdcl⇩W_cp W› full1_def
tranclp_cdcl⇩W_cp_propagate_with_conflict_or_not)
then show ?thesis
proof cases
case V'_W
then show ?thesis
using confl_V' local.decide'(1,2) s' conf_V
no_step_cdcl⇩W_cp_no_step_cdcl⇩W_merge_restart[of V] by blast
next
case propa
then show ?thesis using local.decide'(1,2) s' by (metis cdcl⇩W_merge_cp.simps conf_V
no_step_cdcl⇩W_cp_no_step_cdcl⇩W_merge_restart r_into_rtranclp)
next
case propa_confl
then have "cdcl⇩W_merge_cp⇧*⇧* V' V''"
by (metis rtranclp_unfold cdcl⇩W_merge_cp.propagate' r_into_rtranclp)
then show ?thesis
using local.decide'(1,2) propa_confl(2) s' conf_V
no_step_cdcl⇩W_cp_no_step_cdcl⇩W_merge_restart
by metis
qed
next
case (dec) note s' = this(1) and dec = this(2) and cp = this(3) and ns_cp_T = this(4)
have "full cdcl⇩W_merge_cp T V"
unfolding full_def by (simp add: conf_V local.decide'(2)
no_step_cdcl⇩W_cp_no_step_cdcl⇩W_merge_restart ns_cp_T)
moreover have "no_step cdcl⇩W_merge_cp V"
by (simp add: conf_V local.decide'(2) no_step_cdcl⇩W_cp_no_step_cdcl⇩W_merge_restart)
moreover have "no_step cdcl⇩W_merge_cp S"
by (metis dec)
ultimately have "cdcl⇩W_merge_stgy S V"
using cp by blast
then have "cdcl⇩W_merge_stgy⇧*⇧* R V" using s' by auto
consider
(V'_W) "V' = W"
| (propa) "propagate⇧+⇧+ V' W" and "conflicting W = None"
| (propa_confl) V'' where "propagate⇧*⇧* V' V''" and "conflict V'' W"
using tranclp_cdcl⇩W_cp_propagate_with_conflict_or_not[of V' W] decide'
unfolding full_unfold full1_def by meson
then show ?thesis
proof cases
case V'_W
moreover have "conflicting V' = None"
using decide'(1) by auto
ultimately show ?thesis
using ‹cdcl⇩W_merge_stgy⇧*⇧* R V› decide' ‹no_step cdcl⇩W_merge_cp V› by blast
next
case propa
moreover then have "cdcl⇩W_merge_cp V' W"
by auto
ultimately show ?thesis
using ‹cdcl⇩W_merge_stgy⇧*⇧* R V› decide' ‹no_step cdcl⇩W_merge_cp V›
by (meson r_into_rtranclp)
next
case propa_confl
moreover then have "cdcl⇩W_merge_cp⇧*⇧* V' V''"
by (metis cdcl⇩W_merge_cp.propagate' rtranclp_unfold tranclp_unfold_end)
ultimately show ?thesis using ‹cdcl⇩W_merge_stgy⇧*⇧* R V› decide'
‹no_step cdcl⇩W_merge_cp V› by (meson r_into_rtranclp)
qed
next
case cp
have "no_step cdcl⇩W_merge_cp V"
using conf_V local.decide'(2) no_step_cdcl⇩W_cp_no_step_cdcl⇩W_merge_restart by blast
then have "full cdcl⇩W_merge_cp R V"
unfolding full_def using cp by fast
then have "cdcl⇩W_merge_stgy⇧*⇧* R V"
unfolding full_unfold by auto
have "full1 cdcl⇩W_cp V' W ∨ (V' = W ∧ no_step cdcl⇩W_cp W)"
using decide'(3) unfolding full_unfold by blast
consider
(V'_W) "V' = W"
| (propa) "propagate⇧+⇧+ V' W" and "conflicting W = None"
| (propa_confl) V'' where "propagate⇧*⇧* V' V''" and "conflict V'' W"
using tranclp_cdcl⇩W_cp_propagate_with_conflict_or_not[of V' W] decide'
unfolding full_unfold full1_def by meson
then show ?thesis
proof cases
case V'_W
moreover have "conflicting V' = None"
using decide'(1) by auto
ultimately show ?thesis
using ‹cdcl⇩W_merge_stgy⇧*⇧* R V› decide' ‹no_step cdcl⇩W_merge_cp V› by blast
next
case propa
moreover then have "cdcl⇩W_merge_cp V' W"
by auto
ultimately show ?thesis using ‹cdcl⇩W_merge_stgy⇧*⇧* R V› decide'
‹no_step cdcl⇩W_merge_cp V› by (meson r_into_rtranclp)
next
case propa_confl
moreover then have "cdcl⇩W_merge_cp⇧*⇧* V' V''"
by (metis cdcl⇩W_merge_cp.propagate' rtranclp_unfold tranclp_unfold_end)
ultimately show ?thesis using ‹cdcl⇩W_merge_stgy⇧*⇧* R V› decide'
‹no_step cdcl⇩W_merge_cp V› by (meson r_into_rtranclp)
qed
next
case (dec_confl)
show ?thesis using conf_V dec_confl(5) by auto
next
case cp_confl
then show ?thesis using decide' apply - by (intro HOL.disjI2) fastforce
qed
next
case (bj' V')
then have "¬no_step cdcl⇩W_bj V "
by (auto dest: tranclpD simp: full1_def)
then consider
(s') "cdcl⇩W_merge_stgy⇧*⇧* R V" and "conflicting V = None"
| (dec_confl) S T U where "cdcl⇩W_merge_stgy⇧*⇧* R S" and "no_step cdcl⇩W_merge_cp S" and
"decide S T" and "cdcl⇩W_merge_cp⇧*⇧* T U" and "conflict U V"
| (dec) S T where "cdcl⇩W_merge_stgy⇧*⇧* R S" and "no_step cdcl⇩W_merge_cp S" and "decide S T"
and "cdcl⇩W_merge_cp⇧*⇧* T V" and "conflicting V = None"
| (cp) "cdcl⇩W_merge_cp⇧*⇧* R V" and "conflicting V = None"
| (cp_confl) U where "cdcl⇩W_merge_cp⇧*⇧* R U" and "conflict U V"
using IH by meson
then show ?thesis
proof cases
case s' note _ =this(2)
then have False
using bj'(1) unfolding full1_def by (force dest!: tranclpD simp: cdcl⇩W_bj.simps)
then show ?thesis by fast
next
case dec note _ = this(5)
then have False
using bj'(1) unfolding full1_def by (force dest!: tranclpD simp: cdcl⇩W_bj.simps)
then show ?thesis by fast
next
case dec_confl
then have "cdcl⇩W_merge_cp U V'"
using bj' cdcl⇩W_merge_cp.intros(1)[of U V V'] by (simp add: full_unfold)
then have "cdcl⇩W_merge_cp⇧*⇧* T V'"
using dec_confl(4) by simp
consider
(V'_W) "V' = W"
| (propa) "propagate⇧+⇧+ V' W" and "conflicting W = None"
| (propa_confl) V'' where "propagate⇧*⇧* V' V''" and "conflict V'' W"
using tranclp_cdcl⇩W_cp_propagate_with_conflict_or_not[of V' W] bj'(3)
unfolding full_unfold full1_def by meson
then show ?thesis
proof cases
case V'_W
then have "no_step cdcl⇩W_cp V'"
using bj'(3) unfolding full_def by auto
then have "no_step cdcl⇩W_merge_cp V'"
by (metis cdcl⇩W_cp.propagate' cdcl⇩W_merge_cp.cases tranclpD
no_step_cdcl⇩W_cp_no_conflict_no_propagate(1) )
then have "full1 cdcl⇩W_merge_cp T V'"
unfolding full1_def using ‹cdcl⇩W_merge_cp U V'› dec_confl(4) by auto
then have "full cdcl⇩W_merge_cp T V'"
by (simp add: full_unfold)
then have "cdcl⇩W_merge_stgy S V'"
using dec_confl(3) cdcl⇩W_merge_stgy.fw_s_decide ‹no_step cdcl⇩W_merge_cp S› by blast
then have "cdcl⇩W_merge_stgy⇧*⇧* R V'"
using ‹cdcl⇩W_merge_stgy⇧*⇧* R S› by auto
show ?thesis
proof cases
assume "conflicting W = None"
then show ?thesis using ‹cdcl⇩W_merge_stgy⇧*⇧* R V'› ‹V' = W› by auto
next
assume "conflicting W ≠ None"
then show ?thesis
using ‹cdcl⇩W_merge_stgy⇧*⇧* R V'› ‹V' = W› by (metis ‹cdcl⇩W_merge_cp U V'›
conflicting_not_true_rtranclp_cdcl⇩W_merge_cp_no_step_cdcl⇩W_bj dec_confl(5)
r_into_rtranclp conflictE)
qed
next
case propa
moreover then have "cdcl⇩W_merge_cp V' W"
by auto
ultimately show ?thesis using decide' by (meson ‹cdcl⇩W_merge_cp⇧*⇧* T V'› dec_confl(1-3)
rtranclp.rtrancl_into_rtrancl)
next
case propa_confl
moreover then have "cdcl⇩W_merge_cp⇧*⇧* V' V''"
by (metis cdcl⇩W_merge_cp.propagate' rtranclp_unfold tranclp_unfold_end)
ultimately show ?thesis by (meson ‹cdcl⇩W_merge_cp⇧*⇧* T V'› dec_confl(1-3) rtranclp_trans)
qed
next
case cp note _ = this(2)
then show ?thesis using bj'(1) ‹¬ no_step cdcl⇩W_bj V›
conflicting_not_true_rtranclp_cdcl⇩W_merge_cp_no_step_cdcl⇩W_bj by auto
next
case cp_confl
then have "cdcl⇩W_merge_cp U V'" by (simp add: cdcl⇩W_merge_cp.conflict' full_unfold
local.bj'(1))
consider
(V'_W) "V' = W"
| (propa) "propagate⇧+⇧+ V' W" and "conflicting W = None"
| (propa_confl) V'' where "propagate⇧*⇧* V' V''" and "conflict V'' W"
using tranclp_cdcl⇩W_cp_propagate_with_conflict_or_not[of V' W] bj'
unfolding full_unfold full1_def by meson
then show ?thesis
proof cases
case V'_W
show ?thesis
proof cases
assume "conflicting V' = None"
then show ?thesis
using V'_W ‹cdcl⇩W_merge_cp U V'› cp_confl(1) by force
next
assume confl: "conflicting V' ≠ None"
then have "no_step cdcl⇩W_merge_stgy V'"
by (fastforce simp: cdcl⇩W_merge_stgy.simps full1_def full_def
cdcl⇩W_merge_cp.simps dest!: tranclpD)
have "no_step cdcl⇩W_merge_cp V'"
using confl by (auto simp: full1_def full_def cdcl⇩W_merge_cp.simps
dest!: tranclpD)
moreover have "cdcl⇩W_merge_cp U W"
using V'_W ‹cdcl⇩W_merge_cp U V'› by blast
ultimately have "full1 cdcl⇩W_merge_cp R V'"
using cp_confl(1) V'_W unfolding full1_def by auto
then have "cdcl⇩W_merge_stgy R V'"
by auto
moreover have "no_step cdcl⇩W_merge_stgy V'"
using confl ‹no_step cdcl⇩W_merge_cp V'› by (auto simp: cdcl⇩W_merge_stgy.simps
full1_def dest!: tranclpD)
ultimately have "cdcl⇩W_merge_stgy⇧*⇧* R V'" by auto
show ?thesis by (metis V'_W ‹cdcl⇩W_merge_cp U V'› ‹cdcl⇩W_merge_stgy⇧*⇧* R V'›
conflicting_not_true_rtranclp_cdcl⇩W_merge_cp_no_step_cdcl⇩W_bj cp_confl(1)
rtranclp.rtrancl_into_rtrancl step.prems)
qed
next
case propa
moreover then have "cdcl⇩W_merge_cp V' W"
by auto
ultimately show ?thesis using ‹cdcl⇩W_merge_cp U V'› cp_confl(1) by force
next
case propa_confl
moreover then have "cdcl⇩W_merge_cp⇧*⇧* V' V''"
by (metis cdcl⇩W_merge_cp.propagate' rtranclp_unfold tranclp_unfold_end)
ultimately show ?thesis
using ‹cdcl⇩W_merge_cp U V'› cp_confl(1) by (metis rtranclp.rtrancl_into_rtrancl
rtranclp_trans)
qed
qed
qed
qed
lemma decide_rtranclp_cdcl⇩W_s'_rtranclp_cdcl⇩W_s':
assumes
dec: "decide S T" and
"cdcl⇩W_s'⇧*⇧* T U" and
n_s_S: "no_step cdcl⇩W_cp S" and
"no_step cdcl⇩W_cp U"
shows "cdcl⇩W_s'⇧*⇧* S U"
using assms(2,4)
proof induction
case (step U V) note st =this(1) and s' = this(2) and IH = this(3) and n_s = this(4)
consider
(TU) "T = U"
| (s'_st) T' where "cdcl⇩W_s' T T'" and "cdcl⇩W_s'⇧*⇧* T' U"
using st[unfolded rtranclp_unfold] by (auto dest!: tranclpD)
then show ?case
proof cases
case TU
then show ?thesis
proof -
assume a1: "T = U"
then have f2: "cdcl⇩W_s' T V"
using s' by force
obtain ss :: 'st where
"cdcl⇩W_s'⇧*⇧* S T ∨ cdcl⇩W_cp T ss"
using a1 step.IH by blast
then show ?thesis
using f2 by (metis (full_types) cdcl⇩W_s'.decide' cdcl⇩W_s'E dec full1_is_full n_s_S
rtranclp_unfold tranclp_unfold_end)
qed
next
case (s'_st T') note s'_T' = this(1) and st = this(2)
have "cdcl⇩W_s'⇧*⇧* S T'"
using s'_T'
proof cases
case conflict'
then have "cdcl⇩W_s' S T'"
using dec cdcl⇩W_s'.decide' n_s_S by (simp add: full_unfold)
then show ?thesis
using st by auto
next
case (decide' T'')
then have "cdcl⇩W_s' S T"
using dec cdcl⇩W_s'.decide' n_s_S by (simp add: full_unfold)
then show ?thesis using decide' s'_T' by auto
next
case bj'
then have False
using dec unfolding full1_def by (fastforce dest!: tranclpD simp: cdcl⇩W_bj.simps)
then show ?thesis by fast
qed
then show ?thesis using s' st by auto
qed
next
case base
then have "full cdcl⇩W_cp T T"
by (simp add: full_unfold)
then show ?case
using cdcl⇩W_s'.simps dec n_s_S by auto
qed
lemma rtranclp_cdcl⇩W_merge_stgy_rtranclp_cdcl⇩W_s':
assumes
"cdcl⇩W_merge_stgy⇧*⇧* R V" and
inv: "cdcl⇩W_all_struct_inv R"
shows "cdcl⇩W_s'⇧*⇧* R V"
using assms(1)
proof induction
case base
then show ?case by simp
next
case (step S T) note st = this(1) and fw = this(2) and IH = this(3)
have "cdcl⇩W_all_struct_inv S"
using inv rtranclp_cdcl⇩W_all_struct_inv_inv rtranclp_cdcl⇩W_merge_stgy_rtranclp_cdcl⇩W st by blast
from fw show ?case
proof (cases rule: cdcl⇩W_merge_stgy_cases)
case fw_s_cp
then show ?thesis
proof -
assume a1: "full1 cdcl⇩W_merge_cp S T"
obtain ss :: "('st ⇒ 'st ⇒ bool) ⇒ 'st ⇒ 'st" where
f2: "⋀p s sa pa sb sc sd pb se sf. (¬ full1 p (s::'st) sa ∨ p⇧+⇧+ s sa)
∧ (¬ pa (sb::'st) sc ∨ ¬ full1 pa sd sb) ∧ (¬ pb⇧+⇧+ se sf ∨ pb sf (ss pb sf)
∨ full1 pb se sf)"
by (metis (no_types) full1_def)
then have f3: "cdcl⇩W_merge_cp⇧+⇧+ S T"
using a1 by auto
obtain ssa :: "('st ⇒ 'st ⇒ bool) ⇒ 'st ⇒ 'st ⇒ 'st" where
f4: "⋀p s sa. ¬ p⇧+⇧+ s sa ∨ p s (ssa p s sa)"
by (meson tranclp_unfold_begin)
then have f5: "⋀s. ¬ full1 cdcl⇩W_merge_cp s S"
using f3 f2 by (metis (full_types))
have "⋀s. ¬ full cdcl⇩W_merge_cp s S"
using f4 f3 by (meson full_def)
then have "S = R"
using f5 by (metis (no_types) cdcl⇩W_merge_stgy.simps rtranclp_unfold st
tranclp_unfold_end)
then show ?thesis
using f2 a1 by (metis (no_types) ‹cdcl⇩W_all_struct_inv S›
conflicting_true_full1_cdcl⇩W_merge_cp_imp_full1_cdcl⇩W_s'_without_decode
rtranclp_cdcl⇩W_s'_without_decide_rtranclp_cdcl⇩W_s' rtranclp_unfold)
qed
next
case (fw_s_decide S') note dec = this(1) and n_S = this(2) and full = this(3)
moreover then have "conflicting S' = None"
by auto
ultimately have "full cdcl⇩W_s'_without_decide S' T"
by (meson ‹cdcl⇩W_all_struct_inv S› cdcl⇩W_merge_restart_cdcl⇩W fw_r_decide
rtranclp_cdcl⇩W_all_struct_inv_inv
conflicting_true_full_cdcl⇩W_merge_cp_iff_full_cdcl⇩W_s'_without_decode)
then have a1: "cdcl⇩W_s'⇧*⇧* S' T"
unfolding full_def by (metis (full_types)rtranclp_cdcl⇩W_s'_without_decide_rtranclp_cdcl⇩W_s')
have "cdcl⇩W_merge_stgy⇧*⇧* S T"
using fw by blast
then have "cdcl⇩W_s'⇧*⇧* S T"
using decide_rtranclp_cdcl⇩W_s'_rtranclp_cdcl⇩W_s' a1 by (metis ‹cdcl⇩W_all_struct_inv S› dec
n_S no_step_cdcl⇩W_merge_cp_no_step_cdcl⇩W_cp cdcl⇩W_all_struct_inv_def
rtranclp_cdcl⇩W_merge_stgy'_no_step_cdcl⇩W_cp_or_eq)
then show ?thesis using IH by auto
qed
qed
lemma rtranclp_cdcl⇩W_merge_stgy_distinct_mset_clauses:
assumes invR: "cdcl⇩W_all_struct_inv R" and
st: "cdcl⇩W_merge_stgy⇧*⇧* R S" and
dist: "distinct_mset (clauses R)" and
R: "trail R = []"
shows "distinct_mset (clauses S)"
using rtranclp_cdcl⇩W_stgy_distinct_mset_clauses[OF invR _ dist R]
invR st rtranclp_mono[of cdcl⇩W_s' "cdcl⇩W_stgy⇧*⇧*"] cdcl⇩W_s'_is_rtranclp_cdcl⇩W_stgy
by (auto dest!: cdcl⇩W_s'_is_rtranclp_cdcl⇩W_stgy rtranclp_cdcl⇩W_merge_stgy_rtranclp_cdcl⇩W_s')
lemma no_step_cdcl⇩W_s'_no_step_cdcl⇩W_merge_stgy:
assumes
inv: "cdcl⇩W_all_struct_inv R" and s': "no_step cdcl⇩W_s' R"
shows "no_step cdcl⇩W_merge_stgy R"
proof -
{ fix ss :: 'st
obtain ssa :: "'st ⇒ 'st ⇒ 'st" where
ff1: "⋀s sa. ¬ cdcl⇩W_merge_stgy s sa ∨ full1 cdcl⇩W_merge_cp s sa ∨ decide s (ssa s sa)"
using cdcl⇩W_merge_stgy.cases by moura
obtain ssb :: "('st ⇒ 'st ⇒ bool) ⇒ 'st ⇒ 'st ⇒ 'st" where
ff2: "⋀p s sa. ¬ p⇧+⇧+ s sa ∨ p s (ssb p s sa)"
by (meson tranclp_unfold_begin)
obtain ssc :: "'st ⇒ 'st" where
ff3: "⋀s sa sb. (¬ cdcl⇩W_all_struct_inv s ∨ ¬ cdcl⇩W_cp s sa ∨ cdcl⇩W_s' s (ssc s))
∧ (¬ cdcl⇩W_all_struct_inv s ∨ ¬ cdcl⇩W_o s sb ∨ cdcl⇩W_s' s (ssc s))"
using n_step_cdcl⇩W_stgy_iff_no_step_cdcl⇩W_cl_cdcl⇩W_o by moura
then have ff4: "⋀s. ¬ cdcl⇩W_o R s"
using s' inv by blast
have ff5: "⋀s. ¬ cdcl⇩W_cp⇧+⇧+ R s"
using ff3 ff2 s' by (metis inv)
have "⋀s. ¬ cdcl⇩W_bj⇧+⇧+ R s"
using ff4 ff2 by (metis bj)
then have "⋀s. ¬ cdcl⇩W_s'_without_decide R s"
using ff5 by (simp add: cdcl⇩W_s'_without_decide.simps full1_def)
then have "¬ cdcl⇩W_s'_without_decide⇧+⇧+ R ss"
using ff2 by blast
then have "¬ cdcl⇩W_merge_stgy R ss"
using ff4 ff1 by (metis (full_types) decide full1_def inv
conflicting_true_full1_cdcl⇩W_merge_cp_imp_full1_cdcl⇩W_s'_without_decode) }
then show ?thesis
by fastforce
qed
lemma wf_cdcl⇩W_merge_cp:
"wf{(T, S). cdcl⇩W_all_struct_inv S ∧ cdcl⇩W_merge_cp S T}"
using wf_tranclp_cdcl⇩W_merge by (rule wf_subset) (auto simp: cdcl⇩W_merge_cp_tranclp_cdcl⇩W_merge)
lemma wf_cdcl⇩W_merge_stgy:
"wf{(T, S). cdcl⇩W_all_struct_inv S ∧ cdcl⇩W_merge_stgy S T}"
using wf_tranclp_cdcl⇩W_merge by (rule wf_subset)
(auto simp add: cdcl⇩W_merge_stgy_tranclp_cdcl⇩W_merge)
lemma cdcl⇩W_merge_cp_obtain_normal_form:
assumes inv: "cdcl⇩W_all_struct_inv R"
obtains S where "full cdcl⇩W_merge_cp R S"
proof -
obtain S where "full (λS T. cdcl⇩W_all_struct_inv S ∧ cdcl⇩W_merge_cp S T) R S"
using wf_exists_normal_form_full[OF wf_cdcl⇩W_merge_cp] by blast
then have
st: "(λS T. cdcl⇩W_all_struct_inv S ∧ cdcl⇩W_merge_cp S T)⇧*⇧* R S" and
n_s: "no_step (λS T. cdcl⇩W_all_struct_inv S ∧ cdcl⇩W_merge_cp S T) S"
unfolding full_def by blast+
have "cdcl⇩W_merge_cp⇧*⇧* R S"
using st by induction auto
moreover
have "cdcl⇩W_all_struct_inv S"
using st inv
apply (induction rule: rtranclp_induct)
apply simp
by (meson r_into_rtranclp rtranclp_cdcl⇩W_all_struct_inv_inv
rtranclp_cdcl⇩W_merge_cp_rtranclp_cdcl⇩W)
then have "no_step cdcl⇩W_merge_cp S"
using n_s by auto
ultimately show ?thesis
using that unfolding full_def by blast
qed
lemma no_step_cdcl⇩W_merge_stgy_no_step_cdcl⇩W_s':
assumes
inv: "cdcl⇩W_all_struct_inv R" and
confl: "conflicting R = None" and
n_s: "no_step cdcl⇩W_merge_stgy R"
shows "no_step cdcl⇩W_s' R"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain S where "cdcl⇩W_s' R S" by auto
then show False
proof cases
case conflict'
then obtain S' where "full1 cdcl⇩W_merge_cp R S'"
by (metis (full_types) cdcl⇩W_merge_cp_obtain_normal_form cdcl⇩W_s'_without_decide.simps confl
conflicting_true_no_step_cdcl⇩W_merge_cp_no_step_s'_without_decide full_def full_unfold inv
cdcl⇩W_all_struct_inv_def)
then show False using n_s by blast
next
case (decide' R')
then have "cdcl⇩W_all_struct_inv R'"
using inv cdcl⇩W_all_struct_inv_inv cdcl⇩W.other cdcl⇩W_o.decide by meson
then obtain R'' where "full cdcl⇩W_merge_cp R' R''"
using cdcl⇩W_merge_cp_obtain_normal_form by blast
moreover have "no_step cdcl⇩W_merge_cp R"
by (simp add: confl local.decide'(2) no_step_cdcl⇩W_cp_no_step_cdcl⇩W_merge_restart)
ultimately show False using n_s cdcl⇩W_merge_stgy.intros local.decide'(1) by blast
next
case (bj' R')
then show False
using confl no_step_cdcl⇩W_cp_no_step_cdcl⇩W_s'_without_decide inv
unfolding cdcl⇩W_all_struct_inv_def by blast
qed
qed
lemma rtranclp_cdcl⇩W_merge_cp_no_step_cdcl⇩W_bj:
assumes "conflicting R = None" and "cdcl⇩W_merge_cp⇧*⇧* R S"
shows "no_step cdcl⇩W_bj S"
using assms conflicting_not_true_rtranclp_cdcl⇩W_merge_cp_no_step_cdcl⇩W_bj by blast
lemma rtranclp_cdcl⇩W_merge_stgy_no_step_cdcl⇩W_bj:
assumes confl: "conflicting R = None" and "cdcl⇩W_merge_stgy⇧*⇧* R S"
shows "no_step cdcl⇩W_bj S"
using assms(2)
proof induction
case base
then show ?case
using confl by (auto simp: cdcl⇩W_bj.simps)[]
next
case (step S T) note st = this(1) and fw = this(2) and IH = this(3)
have confl_S: "conflicting S = None"
using fw apply cases
by (auto simp: full1_def cdcl⇩W_merge_cp.simps dest!: tranclpD)
from fw show ?case
proof cases
case fw_s_cp
then show ?thesis
using rtranclp_cdcl⇩W_merge_cp_no_step_cdcl⇩W_bj confl_S
by (simp add: full1_def tranclp_into_rtranclp)
next
case (fw_s_decide S')
moreover then have "conflicting S' = None" by auto
ultimately show ?thesis
using conflicting_not_true_rtranclp_cdcl⇩W_merge_cp_no_step_cdcl⇩W_bj
unfolding full_def by meson
qed
qed
lemma full_cdcl⇩W_s'_full_cdcl⇩W_merge_restart:
assumes
"conflicting R = None" and
inv: "cdcl⇩W_all_struct_inv R"
shows "full cdcl⇩W_s' R V ⟷ full cdcl⇩W_merge_stgy R V" (is "?s' ⟷ ?fw")
proof
assume ?s'
then have "cdcl⇩W_s'⇧*⇧* R V" unfolding full_def by blast
have "cdcl⇩W_all_struct_inv V"
using ‹cdcl⇩W_s'⇧*⇧* R V› inv rtranclp_cdcl⇩W_all_struct_inv_inv rtranclp_cdcl⇩W_s'_rtranclp_cdcl⇩W
by blast
then have n_s: "no_step cdcl⇩W_merge_stgy V"
using no_step_cdcl⇩W_s'_no_step_cdcl⇩W_merge_stgy by (meson ‹full cdcl⇩W_s' R V› full_def)
have n_s_bj: "no_step cdcl⇩W_bj V"
by (metis ‹cdcl⇩W_all_struct_inv V› ‹full cdcl⇩W_s' R V› bj full_def
n_step_cdcl⇩W_stgy_iff_no_step_cdcl⇩W_cl_cdcl⇩W_o)
have n_s_cp: "no_step cdcl⇩W_merge_cp V"
proof -
{ fix ss :: 'st
obtain ssa :: "'st ⇒ 'st" where
ff1: "∀s. ¬ cdcl⇩W_all_struct_inv s ∨ cdcl⇩W_s'_without_decide s (ssa s)
∨ no_step cdcl⇩W_merge_cp s"
using conflicting_true_no_step_s'_without_decide_no_step_cdcl⇩W_merge_cp by moura
have "(∀p s sa. ¬ full p (s::'st) sa ∨ p⇧*⇧* s sa ∧ no_step p sa)" and
"(∀p s sa. (¬ p⇧*⇧* (s::'st) sa ∨ (∃s. p sa s)) ∨ full p s sa)"
by (meson full_def)+
then have "¬ cdcl⇩W_merge_cp V ss"
using ff1 by (metis (no_types) ‹cdcl⇩W_all_struct_inv V› ‹full cdcl⇩W_s' R V› cdcl⇩W_s'.simps
cdcl⇩W_s'_without_decide.cases) }
then show ?thesis
by blast
qed
consider
(fw_no_confl) "cdcl⇩W_merge_stgy⇧*⇧* R V" and "conflicting V = None"
| (fw_confl) "cdcl⇩W_merge_stgy⇧*⇧* R V" and "conflicting V ≠ None" and "no_step cdcl⇩W_bj V"
| (fw_dec_confl) S T U where "cdcl⇩W_merge_stgy⇧*⇧* R S" and "no_step cdcl⇩W_merge_cp S" and
"decide S T" and "cdcl⇩W_merge_cp⇧*⇧* T U" and "conflict U V"
| (fw_dec_no_confl) S T where "cdcl⇩W_merge_stgy⇧*⇧* R S" and "no_step cdcl⇩W_merge_cp S" and
"decide S T" and "cdcl⇩W_merge_cp⇧*⇧* T V" and "conflicting V = None"
| (cp_no_confl) "cdcl⇩W_merge_cp⇧*⇧* R V" and "conflicting V = None"
| (cp_confl) U where "cdcl⇩W_merge_cp⇧*⇧* R U" and "conflict U V"
using rtranclp_cdcl⇩W_s'_no_step_cdcl⇩W_s'_without_decide_decomp_into_cdcl⇩W_merge[OF
‹cdcl⇩W_s'⇧*⇧* R V› assms] by auto
then show ?fw
proof cases
case fw_no_confl
then show ?thesis using n_s unfolding full_def by blast
next
case fw_confl
then show ?thesis using n_s unfolding full_def by blast
next
case fw_dec_confl
have "cdcl⇩W_merge_cp U V"
using n_s_bj by (metis cdcl⇩W_merge_cp.simps full_unfold fw_dec_confl(5))
then have "full1 cdcl⇩W_merge_cp T V"
unfolding full1_def by (metis fw_dec_confl(4) n_s_cp tranclp_unfold_end)
then have "cdcl⇩W_merge_stgy S V" using ‹decide S T› ‹no_step cdcl⇩W_merge_cp S› by auto
then show ?thesis using n_s ‹ cdcl⇩W_merge_stgy⇧*⇧* R S› unfolding full_def by auto
next
case fw_dec_no_confl
then have "full cdcl⇩W_merge_cp T V"
using n_s_cp unfolding full_def by blast
then have "cdcl⇩W_merge_stgy S V" using ‹decide S T› ‹no_step cdcl⇩W_merge_cp S› by auto
then show ?thesis using n_s ‹ cdcl⇩W_merge_stgy⇧*⇧* R S› unfolding full_def by auto
next
case cp_no_confl
then have "full cdcl⇩W_merge_cp R V"
by (simp add: full_def n_s_cp)
then have "R = V ∨ cdcl⇩W_merge_stgy⇧+⇧+ R V"
by (metis (no_types) full_unfold fw_s_cp rtranclp_unfold tranclp_unfold_end)
then show ?thesis
by (simp add: full_def n_s rtranclp_unfold)
next
case cp_confl
have "full cdcl⇩W_bj V V"
using n_s_bj unfolding full_def by blast
then have "full1 cdcl⇩W_merge_cp R V"
unfolding full1_def by (meson cdcl⇩W_merge_cp.conflict' cp_confl(1,2) n_s_cp
rtranclp_into_tranclp1)
then show ?thesis using n_s unfolding full_def by auto
qed
next
assume ?fw
then have "cdcl⇩W⇧*⇧* R V" using rtranclp_mono[of cdcl⇩W_merge_stgy "cdcl⇩W⇧*⇧*"]
cdcl⇩W_merge_stgy_rtranclp_cdcl⇩W unfolding full_def by auto
then have inv': "cdcl⇩W_all_struct_inv V" using inv rtranclp_cdcl⇩W_all_struct_inv_inv by blast
have "cdcl⇩W_s'⇧*⇧* R V"
using ‹?fw› by (simp add: full_def inv rtranclp_cdcl⇩W_merge_stgy_rtranclp_cdcl⇩W_s')
moreover have "no_step cdcl⇩W_s' V"
proof cases
assume "conflicting V = None"
then show ?thesis
by (metis inv' ‹full cdcl⇩W_merge_stgy R V› full_def
no_step_cdcl⇩W_merge_stgy_no_step_cdcl⇩W_s')
next
assume confl_V: "conflicting V ≠ None"
then have "no_step cdcl⇩W_bj V"
using rtranclp_cdcl⇩W_merge_stgy_no_step_cdcl⇩W_bj by (meson ‹full cdcl⇩W_merge_stgy R V›
assms(1) full_def)
then show ?thesis using confl_V by (fastforce simp: cdcl⇩W_s'.simps full1_def cdcl⇩W_cp.simps
dest!: tranclpD)
qed
ultimately show ?s' unfolding full_def by blast
qed
lemma full_cdcl⇩W_stgy_full_cdcl⇩W_merge:
assumes
"conflicting R = None" and
inv: "cdcl⇩W_all_struct_inv R"
shows "full cdcl⇩W_stgy R V ⟷ full cdcl⇩W_merge_stgy R V"
by (simp add: assms(1) full_cdcl⇩W_s'_full_cdcl⇩W_merge_restart full_cdcl⇩W_stgy_iff_full_cdcl⇩W_s'
inv)
lemma full_cdcl⇩W_merge_stgy_final_state_conclusive':
fixes S' :: "'st"
assumes full: "full cdcl⇩W_merge_stgy (init_state N) S'"
and no_d: "distinct_mset_mset N"
shows "(conflicting S' = Some {#} ∧ unsatisfiable (set_mset N))
∨ (conflicting S' = None ∧ trail S' ⊨asm N ∧ satisfiable (set_mset N))"
proof -
have "cdcl⇩W_all_struct_inv (init_state N)"
using no_d unfolding cdcl⇩W_all_struct_inv_def by auto
moreover have "conflicting (init_state N) = None"
by auto
ultimately show ?thesis
by (simp add: full full_cdcl⇩W_stgy_final_state_conclusive_from_init_state
full_cdcl⇩W_stgy_full_cdcl⇩W_merge no_d)
qed
end
subsection ‹Adding Restarts›
locale cdcl⇩W_restart =
cdcl⇩W trail init_clss learned_clss backtrack_lvl conflicting cons_trail tl_trail
add_init_cls
add_learned_cls remove_cls update_backtrack_lvl update_conflicting init_state
restart_state
for
trail :: "'st ⇒ ('v, nat, 'v clause) ann_literals" and
init_clss :: "'st ⇒ 'v clauses" and
learned_clss :: "'st ⇒ 'v clauses" and
backtrack_lvl :: "'st ⇒ nat" and
conflicting :: "'st ⇒'v clause option" and
cons_trail :: "('v, nat, 'v clause) ann_literal ⇒ 'st ⇒ 'st" and
tl_trail :: "'st ⇒ 'st" and
add_init_cls :: "'v clause ⇒ 'st ⇒ 'st" and
add_learned_cls remove_cls :: "'v clause ⇒ 'st ⇒ 'st" and
update_backtrack_lvl :: "nat ⇒ 'st ⇒ 'st" and
update_conflicting :: "'v clause option ⇒ 'st ⇒ 'st" and
init_state :: "'v clauses ⇒ 'st" and
restart_state :: "'st ⇒ 'st" +
fixes f :: "nat ⇒ nat"
assumes f: "unbounded f"
begin
text ‹The condition of the differences of cardinality has to be strict.
Otherwise, you could be in a strange state, where nothing remains to do, but a restart is done.
See the proof of well-foundedness.›
inductive cdcl⇩W_merge_with_restart where
restart_step:
"(cdcl⇩W_merge_stgy^^(card (set_mset (learned_clss T)) - card (set_mset (learned_clss S)))) S T
⟹ card (set_mset (learned_clss T)) - card (set_mset (learned_clss S)) > f n
⟹ restart T U ⟹ cdcl⇩W_merge_with_restart (S, n) (U, Suc n)" |
restart_full: "full1 cdcl⇩W_merge_stgy S T ⟹ cdcl⇩W_merge_with_restart (S, n) (T, Suc n)"
lemma "cdcl⇩W_merge_with_restart S T ⟹ cdcl⇩W_merge_restart⇧*⇧* (fst S) (fst T)"
by (induction rule: cdcl⇩W_merge_with_restart.induct)
(auto dest!: relpowp_imp_rtranclp cdcl⇩W_merge_stgy_tranclp_cdcl⇩W_merge tranclp_into_rtranclp
rtranclp_cdcl⇩W_merge_stgy_rtranclp_cdcl⇩W_merge rtranclp_cdcl⇩W_merge_tranclp_cdcl⇩W_merge_restart
fw_r_rf cdcl⇩W_rf.restart
simp: full1_def)
lemma cdcl⇩W_merge_with_restart_rtranclp_cdcl⇩W:
"cdcl⇩W_merge_with_restart S T ⟹ cdcl⇩W⇧*⇧* (fst S) (fst T)"
by (induction rule: cdcl⇩W_merge_with_restart.induct)
(auto dest!: relpowp_imp_rtranclp rtranclp_cdcl⇩W_merge_stgy_rtranclp_cdcl⇩W cdcl⇩W.rf
cdcl⇩W_rf.restart tranclp_into_rtranclp simp: full1_def)
lemma cdcl⇩W_merge_with_restart_increasing_number:
"cdcl⇩W_merge_with_restart S T ⟹ snd T = 1 + snd S"
by (induction rule: cdcl⇩W_merge_with_restart.induct) auto
lemma "full1 cdcl⇩W_merge_stgy S T ⟹ cdcl⇩W_merge_with_restart (S, n) (T, Suc n)"
using restart_full by blast
lemma cdcl⇩W_all_struct_inv_learned_clss_bound:
assumes inv: "cdcl⇩W_all_struct_inv S"
shows "set_mset (learned_clss S) ⊆ simple_clss (atms_of_msu (init_clss S))"
proof
fix C
assume C: "C ∈ set_mset (learned_clss S)"
have "distinct_mset C"
using C inv unfolding cdcl⇩W_all_struct_inv_def distinct_cdcl⇩W_state_def distinct_mset_set_def
by auto
moreover have "¬tautology C"
using C inv unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_learned_clause_def by auto
moreover
have "atms_of C ⊆ atms_of_msu (learned_clss S)"
using C by auto
then have "atms_of C ⊆ atms_of_msu (init_clss S)"
using inv unfolding cdcl⇩W_all_struct_inv_def no_strange_atm_def by force
moreover have "finite (atms_of_msu (init_clss S))"
using inv unfolding cdcl⇩W_all_struct_inv_def by auto
ultimately show "C ∈ simple_clss (atms_of_msu (init_clss S))"
using distinct_mset_not_tautology_implies_in_simple_clss simple_clss_mono
by blast
qed
lemma cdcl⇩W_merge_with_restart_init_clss:
"cdcl⇩W_merge_with_restart S T ⟹ cdcl⇩W_M_level_inv (fst S) ⟹
init_clss (fst S) = init_clss (fst T)"
using cdcl⇩W_merge_with_restart_rtranclp_cdcl⇩W rtranclp_cdcl⇩W_init_clss by blast
lemma
"wf {(T, S). cdcl⇩W_all_struct_inv (fst S) ∧ cdcl⇩W_merge_with_restart S T}"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain g where
g: "⋀i. cdcl⇩W_merge_with_restart (g i) (g (Suc i))" and
inv: "⋀i. cdcl⇩W_all_struct_inv (fst (g i))"
unfolding wf_iff_no_infinite_down_chain by fast
{ fix i
have "init_clss (fst (g i)) = init_clss (fst (g 0))"
apply (induction i)
apply simp
using g inv unfolding cdcl⇩W_all_struct_inv_def by (metis cdcl⇩W_merge_with_restart_init_clss)
} note init_g = this
let ?S = "g 0"
have "finite (atms_of_msu (init_clss (fst ?S)))"
using inv unfolding cdcl⇩W_all_struct_inv_def by auto
have snd_g: "⋀i. snd (g i) = i + snd (g 0)"
apply (induct_tac i)
apply simp
by (metis Suc_eq_plus1_left add_Suc cdcl⇩W_merge_with_restart_increasing_number g)
then have snd_g_0: "⋀i. i > 0 ⟹ snd (g i) = i + snd (g 0)"
by blast
have unbounded_f_g: "unbounded (λi. f (snd (g i)))"
using f unfolding bounded_def by (metis add.commute f less_or_eq_imp_le snd_g
not_bounded_nat_exists_larger not_le le_iff_add)
obtain k where
f_g_k: "f (snd (g k)) > card (simple_clss (atms_of_msu (init_clss (fst ?S))))" and
"k > card (simple_clss (atms_of_msu (init_clss (fst ?S))))"
using not_bounded_nat_exists_larger[OF unbounded_f_g] by blast
text ‹The following does not hold anymore with the non-strict version of
cardinality in the definition.›
{ fix i
assume "no_step cdcl⇩W_merge_stgy (fst (g i))"
with g[of i]
have False
proof (induction rule: cdcl⇩W_merge_with_restart.induct)
case (restart_step T S n) note H = this(1) and c = this(2) and n_s = this(4)
obtain S' where "cdcl⇩W_merge_stgy S S'"
using H c by (metis gr_implies_not0 relpowp_E2)
then show False using n_s by auto
next
case (restart_full S T)
then show False unfolding full1_def by (auto dest: tranclpD)
qed
} note H = this
obtain m T where
m: "m = card (set_mset (learned_clss T)) - card (set_mset (learned_clss (fst (g k))))" and
"m > f (snd (g k))" and
"restart T (fst (g (k+1)))" and
cdcl⇩W_merge_stgy: "(cdcl⇩W_merge_stgy ^^ m) (fst (g k)) T"
using g[of k] H[of "Suc k"] by (force simp: cdcl⇩W_merge_with_restart.simps full1_def)
have "cdcl⇩W_merge_stgy⇧*⇧* (fst (g k)) T"
using cdcl⇩W_merge_stgy relpowp_imp_rtranclp by metis
then have "cdcl⇩W_all_struct_inv T"
using inv[of k] rtranclp_cdcl⇩W_all_struct_inv_inv rtranclp_cdcl⇩W_merge_stgy_rtranclp_cdcl⇩W
by blast
moreover have "card (set_mset (learned_clss T)) - card (set_mset (learned_clss (fst (g k))))
> card (simple_clss (atms_of_msu (init_clss (fst ?S))))"
unfolding m[symmetric] using ‹m > f (snd (g k))› f_g_k by linarith
then have "card (set_mset (learned_clss T))
> card (simple_clss (atms_of_msu (init_clss (fst ?S))))"
by linarith
moreover
have "init_clss (fst (g k)) = init_clss T"
using ‹cdcl⇩W_merge_stgy⇧*⇧* (fst (g k)) T› rtranclp_cdcl⇩W_merge_stgy_rtranclp_cdcl⇩W
rtranclp_cdcl⇩W_init_clss inv unfolding cdcl⇩W_all_struct_inv_def by blast
then have "init_clss (fst ?S) = init_clss T"
using init_g[of k] by auto
ultimately show False
using cdcl⇩W_all_struct_inv_learned_clss_bound
by (simp add: ‹finite (atms_of_msu (init_clss (fst (g 0))))› simple_clss_finite
card_mono leD)
qed
lemma cdcl⇩W_merge_with_restart_distinct_mset_clauses:
assumes invR: "cdcl⇩W_all_struct_inv (fst R)" and
st: "cdcl⇩W_merge_with_restart R S" and
dist: "distinct_mset (clauses (fst R))" and
R: "trail (fst R) = []"
shows "distinct_mset (clauses (fst S))"
using assms(2,1,3,4)
proof (induction)
case (restart_full S T)
then show ?case using rtranclp_cdcl⇩W_merge_stgy_distinct_mset_clauses[of S T] unfolding full1_def
by (auto dest: tranclp_into_rtranclp)
next
case (restart_step T S n U)
then have "distinct_mset (clauses T)"
using rtranclp_cdcl⇩W_merge_stgy_distinct_mset_clauses[of S T] unfolding full1_def
by (auto dest: relpowp_imp_rtranclp)
then show ?case using ‹restart T U› by (metis clauses_restart distinct_mset_union fstI
mset_le_exists_conv restart.cases state_eq_clauses)
qed
inductive cdcl⇩W_with_restart where
restart_step:
"(cdcl⇩W_stgy^^(card (set_mset (learned_clss T)) - card (set_mset (learned_clss S)))) S T ⟹
card (set_mset (learned_clss T)) - card (set_mset (learned_clss S)) > f n ⟹
restart T U ⟹
cdcl⇩W_with_restart (S, n) (U, Suc n)" |
restart_full: "full1 cdcl⇩W_stgy S T ⟹ cdcl⇩W_with_restart (S, n) (T, Suc n)"
lemma cdcl⇩W_with_restart_rtranclp_cdcl⇩W:
"cdcl⇩W_with_restart S T ⟹ cdcl⇩W⇧*⇧* (fst S) (fst T)"
apply (induction rule: cdcl⇩W_with_restart.induct)
by (auto dest!: relpowp_imp_rtranclp tranclp_into_rtranclp fw_r_rf
cdcl⇩W_rf.restart rtranclp_cdcl⇩W_stgy_rtranclp_cdcl⇩W cdcl⇩W_merge_restart_cdcl⇩W
simp: full1_def)
lemma cdcl⇩W_with_restart_increasing_number:
"cdcl⇩W_with_restart S T ⟹ snd T = 1 + snd S"
by (induction rule: cdcl⇩W_with_restart.induct) auto
lemma "full1 cdcl⇩W_stgy S T ⟹ cdcl⇩W_with_restart (S, n) (T, Suc n)"
using restart_full by blast
lemma cdcl⇩W_with_restart_init_clss:
"cdcl⇩W_with_restart S T ⟹ cdcl⇩W_M_level_inv (fst S) ⟹ init_clss (fst S) = init_clss (fst T)"
using cdcl⇩W_with_restart_rtranclp_cdcl⇩W rtranclp_cdcl⇩W_init_clss by blast
lemma
"wf {(T, S). cdcl⇩W_all_struct_inv (fst S) ∧ cdcl⇩W_with_restart S T}"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain g where
g: "⋀i. cdcl⇩W_with_restart (g i) (g (Suc i))" and
inv: "⋀i. cdcl⇩W_all_struct_inv (fst (g i))"
unfolding wf_iff_no_infinite_down_chain by fast
{ fix i
have "init_clss (fst (g i)) = init_clss (fst (g 0))"
apply (induction i)
apply simp
using g inv unfolding cdcl⇩W_all_struct_inv_def by (metis cdcl⇩W_with_restart_init_clss)
} note init_g = this
let ?S = "g 0"
have "finite (atms_of_msu (init_clss (fst ?S)))"
using inv unfolding cdcl⇩W_all_struct_inv_def by auto
have snd_g: "⋀i. snd (g i) = i + snd (g 0)"
apply (induct_tac i)
apply simp
by (metis Suc_eq_plus1_left add_Suc cdcl⇩W_with_restart_increasing_number g)
then have snd_g_0: "⋀i. i > 0 ⟹ snd (g i) = i + snd (g 0)"
by blast
have unbounded_f_g: "unbounded (λi. f (snd (g i)))"
using f unfolding bounded_def by (metis add.commute f less_or_eq_imp_le snd_g
not_bounded_nat_exists_larger not_le le_iff_add)
obtain k where
f_g_k: "f (snd (g k)) > card (simple_clss (atms_of_msu (init_clss (fst ?S))))" and
"k > card (simple_clss (atms_of_msu (init_clss (fst ?S))))"
using not_bounded_nat_exists_larger[OF unbounded_f_g] by blast
text ‹The following does not hold anymore with the non-strict version of
cardinality in the definition.›
{ fix i
assume "no_step cdcl⇩W_stgy (fst (g i))"
with g[of i]
have False
proof (induction rule: cdcl⇩W_with_restart.induct)
case (restart_step T S n) note H = this(1) and c = this(2) and n_s = this(4)
obtain S' where "cdcl⇩W_stgy S S'"
using H c by (metis gr_implies_not0 relpowp_E2)
then show False using n_s by auto
next
case (restart_full S T)
then show False unfolding full1_def by (auto dest: tranclpD)
qed
} note H = this
obtain m T where
m: "m = card (set_mset (learned_clss T)) - card (set_mset (learned_clss (fst (g k))))" and
"m > f (snd (g k))" and
"restart T (fst (g (k+1)))" and
cdcl⇩W_merge_stgy: "(cdcl⇩W_stgy ^^ m) (fst (g k)) T"
using g[of k] H[of "Suc k"] by (force simp: cdcl⇩W_with_restart.simps full1_def)
have "cdcl⇩W_stgy⇧*⇧* (fst (g k)) T"
using cdcl⇩W_merge_stgy relpowp_imp_rtranclp by metis
then have "cdcl⇩W_all_struct_inv T"
using inv[of k] rtranclp_cdcl⇩W_all_struct_inv_inv rtranclp_cdcl⇩W_stgy_rtranclp_cdcl⇩W by blast
moreover have "card (set_mset (learned_clss T)) - card (set_mset (learned_clss (fst (g k))))
> card (simple_clss (atms_of_msu (init_clss (fst ?S))))"
unfolding m[symmetric] using ‹m > f (snd (g k))› f_g_k by linarith
then have "card (set_mset (learned_clss T))
> card (simple_clss (atms_of_msu (init_clss (fst ?S))))"
by linarith
moreover
have "init_clss (fst (g k)) = init_clss T"
using ‹cdcl⇩W_stgy⇧*⇧* (fst (g k)) T› rtranclp_cdcl⇩W_stgy_rtranclp_cdcl⇩W rtranclp_cdcl⇩W_init_clss
inv unfolding cdcl⇩W_all_struct_inv_def
by blast
then have "init_clss (fst ?S) = init_clss T"
using init_g[of k] by auto
ultimately show False
using cdcl⇩W_all_struct_inv_learned_clss_bound
by (simp add: ‹finite (atms_of_msu (init_clss (fst (g 0))))› simple_clss_finite
card_mono leD)
qed
lemma cdcl⇩W_with_restart_distinct_mset_clauses:
assumes invR: "cdcl⇩W_all_struct_inv (fst R)" and
st: "cdcl⇩W_with_restart R S" and
dist: "distinct_mset (clauses (fst R))" and
R: "trail (fst R) = []"
shows "distinct_mset (clauses (fst S))"
using assms(2,1,3,4)
proof (induction)
case (restart_full S T)
then show ?case using rtranclp_cdcl⇩W_stgy_distinct_mset_clauses[of S T] unfolding full1_def
by (auto dest: tranclp_into_rtranclp)
next
case (restart_step T S n U)
then have "distinct_mset (clauses T)" using rtranclp_cdcl⇩W_stgy_distinct_mset_clauses[of S T]
unfolding full1_def by (auto dest: relpowp_imp_rtranclp)
then show ?case using ‹restart T U› by (metis clauses_restart distinct_mset_union fstI
mset_le_exists_conv restart.cases state_eq_clauses)
qed
end
locale luby_sequence =
fixes ur :: nat
assumes "ur > 0"
begin
lemma exists_luby_decomp:
fixes i ::nat
shows "∃k::nat. (2 ^ (k - 1) ≤ i ∧ i < 2 ^ k - 1) ∨ i = 2 ^ k - 1"
proof (induction i)
case 0
then show ?case
by (rule exI[of _ 0], simp)
next
case (Suc n)
then obtain k where "2 ^ (k - 1) ≤ n ∧ n < 2 ^ k - 1 ∨ n = 2 ^ k - 1"
by blast
then consider
(st_interv) "2 ^ (k - 1) ≤ n" and "n ≤ 2 ^ k - 2"
| (end_interv) "2 ^ (k - 1) ≤ n" and "n = 2 ^ k - 2"
| (pow2) "n = 2 ^ k - 1"
by linarith
then show ?case
proof cases
case st_interv
then show ?thesis apply - apply (rule exI[of _ k])
by (metis (no_types, lifting) One_nat_def Suc_diff_Suc Suc_lessI
‹2 ^ (k - 1) ≤ n ∧ n < 2 ^ k - 1 ∨ n = 2 ^ k - 1› diff_self_eq_0
dual_order.trans le_SucI le_imp_less_Suc numeral_2_eq_2 one_le_numeral
one_le_power zero_less_numeral zero_less_power)
next
case end_interv
then show ?thesis apply - apply (rule exI[of _ k]) by auto
next
case pow2
then show ?thesis apply - apply (rule exI[of _ "k+1"]) by auto
qed
qed
text ‹Luby sequences are defined by:
▪ @{term "(2::nat)^(k::nat)- 1"}, if @{term "i = 2^k - 1"}
▪ @{term "luby_sequence_core (i - (2::nat)^(k - 1) + 1)"}, if @{term "2^(k - 1) ≤ i"} and
@{term "i ≤ 2^k - 1"}
Then the sequence is then scaled by a constant unit run (called @{term ur} here), strictly positive.
›
function luby_sequence_core :: "nat ⇒ nat" where
"luby_sequence_core i =
(if ∃k. i = 2^k - 1
then 2^((SOME k. i = 2^k - 1) - 1)
else luby_sequence_core (i - 2^((SOME k. 2^(k-1)≤ i ∧ i < 2^k - 1) - 1) + 1))"
by auto
termination
proof (relation "less_than", goal_cases)
case 1
then show ?case by auto
next
case (2 i)
let ?k = "(SOME k. 2 ^ (k - 1) ≤ i ∧ i < 2 ^ k - 1)"
have "2 ^ (?k - 1) ≤ i ∧ i < 2 ^ ?k - 1"
apply (rule someI_ex)
using "2" exists_luby_decomp by blast
then show ?case
proof -
have "∀n na. ¬ (1::nat) ≤ n ∨ 1 ≤ n ^ na"
by (meson one_le_power)
then have f1: "(1::nat) ≤ 2 ^ (?k - 1)"
using one_le_numeral by blast
have f2: "i - 2 ^ (?k - 1) + 2 ^ (?k - 1) = i"
using ‹2 ^ (?k - 1) ≤ i ∧ i < 2 ^ ?k - 1› le_add_diff_inverse2 by blast
have f3: "2 ^ ?k - 1 ≠ Suc 0"
using f1 ‹2 ^ (?k - 1) ≤ i ∧ i < 2 ^ ?k - 1› by linarith
have "2 ^ ?k - (1::nat) ≠ 0"
using ‹2 ^ (?k - 1) ≤ i ∧ i < 2 ^ ?k - 1› gr_implies_not0 by blast
then have f4: "2 ^ ?k ≠ (1::nat)"
by linarith
have f5: "∀n na. if na = 0 then (n::nat) ^ na = 1 else n ^ na = n * n ^ (na - 1)"
by (simp add: power_eq_if)
then have "?k ≠ 0"
using f4 by meson
then have "2 ^ (?k - 1) ≠ Suc 0"
using f5 f3 by presburger
then have "Suc 0 < 2 ^ (?k - 1)"
using f1 by linarith
then show ?thesis
using f2 less_than_iff by presburger
qed
qed
declare luby_sequence_core.simps[simp del]
lemma two_pover_n_eq_two_power_n'_eq:
assumes H: "(2::nat) ^ (k::nat) - 1 = 2 ^ k' - 1"
shows "k' = k"
proof -
have "(2::nat) ^ (k::nat) = 2 ^ k'"
using H by (metis One_nat_def Suc_pred zero_less_numeral zero_less_power)
then show ?thesis by simp
qed
lemma luby_sequence_core_two_power_minus_one:
"luby_sequence_core (2^k - 1) = 2^(k-1)" (is "?L = ?K")
proof -
have decomp: "∃ka. 2 ^ k - 1 = 2 ^ ka - 1"
by auto
have "?L = 2^((SOME k'. (2::nat)^k - 1 = 2^k' - 1) - 1)"
apply (subst luby_sequence_core.simps, subst decomp)
by simp
moreover have "(SOME k'. (2::nat)^k - 1 = 2^k' - 1) = k"
apply (rule some_equality)
apply simp
using two_pover_n_eq_two_power_n'_eq by blast
ultimately show ?thesis by presburger
qed
lemma different_luby_decomposition_false:
assumes
H: "2 ^ (k - Suc 0) ≤ i" and
k': "i < 2 ^ k' - Suc 0" and
k_k': "k > k'"
shows "False"
proof -
have "2 ^ k' - Suc 0 < 2 ^ (k - Suc 0)"
using k_k' less_eq_Suc_le by auto
then show ?thesis
using H k' by linarith
qed
lemma luby_sequence_core_not_two_power_minus_one:
assumes
k_i: "2 ^ (k - 1) ≤ i" and
i_k: "i < 2^ k - 1"
shows "luby_sequence_core i = luby_sequence_core (i - 2 ^ (k - 1) + 1)"
proof -
have H: "¬ (∃ka. i = 2 ^ ka - 1)"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain k'::nat where k': "i = 2 ^ k' - 1" by blast
have "(2::nat) ^ k' - 1 < 2 ^ k - 1"
using i_k unfolding k' .
then have "(2::nat) ^ k' < 2 ^ k"
by linarith
then have "k' < k"
by simp
have "2 ^ (k - 1) ≤ 2 ^ k' - (1::nat)"
using k_i unfolding k' .
then have "(2::nat) ^ (k-1) < 2 ^ k'"
by (metis Suc_diff_1 not_le not_less_eq zero_less_numeral zero_less_power)
then have "k-1 < k'"
by simp
show False using ‹k' < k› ‹k-1 < k'› by linarith
qed
have "⋀k k'. 2 ^ (k - Suc 0) ≤ i ⟹ i < 2 ^ k - Suc 0 ⟹ 2 ^ (k' - Suc 0) ≤ i ⟹
i < 2 ^ k' - Suc 0 ⟹ k = k'"
by (meson different_luby_decomposition_false linorder_neqE_nat)
then have k: "(SOME k. 2 ^ (k - Suc 0) ≤ i ∧ i < 2 ^ k - Suc 0) = k"
using k_i i_k by auto
show ?thesis
apply (subst luby_sequence_core.simps[of i], subst H)
by (simp add: k)
qed
lemma unbounded_luby_sequence_core: "unbounded luby_sequence_core"
unfolding bounded_def
proof
assume "∃b. ∀n. luby_sequence_core n ≤ b"
then obtain b where b: "⋀n. luby_sequence_core n ≤ b"
by metis
have "luby_sequence_core (2^(b+1) - 1) = 2^b"
using luby_sequence_core_two_power_minus_one[of "b+1"] by simp
moreover have "(2::nat)^b > b"
by (induction b) auto
ultimately show False using b[of "2^(b+1) - 1"] by linarith
qed
abbreviation luby_sequence :: "nat ⇒ nat" where
"luby_sequence n ≡ ur * luby_sequence_core n"
lemma bounded_luby_sequence: "unbounded luby_sequence"
using bounded_const_product[of ur] luby_sequence_axioms
luby_sequence_def unbounded_luby_sequence_core by blast
lemma luby_sequence_core_0: "luby_sequence_core 0 = 1"
proof -
have 0: "(0::nat) = 2^0-1"
by auto
show ?thesis
by (subst 0, subst luby_sequence_core_two_power_minus_one) simp
qed
lemma "luby_sequence_core n ≥ 1"
proof (induction n rule: nat_less_induct_case)
case 0
then show ?case by (simp add: luby_sequence_core_0)
next
case (Suc n) note IH = this
consider
(interv) k where "2 ^ (k - 1) ≤ Suc n" and "Suc n < 2 ^ k - 1"
| (pow2) k where "Suc n = 2 ^ k - Suc 0"
using exists_luby_decomp[of "Suc n"] by auto
then show ?case
proof cases
case pow2
show ?thesis
using luby_sequence_core_two_power_minus_one pow2 by auto
next
case interv
have n: "Suc n - 2 ^ (k - 1) + 1 < Suc n"
by (metis Suc_1 Suc_eq_plus1 add.commute add_diff_cancel_left' add_less_mono1 gr0I
interv(1) interv(2) le_add_diff_inverse2 less_Suc_eq not_le power_0 power_one_right
power_strict_increasing_iff)
show ?thesis
apply (subst luby_sequence_core_not_two_power_minus_one[OF interv])
using IH n by auto
qed
qed
end
locale luby_sequence_restart =
luby_sequence ur +
cdcl⇩W trail init_clss learned_clss backtrack_lvl conflicting cons_trail tl_trail
add_init_cls
add_learned_cls remove_cls update_backtrack_lvl update_conflicting init_state
restart_state
for
ur :: nat and
trail :: "'st ⇒ ('v, nat, 'v clause) ann_literals" and
init_clss :: "'st ⇒ 'v clauses" and
learned_clss :: "'st ⇒ 'v clauses" and
backtrack_lvl :: "'st ⇒ nat" and
conflicting :: "'st ⇒'v clause option" and
cons_trail :: "('v, nat, 'v clause) ann_literal ⇒ 'st ⇒ 'st" and
tl_trail :: "'st ⇒ 'st" and
add_init_cls :: "'v clause ⇒ 'st ⇒ 'st" and
add_learned_cls remove_cls :: "'v clause ⇒ 'st ⇒ 'st" and
update_backtrack_lvl :: "nat ⇒ 'st ⇒ 'st" and
update_conflicting :: "'v clause option ⇒ 'st ⇒ 'st" and
init_state :: "'v clauses ⇒ 'st" and
restart_state :: "'st ⇒ 'st"
begin
sublocale cdcl⇩W_restart _ _ _ _ _ _ _ _ _ _ _ _ _ _ luby_sequence
apply unfold_locales
using bounded_luby_sequence by blast
end
end