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