Theory Correct_Termination

theory Correct_Termination
  imports SCL_FOL
begin

context scl_fol_calculus begin

lemma not_satisfiable_if_sound_state_conflict_bottom:
  assumes sound_S: "sound_state N β S" and conflict_S: "state_conflict S = Some ({#}, γ)"
  shows "¬ satisfiable (grounding_of_clss (fset N))"
proof -
  from sound_S conflict_S have "fset N ⊫𝒢e {{#}}"
    unfolding sound_state_def state_conflict_def by auto
  thus ?thesis by simp
qed

lemma propagate_if_conflict_follows_decide:
  assumes
    trail_lt_β: "trail_atoms_lt β S2" and
    no_conf: "∄S1. conflict N β S0 S1" and deci: "decide N β S0 S2" and conf: "conflict N β S2 S3"
  shows "∃S4. propagate N β S0 S4"
proof -
  from deci obtain L γ Γ U where
    S0_def: "S0 = (Γ, U, None)" and
    S2_def: "S2 = (trail_decide Γ (L ⋅l γ), U, None)" and
    "is_ground_lit (L ⋅l γ)" and
    "¬ trail_defined_lit Γ (L ⋅l γ)" and
    "atm_of L ⋅a γ ≼B β"
    by (elim decide.cases) blast
  
  from conf S2_def obtain D γD where
    S3_def: "S3 = (trail_decide Γ (L ⋅l γ), U, Some (D, γD))" and
    D_in: "D |∈| N |∪| U" and
    ground_D_σ: "is_ground_cls (D ⋅ γD)" and
    tr_Γ_L_false_D: "trail_false_cls (trail_decide Γ (L ⋅l γ)) (D ⋅ γD)"
    by (auto elim: conflict.cases)

  have "vars_cls D ⊆ subst_domain γD"
    using ground_D_σ vars_cls_subset_subst_domain_if_grounding by blast

  moreover have "¬ trail_false_cls Γ (D ⋅ γD)"
    using not_trail_false_ground_cls_if_no_conflict[OF no_conf] D_in
    by (simp add: S0_def ground_D_σ)

  ultimately have "- (L ⋅l γ) ∈# D ⋅ γD"
    using tr_Γ_L_false_D
    by (metis subtrail_falseI decide_lit_def)

  then obtain D' L' where D_def: "D = add_mset L' D'" and "- (L ⋅l γ) = L' ⋅l γD"
    by (metis Melem_subst_cls multi_member_split)

  define C0 where
    "C0 = {#K ∈# D'. K ⋅l γD ≠ L' ⋅l γD#}"

  define C1 where
    "C1 = {#K ∈# D'. K ⋅l γD = L' ⋅l γD#}"

  have ball_atms_lt_β: "∀K ∈# D ⋅ γD. atm_of K ≼B β"
  proof (rule ballI)
    fix K assume "K ∈# D ⋅ γD"
    hence "K = L' ⋅l γD ∨ (K ∈# D' ⋅ γD)"
      by (simp add: D_def)
    thus "atm_of K ≼B β"
    proof (rule disjE)
      assume "K = L' ⋅l γD"
      thus ?thesis
        using ‹- (L ⋅l γ) = L' ⋅l γD› ‹atm_of L ⋅a γ ≼B β›
        by (metis  atm_of_eq_uminus_if_lit_eq atm_of_subst_lit)
    next
      have trail_lt_β': "∀A ∈ atm_of ` fst ` set (trail_decide Γ (L ⋅l γ)). A ≼B β"
        using trail_lt_β by (simp add: trail_atoms_lt_def S2_def)

      assume K_in: "K ∈# D' ⋅ γD"
      hence "atm_of K ∈ atm_of ` fst ` set (trail_decide Γ (L ⋅l γ))"
        using tr_Γ_L_false_D[unfolded D_def]
        by (metis D_def ‹K ∈# D ⋅ γD› atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set
            trail_false_cls_def trail_false_lit_def)
      moreover from trail_lt_β have "∀A ∈ atm_of ` fst ` set (trail_decide Γ (L ⋅l γ)). A ≼B β"
        by (simp add: trail_atoms_lt_def S2_def)
      ultimately show ?thesis
        by blast
    qed
  qed

  have tr_false_C1: "trail_false_cls Γ (C0 ⋅ γD)"
  proof (rule subtrail_falseI)
    show "trail_false_cls ((L ⋅l γ, None) # Γ) (C0 ⋅ γD)"
      unfolding C0_def trail_false_cls_def
      apply (rule ballI)
      apply (rule tr_Γ_L_false_D[unfolded D_def trail_false_cls_def decide_lit_def, rule_format])
      by auto
  next
    show "- (L ⋅l γ) ∉# C0 ⋅ γD"
      unfolding C0_def
      using ‹- (L ⋅l γ) = L' ⋅l γD› by fastforce
  qed

  have not_def_L'_ρ_σρ: "¬ trail_defined_lit Γ (L' ⋅l γD)"
    using ‹¬ trail_defined_lit Γ (L ⋅l γ)›
    by (metis ‹- (L ⋅l γ) = L' ⋅l γD› trail_defined_lit_iff_defined_uminus)

  obtain xs where "mset xs = add_mset L' C1"
    using ex_mset by auto
  hence set_xs_conv:
    "set xs = set_mset (add_mset L' C1)"
    by (metis set_mset_mset)

  have "unifiers (set (pairs (map atm_of xs))) ≠ {}"
  proof (rule not_empty_if_mem)
    have "set (pairs (map atm_of xs)) =
      atm_of ` set_mset (add_mset L' C1) × atm_of ` set_mset (add_mset L' C1)"
      unfolding set_pairs list.set_map set_xs_conv by simp
    also have "… =
      atm_of ` insert L' (set_mset C1) × atm_of ` insert L' (set_mset C1)"
      unfolding set_mset_add_mset_insert by simp
    also have "… =
      atm_of ` insert L' {K. K ∈# D' ∧ K ⋅l γD = L' ⋅l γD} ×
      atm_of ` insert L' {K. K ∈# D' ∧ K ⋅l γD = L' ⋅l γD}"
      unfolding C1_def set_mset_filter by simp
    finally have set_pairs_xs_simp: "set (pairs (map atm_of xs)) =
      atm_of ` insert L' {K. K ∈# D' ∧ K ⋅l γD = L' ⋅l γD} ×
      atm_of ` insert L' {K. K ∈# D' ∧ K ⋅l γD = L' ⋅l γD}"
      by assumption
      
    show "γD ∈ unifiers (set (pairs (map atm_of xs)))"
      unfolding unifiers_def mem_Collect_eq
    proof (rule ballI)
      fix p assume p_in: "p ∈ set (pairs (map atm_of xs))"
      then obtain K1 K2 where p_def: "p = (atm_of K1, atm_of K2)" and
        "K1 = L' ∨ K1 ∈ {K. K ∈# D' ∧ K ⋅l γD = L' ⋅l γD}" and
        "K2 = L' ∨ K2 ∈ {K. K ∈# D' ∧ K ⋅l γD = L' ⋅l γD}"
        by (auto simp: set_pairs_xs_simp)
      hence "K1 ⋅l γD = L' ⋅l γD ∧ K2 ⋅l γD = L' ⋅l γD"
        by auto
      thus "fst p ⋅a γD = snd p ⋅a γD"
        unfolding p_def prod.sel
        by (metis atm_of_subst_lit)
    qed
  qed
  then obtain ys where
    unify_pairs: "unify (pairs (map atm_of xs)) [] = Some ys"
    using ex_unify_if_unifiers_not_empty[OF _ refl] by blast

  define μ where
    "μ = subst_of ys"

  have imgu_μ: "is_imgu μ {atm_of ` set_mset (add_mset L' C1)}"
  proof (intro is_imgu_if_mgu_sets[unfolded mgu_sets_def] exI conjI)
    show "set (map set [(map atm_of xs)]) = {atm_of ` set_mset (add_mset L' C1)}"
      by (simp add: set_xs_conv)
  next
    show "map_option subst_of (unify (concat (map pairs [map atm_of xs])) []) = Some μ"
      by (simp add: unify_pairs μ_def)
  qed

  show ?thesis
    using propagateI[OF D_in D_def, of γD, unfolded subst_cls_comp_subst subst_lit_comp_subst,
      OF ground_D_σ ball_atms_lt_β C0_def C1_def tr_false_C1 not_def_L'_ρ_σρ imgu_μ]   
    unfolding S0_def by blast
qed

theorem correct_termination:
  fixes gnd_N and gnd_N_lt_β
  assumes
    sound_S: "sound_state N β S" and
    invars: "trail_atoms_lt β S" "trail_propagated_wf (state_trail S)" "trail_lits_consistent S"
      "ground_false_closures S" and
    no_new_conflict: "∄S'. conflict N β S S'" and
    no_new_propagate: "∄S'. propagate N β S S'" and
    no_new_decide: "∄S'. decide N β S S' ∧ (∄S''. conflict N β S' S'')" and
    no_new_skip: "∄S'. skip N β S S'" and
    no_new_resolve: "∄S'. resolve N β S S'" and
    no_new_backtrack: "∄S'. backtrack N β S S' ∧
      is_shortest_backtrack (fst (the (state_conflict S))) (state_trail S) (state_trail S')"
  defines
    "gnd_N ≡ grounding_of_clss (fset N)" and
    "gnd_N_lt_β ≡ {C ∈ gnd_N. ∀L ∈# C. atm_of L ≼B β}"
  shows "¬ satisfiable gnd_N ∧ (∃γ. state_conflict S = Some ({#}, γ)) ∨
    satisfiable gnd_N_lt_β ∧ trail_true_clss (state_trail S) gnd_N_lt_β"
proof -
  obtain Γ U u where S_def: "S = (Γ, U, u)"
    using prod_cases3 by blast

  from sound_S have sound_Γ: "sound_trail N Γ"
    by (simp_all add: S_def sound_state_def)

  from ‹ground_false_closures S› have "ground_closures S"
    by (simp add: ground_false_closures_def)

  have trail_consistent: "trail_consistent (state_trail S)"
    using ‹trail_lits_consistent S› by (simp add: trail_lits_consistent_def)

  show ?thesis
  proof (cases u)
    case u_def: None
    hence "state_conflict S = None"
      by (simp add: S_def)

    have tr_true: "trail_true_clss Γ gnd_N_lt_β"
      unfolding trail_true_clss_def gnd_N_lt_β_def gnd_N_def
    proof (rule ballI, unfold mem_Collect_eq, erule conjE)
      fix C assume C_in: "C ∈ grounding_of_clss (fset N)" and C_lt_β: "∀L ∈# C. atm_of L ≼B β"

      from C_in have "is_ground_cls C"
        by (rule grounding_ground)

      from C_in obtain C' γ where C'_in: "C' |∈| N" and C_def: "C = C' ⋅ γ"
        unfolding grounding_of_clss_def grounding_of_cls_def
        by (smt (verit, ccfv_threshold) UN_iff mem_Collect_eq)

      from no_new_decide have Γ_defined_C: "trail_defined_cls Γ C"
      proof (rule contrapos_np)
        assume "¬ trail_defined_cls Γ C"
        then obtain L where L_in: "L ∈# C" and "¬ trail_defined_lit Γ L"
          using trail_defined_cls_def by blast
        then obtain L' where L'_in: "L' ∈# C'" and "L = L' ⋅l γ"
          using C_def Melem_subst_cls by blast

        have deci: "decide N β (Γ, U, None) (trail_decide Γ (L' ⋅l γ), U, None)"
        proof (rule decideI)
          show "is_ground_lit (L' ⋅l γ)"
            using L_in ‹L = L' ⋅l γ› ‹is_ground_cls C› is_ground_cls_def by blast
        next
          show "¬ trail_defined_lit Γ (L' ⋅l γ)"
            using ‹L = L' ⋅l γ› ‹¬ trail_defined_lit Γ L› by blast
        next
          show "atm_of L' ⋅a γ ≼B β"
            using ‹L = L' ⋅l γ› C_lt_β L_in by fastforce
        qed

        moreover have "∄S''. conflict N β (trail_decide Γ (L' ⋅l γ), U, None) S''"
        proof (rule notI, elim exE)
          fix S''
          assume conf: "conflict N β (trail_decide Γ (L' ⋅l γ), U, None) S''"
          moreover have "trail_atoms_lt β (trail_decide Γ (L' ⋅l γ), U, None)"
            using decide_preserves_trail_atoms_lt[OF deci] ‹trail_atoms_lt β S›
            by (simp add: S_def u_def)
          ultimately have "∃S4. propagate N β S S4"
            using propagate_if_conflict_follows_decide[OF _ no_new_conflict]
            using S_def deci u_def by blast
          with no_new_propagate show False
            by metis
        qed

        ultimately show "∃S'. decide N β S S' ∧ (∄S''. conflict N β S' S'')"
          by (auto simp : S_def u_def)
      qed

      show "trail_true_cls Γ C"
        using Γ_defined_C[THEN trail_true_or_false_cls_if_defined]
      proof (elim disjE)
        show "trail_true_cls Γ C ⟹ trail_true_cls Γ C"
          by assumption
      next
        assume "trail_false_cls Γ C"

        define ρ :: "'v ⇒ ('f, 'v) term" where
          "ρ = renaming_wrt (fset (N |∪| U |∪| clss_of_trail Γ))"

        define γρ where
          "γρ = rename_subst_domain ρ (restrict_subst_domain (vars_cls C') γ)"

        have "conflict N β (Γ, U, None) (Γ, U, Some (C', restrict_subst_domain (vars_cls C') γ))"
        proof (rule conflictI)
          show "C' |∈| N |∪| U"
            using C'_in by simp
        next
          show "is_ground_cls (C' ⋅ restrict_subst_domain (vars_cls C') γ)"
            using ‹is_ground_cls C›[unfolded C_def]
            by (simp add: subst_cls_restrict_subst_domain)
        next
          show "trail_false_cls Γ (C' ⋅ restrict_subst_domain (vars_cls C') γ)"
            using ‹trail_false_cls Γ C›[unfolded C_def]
            by (simp add: subst_cls_restrict_subst_domain)
        qed
        with no_new_conflict have False
          by (simp add: S_def u_def)
        thus "trail_true_cls Γ C" ..
      qed
    qed

    moreover have "satisfiable gnd_N_lt_β"
      unfolding true_clss_def gnd_N_lt_β_def
    proof (intro exI ballI, unfold mem_Collect_eq, elim conjE)
      fix C
      have "trail_consistent Γ"
        using S_def trail_consistent by auto
      show "C ∈ gnd_N ⟹ ∀L ∈# C. atm_of L ≼B β ⟹ trail_interp Γ ⊫ C"
        using tr_true[unfolded gnd_N_lt_β_def]
        using trail_interp_cls_if_trail_true[OF ‹trail_consistent Γ›]
        by (simp add: trail_true_clss_def)
    qed

    ultimately show ?thesis
      by (simp add: S_def)
  next
    case (Some Cl)
    then obtain C γC where u_def: "u = Some (C, γC)" by force

    from ‹ground_false_closures S› have Γ_false_C_γC: "trail_false_cls Γ (C ⋅ γC)"
      by (simp add: S_def u_def ground_false_closures_def)

    show ?thesis
    proof (cases "C = {#}")
      case True
      hence "¬ satisfiable gnd_N ∧ (∃γ. state_conflict S = Some ({#}, γ))"
        using S_def u_def not_satisfiable_if_sound_state_conflict_bottom[OF sound_S]
        by (simp add: gnd_N_def)
      thus ?thesis by simp
    next
      case C_not_empty: False
      have False
      proof (cases Γ)
        case Nil
        with Γ_false_C_γC show False
          using C_not_empty by simp
      next
        case (Cons Ln Γ')
        then obtain KΓ n where Γ_def: "Γ = (KΓ, n) # Γ'"
          by fastforce

        show False
        proof (cases "- KΓ ∈# C ⋅ γC")
          case True ― ‹Literal cannot be skipped›
          then obtain C' L where C_def: "C = add_mset L C'" and K_γ: "L ⋅l γC = - KΓ"
            by (metis Melem_subst_cls multi_member_split)
          hence L_eq_uminus_K_γ: "KΓ = - (L ⋅l γC)"
            by simp

          show False
          proof (cases n)
            case None ― ‹Conflict clause can be backtracked›
            hence Γ_def: "Γ = trail_decide Γ' (- (L ⋅l γC))"
              by (simp add: Γ_def L_eq_uminus_K_γ decide_lit_def)

            from suffix_shortest_backtrack[of "add_mset L C'" Γ'] obtain Γ'' where
              Γ'_def: "Γ' = Γ'' @ shortest_backtrack (add_mset L C') Γ'"
              using suffixE by blast

            define S' :: "('f, 'v) state" where
              "S' = (shortest_backtrack (add_mset L C') Γ', finsert (add_mset L C') U, None)"

            have "backtrack N β S S'"
              unfolding S_def[unfolded u_def C_def] S'_def
            proof (rule backtrackI[OF _ refl])
              show "Γ = trail_decide (Γ'' @ shortest_backtrack (add_mset L C') Γ') (- (L ⋅l γC))"
                using Γ_def Γ'_def by simp
            next
              show "∄γ. is_ground_cls (add_mset L C' ⋅ γ) ∧
                trail_false_cls (shortest_backtrack (add_mset L C') Γ') (add_mset L C' ⋅ γ)"
                using ex_conflict_shortest_backtrack[of "add_mset L C'", simplified]
                by (simp add: ex_conflict_def)
            qed
            moreover have "is_shortest_backtrack (fst (the (state_conflict S)))
              (state_trail S) (state_trail S')"
              unfolding S_def[unfolded u_def C_def] S'_def
              apply simp
              using is_shortest_backtrack_shortest_backtrack[of "add_mset L C'", simplified]
              using Γ_def Γ_false_C_γC
              by (metis (no_types, lifting) C_def ‹S = (Γ, U, Some (add_mset L C', γC))›
                  ‹ground_closures S› ex_conflict_def ground_closures_def is_shortest_backtrack_def
                  state_conflict_simp suffix_Cons)
              (* by (metis C_def Γ_def Γ_false_C_γC ‹S = (Γ, U, Some (add_mset L C', γC))›
                  ‹ground_closures S› ex_conflict_def ground_closures_def is_shortest_backtrack_def
                  state_proj_simp(3) suffix_Cons) *)
            ultimately show False
              using no_new_backtrack by metis
          next
            case Some ― ‹Literal can be resolved›
            then obtain D K γD where n_def: "n = Some (D, K, γD)"
              by (metis prod_cases3)
            with ‹trail_propagated_wf (state_trail S)› have L_def: "KΓ = K ⋅l γD"
              by (simp add: Γ_def S_def trail_propagated_wf_def)
            hence 1: "Γ = trail_propagate Γ' K D γD"
              using Γ_def n_def
              by (simp add: propagate_lit_def)

            from ‹ground_closures S› have
              ground_conf: "is_ground_cls (add_mset L C' ⋅ γC)" and
              ground_prop: "is_ground_cls (add_mset K D ⋅ γD)"
              unfolding S_def ground_closures_def
              by (simp_all add: 1 C_def u_def ground_closures_def propagate_lit_def)

            define ρ :: "'v ⇒ ('f, 'v) Term.term" where
              "ρ = renaming_wrt {add_mset K D}"

            have ren_ρ: "is_renaming ρ"
              unfolding ρ_def
              by (rule is_renaming_renaming_wrt) simp
            hence "∀x. is_Var (ρ x)" "inj ρ"
              by (simp_all add: is_renaming_iff)

            have disjoint_vars: "⋀C. vars_cls (C ⋅ ρ) ∩ vars_cls (add_mset K D ⋅ Var) = {}"
              by (simp add: ρ_def vars_cls_subst_renaming_disj)

            have 2: "K ⋅l γD = - (L ⋅l γC)"
              using K_γ L_def by fastforce

            let ?γD' = "restrict_subst_domain (vars_cls (add_mset K D)) γD"
    
            have "K ⋅l ?γD' = K ⋅l γD" and "D ⋅ ?γD' = D ⋅ γD"
              by (simp_all add: subst_lit_restrict_subst_domain subst_cls_restrict_subst_domain)
            hence "K ⋅l ?γD' = - (L ⋅l γC)" and ground_prop': "is_ground_cls (add_mset K D ⋅ ?γD')"
              using 2 ground_prop by simp_all
    
            have dom_γD': "subst_domain ?γD' ⊆ vars_cls (add_mset K D)"
              by simp
    
            let ?γ = "λx.
              if x ∈ vars_cls (add_mset L C' ⋅ ρ) then
                rename_subst_domain ρ γC x
              else
                γD x"
            have "L ⋅l ρ ⋅l ?γ = L ⋅l γC" and "K ⋅l ?γ = K ⋅l γD"
              using merge_of_renamed_groundings[OF ren_ρ is_renaming_id_subst disjoint_vars
                  ground_conf ground_prop is_grounding_merge_if_mem_then_else]
              unfolding rename_subst_domain_Var_lhs
              by simp_all

            then have "atm_of L ⋅a ρ ⋅a ?γ = atm_of K ⋅a ?γ"
              by (smt (verit, best) "2" atm_of_uminus subst_lit_id_subst atm_of_subst_lit)
            then obtain μ where "Unification.mgu (atm_of L ⋅a ρ) (atm_of K) = Some μ"
              using ex_mgu_if_subst_apply_term_eq_subst_apply_term
              by blast
            hence imgu_μ: "is_imgu μ {{atm_of L ⋅a ρ, atm_of K ⋅a Var}}"
              by (simp add: is_imgu_if_mgu_eq_Some)

            have "∃S. resolve N β (Γ, U, Some (add_mset L C', γC)) S"
              using resolveI[OF 1 2 ren_ρ is_renaming_id_subst disjoint_vars imgu_μ
                  is_grounding_merge_if_mem_then_else] ..
            with no_new_resolve show False
              by (metis C_def S_def u_def)
          qed
        next
          case False ― ‹Literal can be skipped›
          hence "skip N β ((KΓ, n) # Γ', U, Some (C, γC)) (Γ', U, Some (C, γC))"
            by (rule skipI[of KΓ C γC N β n Γ' U])
          with no_new_skip show False
            by (metis S_def Γ_def u_def)
        qed
      qed
      thus ?thesis ..
    qed
  qed
qed

corollary correct_termination_strategy:
  fixes gnd_N and gnd_N_lt_β
  assumes
    run: "(strategy N β)** initial_state S" and
    no_step: "∄S'. strategy N β S S'" and
    strategy_restricted_by_min_back:
      "⋀S S'. shortest_backtrack_strategy regular_scl N β S S' ⟹ strategy N β S S'" and
    strategy_preserves_invars:
      "⋀N β S S'. strategy N β S S' ⟹ sound_state N β S ⟹ sound_state N β S'"
      "⋀N β S S'. strategy N β S S' ⟹ trail_atoms_lt β S ⟹ trail_atoms_lt β S'"
      "⋀N β S S'. strategy N β S S' ⟹ trail_propagated_or_decided' N β S ⟹ trail_propagated_or_decided' N β S'"
      "⋀N β S S'. strategy N β S S' ⟹ trail_lits_consistent S ⟹ trail_lits_consistent S'"
      "⋀N β S S'. strategy N β S S' ⟹ ground_false_closures S ⟹ ground_false_closures S'"
  defines
    "gnd_N ≡ grounding_of_clss (fset N)" and
    "gnd_N_lt_β ≡ {C ∈ gnd_N. ∀L ∈# C. atm_of L ≼B β}"
  shows "¬ satisfiable gnd_N ∧ (∃γ. state_conflict S = Some ({#}, γ)) ∨
    satisfiable gnd_N_lt_β ∧ trail_true_clss (state_trail S) gnd_N_lt_β"
proof -
  from no_step have no_step': "∄S'. shortest_backtrack_strategy regular_scl N β S S'"
  proof (rule contrapos_nn)
    show "∃S'. shortest_backtrack_strategy regular_scl N β S S' ⟹ ∃S'. strategy N β S S'"
      using strategy_restricted_by_min_back by metis
  qed

  show ?thesis
  proof (rule correct_termination[of N β S, folded gnd_N_def, folded gnd_N_lt_β_def])
    from run show "sound_state N β S"
      by (induction S rule: rtranclp_induct) (auto intro: strategy_preserves_invars(1))
  next
    from run show "trail_atoms_lt β S"
      by (induction S rule: rtranclp_induct) (auto intro: strategy_preserves_invars(2))
  next
    from run have "trail_propagated_or_decided' N β S"
      by (induction S rule: rtranclp_induct) (auto intro: strategy_preserves_invars(3))
    thus "trail_propagated_wf (state_trail S)"
      by (simp add: trail_propagated_or_decided'_def
          trail_propagated_wf_if_trail_propagated_or_decided)
  next
    from run show "trail_lits_consistent S"
      by (induction S rule: rtranclp_induct) (auto intro: strategy_preserves_invars(4))
  next
    from run show "ground_false_closures S"
      by (induction S rule: rtranclp_induct) (auto intro: strategy_preserves_invars(5))
  next
    from no_step' show "∄S'. conflict N β S S'"
      unfolding shortest_backtrack_strategy_def regular_scl_def reasonable_scl_def scl_def
      using backtrack_well_defined(3) by blast
  next
    from no_step' show "∄S'. propagate N β S S'"
      unfolding shortest_backtrack_strategy_def regular_scl_def reasonable_scl_def scl_def
      using backtrack_well_defined(3) propagate_well_defined(1) propagate_well_defined(6) by blast
  next
    from no_step' show "∄S'. decide N β S S' ∧ (∄S''. conflict N β S' S'')"
      unfolding shortest_backtrack_strategy_def regular_scl_def reasonable_scl_def scl_def
      using backtrack_well_defined(2) backtrack_well_defined(3) by blast
  next
    from no_step' show "∄S'. skip N β S S'"
      unfolding shortest_backtrack_strategy_def regular_scl_def reasonable_scl_def scl_def
      using backtrack_well_defined(3) backtrack_well_defined(4) skip_well_defined(2) by blast
  next
    from no_step' show "∄S'. resolve N β S S'"
      unfolding shortest_backtrack_strategy_def regular_scl_def reasonable_scl_def scl_def
      using backtrack_well_defined(3) resolve_well_defined(2) resolve_well_defined(5) by blast
  next
    from no_step' show "∄S'. backtrack N β S S' ∧
    is_shortest_backtrack (fst (the (state_conflict S))) (state_trail S) (state_trail S')"
      unfolding shortest_backtrack_strategy_def scl_def regular_scl_def reasonable_scl_def
      using backtrack_well_defined(2) backtrack_well_defined(3) by blast
  qed
qed

corollary correct_termination_scl_run:
  fixes gnd_N and gnd_N_lt_β
  assumes
    run: "(scl N β)** initial_state S" and
    no_step: "∄S'. scl N β S S'"
  defines
    "gnd_N ≡ grounding_of_clss (fset N)" and
    "gnd_N_lt_β ≡ {C ∈ gnd_N. ∀L ∈# C. atm_of L ≼B β}"
  shows "¬ satisfiable gnd_N ∧ (∃γ. state_conflict S = Some ({#}, γ)) ∨
    satisfiable gnd_N_lt_β ∧ trail_true_clss (state_trail S) gnd_N_lt_β"
proof (rule correct_termination_strategy[of _ N β, folded gnd_N_def, folded gnd_N_lt_β_def])
  show "(scl N β)** initial_state S"
    by (rule run)
next
  show "∄S'. scl N β S S'"
    by (rule no_step)
next
  show "⋀S S'. shortest_backtrack_strategy regular_scl N β S S' ⟹ scl N β S S'"
    by (simp add: regular_scl_if_shortest_backtrack_strategy scl_if_regular)
next
  show "⋀N β S S'. scl N β S S' ⟹ sound_state N β S ⟹ sound_state N β S'"
    using scl_preserves_sound_state by simp
next
  show "⋀N β S S'. scl N β S S' ⟹ trail_atoms_lt β S ⟹ trail_atoms_lt β S'"
    using scl_preserves_trail_atoms_lt by simp
next
  show "⋀N β S S'. scl N β S S' ⟹ trail_propagated_or_decided' N β S ⟹
    trail_propagated_or_decided' N β S'"
    using scl_preserves_trail_propagated_or_decided by simp
next
  show "⋀N β S S'. scl N β S S' ⟹ trail_lits_consistent S ⟹ trail_lits_consistent S'"
    using scl_preserves_trail_lits_consistent by simp
next
  show "⋀N β S S'. scl N β S S' ⟹ ground_false_closures S ⟹ ground_false_closures S'"
    using scl_preserves_ground_false_closures by simp
qed

corollary correct_termination_reasonable_scl_run:
  fixes gnd_N and gnd_N_lt_β
  assumes
    run: "(reasonable_scl N β)** initial_state S" and
    no_step: "∄S'. reasonable_scl N β S S'"
  defines
    "gnd_N ≡ grounding_of_clss (fset N)" and
    "gnd_N_lt_β ≡ {C ∈ gnd_N. ∀L ∈# C. atm_of L ≼B β}"
  shows "¬ satisfiable gnd_N ∧ (∃γ. state_conflict S = Some ({#}, γ)) ∨
    satisfiable gnd_N_lt_β ∧ trail_true_clss (state_trail S) gnd_N_lt_β"
proof (rule correct_termination_strategy[of _ N β, folded gnd_N_def, folded gnd_N_lt_β_def])
  show "(reasonable_scl N β)** initial_state S"
    by (rule run)
next
  show "∄S'. reasonable_scl N β S S'"
    by (rule no_step)
next
  show "⋀S S'. shortest_backtrack_strategy regular_scl N β S S' ⟹ reasonable_scl N β S S'"
    by (simp add: reasonable_if_regular regular_scl_if_shortest_backtrack_strategy)
next
  show "⋀N β S S'. reasonable_scl N β S S' ⟹ sound_state N β S ⟹ sound_state N β S'"
    using scl_preserves_sound_state[OF scl_if_reasonable] by simp
next
  show "⋀N β S S'. reasonable_scl N β S S' ⟹ trail_atoms_lt β S ⟹ trail_atoms_lt β S'"
    using scl_preserves_trail_atoms_lt[OF scl_if_reasonable] by simp
next
  show "⋀N β S S'. reasonable_scl N β S S' ⟹ trail_propagated_or_decided' N β S ⟹
    trail_propagated_or_decided' N β S'"
    using scl_preserves_trail_propagated_or_decided[OF scl_if_reasonable] by simp
next
  show "⋀N β S S'. reasonable_scl N β S S' ⟹ trail_lits_consistent S ⟹ trail_lits_consistent S'"
    using scl_preserves_trail_lits_consistent[OF scl_if_reasonable] by simp
next
  show "⋀N β S S'. reasonable_scl N β S S' ⟹ ground_false_closures S ⟹ ground_false_closures S'"
    using scl_preserves_ground_false_closures[OF scl_if_reasonable] by simp
qed

corollary correct_termination_regular_scl_run:
  fixes gnd_N and gnd_N_lt_β
  assumes
    run: "(regular_scl N β)** initial_state S" and
    no_step: "∄S'. regular_scl N β S S'"
  defines
    "gnd_N ≡ grounding_of_clss (fset N)" and
    "gnd_N_lt_β ≡ {C ∈ gnd_N. ∀L ∈# C. atm_of L ≼B β}"
  shows "¬ satisfiable gnd_N ∧ (∃γ. state_conflict S = Some ({#}, γ)) ∨
    satisfiable gnd_N_lt_β ∧ trail_true_clss (state_trail S) gnd_N_lt_β"
proof (rule correct_termination_strategy[of _ N β, folded gnd_N_def, folded gnd_N_lt_β_def])
  show "(regular_scl N β)** initial_state S"
    by (rule run)
next
  show "∄S'. regular_scl N β S S'"
    by (rule no_step)
next
  show "⋀S S'. shortest_backtrack_strategy regular_scl N β S S' ⟹ regular_scl N β S S'"
    by (simp add: reasonable_if_regular regular_scl_if_shortest_backtrack_strategy)
next
  show "⋀N β S S'. regular_scl N β S S' ⟹ sound_state N β S ⟹ sound_state N β S'"
    using scl_preserves_sound_state[OF scl_if_regular] by simp
next
  show "⋀N β S S'. regular_scl N β S S' ⟹ trail_atoms_lt β S ⟹ trail_atoms_lt β S'"
    using scl_preserves_trail_atoms_lt[OF scl_if_regular] by simp
next
  show "⋀N β S S'. regular_scl N β S S' ⟹ trail_propagated_or_decided' N β S ⟹
    trail_propagated_or_decided' N β S'"
    using scl_preserves_trail_propagated_or_decided[OF scl_if_regular] by simp
next
  show "⋀N β S S'. regular_scl N β S S' ⟹ trail_lits_consistent S ⟹ trail_lits_consistent S'"
    using scl_preserves_trail_lits_consistent[OF scl_if_regular] by simp
next
  show "⋀N β S S'. regular_scl N β S S' ⟹ ground_false_closures S ⟹ ground_false_closures S'"
    using scl_preserves_ground_false_closures[OF scl_if_regular] by simp
qed

corollary correct_termination_shortest_backtrack_strategy_regular_scl:
  fixes gnd_N and gnd_N_lt_β
  assumes
    run: "(shortest_backtrack_strategy regular_scl N β)** initial_state S" and
    no_step: "∄S'. shortest_backtrack_strategy regular_scl N β S S'"
  defines
    "gnd_N ≡ grounding_of_clss (fset N)" and
    "gnd_N_lt_β ≡ {C ∈ gnd_N. ∀L ∈# C. atm_of L ≼B β}"
  shows "¬ satisfiable gnd_N ∧ (∃γ. state_conflict S = Some ({#}, γ)) ∨
    satisfiable gnd_N_lt_β ∧ trail_true_clss (state_trail S) gnd_N_lt_β"
proof (rule correct_termination_strategy[of _ N β, folded gnd_N_def, folded gnd_N_lt_β_def])
  show "(shortest_backtrack_strategy regular_scl N β)** initial_state S"
    by (rule run)
next
  show "∄S'. shortest_backtrack_strategy regular_scl N β S S'"
    by (rule no_step)
next
  show "⋀S S'. shortest_backtrack_strategy regular_scl N β S S' ⟹ shortest_backtrack_strategy regular_scl N β S S'"
    by simp
next
  show "⋀N β S S'. shortest_backtrack_strategy regular_scl N β S S' ⟹ sound_state N β S ⟹ sound_state N β S'"
    using scl_preserves_sound_state[OF scl_if_regular]
    by (auto simp: shortest_backtrack_strategy_def)
next
  show "⋀N β S S'. shortest_backtrack_strategy regular_scl N β S S' ⟹ trail_atoms_lt β S ⟹ trail_atoms_lt β S'"
    using scl_preserves_trail_atoms_lt[OF scl_if_regular]
    by (auto simp: shortest_backtrack_strategy_def)
next
  show "⋀N β S S'. shortest_backtrack_strategy regular_scl N β S S' ⟹ trail_propagated_or_decided' N β S ⟹
    trail_propagated_or_decided' N β S'"
    using scl_preserves_trail_propagated_or_decided[OF scl_if_regular]
    by (auto simp: shortest_backtrack_strategy_def)
next
  show "⋀N β S S'. shortest_backtrack_strategy regular_scl N β S S' ⟹ trail_lits_consistent S ⟹ trail_lits_consistent S'"
    using scl_preserves_trail_lits_consistent[OF scl_if_regular]
    by (auto simp: shortest_backtrack_strategy_def)
next
  show "⋀N β S S'. shortest_backtrack_strategy regular_scl N β S S' ⟹ ground_false_closures S ⟹ ground_false_closures S'"
    using scl_preserves_ground_false_closures[OF scl_if_regular]
    by (auto simp: shortest_backtrack_strategy_def)
qed

corollary correct_termination_strategies:
  fixes gnd_N and gnd_N_lt_β
  assumes
    "(scl N β)** initial_state S ∧ (∄S'. scl N β S S') ∨
     (reasonable_scl N β)** initial_state S ∧ (∄S'. reasonable_scl N β S S') ∨
     (regular_scl N β)** initial_state S ∧ (∄S'. regular_scl N β S S') ∨
     (shortest_backtrack_strategy regular_scl N β)** initial_state S ∧
       (∄S'. shortest_backtrack_strategy regular_scl N β S S')"
  defines
    "gnd_N ≡ grounding_of_clss (fset N)" and
    "gnd_N_lt_β ≡ {C ∈ gnd_N. ∀L ∈# C. atm_of L ≼B β}"
  shows "¬ satisfiable gnd_N ∧ (∃γ. state_conflict S = Some ({#}, γ)) ∨
    satisfiable gnd_N_lt_β ∧ trail_true_clss (state_trail S) gnd_N_lt_β"
  unfolding gnd_N_def gnd_N_lt_β_def
  using assms(1)
    correct_termination_scl_run[of N β S]
    correct_termination_reasonable_scl_run[of N β S]
    correct_termination_regular_scl_run[of N β S]
    correct_termination_shortest_backtrack_strategy_regular_scl[of N β S]
  by argo

end

end