Theory SCL_FOL

theory SCL_FOL
  imports
    Main
    "HOL-Library.FSet"
    Saturation_Framework.Calculus
    Saturation_Framework_Extensions.Clausal_Calculus
    Ordered_Resolution_Prover.Clausal_Logic
    Ordered_Resolution_Prover.Abstract_Substitution
    Ordered_Resolution_Prover.Herbrand_Interpretation
    First_Order_Terms.Subsumption
    First_Order_Terms.Term
    First_Order_Terms.Unification
    Abstract_Renaming_Apart
    Ordered_Resolution_Prover_Extra
begin

section ‹Extra Lemmas›


subsection ‹Set Extra›

lemma not_in_iff: "L ∉ xs ⟷ (∀y∈xs. L ≠ y)"
  by auto

lemma disjoint_iff': "A ∩ B = {} ⟷ (∀a ∈ A. a ∉ B) ∧ (∀b ∈ B. b ∉ A)"
  by blast

lemma set_filter_insert_conv:
  "{x ∈ insert y S. P x} = (if P y then insert y else id) {x ∈ S. P x}"
  by auto

lemma not_empty_if_mem: "x ∈ X ⟹ X ≠ {}"
  by blast


subsection ‹Finite Set Extra›

lemma finite_induct' [case_names empty singleton insert_insert, induct set: finite]:
  ― ‹Discharging ‹x ∉ F› entails extra work.›
  assumes "finite F"
  assumes "P {}"
    and singleton: "⋀x. P {x}"
    and insert_insert: "⋀x y F. finite F ⟹ x ≠ y ⟹ x ∉ F ⟹ y ∉ F ⟹ P (insert y F) ⟹ P (insert x (insert y F))"
  shows "P F"
  using ‹finite F›
proof induct
  show "P {}" by fact
next
  fix x F
  assume F: "finite F" and P: "P F"
  thus "P (insert x F)"
  proof (induction F rule: finite.induct)
    case emptyI
    show ?case by (rule singleton)
  next
    case (insertI F y)
    show ?case
    proof (cases "x = y")
      case True
      then show ?thesis
        by (simp add: insertI.prems)
    next
      case x_neq_y: False
      show ?thesis
      proof (cases "x ∈ F ∨ y ∈ F")
        case True
        then show ?thesis
          by (metis insertCI insertI.IH insertI.prems insert_absorb)
      next
        case False
        show ?thesis
        proof (rule insert_insert)
          show "finite F" using insertI by simp
        next
          show "x ≠ y" by (rule x_neq_y)
        next
          show "x ∉ F" using False by simp
        next
          show "y ∉ F" using False by simp
        next
          show "P (insert y F)"
            by (simp add: insertI.prems)
        qed
      qed
    qed
  qed
qed


subsection ‹Product Type Extra›

lemma insert_Times: "insert a A × B = Pair a ` B ∪ A × B"
  by blast

lemma Times_insert: "A × insert b B = (λx. (x, b)) ` A ∪ A × B"
  by blast

lemma insert_Times_insert':
  "insert a A × insert b B = insert (a, b) ((Pair a ` B) ∪ ((λx. (x, b)) ` A) ∪ (A × B))"
  (is "?lhs = ?rhs")
  unfolding insert_Times_insert by auto


subsection ‹List Extra›

lemma lt_lengthD:
  assumes i_lt_xs: "i < length xs"
  shows "∃xs1 xi xs2. xs = xs1 @ xi # xs2 ∧ length xs1 = i"
  using assms
  by (metis Cons_nth_drop_Suc add_diff_cancel_left' add_diff_cancel_right'
      canonically_ordered_monoid_add_class.lessE id_take_nth_drop length_append length_drop)

lemma lt_lt_lengthD:
  assumes i_lt_xs: "i < length xs" and j_lt_xs: "j < length xs" and
    i_lt_j: "i < j"
  shows "∃xs1 xi xs2 xj xs3. xs = xs1 @ xi # xs2 @ xj # xs3 ∧ length xs1 = i ∧
    length (xs1 @ xi # xs2) = j"
proof -
  from i_lt_xs obtain xs1 xi xs' where "xs = xs1 @ xi # xs'" and "length xs1 = i"
    using lt_lengthD by blast
  with j_lt_xs obtain xs2 xj xs3 where "xs = xs1 @ xi # xs2 @ xj # xs3" and "length (xs1 @ xi # xs2) = j"
    using lt_lengthD
    by (smt (verit, del_insts) append.assoc append_Cons append_eq_append_conv i_lt_j list.inject)
  thus ?thesis
    using ‹length xs1 = i› by blast
qed


subsection ‹Sublist Extra›

lemma not_mem_strict_suffix:
  shows "strict_suffix xs (y # ys) ⟹ y ∉ set ys ⟹ y ∉ set xs"
  unfolding strict_suffix_def suffix_def
  by (metis Cons_eq_append_conv Un_iff set_append)

lemma not_mem_strict_suffix':
  shows "strict_suffix xs (y # ys) ⟹ f y ∉ f ` set ys ⟹ f y ∉ f ` set xs"
  using not_mem_strict_suffix[of "map f xs" "f y" "map f ys", unfolded list.set_map]
  using map_mono_strict_suffix[of _ "_ # _", unfolded list.map]
  by fast


subsection ‹Multiset Extra›

lemma multp⇩D⇩M_implies_one_step:
  "multp⇩D⇩M R M N ⟹ ∃I J K. N = I + J ∧ M = I + K ∧ J ≠ {#} ∧ (∀k∈#K. ∃x∈#J. R k x)"
  unfolding multp⇩D⇩M_def
  by (metis subset_mset.le_imp_diff_is_add)

lemma multp⇩H⇩O_implies_one_step:
  "multp⇩H⇩O R M N ⟹ ∃I J K. N = I + J ∧ M = I + K ∧ J ≠ {#} ∧ (∀k∈#K. ∃x∈#J. R k x)"
  by (metis multp⇩D⇩M_implies_one_step multp⇩H⇩O_imp_multp⇩D⇩M)

lemma Multiset_Bex_plus_iff: "(∃x ∈# (M1 + M2). P x) ⟷ (∃x ∈# M1. P x) ∨ (∃x ∈# M2. P x)"
  by auto

lemma multp_singleton_rightD:
  assumes "multp R M {#x#}" and "transp R"
  shows "y ∈# M ⟹ R y x"
  using multp_implies_one_step[OF ‹transp R› ‹multp R M {#x#}›]
  by (metis add_cancel_left_left set_mset_single single_is_union singletonD)


subsubsection ‹Calculus Extra›

lemma (in consequence_relation) entails_one_formula: "N ⊨ U ⟹ D ∈ U ⟹ N ⊨ {D}"
  using entail_set_all_formulas by blast


subsection ‹Clausal Calculus Extra›


subsubsection ‹Clausal Calculus Only›

lemma true_cls_iff_set_mset_eq: "set_mset C = set_mset D ⟹ I ⊫ C ⟷ I ⊫ D"
  by (simp add: true_cls_def)

lemma true_clss_if_set_mset_eq: "(∀D ∈ 𝒟. ∃C ∈ 𝒞. set_mset D = set_mset C) ⟹ I ⊫s 𝒞 ⟹ I ⊫s 𝒟"
  using true_cls_iff_set_mset_eq by (metis true_clss_def)

lemma entails_clss_insert: "N ⊫e insert C U ⟷ N ⊫e {C} ∧ N ⊫e U"
  by auto

lemma Collect_lits_from_atms_conv: "{L. P (atm_of L)} = (⋃x ∈ {x. P x}. {Pos x, Neg x})"
  (is "?lhs = ?rhs")
proof (rule Set.equalityI; rule Set.subsetI)
  fix L
  show "L ∈ ?lhs ⟹ L ∈ ?rhs"
    by (cases L) simp_all
next
  fix L
  show "L ∈ ?rhs ⟹ L ∈ ?lhs"
    by auto
qed


subsubsection ‹Clausal Calculus and Abstract Substitution›

lemma (in substitution) is_ground_lit_Pos[simp]: "is_ground_atm atm ⟹ is_ground_lit (Pos atm)"
  by (simp add: is_ground_lit_def)

lemma (in substitution) is_ground_lit_Neg[simp]: "is_ground_atm atm ⟹ is_ground_lit (Neg atm)"
  by (simp add: is_ground_lit_def)


subsection ‹First Order Terms Extra›


subsubsection ‹First Order Terms Only›

lemma atm_of_eq_uminus_if_lit_eq: "L = - K ⟹ atm_of L = atm_of K"
  by (cases L; cases K) simp_all

lemma subst_subst_eq_subst_subst_if_subst_eq_substI:
  assumes "t ⋅ σ = u ⋅ δ" and
    t_inter_δ_empty: "vars_term t ∩ subst_domain δ = {}" and
    u_inter_σ_empty: "vars_term u ∩ subst_domain σ = {}"
  shows
    "range_vars σ ∩ subst_domain δ = {} ⟹ t ⋅ σ ⋅ δ = u ⋅ σ ⋅ δ"
    "range_vars δ ∩ subst_domain σ = {} ⟹ t ⋅ δ ⋅ σ = u ⋅ δ ⋅ σ"
proof -
  from u_inter_σ_empty have "u ⋅ σ ⋅ δ = u ⋅ δ"
    by (simp add: subst_apply_term_ident)
  with ‹t ⋅ σ = u ⋅ δ› show "range_vars σ ∩ subst_domain δ = {} ⟹ t ⋅ σ ⋅ δ = u ⋅ σ ⋅ δ"
    unfolding subst_apply_term_subst_apply_term_eq_subst_apply_term_lhs[OF _ t_inter_δ_empty]
    by simp

  from t_inter_δ_empty have "t ⋅ δ ⋅ σ = t ⋅ σ"
    by (simp add: subst_apply_term_ident)
  with ‹t ⋅ σ = u ⋅ δ› show "range_vars δ ∩ subst_domain σ = {} ⟹ t ⋅ δ ⋅ σ = u ⋅ δ ⋅ σ"
    unfolding subst_apply_term_subst_apply_term_eq_subst_apply_term_lhs[OF _ u_inter_σ_empty]
    by simp
qed

lemma subst_compose_in_unifiersI:
  assumes "t ⋅ σ = u ⋅ δ" and
    "vars_term t ∩ subst_domain δ = {}" and
    "vars_term u ∩ subst_domain σ = {}"
  shows
    "range_vars σ ∩ subst_domain δ = {} ⟹ σ ∘⇩s δ ∈ unifiers {(t, u)}"
    "range_vars δ ∩ subst_domain σ = {} ⟹ δ ∘⇩s σ ∈ unifiers {(t, u)}"
  using subst_subst_eq_subst_subst_if_subst_eq_substI(1)[OF assms]
  using subst_subst_eq_subst_subst_if_subst_eq_substI(2)[OF assms]
  by (simp_all add: unifiers_def)

lemma subst_ident_if_not_in_domain: "x ∉ subst_domain μ ⟹ μ x = Var x"
  by (simp add: subst_domain_def)

(* lemma fixes υ :: "'a ⇒ ('b, 'a) Term.term" assumes "υ ∈ unifiers E" shows "∃μ. is_mgu μ E"
  unfolding is_mgu_def
proof (rule ccontr)
  assume "∄μ. μ ∈ unifiers E ∧ (∀τ∈unifiers E. ∃γ. τ = μ ∘⇩s γ)"
  fix epred5_5 :: "('b, 'a) Term.term set ⇒ ('a ⇒ ('b, 'a) Term.term) ⇒ ('b, 'a) Term.term set ⇒ ('a ⇒ ('b, 'a) Term.term) ⇒  ('b, 'a) Term.term set ⇒ bool"
  have "⋀(X1 :: 'a ⇒ ('b, 'a) Term.term) (X2 :: ('b, 'a) Term.term set)
    (X3 :: 'a ⇒ ('b, 'a) Term.term)  (X4 :: ('b, 'a) Term.term set) (X5 :: ('b, 'a) Term.term set).
    epred5_5 X5 X3 X4 X1 X2 ⟷ ¬ (X3 ∈ X4 ⟶ True)"
(* thf(c_0_5, plain,
![X1:a > term_b_a, X2:set_a_term_b_a, X3:a > term_b_a, X4:set_a_term_b_a, X5:set_a_term_b_a]:
  (((epred5_5 @ X5 @ X3 @ X4 @ X1 @ X2)<=>
  (~(member_a_term_b_a @ X3 @ X4)=>
    (((insert_a_term_b_a @ X1 @ X2)=(insert_a_term_b_a @ X3 @ X4))<=>
      ((((X1)!=(X3))|(((X2)=(X4))))&
        (((X1)=(X3))|((~((((X2)=(insert_a_term_b_a @ X3 @ X5))&
          (~(member_a_term_b_a @ X3 @ X5)&
          (((X4)=(insert_a_term_b_a @ X1 @ X5))&~(member_a_term_b_a @ X1 @ X5)))))
          |(?[X5:set_a_term_b_a]:($true)))&
      ((((X2)=(insert_a_term_b_a @ X3 @ X5))&
      (~(member_a_term_b_a @ X3 @ X5)&
        (((X4)=(insert_a_term_b_a @ X1 @ X5))&~(member_a_term_b_a @ X1 @ X5))))|
        (?[X5:set_a_term_b_a]:($false)))))))))), introduced(definition)). *)
  show False
  using insert_eq_iff mk_disjoint_insert subst_monoid_mult.mult.right_neutral
  (* sledgehammer [e, slices = 1, dont_minimize, isar_proof, compress = 1, timeout = 30, preplay_timeout = 10, overlord] (insert_eq_iff mk_disjoint_insert subst_monoid_mult.mult.right_neutral) *)
  (* by (metis insert_eq_iff mk_disjoint_insert subst_monoid_mult.mult.right_neutral) *)
  using ex_in_conv insertI1 insert_absorb insert_commute insert_eq_iff insert_iff
    insert_not_empty is_mgu_def mk_disjoint_insert subst_monoid_mult.mult.right_neutral
  (* by (smt (verit) ex_in_conv insertI1 insert_absorb insert_commute insert_eq_iff insert_iff
      insert_not_empty is_mgu_def mk_disjoint_insert subst_monoid_mult.mult.right_neutral) *) *)

lemma "is_renaming (Var(x := Var x'))"
proof (unfold is_renaming_def, intro conjI allI)
  fix y show "is_Var ((Var(x := Var x')) y)"
    by simp
next
  show "inj_on (Var(x := Var x')) (subst_domain (Var(x := Var x')))"
    apply (rule inj_onI)
    apply (simp add: subst_domain_def)
    by presburger
qed

lemma ex_mgu_if_subst_eq_subst_and_disj_vars:
  fixes t u :: "('f, 'v) Term.term" and σ⇩t σ⇩u :: "('f, 'v) subst"
  assumes "t ⋅ σ⇩t = u ⋅ σ⇩u" and "vars_term t ∩ vars_term u = {}"
  shows "∃μ :: ('f, 'v) subst. Unification.mgu t u = Some μ"
proof -
  from assms obtain σ :: "('f, 'v) subst" where "t ⋅ σ = u ⋅ σ"
    using vars_term_disjoint_imp_unifier by metis
  thus ?thesis
    using ex_mgu_if_subst_apply_term_eq_subst_apply_term
    by metis
qed

(* corollary
  fixes μ :: "('f, 'v) subst" and E :: "('f, 'v) equations" and Evars :: "'v set"
  assumes imgu_μ: "is_imgu μ E" and fin_E: "finite E"
  defines "Evars ≡ (⋃e ∈ E. vars_term (fst e) ∪ vars_term (snd e))"
  shows "(⋃x ∈ -Evars. vars_term (μ x)) ⊆ -Evars"
  using imgu_subst_domain_subset[OF assms(1,2), folded Evars_def] *)
(*   by (smt (verit, del_insts) ComplD SUP_le_iff Term.term.simps(17) compl_le_swap1
      subset_Compl_singleton subset_eq subst_ident_if_not_in_domain) *)

lemma restrict_subst_domain_subst_composition:
  fixes σ⇩A σ⇩B A B
  assumes
    distinct_domains: "A ∩ B = {}" and
    distinct_range: "∀x ∈ A. vars_term (σ⇩A x) ∩ subst_domain σ⇩B = {}"
  defines "σ ≡ restrict_subst_domain A σ⇩A ∘⇩s σ⇩B"
  shows "x ∈ A ⟹ σ x = σ⇩A x" "x ∈ B ⟹ σ x = σ⇩B x"
proof -
  assume "x ∈ A"
  hence "restrict_subst_domain A σ⇩A x = σ⇩A x"
    by (simp add: restrict_subst_domain_def)
  moreover have "σ⇩A x ⋅ σ⇩B = σ⇩A x"
    using distinct_range
    by (simp add: ‹x ∈ A› subst_apply_term_ident)
  ultimately show "σ x = σ⇩A x"
    by (simp add: σ_def subst_compose_def)
next
  assume "x ∈ B"
  hence "restrict_subst_domain A σ⇩A x = Var x"
    using distinct_domains
    by (metis Int_iff empty_iff restrict_subst_domain_def)
  then show "σ x = σ⇩B x"
    by (simp add: σ_def subst_compose_def)
qed

lemma merge_substs_on_disjoint_domains:
  fixes σ⇩A σ⇩B A B
  assumes distinct_domains: "A ∩ B = {}"
  defines "σ ≡ (λx. if x ∈ A then σ⇩A x else if x ∈ B then σ⇩B x else Var x)"
  shows
    "x ∈ A ⟹ σ x = σ⇩A x"
    "x ∈ B ⟹ σ x = σ⇩B x"
    "x ∉ A ∪ B ⟹ σ x = Var x"
proof -
  show "x ∈ A ⟹ σ x = σ⇩A x"
    by (simp add: σ_def)
next
  assume "x ∈ B"
  moreover hence "x ∉ A"
    using distinct_domains by auto
  ultimately show "σ x = σ⇩B x"
    by (simp add: σ_def)
next
  show "x ∉ A ∪ B ⟹ σ x = Var x"
    by (simp add: σ_def)
qed

definition is_grounding_merge where
  "is_grounding_merge γ A γ⇩A B γ⇩B ⟷
    A ∩ B = {} ⟶ (∀x ∈ A. vars_term (γ⇩A x) = {}) ⟶ (∀x ∈ B. vars_term (γ⇩B x) = {}) ⟶
    (∀x ∈ A. γ x = γ⇩A x) ∧ (∀x ∈ B. γ x = γ⇩B x)"

lemma is_grounding_merge_if_mem_then_else[simp]:
  fixes γ⇩A γ⇩B A B
  defines "γ ≡ (λx. if x ∈ A then γ⇩A x else γ⇩B x)"
  shows "is_grounding_merge γ A γ⇩A B γ⇩B"
  unfolding is_grounding_merge_def
  by (auto simp: γ_def)

lemma is_grounding_merge_restrict_subst_domain_comp[simp]:
  fixes γ⇩A γ⇩B A B
  defines "γ ≡ restrict_subst_domain A γ⇩A ∘⇩s γ⇩B"
  shows "is_grounding_merge γ A γ⇩A B γ⇩B"
  unfolding is_grounding_merge_def
proof (intro impI)
  assume disjoint: "A ∩ B = {}" and
    ball_A_ground: "∀x∈A. vars_term (γ⇩A x) = {}" and
    ball_B_ground: "∀x∈B. vars_term (γ⇩B x) = {}"

  from ball_A_ground have "∀x∈A. vars_term (γ⇩A x) ∩ subst_domain γ⇩B = {}"
    by simp
  thus "(∀x∈A. γ x = γ⇩A x) ∧ (∀x∈B. γ x = γ⇩B x)"
    using restrict_subst_domain_subst_composition[OF disjoint, of γ⇩A γ⇩B]
    by (simp_all add: γ_def)
qed
  

subsubsection ‹First Order Terms And Abstract Substitution›

no_notation subst_apply_term (infixl "⋅" 67)
no_notation subst_compose (infixl "∘⇩s" 75)

global_interpretation substitution_ops subst_apply_term Var subst_compose .

notation subst_atm_abbrev (infixl "⋅a" 67)
notation subst_atm_list (infixl "⋅al" 67)
notation subst_lit (infixl "⋅l" 67)
notation subst_cls (infixl "⋅" 67)
notation subst_clss (infixl "⋅cs" 67)
notation subst_cls_list (infixl "⋅cl" 67)
notation subst_cls_lists (infixl "⋅⋅cl" 67)
notation comp_subst_abbrev (infixl "⊙" 67)

abbreviation vars_lit :: "('f, 'v) Term.term literal ⇒ 'v set" where
  "vars_lit L ≡ vars_term (atm_of L)"

definition vars_cls :: "('f, 'v) term clause ⇒ 'v set" where
  "vars_cls C = Union (set_mset (image_mset vars_lit C))"

definition vars_clss :: "('f, 'v) term clause set ⇒ 'v set" where
  "vars_clss N = (⋃C ∈ N. vars_cls C)"

lemma vars_clss_empty[simp]: "vars_clss {} = {}"
  by (simp add: vars_clss_def)

lemma vars_clss_insert[simp]: "vars_clss (insert C N) = vars_cls C ∪ vars_clss N"
  by (simp add: vars_clss_def)

lemma vars_clss_union[simp]: "vars_clss (CC ∪ DD) = vars_clss CC ∪ vars_clss DD"
  by (simp add: vars_clss_def)

lemma vars_cls_empty[simp]: "vars_cls {#} = {}"
  unfolding vars_cls_def by simp

lemma finite_vars_cls[simp]: "finite (vars_cls C)"
  unfolding vars_cls_def by simp

lemma vars_cls_plus_iff: "vars_cls (C + D) = vars_cls C ∪ vars_cls D"
  unfolding vars_cls_def by simp

lemma vars_cls_subset_vars_cls_if_subset_mset: "C ⊆# D ⟹ vars_cls C ⊆ vars_cls D"
  by (auto simp add: vars_cls_def)

lemma is_ground_atm_iff_vars_empty: "is_ground_atm t ⟷ vars_term t = {}"
  by (metis (mono_tags, opaque_lifting) equals0D equals0I is_ground_atm_def subst_apply_term_empty
      subst_def subst_simps(1) term.distinct(1) term_subst_eq term_subst_eq_rev)

lemma is_ground_lit_iff_vars_empty: "is_ground_lit L ⟷ vars_lit L = {}"
  by (simp add: is_ground_atm_iff_vars_empty is_ground_lit_def)

lemma is_ground_cls_iff_vars_empty: "is_ground_cls C ⟷ vars_cls C = {}"
  by (auto simp: is_ground_cls_def is_ground_lit_iff_vars_empty vars_cls_def)

lemma is_ground_atm_is_ground_on_var:
  assumes "is_ground_atm (A ⋅a σ)" and "v ∈ vars_term A"
  shows "is_ground_atm (σ v)"
using assms proof (induction A)
  case (Var x)
  then show ?case by auto
next
  case (Fun f ts)
  then show ?case unfolding is_ground_atm_def
    by auto
qed

lemma is_ground_lit_is_ground_on_var:
  assumes ground_lit: "is_ground_lit (subst_lit L σ)" and v_in_L: "v ∈ vars_lit L"
  shows "is_ground_atm (σ v)"
proof -
  let ?A = "atm_of L"
  from v_in_L have A_p: "v ∈ vars_term ?A"
    by auto
  then have "is_ground_atm (?A ⋅a σ)"
    using ground_lit unfolding is_ground_lit_def by auto
  then show ?thesis
    using A_p is_ground_atm_is_ground_on_var by metis
qed

lemma is_ground_cls_is_ground_on_var:
  assumes
    ground_clause: "is_ground_cls (subst_cls C σ)" and
    v_in_C: "v ∈ vars_cls C"
  shows "is_ground_atm (σ v)"
proof -
  from v_in_C obtain L where L_p: "L ∈# C" "v ∈ vars_lit L"
    unfolding vars_cls_def by auto
  then have "is_ground_lit (subst_lit L σ)"
    using ground_clause unfolding is_ground_cls_def subst_cls_def by auto
  then show ?thesis
    using L_p is_ground_lit_is_ground_on_var by metis
qed


lemma vars_atm_subset_subst_domain_if_grounding:
  assumes "is_ground_atm (t ⋅a γ)"
  shows "vars_term t ⊆ subst_domain γ"
  using assms
  by (metis empty_iff is_ground_atm_iff_vars_empty is_ground_atm_is_ground_on_var subsetI
      subst_ident_if_not_in_domain term.set_intros(3))

lemma vars_lit_subset_subst_domain_if_grounding:
  assumes "is_ground_lit (L ⋅l γ)"
  shows "vars_lit L ⊆ subst_domain γ"
  using assms vars_atm_subset_subst_domain_if_grounding
  by (metis atm_of_subst_lit is_ground_lit_def)

lemma vars_cls_subset_subst_domain_if_grounding:
  assumes "is_ground_cls (C ⋅ σ)"
  shows "vars_cls C ⊆ subst_domain σ"
proof (rule Set.subsetI)
  fix x assume "x ∈ vars_cls C"
  thus "x ∈ subst_domain σ"
    unfolding subst_domain_def mem_Collect_eq
    by (metis assms empty_iff is_ground_atm_iff_vars_empty is_ground_cls_is_ground_on_var
        term.set_intros(3))
qed

lemma same_on_vars_lit:
  assumes "∀v ∈ vars_lit L. σ v = τ v"
  shows "subst_lit L σ = subst_lit L τ"
  using assms
proof (induction L)
  case (Pos x)
  then have "∀v ∈ vars_term x. σ v = τ v ⟹ subst_atm_abbrev x σ = subst_atm_abbrev x τ"
    using term_subst_eq by metis+
  then show ?case
    unfolding subst_lit_def using Pos by auto
next
  case (Neg x)
  then have "∀v ∈ vars_term x. σ v = τ v ⟹ subst_atm_abbrev x σ = subst_atm_abbrev x τ"
    using term_subst_eq by metis+
  then show ?case
    unfolding subst_lit_def using Neg by auto
qed

lemma same_on_vars_clause:
  assumes "∀v ∈ vars_cls S. σ v = τ v"
  shows "subst_cls S σ = subst_cls S τ"
  by (smt assms image_eqI image_mset_cong2 mem_simps(9) same_on_vars_lit set_image_mset
      subst_cls_def vars_cls_def)

lemma same_on_lits_clause:
  assumes "∀L ∈# C. subst_lit L σ = subst_lit L τ"
  shows "subst_cls C σ = subst_cls C τ"
  using assms unfolding subst_cls_def
  by simp

global_interpretation substitution "(⋅a)" "Var :: _ ⇒ ('f, 'v) term" "(⊙)"
proof unfold_locales
  show "⋀A. A ⋅a Var = A"
    by auto
next
  show "⋀A τ σ. A ⋅a (τ ⊙ σ) = A ⋅a τ ⋅a σ"
    by auto
next
  show "⋀σ τ. (⋀A. A ⋅a σ = A ⋅a τ) ⟹ σ = τ"
    by (simp add: subst_term_eqI)
next
  fix C :: "('f, 'v) term clause" and σ :: "('f, 'v) subst"
  assume "is_ground_cls (subst_cls C σ)"
  hence ground_atms_σ: "⋀v. v ∈ vars_cls C ⟹ is_ground_atm (σ v)"
    by (meson is_ground_cls_is_ground_on_var)

  define some_ground_trm :: "('f, 'v) term" where "some_ground_trm = (Fun undefined [])"
  have ground_trm: "is_ground_atm some_ground_trm"
    unfolding is_ground_atm_def some_ground_trm_def by auto
  define τ where "τ = (λv. if v ∈ vars_cls C then σ v else some_ground_trm)"
  then have τ_σ: "∀v ∈ vars_cls C. σ v = τ v"
    unfolding τ_def by auto

  have all_ground_τ: "is_ground_atm (τ v)" for v
  proof (cases "v ∈ vars_cls C")
    case True
    then show ?thesis
      using ground_atms_σ τ_σ by auto
  next
    case False
    then show ?thesis
      unfolding τ_def using ground_trm by auto
  qed
  have "is_ground_subst τ"
    unfolding is_ground_subst_def
  proof
    fix A
    show "is_ground_atm (A ⋅a τ)"
    proof (induction A)
      case (Var v)
      thus ?case using all_ground_τ by auto
    next
      case (Fun f As)
      thus ?case using all_ground_τ by (simp add: is_ground_atm_def)
    qed
  qed
  moreover with τ_σ have "C ⋅ σ = C ⋅ τ"
    using same_on_vars_clause by auto
  ultimately show "∃τ. is_ground_subst τ ∧ C ⋅ τ = C ⋅ σ"
    by auto
next
  show "wfP (strictly_generalizes_atm :: ('f, 'v) term ⇒ _ ⇒ _)"
    unfolding wfP_def
    by (rule wf_subset[OF wf_subsumes])
      (auto simp: strictly_generalizes_atm_def generalizes_atm_def term_subsumable.subsumes_def
        subsumeseq_term.simps)
qed

lemma vars_subst_lit_eq_vars_subst_atm: "vars_lit (L ⋅l σ) = vars_term (atm_of L ⋅a σ)"
  by (cases L) simp_all

lemma vars_subst_lit_eq:
  "vars_lit (L ⋅l σ) = (⋃x ∈ vars_lit L. vars_term (σ x))"
  using vars_term_subst_apply_term by (metis atm_of_subst_lit)

lemma vars_subst_cls_eq:
  "vars_cls (C ⋅ σ) = (⋃x ∈ vars_cls C. vars_term (σ x))"
  by (simp add: vars_cls_def multiset.set_map UN_UN_flatten subst_cls_def
      vars_subst_lit_eq[symmetric])

lemma vars_subst_lit_subset: "vars_lit (L ⋅l σ) ⊆ vars_lit L - subst_domain σ ∪ range_vars σ"
  using vars_term_subst_apply_term_subset[of "atm_of L"] by simp

lemma vars_subst_cls_subset: "vars_cls (C ⋅ σ) ⊆ vars_cls C - subst_domain σ ∪ range_vars σ"
  unfolding vars_cls_def subst_cls_def
  apply simp
  using vars_subst_lit_subset
  by fastforce

lemma vars_subst_cls_subset_weak: "vars_cls (C ⋅ σ) ⊆ vars_cls C ∪ range_vars σ"
  unfolding vars_cls_def subst_cls_def
  apply simp
  using vars_subst_lit_subset
  by fastforce

lemma vars_cls_plus[simp]: "vars_cls (C + D) = vars_cls C ∪ vars_cls D"
  unfolding vars_cls_def by simp

lemma vars_cls_add_mset[simp]: "vars_cls (add_mset L C) = vars_lit L ∪ vars_cls C"
  by (simp add: vars_cls_def)

lemma UN_vars_term_atm_of_cls[simp]: "(⋃T∈{atm_of ` set_mset C}. ⋃ (vars_term ` T)) = vars_cls C"
  by (induction C) simp_all

lemma vars_lit_subst_subset_vars_cls_substI[intro]:
  "vars_lit L ⊆ vars_cls C ⟹ vars_lit (L ⋅l σ) ⊆ vars_cls (C ⋅ σ)"
  by (metis subset_Un_eq subst_cls_add_mset vars_cls_add_mset vars_subst_cls_eq)

lemma vars_subst_cls_subset_vars_cls_subst:
  "vars_cls C ⊆ vars_cls D ⟹ vars_cls (C ⋅ σ) ⊆ vars_cls (D ⋅ σ)"
  by (metis subset_Un_eq subst_cls_union vars_cls_plus_iff vars_subst_cls_eq)

lemma vars_cls_subst_subset:
  assumes range_vars_η: "range_vars η ⊆ vars_lit L ∪ vars_lit L'"
  shows "vars_cls (add_mset L D ⋅ η) ⊆ vars_cls (add_mset L' (add_mset L D))"
proof -
  have "vars_cls ((add_mset L D) ⋅ η) ⊆ vars_cls (add_mset L D) - subst_domain η ∪ range_vars η"
    by (rule vars_subst_cls_subset[of "add_mset L D" η])
  also have "... ⊆ vars_cls (add_mset L D) - (vars_lit L ∪ vars_lit L') ∪ vars_lit L ∪ vars_lit L'"
    using range_vars_η by blast
  also have "... ⊆ vars_cls (add_mset L D) ∪ vars_lit L' ∪ vars_lit L"
    by auto
  also have "... ⊆ vars_cls D ∪ vars_lit L' ∪ vars_lit L"
    by auto
  also have "... ⊆ vars_cls (add_mset L' (add_mset L D))"
    by auto
  finally show ?thesis
    by assumption
qed

definition disjoint_vars where
  "disjoint_vars C D ⟷ vars_cls C ∩ vars_cls D = {}"

lemma disjoint_vars_iff_inter_empty: "disjoint_vars C D ⟷ vars_cls C ∩ vars_cls D = {}"
  by (rule disjoint_vars_def)

hide_fact disjoint_vars_def

lemma disjoint_vars_sym: "disjoint_vars C D ⟷ disjoint_vars D C"
  unfolding disjoint_vars_iff_inter_empty by blast

lemma disjoint_vars_plus_iff: "disjoint_vars (C + D) E ⟷ disjoint_vars C E ∧ disjoint_vars D E"
  unfolding disjoint_vars_iff_inter_empty vars_cls_plus_iff
  by (simp add: Int_Un_distrib2)

lemma disjoint_vars_subset_mset: "disjoint_vars C D ⟹ E ⊆# C ⟹ disjoint_vars E D"
  by (metis disjoint_vars_plus_iff subset_mset.diff_add)

lemma disjoint_vars_subst_clsI:
  "disjoint_vars C D ⟹ range_vars σ ∩ vars_cls D = {} ⟹ disjoint_vars (C ⋅ σ) D"
  unfolding disjoint_vars_iff_inter_empty
  unfolding vars_subst_cls_eq
  by (smt (verit, best) Diff_subset Un_iff disjoint_iff image_cong subsetD vars_subst_cls_eq
      vars_subst_cls_subset)

lemma is_renaming_iff: "is_renaming ρ ⟷ (∀x. is_Var (ρ x)) ∧ inj ρ"
  (is "?lhs ⟷ ?rhs")
proof (rule iffI)
  show "?lhs ⟹ ?rhs"
    unfolding is_renaming_def
    apply safe
     apply (metis subst_apply_eq_Var subst_compose term.disc(1))
    by (metis injI subst_compose_def term.sel(1))
next
  show "?rhs ⟹ ?lhs"
    by (auto simp: is_renaming_def intro: ex_inverse_of_renaming)
qed

lemma subst_cls_idem_if_disj_vars: "subst_domain σ ∩ vars_cls C = {} ⟹ C ⋅ σ = C"
  by (metis (mono_tags, lifting) Int_iff empty_iff mem_Collect_eq same_on_vars_clause
      subst_cls_id_subst subst_domain_def)

lemma subst_lit_idem_if_disj_vars: "subst_domain σ ∩ vars_lit L = {} ⟹ L ⋅l σ = L"
  by (rule subst_cls_idem_if_disj_vars[of _ "{#L#}", simplified])

lemma subst_lit_restrict_subst_domain: "vars_lit L ⊆ V ⟹ L ⋅l restrict_subst_domain V σ = L ⋅l σ"
  by (simp add: restrict_subst_domain_def same_on_vars_lit subsetD)

lemma subst_cls_restrict_subst_domain: "vars_cls C ⊆ V ⟹ C ⋅ restrict_subst_domain V σ = C ⋅ σ"
  by (simp add: restrict_subst_domain_def same_on_vars_clause subsetD)

lemma subst_clss_insert[simp]: "insert C U ⋅cs η = insert (C ⋅ η) (U ⋅cs η)"
  by (simp add: subst_clss_def)

lemma valid_grounding_of_renaming:
  assumes "is_renaming ρ"
  shows "I ⊫s grounding_of_cls (C ⋅ ρ) ⟷ I ⊫s grounding_of_cls C"
proof -
  have "grounding_of_cls (C ⋅ ρ) = grounding_of_cls C"
    by (rule grounding_of_subst_cls_renaming_ident[OF ‹is_renaming ρ›])
  thus ?thesis
    by simp
qed

lemma is_unifier_iff_mem_unifiers_Times:
  assumes fin_AA: "finite AA"
  shows "is_unifier υ AA ⟷ υ ∈ unifiers (AA × AA)"
proof (rule iffI)
  assume unif_υ_AA: "is_unifier υ AA"
  show "υ ∈ unifiers (AA × AA)"
  unfolding unifiers_def mem_Collect_eq
  proof (rule ballI)
    have "card (AA ⋅⇩s⇩e⇩t υ) ≤ 1"
      by (rule unif_υ_AA[unfolded is_unifier_def subst_atms_def])
  
    fix p assume "p ∈ AA × AA"
    then obtain a b where p_def: "p = (a, b)" and "a ∈ AA" and "b ∈ AA"
      by auto
    hence "card (AA ⋅⇩s⇩e⇩t υ) = 1"
      using fin_AA ‹card (AA ⋅⇩s⇩e⇩t υ) ≤ 1› antisym_conv2 by fastforce
  
    hence "a ⋅a υ = b ⋅a υ"
      using ‹a ∈ AA› ‹b ∈ AA› fin_AA is_unifier_subst_atm_eqI unif_υ_AA by blast
    thus "fst p ⋅a υ = snd p ⋅a υ"
      by (simp add: p_def)
  qed
next
  assume unif_υ_AA: "υ ∈ unifiers (AA × AA)"
  show "is_unifier υ AA"
    using fin_AA unif_υ_AA
  proof (induction AA arbitrary: υ rule: finite_induct)
    case empty
    then show ?case
      by (simp add: is_unifier_def)
  next
    case (insert a AA)
    from insert.prems have
      υ_in: "υ ∈ unifiers ((insert (a, a) (Pair a ` AA) ∪ (λx. (x, a)) ` AA) ∪ AA × AA)"
      unfolding insert_Times_insert'[of a AA a AA] by simp
    then show ?case
      by (smt (verit, del_insts) Set.set_insert Un_insert_left finite.insertI fst_conv image_insert
          insert.hyps(1) insert_compr is_unifier_alt mem_Collect_eq snd_conv unifiers_def)
  qed
qed

lemma is_mgu_singleton_iff_Unifiers_is_mgu_Times:
  assumes fin: "finite AA"
  shows "is_mgu υ {AA} ⟷ Unifiers.is_mgu υ (AA × AA)"
  by (auto simp: is_mgu_def Unifiers.is_mgu_def is_unifiers_def
      is_unifier_iff_mem_unifiers_Times[OF fin])

lemma is_imgu_singleton_iff_Unifiers_is_imgu_Times:
  assumes fin: "finite AA"
  shows "is_imgu υ {AA} ⟷ Unifiers.is_imgu υ (AA × AA)"
  by (auto simp: is_imgu_def Unifiers.is_imgu_def is_unifiers_def
      is_unifier_iff_mem_unifiers_Times[OF fin])


lemma unifiers_without_refl: "unifiers E = unifiers {e ∈ E. fst e ≠ snd e}"
  (is "?lhs = ?rhs")
  unfolding unifiers_def by fastforce

lemma subst_lit_renaming_subst_adapted:
  assumes ren_ρ: "is_renaming ρ" and vars_L: "vars_lit L ⊆ subst_domain σ"
  shows "L ⋅l ρ ⋅l rename_subst_domain ρ σ = L ⋅l σ"
proof -
  from ren_ρ have is_var_ρ: "∀x. is_Var (ρ x)" and "inj ρ"
    by (simp_all add: is_renaming_iff)

  show ?thesis
    using vars_L renaming_cancels_rename_subst_domain[OF is_var_ρ ‹inj ρ›]
    by (cases L) (simp_all add: subst_lit_def)
qed

lemma subst_renaming_subst_adapted:
  assumes ren_ρ: "is_renaming ρ" and vars_D: "vars_cls D ⊆ subst_domain σ"
  shows "D ⋅ ρ ⋅ rename_subst_domain ρ σ = D ⋅ σ"
  unfolding subst_cls_comp_subst[symmetric]
proof (intro same_on_lits_clause ballI)
  fix L assume "L ∈# D"
  with vars_D have "vars_lit L ⊆ subst_domain σ"
    by (auto dest!: multi_member_split)
  thus "L ⋅l (ρ ⊙ rename_subst_domain ρ σ) = L ⋅l σ"
    unfolding subst_lit_comp_subst
    by (rule subst_lit_renaming_subst_adapted[OF ren_ρ])
qed

lemma subst_domain_rename_subst_domain_subset':
  assumes is_var_ρ: "∀x. is_Var (ρ x)"
  shows "subst_domain (rename_subst_domain ρ σ) ⊆ (⋃x ∈ subst_domain σ. vars_term (ρ x))"
proof (rule subset_trans)
  show "subst_domain (rename_subst_domain ρ σ) ⊆ the_Var ` ρ ` subst_domain σ"
    by (rule subst_domain_rename_subst_domain_subset[OF is_var_ρ])
next
  show "the_Var ` ρ ` subst_domain σ ⊆ (⋃x∈subst_domain σ. vars_term (ρ x))"
    unfolding image_the_Var_image_subst_renaming_eq[OF is_var_ρ] by simp
qed

lemma range_vars_eq_empty_if_is_ground:
  "is_ground_cls (C ⋅ γ) ⟹ subst_domain γ ⊆ vars_cls C ⟹ range_vars γ = {}"
  unfolding range_vars_def UNION_empty_conv subst_range.simps is_ground_cls_iff_vars_empty
  by (metis (no_types, opaque_lifting) dual_order.eq_iff imageE is_ground_atm_iff_vars_empty
      is_ground_cls_iff_vars_empty is_ground_cls_is_ground_on_var
      vars_cls_subset_subst_domain_if_grounding)


subsubsection ‹Minimal, Idempotent Most General Unifier›

lemma is_imgu_if_mgu_eq_Some:
  assumes mgu: "Unification.mgu t u = Some μ"
  shows "is_imgu μ {{t, u}}"
proof -
  have "unifiers ({t, u} × {t, u}) = unifiers {(t, u)}"
    by (auto simp: unifiers_def)
  hence  "Unifiers.is_imgu μ ({t, u} × {t, u})"
    using mgu_sound[OF mgu]
    by (simp add: Unifiers.is_imgu_def)
  thus ?thesis
    by (simp add: is_imgu_singleton_iff_Unifiers_is_imgu_Times)
qed

primrec pairs where
  "pairs [] = []" |
  "pairs (x # xs) = (x, x) # map (Pair x) xs @ map (λy. (y, x)) xs @ pairs xs"

lemma "set (pairs [a, b, c, d]) =
  {(a, a), (a, b), (a, c), (a, d),
   (b, a), (b, b), (b, c), (b, d),
   (c, a), (c, b), (c, c), (c, d),
   (d, a), (d, b), (d, c), (d, d)}"
  by auto

lemma set_pairs: "set (pairs xs) = set xs × set xs"
  by (induction xs) auto

text ‹Reflexive and symmetric pairs are not necessary to computing the MGU, but it makes the set of
the resulting list equivalent to @{term "{(x, y). x ∈ xs ∧ y ∈ ys}"}, which is necessary for the
following properties.›

lemma pair_in_set_pairs: "a ∈ set as ⟹ b ∈ set as ⟹ (a, b) ∈ set (pairs as)"
  by (induction as) auto

lemma fst_pair_in_set_if_pair_in_pairs: "p ∈ set (pairs as) ⟹ fst p ∈ set as"
  by (induction as) auto

lemma snd_pair_in_set_if_pair_in_pairs: "p ∈ set (pairs as) ⟹ snd p ∈ set as"
  by (induction as) auto

lemma vars_mset_mset_pairs:
  "vars_mset (mset (pairs as)) = (⋃b ∈ set as. ⋃a ∈ set as. vars_term a ∪ vars_term b)"
  by (induction as) (auto simp: vars_mset_def)

definition mgu_sets where
  "mgu_sets μ AAA ⟷ (∃ass. set (map set ass) = AAA ∧
    map_option subst_of (unify (concat (map pairs ass)) []) = Some μ)"

lemma is_imgu_if_mgu_sets:
  assumes mgu_AAA: "mgu_sets μ AAA"
  shows "is_imgu μ AAA"
proof -
  from mgu_AAA obtain ass xs where
    AAA_def: "AAA = set (map set ass)" and
    unify: "unify (concat (map pairs ass)) [] = Some xs" and
    "subst_of xs = μ"
    unfolding mgu_sets_def by auto
  hence "Unifiers.is_imgu μ (set (concat (map pairs ass)))"
    using unify_sound[OF unify] by simp
  moreover have "unifiers (set (concat (map pairs ass))) = {υ. is_unifiers υ AAA}"
    unfolding AAA_def
  proof (rule Set.equalityI; rule Set.subsetI; unfold mem_Collect_eq)
    fix x assume x_in: "x ∈ unifiers (set (concat (map pairs ass)))"
    show "is_unifiers x (set (map set ass))"
      unfolding is_unifiers_def
    proof (rule ballI)
      fix As assume "As ∈ set (map set ass)"
      hence "finite As" by auto

      from ‹As ∈ set (map set ass)› obtain as where
        as_in: "as ∈ set ass" and As_def: "As = set as"
        by auto

      show "is_unifier x As"
        unfolding is_unifier_alt[OF ‹finite As›]
      proof (intro ballI)
        fix A B assume "A ∈ As" "B ∈ As"
        hence "∃xs ∈ set ass. (A, B) ∈ set (pairs xs)"
          using as_in by (auto simp: As_def intro: pair_in_set_pairs)
        thus "A ⋅a x = B ⋅a x"
          using x_in[unfolded unifiers_def mem_Collect_eq, rule_format, of "(A, B)", simplified]
          by simp
      qed
    qed
  next
    fix x assume is_unifs_x: "is_unifiers x (set (map set ass))"
    show "x ∈ unifiers (set (concat (map pairs ass)))"
      unfolding unifiers_def mem_Collect_eq
    proof (rule ballI)
      fix p assume "p ∈ set (concat (map pairs ass))"
      then obtain as where "as ∈ set ass" and p_in: "p ∈ set (pairs as)"
        by auto
      hence is_unif_x: "is_unifier x (set as)"
        using is_unifs_x[unfolded is_unifiers_def] by simp
      moreover have "fst p ∈ set as"
        by (rule p_in[THEN fst_pair_in_set_if_pair_in_pairs])
      moreover have "snd p ∈ set as"
        by (rule p_in[THEN snd_pair_in_set_if_pair_in_pairs])
      ultimately show "fst p ⋅a x = snd p ⋅a x"
        unfolding is_unifier_alt[of "set as", simplified]
        by blast
    qed
  qed
  ultimately show "is_imgu μ AAA"
    unfolding Unifiers.is_imgu_def is_imgu_def by simp
qed


subsubsection ‹Renaming Extra›

context renaming_apart begin

lemma inj_Var_comp_renaming: "finite V ⟹ inj (Var ∘ renaming V)"
  using inj_compose inj_renaming by (metis inj_def term.inject(1))

lemma is_renaming_Var_comp_renaming: "finite V ⟹ Term.is_renaming (Var ∘ renaming V)"
  unfolding Term.is_renaming_def
  using inj_Var_comp_renaming by (metis comp_apply inj_on_subset term.disc(1) top_greatest)

lemma vars_term_subst_term_Var_comp_renaming_disj:
  assumes fin_V: "finite V"
  shows "vars_term (t ⋅a (Var ∘ renaming V)) ∩ V = {}"
  using is_renaming_Var_comp_renaming[OF fin_V] renaming_correct[OF fin_V]
  by (induction t) auto

lemma vars_term_subst_term_Var_comp_renaming_disj':
  assumes fin_V: "finite V1" and sub: "V2 ⊆ V1"
  shows "vars_term (t ⋅a (Var ∘ renaming V1)) ∩ V2 = {}"
  by (meson disjoint_iff fin_V sub subsetD vars_term_subst_term_Var_comp_renaming_disj)

lemma vars_lit_subst_renaming_disj:
  assumes fin_V: "finite V"
  shows "vars_lit (L ⋅l (Var ∘ renaming V)) ∩ V = {}"
  using vars_term_subst_term_Var_comp_renaming_disj[OF fin_V] by auto

lemma vars_cls_subst_renaming_disj:
  assumes fin_V: "finite V"
  shows "vars_cls (C ⋅ (Var ∘ renaming V)) ∩ V = {}"
  unfolding vars_cls_def
  apply simp
  using vars_lit_subst_renaming_disj[OF fin_V]
  by (smt (verit, best) UN_iff UN_simps(10) disjoint_iff multiset.set_map subst_cls_def)

abbreviation renaming_wrt :: "('f, _) Term.term clause set ⇒ _ ⇒ ('f, _) Term.term" where
  "renaming_wrt N ≡ Var ∘ renaming (vars_clss N)"

lemma is_renaming_renaming_wrt: "finite N ⟹ is_renaming (renaming_wrt N)"
  by (simp add: inj_Var_comp_renaming is_renaming_iff vars_clss_def)

lemma ex_renaming_to_disjoint_vars:
  fixes C :: "('f, 'a) Term.term clause" and N :: "('f, 'a) Term.term clause set"
  assumes fin: "finite N"
  shows "∃ρ. is_renaming ρ ∧ vars_cls (C ⋅ ρ) ∩ vars_clss N = {}"
proof (intro exI conjI)
  show "SCL_FOL.is_renaming (renaming_wrt N)"
    using fin is_renaming_renaming_wrt by metis
next
  show "vars_cls (C ⋅ renaming_wrt N) ∩ vars_clss N = {}"
    by (simp add: fin vars_cls_subst_renaming_disj vars_clss_def)
qed

end


section ‹SCL State›

type_synonym ('f, 'v) closure = "('f, 'v) term clause × ('f, 'v) subst"
type_synonym ('f, 'v) closure_with_lit =
  "('f, 'v) term clause × ('f, 'v) term literal × ('f, 'v) subst"
type_synonym ('f, 'v) trail = "(('f, 'v) term literal × ('f, 'v) closure_with_lit option) list"
type_synonym ('f, 'v) state =
  "('f, 'v) trail × ('f, 'v) term clause fset × ('f, 'v) closure option"

text ‹Note that, in contrast to Bromberger, Schwarz, and Weidenbach, the level is not part of the
state. It would be redundant because it can always be computed from the trail.›

abbreviation initial_state :: "('f, 'v) state" where
  "initial_state ≡ ([], {||}, None)"

definition state_trail :: "('f, 'v) state ⇒ ('f, 'v) trail" where
  "state_trail S = fst S"

lemma state_trail_simp[simp]: "state_trail (Γ, U, u) = Γ"
  by (simp add: state_trail_def)

definition state_learned :: "('f, 'v) state ⇒ ('f, 'v) term clause fset" where
  "state_learned S = fst (snd S)"

lemma state_learned_simp[simp]: "state_learned (Γ, U, u) = U"
  by (simp add: state_learned_def)

definition state_conflict :: "('f, 'v) state ⇒ ('f, 'v) closure option" where
  "state_conflict S = snd (snd S)"

lemma state_conflict_simp[simp]: "state_conflict (Γ, U, u) = u"
  by (simp add: state_conflict_def)

lemmas state_proj_simp = state_trail_simp state_learned_simp state_conflict_simp

lemma state_simp[simp]: "(state_trail S, state_learned S, state_conflict S) = S"
  by (simp add: state_conflict_def state_learned_def state_trail_def)

fun clss_of_trail_lit where
  "clss_of_trail_lit (_, None) = {||}" |
  "clss_of_trail_lit (_, Some (C, L, _)) = {|add_mset L C|}"

primrec clss_of_trail :: "('f, 'v) trail ⇒ ('f, 'v) term clause fset" where
  "clss_of_trail [] = {||}" |
  "clss_of_trail (Ln # Γ) = clss_of_trail_lit Ln |∪| clss_of_trail Γ"

hide_fact clss_of_trail_def

lemma clss_of_trail_append: "clss_of_trail (Γ⇩0 @ Γ⇩1) = clss_of_trail Γ⇩0 |∪| clss_of_trail Γ⇩1"
  by (induction Γ⇩0) (simp_all add: funion_assoc)

fun clss_of_closure where
  "clss_of_closure None = {||}" |
  "clss_of_closure (Some (C, _)) = {|C|}"


definition propagate_lit where
  "propagate_lit L C γ = (L ⋅l γ, Some (C, L, γ))"

abbreviation trail_propagate ::
  "('f, 'v) trail ⇒ ('f, 'v) term literal ⇒ ('f, 'v) term clause ⇒ ('f, 'v) subst ⇒
    ('f, 'v) trail" where
  "trail_propagate Γ L C γ ≡ propagate_lit L C γ # Γ"

lemma suffix_trail_propagate[simp]: "suffix Γ (trail_propagate Γ L C δ)"
  unfolding suffix_def propagate_lit_def
  by simp

lemma clss_of_trail_trail_propagate[simp]:
  "clss_of_trail (trail_propagate Γ L C γ) = finsert (add_mset L C) (clss_of_trail Γ)"
  unfolding propagate_lit_def by simp

definition decide_lit where
  "decide_lit L = (L, None)"

abbreviation trail_decide :: "('f, 'v) trail ⇒ ('f, 'v) term literal ⇒ ('f, 'v) trail" where
  "trail_decide Γ L ≡ decide_lit L # Γ"

lemma clss_of_trail_trail_decide[simp]:
  "clss_of_trail (trail_decide Γ L) = clss_of_trail Γ"
  by (simp add: decide_lit_def)

definition is_decision_lit
  :: "('f, 'v) term literal × ('f, 'v) closure_with_lit option ⇒ bool" where
  "is_decision_lit Ln ⟷ snd Ln = None"

definition trail_interp :: "('f, 'v) trail ⇒ ('f, 'v) term interp" where
  "trail_interp Γ = ⋃((λL. case L of Pos A ⇒ {A} | Neg A ⇒ {}) ` fst ` set Γ)"

lemma "trail_interp Γ = (⋃Ln ∈ set Γ. case fst Ln of Pos t ⇒ {t} | Neg t ⇒ {})"
  unfolding trail_interp_def by simp

definition trail_true_lit :: "('f, 'v) trail ⇒ ('f, 'v) term literal ⇒ bool" where
  "trail_true_lit Γ L ⟷ L ∈ fst ` set Γ"

definition trail_false_lit :: "('f, 'v) trail ⇒ ('f, 'v) term literal ⇒ bool" where
  "trail_false_lit Γ L ⟷ - L ∈ fst ` set Γ"

definition trail_true_cls :: "('f, 'v) trail ⇒ ('f, 'v) term clause ⇒ bool" where
  "trail_true_cls Γ C ⟷ (∃L ∈# C. trail_true_lit Γ L)"

definition trail_false_cls :: "('f, 'v) trail ⇒ ('f, 'v) term clause ⇒ bool" where
  "trail_false_cls Γ C ⟷ (∀L ∈# C. trail_false_lit Γ L)"

definition trail_true_clss :: "('f, 'v) trail ⇒ ('f, 'v) term clause set ⇒ bool" where
  "trail_true_clss Γ N ⟷ (∀C ∈ N. trail_true_cls Γ C)"

definition trail_defined_lit :: "('f, 'v) trail ⇒ ('f, 'v) term literal ⇒ bool" where
  "trail_defined_lit Γ L ⟷ (L ∈ fst ` set Γ ∨ - L ∈ fst ` set Γ)"

definition trail_defined_cls :: "('f, 'v) trail ⇒ ('f, 'v) term clause ⇒ bool" where
  "trail_defined_cls Γ C ⟷ (∀L ∈# C. trail_defined_lit Γ L)"

lemma trail_defined_lit_iff_true_or_false:
  "trail_defined_lit Γ L ⟷ trail_true_lit Γ L ∨ trail_false_lit Γ L"
  unfolding trail_defined_lit_def trail_false_lit_def trail_true_lit_def by (rule refl)

lemma trail_true_or_false_cls_if_defined:
  "trail_defined_cls Γ C ⟹ trail_true_cls Γ C ∨ trail_false_cls Γ C"
  unfolding trail_defined_cls_def trail_false_cls_def trail_true_cls_def
  unfolding trail_defined_lit_iff_true_or_false
  by blast

lemma trail_false_cls_mempty[simp]: "trail_false_cls Γ {#}"
  by (simp add: trail_false_cls_def)

lemma trail_false_cls_add_mset:
  "trail_false_cls Γ (add_mset L C) ⟷ trail_false_lit Γ L ∧ trail_false_cls Γ C"
  by (auto simp: trail_false_cls_def)

lemma trail_false_cls_plus:
  "trail_false_cls Γ (C + D) ⟷ trail_false_cls Γ C ∧ trail_false_cls Γ D"
  by (auto simp: trail_false_cls_def)

lemma not_trail_true_Nil[simp]:
  "¬ trail_true_lit [] L"
  "¬ trail_true_cls [] C"
  "N ≠ {} ⟹ ¬ trail_true_clss [] N"
  by (simp_all add: trail_true_lit_def trail_true_cls_def trail_true_clss_def)

lemma not_trail_false_Nil[simp]:
  "¬ trail_false_lit [] L"
  "trail_false_cls [] C ⟷ C = {#}"
  by (simp_all add: trail_false_lit_def trail_false_cls_def)

lemma not_trail_defined_lit_Nil[simp]: "¬ trail_defined_lit [] L"
  by (simp add: trail_defined_lit_iff_true_or_false)

lemma trail_false_lit_if_trail_false_suffix:
  "suffix Γ' Γ ⟹ trail_false_lit Γ' K ⟹ trail_false_lit Γ K"
  by (meson image_mono set_mono_suffix subsetD trail_false_lit_def)

lemma trail_false_cls_if_trail_false_suffix:
  "suffix Γ' Γ ⟹ trail_false_cls Γ' C ⟹ trail_false_cls Γ C"
  using trail_false_cls_def trail_false_lit_if_trail_false_suffix by metis

lemma trail_interp_Cons: "trail_interp (Ln # Γ) = trail_interp [Ln] ∪ trail_interp Γ"
  unfolding trail_interp_def by simp

lemma trail_interp_Cons': "trail_interp (Ln # Γ) = (case fst Ln of Pos A ⇒ {A} | Neg A ⇒ {}) ∪ trail_interp Γ"
  unfolding trail_interp_def by simp

lemma true_lit_thick_unionD: "(I1 ∪ I2) ⊫l L ⟹ I1 ⊫l L ∨ I2 ⊫l L"
  by auto

lemma subtrail_falseI:
  assumes tr_false: "trail_false_cls ((L, Cl) # Γ) C" and L_not_in: "-L ∉# C"
  shows "trail_false_cls Γ C"
  unfolding trail_false_cls_def
proof (rule ballI)
  fix M
  assume M_in: "M ∈# C"

  from M_in L_not_in have M_neq_L: "M ≠ -L" by auto

  from M_in tr_false have tr_false_lit_M: "trail_false_lit ((L, Cl) # Γ) M"
    unfolding trail_false_cls_def by simp
  thus "trail_false_lit Γ M"
    unfolding trail_false_lit_def
    using M_neq_L
    by (cases L; cases M) (simp_all add: trail_interp_def trail_false_lit_def)
qed

lemma trail_false_cls_ignores_duplicates:
  "set_mset C = set_mset D ⟹ trail_false_cls Γ C ⟷ trail_false_cls Γ D"
  by (simp add: trail_false_cls_def)

lemma ball_trail_propagate_is_ground_lit:
  assumes "∀x∈set Γ. is_ground_lit (fst x)" and "is_ground_lit (L ⋅l σ)"
  shows "∀x∈set (trail_propagate Γ L C σ). is_ground_lit (fst x)"
  unfolding propagate_lit_def
  using assms by simp

lemma ball_trail_decide_is_ground_lit:
  assumes "∀x∈set Γ. is_ground_lit (fst x)" and "is_ground_lit L"
  shows "∀x∈set (trail_decide Γ L). is_ground_lit (fst x)"
  using assms
  by (simp add: decide_lit_def)

lemma trail_false_cls_subst_mgu_before_grounding:
  assumes tr_false_cls: "trail_false_cls Γ ((D + {#L, L'#}) ⋅ σ)" and
    imgu_μ: "is_imgu μ {{atm_of L, atm_of L'}}" and
    unif_σ: "is_unifiers σ {{atm_of L, atm_of L'}}"
  shows "trail_false_cls Γ ((D + {#L#}) ⋅ μ ⋅ σ)"
  unfolding trail_false_cls_def
proof (rule ballI)
  fix K
  assume "K ∈# (D + {#L#}) ⋅ μ ⋅ σ"
  hence "K ∈# D ⋅ μ ⋅ σ ∨ K = L  ⋅l μ ⋅l σ" by force
  thus "trail_false_lit Γ K"
  proof (elim disjE)
    show "K ∈# D ⋅ μ ⋅ σ ⟹ trail_false_lit Γ K"
      using imgu_μ unif_σ
      by (metis is_imgu_def subst_cls_comp_subst subst_cls_union tr_false_cls trail_false_cls_def
          union_iff)
  next
    have "L ⋅l μ ⋅l σ = L ⋅l σ"
      using imgu_μ unif_σ by (metis is_imgu_def subst_lit_comp_subst)
    thus "K = L ⋅l μ ⋅l σ ⟹ trail_false_lit Γ K"
      by (auto intro: tr_false_cls[unfolded trail_false_cls_def, rule_format])
  qed
qed

lemma trail_defined_lit_iff_defined_uminus: "trail_defined_lit Γ L ⟷ trail_defined_lit Γ (-L)"
  by (auto simp add: trail_defined_lit_def)

lemma trail_defined_lit_iff: "trail_defined_lit Γ L ⟷ atm_of L ∈ atm_of ` fst ` set Γ"
  by (simp add: atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set trail_defined_lit_def)

lemma trail_interp_conv: "trail_interp Γ = atm_of ` {L ∈ fst ` set Γ. is_pos L}"
proof (induction Γ)
  case Nil
  show ?case by (simp add: trail_interp_def)
next
  case (Cons Ln Γ)
  then show ?case
    unfolding list.set image_insert set_filter_insert_conv trail_interp_Cons'
    by (simp add: literal.case_eq_if)
qed

lemma not_in_trail_interp_if_not_in_trail: "t ∉ atm_of ` fst ` set Γ ⟹ t ∉ trail_interp Γ"
  by (metis (no_types, lifting) atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set
      literal.sel(2) mem_Collect_eq trail_interp_conv)

inductive trail_consistent where
  Nil[simp]: "trail_consistent []" |
  Cons: "¬ trail_defined_lit Γ L ⟹ trail_consistent Γ ⟹ trail_consistent ((L, u) # Γ)"

lemma distinct_atm_of_trail_if_trail_consistent:
  "trail_consistent Γ ⟹ distinct (map (atm_of ∘ fst) Γ)"
  by (induction Γ rule: trail_consistent.induct)
    (simp_all add: image_comp trail_defined_lit_iff)

lemma trail_consistent_appendD: "trail_consistent (Γ @ Γ') ⟹ trail_consistent Γ'"
  by (induction Γ) (auto elim: trail_consistent.cases)

lemma trail_consistent_if_suffix:
  "trail_consistent Γ ⟹ suffix Γ' Γ ⟹ trail_consistent Γ'"
  by (auto simp: suffix_def intro: trail_consistent_appendD)

lemma trail_interp_lit_if_trail_true:
  shows "trail_consistent Γ ⟹ trail_true_lit Γ L ⟹ trail_interp Γ ⊫l L"
proof (induction Γ rule: trail_consistent.induct)
  case Nil
  thus ?case
    by (simp add: trail_true_lit_def)
next
  case (Cons Γ K u)
  show ?case
  proof (cases "L = K ∨ L = - K")
    case True
    then show ?thesis 
    proof (elim disjE)
      assume "L = K"
      thus ?thesis
      proof (cases L; cases K)
        fix t⇩L t⇩K
        from ‹L = K› show "L = Pos t⇩L ⟹ K = Pos t⇩K ⟹ ?thesis"
          by (simp add: trail_interp_def)
      next
        fix t⇩L t⇩K
        from ‹L = K› show "L = Neg t⇩L ⟹ K = Neg t⇩K ⟹ ?thesis"
          using Cons.hyps(1)
          by (simp add: trail_defined_lit_iff trail_interp_Cons'
              not_in_trail_interp_if_not_in_trail)
      qed simp_all
    next
      assume "L = - K"
      then show ?thesis
      proof (cases L; cases K)
        fix t⇩L t⇩K
        from ‹L = - K› show "L = Pos t⇩L ⟹ K = Neg t⇩K ⟹ ?thesis"
          unfolding trail_interp_Cons'
          using Cons.hyps(1) Cons.prems
          by (metis (no_types, lifting) image_insert insertE list.simps(15) literal.distinct(1)
              prod.sel(1) trail_defined_lit_def trail_true_lit_def)
      next
        fix t⇩L t⇩K
        from ‹L = - K› show "L = Neg t⇩L ⟹ K = Pos t⇩K ⟹ ?thesis"
          unfolding trail_interp_Cons'
          using Cons.hyps(1) Cons.prems
          by (metis (no_types, lifting) image_insert insertE list.simps(15) literal.distinct(1)
              prod.sel(1) trail_defined_lit_def trail_true_lit_def)
      qed simp_all
    qed
  next
    case False
    with Cons.prems have "trail_true_lit Γ L"
      by (simp add: trail_true_lit_def)
    with Cons.IH have "trail_interp Γ ⊫l L"
      by simp
    with False show ?thesis
      by (cases L; cases K) (simp_all add: trail_interp_def del: true_lit_iff)
  qed
qed

lemma trail_interp_cls_if_trail_true:
  assumes "trail_consistent Γ" and "trail_true_cls Γ C"
  shows "trail_interp Γ ⊫ C"
proof -
  from ‹trail_true_cls Γ C› obtain L where "L ∈# C" and "trail_true_lit Γ L"
    by (auto simp: trail_true_cls_def)
  show ?thesis
    unfolding true_cls_def
  proof (rule bexI[OF _ ‹L ∈# C›])
    show "trail_interp Γ ⊫l L"
      by (rule trail_interp_lit_if_trail_true[OF ‹trail_consistent Γ› ‹trail_true_lit Γ L›])
  qed
qed

lemma trail_true_cls_iff_trail_interp_entails:
  assumes "trail_consistent Γ" "∀L ∈# C. trail_defined_lit Γ L"
  shows "trail_true_cls Γ C ⟷ trail_interp Γ ⊫ C"
proof (rule iffI)
  assume "trail_true_cls Γ C"
  thus "trail_interp Γ ⊫ C"
    using assms(1) trail_interp_cls_if_trail_true by fast
next
  assume "trail_interp Γ ⊫ C"
  then obtain L where "L ∈# C" and "trail_interp Γ ⊫l L"
    by (auto simp: true_cls_def)
  show "trail_true_cls Γ C"
  proof (cases L)
    case (Pos t)
    hence "t ∈ trail_interp Γ"
      using ‹trail_interp Γ ⊫l L› by simp
    then show ?thesis
      unfolding trail_true_cls_def
      using ‹L ∈# C› Pos
      by (metis assms(1) assms(2) trail_defined_lit_def trail_interp_lit_if_trail_true
          trail_true_lit_def true_lit_simps(2) uminus_Pos)
  next
    case (Neg t)
    then show ?thesis
      by (metis ‹L ∈# C› ‹trail_interp Γ ⊫l L› assms(1) assms(2) trail_defined_lit_def
          trail_interp_lit_if_trail_true trail_true_cls_def trail_true_lit_def true_lit_simps(1,2)
          uminus_Neg)
  qed
qed

lemma trail_false_cls_iff_not_trail_interp_entails:
  assumes "trail_consistent Γ" "∀L ∈# C. trail_defined_lit Γ L"
  shows "trail_false_cls Γ C ⟷ ¬ trail_interp Γ ⊫ C"
proof (rule iffI)
  show "trail_false_cls Γ C ⟹ ¬ trail_interp Γ ⊫ C"
    by (metis (mono_tags, opaque_lifting) assms(1) trail_false_cls_def trail_false_lit_def
        trail_interp_lit_if_trail_true trail_true_lit_def true_cls_def true_lit_iff
        true_lit_simps(1) true_lit_simps(2) uminus_Neg uminus_Pos)
next
  show "¬ trail_interp Γ ⊫ C ⟹ trail_false_cls Γ C"
    using assms(1) assms(2) trail_defined_cls_def trail_interp_cls_if_trail_true
      trail_true_or_false_cls_if_defined by blast
qed

inductive trail_closures_false where
  Nil[simp]: "trail_closures_false []" |
  Cons:
    "(∀D K γ. Kn = propagate_lit K D γ ⟶ trail_false_cls Γ (D ⋅ γ)) ⟹
    trail_closures_false Γ ⟹ trail_closures_false (Kn # Γ)"

lemma trail_closures_false_ConsD: "trail_closures_false (Ln # Γ) ⟹ trail_closures_false Γ"
  by (auto elim: trail_closures_false.cases)

lemma trail_closures_false_appendD: "trail_closures_false (Γ @ Γ') ⟹ trail_closures_false Γ'"
  by (induction Γ) (auto elim: trail_closures_false.cases)

lemma is_ground_lit_if_true_in_ground_trail:
  assumes "∀L ∈ fst ` set Γ. is_ground_lit L"
  shows "trail_true_lit Γ L ⟹ is_ground_lit L"
  using assms by (metis trail_true_lit_def)

lemma is_ground_lit_if_false_in_ground_trail:
  assumes "∀L ∈ fst ` set Γ. is_ground_lit L"
  shows "trail_false_lit Γ L ⟹ is_ground_lit L"
  using assms by (metis trail_false_lit_def atm_of_uminus is_ground_lit_def)

lemma is_ground_lit_if_defined_in_ground_trail:
  assumes "∀L ∈ fst ` set Γ. is_ground_lit L"
  shows "trail_defined_lit Γ L ⟹ is_ground_lit L"
  using assms is_ground_lit_if_true_in_ground_trail is_ground_lit_if_false_in_ground_trail
  unfolding trail_defined_lit_iff_true_or_false
  by fast

lemma is_ground_cls_if_false_in_ground_trail:
  assumes "∀L ∈ fst ` set Γ. is_ground_lit L"
  shows "trail_false_cls Γ C ⟹ is_ground_cls C"
  unfolding trail_false_cls_def is_ground_cls_def
  using assms by (auto intro: is_ground_lit_if_false_in_ground_trail)


section ‹SCL(FOL) Calculus›

locale scl_fol_calculus = renaming_apart renaming_vars
  for renaming_vars :: "'v set ⇒ 'v ⇒ 'v" +
  fixes less_B :: "('f, 'v) term ⇒ ('f, 'v) term ⇒ bool" (infix "≺⇩B" 50)
  assumes
    finite_less_B: "⋀β. finite {x. x ≺⇩B β}"
begin

abbreviation lesseq_B (infix "≼⇩B" 50) where
  "lesseq_B ≡ (≺⇩B)⇧=⇧="

subsection ‹Lemmas About @{term less_B}›

lemma lits_less_B_conv: "{L. atm_of L ≺⇩B β} = (⋃x∈{x. x ≺⇩B β}. {Pos x, Neg x})"
  by (rule Collect_lits_from_atms_conv)

lemma lits_eq_conv: "{L. atm_of L = β} = {Pos β, Neg β}"
  by (rule Collect_lits_from_atms_conv[of "λx. x = β", simplified])

lemma lits_less_eq_B_conv:
  "{L. atm_of L ≺⇩B β ∨ atm_of L = β} = insert (Pos β) (insert (Neg β) {L. atm_of L ≺⇩B β})"
  unfolding Collect_disj_eq lits_eq_conv by simp

lemma finite_lits_less_B: "finite {L. atm_of L ≺⇩B β}"
  unfolding lits_less_B_conv
proof (rule finite_UN_I)
  show "finite {x. x ≺⇩B β}"
    by (rule finite_less_B)
next
  show "⋀x. x ∈ {x. x ≺⇩B β} ⟹ finite {Pos x, Neg x}"
    by simp
qed

lemma finite_lits_less_eq_B: "finite {L. atm_of L ≼⇩B β}"
  using finite_lits_less_B by (simp add: lits_less_eq_B_conv)

lemma Collect_ball_eq_Pow_Collect: "{X. ∀x ∈ X. P x} = Pow {x. P x}"
  by blast

lemma finite_lit_clss_nodup_less_B: "finite {C. ∀L ∈# C. atm_of L ≺⇩B β ∧ count C L = 1}"
proof -
  have 1: "(∀L ∈# C. P L ∧ count C L = 1) ⟷ (∃C'. C = mset_set C' ∧ finite C' ∧ (∀L ∈ C'. P L))"
    for C P
    by (smt (verit) count_eq_zero_iff count_mset_set' finite_set_mset finite_set_mset_mset_set
        multiset_eqI)

  have 2: "finite {C'. ∀L∈C'. atm_of L ≺⇩B β}"
    unfolding Collect_ball_eq_Pow_Collect finite_Pow_iff
    by (rule finite_lits_less_B)

  show ?thesis
    unfolding 1
    unfolding setcompr_eq_image
    apply (rule finite_imageI)
    using 2 by simp
qed


subsection ‹Rules›

inductive propagate :: "('f, 'v) term clause fset ⇒ ('f, 'v) term ⇒ ('f, 'v) state ⇒
  ('f, 'v) state ⇒ bool" for N β where
  propagateI: "C |∈| N |∪| U ⟹ C = add_mset L C' ⟹ is_ground_cls (C ⋅ γ) ⟹
    ∀K ∈# C ⋅ γ. atm_of K ≼⇩B β ⟹
    C⇩0 = {#K ∈# C'. K ⋅l γ ≠ L ⋅l γ#} ⟹ C⇩1 = {#K ∈# C'. K ⋅l γ = L ⋅l γ#} ⟹
    trail_false_cls Γ (C⇩0 ⋅ γ) ⟹ ¬ trail_defined_lit Γ (L ⋅l γ) ⟹
    is_imgu μ {atm_of ` set_mset (add_mset L C⇩1)} ⟹
    propagate N β (Γ, U, None) (trail_propagate Γ (L ⋅l μ) (C⇩0 ⋅ μ) γ, U, None)"

lemma "C |∈| N |∪| U ⟹ C = add_mset L C' ⟹ is_ground_cls (C ⋅ γ) ⟹
    ∀K ∈# C. atm_of (K ⋅l γ) ≼⇩B β ⟹
    C⇩0 = {#K ∈# C'. K ⋅l γ ≠ L ⋅l γ#} ⟹ C⇩1 = {#K ∈# C'. K ⋅l γ = L ⋅l γ#} ⟹
    trail_false_cls Γ (C⇩0 ⋅ γ) ⟹ ¬ trail_defined_lit Γ (L ⋅l γ) ⟹
    is_imgu μ {atm_of ` set_mset (add_mset L C⇩1)} ⟹
    propagate N β (Γ, U, None) (trail_propagate Γ (L ⋅l μ) (C⇩0 ⋅ μ) γ, U, None)"
  apply (rule propagateI[of C N U L C' γ β _ _ Γ μ]; assumption?)
  by (metis Melem_subst_cls)

(* Whatch out for equality! *)

inductive decide :: "('f, 'v) term clause fset ⇒ ('f, 'v) term ⇒ ('f, 'v) state ⇒
  ('f, 'v) state ⇒ bool" for N β where
  decideI: "L ∈ ⋃(set_mset ` fset N) ⟹ is_ground_lit (L ⋅l γ) ⟹
    ¬ trail_defined_lit Γ (L ⋅l γ) ⟹ atm_of L ⋅a γ ≼⇩B β ⟹
    decide N β (Γ, U, None) (trail_decide Γ (L ⋅l γ), U, None)"

lemma "add_mset L C |∈| N ⟹ is_ground_lit (L ⋅l γ) ⟹
    ¬ trail_defined_lit Γ (L ⋅l γ) ⟹ atm_of L ⋅a γ ≼⇩B β ⟹
    decide N β (Γ, U, None) (trail_decide Γ (L ⋅l γ), U, None)"
  by (auto intro!: decideI)

inductive conflict :: "('f, 'v) term clause fset ⇒ ('f, 'v) term ⇒ ('f, 'v) state ⇒
  ('f, 'v) state ⇒ bool" for N β where
  conflictI: "D |∈| N |∪| U ⟹ is_ground_cls (D ⋅ γ) ⟹ trail_false_cls Γ (D ⋅ γ) ⟹
    conflict N β (Γ, U, None) (Γ, U, Some (D, γ))"

inductive skip :: "('f, 'v) term clause fset ⇒ ('f, 'v) term ⇒ ('f, 'v) state ⇒
  ('f, 'v) state ⇒ bool" for N β where
  skipI: "-L ∉# D ⋅ σ ⟹
    skip N β ((L, n) # Γ, U, Some (D, σ)) (Γ, U, Some (D, σ))"

lemma "-(fst 𝒦) ∉# D ⋅ σ ⟹ skip N β (𝒦 # Γ, U, Some (D, σ)) (Γ, U, Some (D, σ))"
  by (metis prod.exhaust_sel skipI)

inductive factorize :: "('f, 'v) term clause fset ⇒ ('f, 'v) term ⇒ ('f, 'v) state ⇒
  ('f, 'v) state ⇒ bool" for N β where
  factorizeI: "L ⋅l γ = L' ⋅l γ ⟹ is_imgu μ {{atm_of L, atm_of L'}} ⟹
    factorize N β (Γ, U, Some (add_mset L' (add_mset L D), γ)) (Γ, U, Some (add_mset L D ⋅ μ, γ))"

inductive resolve :: "('f, 'v) term clause fset ⇒ ('f, 'v) term ⇒ ('f, 'v) state ⇒
  ('f, 'v) state ⇒ bool" for N β where
  resolveI: "Γ = trail_propagate Γ' K D γ⇩D ⟹ K ⋅l γ⇩D = -(L ⋅l γ⇩C) ⟹
    is_renaming ρ⇩C ⟹ is_renaming ρ⇩D ⟹
    vars_cls (add_mset L C ⋅ ρ⇩C) ∩ vars_cls (add_mset K D ⋅ ρ⇩D) = {} ⟹
    is_imgu μ {{atm_of L ⋅a ρ⇩C, atm_of K ⋅a ρ⇩D}} ⟹
    is_grounding_merge γ
      (vars_cls (add_mset L C ⋅ ρ⇩C)) (rename_subst_domain ρ⇩C γ⇩C)
      (vars_cls (add_mset K D ⋅ ρ⇩D)) (rename_subst_domain ρ⇩D γ⇩D) ⟹
    resolve N β (Γ, U, Some (add_mset L C, γ⇩C)) (Γ, U, Some ((C ⋅ ρ⇩C + D ⋅ ρ⇩D) ⋅ μ, γ))"

(* Think about showing that the more specific rule from the paper is an instance of this generic rule. *)

inductive backtrack :: "('f, 'v) term clause fset ⇒ ('f, 'v) term ⇒ ('f, 'v) state ⇒
  ('f, 'v) state ⇒ bool" for N β where
  backtrackI: "Γ = trail_decide (Γ' @ Γ'') K ⟹ K = - (L ⋅l σ) ⟹
    ∄γ. is_ground_cls (add_mset L D ⋅ γ) ∧ trail_false_cls Γ'' (add_mset L D ⋅ γ) ⟹
    backtrack N β (Γ, U, Some (add_mset L D, σ)) (Γ'', finsert (add_mset L D) U, None)"

definition scl :: "('f, 'v) term clause fset ⇒ ('f, 'v) term ⇒ ('f, 'v) state ⇒
  ('f, 'v) state ⇒ bool" where
  "scl N β S S' ⟷ propagate N β S S' ∨ decide N β S S' ∨ conflict N β S S' ∨ skip N β S S' ∨
    factorize N β S S' ∨ resolve N β S S' ∨ backtrack N β S S'"

text ‹Note that, in contrast to Fiori and Weidenbach (CADE 2019), the set @{term N} of initial
clauses and the ground atom @{term β} are parameters of the relation instead of being repeated twice
in the states. This is to highlight the fact that they are constant.›


subsection ‹Well-Defined›

lemma propagate_well_defined:
  assumes "propagate N β S S'"
  shows
    "¬ decide N' β' S S'"
    "¬ conflict N' β' S S'"
    "¬ skip N' β' S S'"
    "¬ factorize N' β' S S'"
    "¬ resolve N' β' S S'"
    "¬ backtrack N' β' S S'"
proof -
  from assms obtain L C γ Γ U where
    S_def: "S = (Γ, U, None)" and
    S'_def: "S' = (trail_propagate Γ L C γ, U, None)"
    by (auto elim: propagate.cases)

  show "¬ decide N' β' S S'"
    using S_def S'_def
    by (auto simp add: decide_lit_def propagate_lit_def elim: decide.cases)

  show "¬ conflict N' β' S S'"
    using S_def S'_def
    by (auto elim: conflict.cases)

  show "¬ skip N' β' S S'"
    using S_def S'_def
    by (auto elim: skip.cases)

  show "¬ factorize N' β' S S'"
    using S_def S'_def
    by (auto elim: factorize.cases)

  show "¬ resolve N' β' S S'"
    using S_def S'_def
    by (auto elim: resolve.cases)

  show "¬ backtrack N' β' S S'"
    using S_def S'_def
    by (auto elim: backtrack.cases)
qed

lemma decide_well_defined:
  assumes "decide N β S S'"
  shows
    "¬ propagate N' β' S S'"
    "¬ conflict N' β' S S'"
    "¬ skip N' β' S S'"
    "¬ factorize N' β' S S'"
    "¬ resolve N' β' S S'"
    "¬ backtrack N' β' S S'"
proof -
  from assms obtain L γ Γ U where
    S_def: "S = (Γ, U, None)" and
    S'_def: "S' = (trail_decide Γ (L ⋅l γ), U, None)"
    by (auto elim: decide.cases)

  show "¬ propagate N' β' S S'"
    using S_def S'_def
    by (auto simp add: decide_lit_def propagate_lit_def elim: propagate.cases)

  show "¬ conflict N' β' S S'"
    using S_def S'_def
    by (auto elim: conflict.cases)

  show "¬ skip N' β' S S'"
    using S_def S'_def
    by (auto elim: skip.cases)

  show "¬ factorize N' β' S S'"
    using S_def S'_def
    by (auto elim: factorize.cases)

  show "¬ resolve N' β' S S'"
    using S_def S'_def
    by (auto elim: resolve.cases)

  show "¬ backtrack N' β' S S'"
    using S_def S'_def
    by (auto elim: backtrack.cases)
qed

lemma conflict_well_defined:
  assumes "conflict N β S S'"
  shows
    "¬ propagate N' β' S S'"
    "¬ decide N' β' S S'"
    "¬ skip N' β' S S'"
    "¬ factorize N' β' S S'"
    "¬ resolve N' β' S S'"
    "¬ backtrack N' β' S S'"
proof -
  from assms obtain C γ Γ U where
    S_def: "S = (Γ, U, None)" and
    S'_def: "S' = (Γ, U, Some (C, γ))"
    by (auto elim: conflict.cases)

  show "¬ propagate N' β' S S'"
    using S_def S'_def
    by (auto simp add: decide_lit_def propagate_lit_def elim: propagate.cases)

  show "¬ decide N' β' S S'"
    using S_def S'_def
    by (auto elim: decide.cases)

  show "¬ skip N' β' S S'"
    using S_def S'_def
    by (auto elim: skip.cases)

  show "¬ factorize N' β' S S'"
    using S_def S'_def
    by (auto elim: factorize.cases)

  show "¬ resolve N' β' S S'"
    using S_def S'_def
    by (auto elim: resolve.cases)

  show "¬ backtrack N' β' S S'"
    using S_def S'_def
    by (auto elim: backtrack.cases)
qed

lemma skip_well_defined:
  assumes "skip N β S S'"
  shows
    "¬ propagate N' β' S S'"
    "¬ decide N' β' S S'"
    "¬ conflict N' β' S S'"
    "¬ factorize N' β' S S'"
    "¬ resolve N' β' S S'"
    "¬ backtrack N' β' S S'"
proof -
  from assms obtain Ln Γ U opt where
    S_def: "S = (Ln # Γ, U, opt)" and
    S'_def: "S' = (Γ, U, opt)"
    by (auto elim: skip.cases)

  show "¬ propagate N' β' S S'"
    using S_def S'_def
    by (auto simp add: decide_lit_def propagate_lit_def elim: propagate.cases)

  show "¬ decide N' β' S S'"
    using S_def S'_def
    by (auto elim: decide.cases)

  show "¬ conflict N' β' S S'"
    using S_def S'_def
    by (auto elim: conflict.cases)

  show "¬ factorize N' β' S S'"
    using S_def S'_def
    by (auto elim: factorize.cases)

  show "¬ resolve N' β' S S'"
    using S_def S'_def
    by (auto elim: resolve.cases)

  show "¬ backtrack N' β' S S'"
    using S_def S'_def
    by (auto elim: backtrack.cases)
qed

lemma factorize_well_defined:
  assumes "factorize N β S S'"
  shows
    "¬ propagate N β S S'"
    "¬ decide N β S S'"
    "¬ conflict N β S S'"
    "¬ skip N β S S'"
    (* "¬ resolve N β S S'" *)
    "¬ backtrack N β S S'"
  using assms
  by (auto elim!: propagate.cases decide.cases conflict.cases skip.cases factorize.cases
          resolve.cases backtrack.cases
        simp: decide_lit_def propagate_lit_def)

lemma resolve_well_defined:
  assumes "resolve N β S S'"
  shows
    "¬ propagate N β S S'"
    "¬ decide N β S S'"
    "¬ conflict N β S S'"
    "¬ skip N β S S'"
    (* "¬ factorize N β S S'" *)
    "¬ backtrack N β S S'"
  using assms
  by (auto elim!: propagate.cases decide.cases conflict.cases skip.cases factorize.cases
          resolve.cases backtrack.cases
        simp: decide_lit_def propagate_lit_def)

lemma backtrack_well_defined:
  assumes "backtrack N β S S'"
  shows
    "¬ propagate N' β' S S'"
    "¬ decide N' β' S S'"
    "¬ conflict N' β' S S'"
    "¬ skip N' β' S S'"
    "¬ factorize N' β' S S'"
    "¬ resolve N' β' S S'"
proof -
  from assms obtain Γ Γ'' U C γ where
    S_def: "S = (Γ, U, Some (C, γ))" and
    S'_def: "S' = (Γ'', finsert (C) U, None)"
    by (auto elim: backtrack.cases)

  show "¬ propagate N' β' S S'"
    using S_def S'_def
    by (auto elim: propagate.cases)

  show "¬ decide N' β' S S'"
    using S_def S'_def
    by (auto elim: decide.cases)

  show "¬ conflict N' β' S S'"
    using S_def S'_def
    by (auto elim: conflict.cases)

  show "¬ skip N' β' S S'"
    using S_def S'_def
    by (auto elim: skip.cases)

  show "¬ factorize N' β' S S'"
    using S_def S'_def
    by (auto elim: factorize.cases)

  show "¬ resolve N' β' S S'"
    using S_def S'_def
    by (auto elim: resolve.cases)
qed


subsection ‹Miscellaneous Lemmas›

lemma conflict_set_after_factorization:
  assumes fact: "factorize N β S S'" and conflict_S: "state_conflict S = Some (C, γ)"
  shows "∃C' γ'. state_conflict S' = Some (C', γ') ∧ set_mset (C ⋅ γ) = set_mset (C' ⋅ γ')"
  using fact
proof (cases N β S S' rule: factorize.cases)
  case (factorizeI L γ L' μ Γ U D)

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

  have "L ⋅l μ ⋅l γ = L ⋅l γ"
    using ‹μ ⊙ γ = γ›
    by (metis subst_lit_comp_subst)

  moreover have "D ⋅ μ ⋅ γ = D ⋅ γ"
    using ‹μ ⊙ γ = γ›
    by (metis subst_cls_comp_subst)

  ultimately show ?thesis
    using conflict_S[symmetric]
    unfolding factorizeI(1,2)
    by (simp add: ‹L ⋅l γ = L' ⋅l γ›)
qed

lemma not_trail_false_ground_cls_if_no_conflict:
  assumes
    no_conf: "∄S'. conflict N β S S'" and
    could_conf: "state_conflict S = None" and
    C_in: "C |∈| N |∪| state_learned S" and
    gr_C_γ: "is_ground_cls (C ⋅ γ)"
  shows "¬ trail_false_cls (state_trail S) (C ⋅ γ)"
proof (rule notI)
  assume tr_false: "trail_false_cls (state_trail S) (C ⋅ γ)"

  from could_conf obtain Γ U where S_def: "S = (Γ, U, None)"
    by (metis prod_cases3 state_conflict_simp)

  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 add: S_def)
  next
    show "is_ground_cls (C ⋅ restrict_subst_domain (vars_cls C) γ)"
      using gr_C_γ by (simp add: subst_cls_restrict_subst_domain)
  next
    show "trail_false_cls Γ (C ⋅ restrict_subst_domain (vars_cls C) γ)"
      using tr_false by (simp add: S_def subst_cls_restrict_subst_domain)
  qed
  with no_conf show False
    by (simp add: S_def)
qed

lemma scl_mempty_not_in_sate_learned:
  "scl N β S S' ⟹ {#} |∉| state_learned S ⟹ {#} |∉| state_learned S'"
  unfolding scl_def
  by (elim disjE propagate.cases decide.cases conflict.cases skip.cases factorize.cases
      resolve.cases backtrack.cases) simp_all

lemma conflict_if_mempty_in_initial_clauses_and_no_conflict:
  assumes "{#} |∈| N" and "state_conflict S = None"
  shows "conflict N β S (state_trail S, state_learned S, Some ({#}, Var))"
proof -
  from assms(2) obtain Γ U where S_def: "S = (Γ, U, None)"
    by (metis snd_conv state_conflict_def surj_pair)

  show ?thesis
    unfolding S_def state_trail_simp state_learned_simp
  proof (rule conflictI[of "{#}" N _  Var _ _, unfolded subst_cls_empty])
    from assms(1) show "{#} |∈| N |∪| U"
      by simp
  qed simp_all
qed

lemma conflict_initial_state_if_mempty_in_intial_clauses:
  "{#} |∈| N ⟹ conflict N β initial_state ([], {||}, Some ({#}, Var))"
  using conflict_if_mempty_in_initial_clauses_and_no_conflict by auto

lemma conflict_empty_trail:
  assumes conf: "conflict N β S S'" and empty_trail: "state_trail S = []"
  shows "{#} |∈| N |∪| state_learned S"
  using conf
proof (cases N β S S' rule: conflict.cases)
  case (conflictI D U γ Γ)
  from empty_trail have "Γ = []"
    unfolding conflictI(1,2) by simp
  with ‹trail_false_cls Γ (D ⋅ γ)› have "D = {#}"
    using not_trail_false_Nil(2) subst_cls_empty_iff by blast
  with ‹D |∈| N |∪| U› show ?thesis
    unfolding conflictI(1,2) by simp
qed

lemma conflict_empty_trail':
  assumes "{#} |∈| N |∪| U"
  shows "∃S'. conflict N β ([], U, None) S'"
  by (metis assms is_ground_cls_empty not_trail_false_ground_cls_if_no_conflict state_conflict_simp
      state_learned_simp subst_cls_empty trail_false_cls_mempty)

lemma mempty_in_iff_ex_conflict: "{#} |∈| N |∪| U ⟷ (∃S'. conflict N β ([], U, None) S')"
  by (metis conflict_empty_trail conflict_empty_trail' state_learned_simp state_trail_simp)

lemma conflict_initial_state_only_with_mempty:
  assumes "conflict N β initial_state S"
  shows "∃γ. S = ([], {||}, Some ({#}, γ))"
  using assms(1)
proof (cases rule: conflict.cases)
  case (conflictI D γ)

  from ‹trail_false_cls [] (D ⋅ γ)› have "D ⋅ γ = {#}"
    using not_trail_false_Nil(2) by blast
  hence "D = {#}"
    by simp
  thus ?thesis
    using ‹S = ([], {||}, Some (D, γ))› by simp
qed

lemma no_more_step_if_conflict_mempty:
  assumes "state_trail S = []" "state_conflict S = Some ({#}, γ)"
  shows "∄S'. scl N β S S'"
  apply (rule notI)
  unfolding scl_def
  apply (insert assms)
  by (elim exE disjE propagate.cases decide.cases conflict.cases skip.cases factorize.cases
      resolve.cases backtrack.cases) simp_all

lemma ex_conflict_if_trail_false_cls:
  assumes tr_false_Γ_D: "trail_false_cls Γ D" and D_in: "D ∈ grounding_of_clss (fset N ∪ fset U)"
  shows "∃S'. conflict N β (Γ, U, None) S'"
proof -
  from D_in obtain D' γ' where
    D'_in: "D' |∈| N |∪| U" and D_def: "D = D' ⋅ γ'" and gr_D_γ: "is_ground_cls (D' ⋅ γ')"
    unfolding grounding_of_clss_def grounding_of_cls_def
    by (smt (verit, ccfv_threshold) D_in UN_iff grounding_ground mem_Collect_eq union_fset)

  define γ where
    "γ ≡ restrict_subst_domain (vars_cls D') γ'"

  have "conflict N β (Γ, U, None) (Γ, U, Some (D', γ))"
  proof (rule conflictI[OF D'_in])
    show "is_ground_cls (D' ⋅ γ)"
      using gr_D_γ by (simp add: γ_def subst_cls_restrict_subst_domain)
  next
    show "trail_false_cls Γ (D' ⋅ γ)"
      using tr_false_Γ_D by (simp add: D_def γ_def subst_cls_restrict_subst_domain)
  qed
  thus ?thesis
    by auto
qed

lemma no_conflict_tail_trail:
  assumes "∄S. conflict N β (Ln # Γ, U, None) S"
  shows "∄S. conflict N β (Γ, U, None) S"
proof (rule notI, erule exE)
  fix S assume "conflict N β (Γ, U, None) S"
  hence "∃S. conflict N β (Ln # Γ, U, None) S"
  proof (cases N β _ S rule: conflict.cases)
    case (conflictI D γ)
    have "conflict N β (Ln # Γ, U, None) (Ln # Γ, U, Some (D, γ))"
    proof (rule conflict.conflictI)
      show "D |∈| N |∪| U"
        by (rule conflictI)
    next
      show "is_ground_cls (D ⋅ γ)"
        by (rule conflictI)
    next
      show "trail_false_cls (Ln # Γ) (D ⋅ γ)"
        using ‹trail_false_cls Γ (D ⋅ γ)›
        by (simp add: trail_false_cls_def trail_false_lit_def)
    qed
    thus ?thesis
      by metis
  qed
  with assms show False
    by argo
qed

lemma subst_domain_rename_subst_domain_subset_vars_cls_subst_cls:
  assumes "∀x. is_Var (ρ⇩C x)" and
    dom_γ⇩C: "subst_domain γ⇩C ⊆ vars_cls (add_mset L C)"
  shows "subst_domain (rename_subst_domain ρ⇩C γ⇩C) ⊆ vars_cls (add_mset L C ⋅ ρ⇩C)"
proof -
  have "subst_domain (rename_subst_domain ρ⇩C γ⇩C) ⊆ the_Var ` ρ⇩C ` subst_domain γ⇩C"
    using subst_domain_rename_subst_domain_subset[OF ‹∀x. is_Var (ρ⇩C x)›] by simp
  also have "… ⊆ the_Var ` ρ⇩C ` vars_cls (add_mset L C)"
    using dom_γ⇩C by auto
  also have "… = (⋃x ∈ vars_cls (add_mset L C). vars_term (ρ⇩C x))"
    using image_the_Var_image_subst_renaming_eq[OF ‹∀x. is_Var (ρ⇩C x)›] by simp
  also have "… = vars_cls (add_mset L C ⋅ ρ⇩C)"
    using vars_subst_cls_eq by metis
  finally show dom_ren_dom_ρ⇩C_γ⇩C:
    "subst_domain (rename_subst_domain ρ⇩C γ⇩C) ⊆ vars_cls (add_mset L C ⋅ ρ⇩C)"
    by assumption
qed

lemma renamed_comp_renamed_simp:
  fixes γ⇩C γ⇩D
  assumes
    "K ⋅l γ⇩D = - (L ⋅l γ⇩C)" and
    ground_conf: "is_ground_cls (add_mset L C ⋅ γ⇩C)" and
    ground_prop: "is_ground_cls (add_mset K D ⋅ γ⇩D)" and
    dom_γ⇩D: "subst_domain γ⇩D ⊆ vars_cls (add_mset K D)" and
    ren_ρ⇩C: "is_renaming ρ⇩C" and
    ren_ρ⇩D: "is_renaming ρ⇩D" and
    disjoint_vars: "vars_cls (add_mset L C ⋅ ρ⇩C) ∩ vars_cls (add_mset K D ⋅ ρ⇩D) = {}"
  defines "γ ≡ rename_subst_domain ρ⇩D γ⇩D ⊙ rename_subst_domain ρ⇩C γ⇩C"
  shows
    subst_renamed_comp_renamed_simp:
      "L ⋅l ρ⇩C ⋅l γ = L ⋅l γ⇩C" "C ⋅ ρ⇩C ⋅ γ = C ⋅ γ⇩C"
      "K ⋅l ρ⇩D ⋅l γ = K ⋅l γ⇩D" "D ⋅ ρ⇩D ⋅ γ = D ⋅ γ⇩D" and
    imgu_comp_renamed_comp_renamed_simp:
      "is_imgu μ {{atm_of L ⋅a ρ⇩C, atm_of K ⋅a ρ⇩D}} ⟹ μ ⊙ γ = γ"
proof -
  have subst_adapt_ρ⇩D_γ⇩D:
    "subst_domain (rename_subst_domain ρ⇩D γ⇩D) ∩ vars_cls (add_mset L C ⋅ ρ⇩C) = {}"
    using disjoint_vars ren_ρ⇩D dom_γ⇩D
      subst_domain_rename_subst_domain_subset_vars_cls_subst_cls
    by (metis Int_commute Orderings.order_eq_iff ground_prop is_renaming_iff
        subst_renaming_subst_adapted vars_cls_subset_subst_domain_if_grounding)

  show "C ⋅ ρ⇩C ⋅ γ = C ⋅ γ⇩C"
  proof -
    have "C ⋅ ρ⇩C ⋅ rename_subst_domain ρ⇩C γ⇩C = C ⋅ γ⇩C"
    proof (rule subst_renaming_subst_adapted[OF ren_ρ⇩C])
      show "vars_cls C ⊆ subst_domain γ⇩C"
        using vars_cls_subset_subst_domain_if_grounding[OF ground_conf] by simp
    qed
    moreover have "C ⋅ ρ⇩C ⋅ rename_subst_domain ρ⇩D γ⇩D = C ⋅ ρ⇩C"
    proof (rule subst_cls_idem_if_disj_vars)
      show "subst_domain (rename_subst_domain ρ⇩D γ⇩D) ∩ vars_cls (C ⋅ ρ⇩C) = {}"
        using subst_adapt_ρ⇩D_γ⇩D by auto
    qed
    ultimately show ?thesis
      unfolding γ_def by simp
  qed

  show "D ⋅ ρ⇩D ⋅ γ = D ⋅ γ⇩D"
  proof -
    have "D ⋅ ρ⇩D ⋅ rename_subst_domain ρ⇩D γ⇩D = D ⋅ γ⇩D"
    proof (rule subst_renaming_subst_adapted[OF ren_ρ⇩D])
      show "vars_cls D ⊆ subst_domain γ⇩D"
        using vars_cls_subset_subst_domain_if_grounding[OF ground_prop] by simp
    qed
    moreover have "D ⋅ γ⇩D ⋅ rename_subst_domain ρ⇩C γ⇩C = D ⋅ γ⇩D"
        using ground_prop by simp
    ultimately show ?thesis
      unfolding γ_def by simp
  qed

  show "L ⋅l ρ⇩C ⋅l γ = L ⋅l γ⇩C"
  proof -
    have "L ⋅l ρ⇩C ⋅l rename_subst_domain ρ⇩C γ⇩C = L ⋅l γ⇩C"
    proof (rule subst_lit_renaming_subst_adapted[OF ren_ρ⇩C])
      show "vars_lit L ⊆ subst_domain γ⇩C"
        using ground_conf
        by (simp add: vars_lit_subset_subst_domain_if_grounding)
    qed
    moreover have "L ⋅l ρ⇩C ⋅l rename_subst_domain ρ⇩D γ⇩D = L ⋅l ρ⇩C"
    proof (rule subst_lit_idem_if_disj_vars)
      show "subst_domain (rename_subst_domain ρ⇩D γ⇩D) ∩ vars_lit (L ⋅l ρ⇩C) = {}"
        using subst_adapt_ρ⇩D_γ⇩D by auto
    qed
    ultimately show ?thesis
      unfolding γ_def
      by (simp add: literal.expand)
  qed

  moreover show "K ⋅l ρ⇩D ⋅l γ = K ⋅l γ⇩D"
  proof -
    have "⋀σ. K ⋅l γ⇩D ⋅l σ = K ⋅l γ⇩D"
      using ground_prop by (simp add: is_ground_lit_def)
    moreover have "K ⋅l ρ⇩D ⋅l rename_subst_domain ρ⇩D γ⇩D = K ⋅l γ⇩D"
    proof (rule subst_lit_renaming_subst_adapted[OF ren_ρ⇩D])
      show "vars_lit K ⊆ subst_domain γ⇩D"
        using ground_prop
        by (simp add: vars_lit_subset_subst_domain_if_grounding)
    qed
    ultimately show ?thesis
      unfolding γ_def
      by (simp add: literal.expand)
  qed
  ultimately have "atm_of L ⋅a ρ⇩C ⋅a γ = atm_of K ⋅a ρ⇩D ⋅a γ"
    using ‹K ⋅l γ⇩D = - (L ⋅l γ⇩C)›
    by (metis atm_of_subst_lit atm_of_uminus)
  hence "is_unifiers γ {{atm_of L ⋅a ρ⇩C, atm_of K ⋅a ρ⇩D}}"
    by (simp add: is_unifiers_def is_unifier_alt)

  moreover assume imgu_μ: "is_imgu μ {{atm_of L ⋅a ρ⇩C, atm_of K ⋅a ρ⇩D}}"

  ultimately show  "μ ⊙ γ = γ"
    by (auto simp: is_imgu_def)
qed


section ‹Invariants›


subsection ‹Initial Literals Generalize Learned, Trail, and Conflict Literals›

definition clss_lits_generalize_clss_lits where
  "clss_lits_generalize_clss_lits N U ⟷
    (∀L ∈ ⋃ (set_mset ` U). ∃K ∈ ⋃(set_mset ` N). generalizes_lit K L)"

lemma clss_lits_generalize_clss_lits_if_superset[simp]:
  assumes "N2 ⊆ N1"
  shows "clss_lits_generalize_clss_lits N1 N2"
proof (unfold clss_lits_generalize_clss_lits_def, rule ballI)
  fix L
  assume L_in: "L ∈ ⋃ (set_mset ` N2)"
  show "∃K ∈ ⋃ (set_mset ` N1). generalizes_lit K L"
    unfolding generalizes_lit_def
  proof (intro bexI exI conjI)
    show "L ∈ ⋃ (set_mset ` N1)"
      using L_in ‹N2 ⊆ N1› by blast
  next
    show "L ⋅l Var = L"
      by simp
  qed
qed

lemma clss_lits_generalize_clss_lits_subset:
  "clss_lits_generalize_clss_lits N U1 ⟹ U2 ⊆ U1 ⟹ clss_lits_generalize_clss_lits N U2"
  unfolding clss_lits_generalize_clss_lits_def by blast

lemma clss_lits_generalize_clss_lits_insert:
  "clss_lits_generalize_clss_lits N (insert C U) ⟷
    (∀L ∈# C. ∃K ∈ ⋃(set_mset ` N). generalizes_lit K L) ∧ clss_lits_generalize_clss_lits N U"
  unfolding clss_lits_generalize_clss_lits_def by blast

lemma clss_lits_generalize_clss_lits_trans:
  assumes
    "clss_lits_generalize_clss_lits N1 N2" and
    "clss_lits_generalize_clss_lits N2 N3"
  shows "clss_lits_generalize_clss_lits N1 N3"
proof (unfold clss_lits_generalize_clss_lits_def, rule ballI)
  fix L3
  assume "L3 ∈ ⋃ (set_mset ` N3)"
  then obtain L2 σ2 where "L2 ∈ ⋃ (set_mset ` N2)" and "L2 ⋅l σ2 = L3"
    using assms(2)[unfolded clss_lits_generalize_clss_lits_def] generalizes_lit_def by meson
  then obtain L1 σ1 where "L1 ∈ ⋃ (set_mset ` N1)" and "L1 ⋅l σ1 = L2"
    using assms(1)[unfolded clss_lits_generalize_clss_lits_def] generalizes_lit_def by meson
  
  thus "∃K ∈ ⋃ (set_mset ` N1). generalizes_lit K L3"
    unfolding generalizes_lit_def
  proof (intro bexI exI conjI)
    show "L1 ⋅l (σ1 ⊙ σ2) = L3"
      by (simp add: ‹L1 ⋅l σ1 = L2› ‹L2 ⋅l σ2 = L3›)
  qed simp_all
qed

lemma clss_lits_generalize_clss_lits_subst_clss:
  assumes "clss_lits_generalize_clss_lits N1 N2"
  shows "clss_lits_generalize_clss_lits N1 ((λC. C ⋅ σ) ` N2)"
  unfolding clss_lits_generalize_clss_lits_def
proof (rule ballI)
  fix L assume "L ∈ ⋃ (set_mset ` (λC. C ⋅ σ) ` N2)"
  then obtain L⇩2 where "L⇩2 ∈ ⋃ (set_mset ` N2)" and L_def: "L = L⇩2 ⋅l σ" by auto
  then obtain L⇩1 σ⇩1 where L⇩1_in: "L⇩1 ∈ ⋃ (set_mset ` N1)" and L⇩2_def: "L⇩2 = L⇩1 ⋅l σ⇩1"
    using assms[unfolded clss_lits_generalize_clss_lits_def]
    unfolding generalizes_lit_def by metis

  show "∃K ∈ ⋃ (set_mset ` N1). generalizes_lit K L"
    unfolding generalizes_lit_def
  proof (intro bexI exI)
    show "L⇩1 ∈ ⋃ (set_mset ` N1)"
      by (rule L⇩1_in)
  next
    show "L⇩1 ⋅l (σ⇩1 ⊙ σ) = L"
      unfolding L_def L⇩2_def by simp
  qed
qed

lemma clss_lits_generalize_clss_lits_singleton_subst_cls:
  "clss_lits_generalize_clss_lits N {C} ⟹ clss_lits_generalize_clss_lits N {C ⋅ σ}"
  by (rule clss_lits_generalize_clss_lits_subst_clss[of N "{C}" σ, simplified])

lemma clss_lits_generalize_clss_lits_subst_cls:
  assumes "clss_lits_generalize_clss_lits N {add_mset L1 (add_mset L2 C)}"
  shows "clss_lits_generalize_clss_lits N {add_mset (L1 ⋅l σ) (C ⋅ σ)}"
proof (rule clss_lits_generalize_clss_lits_trans)
  show "clss_lits_generalize_clss_lits N {add_mset L1 (add_mset L2 C) ⋅ σ}"
    by (rule clss_lits_generalize_clss_lits_singleton_subst_cls[of N _ σ, OF assms])
next
  show "clss_lits_generalize_clss_lits {add_mset L1 (add_mset L2 C) ⋅ σ}
    {add_mset (L1 ⋅l σ) (C ⋅ σ)}"
    apply (simp add: clss_lits_generalize_clss_lits_def generalizes_lit_def)
    using subst_lit_id_subst by blast
qed

definition initial_lits_generalize_learned_trail_conflict where
  "initial_lits_generalize_learned_trail_conflict N S ⟷ clss_lits_generalize_clss_lits (fset N)
    (fset (state_learned S |∪| clss_of_trail (state_trail S) |∪|
      (case state_conflict S of None ⇒ {||} | Some (C, _) ⇒ {|C|})))"

lemma initial_lits_generalize_learned_trail_conflict_initial_state[simp]:
  "initial_lits_generalize_learned_trail_conflict N initial_state"
  unfolding initial_lits_generalize_learned_trail_conflict_def by simp

lemma propagate_preserves_initial_lits_generalize_learned_trail_conflict:
  "propagate N β S S' ⟹ initial_lits_generalize_learned_trail_conflict N S ⟹
    initial_lits_generalize_learned_trail_conflict N S'"
proof (induction S S' rule: propagate.induct)
  case (propagateI C U L C' γ C⇩0 C⇩1 Γ μ)

  from propagateI.prems have
    N_generalize: "clss_lits_generalize_clss_lits (fset N) (fset (U |∪| clss_of_trail Γ))"
    unfolding initial_lits_generalize_learned_trail_conflict_def by simp_all

  from propagateI.hyps have
    C_in: "C |∈| N |∪| U" and
    C_def: "C = add_mset L C'" and
    C⇩0_def: "C⇩0 = {#K ∈# C'. K ⋅l γ ≠ L ⋅l γ#}" by simp_all

  have "clss_lits_generalize_clss_lits (fset N)
    (insert (add_mset L C⇩0 ⋅ μ) (fset (U |∪| clss_of_trail Γ)))"
    unfolding clss_lits_generalize_clss_lits_insert
  proof (rule conjI)
    show "∀L ∈# add_mset L C⇩0 ⋅ μ. ∃K∈⋃ (set_mset ` fset N). generalizes_lit K L"
    proof (rule ballI)
      fix K assume "K ∈# add_mset L C⇩0 ⋅ μ"
      hence "K = L ⋅l μ ∨ (∃M. M ∈# C⇩0 ∧ K = M ⋅l μ)"
        by auto
      then obtain K' where K'_in: "K' ∈# C" and K_def: "K = K' ⋅l μ"
        using C⇩0_def C_def by auto
      
      obtain D L⇩D where "D |∈| N" and "L⇩D ∈# D" and "generalizes_lit L⇩D K'"
        using K'_in C_in N_generalize[unfolded clss_lits_generalize_clss_lits_def]
        by (metis (mono_tags, opaque_lifting) UN_iff funion_iff generalizes_lit_refl)

      show "∃K'∈⋃ (set_mset ` fset N). generalizes_lit K' K"
      proof (rule bexI)
        show "generalizes_lit L⇩D K"
          using ‹generalizes_lit L⇩D K'› 
          by (metis generalizes_lit_def K_def subst_lit_comp_subst)
      next
        show ‹L⇩D ∈ ⋃ (set_mset ` fset N)›
          using ‹D |∈| N› ‹L⇩D ∈# D›
          by (meson UN_I)
      qed
    qed
  next
    show "clss_lits_generalize_clss_lits (fset N) (fset (U |∪| clss_of_trail Γ))"
      by (rule N_generalize)
  qed
  thus ?case
    by (simp add: initial_lits_generalize_learned_trail_conflict_def propagate_lit_def)
qed

lemma decide_preserves_initial_lits_generalize_learned_trail_conflict:
  "decide N β S S' ⟹ initial_lits_generalize_learned_trail_conflict N S ⟹
    initial_lits_generalize_learned_trail_conflict N S'"
proof (induction S S' rule: decide.induct)
  case (decideI L Γ U)
  thus ?case
    by (simp add: decide_lit_def initial_lits_generalize_learned_trail_conflict_def)
qed

lemma conflict_preserves_initial_lits_generalize_learned_trail_conflict:
  assumes "conflict N β S S'" and "initial_lits_generalize_learned_trail_conflict N S"
  shows "initial_lits_generalize_learned_trail_conflict N S'"
  using assms(1)
proof (cases N β S S' rule: conflict.cases)
  case (conflictI D U γ Γ)
  from assms(2) have "clss_lits_generalize_clss_lits (fset N) (fset (U |∪| clss_of_trail Γ))"
    unfolding conflictI(1) by (simp add: initial_lits_generalize_learned_trail_conflict_def)
  hence ball_U_Γ_generalize:
    "⋀L. L ∈ ⋃ (set_mset ` fset (U |∪| clss_of_trail Γ)) ⟹
      ∃K ∈ ⋃ (set_mset ` fset N). generalizes_lit K L"
    unfolding clss_lits_generalize_clss_lits_def by blast

  have "clss_lits_generalize_clss_lits (fset N) (insert D (fset (U |∪| clss_of_trail Γ)))"
    unfolding clss_lits_generalize_clss_lits_def
  proof (rule ballI)
    fix L assume "L ∈ ⋃ (set_mset ` insert D (fset (U |∪| clss_of_trail Γ)))"
    hence "L ∈ set_mset D ∨ L ∈ ⋃ (set_mset ` (fset (U |∪| clss_of_trail Γ)))"
      by simp
    thus "∃K ∈ ⋃ (set_mset ` fset N). generalizes_lit K L"
    proof (elim disjE)
      assume L_in: "L ∈# D"
      show "?thesis"
        using ‹D |∈| N |∪| U›[unfolded funion_iff]
      proof (elim disjE)
        show "D |∈| N ⟹ ?thesis"
          using L_in
          by (meson UN_I generalizes_lit_refl)
      next
        assume "D |∈| U"
        hence "∃K ∈ ⋃ (set_mset ` fset N). generalizes_lit K L"
          using ball_U_Γ_generalize[of L] L_in
          using mk_disjoint_finsert by fastforce
        thus ?thesis
          by metis
      qed
    next
      show "L ∈ ⋃ (set_mset ` fset (U |∪| clss_of_trail Γ)) ⟹ ?thesis"
        using ball_U_Γ_generalize by simp
    qed
  qed
  then show ?thesis
    using assms(2)
    unfolding conflictI(1,2)
    by (simp add: initial_lits_generalize_learned_trail_conflict_def)
qed

lemma skip_preserves_initial_lits_generalize_learned_trail_conflict:
  "skip N β S S' ⟹ initial_lits_generalize_learned_trail_conflict N S ⟹
    initial_lits_generalize_learned_trail_conflict N S'"
proof (induction S S' rule: skip.induct)
  case (skipI L D σ Cl Γ U)
  then show ?case
    unfolding initial_lits_generalize_learned_trail_conflict_def
    unfolding state_learned_simp state_conflict_simp state_trail_simp option.case prod.case
    by (auto elim: clss_lits_generalize_clss_lits_subset)
qed

lemma factorize_preserves_initial_lits_generalize_learned_trail_conflict:
  "factorize N β S S' ⟹ initial_lits_generalize_learned_trail_conflict N S ⟹
    initial_lits_generalize_learned_trail_conflict N S'"
proof (induction S S' rule: factorize.induct)
  case (factorizeI L γ L' μ Γ U D)
  moreover have "clss_lits_generalize_clss_lits (fset N) {add_mset (L ⋅l μ) (D ⋅ μ)}"
    using factorizeI
    unfolding initial_lits_generalize_learned_trail_conflict_def
    apply (simp add: clss_lits_generalize_clss_lits_insert generalizes_lit_def)
    by (smt (verit, best) Melem_subst_cls subst_lit_comp_subst)
  ultimately show ?case
    unfolding initial_lits_generalize_learned_trail_conflict_def
    apply simp
    using clss_lits_generalize_clss_lits_insert by blast
qed

lemma resolve_preserves_initial_lits_generalize_learned_trail_conflict:
  "resolve N β S S' ⟹ initial_lits_generalize_learned_trail_conflict N S ⟹
    initial_lits_generalize_learned_trail_conflict N S'"
proof (induction S S' rule: resolve.induct)
  case (resolveI Γ Γ' K D δ⇩D L δ⇩C ρ⇩C ρ⇩D C μ γ U)
  moreover have "clss_lits_generalize_clss_lits (fset N) {(C ⋅ ρ⇩C + D ⋅ ρ⇩D) ⋅ μ}"
  proof -
    from resolveI.prems have
      N_lits_sup: "clss_lits_generalize_clss_lits (fset N)
        (fset (U |∪| clss_of_trail Γ |∪| {|add_mset L C|}))"
      unfolding initial_lits_generalize_learned_trail_conflict_def by simp

    have "clss_lits_generalize_clss_lits (fset N) {C ⋅ ρ⇩C ⋅ μ}"
    proof -
      from N_lits_sup have "clss_lits_generalize_clss_lits (fset N) {add_mset L C}"
        by (simp add: clss_lits_generalize_clss_lits_insert)
      hence "clss_lits_generalize_clss_lits (fset N) {C}"
        by (simp add: clss_lits_generalize_clss_lits_def)
      thus ?thesis
        by (auto intro: clss_lits_generalize_clss_lits_singleton_subst_cls)
    qed
    moreover have "clss_lits_generalize_clss_lits (fset N) {D ⋅ ρ⇩D ⋅ μ}"
    proof -
      from N_lits_sup have "clss_lits_generalize_clss_lits (fset N) (fset (clss_of_trail Γ))"
        by (rule clss_lits_generalize_clss_lits_subset) auto
      hence "clss_lits_generalize_clss_lits (fset N) {add_mset K D}"
        unfolding resolveI.hyps
        by (simp add: clss_lits_generalize_clss_lits_insert propagate_lit_def)
      hence "clss_lits_generalize_clss_lits (fset N) {D}"
        by (simp add: clss_lits_generalize_clss_lits_def)
      thus ?thesis
        by (auto intro: clss_lits_generalize_clss_lits_singleton_subst_cls)
    qed
    ultimately show ?thesis
      by (auto simp add: clss_lits_generalize_clss_lits_def)
  qed
  ultimately show ?case
    unfolding initial_lits_generalize_learned_trail_conflict_def
    unfolding state_trail_simp state_learned_simp state_conflict_simp
    unfolding option.case prod.case
    by (metis clss_lits_generalize_clss_lits_insert finsert.rep_eq funion_finsert_right)
qed

lemma backtrack_preserves_initial_lits_generalize_learned_trail_conflict:
  "backtrack N β S S' ⟹ initial_lits_generalize_learned_trail_conflict N S ⟹
    initial_lits_generalize_learned_trail_conflict N S'"
proof (induction S S' rule: backtrack.induct)
  case (backtrackI Γ Γ' Γ'' L σ D U)
  then show ?case
    unfolding initial_lits_generalize_learned_trail_conflict_def
    apply (simp add: clss_of_trail_append)
    apply (erule clss_lits_generalize_clss_lits_subset)
    by blast
qed

lemma scl_preserves_initial_lits_generalize_learned_trail_conflict:
  assumes "scl N β S S'" and "initial_lits_generalize_learned_trail_conflict N S"
  shows "initial_lits_generalize_learned_trail_conflict N S'"
  using assms unfolding scl_def
  using propagate_preserves_initial_lits_generalize_learned_trail_conflict
    decide_preserves_initial_lits_generalize_learned_trail_conflict
    conflict_preserves_initial_lits_generalize_learned_trail_conflict
    skip_preserves_initial_lits_generalize_learned_trail_conflict
    factorize_preserves_initial_lits_generalize_learned_trail_conflict
    resolve_preserves_initial_lits_generalize_learned_trail_conflict
    backtrack_preserves_initial_lits_generalize_learned_trail_conflict
  by metis


subsection ‹Trail Literals Come From Clauses›

definition trail_lits_from_clauses where
  "trail_lits_from_clauses N S ⟷
    (∀L ∈ fst ` set (state_trail S).
      ∃L' ∈ ⋃(set_mset ` (fset N ∪ fset (state_learned S))). generalizes_lit L' L)"

lemma trail_lits_from_clauses_initial_state[simp]: "trail_lits_from_clauses N initial_state"
  by (simp add: trail_lits_from_clauses_def)

lemma propagate_preserves_trail_lits_from_clauses:
  assumes "propagate N β S S'" and "trail_lits_from_clauses N S"
  shows "trail_lits_from_clauses N S'"
  using assms(1)
proof (cases N β S S' rule: propagate.cases)
  case (propagateI C U L C' γ C⇩0 C⇩1 Γ μ)

  have "∃L'∈ ⋃ (fset (set_mset |`| (N |∪| U))). generalizes_lit L' (L ⋅l μ ⋅l γ)"
  proof (rule bexI[of _ L])
    show "L ∈ ⋃ (fset (set_mset |`| (N |∪| U)))"
      using ‹C |∈| N |∪| U› ‹C = add_mset L C'›
      by (meson Union_iff fimage_eqI union_single_eq_member)
  next
    show "generalizes_lit L (L ⋅l μ ⋅l γ)"
      unfolding generalizes_lit_def by (metis subst_lit_comp_subst)
  qed

  moreover have "∀L ∈ fst ` set Γ. ∃L' ∈ ⋃ (fset (set_mset |`| (N |∪| U))). generalizes_lit L' L"
    using assms(2) unfolding propagateI by (simp add: trail_lits_from_clauses_def)

  ultimately show ?thesis
    unfolding propagateI(2) by (simp add: trail_lits_from_clauses_def propagate_lit_def)
qed

lemma decide_preserves_trail_lits_from_clauses:
  assumes "decide N β S S'" and "trail_lits_from_clauses N S"
  shows "trail_lits_from_clauses N S'"
  using assms(1)
proof (cases N β S S' rule: decide.cases)
  case (decideI L γ Γ U)

  hence "∃L'∈⋃ (fset (set_mset |`| (N |∪| U))). generalizes_lit L' (L ⋅l γ)"
    by (auto simp: generalizes_lit_def)

  moreover have "∀L ∈ fst ` set Γ. ∃L' ∈ ⋃ (fset (set_mset |`| (N |∪| U))). generalizes_lit L' L"
    using assms(2) unfolding decideI by (simp add: trail_lits_from_clauses_def)

  ultimately show ?thesis
    unfolding decideI by (simp add: trail_lits_from_clauses_def decide_lit_def)
qed

lemma conflict_preserves_trail_lits_from_clauses:
  assumes "conflict N β S S'" and "trail_lits_from_clauses N S"
  shows "trail_lits_from_clauses N S'"
  using assms(1)
proof (cases N β S S' rule: conflict.cases)
  case (conflictI D U γ Γ)
  thus ?thesis
    using assms(2) by (simp add: trail_lits_from_clauses_def)
qed

lemma skip_preserves_trail_lits_from_clauses:
  assumes "skip N β S S'" and "trail_lits_from_clauses N S"
  shows "trail_lits_from_clauses N S'"
  using assms(1)
proof (cases N β S S' rule: skip.cases)
  case (skipI L D σ n Γ U)
  thus ?thesis
    using assms(2) by (simp add: trail_lits_from_clauses_def)
qed

lemma factorize_preserves_trail_lits_from_clauses:
  assumes "factorize N β S S'" and "trail_lits_from_clauses N S"
  shows "trail_lits_from_clauses N S'"
  using assms(1)
proof (cases N β S S' rule: factorize.cases)
  case (factorizeI L γ L' μ Γ U D)
  thus ?thesis
    using assms(2) by (simp add: trail_lits_from_clauses_def)
qed

lemma resolve_preserves_trail_lits_from_clauses:
  assumes "resolve N β S S'" and "trail_lits_from_clauses N S"
  shows "trail_lits_from_clauses N S'"
  using assms(1)
proof (cases N β S S' rule: resolve.cases)
  case (resolveI Γ Γ' L C δ ρ U D L' σ μ)
  thus ?thesis
    using assms(2) by (simp add: trail_lits_from_clauses_def)
qed

lemma backtrack_preserves_trail_lits_from_clauses:
  assumes "backtrack N β S S'" and "trail_lits_from_clauses N S"
  shows "trail_lits_from_clauses N S'"
  using assms(1)
proof (cases N β S S' rule: backtrack.cases)
  case (backtrackI Γ Γ' Γ'' K L σ D U)
  hence "suffix Γ'' Γ"
    by (simp add: suffixI decide_lit_def)
  hence "set Γ'' ⊆ set Γ"
    by (simp add: set_mono_suffix)

  moreover have "∀L ∈ fst ` set Γ. ∃L' ∈ ⋃ (fset (set_mset |`| (N |∪| U))). generalizes_lit L' L"
    using assms(2) unfolding backtrackI by (simp add: trail_lits_from_clauses_def)

  ultimately have "∀L ∈ fst ` set Γ''. ∃L' ∈ ⋃ (fset (set_mset |`| (N |∪| U))). generalizes_lit L' L"
    by fast
  thus ?thesis
    unfolding trail_lits_from_clauses_def backtrackI(1,2) state_trail_simp state_learned_simp
    by auto
qed

lemma scl_preserves_trail_lits_from_clauses:
  assumes "scl N β S S'" and "trail_lits_from_clauses N S"
  shows "trail_lits_from_clauses N S'"
  using assms unfolding scl_def
  using propagate_preserves_trail_lits_from_clauses decide_preserves_trail_lits_from_clauses
    conflict_preserves_trail_lits_from_clauses skip_preserves_trail_lits_from_clauses
    factorize_preserves_trail_lits_from_clauses resolve_preserves_trail_lits_from_clauses
    backtrack_preserves_trail_lits_from_clauses
  by metis


subsection ‹Trail Literals Come From Initial Clauses›

definition trail_lits_from_init_clauses where
  "trail_lits_from_init_clauses N S ⟷
    (∀L ∈ fst ` set (state_trail S). ∃L' ∈ ⋃(set_mset ` fset N). generalizes_lit L' L)"

lemma trail_lits_from_init_clausesI:
  assumes "trail_lits_from_clauses N S" and "initial_lits_generalize_learned_trail_conflict N S"
  shows "trail_lits_from_init_clauses N S"
  unfolding trail_lits_from_init_clauses_def
proof (rule ballI)
  fix L assume "L ∈ fst ` set (state_trail S)"
  with assms(1) obtain L' where
    "L' ∈ ⋃ (set_mset ` (fset N ∪ fset (state_learned S))) ∧ generalizes_lit L' L"
    unfolding trail_lits_from_clauses_def by metis
  hence "(∃x∈fset N. L' ∈# x) ∨ (∃x ∈ fset (state_learned S). L' ∈# x)" and "generalizes_lit L' L"
    by simp_all
  thus "∃L'∈⋃ (set_mset ` fset N). generalizes_lit L' L"
  proof (elim disjE bexE)
    fix C assume "C ∈ fset N"
    thus "L' ∈# C ⟹ ?thesis"
      using ‹generalizes_lit L' L› by auto
  next
    fix C assume "C ∈ fset (state_learned S)" and "L' ∈# C"
    with assms(2) have "∃K∈⋃ (set_mset ` fset N). generalizes_lit K L'"
      unfolding initial_lits_generalize_learned_trail_conflict_def
        clss_lits_generalize_clss_lits_def
      by auto
    thus "?thesis"
      using ‹generalizes_lit L' L› by (metis generalizes_lit_def subst_lit_comp_subst)
  qed
qed


subsection ‹Trail Literals Are Ground›

definition trail_lits_ground where
  "trail_lits_ground S ⟷ (∀L ∈ fst ` set (state_trail S). is_ground_lit L)"

lemma trail_lits_ground_initial_state[simp]: "trail_lits_ground initial_state"
  by (simp add: trail_lits_ground_def)

lemma propagate_preserves_trail_lits_ground:
  assumes "propagate N β S S'" and "trail_lits_ground S"
  shows "trail_lits_ground S'"
  using assms(1)
proof (cases N β S S' rule: propagate.cases)
  case (propagateI C U L C' γ C⇩0 C⇩1 Γ μ)
  hence "is_ground_lit (L ⋅l γ)"
    by (meson Melem_subst_cls is_ground_cls_def mset_subset_eqD mset_subset_eq_add_right
        union_single_eq_member)

  moreover have "∀τ. is_unifiers τ {atm_of ` set_mset (add_mset L C⇩1)} ⟶ τ = μ ⊙ τ"
    using ‹is_imgu μ {atm_of ` set_mset (add_mset L C⇩1)}›
    by (simp add: is_imgu_def)

  moreover have "is_unifiers γ {atm_of ` set_mset (add_mset L C⇩1)}"
    by (auto simp: is_unifiers_def is_unifier_alt ‹C⇩1 = {#K ∈# C'. K ⋅l γ = L ⋅l γ#}›
        intro: subst_atm_of_eqI)

  ultimately have "is_ground_lit (L ⋅l μ ⋅l γ)"
    by (metis subst_lit_comp_subst)

  moreover have "∀L ∈ fst ` set Γ. is_ground_lit L"
    using ‹trail_lits_ground S› by (simp add: propagateI(1) trail_lits_ground_def)

  ultimately show ?thesis
    by (simp add: propagateI(2) trail_lits_ground_def propagate_lit_def)
qed

lemma decide_preserves_trail_lits_ground:
  assumes "decide N β S S'" and "trail_lits_ground S"
  shows "trail_lits_ground S'"
  using assms(1)
proof (cases N β S S' rule: decide.cases)
  case (decideI L γ Γ U)
  hence "is_ground_lit (L ⋅l γ)"
    by metis

  moreover have "∀L ∈ fst ` set Γ. is_ground_lit L"
    using assms(2) by (simp add: decideI(1) trail_lits_ground_def)

  ultimately show ?thesis
    by (simp add: decideI(2) trail_lits_ground_def decide_lit_def)
qed

lemma conflict_preserves_trail_lits_ground:
  assumes "conflict N β S S'" and "trail_lits_ground S"
  shows "trail_lits_ground S'"
  using assms by (auto simp: trail_lits_ground_def elim!: conflict.cases)

lemma skip_preserves_trail_lits_ground:
  assumes "skip N β S S'" and "trail_lits_ground S"
  shows "trail_lits_ground S'"
  using assms by (auto simp: trail_lits_ground_def elim!: skip.cases)

lemma factorize_preserves_trail_lits_ground:
  assumes "factorize N β S S'" and "trail_lits_ground S"
  shows "trail_lits_ground S'"
  using assms by (auto simp: trail_lits_ground_def elim!: factorize.cases)

lemma resolve_preserves_trail_lits_ground:
  assumes "resolve N β S S'" and "trail_lits_ground S"
  shows "trail_lits_ground S'"
  using assms by (auto simp: trail_lits_ground_def elim!: resolve.cases)

lemma backtrack_preserves_trail_lits_ground:
  assumes "backtrack N β S S'" and "trail_lits_ground S"
  shows "trail_lits_ground S'"
  using assms by (auto simp: trail_lits_ground_def decide_lit_def elim!: backtrack.cases)

lemma scl_preserves_trail_lits_ground:
  assumes "scl N β S S'" and "trail_lits_ground S"
  shows "trail_lits_ground S'"
  using assms unfolding scl_def
  using propagate_preserves_trail_lits_ground decide_preserves_trail_lits_ground
    conflict_preserves_trail_lits_ground skip_preserves_trail_lits_ground
    factorize_preserves_trail_lits_ground resolve_preserves_trail_lits_ground
    backtrack_preserves_trail_lits_ground
  by metis


subsection ‹Trail Literals Are Defined Only Once›

definition trail_lits_consistent where
  "trail_lits_consistent S ⟷ trail_consistent (state_trail S)"

lemma trail_lits_consistent_initial_state[simp]: "trail_lits_consistent initial_state"
  by (simp add: trail_lits_consistent_def)

lemma propagate_preserves_trail_lits_consistent:
  assumes "propagate N β S S'" and invar: "trail_lits_consistent S"
  shows "trail_lits_consistent S'"
  using assms(1)
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)}"
      by (smt (verit, del_insts) finite_imageI finite_set_mset image_iff insert_iff is_unifier_alt
          is_unifiers_def local.propagateI(8) mem_Collect_eq set_mset_add_mset_insert
          set_mset_filter singletonD subst_atm_of_eqI)
    hence "γ = μ ⊙ γ"
      using ‹is_imgu μ {atm_of ` set_mset (add_mset L C⇩1)}›
      by (simp add: is_imgu_def)
    thus ?thesis
      by (metis subst_lit_comp_subst)
  qed
  hence "¬ trail_defined_lit Γ (L ⋅l μ ⋅l γ)"
    using ‹¬ trail_defined_lit Γ (L ⋅l γ)› by metis
  
  moreover from invar have "trail_consistent Γ"
    by (simp add: propagateI(1) trail_lits_consistent_def)

  ultimately show ?thesis
    by (auto simp: propagateI(2) propagate_lit_def trail_lits_consistent_def
        intro: trail_consistent.Cons)
qed

lemma decide_preserves_trail_lits_consistent:
  assumes "decide N β S S'" and invar: "trail_lits_consistent S"
  shows "trail_lits_consistent S'"
  using assms
  by (auto simp: trail_lits_consistent_def decide_lit_def elim!: decide.cases
      intro: trail_consistent.Cons)

lemma conflict_preserves_trail_lits_consistent:
  assumes "conflict N β S S'" and invar: "trail_lits_consistent S"
  shows "trail_lits_consistent S'"
  using assms
  by (auto simp: trail_lits_consistent_def elim: conflict.cases)

lemma skip_preserves_trail_lits_consistent:
  assumes "skip N β S S'" and invar: "trail_lits_consistent S"
  shows "trail_lits_consistent S'"
  using assms
  by (auto simp: trail_lits_consistent_def elim!: skip.cases elim: trail_consistent.cases)

lemma factorize_preserves_trail_lits_consistent:
  assumes "factorize N β S S'" and invar: "trail_lits_consistent S"
  shows "trail_lits_consistent S'"
  using assms
  by (auto simp: trail_lits_consistent_def elim: factorize.cases)

lemma resolve_preserves_trail_lits_consistent:
  assumes "resolve N β S S'" and invar: "trail_lits_consistent S"
  shows "trail_lits_consistent S'"
  using assms
  by (auto simp: trail_lits_consistent_def elim: resolve.cases)

lemma backtrack_preserves_trail_lits_consistent:
  assumes "backtrack N β S S'" and invar: "trail_lits_consistent S"
  shows "trail_lits_consistent S'"
  using assms
  by (auto simp: trail_lits_consistent_def decide_lit_def elim!: backtrack.cases
      elim!: trail_consistent_if_suffix intro: suffixI)

lemma scl_preserves_trail_lits_consistent:
  assumes "scl N β S S'" and "trail_lits_consistent S"
  shows "trail_lits_consistent S'"
  using assms unfolding scl_def
  using propagate_preserves_trail_lits_consistent decide_preserves_trail_lits_consistent
    conflict_preserves_trail_lits_consistent skip_preserves_trail_lits_consistent
    factorize_preserves_trail_lits_consistent resolve_preserves_trail_lits_consistent
    backtrack_preserves_trail_lits_consistent
  by metis

lemma trail_consistent_iff: "trail_consistent Γ ⟷ (∀Γ' Ln Γ''. Γ = Γ'' @ Ln # Γ' ⟶ ¬ trail_defined_lit Γ' (fst Ln))"
proof (intro iffI allI impI)
  fix Γ' Ln Γ''
  assume "trail_consistent Γ" and "Γ = Γ'' @ Ln # Γ'"
  thus "¬ trail_defined_lit Γ' (fst Ln)"
  proof (induction Γ arbitrary: Γ'' rule: trail_consistent.induct)
    case Nil
    thus ?case
      by simp
  next
    case ind_hyps: (Cons Γ L u)
    thus ?case
      by (cases Γ'') auto
  qed
next
  assume "∀Γ' Ln Γ''. Γ = Γ'' @ Ln # Γ' ⟶ ¬ trail_defined_lit Γ' (fst Ln)"
  then show "trail_consistent Γ"
  proof (induction Γ)
    case Nil
    thus ?case
      by simp
  next
    case (Cons Ln Γ)
    thus ?case
      by (cases Ln) (simp add: trail_consistent.Cons)
  qed
qed


subsection ‹Trail Closures Are False In Subtrails›

definition trail_closures_false' where
  "trail_closures_false' S ⟷ trail_closures_false (state_trail S)"

lemma trail_closures_false'_initial_state[simp]: "trail_closures_false' initial_state"
  by (simp add: trail_closures_false'_def)

lemma propagate_preserves_trail_closures_false':
  assumes step: "propagate N β S S'" and invar: "trail_closures_false' S"
  shows "trail_closures_false' S'"
  using step
proof (cases N β S S' rule: propagate.cases)
  case step_hyps: (propagateI C U L C' γ C⇩0 C⇩1 Γ μ)
  have "is_unifier γ (atm_of ` set_mset (add_mset L C⇩1))"
    unfolding step_hyps
    by (auto simp add: is_unifier_alt intro: subst_atm_of_eqI)
  hence "μ ⊙ γ = γ"
    using ‹is_imgu μ {atm_of ` set_mset (add_mset L C⇩1)}›
    by (simp add: is_imgu_def is_unifiers_def)
  hence "trail_false_cls Γ (C⇩0 ⋅ μ ⋅ γ)"
    using ‹trail_false_cls Γ (C⇩0 ⋅ γ)›
    by (metis subst_cls_comp_subst)
  with invar show ?thesis
    unfolding step_hyps(1,2)
    by (simp add: trail_closures_false'_def propagate_lit_def trail_closures_false.Cons)
qed

lemma decide_preserves_trail_closures_false':
  assumes step: "decide N β S S'" and invar: "trail_closures_false' S"
  shows "trail_closures_false' S'"
  using step
proof (cases N β S S' rule: decide.cases)
  case step_hyps: (decideI L γ Γ U)
  with invar show ?thesis
    by (simp add: trail_closures_false'_def decide_lit_def propagate_lit_def
        trail_closures_false.Cons)
qed

lemma conflict_preserves_trail_closures_false':
  assumes step: "conflict N β S S'" and invar: "trail_closures_false' S"
  shows "trail_closures_false' S'"
  using step
proof (cases N β S S' rule: conflict.cases)
  case (conflictI D U γ Γ)
  with invar show ?thesis
    by (simp add: trail_closures_false'_def)
qed

lemma skip_preserves_trail_closures_false':
  assumes step: "skip N β S S'" and invar: "trail_closures_false' S"
  shows "trail_closures_false' S'"
  using step
proof (cases N β S S' rule: skip.cases)
  case (skipI L D σ n Γ U)
  with invar show ?thesis
    by (simp add: trail_closures_false'_def trail_closures_false_ConsD)
qed

lemma factorize_preserves_trail_closures_false':
  assumes step: "factorize N β S S'" and invar: "trail_closures_false' S"
  shows "trail_closures_false' S'"
  using step
proof (cases N β S S' rule: factorize.cases)
  case (factorizeI L γ L' μ Γ U D)
  with invar show ?thesis
    by (simp add: trail_closures_false'_def)
qed

lemma resolve_preserves_trail_closures_false':
  assumes step: "resolve N β S S'" and invar: "trail_closures_false' S"
  shows "trail_closures_false' S'"
  using step
proof (cases N β S S' rule: resolve.cases)
  case (resolveI Γ Γ' K D γ⇩D L γ⇩C ρ⇩C ρ⇩D C μ γ U)
  with invar show ?thesis
    by (simp add: trail_closures_false'_def)
qed

lemma backtrack_preserves_trail_closures_false':
  assumes step: "backtrack N β S S'" and invar: "trail_closures_false' S"
  shows "trail_closures_false' S'"
  using step
proof (cases N β S S' rule: backtrack.cases)
  case (backtrackI Γ Γ' Γ'' K L σ D U)
  with invar show ?thesis
    by (auto simp add: trail_closures_false'_def
        intro: trail_closures_false_ConsD trail_closures_false_appendD)
qed

lemma scl_preserves_trail_closures_false':
  assumes "scl N β S S'" and "trail_closures_false' S"
  shows "trail_closures_false' S'"
  using assms unfolding scl_def
  using propagate_preserves_trail_closures_false' decide_preserves_trail_closures_false'
    conflict_preserves_trail_closures_false' skip_preserves_trail_closures_false'
    factorize_preserves_trail_closures_false' resolve_preserves_trail_closures_false'
    backtrack_preserves_trail_closures_false'
  by metis

lemma "trail_closures_false Γ ⟷
  (∀K D γ Γ' Γ''. Γ = Γ'' @ propagate_lit K D γ # Γ' ⟶ trail_false_cls Γ' (D ⋅ γ))"
proof (intro iffI allI impI)
  fix K D γ Γ' Γ''
  assume "trail_closures_false Γ" and "Γ = Γ'' @ trail_propagate Γ' K D γ"
  thus "trail_false_cls Γ' (D ⋅ γ)"
  proof (induction Γ arbitrary: Γ'' Γ' K D γ rule: trail_closures_false.induct)
    case Nil
    thus ?case by simp
  next
    case (Cons u Γ L)
    thus ?case
      by (metis (no_types, opaque_lifting) Cons_eq_append_conv list.inject)
  qed
next
  assume "∀K D γ Γ' Γ''. Γ = Γ'' @ trail_propagate Γ' K D γ ⟶ trail_false_cls Γ' (D ⋅ γ)"
  thus "trail_closures_false Γ"
    by (induction Γ) (simp_all add: trail_closures_false.Cons)
qed


subsection ‹Trail Literals Were Propagated or Decided›

inductive trail_propagated_or_decided for N β U where
  Nil[simp]: "trail_propagated_or_decided N β U []" |
  Propagate: "
    C |∈| N |∪| U ⟹
    C = add_mset L C' ⟹
    is_ground_cls (C ⋅ γ) ⟹
    ∀K∈#C ⋅ γ. atm_of K ≼⇩B β ⟹
    C⇩0 = {#K ∈# C'. K ⋅l γ ≠ L ⋅l γ#} ⟹
    C⇩1 = {#K ∈# C'. K ⋅l γ = L ⋅l γ#} ⟹
    trail_false_cls Γ (C⇩0 ⋅ γ) ⟹
    ¬ trail_defined_lit Γ (L ⋅l γ) ⟹
    is_imgu μ {atm_of ` set_mset (add_mset L C⇩1)} ⟹
    trail_propagated_or_decided N β U Γ ⟹
    trail_propagated_or_decided N β U (trail_propagate Γ (L ⋅l μ) (C⇩0 ⋅ μ) γ)" |
  Decide: "
    L ∈ ⋃ (set_mset ` fset N) ⟹
    is_ground_lit (L ⋅l γ) ⟹
    ¬ trail_defined_lit Γ (L ⋅l γ) ⟹
    atm_of L ⋅a γ ≼⇩B β ⟹
    trail_propagated_or_decided N β U Γ ⟹
    trail_propagated_or_decided N β U (trail_decide Γ (L ⋅l γ))"

lemma trail_propagate_or_decide_suffixI:
  assumes "trail_propagated_or_decided N β U ys" and "suffix xs ys"
  shows "trail_propagated_or_decided N β U xs"
  using assms
proof (induction ys arbitrary: xs rule: trail_propagated_or_decided.induct)
  case Nil
  hence "xs = []"
    by simp
  thus ?case
    by simp
next
  case (Propagate C L C' γ C⇩0 C⇩1 Γ μ)
  from Propagate.prems obtain zs where
    tr_prop_eq: "trail_propagate Γ (L ⋅l μ) (C⇩0 ⋅ μ) γ = zs @ xs"
    by (auto simp: suffix_def)
  show ?case
  proof (cases zs)
    case Nil
    with tr_prop_eq have "xs = trail_propagate Γ (L ⋅l μ) (C⇩0 ⋅ μ) γ"
      by simp
    then show ?thesis
      by (simp add: trail_propagated_or_decided.Propagate[OF Propagate.hyps])
  next
    case (Cons Ln Γ')
    with tr_prop_eq have "suffix xs Γ"
      by (simp add: suffix_def propagate_lit_def)
    thus ?thesis
      by (rule Propagate.IH)
  qed
next
  case (Decide L γ Γ)
  from Decide.prems obtain zs where
    tr_deci_eq: "trail_decide Γ (L ⋅l γ) = zs @ xs"
    by (auto simp: suffix_def)
  show ?case
  proof (cases zs)
    case Nil
    with tr_deci_eq have "xs = trail_decide Γ (L ⋅l γ)"
      by simp
    then show ?thesis
      by (simp add: trail_propagated_or_decided.Decide[OF Decide.hyps])
  next
    case (Cons Ln Γ')
    with tr_deci_eq have "suffix xs Γ"
      by (simp add: suffix_def decide_lit_def)
    thus ?thesis
      by (rule Decide.IH)
  qed
qed

definition trail_propagated_or_decided' where
  "trail_propagated_or_decided' N β S =
    trail_propagated_or_decided N β (state_learned S) (state_trail S)"

lemma trail_propagated_or_decided_learned_finsert:
  assumes "trail_propagated_or_decided N β U Γ"
  shows "trail_propagated_or_decided N β (finsert C U) Γ"
  using assms
proof (induction Γ rule: trail_propagated_or_decided.induct)
  case Nil
  show ?case by (simp add: trail_propagated_or_decided.Nil)
next
  case (Propagate D L D' γ D⇩0 D⇩1 Γ μ)
  
  from Propagate.hyps have D_in: "D |∈| N |∪| finsert C U"
    by simp

  have IH: "trail_propagated_or_decided N β (finsert C U) Γ"
    by (rule Propagate.IH)

  show ?case
    using trail_propagated_or_decided.Propagate[OF D_in Propagate.hyps(2,3,4,5,6,7,8,9) IH] .
next
  case (Decide L γ Γ)
  then show ?case
    by (simp add: trail_propagated_or_decided.Decide)
qed

lemma trail_propagated_or_decided_trail_append:
  assumes "trail_propagated_or_decided N β U (Γ⇩1 @ Γ⇩2)"
  shows "trail_propagated_or_decided N β U Γ⇩2"
  using assms
proof (induction "Γ⇩1 @ Γ⇩2" arbitrary: Γ⇩1 Γ⇩2 rule: trail_propagated_or_decided.induct)
  case Nil
  thus ?case
    by simp
next
  case (Propagate C L C' γ C⇩0 C⇩1 Γ μ)
  hence tr_prop_eq_Γ⇩1_Γ⇩2:
    "Γ⇩1 @ Γ⇩2 = trail_propagate Γ (L ⋅l μ) (C⇩0 ⋅ μ) γ"
    by simp
  thus ?case
    unfolding propagate_lit_def append_eq_Cons_conv
  proof (elim disjE conjE exE)
    assume "Γ⇩1 = []" and Γ⇩2_def: "Γ⇩2 = (L ⋅l μ ⋅l γ, Some (C⇩0 ⋅ μ, L ⋅l μ, γ)) # Γ"
    show ?thesis
      unfolding Γ⇩2_def
      by (rule trail_propagated_or_decided.Propagate[unfolded propagate_lit_def];
          rule Propagate.hyps)
  next
    fix Γ⇩1'
    assume "Γ⇩1 = (L ⋅l μ ⋅l γ, Some (C⇩0 ⋅ μ, L ⋅l μ, γ)) # Γ⇩1'" and "Γ⇩1' @ Γ⇩2 = Γ"
    thus ?thesis
      using Propagate.hyps by blast
  qed
next
  case (Decide L γ Γ)
  hence "Γ⇩1 @ Γ⇩2 = trail_decide Γ (L ⋅l γ)"
    by simp
  thus ?case
    unfolding decide_lit_def append_eq_Cons_conv
  proof (elim disjE conjE exE)
    assume "Γ⇩1 = []" and Γ⇩2_def: "Γ⇩2 = (L ⋅l γ, None) # Γ"
    show ?thesis
      unfolding Γ⇩2_def
      by (rule trail_propagated_or_decided.Decide[unfolded decide_lit_def]; rule Decide.hyps)
  next
    fix Γ⇩1' assume "Γ⇩1 = (L ⋅l γ, None) # Γ⇩1'" and "Γ⇩1' @ Γ⇩2 = Γ"
    then show ?thesis
      using Decide.hyps by blast
  qed
qed

lemma trail_propagated_or_decided_initial_state[simp]:
  "trail_propagated_or_decided' N β initial_state"
  by (auto simp: trail_propagated_or_decided'_def intro: trail_propagated_or_decided.Nil)

lemma propagate_preserves_trail_propagated_or_decided:
  assumes "propagate N β S S'" and "trail_propagated_or_decided' N β S"
  shows "trail_propagated_or_decided' N β S'"
  using assms(1)
proof (cases N β S S' rule: propagate.cases)
  case (propagateI C U L C' γ C⇩0 C⇩1 Γ μ)

  from propagateI(1) assms(2) have IH: "trail_propagated_or_decided N β U Γ"
    by (simp add: trail_propagated_or_decided'_def)

  show ?thesis
    unfolding propagateI(2)
    apply (simp add: trail_propagated_or_decided'_def)
    by (rule trail_propagated_or_decided.Propagate[rotated -1, OF IH])
      (rule propagateI)+
qed

lemma decide_preserves_trail_propagated_or_decided:
  assumes "decide N β S S'" and "trail_propagated_or_decided' N β S"
  shows "trail_propagated_or_decided' N β S'"
  using assms(1)
proof (cases N β S S' rule: decide.cases)
  case (decideI L γ Γ U)

  from decideI(1) assms(2) have IH: "trail_propagated_or_decided N β U Γ"
    by (simp add: trail_propagated_or_decided'_def)
  show ?thesis
    unfolding decideI(2)
    apply (simp add: trail_propagated_or_decided'_def)
    by (rule trail_propagated_or_decided.Decide[rotated -1, OF IH])
      (rule decideI)+
qed

lemma conflict_preserves_trail_propagated_or_decided:
  assumes "conflict N β S S'" and invar: "trail_propagated_or_decided' N β S"
  shows "trail_propagated_or_decided' N β S'"
  using assms by (auto simp: trail_propagated_or_decided'_def elim: conflict.cases)

lemma skip_preserves_trail_propagated_or_decided:
  assumes "skip N β S S'" and invar: "trail_propagated_or_decided' N β S"
  shows "trail_propagated_or_decided' N β S'"
  using assms(1)
proof (cases N β S S' rule: skip.cases)
  case (skipI L D σ n Γ U)

  from invar have "trail_propagated_or_decided N β U ((L, n) # Γ)"
    unfolding skipI(1) by (simp add: trail_propagated_or_decided'_def)
  hence "trail_propagated_or_decided N β U Γ"
    by (cases N β U "(L, n) # Γ" rule: trail_propagated_or_decided.cases)
      (simp_all add: propagate_lit_def decide_lit_def)
  thus ?thesis
    unfolding skipI(2) by (simp add: trail_propagated_or_decided'_def)
qed

lemma factorize_preserves_trail_propagated_or_decided:
  assumes "factorize N β S S'" and invar: "trail_propagated_or_decided' N β S"
  shows "trail_propagated_or_decided' N β S'"
  using assms by (auto simp: trail_propagated_or_decided'_def elim: factorize.cases)

lemma resolve_preserves_trail_propagated_or_decided:
  assumes "resolve N β S S'" and invar: "trail_propagated_or_decided' N β S"
  shows "trail_propagated_or_decided' N β S'"
  using assms by (auto simp: trail_propagated_or_decided'_def elim: resolve.cases) 

lemma backtrack_preserves_trail_propagated_or_decided:
  assumes "backtrack N β S S'" and invar: "trail_propagated_or_decided' N β S"
  shows "trail_propagated_or_decided' N β S'"
  using assms(1)
proof (cases N β S S' rule: backtrack.cases)
  case (backtrackI Γ Γ' Γ'' K L σ D U)

  have "trail_propagated_or_decided N β (finsert (add_mset L D) U) Γ''"
  proof (rule trail_propagated_or_decided_learned_finsert)
    from invar have "trail_propagated_or_decided N β U (trail_decide (Γ' @ Γ'') (- (L ⋅l σ)))"
      unfolding backtrackI by (simp add: trail_propagated_or_decided'_def)
    then show "trail_propagated_or_decided N β U Γ''"
      by (induction "(trail_decide (Γ' @ Γ'') (- (L ⋅l σ)))"
          rule: trail_propagated_or_decided.induct)
        (simp_all add: decide_lit_def propagate_lit_def
          trail_propagated_or_decided_trail_append)
  qed
  thus ?thesis
    unfolding backtrackI by (simp add: trail_propagated_or_decided'_def)
qed

lemma scl_preserves_trail_propagated_or_decided:
  assumes "scl N β S S'" and "trail_propagated_or_decided' N β S"
  shows "trail_propagated_or_decided' N β S'"
  using assms unfolding scl_def
  using propagate_preserves_trail_propagated_or_decided decide_preserves_trail_propagated_or_decided
    conflict_preserves_trail_propagated_or_decided skip_preserves_trail_propagated_or_decided
    factorize_preserves_trail_propagated_or_decided resolve_preserves_trail_propagated_or_decided
    backtrack_preserves_trail_propagated_or_decided
  by metis

definition trail_propagated_wf where
  "trail_propagated_wf Γ ⟷ (∀(L⇩γ, n) ∈ set Γ.
    case n of
      None ⇒ True
    | Some (_, L, γ) ⇒ L⇩γ = L ⋅l γ)"

lemma trail_propagated_wf_iff:
  "trail_propagated_wf Γ ⟷ (∀Ln ∈ set Γ. ∀D K γ. snd Ln = Some (D, K, γ) ⟶ fst Ln = K ⋅l γ)"
  (is "?lhs ⟷ ?rhs")
proof (rule iffI)
  show "?lhs ⟹ ?rhs"
    unfolding trail_propagated_wf_def
    by fastforce
next
  assume ?rhs
  show ?lhs
    unfolding trail_propagated_wf_def
  proof (rule ballI)
    fix 𝒦 assume "𝒦 ∈ set Γ"
    show "case 𝒦 of (L⇩γ, None) ⇒ True | (L⇩γ, Some (x, L, γ)) ⇒ L⇩γ = L ⋅l γ"
      unfolding case_prod_beta
      using ‹?rhs›[rule_format, OF ‹𝒦 ∈ set Γ›]
      by (cases "snd 𝒦") auto
  qed
qed

lemma trail_propagated_wf_if_trail_propagated_or_decided:
  "trail_propagated_or_decided N U β Γ ⟹ trail_propagated_wf Γ"
proof (induction Γ rule: trail_propagated_or_decided.induct)
  case Nil
  then show ?case
    by (simp add: trail_propagated_wf_def)
next
  case (Propagate C L C' γ C⇩0 C⇩1 Γ μ)
  then show ?case
    by (simp add: trail_propagated_wf_def propagate_lit_def)
next
  case (Decide L γ Γ)
  then show ?case
    by (simp add: trail_propagated_wf_def decide_lit_def)
qed

lemma trail_propagated_wf_if_trail_propagated_or_decided':
  "trail_propagated_or_decided' N β S ⟹ trail_propagated_wf (state_trail S)"
  unfolding trail_propagated_or_decided'_def
  using trail_propagated_wf_if_trail_propagated_or_decided .

lemma trail_propagated_lit_wf_initial_state:
  "∀𝒦∈set (state_trail initial_state). ∀D K γ. snd 𝒦 = Some (D, K, γ) ⟶ fst 𝒦 = K ⋅l γ"
  by simp

lemma scl_preserves_trail_propagated_lit_wf:
  assumes step: "scl N β S S'" and
    inv: "∀𝒦 ∈ set (state_trail S). ∀D K γ. snd 𝒦 = Some (D, K, γ) ⟶ fst 𝒦 = K ⋅l γ"
  shows "∀𝒦 ∈ set (state_trail S'). ∀D K γ. snd 𝒦 = Some (D, K, γ) ⟶ fst 𝒦 = K ⋅l γ"
  using step inv
  unfolding scl_def
proof (elim disjE)
  assume "propagate N β S S'"
  thus "∀𝒦∈set (state_trail S'). ∀D K γ. snd 𝒦 = Some (D, K, γ) ⟶ fst 𝒦 = K ⋅l γ"
    using inv
    by (smt (verit) fst_conv insert_iff list.simps(15) option.inject propagate.cases
        propagate_lit_def snd_conv state_trail_simp)
next
  assume "decide N β S S'"
  thus "∀𝒦∈set (state_trail S'). ∀D K γ. snd 𝒦 = Some (D, K, γ) ⟶ fst 𝒦 = K ⋅l γ"
    using inv
    by (smt (verit) Pair_inject decide.simps decide_lit_def option.discI set_ConsD sndI state_simp)
next
  assume "conflict N β S S'"
  thus "∀𝒦∈set (state_trail S'). ∀D K γ. snd 𝒦 = Some (D, K, γ) ⟶ fst 𝒦 = K ⋅l γ"
    using inv conflict.simps by fastforce
next
  assume "skip N β S S'"
  thus "∀𝒦∈set (state_trail S'). ∀D K γ. snd 𝒦 = Some (D, K, γ) ⟶ fst 𝒦 = K ⋅l γ"
    using inv skip.simps by fastforce
next
  assume "factorize N β S S'"
  thus "∀𝒦∈set (state_trail S'). ∀D K γ. snd 𝒦 = Some (D, K, γ) ⟶ fst 𝒦 = K ⋅l γ"
    using inv factorize.simps by fastforce
next
  assume "resolve N β S S'"
  thus "∀𝒦∈set (state_trail S'). ∀D K γ. snd 𝒦 = Some (D, K, γ) ⟶ fst 𝒦 = K ⋅l γ"
    using inv
    by (smt (verit) resolve.cases state_trail_simp)
next
  assume "backtrack N β S S'"
  thus "∀𝒦∈set (state_trail S'). ∀D K γ. snd 𝒦 = Some (D, K, γ) ⟶ fst 𝒦 = K ⋅l γ"
    using inv
    by (smt (verit, del_insts) Un_iff fst_conv insertCI list.simps(15) backtrack.cases set_append state_trail_def)
qed


subsection ‹Trail Atoms Are Less Than Bound›

definition trail_atoms_lt where
  "trail_atoms_lt β S ⟷ (∀A ∈ atm_of ` fst ` set (state_trail S). A ≼⇩B β)"

lemma trail_atoms_lt_initial_state[simp]: "trail_atoms_lt β initial_state"
  by (simp add: trail_atoms_lt_def)

lemma propagate_preserves_trail_atoms_lt:
  assumes "propagate N β S S'" and "trail_atoms_lt β S"
  shows "trail_atoms_lt β S'"
  using assms(1)
proof (cases N β S S' rule: propagate.cases)
  case (propagateI C U L C' γ C⇩0 C⇩1 Γ μ)
  hence "is_ground_lit (L ⋅l γ)"
    by (meson Melem_subst_cls is_ground_cls_def mset_subset_eqD mset_subset_eq_add_right
        union_single_eq_member)

  moreover have "∀τ. is_unifiers τ {atm_of ` set_mset (add_mset L C⇩1)} ⟶ τ = μ ⊙ τ"
    using ‹is_imgu μ {atm_of ` set_mset (add_mset L C⇩1)}›
    by (simp add: is_imgu_def)

  moreover have "is_unifiers γ {atm_of ` set_mset (add_mset L C⇩1)}"
    by (auto simp: is_unifiers_def is_unifier_alt ‹C⇩1 = {#K ∈# C'. K ⋅l γ = L ⋅l γ#}›
        intro: subst_atm_of_eqI)

  ultimately have "is_ground_lit (L ⋅l μ ⋅l γ)"
    by (metis subst_lit_comp_subst)

  have "atm_of L ⋅a μ ⋅a γ = atm_of L ⋅a γ"
  proof -
    from propagateI have "is_unifiers γ {atm_of ` set_mset (add_mset L C⇩1)}"
      by (auto simp: is_unifiers_def is_unifier_alt intro: subst_atm_of_eqI)
    with propagateI have "γ = μ ⊙ γ"
      by (simp add: is_imgu_def)
    thus ?thesis
      by (metis subst_atm_comp_subst)
  qed

  moreover from propagateI have "atm_of L ⋅a γ ≼⇩B β"
    by (metis add_mset_add_single atm_of_subst_lit subst_cls_single subst_cls_union
        union_single_eq_member)

  ultimately have "atm_of L ⋅a μ ⋅a γ ≼⇩B β"
    by simp
  with ‹trail_atoms_lt β S› show ?thesis
    by (simp add: trail_atoms_lt_def propagateI(1,2) propagate_lit_def)
qed

lemma decide_preserves_trail_atoms_lt:
  assumes "decide N β S S'" and "trail_atoms_lt β S"
  shows "trail_atoms_lt β S'"
  using assms by (auto simp: trail_atoms_lt_def decide_lit_def elim!: decide.cases)

lemma conflict_preserves_trail_atoms_lt:
  assumes "conflict N β S S'" and "trail_atoms_lt β S"
  shows "trail_atoms_lt β S'"
  using assms by (auto simp: trail_atoms_lt_def elim!: conflict.cases)

lemma skip_preserves_trail_atoms_lt:
  assumes "skip N β S S'" and "trail_atoms_lt β S"
  shows "trail_atoms_lt β S'"
  using assms by (auto simp: trail_atoms_lt_def elim!: skip.cases)

lemma factorize_preserves_trail_atoms_lt:
  assumes "factorize N β S S'" and "trail_atoms_lt β S"
  shows "trail_atoms_lt β S'"
  using assms by (auto simp: trail_atoms_lt_def elim!: factorize.cases)

lemma resolve_preserves_trail_atoms_lt:
  assumes "resolve N β S S'" and "trail_atoms_lt β S"
  shows "trail_atoms_lt β S'"
  using assms by (auto simp: trail_atoms_lt_def elim!: resolve.cases)

lemma backtrack_preserves_trail_atoms_lt:
  assumes "backtrack N β S S'" and "trail_atoms_lt β S"
  shows "trail_atoms_lt β S'"
  using assms by (auto simp: trail_atoms_lt_def decide_lit_def elim!: backtrack.cases)

lemma scl_preserves_trail_atoms_lt:
  assumes "scl N β S S'" and "trail_atoms_lt β S"
  shows "trail_atoms_lt β S'"
  using assms unfolding scl_def
  using propagate_preserves_trail_atoms_lt decide_preserves_trail_atoms_lt
    conflict_preserves_trail_atoms_lt skip_preserves_trail_atoms_lt
    factorize_preserves_trail_atoms_lt resolve_preserves_trail_atoms_lt
    backtrack_preserves_trail_atoms_lt
  by metis


subsection ‹Trail Resolved Literals Have Unique Polarity›

definition trail_resolved_lits_pol where
  "trail_resolved_lits_pol S ⟷
  (∀Ln ∈ set (state_trail S). ∀C L γ. snd Ln = Some (C, L, γ) ⟶ -(L ⋅l γ) ∉# C ⋅ γ)"

lemma trail_resolved_lits_pol_initial_state[simp]: "trail_resolved_lits_pol initial_state"
  by (simp add: trail_resolved_lits_pol_def)

lemma propagate_preserves_trail_resolved_lits_pol:
  assumes step: "propagate N β S S'" and invar: "trail_resolved_lits_pol S"
  shows "trail_resolved_lits_pol S'"
  using step
proof (cases N β S S' rule: propagate.cases)
  case (propagateI C U L C' γ C⇩0 C⇩1 Γ μ)
  have "is_unifiers γ {atm_of ` set_mset (add_mset L C⇩1)}"
    unfolding ‹C⇩1 = {#K ∈# C'. K ⋅l γ = L ⋅l γ#}›
    by (auto simp add: is_unifiers_def is_unifier_alt intro: subst_atm_of_eqI)
  hence "μ ⊙ γ = γ"
    using ‹is_imgu μ {atm_of ` set_mset (add_mset L C⇩1)}›
    by (simp add: is_imgu_def)
  hence "L ⋅l μ ⋅l γ = L ⋅l γ" and "C⇩0 ⋅ μ ⋅ γ = C⇩0 ⋅ γ"
    by (simp_all del: subst_lit_comp_subst subst_cls_comp_subst
        add: subst_lit_comp_subst[symmetric] subst_cls_comp_subst[symmetric])
  hence "- (L ⋅l μ ⋅l γ) ∉# C⇩0 ⋅ μ ⋅ γ"
    using ‹C⇩0 = {#K ∈# C'. K ⋅l γ ≠ L ⋅l γ#}› ‹¬ trail_defined_lit Γ (L ⋅l γ)›
      ‹trail_false_cls Γ (C⇩0 ⋅ γ)›
    by (metis trail_defined_lit_iff_defined_uminus trail_defined_lit_iff_true_or_false
        trail_false_cls_def)

  moreover from invar have "∀Ln ∈ set Γ. ∀C L γ. snd Ln = Some (C, L, γ) ⟶ - (L ⋅l γ) ∉# C ⋅ γ"
    unfolding propagateI(1,2) trail_resolved_lits_pol_def
    by simp
  
  ultimately show ?thesis
    unfolding propagateI(1,2)
    unfolding trail_resolved_lits_pol_def propagate_lit_def state_proj_simp list.set
    by fastforce
qed

lemma decide_preserves_trail_resolved_lits_pol:
  assumes step: "decide N β S S'" and invar: "trail_resolved_lits_pol S"
  shows "trail_resolved_lits_pol S'"
  using assms
  by (auto simp: trail_resolved_lits_pol_def decide_lit_def elim: decide.cases)

lemma conflict_preserves_trail_resolved_lits_pol:
  assumes step: "conflict N β S S'" and invar: "trail_resolved_lits_pol S"
  shows "trail_resolved_lits_pol S'"
  using assms
  by (auto simp: trail_resolved_lits_pol_def elim: conflict.cases)

lemma skip_preserves_trail_resolved_lits_pol:
  assumes step: "skip N β S S'" and invar: "trail_resolved_lits_pol S"
  shows "trail_resolved_lits_pol S'"
  using assms
  by (auto simp: trail_resolved_lits_pol_def elim: skip.cases)

lemma factorize_preserves_trail_resolved_lits_pol:
  assumes step: "factorize N β S S'" and invar: "trail_resolved_lits_pol S"
  shows "trail_resolved_lits_pol S'"
  using assms
  by (auto simp: trail_resolved_lits_pol_def elim: factorize.cases)

lemma resolve_preserves_trail_resolved_lits_pol:
  assumes step: "resolve N β S S'" and invar: "trail_resolved_lits_pol S"
  shows "trail_resolved_lits_pol S'"
  using assms
  by (auto simp: trail_resolved_lits_pol_def propagate_lit_def elim!: resolve.cases)

lemma backtrack_preserves_trail_resolved_lits_pol:
  assumes step: "backtrack N β S S'" and invar: "trail_resolved_lits_pol S"
  shows "trail_resolved_lits_pol S'"
  using assms
  by (auto simp: trail_resolved_lits_pol_def decide_lit_def ball_Un elim: backtrack.cases)

lemma scl_preserves_trail_resolved_lits_pol:
  assumes "scl N β S S'" and "trail_resolved_lits_pol S"
  shows "trail_resolved_lits_pol S'"
  using assms unfolding scl_def
  using propagate_preserves_trail_resolved_lits_pol decide_preserves_trail_resolved_lits_pol
    conflict_preserves_trail_resolved_lits_pol skip_preserves_trail_resolved_lits_pol
    factorize_preserves_trail_resolved_lits_pol resolve_preserves_trail_resolved_lits_pol
    backtrack_preserves_trail_resolved_lits_pol
  by metis


subsection ‹Trail And Conflict Closures Are Ground›

definition ground_closures where
  "ground_closures S ⟷
    (∀Ln ∈ set (state_trail S). ∀C L γ. snd Ln = Some (C, L, γ) ⟶ is_ground_cls (add_mset L C ⋅ γ)) ∧
    (∀C γ. state_conflict S = Some (C, γ) ⟶ is_ground_cls (C ⋅ γ))"

lemma ground_closures_initial_state[simp]: "ground_closures initial_state"
  by (simp add: ground_closures_def)

lemma propagate_preserves_ground_closures:
  assumes step: "propagate N β S S'" and invar: "ground_closures S"
  shows "ground_closures S'"
  using step
proof (cases N β S S' rule: propagate.cases)
  case (propagateI C U L C' γ C⇩0 C⇩1 Γ μ)

  have C_def: "C = add_mset L (C⇩0 + C⇩1)"
    using propagateI(3-) by auto

  have "is_unifiers γ {atm_of ` set_mset (add_mset L C⇩1)}"
    unfolding ‹C⇩1 = {#K ∈# C'. K ⋅l γ = L ⋅l γ#}›
    by (auto simp add: is_unifiers_def is_unifier_alt intro: subst_atm_of_eqI)
  hence "μ ⊙ γ = γ"
    using ‹is_imgu μ {atm_of ` set_mset (add_mset L C⇩1)}›
    by (simp add: is_imgu_def)
  hence "L ⋅l μ ⋅l γ = L ⋅l γ" and "C⇩0 ⋅ μ ⋅ γ = C⇩0 ⋅ γ"
    by (simp_all del: subst_lit_comp_subst subst_cls_comp_subst
        add: subst_lit_comp_subst[symmetric] subst_cls_comp_subst[symmetric])
  hence "is_ground_cls (add_mset L C⇩0 ⋅ μ ⋅ γ)"
    using ‹is_ground_cls (C ⋅ γ)›
    by (simp add: C_def)
  thus ?thesis
    using invar
    unfolding propagateI(1,2)
    by (simp add: ground_closures_def propagate_lit_def)
qed

lemma decide_preserves_ground_closures:
  assumes step: "decide N β S S'" and invar: "ground_closures S"
  shows "ground_closures S'"
  using assms
  by (cases N β S S' rule: decide.cases) (simp add: ground_closures_def decide_lit_def)

lemma conflict_preserves_ground_closures:
  assumes step: "conflict N β S S'" and invar: "ground_closures S"
  shows "ground_closures S'"
  using step
proof (cases N β S S' rule: conflict.cases)
  case (conflictI D U γ Γ)
  thus ?thesis
    using invar
    unfolding conflictI(1,2)
    by (simp add: ground_closures_def)
qed

lemma skip_preserves_ground_closures:
  assumes step: "skip N β S S'" and invar: "ground_closures S"
  shows "ground_closures S'"
  using assms
  by (cases N β S S' rule: skip.cases) (simp add: ground_closures_def)

lemma factorize_preserves_ground_closures:
  assumes step: "factorize N β S S'" and invar: "ground_closures S"
  shows "ground_closures S'"
  using step
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 "is_ground_cls (add_mset L D ⋅ μ ⋅ γ)"
    using factorizeI(3-) invar
    unfolding factorizeI(1,2)
    by (simp add: ground_closures_def)
  thus ?thesis
    using invar
    unfolding factorizeI(1,2)
    by (simp add: ground_closures_def)
qed

lemma merge_of_renamed_groundings:
  assumes
    ren_ρ⇩C: "is_renaming ρ⇩C" and
    ren_ρ⇩D: "is_renaming ρ⇩D" and
    disjoint_vars: "vars_cls (C ⋅ ρ⇩C) ∩ vars_cls (D ⋅ ρ⇩D) = {}" and
    ground_conf: "is_ground_cls (C ⋅ γ⇩C)" and
    ground_prop: "is_ground_cls (D ⋅ γ⇩D)" and
    merge_γ: "is_grounding_merge γ
      (vars_cls (C ⋅ ρ⇩C)) (rename_subst_domain ρ⇩C γ⇩C)
      (vars_cls (D ⋅ ρ⇩D)) (rename_subst_domain ρ⇩D γ⇩D)"
  shows
    "∀L ∈# C. L ⋅l ρ⇩C ⋅l γ = L ⋅l γ⇩C"
    "∀K ∈# D. K ⋅l ρ⇩D ⋅l γ = K ⋅l γ⇩D"
proof -
  have "∀x∈vars_cls (C ⋅ ρ⇩C). vars_term (rename_subst_domain ρ⇩C γ⇩C x) = {}"
    using ground_conf ren_ρ⇩C
    by (metis is_ground_atm_iff_vars_empty is_ground_cls_is_ground_on_var
        subst_renaming_subst_adapted vars_cls_subset_subst_domain_if_grounding)

  moreover have "∀x∈vars_cls (D ⋅ ρ⇩D). vars_term (rename_subst_domain ρ⇩D γ⇩D x) = {}"
    using ground_prop ren_ρ⇩D
    by (metis is_ground_atm_iff_vars_empty is_ground_cls_is_ground_on_var
        subst_renaming_subst_adapted vars_cls_subset_subst_domain_if_grounding)

  ultimately have
    ball_C_ρ⇩C_apply_γ: "∀x∈vars_cls (C ⋅ ρ⇩C). γ x = rename_subst_domain ρ⇩C γ⇩C x" and
    ball_D_ρ⇩D_apply_γ: "∀x∈vars_cls (D ⋅ ρ⇩D). γ x = rename_subst_domain ρ⇩D γ⇩D x"
    using disjoint_vars merge_γ
    unfolding is_grounding_merge_def
    by simp_all

  show "∀L ∈# C. L ⋅l ρ⇩C ⋅l γ = L ⋅l γ⇩C"
  proof (rule ballI)
    fix L assume L_in: "L ∈# C"
    show "L ⋅l ρ⇩C ⋅l γ = L ⋅l γ⇩C"
      unfolding subst_lit_comp_subst[symmetric]
    proof (intro same_on_vars_lit ballI)
      fix x assume "x ∈ vars_lit L"
      moreover obtain x' where "ρ⇩C x = Var x'"
        using ren_ρ⇩C
        by (meson is_Var_def is_renaming_iff)
      ultimately have "x' ∈ vars_lit (L ⋅l ρ⇩C)"
        using vars_subst_lit_eq by fastforce
      hence "γ x' = rename_subst_domain ρ⇩C γ⇩C x'"
        using ball_C_ρ⇩C_apply_γ L_in multi_member_split by force
      thus "(ρ⇩C ⊙ γ) x = γ⇩C x"
        apply (simp add: subst_compose_def ‹ρ⇩C x = Var x'›)
        by (metis (no_types, opaque_lifting) L_in Un_iff ‹ρ⇩C x = Var x'› ‹x ∈ vars_lit L›
            ground_conf image_eqI insert_DiffM is_renaming_iff ren_ρ⇩C rename_subst_domain_def
            subsetD the_inv_f_f vars_cls_add_mset vars_cls_subset_subst_domain_if_grounding)
    qed
  qed

  show "∀K ∈# D. K ⋅l ρ⇩D ⋅l γ = K ⋅l γ⇩D"
  proof (rule ballI)
    fix K assume K_in: "K ∈# D"
    show "K ⋅l ρ⇩D ⋅l γ = K ⋅l γ⇩D"
      unfolding subst_lit_comp_subst[symmetric]
    proof (intro same_on_vars_lit ballI)
      fix x assume "x ∈ vars_lit K"
      moreover obtain x' where "ρ⇩D x = Var x'"
        using ren_ρ⇩D
        by (meson is_Var_def is_renaming_iff)
      ultimately have "x' ∈ vars_lit (K ⋅l ρ⇩D)"
        using vars_subst_lit_eq by fastforce
      hence "γ x' = rename_subst_domain ρ⇩D γ⇩D x'"
        using ball_D_ρ⇩D_apply_γ K_in multi_member_split by force
      thus "(ρ⇩D ⊙ γ) x = γ⇩D x"
        apply (simp add: subst_compose_def ‹ρ⇩D x = Var x'›)
        by (metis (no_types, opaque_lifting) K_in UnI1 ‹ρ⇩D x = Var x'› ‹x ∈ vars_lit K›
            ground_prop image_eqI is_renaming_iff multi_member_split ren_ρ⇩D rename_subst_domain_def
            subset_iff the_inv_f_f vars_cls_add_mset vars_cls_subset_subst_domain_if_grounding)
    qed
  qed
qed

lemma resolve_preserves_ground_closures:
  assumes step: "resolve N β S S'" and invar: "ground_closures S"
  shows "ground_closures S'"
  using step
proof (cases N β S S' rule: resolve.cases)
  case (resolveI Γ Γ' K D γ⇩D L γ⇩C ρ⇩C ρ⇩D C μ γ U) 
  hence
    ren_ρ⇩C: "is_renaming ρ⇩C" and
    ren_ρ⇩D: "is_renaming ρ⇩D" and
    disjoint_vars: "vars_cls (add_mset L C ⋅ ρ⇩C) ∩ vars_cls (add_mset K D ⋅ ρ⇩D) = {}" and
    merge_γ: "is_grounding_merge γ
      (vars_cls (add_mset L C ⋅ ρ⇩C)) (rename_subst_domain ρ⇩C γ⇩C)
      (vars_cls (add_mset K D ⋅ ρ⇩D)) (rename_subst_domain ρ⇩D γ⇩D)"
    by simp_all
  hence "∀x. is_Var (ρ⇩C x)" and "inj ρ⇩C" and "∀x. is_Var (ρ⇩D x)" and "inj ρ⇩D"
    by (simp_all add: is_renaming_iff)

  from invar have
    ground_conf: "is_ground_cls (add_mset L C ⋅ γ⇩C)" and
    ground_prop: "is_ground_cls (add_mset K D ⋅ γ⇩D)" and
    min_ground_clo_Γ: "∀Ln ∈ set  Γ. ∀C L γ. snd Ln = Some (C, L, γ) ⟶ is_ground_cls (add_mset L C ⋅ γ)"
    unfolding resolveI(1,2) ‹Γ = trail_propagate Γ' K D γ⇩D›
    by (simp_all add: propagate_lit_def ground_closures_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 merge_of_renamed_groundings[OF ren_ρ⇩C ren_ρ⇩D disjoint_vars _ _ merge_γ] by simp_all

  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)
  thus ?thesis
    using ground_conf ground_prop min_ground_clo_Γ
    unfolding resolveI
    by (simp add: ground_closures_def)
qed

lemma backtrack_preserves_ground_closures:
  assumes step: "backtrack N β S S'" and invar: "ground_closures S"
  shows "ground_closures S'"
  using assms
  by (cases N β S S' rule: backtrack.cases)
    (simp add: ground_closures_def decide_lit_def ball_Un)

lemma scl_preserves_ground_closures:
  assumes "scl N β S S'" and "ground_closures S"
  shows "ground_closures S'"
  using assms unfolding scl_def
  using propagate_preserves_ground_closures decide_preserves_ground_closures
    conflict_preserves_ground_closures skip_preserves_ground_closures
    factorize_preserves_ground_closures resolve_preserves_ground_closures
    backtrack_preserves_ground_closures
  by metis

subsection ‹Trail And Conflict Closures Are Ground And False›

definition ground_false_closures where
  "ground_false_closures S ⟷ ground_closures S ∧
    trail_closures_false (state_trail S) ∧
    (∀C γ. state_conflict S = Some (C, γ) ⟶ trail_false_cls (state_trail S) (C ⋅ γ))"

lemma ground_false_closures_initial_state[simp]: "ground_false_closures initial_state"
  by (simp add: ground_false_closures_def)

lemma propagate_preserves_ground_false_closures:
  assumes step: "propagate N β S S'" and invar: "ground_false_closures S"
  shows "ground_false_closures S'"
  using step
proof (cases N β S S' rule: propagate.cases)
  case step_hyps: (propagateI C U L C' γ C⇩0 C⇩1 Γ μ)

  have "ground_closures S'"
    using invar propagate_preserves_ground_closures[OF step]
    by (metis ground_false_closures_def)

  moreover have "trail_closures_false (state_trail S')"
    using invar propagate_preserves_trail_closures_false'[OF step]
    by (metis ground_false_closures_def trail_closures_false'_def)

  moreover have "∀C γ. state_conflict S' = Some (C, γ) ⟶ trail_false_cls (state_trail S') (C ⋅ γ)"
    unfolding step_hyps(1,2) by simp

  ultimately show ?thesis
    unfolding ground_false_closures_def by metis
qed

lemma decide_preserves_ground_false_closures:
  assumes step: "decide N β S S'" and invar: "ground_false_closures S"
  shows "ground_false_closures S'"
  using step
proof (cases N β S S' rule: decide.cases)
  case step_hyps: (decideI L γ Γ U)

  have "ground_closures S'"
    using invar decide_preserves_ground_closures[OF step]
    by (metis ground_false_closures_def)

  moreover have "trail_closures_false (state_trail S')"
    using invar decide_preserves_trail_closures_false'[OF step]
    by (metis ground_false_closures_def trail_closures_false'_def)

  moreover have "∀C γ. state_conflict S' = Some (C, γ) ⟶ trail_false_cls (state_trail S') (C ⋅ γ)"
    unfolding step_hyps(1,2) by simp

  ultimately show ?thesis
    unfolding ground_false_closures_def by metis
qed

lemma conflict_preserves_ground_false_closures:
  assumes step: "conflict N β S S'" and invar: "ground_false_closures S"
  shows "ground_false_closures S'"
  using step
proof (cases N β S S' rule: conflict.cases)
  case step_hyps: (conflictI D U γ Γ)

  have "ground_closures S'"
    using invar conflict_preserves_ground_closures[OF step]
    by (metis ground_false_closures_def)

  moreover have "trail_closures_false (state_trail S')"
    using invar conflict_preserves_trail_closures_false'[OF step]
    by (metis ground_false_closures_def trail_closures_false'_def)

  moreover have "∀C γ. state_conflict S' = Some (C, γ) ⟶ trail_false_cls (state_trail S') (C ⋅ γ)"
    unfolding step_hyps(1,2)
    using step_hyps(3-) by simp

  ultimately show ?thesis
    unfolding ground_false_closures_def by metis
qed

lemma skip_preserves_ground_false_closures:
  assumes step: "skip N β S S'" and invar: "ground_false_closures S"
  shows "ground_false_closures S'"
  using step
proof (cases N β S S' rule: skip.cases)
  case step_hyps: (skipI L D σ n Γ U)

  have "ground_closures S'"
    using invar skip_preserves_ground_closures[OF step]
    by (metis ground_false_closures_def)

  moreover have "trail_closures_false (state_trail S')"
    using invar skip_preserves_trail_closures_false'[OF step]
    by (metis ground_false_closures_def trail_closures_false'_def)

  moreover have "∀C γ. state_conflict S' = Some (C, γ) ⟶ trail_false_cls (state_trail S') (C ⋅ γ)"
    using invar
    unfolding step_hyps(1,2)
    using ‹- L ∉# D ⋅ σ›
    by (auto simp add: ground_false_closures_def elim!: subtrail_falseI)

  ultimately show ?thesis
    unfolding ground_false_closures_def by metis
qed

lemma factorize_preserves_ground_false_closures:
  assumes step: "factorize N β S S'" and invar: "ground_false_closures S"
  shows "ground_false_closures S'"
  using step
proof (cases N β S S' rule: factorize.cases)
  case step_hyps: (factorizeI L γ L' μ Γ U D)

  have "ground_closures S'"
    using invar factorize_preserves_ground_closures[OF step]
    by (metis ground_false_closures_def)

  moreover have "trail_closures_false (state_trail S')"
    using invar factorize_preserves_trail_closures_false'[OF step]
    by (metis ground_false_closures_def trail_closures_false'_def)

  moreover have "∀C γ. state_conflict S' = Some (C, γ) ⟶ trail_false_cls (state_trail S') (C ⋅ γ)"
    using invar conflict_set_after_factorization[OF step]
    unfolding step_hyps(1,2) ground_false_closures_def
    by (auto simp del: set_mset_add_mset_insert dest: trail_false_cls_ignores_duplicates)

  ultimately show ?thesis
    unfolding ground_false_closures_def by metis
qed

lemma resolve_preserves_ground_false_closures:
  assumes step: "resolve N β S S'" and invar: "ground_false_closures S"
  shows "ground_false_closures S'"
  using step
proof (cases N β S S' rule: resolve.cases)
  case step_hyps: (resolveI Γ Γ' K D γ⇩D L γ⇩C ρ⇩C ρ⇩D C μ γ U)
  hence Γ_def: "Γ = trail_propagate Γ' K D γ⇩D"
    by simp

  have "ground_closures S"
    using invar
    by (metis ground_false_closures_def)
  hence "ground_closures S'"
    using resolve_preserves_ground_closures[OF step]
    by metis

  moreover have "trail_closures_false (state_trail S')"
    using invar resolve_preserves_trail_closures_false'[OF step]
    by (metis ground_false_closures_def trail_closures_false'_def)

  moreover have "∀C γ. state_conflict S' = Some (C, γ) ⟶ trail_false_cls (state_trail S') (C ⋅ γ)"
  proof -
    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 step_hyps(1,2)
      by (simp_all add: ground_closures_def Γ_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 merge_of_renamed_groundings step_hyps(3-)
      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)+

    moreover have "trail_false_cls Γ (C ⋅ γ⇩C)"
      using invar
      unfolding step_hyps(1,2)
      by (simp add: ground_false_closures_def trail_false_cls_add_mset)

    moreover have "trail_false_cls Γ (D ⋅ γ⇩D)"
    proof (rule trail_false_cls_if_trail_false_suffix)
      show "suffix Γ' Γ"
        unfolding ‹Γ = trail_propagate Γ' K D γ⇩D›
        by (simp add: suffix_def)
    next
      show "trail_false_cls Γ' (D ⋅ γ⇩D)"
        using invar
        unfolding step_hyps(1,2) ‹Γ = trail_propagate Γ' K D γ⇩D›
        by (auto simp: ground_false_closures_def propagate_lit_def elim: trail_closures_false.cases)
    qed

    ultimately show ?thesis
      unfolding step_hyps(1,2)
      by (simp add: trail_false_cls_plus)
  qed

  ultimately show ?thesis
    unfolding ground_false_closures_def by metis
qed

lemma backtrack_preserves_ground_false_closures:
  assumes step: "backtrack N β S S'" and invar: "ground_false_closures S"
  shows "ground_false_closures S'"
  using step
proof (cases N β S S' rule: backtrack.cases)
  case step_hyps: (backtrackI Γ Γ' Γ'' K L σ D U)

  have "ground_closures S'"
    using invar backtrack_preserves_ground_closures[OF step]
    by (metis ground_false_closures_def)

  moreover have "trail_closures_false (state_trail S')"
    using invar backtrack_preserves_trail_closures_false'[OF step]
    by (metis ground_false_closures_def trail_closures_false'_def)

  moreover have "∀C γ. state_conflict S' = Some (C, γ) ⟶ trail_false_cls (state_trail S') (C ⋅ γ)"
    unfolding step_hyps(1,2) by simp

  ultimately show ?thesis
    unfolding ground_false_closures_def by metis
qed

lemma scl_preserves_ground_false_closures:
  assumes "scl N β S S'" and "ground_false_closures S"
  shows "ground_false_closures S'"
  using assms unfolding scl_def
  using propagate_preserves_ground_false_closures decide_preserves_ground_false_closures
    conflict_preserves_ground_false_closures skip_preserves_ground_false_closures
    factorize_preserves_ground_false_closures resolve_preserves_ground_false_closures
    backtrack_preserves_ground_false_closures
  by metis


subsection ‹Learned Clauses Are Non-empty›

definition learned_nonempty where
  "learned_nonempty S ⟷ {#} |∉| state_learned S"

lemma learned_nonempty_initial_state[simp]: "learned_nonempty initial_state"
  by (simp add: learned_nonempty_def)

lemma propagate_preserves_learned_nonempty:
  assumes "propagate N β S S'" and "learned_nonempty S"
  shows "learned_nonempty S'"
  using assms by (cases rule: propagate.cases) (simp add: learned_nonempty_def)

lemma decide_preserves_learned_nonempty:
  assumes "decide N β S S'" and "learned_nonempty S"
  shows "learned_nonempty S'"
  using assms by (cases rule: decide.cases) (simp add: learned_nonempty_def)

lemma conflict_preserves_learned_nonempty:
  assumes "conflict N β S S'" and "learned_nonempty S"
  shows "learned_nonempty S'"
  using assms by (cases rule: conflict.cases) (simp add: learned_nonempty_def)

lemma skip_preserves_learned_nonempty:
  assumes "skip N β S S'" and "learned_nonempty S"
  shows "learned_nonempty S'"
  using assms by (cases rule: skip.cases) (simp add: learned_nonempty_def)

lemma factorize_preserves_learned_nonempty:
  assumes "factorize N β S S'" and "learned_nonempty S"
  shows "learned_nonempty S'"
  using assms by (cases rule: factorize.cases) (simp add: learned_nonempty_def)

lemma resolve_preserves_learned_nonempty:
  assumes "resolve N β S S'" and "learned_nonempty S"
  shows "learned_nonempty S'"
  using assms by (cases rule: resolve.cases) (simp add: learned_nonempty_def)

lemma backtrack_preserves_learned_nonempty:
  assumes "backtrack N β S S'" and "learned_nonempty S"
  shows "learned_nonempty S'"
  using assms by (cases rule: backtrack.cases) (simp add: learned_nonempty_def)

lemma scl_preserves_learned_nonempty:
  assumes "scl N β S S'" and "learned_nonempty S"
  shows "learned_nonempty S'"
  using assms unfolding scl_def
  using propagate_preserves_learned_nonempty decide_preserves_learned_nonempty
    conflict_preserves_learned_nonempty skip_preserves_learned_nonempty
    factorize_preserves_learned_nonempty resolve_preserves_learned_nonempty
    backtrack_preserves_learned_nonempty
  by metis


subsection ‹Backtrack Follows Conflict Resolution›

definition conflict_resolution where
  "conflict_resolution N β S ⟷ (state_conflict S ≠ None ⟶
    (∃S0 S1. conflict N β S0 S1 ∧ (skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S1 S))"

lemma conflict_resolution_initial_state[simp]: "conflict_resolution N β initial_state"
  by (simp add: conflict_resolution_def)

lemma propagate_preserves_conflict_resolution:
  assumes step: "propagate N β S S'"
  shows "conflict_resolution N β S'"
  using step by (auto simp: conflict_resolution_def elim: propagate.cases)

lemma decide_preserves_conflict_resolution:
  assumes step: "decide N β S S'"
  shows "conflict_resolution N β S'"
  using step by (auto simp: conflict_resolution_def elim: decide.cases)

lemma conflict_preserves_conflict_resolution:
  assumes step: "conflict N β S S'"
  shows "conflict_resolution N β S'"
  using step unfolding conflict_resolution_def by blast

lemma skip_preserves_conflict_resolution:
  assumes step: "skip N β S S'" and invar: "conflict_resolution N β S"
  shows "conflict_resolution N β S'"
  using step
proof -
  from step have "state_conflict S ≠ None"
    by (auto elim: skip.cases)
  with invar obtain S0 S1 where
    "conflict N β S0 S1" and "(skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S1 S"
    by (auto simp: conflict_resolution_def)
  show ?thesis
    unfolding conflict_resolution_def
  proof (intro impI exI conjI)
    show "conflict N β S0 S1"
      by (rule ‹conflict N β S0 S1›)
  next
    show "(skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S1 S'"
      using ‹(skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S1 S› step
      by (metis (no_types, opaque_lifting) rtranclp.rtrancl_into_rtrancl sup2CI)
  qed
qed

lemma factorize_preserves_conflict_resolution:
  assumes step: "factorize N β S S'" and invar: "conflict_resolution N β S"
  shows "conflict_resolution N β S'"
  using step
proof -
  from step have "state_conflict S ≠ None"
    by (auto elim: factorize.cases)
  with invar obtain S0 S1 where
    "conflict N β S0 S1" and "(skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S1 S"
    by (auto simp: conflict_resolution_def)
  show ?thesis
    unfolding conflict_resolution_def
  proof (intro impI exI conjI)
    show "conflict N β S0 S1"
      by (rule ‹conflict N β S0 S1›)
  next
    show "(skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S1 S'"
      using ‹(skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S1 S› step
      by (metis (no_types, opaque_lifting) rtranclp.rtrancl_into_rtrancl sup2CI)
  qed
qed

lemma resolve_preserves_conflict_resolution:
  assumes step: "resolve N β S S'" and invar: "conflict_resolution N β S"
  shows "conflict_resolution N β S'"
  using step
proof -
  from step have "state_conflict S ≠ None"
    by (auto elim: resolve.cases)
  with invar obtain S0 S1 where
    "conflict N β S0 S1" and "(skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S1 S"
    by (auto simp: conflict_resolution_def)
  show ?thesis
    unfolding conflict_resolution_def
  proof (intro impI exI conjI)
    show "conflict N β S0 S1"
      by (rule ‹conflict N β S0 S1›)
  next
    show "(skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S1 S'"
      using ‹(skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S1 S› step
      by (metis (no_types, opaque_lifting) rtranclp.rtrancl_into_rtrancl sup2CI)
  qed
qed

lemma backtrack_preserves_conflict_resolution:
  assumes step: "backtrack N β S S'"
  shows "conflict_resolution N β S'"
  using step by (auto simp: conflict_resolution_def elim: backtrack.cases)

lemma scl_preserves_conflict_resolution:
  assumes "scl N β S S'" and "conflict_resolution N β S"
  shows "conflict_resolution N β S'"
  using assms unfolding scl_def
  using propagate_preserves_conflict_resolution decide_preserves_conflict_resolution
    conflict_preserves_conflict_resolution skip_preserves_conflict_resolution
    factorize_preserves_conflict_resolution resolve_preserves_conflict_resolution
    backtrack_preserves_conflict_resolution
  by metis


subsection ‹Miscellaneous Lemmas›

lemma before_conflict:
  assumes "conflict N β S1 S2" and
    invars: "learned_nonempty S1" "trail_propagated_or_decided' N β S1"
  shows "{#} |∈| N ∨ (∃S0. propagate N β S0 S1) ∨ (∃S0. decide N β S0 S1)"
  using assms
proof (cases N β S1 S2 rule: conflict.cases)
  case (conflictI D U γ Γ)
  with invars(2) have "trail_propagated_or_decided N β U Γ"
    by (simp add: trail_propagated_or_decided'_def)
  thus ?thesis
  proof (cases N β U Γ rule: trail_propagated_or_decided.cases)
    case Nil
    hence "D ⋅ γ = {#}"
      using ‹trail_false_cls Γ (D ⋅ γ)› not_trail_false_Nil(2) by blast
    hence "D = {#}"
      by (simp add: local.conflictI(4))
    moreover from invars(1) have "{#} |∉| U"
      by (simp add: conflictI(1) learned_nonempty_def)
    ultimately have "{#} |∈| N"
      using ‹D |∈| N |∪| U› by simp
    thus ?thesis by simp
  next
    case (Propagate C L C' γ⇩C C⇩0 C⇩1 Γ' μ)
    hence "∃S0. propagate N β S0 S1"
      unfolding conflictI(1)
      using propagateI by blast
    thus ?thesis by simp
  next
    case (Decide L γ⇩L Γ')
    hence "∃S0. decide N β S0 S1"
      unfolding conflictI(1)
      using decideI by blast
    thus ?thesis by simp
  qed
qed

lemma before_backtrack:
  assumes backt: "backtrack N β Sn Sm" and
    invar: "conflict_resolution N β Sn"
  shows "∃S0 S1. conflict N β S0 S1 ∧ (skip N β ⊔ factorize N β ⊔ resolve N β)⇧*⇧* S1 Sn"
  using backt
proof (cases N β Sn Sm rule: backtrack.cases)
  case (backtrackI Γ Γ' Γ'' L σ D U)
  thus ?thesis
    using invar by (simp add: conflict_resolution_def)
qed

lemma ball_less_B_if_trail_false_and_trail_atoms_lt:
  "trail_false_cls (state_trail S) C ⟹ trail_atoms_lt β S ⟹ ∀L ∈# C. atm_of L ≼⇩B β"
  unfolding trail_atoms_lt_def
  by (meson atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set trail_false_cls_def
      trail_false_lit_def)


section ‹Soundness›


subsection ‹Sound Trail›

abbreviation entails_𝒢 (infix "⊫𝒢e" 50) where
  "entails_𝒢 N U ≡ grounding_of_clss N ⊫e grounding_of_clss U"

definition sound_trail where
  "sound_trail N Γ ⟷
    (∀Ln ∈ set Γ. ∀D K γ. snd Ln = Some (D, K, γ) ⟶ fset N ⊫𝒢e {add_mset K D})"

lemma sound_trail_Nil[simp]: "sound_trail N []"
  by (simp add: sound_trail_def)

lemma entails_𝒢_mono: "N ⊫𝒢e U ⟹ N ⊆ NN ⟹ NN ⊫𝒢e U"
  by (meson grounding_of_clss_mono true_clss_mono)

lemma sound_trail_supersetI: "sound_trail N Γ ⟹ N |⊆| NN ⟹ sound_trail NN Γ"
  unfolding sound_trail_def
  by (meson entails_𝒢_mono less_eq_fset.rep_eq)

lemma sound_trail_ConsD: "sound_trail N (Ln # Γ) ⟹ sound_trail N Γ"
  by (simp add: sound_trail_def)

lemma sound_trail_appendD: "sound_trail N (Γ @ Γ') ⟹ sound_trail N Γ'"
  by (induction Γ) (auto intro: sound_trail_ConsD)

lemma sound_trail_propagate:
  assumes
    sound_Γ: "sound_trail N Γ" and
    N_entails_C_L: "fset N ⊫𝒢e {C + {#L#}}"
  shows "sound_trail N (trail_propagate Γ L C σ)"
  using assms
  by (simp add: sound_trail_def propagate_lit_def)

lemma sound_trail_decide:
  "sound_trail N Γ ⟹ sound_trail N (trail_decide Γ L)"
  by (simp add: sound_trail_def decide_lit_def)


subsection ‹Sound State›

definition sound_state :: "('f, 'v) term clause fset ⇒ ('f, 'v) term ⇒ ('f, 'v) state ⇒ bool" where
  "sound_state N β S ⟷
    (∃Γ U u. S = (Γ, U, u) ∧ sound_trail N Γ ∧ fset N ⊫𝒢e fset U ∧
    (case u of None ⇒ True | Some (C, γ) ⇒ fset N ⊫𝒢e {C}))"


subsection ‹Initial State Is Sound›

lemma sound_initial_state[simp]: "sound_state N β initial_state"
  by (simp add: sound_state_def trail_atoms_lt_def)


subsection ‹SCL Rules Preserve Soundness›

lemma mem_vars_cls_subst_clsD: "x' ∈ vars_cls (C ⋅ ρ) ⟹ ∃x∈vars_cls C. x' ∈ vars_term (ρ x)"
  unfolding vars_subst_cls_eq
  using subst_domain_def by force

lemma propagate_preserves_sound_state:
  assumes step: "propagate N β S S'" and sound: "sound_state N β S"
  shows "sound_state N β S'"
  using assms(1)
proof (cases N β S S' rule: propagate.cases)
  case (propagateI C U L C' γ C⇩0 C⇩1 Γ μ)
  hence
    S_def: "S = (Γ, U, None)" and
    S'_def: "S' = (trail_propagate Γ (L ⋅l μ) (C⇩0 ⋅ μ) γ, U, None)" and
    C_in: "C |∈| N |∪| U" and
    C_def: "C = add_mset L C'" and
    gr_C_γ: "is_ground_cls (C ⋅ γ)" and
    C⇩0_def: "C⇩0 = {#K ∈# C'. K ⋅l γ ≠ L ⋅l γ#}" and
    C⇩1_def: "C⇩1 = {#K ∈# C'. K ⋅l γ = L ⋅l γ#}" and
    Γ_false_C⇩0_γ: "trail_false_cls Γ (C⇩0 ⋅ γ)" and
    undef_Γ_L_γ: "¬ trail_defined_lit Γ (L ⋅l γ)" and
    imgu_μ: "is_imgu μ {atm_of ` set_mset (add_mset L C⇩1)}"
    by simp_all

  from sound have
    sound_Γ: "sound_trail N Γ" and
    N_entails_U: "fset N ⊫𝒢e fset U"
    unfolding sound_state_def S_def by auto

  have vars_C⇩0: "vars_cls C⇩0 ⊆ vars_cls C'"
    apply (simp add: C⇩0_def)
    by (metis multiset_partition order_refl sup.coboundedI1 vars_cls_plus_iff)

  have vars_C⇩1: "vars_cls C⇩1 ⊆ vars_cls C'"
    apply (simp add: C⇩1_def)
    by (metis multiset_partition order_refl sup.coboundedI1 vars_cls_plus_iff)

  have fin_atm_C⇩1: "finite (atm_of ` (set_mset C⇩1))"
    by blast
  hence "is_unifier γ (atm_of ` (set_mset (add_mset L C⇩1)))"
    by (auto simp add: is_unifier_alt C⇩1_def intro: subst_atm_of_eqI)
  hence μ_γ_simp: "μ ⊙ γ = γ"
    using imgu_μ[unfolded is_imgu_def, THEN conjunct2]
    using is_unifiers_def by fastforce

  have "L ⋅l μ ⋅l γ = L ⋅l γ"
    using μ_γ_simp by (metis subst_lit_comp_subst)

  have "C⇩0 ⋅ μ ⋅ γ = C⇩0 ⋅ γ"
    using μ_γ_simp by (metis subst_cls_comp_subst)

  have "sound_trail N (trail_propagate Γ (L ⋅l μ) (C⇩0 ⋅ μ) γ)"
  proof (rule sound_trail_propagate)
    show "sound_trail N Γ"
      by (rule sound_Γ)
  next
    from C_in N_entails_U have "fset N ⊫𝒢e {C}"
      by (metis (no_types, opaque_lifting) empty_subsetI funion_iff grounding_of_clss_mono
          insert_subset true_clss_mono)
    hence "fset N ⊫𝒢e {add_mset L (C⇩0 + C⇩1)}"
      by (simp add: C_def C⇩0_def C⇩1_def)
    hence "fset N ⊫𝒢e {add_mset L (C⇩0 + C⇩1) ⋅ μ}"
      by (metis (no_types, opaque_lifting) grounding_of_clss_singleton
          subst_cls_eq_grounding_of_cls_subset_eq true_clss_mono)
    hence "fset N ⊫𝒢e {add_mset L C⇩0 ⋅ μ}"
    proof (rule entails_trans)
      have "∃C∈grounding_of_clss {(C⇩0 + C⇩1 + {#L#}) ⋅ μ}. set_mset D = set_mset C"
        if D_in: "D ∈ grounding_of_clss {(C⇩0 + {#L#}) ⋅ μ}" for I D
      proof-
        from D_in obtain σ where
          D_def: "D = add_mset L C⇩0 ⋅ μ ⋅ σ" and gr_σ: "is_ground_subst σ"
          by (auto simp: grounding_of_cls_def)
        show ?thesis
        proof (rule bexI)
          from imgu_μ have "is_unifier μ (atm_of ` set_mset (add_mset L C⇩1))"
            by (simp add: is_imgu_def is_unifiers_def)
          hence "∀A∈atm_of ` set_mset (add_mset L C⇩1). ∀B∈atm_of ` set_mset (add_mset L C⇩1).
            A ⋅a μ = B ⋅a μ"
            using is_unifier_alt
            by (metis (mono_tags, opaque_lifting) finite_imageI finite_set_mset)
          hence "∀A∈atm_of ` set_mset C⇩1. A ⋅a μ = atm_of L ⋅a μ"
            by (metis image_insert insert_iff set_mset_add_mset_insert)
          hence "∀A∈set_mset C⇩1. A ⋅l μ = L ⋅l μ"
            unfolding C⇩1_def
            by (metis (mono_tags, lifting) atm_of_subst_lit image_eqI literal.expand mem_Collect_eq
                set_mset_filter subst_lit_is_neg)
          hence "set_mset ((add_mset L C⇩1) ⋅ μ) = {L ⋅l μ}"
            by auto
          hence "set_mset ((C⇩0 + C⇩1 + {#L#}) ⋅ μ) = set_mset ((C⇩0 + {#L#}) ⋅ μ)"
            by auto
          thus "set_mset D = set_mset ((C⇩0 + C⇩1 + {#L#}) ⋅ μ ⋅ σ)"
            unfolding D_def set_mset_subst_cls_conv[of _ σ]
            by simp
        next
          show "(C⇩0 + C⇩1 + {#L#}) ⋅ μ ⋅ σ ∈ grounding_of_clss {(C⇩0 + C⇩1 + {#L#}) ⋅ μ}"
            using gr_σ by (auto simp: grounding_of_cls_def)
        qed
      qed
      then show "{add_mset L (C⇩0 + C⇩1) ⋅ μ} ⊫𝒢e {add_mset L C⇩0 ⋅ μ}"
        by (auto elim: true_clss_if_set_mset_eq[rotated])
    qed
    thus "fset N ⊫𝒢e {C⇩0 ⋅ μ + {#L ⋅l μ#}}"
      by (metis (no_types, opaque_lifting) add_mset_add_single grounding_of_clss_singleton
          subst_cls_add_mset)
  qed
  thus ?thesis
    unfolding S'_def sound_state_def
    using N_entails_U by simp
qed

lemma decide_preserves_sound_state:
  assumes step: "decide N β S S'" and sound: "sound_state N β S"
  shows "sound_state N β S'"
  using assms(1)
proof (cases N β S S' rule: decide.cases)
  case (decideI L γ Γ U)
  from decideI(1) sound have
    sound_Γ: "sound_trail N Γ" and
    N_entails_U: "fset N ⊫𝒢e fset U"
    unfolding sound_state_def by auto

  moreover have "sound_trail N (trail_decide Γ (L ⋅l γ))"
    by (simp add: local.decideI(4) local.decideI(5) sound_Γ sound_trail_decide)

  ultimately show ?thesis
    unfolding decideI sound_state_def by simp
qed

lemma conflict_preserves_sound_state:
  assumes step: "conflict N β S S'" and sound: "sound_state N β S"
  shows "sound_state N β S'"
  using assms(1)
proof (cases N β S S' rule: conflict.cases)
  case (conflictI D U γ Γ)
  hence D_in: "D |∈| N |∪| U" by simp
  
  from conflictI(1) sound have
    sound_Γ: "sound_trail N Γ" and
    N_entails_U: "fset N ⊫𝒢e fset U"
    unfolding sound_state_def by auto

  have N_entails_D': "fset N ⊫𝒢e {D}"
  proof (intro allI impI)
    fix I
    assume valid_N: "I ⊫s grounding_of_clss (fset N)"
    then show "I ⊫s grounding_of_clss {D}"
      using D_in
      unfolding grounding_of_clss_singleton
      by (metis (mono_tags, opaque_lifting) N_entails_U UN_I funion_iff grounding_of_clss_def
          true_clss_def)
  qed
  thus ?thesis
    unfolding conflictI(1,2) sound_state_def
    using sound_Γ N_entails_U by simp
qed

lemma skip_preserves_sound_state:
  assumes step: "skip N β S S'" and sound: "sound_state N β S"
  shows "sound_state N β S'"
  using step
proof (cases N β S S' rule: skip.cases)
  case (skipI L D σ Cl Γ U)
  thus ?thesis
    using sound
    by (auto simp: sound_state_def trail_atoms_lt_def
        intro: sound_trail_ConsD elim!: subtrail_falseI)
qed

lemma factorize_preserves_sound_state:
  assumes step: "factorize N β S S'" and sound: "sound_state N β S"
  shows "sound_state N β S'"
  using assms(1)
proof (cases N β S S' rule: factorize.cases)
  case (factorizeI L γ L' μ Γ U D)

  from factorizeI(1) sound have
    sound_Γ: "sound_trail N Γ" and
    N_entails_U: "fset N ⊫𝒢e fset U" and
    N_entails_D_L_L': "fset N ⊫𝒢e {D + {#L, L'#}}"
    unfolding sound_state_def by (simp_all add: add_mset_commute)

  from factorizeI have
    imgu_μ: "is_imgu μ {{atm_of L, atm_of L'}}"
    by simp
  from factorizeI have L_eq_L'_γ: "L ⋅l γ = L' ⋅l γ" by simp

  from L_eq_L'_γ have unif_γ: "is_unifier γ {atm_of L, atm_of L'}"
    by (auto simp: is_unifier_alt intro: subst_atm_of_eqI)
  hence unifs_γ: "is_unifiers γ {{atm_of L, atm_of L'}}"
    by (simp add: is_unifiers_def)

  from imgu_μ have "is_unifier μ {atm_of L, atm_of L'}"
    by (auto simp add: is_unifiers_def dest: is_imgu_is_mgu[THEN is_mgu_is_unifiers])
  hence L_eq_L'_μ: "L ⋅l μ = L' ⋅l μ"
    apply (simp add: is_unifier_alt)
    by (metis L_eq_L'_γ atm_of_subst_lit literal.expand subst_lit_is_neg)

  have "fset N ⊫𝒢e {(D + {#L#}) ⋅ μ}"
  proof (rule entails_trans)
    show "fset N ⊫𝒢e {D + {#L, L'#}}"
      by (rule N_entails_D_L_L')
  next
    have *: "{(D + {#L, L'#}) ⋅ μ} = {D ⋅ μ + {#L ⋅l μ, L ⋅l μ#}}"
      by (simp add: L_eq_L'_μ)

    have "{D + {#L, L'#}} ⊫𝒢e {(D + {#L, L'#}) ⋅ μ}"
      using subst_cls_eq_grounding_of_cls_subset_eq true_clss_mono
      by (metis (mono_tags, lifting) grounding_of_clss_singleton)

    moreover have "{(D + {#L, L'#}) ⋅ μ} ⊫𝒢e {(D + {#L#}) ⋅ μ}"
      apply (intro allI impI)
      by (erule true_clss_if_set_mset_eq[rotated]) (auto simp add: L_eq_L'_μ grounding_of_cls_def)

    ultimately show "{D + {#L, L'#}} ⊫𝒢e {(D + {#L#}) ⋅ μ}"
      by simp
  qed
  thus ?thesis
    unfolding factorizeI sound_state_def
    using sound_Γ N_entails_U by simp
qed

lemma resolve_preserves_sound_state:
  assumes step: "resolve N β S S'" and sound: "sound_state N β S"
  shows "sound_state N β S'"
  using assms(1)
proof (cases N β S S' rule: resolve.cases)
  case (resolveI Γ Γ' K D γ⇩D L γ⇩C ρ⇩C ρ⇩D C μ γ U)
  hence
    Γ_def: "Γ = trail_propagate Γ' K D γ⇩D" and
    imgu_μ: "is_imgu μ {{atm_of L ⋅a ρ⇩C, atm_of K ⋅a ρ⇩D}}"
    by simp_all

  from sound have
    sound_Γ: "sound_trail N Γ" and
    N_entails_U: "fset N ⊫𝒢e fset U" and
    N_entails_conf: "fset N ⊫𝒢e {add_mset L C}"
    unfolding resolveI(1,2) sound_state_def by simp_all

  from sound_Γ have
    N_entails_prop: "fset N ⊫𝒢e {add_mset K D}"
    unfolding sound_trail_def Γ_def
    by (simp add: propagate_lit_def)

  moreover have "fset N ⊫𝒢e {(C ⋅ ρ⇩C + D ⋅ ρ⇩D) ⋅ μ}"
  proof -
    have *: "fset N ⊫𝒢e {add_mset L C ⋅ ρ⇩C ⋅ μ}"
      using N_entails_conf
      by (metis (no_types, opaque_lifting) grounding_of_clss_singleton grounding_of_subst_cls_subset
          true_clss_mono)

    have **: "fset N ⊫𝒢e {add_mset K D ⋅ ρ⇩D ⋅ μ}"
      using N_entails_prop
      by (metis (no_types, opaque_lifting) grounding_of_clss_singleton grounding_of_subst_cls_subset
          true_clss_mono)

    show "fset N ⊫𝒢e {(C ⋅ ρ⇩C + D ⋅ ρ⇩D) ⋅ μ}"
      unfolding true_clss_def
    proof (intro allI impI ballI)
      fix I E
      assume I_entails: "∀E ∈ grounding_of_clss (fset N). I ⊫ E" and
        E_in: "E ∈ grounding_of_clss {(C ⋅ ρ⇩C + D ⋅ ρ⇩D) ⋅ μ}"
      then obtain γ⇩E where
        E_def: "E = (C ⋅ ρ⇩C + D ⋅ ρ⇩D) ⋅ μ ⋅ γ⇩E" and gr_γ⇩E: "is_ground_subst γ⇩E"
        unfolding grounding_of_clss_def grounding_of_cls_def by auto

      have "I ⊫l L ⋅l ρ⇩C ⋅l μ ⋅l γ⇩E ∨ (∃x ∈# C ⋅ ρ⇩C ⋅ μ ⋅ γ⇩E. I ⊫l x)"
      proof -
        have "add_mset L C ⋅ ρ⇩C ⋅ μ ⋅ γ⇩E ∈ grounding_of_clss {add_mset L C ⋅ ρ⇩C ⋅ μ}"
          using gr_γ⇩E unfolding grounding_of_clss_def grounding_of_cls_def by auto
        hence "∃K ∈# add_mset L C ⋅ ρ⇩C ⋅ μ ⋅ γ⇩E. I ⊫l K"
          using *[rule_format, unfolded true_clss_def, OF I_entails]
          by (metis true_cls_def)
        thus ?thesis
          by simp
      qed

      moreover have "I ⊫l K ⋅l ρ⇩D ⋅l μ ⋅l γ⇩E ∨ (∃x ∈# D ⋅ ρ⇩D ⋅ μ ⋅ γ⇩E. I ⊫l x)"
      proof -
        have "add_mset K D ⋅ ρ⇩D ⋅ μ ⋅ γ⇩E ∈ grounding_of_clss {add_mset K D ⋅ ρ⇩D ⋅ μ}"
          using gr_γ⇩E unfolding grounding_of_clss_def grounding_of_cls_def by auto
        hence "∃K ∈# add_mset K D ⋅ ρ⇩D ⋅ μ ⋅ γ⇩E. I ⊫l K"
          using **[rule_format, unfolded true_clss_def, OF I_entails]
          by (metis true_cls_def)
        thus ?thesis
          by simp
      qed

      ultimately show "I ⊫ E"
      proof (elim disjE)
        assume "I ⊫l L ⋅l ρ⇩C ⋅l μ ⋅l γ⇩E" and "I ⊫l K ⋅l ρ⇩D ⋅l μ ⋅l γ⇩E"
        moreover have "atm_of L ⋅a ρ⇩C ⋅a μ = atm_of K ⋅a ρ⇩D ⋅a μ"
          using imgu_μ[unfolded is_imgu_def]
          by (meson finite.emptyI finite.insertI insertCI is_unifier_alt is_unifiers_def)
        ultimately have False
          using ‹K ⋅l γ⇩D = - (L ⋅l γ⇩C)›
          by (cases L; cases K; simp add: uminus_literal_def subst_lit_def)
        thus ?thesis ..
      qed (auto simp: E_def)
    qed
  qed

  moreover have "sound_trail N (trail_propagate Γ' K D γ⇩D)"
    using Γ_def sound_Γ by blast

  ultimately show ?thesis
    unfolding resolveI sound_state_def
    using N_entails_U by simp
qed

lemma backtrack_preserves_sound_state:
  assumes step: "backtrack N β S S'" and sound: "sound_state N β S"
  shows "sound_state N β S'"
  using assms(1)
proof (cases N β S S' rule: backtrack.cases)
  case (backtrackI Γ Γ' Γ'' K L σ D U)
  from backtrackI(1) sound have
    sound_Γ: "sound_trail N Γ" and
    N_entails_U: "fset N ⊫𝒢e fset U" and
    N_entails_D_L_L': "fset N ⊫𝒢e {D + {#L#}}"
    unfolding sound_state_def by simp_all

  from backtrackI have Γ_def: "Γ = trail_decide (Γ' @ Γ'') (- (L ⋅l σ))" by simp

  moreover have "sound_trail N Γ''"
  proof -
    from sound_Γ have "sound_trail N Γ"
      by (rule sound_trail_supersetI) auto
    then show ?thesis
      by (auto simp: Γ_def decide_lit_def intro: sound_trail_ConsD sound_trail_appendD)
  qed

  moreover have "fset N ⊫𝒢e (fset U ∪ {D + {#L#}})"
    using N_entails_U N_entails_D_L_L' by (metis UN_Un grounding_of_clss_def true_clss_union)

  ultimately show ?thesis
    unfolding backtrackI sound_state_def by simp
qed

theorem scl_preserves_sound_state:
  fixes N :: "('f, 'v) Term.term clause fset"
  shows "scl N β S S' ⟹ sound_state N β S ⟹ sound_state N β S'"
  unfolding scl_def
  using propagate_preserves_sound_state decide_preserves_sound_state conflict_preserves_sound_state skip_preserves_sound_state
    factorize_preserves_sound_state resolve_preserves_sound_state backtrack_preserves_sound_state
  by metis


section ‹Strategies›

definition reasonable_scl where
  "reasonable_scl N β S S' ⟷
    scl N β S S' ∧ (decide N β S S' ⟶ ¬(∃S''. conflict N β S' S''))"

lemma scl_if_reasonable: "reasonable_scl N β S S' ⟹ scl N β S S'"
  unfolding reasonable_scl_def scl_def by simp

definition regular_scl where
  "regular_scl N β S S' ⟷
    conflict N β S S' ∨ ¬ (∃S''. conflict N β S S'') ∧ reasonable_scl N β S S'"

lemma reasonable_if_regular:
  "regular_scl N β S S' ⟹ reasonable_scl N β S S'"
  unfolding regular_scl_def
proof (elim disjE conjE)
  assume "conflict N β S S'"
  hence "scl N β S S'"
    by (simp add: scl_def)
  moreover have "decide N β S S' ⟶ ¬(∃S''. conflict N β S' S'')"
    by (smt (verit, best) ‹conflict N β S S'› conflict.cases option.distinct(1) snd_conv)
  ultimately show "reasonable_scl N β S S'"
    by (simp add: reasonable_scl_def)
next
  assume "¬ (∃S''. conflict N β S S'')" and "reasonable_scl N β S S'"
  thus ?thesis by simp
qed

lemma scl_if_regular:
  "regular_scl N β S S' ⟹ scl N β S S'"
  using scl_if_reasonable reasonable_if_regular by simp

text ‹The following specification of @{const regular_scl} is better for the paper as it highlights
that it is a restriction of @{const reasonable_scl}.›

lemma "regular_scl N β S S' ⟷ reasonable_scl N β S S' ∧
  ((∃S''. conflict N β S S'') ⟶ conflict N β S S')"
  (is "?lhs = ?rhs")
proof (rule iffI)
  assume ?lhs
  thus ?rhs
    unfolding regular_scl_def
  proof (elim disjE conjE)
    assume conf: "conflict N β S S'"
    show ?rhs
    proof (rule conjI)
      from conf have "¬ decide N β S S'"
        by (simp add: conflict_well_defined(2))
      with conf show "reasonable_scl N β S S'"
        unfolding reasonable_scl_def scl_def by simp
    next
      show "(∃S''. conflict N β S S'') ⟶ conflict N β S S'"
        using conf by simp
    qed
  next
    assume "¬ (∃S''. conflict N β S S'')" and "reasonable_scl N β S S'"
    thus ?rhs
      by simp
  qed
next
  assume ?rhs
  thus ?lhs
  proof (cases "∃S''. conflict N β S S''")
    case True
    with ‹?rhs› have "conflict N β S S'"
      by blast
    then show ?thesis
      unfolding regular_scl_def
      by simp
  next
    case False
    then show ?thesis
      unfolding regular_scl_def
      using ‹?rhs› by simp
  qed
qed

definition ex_conflict where
  "ex_conflict C Γ ⟷ (∃γ. is_ground_cls (C ⋅ γ) ∧ trail_false_cls Γ (C ⋅ γ))"

definition is_shortest_backtrack where
  "is_shortest_backtrack C Γ Γ⇩0 ⟷ C ≠ {#} ⟶ suffix Γ⇩0 Γ ∧ ¬ ex_conflict C Γ⇩0 ∧
    (∀Kn. suffix (Kn # Γ⇩0) Γ ⟶ ex_conflict C (Kn # Γ⇩0))"

definition shortest_backtrack_strategy where
  "shortest_backtrack_strategy R N β S S' ⟷ R N β S S' ∧ (backtrack N β S S' ⟶
    is_shortest_backtrack (fst (the (state_conflict S))) (state_trail S) (state_trail S'))"

lemma regular_scl_if_shortest_backtrack_strategy:
  "shortest_backtrack_strategy regular_scl N β S S' ⟹ regular_scl N β S S'"
  by (simp add: shortest_backtrack_strategy_def)

lemma strategy_restrictions:
  shows
    "shortest_backtrack_strategy regular_scl N β S S' ⟹ regular_scl N β S S'" and
    "regular_scl N β S S' ⟹ reasonable_scl N β S S'" and
    "reasonable_scl N β S S' ⟹ scl N β S S'"
  using regular_scl_if_shortest_backtrack_strategy reasonable_if_regular scl_if_reasonable
  by metis+

primrec shortest_backtrack where
  "shortest_backtrack C [] = []" |
  "shortest_backtrack C (Ln # Γ) =
    (if ex_conflict C (Ln # Γ) then
      shortest_backtrack C Γ
    else
      Ln # Γ)"

lemma suffix_shortest_backtrack: "suffix (shortest_backtrack C Γ) Γ"
  by (induction Γ) (simp_all add: suffix_Cons)

lemma ex_conflict_shortest_backtrack: "ex_conflict C (shortest_backtrack C Γ) ⟷ C = {#}"
  by (induction Γ) (auto simp add: ex_conflict_def)

lemma is_shortest_backtrack_shortest_backtrack:
  "C ≠ {#} ⟹ is_shortest_backtrack C Γ (shortest_backtrack C Γ)"
proof (induction Γ)
  case Nil
  then show ?case
    by (simp add: is_shortest_backtrack_def ex_conflict_def)
next
  case (Cons Kn Γ)
  then show ?case
    apply (simp del: )
    apply (rule conjI)
     apply (simp add: is_shortest_backtrack_def suffix_Cons)
    by (meson is_shortest_backtrack_def not_Cons_self2 suffix_ConsD suffix_appendD
        suffix_order.dual_order.antisym suffix_order.dual_order.refl)
qed


section ‹Monotonicity w.r.t. the Bounding Atom›

lemma scl_monotone_wrt_bound:
  assumes "⋀A. is_ground_atm A ⟹ A ≼⇩B β ⟹ A ≼⇩B β'" and "scl N β S⇩0 S⇩1"
  shows "scl N β' S⇩0 S⇩1"
  using assms(2)[unfolded scl_def]
proof (elim disjE)
  assume "propagate N β S⇩0 S⇩1"
  with assms(1) have "propagate N β' S⇩0 S⇩1"
    using propagateI propagate.cases
    by (smt (verit) is_ground_cls_imp_is_ground_lit is_ground_lit_def)
  thus ?thesis
    by (simp add: scl_def)
next
  assume "decide N β S⇩0 S⇩1"
  with assms(1) have "decide N β' S⇩0 S⇩1"
    using decideI decide.cases
    by (metis atm_of_subst_lit is_ground_lit_def)
  thus ?thesis
    by (simp add: scl_def)
next
  assume "conflict N β S⇩0 S⇩1"
  with assms(1) have "conflict N β' S⇩0 S⇩1"
    by (auto intro!: conflictI elim: conflict.cases)
  thus ?thesis
    by (simp add: scl_def)
next
  assume "skip N β S⇩0 S⇩1"
  with assms(1) have "skip N β' S⇩0 S⇩1"
    by (auto intro!: skipI elim: skip.cases)
  thus ?thesis
    by (simp add: scl_def)
next
  assume "factorize N β S⇩0 S⇩1"
  with assms(1) have "factorize N β' S⇩0 S⇩1"
    by (auto intro!: factorizeI elim: factorize.cases)
  thus ?thesis
    by (simp add: scl_def)
next
  assume "resolve N β S⇩0 S⇩1"
  with assms(1) have "resolve N β' S⇩0 S⇩1"
    by (auto intro!: resolveI elim: resolve.cases)
  thus ?thesis
    by (simp add: scl_def)
next
  assume "backtrack N β S⇩0 S⇩1"
  with assms(1) have "backtrack N β' S⇩0 S⇩1"
    by (auto intro!: backtrackI elim: backtrack.cases)
  thus ?thesis
    by (simp add: scl_def)
qed

lemma reasonable_scl_monotone_wrt_bound:
  assumes "⋀A. is_ground_atm A ⟹ A ≼⇩B β ⟹ A ≼⇩B β'" and "reasonable_scl N β S⇩0 S⇩1"
  shows "reasonable_scl N β' S⇩0 S⇩1"
  unfolding reasonable_scl_def
proof (intro conjI impI)
  show "scl N β' S⇩0 S⇩1"
    using assms scl_monotone_wrt_bound scl_if_reasonable by metis
next
  assume "decide N β' S⇩0 S⇩1"
  with assms(2) have "decide N β S⇩0 S⇩1"
    using decide_well_defined
    by (simp add: reasonable_scl_def scl_def)
  with assms(2) have "∄S⇩2. conflict N β S⇩1 S⇩2"
    by (simp add: reasonable_scl_def)
  with assms(1) show "∄S⇩2. conflict N β' S⇩1 S⇩2"
    by (simp add: conflict.simps)
qed

lemma regular_scl_monotone_wrt_bound:
  assumes "⋀A. is_ground_atm A ⟹ A ≼⇩B β ⟹ A ≼⇩B β'" and "regular_scl N β S⇩0 S⇩1"
  shows "regular_scl N β' S⇩0 S⇩1"
  using assms(2)[unfolded regular_scl_def]
proof (elim disjE conjE)
  assume "conflict N β S⇩0 S⇩1"
  hence "conflict N β' S⇩0 S⇩1"
    by (simp add: conflict.simps)
  thus "regular_scl N β' S⇩0 S⇩1"
    by (simp add: regular_scl_def)
next
  assume "∄S⇩1'. conflict N β S⇩0 S⇩1'" and "reasonable_scl N β S⇩0 S⇩1"
  have "∄S⇩1'. conflict N β' S⇩0 S⇩1'"
    using ‹∄S⇩1'. conflict N β S⇩0 S⇩1'›
    by (simp add: conflict.simps)
  moreover have "reasonable_scl N β' S⇩0 S⇩1"
    using assms(1) ‹reasonable_scl N β S⇩0 S⇩1› reasonable_scl_monotone_wrt_bound
    by metis
  ultimately show "regular_scl N β' S⇩0 S⇩1"
    by (simp add: regular_scl_def)
qed

lemma min_back_regular_scl_monotone_wrt_bound:
  assumes
    "⋀A. is_ground_atm A ⟹ A ≼⇩B β ⟹ A ≼⇩B β'" and
    "shortest_backtrack_strategy regular_scl N β S⇩0 S⇩1"
  shows "shortest_backtrack_strategy regular_scl N β' S⇩0 S⇩1"
  unfolding shortest_backtrack_strategy_def
proof (intro conjI impI)
  from assms(2) have "regular_scl N β S⇩0 S⇩1"
    by (simp add: shortest_backtrack_strategy_def)
  with assms(1) show "regular_scl N β' S⇩0 S⇩1"
    using regular_scl_monotone_wrt_bound
    by metis
next
  assume "backtrack N β' S⇩0 S⇩1"
  with assms(2) have "backtrack N β S⇩0 S⇩1"
    using backtrack_well_defined
    by (simp add: shortest_backtrack_strategy_def regular_scl_def reasonable_scl_def scl_def)
  with assms(2) show "is_shortest_backtrack
    (fst (the (state_conflict S⇩0))) (state_trail S⇩0) (state_trail S⇩1)"
    by (simp add: shortest_backtrack_strategy_def)
qed


lemma monotonicity_wrt_bound:
  assumes "⋀A. is_ground_atm A ⟹ A ≼⇩B β ⟹ A ≼⇩B β'"
  shows
    "scl N β S⇩0 S⇩1 ⟹ scl N β' S⇩0 S⇩1" and
    "reasonable_scl N β S⇩0 S⇩1 ⟹ reasonable_scl N β' S⇩0 S⇩1" and
    "regular_scl N β S⇩0 S⇩1 ⟹ regular_scl N β' S⇩0 S⇩1" and
    "shortest_backtrack_strategy regular_scl N β S⇩0 S⇩1 ⟹
      shortest_backtrack_strategy regular_scl N β' S⇩0 S⇩1"
  using assms
    scl_monotone_wrt_bound
    reasonable_scl_monotone_wrt_bound
    regular_scl_monotone_wrt_bound
    min_back_regular_scl_monotone_wrt_bound
  by metis+

corollary
  assumes
    "transp_on {A. is_ground_atm A} (≺⇩B)" and
    "is_ground_atm β" and
    "is_ground_atm β'" and
    "β ≺⇩B β'"
  shows
    "scl N β S⇩0 S⇩1 ⟹ scl N β' S⇩0 S⇩1" and
    "reasonable_scl N β S⇩0 S⇩1 ⟹ reasonable_scl N β' S⇩0 S⇩1" and
    "regular_scl N β S⇩0 S⇩1 ⟹ regular_scl N β' S⇩0 S⇩1" and
    "shortest_backtrack_strategy regular_scl N β S⇩0 S⇩1 ⟹
      shortest_backtrack_strategy regular_scl N β' S⇩0 S⇩1"
proof -
  from ‹transp_on {A. is_ground_atm A} (≺⇩B)› have "transp_on {A. is_ground_atm A} (≼⇩B)"
    by (metis transp_on_reflclp)
  moreover from ‹β ≺⇩B β'› have "β ≼⇩B β'"
    by blast
  ultimately have "⋀A. is_ground_atm A ⟹ A ≼⇩B β ⟹ A ≼⇩B β'"
    using ‹is_ground_atm β› ‹is_ground_atm β'›
    by (meson CollectI transp_onD)
  thus
    "scl N β S⇩0 S⇩1 ⟹ scl N β' S⇩0 S⇩1" and
    "reasonable_scl N β S⇩0 S⇩1 ⟹ reasonable_scl N β' S⇩0 S⇩1" and
    "regular_scl N β S⇩0 S⇩1 ⟹ regular_scl N β' S⇩0 S⇩1" and
    "shortest_backtrack_strategy regular_scl N β S⇩0 S⇩1 ⟹
      shortest_backtrack_strategy regular_scl N β' S⇩0 S⇩1"
    using monotonicity_wrt_bound
    by metis+
qed

end

end