# Theory Correct_Termination

```theory Correct_Termination
imports SCL_FOL
begin

context scl_fol_calculus begin

lemma not_satisfiable_if_sound_state_conflict_bottom:
assumes sound_S: "sound_state N β S" and conflict_S: "state_conflict S = Some ({#}, γ)"
shows "¬ satisfiable (grounding_of_clss (fset N))"
proof -
from sound_S conflict_S have "fset N ⊫𝒢e {{#}}"
unfolding sound_state_def state_conflict_def by auto
thus ?thesis by simp
qed

lemma propagate_if_conflict_follows_decide:
assumes
trail_lt_β: "trail_atoms_lt β S⇩2" and
no_conf: "∄S⇩1. conflict N β S⇩0 S⇩1" and deci: "decide N β S⇩0 S⇩2" and conf: "conflict N β S⇩2 S⇩3"
shows "∃S⇩4. propagate N β S⇩0 S⇩4"
proof -
from deci obtain L γ Γ U where
S⇩0_def: "S⇩0 = (Γ, U, None)" and
S⇩2_def: "S⇩2 = (trail_decide Γ (L ⋅l γ), U, None)" and
"L ∈ ⋃ (set_mset ` fset N)" and
"is_ground_lit (L ⋅l γ)" and
"¬ trail_defined_lit Γ (L ⋅l γ)" and
"atm_of L ⋅a γ ≼⇩B β"
by (elim decide.cases) blast

from conf S⇩2_def obtain D γ⇩D where
S⇩3_def: "S⇩3 = (trail_decide Γ (L ⋅l γ), U, Some (D, γ⇩D))" and
D_in: "D |∈| N |∪| U" and
ground_D_σ: "is_ground_cls (D ⋅ γ⇩D)" and
tr_Γ_L_false_D: "trail_false_cls (trail_decide Γ (L ⋅l γ)) (D ⋅ γ⇩D)"
by (auto elim: conflict.cases)

have "vars_cls D ⊆ subst_domain γ⇩D"
using ground_D_σ vars_cls_subset_subst_domain_if_grounding by blast

moreover have "¬ trail_false_cls Γ (D ⋅ γ⇩D)"
using not_trail_false_ground_cls_if_no_conflict[OF no_conf] D_in
by (simp add: S⇩0_def ground_D_σ)

ultimately have "- (L ⋅l γ) ∈# D ⋅ γ⇩D"
using tr_Γ_L_false_D
by (metis subtrail_falseI decide_lit_def)

then obtain D' L' where D_def: "D = add_mset L' D'" and "- (L ⋅l γ) = L' ⋅l γ⇩D"
by (metis Melem_subst_cls multi_member_split)

define C⇩0 where
"C⇩0 = {#K ∈# D'. K ⋅l γ⇩D ≠ L' ⋅l γ⇩D#}"

define C⇩1 where
"C⇩1 = {#K ∈# D'. K ⋅l γ⇩D = L' ⋅l γ⇩D#}"

have ball_atms_lt_β: "∀K ∈# D ⋅ γ⇩D. atm_of K ≼⇩B β"
proof (rule ballI)
fix K assume "K ∈# D ⋅ γ⇩D"
hence "K = L' ⋅l γ⇩D ∨ (K ∈# D' ⋅ γ⇩D)"
by (simp add: D_def)
thus "atm_of K ≼⇩B β"
proof (rule disjE)
assume "K = L' ⋅l γ⇩D"
thus ?thesis
using ‹- (L ⋅l γ) = L' ⋅l γ⇩D› ‹atm_of L ⋅a γ ≼⇩B β›
by (metis  atm_of_eq_uminus_if_lit_eq atm_of_subst_lit)
next
have trail_lt_β': "∀A ∈ atm_of ` fst ` set (trail_decide Γ (L ⋅l γ)). A ≼⇩B β"
using trail_lt_β by (simp add: trail_atoms_lt_def S⇩2_def)

assume K_in: "K ∈# D' ⋅ γ⇩D"
hence "atm_of K ∈ atm_of ` fst ` set (trail_decide Γ (L ⋅l γ))"
using tr_Γ_L_false_D[unfolded D_def]
by (metis D_def ‹K ∈# D ⋅ γ⇩D› atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set
trail_false_cls_def trail_false_lit_def)
moreover from trail_lt_β have "∀A ∈ atm_of ` fst ` set (trail_decide Γ (L ⋅l γ)). A ≼⇩B β"
by (simp add: trail_atoms_lt_def S⇩2_def)
ultimately show ?thesis
by blast
qed
qed

have tr_false_C⇩1: "trail_false_cls Γ (C⇩0 ⋅ γ⇩D)"
proof (rule subtrail_falseI)
show "trail_false_cls ((L ⋅l γ, None) # Γ) (C⇩0 ⋅ γ⇩D)"
unfolding C⇩0_def trail_false_cls_def
apply (rule ballI)
apply (rule tr_Γ_L_false_D[unfolded D_def trail_false_cls_def decide_lit_def, rule_format])
by auto
next
show "- (L ⋅l γ) ∉# C⇩0 ⋅ γ⇩D"
unfolding C⇩0_def
using ‹- (L ⋅l γ) = L' ⋅l γ⇩D› by fastforce
qed

have not_def_L'_ρ_σ⇩ρ: "¬ trail_defined_lit Γ (L' ⋅l γ⇩D)"
using ‹¬ trail_defined_lit Γ (L ⋅l γ)›
by (metis ‹- (L ⋅l γ) = L' ⋅l γ⇩D› trail_defined_lit_iff_defined_uminus)

obtain xs where "mset xs = add_mset L' C⇩1"
using ex_mset by auto
hence set_xs_conv:
"set xs = set_mset (add_mset L' C⇩1)"
by (metis set_mset_mset)

have "unifiers (set (pairs (map atm_of xs))) ≠ {}"
proof (rule not_empty_if_mem)
have "set (pairs (map atm_of xs)) =
atm_of ` set_mset (add_mset L' C⇩1) × atm_of ` set_mset (add_mset L' C⇩1)"
unfolding set_pairs list.set_map set_xs_conv by simp
also have "… =
atm_of ` insert L' (set_mset C⇩1) × atm_of ` insert L' (set_mset C⇩1)"
unfolding set_mset_add_mset_insert by simp
also have "… =
atm_of ` insert L' {K. K ∈# D' ∧ K ⋅l γ⇩D = L' ⋅l γ⇩D} ×
atm_of ` insert L' {K. K ∈# D' ∧ K ⋅l γ⇩D = L' ⋅l γ⇩D}"
unfolding C⇩1_def set_mset_filter by simp
finally have set_pairs_xs_simp: "set (pairs (map atm_of xs)) =
atm_of ` insert L' {K. K ∈# D' ∧ K ⋅l γ⇩D = L' ⋅l γ⇩D} ×
atm_of ` insert L' {K. K ∈# D' ∧ K ⋅l γ⇩D = L' ⋅l γ⇩D}"
by assumption

show "γ⇩D ∈ unifiers (set (pairs (map atm_of xs)))"
unfolding unifiers_def mem_Collect_eq
proof (rule ballI)
fix p assume p_in: "p ∈ set (pairs (map atm_of xs))"
then obtain K1 K2 where p_def: "p = (atm_of K1, atm_of K2)" and
"K1 = L' ∨ K1 ∈ {K. K ∈# D' ∧ K ⋅l γ⇩D = L' ⋅l γ⇩D}" and
"K2 = L' ∨ K2 ∈ {K. K ∈# D' ∧ K ⋅l γ⇩D = L' ⋅l γ⇩D}"
by (auto simp: set_pairs_xs_simp)
hence "K1 ⋅l γ⇩D = L' ⋅l γ⇩D ∧ K2 ⋅l γ⇩D = L' ⋅l γ⇩D"
by auto
thus "fst p ⋅a γ⇩D = snd p ⋅a γ⇩D"
unfolding p_def prod.sel
by (metis atm_of_subst_lit)
qed
qed
then obtain ys where
unify_pairs: "unify (pairs (map atm_of xs)) [] = Some ys"
using ex_unify_if_unifiers_not_empty[OF _ refl] by blast

define μ where
"μ = subst_of ys"

have imgu_μ: "is_imgu μ {atm_of ` set_mset (add_mset L' C⇩1)}"
proof (intro is_imgu_if_mgu_sets[unfolded mgu_sets_def] exI conjI)
show "set (map set [(map atm_of xs)]) = {atm_of ` set_mset (add_mset L' C⇩1)}"
by (simp add: set_xs_conv)
next
show "map_option subst_of (unify (concat (map pairs [map atm_of xs])) []) = Some μ"
by (simp add: unify_pairs μ_def)
qed

show ?thesis
using propagateI[OF D_in D_def, of γ⇩D, unfolded subst_cls_comp_subst subst_lit_comp_subst,
OF ground_D_σ ball_atms_lt_β C⇩0_def C⇩1_def tr_false_C⇩1 not_def_L'_ρ_σ⇩ρ imgu_μ]
unfolding S⇩0_def by blast
qed

theorem correct_termination:
fixes gnd_N and gnd_N_lt_β
assumes
sound_S: "sound_state N β S" and
invars: "trail_atoms_lt β S" "trail_propagated_wf (state_trail S)" "trail_lits_consistent S"
"ground_false_closures S" and
no_new_conflict: "∄S'. conflict N β S S'" and
no_new_propagate: "∄S'. propagate N β S S'" and
no_new_decide: "∄S'. decide N β S S' ∧ (∄S''. conflict N β S' S'')" and
no_new_skip: "∄S'. skip N β S S'" and
no_new_resolve: "∄S'. resolve N β S S'" and
no_new_backtrack: "∄S'. backtrack N β S S' ∧
is_shortest_backtrack (fst (the (state_conflict S))) (state_trail S) (state_trail S')"
defines
"gnd_N ≡ grounding_of_clss (fset N)" and
"gnd_N_lt_β ≡ {C ∈ gnd_N. ∀L ∈# C. atm_of L ≼⇩B β}"
shows "¬ satisfiable gnd_N ∧ (∃γ. state_conflict S = Some ({#}, γ)) ∨
satisfiable gnd_N_lt_β ∧ trail_true_clss (state_trail S) gnd_N_lt_β"
proof -
obtain Γ U u where S_def: "S = (Γ, U, u)"
using prod_cases3 by blast

from sound_S have sound_Γ: "sound_trail N Γ"
by (simp_all add: S_def sound_state_def)

from ‹ground_false_closures S› have "ground_closures S"
by (simp add: ground_false_closures_def)

have trail_consistent: "trail_consistent (state_trail S)"
using ‹trail_lits_consistent S› by (simp add: trail_lits_consistent_def)

show ?thesis
proof (cases u)
case u_def: None
hence "state_conflict S = None"
by (simp add: S_def)

have tr_true: "trail_true_clss Γ gnd_N_lt_β"
unfolding trail_true_clss_def gnd_N_lt_β_def gnd_N_def
proof (rule ballI, unfold mem_Collect_eq, erule conjE)
fix C assume C_in: "C ∈ grounding_of_clss (fset N)" and C_lt_β: "∀L ∈# C. atm_of L ≼⇩B β"

from C_in have "is_ground_cls C"
by (rule grounding_ground)

from C_in obtain C' γ where C'_in: "C' |∈| N" and C_def: "C = C' ⋅ γ"
unfolding grounding_of_clss_def grounding_of_cls_def
by (smt (verit, ccfv_threshold) UN_iff mem_Collect_eq)

from no_new_decide have Γ_defined_C: "trail_defined_cls Γ C"
proof (rule contrapos_np)
assume "¬ trail_defined_cls Γ C"
then obtain L where L_in: "L ∈# C" and "¬ trail_defined_lit Γ L"
using trail_defined_cls_def by blast
then obtain L' where L'_in: "L' ∈# C'" and "L = L' ⋅l γ"
using C_def Melem_subst_cls by blast

have deci: "decide N β (Γ, U, None) (trail_decide Γ (L' ⋅l γ), U, None)"
proof (rule decideI)
show "L' ∈ ⋃ (set_mset ` fset N)"
using C'_in L'_in
by (meson UN_I)
next
show "is_ground_lit (L' ⋅l γ)"
using L_in ‹L = L' ⋅l γ› ‹is_ground_cls C› is_ground_cls_def by blast
next
show "¬ trail_defined_lit Γ (L' ⋅l γ)"
using ‹L = L' ⋅l γ› ‹¬ trail_defined_lit Γ L› by blast
next
show "atm_of L' ⋅a γ ≼⇩B β"
using ‹L = L' ⋅l γ› C_lt_β L_in by fastforce
qed

moreover have "∄S''. conflict N β (trail_decide Γ (L' ⋅l γ), U, None) S''"
proof (rule notI, elim exE)
fix S''
assume conf: "conflict N β (trail_decide Γ (L' ⋅l γ), U, None) S''"
moreover have "trail_atoms_lt β (trail_decide Γ (L' ⋅l γ), U, None)"
using decide_preserves_trail_atoms_lt[OF deci] ‹trail_atoms_lt β S›
by (simp add: S_def u_def)
ultimately have "∃S⇩4. propagate N β S S⇩4"
using propagate_if_conflict_follows_decide[OF _ no_new_conflict]
using S_def deci u_def by blast
with no_new_propagate show False
by metis
qed

ultimately show "∃S'. decide N β S S' ∧ (∄S''. conflict N β S' S'')"
by (auto simp : S_def u_def)
qed

show "trail_true_cls Γ C"
using Γ_defined_C[THEN trail_true_or_false_cls_if_defined]
proof (elim disjE)
show "trail_true_cls Γ C ⟹ trail_true_cls Γ C"
by assumption
next
assume "trail_false_cls Γ C"

define ρ :: "'v ⇒ ('f, 'v) term" where
"ρ = renaming_wrt (fset (N |∪| U |∪| clss_of_trail Γ))"

define γ⇩ρ where
"γ⇩ρ = rename_subst_domain ρ (restrict_subst_domain (vars_cls C') γ)"

have "conflict N β (Γ, U, None) (Γ, U, Some (C', restrict_subst_domain (vars_cls C') γ))"
proof (rule conflictI)
show "C' |∈| N |∪| U"
using C'_in by simp
next
show "is_ground_cls (C' ⋅ restrict_subst_domain (vars_cls C') γ)"
using ‹is_ground_cls C›[unfolded C_def]
by (simp add: subst_cls_restrict_subst_domain)
next
show "trail_false_cls Γ (C' ⋅ restrict_subst_domain (vars_cls C') γ)"
using ‹trail_false_cls Γ C›[unfolded C_def]
by (simp add: subst_cls_restrict_subst_domain)
qed
with no_new_conflict have False
by (simp add: S_def u_def)
thus "trail_true_cls Γ C" ..
qed
qed

moreover have "satisfiable gnd_N_lt_β"
unfolding true_clss_def gnd_N_lt_β_def
proof (intro exI ballI, unfold mem_Collect_eq, elim conjE)
fix C
have "trail_consistent Γ"
using S_def trail_consistent by auto
show "C ∈ gnd_N ⟹ ∀L ∈# C. atm_of L ≼⇩B β ⟹ trail_interp Γ ⊫ C"
using tr_true[unfolded gnd_N_lt_β_def]
using trail_interp_cls_if_trail_true[OF ‹trail_consistent Γ›]
by (simp add: trail_true_clss_def)
qed

ultimately show ?thesis
by (simp add: S_def)
next
case (Some Cl)
then obtain C γ⇩C where u_def: "u = Some (C, γ⇩C)" by force

from ‹ground_false_closures S› have Γ_false_C_γ⇩C: "trail_false_cls Γ (C ⋅ γ⇩C)"
by (simp add: S_def u_def ground_false_closures_def)

show ?thesis
proof (cases "C = {#}")
case True
hence "¬ satisfiable gnd_N ∧ (∃γ. state_conflict S = Some ({#}, γ))"
using S_def u_def not_satisfiable_if_sound_state_conflict_bottom[OF sound_S]
by (simp add: gnd_N_def)
thus ?thesis by simp
next
case C_not_empty: False
have False
proof (cases Γ)
case Nil
with Γ_false_C_γ⇩C show False
using C_not_empty by simp
next
case (Cons Ln Γ')
then obtain K⇩Γ n where Γ_def: "Γ = (K⇩Γ, n) # Γ'"
by fastforce

show False
proof (cases "- K⇩Γ ∈# C ⋅ γ⇩C")
case True ― ‹Literal cannot be skipped›
then obtain C' L where C_def: "C = add_mset L C'" and K_γ: "L ⋅l γ⇩C = - K⇩Γ"
by (metis Melem_subst_cls multi_member_split)
hence L_eq_uminus_K_γ: "K⇩Γ = - (L ⋅l γ⇩C)"
by simp

show False
proof (cases n)
case None ― ‹Conflict clause can be backtracked›
hence Γ_def: "Γ = trail_decide Γ' (- (L ⋅l γ⇩C))"
by (simp add: Γ_def L_eq_uminus_K_γ decide_lit_def)

from suffix_shortest_backtrack[of "add_mset L C'" Γ'] obtain Γ'' where
Γ'_def: "Γ' = Γ'' @ shortest_backtrack (add_mset L C') Γ'"
using suffixE by blast

define S' :: "('f, 'v) state" where
"S' = (shortest_backtrack (add_mset L C') Γ', finsert (add_mset L C') U, None)"

have "backtrack N β S S'"
unfolding S_def[unfolded u_def C_def] S'_def
proof (rule backtrackI[OF _ refl])
show "Γ = trail_decide (Γ'' @ shortest_backtrack (add_mset L C') Γ') (- (L ⋅l γ⇩C))"
using Γ_def Γ'_def by simp
next
show "∄γ. is_ground_cls (add_mset L C' ⋅ γ) ∧
trail_false_cls (shortest_backtrack (add_mset L C') Γ') (add_mset L C' ⋅ γ)"
using ex_conflict_shortest_backtrack[of "add_mset L C'", simplified]
by (simp add: ex_conflict_def)
qed
moreover have "is_shortest_backtrack (fst (the (state_conflict S)))
(state_trail S) (state_trail S')"
unfolding S_def[unfolded u_def C_def] S'_def
apply simp
using is_shortest_backtrack_shortest_backtrack[of "add_mset L C'", simplified]
by (metis C_def Γ_def Γ_false_C_γ⇩C ‹S = (Γ, U, Some (add_mset L C', γ⇩C))›
‹ground_closures S› ex_conflict_def ground_closures_def is_shortest_backtrack_def
state_proj_simp(3) suffix_Cons)
ultimately show False
using no_new_backtrack by metis
next
case Some ― ‹Literal can be resolved›
then obtain D K γ⇩D where n_def: "n = Some (D, K, γ⇩D)"
by (metis prod_cases3)
with ‹trail_propagated_wf (state_trail S)› have L_def: "K⇩Γ = K ⋅l γ⇩D"
by (simp add: Γ_def S_def trail_propagated_wf_def)
hence 1: "Γ = trail_propagate Γ' K D γ⇩D"
using Γ_def n_def
by (simp add: propagate_lit_def)

from ‹ground_closures S› have
ground_conf: "is_ground_cls (add_mset L C' ⋅ γ⇩C)" and
ground_prop: "is_ground_cls (add_mset K D ⋅ γ⇩D)"
unfolding S_def ground_closures_def
by (simp_all add: 1 C_def u_def ground_closures_def propagate_lit_def)

define ρ :: "'v ⇒ ('f, 'v) Term.term" where
"ρ = renaming_wrt {add_mset K D}"

have ren_ρ: "is_renaming ρ"
unfolding ρ_def
by (rule is_renaming_renaming_wrt) simp
hence "∀x. is_Var (ρ x)" "inj ρ"
by (simp_all add: is_renaming_iff)

have disjoint_vars: "⋀C. vars_cls (C ⋅ ρ) ∩ vars_cls (add_mset K D ⋅ Var) = {}"
by (simp add: ρ_def vars_cls_subst_renaming_disj)

have 2: "K ⋅l γ⇩D = - (L ⋅l γ⇩C)"
using K_γ L_def by fastforce

let ?γ⇩D' = "restrict_subst_domain (vars_cls (add_mset K D)) γ⇩D"

have "K ⋅l ?γ⇩D' = K ⋅l γ⇩D" and "D ⋅ ?γ⇩D' = D ⋅ γ⇩D"
by (simp_all add: subst_lit_restrict_subst_domain subst_cls_restrict_subst_domain)
hence "K ⋅l ?γ⇩D' = - (L ⋅l γ⇩C)" and ground_prop': "is_ground_cls (add_mset K D ⋅ ?γ⇩D')"
using 2 ground_prop by simp_all

have dom_γ⇩D': "subst_domain ?γ⇩D' ⊆ vars_cls (add_mset K D)"
by simp

let ?γ = "λx.
if x ∈ vars_cls (add_mset L C' ⋅ ρ) then
rename_subst_domain ρ γ⇩C x
else
γ⇩D x"
have "L ⋅l ρ ⋅l ?γ = L ⋅l γ⇩C" and "K ⋅l ?γ = K ⋅l γ⇩D"
using merge_of_renamed_groundings[OF ren_ρ is_renaming_id_subst disjoint_vars
ground_conf ground_prop is_grounding_merge_if_mem_then_else]
unfolding rename_subst_domain_Var_lhs
by simp_all

then have "atm_of L ⋅a ρ ⋅a ?γ = atm_of K ⋅a ?γ"
by (smt (verit, best) "2" atm_of_uminus subst_lit_id_subst atm_of_subst_lit)
then obtain μ where "Unification.mgu (atm_of L ⋅a ρ) (atm_of K) = Some μ"
using ex_mgu_if_subst_apply_term_eq_subst_apply_term
by blast
hence imgu_μ: "is_imgu μ {{atm_of L ⋅a ρ, atm_of K ⋅a Var}}"
by (simp add: is_imgu_if_mgu_eq_Some)

have "∃S. resolve N β (Γ, U, Some (add_mset L C', γ⇩C)) S"
using resolveI[OF 1 2 ren_ρ is_renaming_id_subst disjoint_vars imgu_μ
is_grounding_merge_if_mem_then_else] ..
with no_new_resolve show False
by (metis C_def S_def u_def)
qed
next
case False ― ‹Literal can be skipped›
hence "skip N β ((K⇩Γ, n) # Γ', U, Some (C, γ⇩C)) (Γ', U, Some (C, γ⇩C))"
by (rule skipI[of K⇩Γ C γ⇩C N β n Γ' U])
with no_new_skip show False
by (metis S_def Γ_def u_def)
qed
qed
thus ?thesis ..
qed
qed
qed

corollary correct_termination_strategy:
fixes gnd_N and gnd_N_lt_β
assumes
run: "(strategy N β)⇧*⇧* initial_state S" and
no_step: "∄S'. strategy N β S S'" and
strategy_restricted_by_min_back:
"⋀S S'. shortest_backtrack_strategy regular_scl N β S S' ⟹ strategy N β S S'" and
strategy_preserves_invars:
"⋀N β S S'. strategy N β S S' ⟹ sound_state N β S ⟹ sound_state N β S'"
"⋀N β S S'. strategy N β S S' ⟹ trail_atoms_lt β S ⟹ trail_atoms_lt β S'"
"⋀N β S S'. strategy N β S S' ⟹ trail_propagated_or_decided' N β S ⟹ trail_propagated_or_decided' N β S'"
"⋀N β S S'. strategy N β S S' ⟹ trail_lits_consistent S ⟹ trail_lits_consistent S'"
"⋀N β S S'. strategy N β S S' ⟹ ground_false_closures S ⟹ ground_false_closures S'"
defines
"gnd_N ≡ grounding_of_clss (fset N)" and
"gnd_N_lt_β ≡ {C ∈ gnd_N. ∀L ∈# C. atm_of L ≼⇩B β}"
shows "¬ satisfiable gnd_N ∧ (∃γ. state_conflict S = Some ({#}, γ)) ∨
satisfiable gnd_N_lt_β ∧ trail_true_clss (state_trail S) gnd_N_lt_β"
proof -
from no_step have no_step': "∄S'. shortest_backtrack_strategy regular_scl N β S S'"
proof (rule contrapos_nn)
show "∃S'. shortest_backtrack_strategy regular_scl N β S S' ⟹ ∃S'. strategy N β S S'"
using strategy_restricted_by_min_back by metis
qed

show ?thesis
proof (rule correct_termination[of N β S, folded gnd_N_def, folded gnd_N_lt_β_def])
from run show "sound_state N β S"
by (induction S rule: rtranclp_induct) (auto intro: strategy_preserves_invars(1))
next
from run show "trail_atoms_lt β S"
by (induction S rule: rtranclp_induct) (auto intro: strategy_preserves_invars(2))
next
from run have "trail_propagated_or_decided' N β S"
by (induction S rule: rtranclp_induct) (auto intro: strategy_preserves_invars(3))
thus "trail_propagated_wf (state_trail S)"
by (simp add: trail_propagated_or_decided'_def
trail_propagated_wf_if_trail_propagated_or_decided)
next
from run show "trail_lits_consistent S"
by (induction S rule: rtranclp_induct) (auto intro: strategy_preserves_invars(4))
next
from run show "ground_false_closures S"
by (induction S rule: rtranclp_induct) (auto intro: strategy_preserves_invars(5))
next
from no_step' show "∄S'. conflict N β S S'"
unfolding shortest_backtrack_strategy_def regular_scl_def reasonable_scl_def scl_def
using backtrack_well_defined(3) by blast
next
from no_step' show "∄S'. propagate N β S S'"
unfolding shortest_backtrack_strategy_def regular_scl_def reasonable_scl_def scl_def
using backtrack_well_defined(3) propagate_well_defined(1) propagate_well_defined(6) by blast
next
from no_step' show "∄S'. decide N β S S' ∧ (∄S''. conflict N β S' S'')"
unfolding shortest_backtrack_strategy_def regular_scl_def reasonable_scl_def scl_def
using backtrack_well_defined(2) backtrack_well_defined(3) by blast
next
from no_step' show "∄S'. skip N β S S'"
unfolding shortest_backtrack_strategy_def regular_scl_def reasonable_scl_def scl_def
using backtrack_well_defined(3) backtrack_well_defined(4) skip_well_defined(2) by blast
next
from no_step' show "∄S'. resolve N β S S'"
unfolding shortest_backtrack_strategy_def regular_scl_def reasonable_scl_def scl_def
using backtrack_well_defined(3) resolve_well_defined(2) resolve_well_defined(5) by blast
next
from no_step' show "∄S'. backtrack N β S S' ∧
is_shortest_backtrack (fst (the (state_conflict S))) (state_trail S) (state_trail S')"
unfolding shortest_backtrack_strategy_def scl_def regular_scl_def reasonable_scl_def
using backtrack_well_defined(2) backtrack_well_defined(3) by blast
qed
qed

corollary correct_termination_scl_run:
fixes gnd_N and gnd_N_lt_β
assumes
run: "(scl N β)⇧*⇧* initial_state S" and
no_step: "∄S'. scl N β S S'"
defines
"gnd_N ≡ grounding_of_clss (fset N)" and
"gnd_N_lt_β ≡ {C ∈ gnd_N. ∀L ∈# C. atm_of L ≼⇩B β}"
shows "¬ satisfiable gnd_N ∧ (∃γ. state_conflict S = Some ({#}, γ)) ∨
satisfiable gnd_N_lt_β ∧ trail_true_clss (state_trail S) gnd_N_lt_β"
proof (rule correct_termination_strategy[of _ N β, folded gnd_N_def, folded gnd_N_lt_β_def])
show "(scl N β)⇧*⇧* initial_state S"
by (rule run)
next
show "∄S'. scl N β S S'"
by (rule no_step)
next
show "⋀S S'. shortest_backtrack_strategy regular_scl N β S S' ⟹ scl N β S S'"
by (simp add: regular_scl_if_shortest_backtrack_strategy scl_if_regular)
next
show "⋀N β S S'. scl N β S S' ⟹ sound_state N β S ⟹ sound_state N β S'"
using scl_preserves_sound_state by simp
next
show "⋀N β S S'. scl N β S S' ⟹ trail_atoms_lt β S ⟹ trail_atoms_lt β S'"
using scl_preserves_trail_atoms_lt by simp
next
show "⋀N β S S'. scl N β S S' ⟹ trail_propagated_or_decided' N β S ⟹
trail_propagated_or_decided' N β S'"
using scl_preserves_trail_propagated_or_decided by simp
next
show "⋀N β S S'. scl N β S S' ⟹ trail_lits_consistent S ⟹ trail_lits_consistent S'"
using scl_preserves_trail_lits_consistent by simp
next
show "⋀N β S S'. scl N β S S' ⟹ ground_false_closures S ⟹ ground_false_closures S'"
using scl_preserves_ground_false_closures by simp
qed

corollary correct_termination_reasonable_scl_run:
fixes gnd_N and gnd_N_lt_β
assumes
run: "(reasonable_scl N β)⇧*⇧* initial_state S" and
no_step: "∄S'. reasonable_scl N β S S'"
defines
"gnd_N ≡ grounding_of_clss (fset N)" and
"gnd_N_lt_β ≡ {C ∈ gnd_N. ∀L ∈# C. atm_of L ≼⇩B β}"
shows "¬ satisfiable gnd_N ∧ (∃γ. state_conflict S = Some ({#}, γ)) ∨
satisfiable gnd_N_lt_β ∧ trail_true_clss (state_trail S) gnd_N_lt_β"
proof (rule correct_termination_strategy[of _ N β, folded gnd_N_def, folded gnd_N_lt_β_def])
show "(reasonable_scl N β)⇧*⇧* initial_state S"
by (rule run)
next
show "∄S'. reasonable_scl N β S S'"
by (rule no_step)
next
show "⋀S S'. shortest_backtrack_strategy regular_scl N β S S' ⟹ reasonable_scl N β S S'"
by (simp add: reasonable_if_regular regular_scl_if_shortest_backtrack_strategy)
next
show "⋀N β S S'. reasonable_scl N β S S' ⟹ sound_state N β S ⟹ sound_state N β S'"
using scl_preserves_sound_state[OF scl_if_reasonable] by simp
next
show "⋀N β S S'. reasonable_scl N β S S' ⟹ trail_atoms_lt β S ⟹ trail_atoms_lt β S'"
using scl_preserves_trail_atoms_lt[OF scl_if_reasonable] by simp
next
show "⋀N β S S'. reasonable_scl N β S S' ⟹ trail_propagated_or_decided' N β S ⟹
trail_propagated_or_decided' N β S'"
using scl_preserves_trail_propagated_or_decided[OF scl_if_reasonable] by simp
next
show "⋀N β S S'. reasonable_scl N β S S' ⟹ trail_lits_consistent S ⟹ trail_lits_consistent S'"
using scl_preserves_trail_lits_consistent[OF scl_if_reasonable] by simp
next
show "⋀N β S S'. reasonable_scl N β S S' ⟹ ground_false_closures S ⟹ ground_false_closures S'"
using scl_preserves_ground_false_closures[OF scl_if_reasonable] by simp
qed

corollary correct_termination_regular_scl_run:
fixes gnd_N and gnd_N_lt_β
assumes
run: "(regular_scl N β)⇧*⇧* initial_state S" and
no_step: "∄S'. regular_scl N β S S'"
defines
"gnd_N ≡ grounding_of_clss (fset N)" and
"gnd_N_lt_β ≡ {C ∈ gnd_N. ∀L ∈# C. atm_of L ≼⇩B β}"
shows "¬ satisfiable gnd_N ∧ (∃γ. state_conflict S = Some ({#}, γ)) ∨
satisfiable gnd_N_lt_β ∧ trail_true_clss (state_trail S) gnd_N_lt_β"
proof (rule correct_termination_strategy[of _ N β, folded gnd_N_def, folded gnd_N_lt_β_def])
show "(regular_scl N β)⇧*⇧* initial_state S"
by (rule run)
next
show "∄S'. regular_scl N β S S'"
by (rule no_step)
next
show "⋀S S'. shortest_backtrack_strategy regular_scl N β S S' ⟹ regular_scl N β S S'"
by (simp add: reasonable_if_regular regular_scl_if_shortest_backtrack_strategy)
next
show "⋀N β S S'. regular_scl N β S S' ⟹ sound_state N β S ⟹ sound_state N β S'"
using scl_preserves_sound_state[OF scl_if_regular] by simp
next
show "⋀N β S S'. regular_scl N β S S' ⟹ trail_atoms_lt β S ⟹ trail_atoms_lt β S'"
using scl_preserves_trail_atoms_lt[OF scl_if_regular] by simp
next
show "⋀N β S S'. regular_scl N β S S' ⟹ trail_propagated_or_decided' N β S ⟹
trail_propagated_or_decided' N β S'"
using scl_preserves_trail_propagated_or_decided[OF scl_if_regular] by simp
next
show "⋀N β S S'. regular_scl N β S S' ⟹ trail_lits_consistent S ⟹ trail_lits_consistent S'"
using scl_preserves_trail_lits_consistent[OF scl_if_regular] by simp
next
show "⋀N β S S'. regular_scl N β S S' ⟹ ground_false_closures S ⟹ ground_false_closures S'"
using scl_preserves_ground_false_closures[OF scl_if_regular] by simp
qed

corollary correct_termination_shortest_backtrack_strategy_regular_scl:
fixes gnd_N and gnd_N_lt_β
assumes
run: "(shortest_backtrack_strategy regular_scl N β)⇧*⇧* initial_state S" and
no_step: "∄S'. shortest_backtrack_strategy regular_scl N β S S'"
defines
"gnd_N ≡ grounding_of_clss (fset N)" and
"gnd_N_lt_β ≡ {C ∈ gnd_N. ∀L ∈# C. atm_of L ≼⇩B β}"
shows "¬ satisfiable gnd_N ∧ (∃γ. state_conflict S = Some ({#}, γ)) ∨
satisfiable gnd_N_lt_β ∧ trail_true_clss (state_trail S) gnd_N_lt_β"
proof (rule correct_termination_strategy[of _ N β, folded gnd_N_def, folded gnd_N_lt_β_def])
show "(shortest_backtrack_strategy regular_scl N β)⇧*⇧* initial_state S"
by (rule run)
next
show "∄S'. shortest_backtrack_strategy regular_scl N β S S'"
by (rule no_step)
next
show "⋀S S'. shortest_backtrack_strategy regular_scl N β S S' ⟹ shortest_backtrack_strategy regular_scl N β S S'"
by simp
next
show "⋀N β S S'. shortest_backtrack_strategy regular_scl N β S S' ⟹ sound_state N β S ⟹ sound_state N β S'"
using scl_preserves_sound_state[OF scl_if_regular]
by (auto simp: shortest_backtrack_strategy_def)
next
show "⋀N β S S'. shortest_backtrack_strategy regular_scl N β S S' ⟹ trail_atoms_lt β S ⟹ trail_atoms_lt β S'"
using scl_preserves_trail_atoms_lt[OF scl_if_regular]
by (auto simp: shortest_backtrack_strategy_def)
next
show "⋀N β S S'. shortest_backtrack_strategy regular_scl N β S S' ⟹ trail_propagated_or_decided' N β S ⟹
trail_propagated_or_decided' N β S'"
using scl_preserves_trail_propagated_or_decided[OF scl_if_regular]
by (auto simp: shortest_backtrack_strategy_def)
next
show "⋀N β S S'. shortest_backtrack_strategy regular_scl N β S S' ⟹ trail_lits_consistent S ⟹ trail_lits_consistent S'"
using scl_preserves_trail_lits_consistent[OF scl_if_regular]
by (auto simp: shortest_backtrack_strategy_def)
next
show "⋀N β S S'. shortest_backtrack_strategy regular_scl N β S S' ⟹ ground_false_closures S ⟹ ground_false_closures S'"
using scl_preserves_ground_false_closures[OF scl_if_regular]
by (auto simp: shortest_backtrack_strategy_def)
qed

corollary correct_termination_strategies:
fixes gnd_N and gnd_N_lt_β
assumes
"(scl N β)⇧*⇧* initial_state S ∧ (∄S'. scl N β S S') ∨
(reasonable_scl N β)⇧*⇧* initial_state S ∧ (∄S'. reasonable_scl N β S S') ∨
(regular_scl N β)⇧*⇧* initial_state S ∧ (∄S'. regular_scl N β S S') ∨
(shortest_backtrack_strategy regular_scl N β)⇧*⇧* initial_state S ∧
(∄S'. shortest_backtrack_strategy regular_scl N β S S')"
defines
"gnd_N ≡ grounding_of_clss (fset N)" and
"gnd_N_lt_β ≡ {C ∈ gnd_N. ∀L ∈# C. atm_of L ≼⇩B β}"
shows "¬ satisfiable gnd_N ∧ (∃γ. state_conflict S = Some ({#}, γ)) ∨
satisfiable gnd_N_lt_β ∧ trail_true_clss (state_trail S) gnd_N_lt_β"
unfolding gnd_N_def gnd_N_lt_β_def
using assms(1)
correct_termination_scl_run[of N β S]
correct_termination_reasonable_scl_run[of N β S]
correct_termination_regular_scl_run[of N β S]
correct_termination_shortest_backtrack_strategy_regular_scl[of N β S]
by argo

end

end```