# Theory Termination

```theory Termination
imports
SCL_FOL
Non_Redundancy
Wellfounded_Extra
"HOL-Library.Monad_Syntax"
begin

section ‹Extra Lemmas›

subsection ‹Set Extra›

lemma minus_psubset_minusI:
assumes "C ⊂ B" and "B ⊆ A"
shows "(A - B ⊂ A - C)"
proof (rule Set.psubsetI)
show "A - B ⊆ A - C"
using assms(1) by blast
next
show "A - B ≠ A - C"
using assms by blast
qed

lemma wfP_pfsubset: "wfP (|⊂|)"
proof (rule wfP_if_convertible_to_nat)
show "⋀x y. x |⊂| y ⟹ fcard x < fcard y"
by (rule pfsubset_fcard_mono)
qed

subsection ‹Prod Extra›

lemma lex_prod_lex_prodp_eq:
"lex_prod {(x, y). RA x y} {(x, y). RB x y} = {(x, y). lex_prodp RA RB x y}"
unfolding lex_prodp_def lex_prod_def
by auto

lemma reflp_on_lex_prodp:
assumes "reflp_on A RA"
shows "reflp_on (A × B) (lex_prodp RA RB)"
proof (rule reflp_onI)
fix x assume "x ∈ A × B"
hence "fst x ∈ A"
by auto
thus "lex_prodp RA RB x x"
by (simp add: lex_prodp_def ‹reflp_on A RA›[THEN reflp_onD])
qed

lemma transp_lex_prodp:
assumes "transp RA" and "transp RB"
shows "transp (lex_prodp RA RB)"
proof (rule transpI)
fix x y z assume "lex_prodp RA RB x y" and "lex_prodp RA RB y z"
thus "lex_prodp RA RB x z"
by (auto simp add: lex_prodp_def ‹transp RA›[THEN transpD, of "fst x" "fst y" "fst z"]
‹transp RB›[THEN transpD, of "snd x" "snd y" "snd z"])
qed

lemma asymp_lex_prodp:
assumes "asymp RA" and "asymp RB"
shows "asymp (lex_prodp RA RB)"
proof (rule asympI)
fix x y assume "lex_prodp RA RB x y"
thus "¬ lex_prodp RA RB y x"
using assms by (metis (full_types, opaque_lifting) asympD lex_prodp_def)
qed

lemma totalp_on_lex_prodp:
assumes "totalp_on A RA" and "totalp_on B RB"
shows "totalp_on (A × B) (lex_prodp RA RB)"
proof (rule totalp_onI)
fix x y assume "x ∈ A × B" and "y ∈ A × B" and "x ≠ y"
then show "lex_prodp RA RB x y ∨ lex_prodp RA RB y x"
using assms
by (metis (full_types) lex_prodp_def mem_Times_iff prod_eq_iff totalp_on_def)
qed

subsection ‹Wellfounded Extra›

subsection ‹FSet Extra›

lemma finsert_Abs_fset: "finite A ⟹ finsert a (Abs_fset A) = Abs_fset (insert a A)"
by (simp add: eq_onp_same_args finsert.abs_eq)

lemma minus_pfsubset_minusI:
assumes "C |⊂| B" and "B |⊆| A"
shows "(A |-| B |⊂| A |-| C)"
proof (rule FSet.pfsubsetI)
show "A |-| B |⊆| A |-| C"
using assms(1) by blast
next
show "A |-| B ≠ A |-| C"
using assms by blast
qed

lemma Abs_fset_minus: "finite A ⟹ finite B ⟹ Abs_fset (A - B) = Abs_fset A |-| Abs_fset B"
by (metis Abs_fset_inverse fset_inverse mem_Collect_eq minus_fset)

lemma fminus_conv: "A |⊂| B ⟷ fset A ⊂ fset B ∧ finite (fset A) ∧ finite (fset B)"
by (simp add: less_eq_fset.rep_eq less_le_not_le)

section ‹Termination›

context scl_fol_calculus begin

subsection ‹SCL without backtracking terminates›

definition ℳ_prop_deci :: "_ ⇒ _ ⇒ (_, _) Term.term literal fset" where
"ℳ_prop_deci β Γ = Abs_fset {L. atm_of L ≼⇩B β} |-| (fst |`| fset_of_list Γ)"

primrec ℳ_skip_fact_reso where
"ℳ_skip_fact_reso [] C = []" |
"ℳ_skip_fact_reso (Ln # Γ) C =
(let n = count C (- (fst Ln)) in
(case snd Ln of None ⇒ 0 | Some _ ⇒ n) #
ℳ_skip_fact_reso Γ (C + (case snd Ln of None ⇒ {#} | Some (D, _, γ) ⇒ repeat_mset n (D ⋅ γ))))"

fun ℳ_skip_fact_reso' where
"ℳ_skip_fact_reso' C [] = []" |
"ℳ_skip_fact_reso' C ((_, None) # Γ) = 0 # ℳ_skip_fact_reso' C Γ" |
"ℳ_skip_fact_reso' C ((K, Some (D, _, γ)) # Γ) =
(let n = count C (- K) in n # ℳ_skip_fact_reso' (C + repeat_mset n (D ⋅ γ)) Γ)"

lemma "ℳ_skip_fact_reso Γ C = ℳ_skip_fact_reso' C Γ"
proof (induction Γ arbitrary: C)
case Nil
show ?case
by simp
next
case (Cons Kn Γ)
then show ?case
apply (cases "Kn")
apply (cases "snd Kn")
by (auto simp add: Let_def)
qed

lemma "ℳ_skip_fact_reso' C (decide_lit K # Γ) = 0 # ℳ_skip_fact_reso' C Γ"
by (simp add: decide_lit_def)

lemma "ℳ_skip_fact_reso' C (propagate_lit K D γ # Γ) =
(let n = count C (- (K ⋅l γ)) in n # ℳ_skip_fact_reso' (C + repeat_mset n (D ⋅ γ)) Γ)"
by (simp add: propagate_lit_def)

fun ℳ :: "_ ⇒ _ ⇒ ('f, 'v) state ⇒
bool × ('f, 'v) Term.term literal fset × nat list × nat" where
"ℳ N β (Γ, U, None) = (True, ℳ_prop_deci β Γ, [], 0)" |
"ℳ N β (Γ, U, Some (C, γ)) = (False, {||}, ℳ_skip_fact_reso Γ (C ⋅ γ), size C)"

lemma length_ℳ_skip_fact_reso[simp]: "length (ℳ_skip_fact_reso Γ C) = length Γ"
by (induction Γ arbitrary: C) (simp_all add: Let_def)

lemma ℳ_skip_fact_reso_add_mset:
"(ℳ_skip_fact_reso Γ C, ℳ_skip_fact_reso Γ (add_mset L C)) ∈ (List.lenlex {(x, y). x < y})⇧="
proof (induction Γ arbitrary: C)
case Nil
show ?case by simp
next
case (Cons Ln Γ)
show ?case
proof (cases "snd Ln")
case None
then show ?thesis
using Cons.IH[of C]
by (simp add: Cons_lenlex_iff)
next
case (Some cl)
show ?thesis
proof (cases "L = - fst Ln")
case True
then show ?thesis
by (simp add: Let_def Some Cons_lenlex_iff)
next
case False
then show ?thesis
using Cons.IH
by (auto simp add: Let_def Some Cons_lenlex_iff)
qed
qed
qed

lemma termination_scl_without_back_invars:
fixes N β
defines
"scl_without_backtrack ≡ propagate N β ⊔ decide N β ⊔ conflict N β ⊔ skip N β ⊔
factorize N β ⊔ resolve N β" and
"invars ≡ trail_atoms_lt β ⊓ trail_resolved_lits_pol ⊓ trail_lits_ground ⊓
trail_lits_from_clauses N ⊓ initial_lits_generalize_learned_trail_conflict N ⊓
ground_closures"
shows "wfp_on {S. invars S} scl_without_backtrack¯¯"
proof -
let ?less =
"lex_prodp ((<) :: bool ⇒ bool ⇒ bool)
(lex_prodp (|⊂|)
(lex_prodp (λx y. (x, y) ∈ List.lenlex {(x :: _ :: wellorder, y). x < y})
((<) :: nat ⇒ nat ⇒ bool)))"

show "wfp_on {S. invars S} scl_without_backtrack¯¯"
proof (rule wfp_on_if_convertible_to_wfp)
fix S' S :: "('f, 'v) state"
assume "S' ∈ {S. invars S}" and "S ∈ {S. invars S}" and step: "scl_without_backtrack¯¯ S' S"
hence
"trail_atoms_lt β S" and
"trail_resolved_lits_pol S" and
"trail_lits_ground S" and
"trail_lits_from_clauses N S" and
"initial_lits_generalize_learned_trail_conflict N S" and
"ground_closures S"
"trail_lits_from_clauses N S'" and
"initial_lits_generalize_learned_trail_conflict N S'"
by (simp_all add: invars_def)

have "trail_lits_from_init_clauses N S"
using ‹trail_lits_from_clauses N S› ‹initial_lits_generalize_learned_trail_conflict N S›
by (simp add: trail_lits_from_init_clausesI)

have "trail_lits_from_init_clauses N S'"
using ‹trail_lits_from_clauses N S'› ‹initial_lits_generalize_learned_trail_conflict N S'›
by (simp add: trail_lits_from_init_clausesI)

from step show "?less (ℳ N β S') (ℳ N β S)"
unfolding conversep_iff scl_without_backtrack_def sup_apply sup_bool_def
proof (elim disjE)
assume "decide N β S S'"
thus "?less (ℳ N β S') (ℳ N β S)"
proof (cases N β S S' rule: decide.cases)
case (decideI L γ Γ U)
have "ℳ_prop_deci β ((L ⋅l γ, None) # Γ) |⊂| ℳ_prop_deci β Γ"
unfolding ℳ_prop_deci_def fset_of_list_simps fimage_finsert prod.sel
proof (rule minus_pfsubset_minusI)
show "fst |`| fset_of_list Γ |⊂| finsert (L ⋅l γ) (fst |`| fset_of_list Γ)"
using ‹¬ trail_defined_lit Γ (L ⋅l γ)›[unfolded trail_defined_lit_def]
by (metis (no_types, lifting) finsertCI fset_of_list_elem fset_of_list_map
fsubset_finsertI list.set_map nless_le)
next
have "L ⋅l γ ∈ {L. atm_of L ≼⇩B β}"
using ‹atm_of L ⋅a γ ≼⇩B β›
by simp
moreover have "fst ` set Γ ⊆ {L. atm_of L ≼⇩B β}"
using ‹trail_atoms_lt β S›
by (auto simp: trail_atoms_lt_def decideI(1))
ultimately have "insert (L ⋅l γ) (fst ` set Γ) ⊆ {L. atm_of L ≼⇩B β}"
by simp
then show "finsert (L ⋅l γ) (fst |`| fset_of_list Γ) |⊆| Abs_fset {L. atm_of L ≼⇩B β}"
using finite_lits_less_eq_B
by (simp add: less_eq_fset.rep_eq Abs_fset_inverse fset_of_list.rep_eq)
qed
then show ?thesis
unfolding decideI(1,2) decide_lit_def
unfolding lex_prodp_def
by simp
qed
next
assume "propagate N β S S'"
thus "?less (ℳ N β S') (ℳ N β S)"
proof (cases N β S S' rule: propagate.cases)
case (propagateI C U L C' γ C⇩0 C⇩1 Γ μ)

have "L ⋅l μ ⋅l γ = L ⋅l γ"
proof -
have "is_unifiers γ {atm_of ` set_mset (add_mset L C⇩1)}"
unfolding ‹C⇩1 = {#K ∈# C'. K ⋅l γ = L ⋅l γ#}›
by (auto simp: is_unifiers_def is_unifier_alt intro: subst_atm_of_eqI)
hence "μ ⊙ γ = γ"
using ‹is_imgu μ {atm_of ` set_mset (add_mset L C⇩1)}›[unfolded is_imgu_def, THEN conjunct2]
by simp
thus ?thesis
by (metis subst_lit_comp_subst)
qed

have "ℳ_prop_deci β ((L ⋅l γ, Some (C⇩0 ⋅ μ, L ⋅l μ, γ)) # Γ) |⊂| ℳ_prop_deci β Γ"
unfolding ℳ_prop_deci_def fset_of_list_simps fimage_finsert prod.sel
proof (rule minus_pfsubset_minusI)
show "fst |`| fset_of_list Γ |⊂| finsert (L ⋅l γ) (fst |`| fset_of_list Γ)"
using ‹¬ trail_defined_lit Γ (L ⋅l γ)›[unfolded trail_defined_lit_def]
by (metis (no_types, lifting) finsertCI fset_of_list_elem fset_of_list_map
fsubset_finsertI list.set_map nless_le)
next
have "insert (L ⋅l γ) (fst ` set Γ) ⊆ {L. atm_of L ≼⇩B β}"
proof (intro Set.subsetI Set.CollectI)
fix K assume "K ∈ insert (L ⋅l γ) (fst ` set Γ)"
thus "atm_of K ≼⇩B β"
using ‹trail_atoms_lt β S›
by (metis image_eqI insert_iff propagateI(1,4,6) state_trail_simp subst_cls_add_mset
trail_atoms_lt_def union_single_eq_member)
qed
then show "finsert (L ⋅l γ) (fst |`| fset_of_list Γ) |⊆| Abs_fset {L. atm_of L ≼⇩B β}"
using finite_lits_less_eq_B
by (simp add: less_eq_fset.rep_eq fset_of_list.rep_eq Abs_fset_inverse)
qed
thus ?thesis
unfolding propagateI(1,2) propagate_lit_def state_proj_simp option.case
unfolding ‹L ⋅l μ ⋅l γ = L ⋅l γ›
unfolding lex_prodp_def
by simp
qed
next
assume "conflict N β S S'"
thus "?less (ℳ N β S') (ℳ N β S)"
proof (cases N β S S' rule: conflict.cases)
case (conflictI D U γ Γ)
show ?thesis
unfolding lex_prodp_def conflictI(1,2) by simp
qed
next
assume "skip N β S S'"
thus "?less (ℳ N β S') (ℳ N β S)"
proof (cases N β S S' rule: skip.cases)
case (skipI L D σ n Γ U)
have "(ℳ_skip_fact_reso Γ (D ⋅ σ), ℳ_skip_fact_reso ((L, n) # Γ) (D ⋅ σ)) ∈
lenlex {(x, y). x < y}"
by (simp add: lenlex_conv Let_def)
thus ?thesis
unfolding lex_prodp_def skipI(1,2) by simp
qed
next
assume "factorize N β S S'"
thus "?less (ℳ N β S') (ℳ N β S)"
proof (cases N β S S' rule: factorize.cases)
case (factorizeI L γ L' μ Γ U D)

have "is_unifier γ {atm_of L, atm_of L'}"
using ‹L ⋅l γ = L' ⋅l γ›[THEN subst_atm_of_eqI]
by (simp add: is_unifier_alt)
hence "μ ⊙ γ = γ"
using ‹is_imgu μ {{atm_of L, atm_of L'}}›
by (simp add: is_imgu_def is_unifiers_def)

have "add_mset L D ⋅ μ ⋅ γ = add_mset L D ⋅ γ"
using ‹μ ⊙ γ = γ›
by (metis subst_cls_comp_subst)
hence "(ℳ_skip_fact_reso Γ (add_mset L D ⋅ μ ⋅ γ),
ℳ_skip_fact_reso Γ (add_mset L' (add_mset L D) ⋅ γ)) ∈ (lenlex {(x, y). x < y})⇧="
using ℳ_skip_fact_reso_add_mset
by (metis subst_cls_add_mset)
thus ?thesis
unfolding lex_prodp_def factorizeI(1,2)
unfolding add_mset_commute[of L' L]
by simp
qed
next
assume "resolve N β S S'"
thus "?less (ℳ N β S') (ℳ N β S)"
proof (cases N β S S' rule: resolve.cases)
case (resolveI Γ Γ' K D γ⇩D L γ⇩C ρ⇩C ρ⇩D C μ γ U)
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 resolveI(1,2) ‹Γ = trail_propagate Γ' K D γ⇩D›
by (simp_all add: ground_closures_def propagate_lit_def)
hence
"∀L∈#add_mset L C. L ⋅l ρ⇩C ⋅l γ = L ⋅l γ⇩C"
"∀K∈#add_mset K D. K ⋅l ρ⇩D ⋅l γ = K ⋅l γ⇩D"
using resolveI merge_of_renamed_groundings by metis+

have "atm_of L ⋅a ρ⇩C ⋅a γ = atm_of K ⋅a ρ⇩D ⋅a γ"
using ‹K ⋅l γ⇩D = - (L ⋅l γ⇩C)›
‹∀L∈#add_mset L C. L ⋅l ρ⇩C ⋅l γ = L ⋅l γ⇩C›[rule_format, of L, simplified]
‹∀K∈#add_mset K D. K ⋅l ρ⇩D ⋅l γ = K ⋅l γ⇩D›[rule_format, of K, simplified]
by (metis atm_of_eq_uminus_if_lit_eq atm_of_subst_lit)
hence "is_unifiers γ {{atm_of L ⋅a ρ⇩C, atm_of K ⋅a ρ⇩D}}"
by (simp add: is_unifiers_def is_unifier_alt)
hence "μ ⊙ γ = γ"
using ‹is_imgu μ {{atm_of L ⋅a ρ⇩C, atm_of K ⋅a ρ⇩D}}›
by (auto simp: is_imgu_def)
hence "C ⋅ ρ⇩C ⋅ μ ⋅ γ = C ⋅ γ⇩C" and "D ⋅ ρ⇩D ⋅ μ ⋅ γ = D ⋅ γ⇩D"
using ‹∀L∈#add_mset L C. L ⋅l ρ⇩C ⋅l γ = L ⋅l γ⇩C› ‹∀K∈#add_mset K D. K ⋅l ρ⇩D ⋅l γ = K ⋅l γ⇩D›
by (metis insert_iff same_on_lits_clause set_mset_add_mset_insert subst_cls_comp_subst
subst_lit_comp_subst)+
hence "(C ⋅ ρ⇩C + D ⋅ ρ⇩D) ⋅ μ ⋅ γ = C ⋅ γ⇩C + D ⋅ γ⇩D"
by (metis subst_cls_comp_subst subst_cls_union)

have "L ⋅l γ⇩C ∉# D ⋅ γ⇩D"
using ‹trail_resolved_lits_pol S› ‹K ⋅l γ⇩D = - (L ⋅l γ⇩C)›
unfolding resolveI(1,2) ‹Γ = trail_propagate Γ' K D γ⇩D›
by (simp add: trail_resolved_lits_pol_def propagate_lit_def)

have "(ℳ_skip_fact_reso Γ (C ⋅ γ⇩C + D ⋅ γ⇩D), ℳ_skip_fact_reso Γ (add_mset L C ⋅ γ⇩C)) ∈
lex {(x, y). x < y}"
unfolding ‹Γ = trail_propagate Γ' K D γ⇩D› propagate_lit_def
unfolding ℳ_skip_fact_reso.simps Let_def prod.sel option.case prod.case
unfolding lex_conv mem_Collect_eq prod.case
apply (rule conjI)
apply simp
apply (rule exI[of _ "[]"])
apply simp
using ‹K ⋅l γ⇩D = - (L ⋅l γ⇩C)›
apply simp
unfolding count_eq_zero_iff
by (rule ‹L ⋅l γ⇩C ∉# D ⋅ γ⇩D›)
hence "(ℳ_skip_fact_reso Γ (C ⋅ γ⇩C + D ⋅ γ⇩D), ℳ_skip_fact_reso Γ (add_mset L C ⋅ γ⇩C)) ∈
lenlex {(x, y). x < y}"
unfolding lenlex_conv by simp
thus ?thesis
unfolding lex_prodp_def resolveI(1,2)
unfolding ℳ.simps state_proj_simp option.case prod.case prod.sel
unfolding ‹(C ⋅ ρ⇩C + D ⋅ ρ⇩D) ⋅ μ ⋅ γ = C ⋅ γ⇩C + D ⋅ γ⇩D›
by simp
qed
qed
next
show "wfp_on (ℳ N β ` {S. invars S}) ?less"
proof (rule wfp_on_subset)
show "ℳ N β ` {S. invars S} ⊆ UNIV"
by simp
next
show "wfp ?less"
proof (intro wfp_lex_prodp)
show "wfp ((<) :: bool ⇒ bool ⇒ bool)"
unfolding wfp_iff_wfP
by (simp add: Wellfounded.wfPUNIVI)
next
show "wfp (|⊂|)"
unfolding wfp_iff_wfP
by (rule wfP_pfsubset)
next
show "wfp (λx y. (x, y) ∈ lenlex {(x :: _ :: wellorder, y). x < y})"
unfolding wfp_iff_wfP Wellfounded.wfP_wf_eq
using wf_lenlex
using wf by blast
next
show "wfp ((<) :: nat ⇒ nat ⇒ bool)"
unfolding wfp_iff_wfP by simp
qed
qed
qed
qed

corollary termination_scl_without_back:
fixes
N :: "('f, 'v) Term.term clause fset" and
β :: "('f, 'v) Term.term"
defines
"scl_without_backtrack ≡ propagate N β ⊔ decide N β ⊔ conflict N β ⊔ skip N β ⊔
factorize N β ⊔ resolve N β" and
"invars ≡ trail_atoms_lt β ⊓ trail_resolved_lits_pol ⊓ trail_lits_ground ⊓
trail_lits_from_clauses N ⊓ initial_lits_generalize_learned_trail_conflict N ⊓
ground_closures"
shows "wfp_on {S. scl_without_backtrack⇧*⇧* initial_state S} scl_without_backtrack¯¯"
proof (rule wfp_on_subset)
show "wfp_on {S. invars S} scl_without_backtrack¯¯"
by (rule termination_scl_without_back_invars(1)[of β N,
folded invars_def scl_without_backtrack_def])
next
have "invars initial_state"
by (simp add: invars_def)

moreover have "invars S ⟹ invars S'"
if "scl_without_backtrack S S'"
for S S'
proof -
from that have "scl N β S S'"
by (auto simp: scl_without_backtrack_def scl_def)
thus "invars S ⟹ invars S'"
unfolding invars_def
using
scl_preserves_trail_atoms_lt
scl_preserves_trail_resolved_lits_pol
scl_preserves_trail_lits_ground
scl_preserves_trail_lits_from_clauses
scl_preserves_initial_lits_generalize_learned_trail_conflict
scl_preserves_ground_closures
by simp_all
qed
ultimately have "scl_without_backtrack⇧*⇧* initial_state S ⟹ invars S" for S
by (auto elim: rtranclp_induct)
thus "{S. scl_without_backtrack⇧*⇧* initial_state S} ⊆ {S. invars S}"
by auto
qed

corollary termination_stragegy_without_back:
fixes
N :: "('f, 'v) Term.term clause fset" and
β :: "('f, 'v) Term.term"
defines
"scl_without_backtrack ≡ propagate N β ⊔ decide N β ⊔ conflict N β ⊔ skip N β ⊔
factorize N β ⊔ resolve N β"
assumes strategy_stronger: "⋀S S'. strategy S S' ⟹ scl_without_backtrack S S'"
shows "wfp_on {S. strategy⇧*⇧* initial_state S} strategy¯¯"
proof (rule wfp_on_mono_strong)
show "wfp_on {S. strategy⇧*⇧* initial_state S} scl_without_backtrack¯¯"
proof (rule wfp_on_subset)
show "wfp_on {S. scl_without_backtrack⇧*⇧* initial_state S} scl_without_backtrack¯¯"
unfolding scl_without_backtrack_def
using termination_scl_without_back by metis
next
show "{S. strategy⇧*⇧* initial_state S} ⊆ {S. scl_without_backtrack⇧*⇧* initial_state S}"
using strategy_stronger
by (metis (no_types, opaque_lifting) Collect_mono mono_rtranclp)
qed
next
show "⋀S' S. strategy¯¯ S' S ⟹ scl_without_backtrack¯¯ S' S"
using strategy_stronger by simp
qed

subsection ‹Backtracking can only be done finitely often›

(* lemma ex_new_grounding_if_not_redudant:
assumes not_redundant: "¬ redundant R N C"
shows "∃C' ∈ grounding_of_cls C. C' ∉ grounding_of_clss N"
proof -
from not_redundant obtain C' I where
C'_in: "C' ∈ grounding_of_cls C" and
I_entails: "I ⊫s {D ∈ grounding_of_clss N. R D C' ∨ D = C'}" and
not_I_entails: "¬ I ⊫ C'"
using not_redundant[unfolded redundant_def ground_redundant_def, rule_format, simplified]
by (auto simp: is_ground_cls_if_in_grounding_of_cls)

from I_entails have "C' ∈ grounding_of_clss N ⟹ I ⊫ C'"
by (simp add: true_clss_def)
with not_I_entails have "C' ∉ grounding_of_clss N"
by argo
with C'_in show ?thesis
by metis
qed *)

(* lemma
assumes
regular_run: "(regular_scl N β)⇧*⇧* initial_state S0" and
conflict: "conflict N β S0 S1" and
resolution: "(skip N β ⊔ factorize N β ⊔ resolve N β)⇧+⇧+ S1 Sn" and
backtrack: "backtrack N β Sn Sn'" and
"transp lt"
defines
"trail_ord ≡ multp (trail_less_ex lt (map fst (state_trail S1)))" and
"U ≡ state_learned S1"
shows "(∃C γ. state_conflict Sn = Some (C, γ) ∧
(∃C' ∈ grounding_of_cls C. C' ∉ grounding_of_clss (fset U))) ∧
grounding_of_clss (fset U) ⊂ grounding_of_clss (fset (state_learned Sn'))"
proof -
from learned_clauses_in_regular_runs_static_order
obtain C γ where
conf_Sn: "state_conflict Sn = Some (C, γ)" and
not_redundant: "¬ redundant (⊂#) (fset N ∪ fset (state_learned S1)) C"
by auto

moreover have bex_grounding_not_in_U: "∃C' ∈ grounding_of_cls C. C' ∉ grounding_of_clss (fset U)"
using ex_new_grounding_if_not_redudant[OF not_redundant, folded U_def]
by (auto simp: grounding_of_clss_union)

moreover have "grounding_of_clss (fset U) ⊂ grounding_of_clss (fset (state_learned Sn'))"
proof -
have "state_learned Sn = state_learned S1"
using resolution
proof (induction Sn rule: tranclp_induct)
case (base y)
thus ?case
by (auto elim: skip.cases factorize.cases resolve.cases)
next
case (step y z)
from step.hyps have "state_learned z = state_learned y"
by (auto elim: skip.cases factorize.cases resolve.cases)
with step.IH show ?case
by simp
qed

moreover have "state_learned Sn' = finsert C (state_learned Sn)"
using backtrack conf_Sn
by (auto elim: backtrack.cases)

ultimately have "state_learned Sn' = finsert C U"
by (simp add: U_def)

show ?thesis
unfolding ‹state_learned Sn' = finsert C U›
proof (rule Set.psubsetI)
show "grounding_of_clss (fset U) ⊆ grounding_of_clss (fset (finsert C U))"
by (simp add: grounding_of_clss_insert)
next
show "grounding_of_clss (fset U) ≠ grounding_of_clss (fset (finsert C U))"
using bex_grounding_not_in_U by (auto simp: grounding_of_clss_insert)
qed
qed

ultimately show ?thesis
by simp
qed *)

definition fclss_no_dup :: "('f, 'v) Term.term ⇒ ('f, 'v) Term.term literal fset fset" where
"fclss_no_dup β = fPow (Abs_fset {L. atm_of L ≼⇩B β})"

lemma image_fset_fset_fPow_eq: "fset ` fset (fPow A) = Pow (fset A)"
proof (rule Set.equalityI)
show "fset ` fset (fPow A) ⊆ Pow (fset A)"
by (meson PowI fPowD image_subset_iff less_eq_fset.rep_eq)
next
show "Pow (fset A) ⊆ fset ` fset (fPow A)"
proof (rule Set.subsetI)
fix x assume "x ∈ Pow (fset A)"
moreover hence "finite x"
by (metis PowD finite_fset rev_finite_subset)
ultimately show "x ∈ fset ` fset (fPow A)"
unfolding image_iff
by (metis PowD fPowI fset_cases less_eq_fset.rep_eq mem_Collect_eq)
qed
qed

lemma
assumes "∀L ∈# C. count C L = 1"
shows "∃C'. C = mset_set C'"
using assms
by (metis count_eq_zero_iff count_mset_set(1) count_mset_set(3) finite_set_mset multiset_eqI)

lemma fmember_fclss_no_dup_if:
assumes "∀L |∈| C. atm_of L ≼⇩B β"
shows "C |∈| fclss_no_dup β"
proof -
show ?thesis
unfolding fclss_no_dup_def fPow_iff
proof (rule fsubsetI)
fix K assume "K |∈| C"
with assms show "K |∈| Abs_fset {L. atm_of L ≼⇩B β}"
using Abs_fset_inverse[simplified, OF finite_lits_less_eq_B]
by simp
qed
qed

definition ℳ_back :: " _ ⇒ ('f, 'v) state ⇒ ('f, 'v) Term.term literal fset fset" where
"ℳ_back β S = Abs_fset (fset (fclss_no_dup β) -
Abs_fset ` set_mset ` grounding_of_clss (fset (state_learned S)))"

lemma ℳ_back_after_regular_backtrack:
assumes
regular_run: "(regular_scl N β)⇧*⇧* initial_state S0" and
conflict: "conflict N β S0 S1" and
resolution: "(skip N β ⊔ factorize N β ⊔ resolve N β)⇧+⇧+ S1 Sn" and
backtrack: "backtrack N β Sn Sn'"
defines "U ≡ state_learned Sn"
shows
"∃C γ. state_conflict Sn = Some (C, γ) ∧
set_mset (C ⋅ γ) ∉ set_mset ` grounding_of_clss (fset N ∪ fset U)" and
"ℳ_back β Sn' |⊂| ℳ_back β Sn"
proof -
from regular_run have "(scl N β)⇧*⇧* initial_state S0"
by (induction S0 rule: rtranclp_induct)
(auto intro: scl_if_regular rtranclp.rtrancl_into_rtrancl)
with conflict have "(scl N β)⇧*⇧* initial_state S1"
by (meson regular_scl_if_conflict rtranclp.rtrancl_into_rtrancl scl_if_regular)
with resolution have scl_run: "(scl N β)⇧*⇧* initial_state Sn"
by (metis (no_types, lifting) Nitpick.rtranclp_unfold mono_rtranclp
regular_run_if_skip_factorize_resolve_run rtranclp_tranclp_tranclp scl_if_regular)

from scl_run have "ground_false_closures Sn"
by (induction Sn rule: rtranclp_induct)
(auto intro: scl_preserves_ground_false_closures)
hence "ground_closures Sn"
using ground_false_closures_def by blast

from scl_run have "trail_atoms_lt β Sn"
by (induction Sn rule: rtranclp_induct)
(auto intro: scl_preserves_trail_atoms_lt)

obtain C γ where
conf: "state_conflict Sn = Some (C, γ)" and
set_conf_not_in_set_groundings:
"set_mset (C ⋅ γ) ∉ set_mset ` grounding_of_clss (fset N ∪ fset (state_learned S1))"
using dynamic_non_redundancy_regular_scl[OF assms(1,2,3,4)]
using standard_lit_less_preserves_term_less
by metis

have 1: "state_learned Sn' = finsert C (state_learned Sn)"
using backtrack conf by (auto elim: backtrack.cases)

have 2: "state_learned Sn = state_learned S1"
using resolution
proof (induction Sn rule: tranclp_induct)
case (base y)
thus ?case
by (auto elim: skip.cases factorize.cases resolve.cases)
next
case (step y z)
from step.hyps(2) have "state_learned z = state_learned y"
by (auto elim: skip.cases factorize.cases resolve.cases)
with step.IH show ?case
by simp
qed
with conf set_conf_not_in_set_groundings show "∃C γ. state_conflict Sn = Some (C, γ) ∧
set_mset (C ⋅ γ) ∉ set_mset ` grounding_of_clss (fset N ∪ fset U)"
by (simp add: U_def)

have Diff_strict_subsetI: "x ∈ A ⟹ x ∈ B ⟹ A - B ⊂ A" for x A B
by auto

have "fset (fclss_no_dup β) - Abs_fset ` set_mset ` grounding_of_clss (fset (state_learned Sn')) =
fset (fclss_no_dup β) - Abs_fset ` set_mset ` grounding_of_clss (fset (state_learned Sn)) -
Abs_fset ` set_mset ` grounding_of_cls C"
unfolding 1 finsert.rep_eq grounding_of_clss_insert image_Un
by auto

also have "… ⊂
fset (fclss_no_dup β) - Abs_fset ` set_mset ` grounding_of_clss (fset (state_learned Sn))"
proof (rule Diff_strict_subsetI)
from ‹ground_closures Sn› have "C ⋅ γ ∈ grounding_of_cls C"
unfolding ground_closures_def conf
using grounding_of_cls_ground grounding_of_subst_cls_subset by blast
thus "Abs_fset (set_mset (C ⋅ γ)) ∈ Abs_fset ` set_mset ` grounding_of_cls C"
by blast
next
have Abs_fset_in_image_Abs_fset_iff: "Abs_fset A ∈ Abs_fset ` AA ⟷ A ∈ AA"
if "finite A ∧ (∀B ∈ AA. finite B)"
for A AA
apply (rule iffI)
using that
apply (metis Abs_fset_inverse imageE mem_Collect_eq)
using that
by blast

have "set_mset (C ⋅ γ) ∉ set_mset ` grounding_of_clss (fset (state_learned S1))"
using set_conf_not_in_set_groundings
by (auto simp: grounding_of_clss_union)
then have "Abs_fset (set_mset (C ⋅ γ)) ∉
Abs_fset ` set_mset ` grounding_of_clss (fset (state_learned Sn))"
unfolding 2
using Abs_fset_in_image_Abs_fset_iff
by (metis finite_set_mset image_iff)

moreover have "Abs_fset (set_mset (C ⋅ γ)) ∈ fset (fclss_no_dup β)"
proof (intro fmember_fclss_no_dup_if ballI)
fix L assume "L |∈| Abs_fset (set_mset (C ⋅ γ))"
hence "L ∈# C ⋅ γ"
by (metis fset_fset_mset fset_inverse)
moreover have "trail_false_cls (state_trail Sn) (C ⋅ γ)"
using ‹ground_false_closures Sn› conf by (auto simp: ground_false_closures_def)
ultimately show "atm_of L ≼⇩B β"
using ball_less_B_if_trail_false_and_trail_atoms_lt[OF _ ‹trail_atoms_lt β Sn›]
by metis
qed

ultimately show "Abs_fset (set_mset (C ⋅ γ)) ∈ fset (fclss_no_dup β) -
Abs_fset ` set_mset ` grounding_of_clss (fset (state_learned Sn))"
by simp
qed

finally show "ℳ_back β Sn' |⊂| ℳ_back β Sn"
unfolding ℳ_back_def
unfolding fminus_conv
by (simp add: Abs_fset_inverse[simplified])
qed

subsection ‹Regular SCL terminates›

theorem termination_regular_scl_invars:
fixes
N :: "('f, 'v) Term.term clause fset" and
β :: "('f, 'v) Term.term"
defines
"invars ≡ trail_atoms_lt β ⊓ trail_resolved_lits_pol ⊓ trail_lits_ground ⊓
trail_lits_from_clauses N ⊓ initial_lits_generalize_learned_trail_conflict N ⊓
ground_closures ⊓ ground_false_closures ⊓ sound_state N β ⊓
almost_no_conflict_with_trail N β ⊓
regular_conflict_resolution N β"
shows
"wfp_on {S. invars S} (regular_scl N β)¯¯"
proof (rule wfp_on_mono_strong)
fix S S' assume "(regular_scl N β)¯¯ S S'"
thus "(backtrack N β ⊔ (propagate N β ⊔ decide N β ⊔ conflict N β ⊔ skip N β ⊔ factorize N β ⊔
resolve N β))¯¯ S S'"
by (auto simp: regular_scl_def reasonable_scl_def scl_def)
next
show "wfp_on {S. invars S} (backtrack N β ⊔ (propagate N β ⊔ decide N β ⊔ conflict N β ⊔
skip N β ⊔ factorize N β ⊔ resolve N β))¯¯"
unfolding converse_join[of "backtrack N β"]
proof (rule wfp_on_sup_if_convertible_to_wfp, unfold mem_Collect_eq)
show "wfp_on {S. invars S} (propagate N β ⊔ decide N β ⊔ conflict N β ⊔ skip N β ⊔
factorize N β ⊔ resolve N β)¯¯"
using termination_scl_without_back_invars(1)[of β N]
by (auto simp: invars_def inf_assoc elim: wfp_on_subset)
next
show "wfp_on (ℳ_back β ` {S. invars S}) (|⊂|)"
proof (rule wfp_on_subset)
show "wfp (|⊂|)"
unfolding wfp_iff_wfP
by (rule wfP_pfsubset)
qed simp
next
fix S' S
assume "invars S'" and "invars S" and "(backtrack N β)¯¯ S' S"
moreover from ‹invars S› have "sound_state N β S"
by (simp add: invars_def)

moreover from ‹invars S› have "almost_no_conflict_with_trail N β S"
by (simp add: invars_def)

moreover from ‹invars S› have "regular_conflict_resolution N β S"
by (simp add: invars_def)

moreover from ‹invars S› have "ground_false_closures S"
by (simp add: invars_def)

ultimately obtain S0 S1 S2 S3 S4 where
reg_run: "(regular_scl N β)⇧*⇧* initial_state S0" and
propa: "propagate N β S0 S1" "regular_scl N β S0 S1" and
confl: "conflict N β S1 S2" and
facto: "(factorize N β)⇧*⇧* S2 S3" and
resol: "resolve N β S3 S4" and
reg_res: "(skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S4 S"
using before_regular_backtrack by blast

show "ℳ_back β S' |⊂| ℳ_back β S"
proof (rule ℳ_back_after_regular_backtrack)
show "(regular_scl N β)⇧*⇧* initial_state S1"
using reg_run propa(2) by simp
next
show "conflict N β S1 S2"
by (rule confl)
next
have "(skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S2 S3"
using facto
by (rule mono_rtranclp[rule_format, rotated]) simp
also have "(skip N β ⊔ factorize N β ⊔ resolve N β)⇧+⇧+ S3 S4"
using resol by auto
finally show "(skip N β ⊔ factorize N β ⊔ resolve N β)⇧+⇧+ S2 S"
using reg_res by simp
next
from ‹(backtrack N β)¯¯ S' S› show "backtrack N β S S'"
by simp
qed
next
fix S' S
assume "invars S'" and "invars S" and
"(propagate N β ⊔ decide N β ⊔ conflict N β ⊔ skip N β ⊔ factorize N β ⊔
resolve N β)¯¯ S' S"
hence "state_learned S' = state_learned S"
by (auto elim: propagate.cases decide.cases conflict.cases skip.cases factorize.cases
resolve.cases)
hence "ℳ_back β S' = ℳ_back β S"
by (simp add: ℳ_back_def)
thus "ℳ_back β S' |⊂| ℳ_back β S ∨ ℳ_back β S' = ℳ_back β S" ..
qed
qed

corollary termination_regular_scl:
fixes
N :: "('f, 'v) Term.term clause fset" and
β :: "('f, 'v) Term.term"
defines
"invars ≡ trail_atoms_lt β ⊓ trail_resolved_lits_pol ⊓ trail_lits_ground ⊓
trail_lits_from_clauses N ⊓ initial_lits_generalize_learned_trail_conflict N ⊓
ground_closures ⊓ ground_false_closures ⊓ sound_state N β ⊓
almost_no_conflict_with_trail N β ⊓
regular_conflict_resolution N β"
shows "wfp_on {S. (regular_scl N β)⇧*⇧* initial_state S} (regular_scl N β)¯¯"
proof (rule wfp_on_subset)
show "wfp_on {S. invars S} (regular_scl N β)¯¯"
by (rule termination_regular_scl_invars(1)[of β N, folded invars_def])
next
note rea_to_scl = scl_if_reasonable
note reg_to_rea = reasonable_if_regular
note reg_to_scl = reg_to_rea[THEN rea_to_scl]

have "invars initial_state"
by (simp add: invars_def)

moreover have "⋀S S'. regular_scl N β S S' ⟹ invars S ⟹ invars S'"
unfolding invars_def
using
reg_to_scl[THEN scl_preserves_trail_atoms_lt]
reg_to_scl[THEN scl_preserves_trail_resolved_lits_pol]
reg_to_scl[THEN scl_preserves_trail_lits_ground]
reg_to_scl[THEN scl_preserves_trail_lits_from_clauses]
reg_to_scl[THEN scl_preserves_initial_lits_generalize_learned_trail_conflict]
reg_to_scl[THEN scl_preserves_ground_closures]
reg_to_scl[THEN scl_preserves_ground_false_closures]
reg_to_scl[THEN scl_preserves_sound_state]
regular_scl_preserves_almost_no_conflict_with_trail
regular_scl_preserves_regular_conflict_resolution
by simp
ultimately have "(regular_scl N β)⇧*⇧* initial_state S ⟹ invars S" for S
by (auto elim: rtranclp_induct)
thus "{S. (regular_scl N β)⇧*⇧* initial_state S} ⊆ {S. invars S}"
by auto
qed

corollary termination_strategy:
fixes
N :: "('f, 'v) Term.term clause fset" and
β :: "('f, 'v) Term.term"
assumes strategy_restricts_regular_scl: "⋀S S'. strategy S S' ⟹ regular_scl N β S S'"
shows "wfp_on {S. strategy⇧*⇧* initial_state S} strategy¯¯"
proof (rule wfp_on_mono_strong)
show "wfp_on {S. strategy⇧*⇧* initial_state S} (regular_scl N β)¯¯"
proof (rule wfp_on_subset)
show "wfp_on {S. (regular_scl N β)⇧*⇧* initial_state S} (regular_scl N β)¯¯"
using termination_regular_scl by metis
next
show "{S. strategy⇧*⇧* initial_state S} ⊆ {S. (regular_scl N β)⇧*⇧* initial_state S}"
using strategy_restricts_regular_scl
by (metis (no_types, opaque_lifting) Collect_mono mono_rtranclp)
qed
next
show "⋀S' S. strategy¯¯ S' S ⟹ (regular_scl N β)¯¯ S' S"
using strategy_restricts_regular_scl by simp
qed

end

end```