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


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 
      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
      "initial_lits_generalize_learned_trail_conflict N S" and
      "ground_closures S"
      "initial_lits_generalize_learned_trail_conflict N S'"
      by (simp_all add: invars_def)

    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' γ C0 C1 Γ μ)

        have "L ⋅l μ ⋅l γ = L ⋅l γ"
        proof -
          have "is_unifiers γ {atm_of ` set_mset (add_mset L C1)}"
            unfolding C1 = {#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 C1)}[unfolded is_imgu_def, THEN conjunct2]
            by simp
          thus ?thesis
            by (metis subst_lit_comp_subst)
        qed

        have "ℳ_prop_deci β ((L ⋅l γ, Some (C0  μ, 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)"
          by (simp add: Wellfounded.wfPUNIVI)
      next
        show "wfp (|⊂|)"
          by (rule wfP_pfsubset)
      next
        show "wfp (λx y. (x, y)  lenlex {(x :: _ :: wellorder, y). x < y})"
          unfolding Wellfounded.wfP_wf_eq
          using wf_lenlex
          using wf by blast
      next
        show "wfp ((<) :: nat  nat  bool)"
          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 
      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_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_antimono_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 simp
  

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 
      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_antimono_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 (|⊂|)"
        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 simp

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 
      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_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_antimono_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 simp

end

end