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