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  (yxs. 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 multpDM_implies_one_step:
  "multpDM R M N  I J K. N = I + J  M = I + K  J  {#}  (k∈#K. x∈#J. R k x)"
  unfolding multpDM_def
  by (metis subset_mset.le_imp_diff_is_add)

lemma multpHO_implies_one_step:
  "multpHO R M N  I J K. N = I + J  M = I + K  J  {#}  (k∈#K. x∈#J. R k x)"
  by (metis multpDM_implies_one_step multpHO_imp_multpDM)

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: "xA. vars_term (γA x) = {}" and
    ball_B_ground: "xB. vars_term (γB x) = {}"

  from ball_A_ground have "xA. vars_term (γA x)  subst_domain γB = {}"
    by simp
  thus "(xA. γ x = γA x)  (xB. γ 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 set υ)  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 set υ) = 1"
      using fin_AA card (AA set υ)  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 σ  (xsubst_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 "xset Γ. is_ground_lit (fst x)" and "is_ground_lit (L ⋅l σ)"
  shows "xset (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 "xset Γ. is_ground_lit (fst x)" and "is_ground_lit L"
  shows "xset (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 tL tK
        from L = K show "L = Pos tL  K = Pos tK  ?thesis"
          by (simp add: trail_interp_def)
      next
        fix tL tK
        from L = K show "L = Neg tL  K = Neg tK  ?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 tL tK
        from L = - K show "L = Pos tL  K = Neg tK  ?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 tL tK
        from L = - K show "L = Neg tL  K = Pos tK  ?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'. LC'. 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 β 
    C0 = {#K ∈# C'. K ⋅l γ  L ⋅l γ#}  C1 = {#K ∈# C'. K ⋅l γ = L ⋅l γ#} 
    trail_false_cls Γ (C0  γ)  ¬ trail_defined_lit Γ (L ⋅l γ) 
    is_imgu μ {atm_of ` set_mset (add_mset L C1)} 
    propagate N β (Γ, U, None) (trail_propagate Γ (L ⋅l μ) (C0  μ) γ, U, None)"

lemma "C |∈| N |∪| U  C = add_mset L C'  is_ground_cls (C  γ) 
    K ∈# C. atm_of (K ⋅l γ) B β 
    C0 = {#K ∈# C'. K ⋅l γ  L ⋅l γ#}  C1 = {#K ∈# C'. K ⋅l γ = L ⋅l γ#} 
    trail_false_cls Γ (C0  γ)  ¬ trail_defined_lit Γ (L ⋅l γ) 
    is_imgu μ {atm_of ` set_mset (add_mset L C1)} 
    propagate N β (Γ, U, None) (trail_propagate Γ (L ⋅l μ) (C0  μ) γ, 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: