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