Theory Background

theory Background
  imports
    Simple_Clause_Learning.SCL_FOL
    Simple_Clause_Learning.Correct_Termination
    Simple_Clause_Learning.Initial_Literals_Generalize_Learned_Literals
    Simple_Clause_Learning.Termination
    Ground_Ordered_Resolution
    Min_Max_Least_Greatest.Min_Max_Least_Greatest_FSet
    Superposition_Calculus.Multiset_Extra
    VeriComp.Compiler
    "HOL-ex.Sketch_and_Explore"
    "HOL-Library.FuncSet"
    Lower_Set
    HOL_Extra_Extra
    The_Optional
    Full_Run
begin

lemma "I ⊫l L ⟷ (is_pos L ⟷ atm_of L ∈ I)"
  by (cases L) simp_all

section ‹Move to \<^theory>‹HOL-Library.Multiset››

lemmas strict_subset_implies_multp = subset_implies_multp
hide_fact subset_implies_multp

lemma subset_implies_reflclp_multp: "A ⊆# B ⟹ (multp R)⇧=⇧= A B"
  by (metis reflclp_iff strict_subset_implies_multp subset_mset.le_imp_less_or_eq)

lemma member_mset_repeat_msetD: "L ∈# repeat_mset n M ⟹ L ∈# M"
  by (induction n) auto

lemma member_mset_repeat_mset_Suc[simp]: "L ∈# repeat_mset (Suc n) M ⟷ L ∈# M"
  by (metis member_mset_repeat_msetD repeat_mset_Suc union_iff)

lemma image_msetI: "x ∈# M ⟹ f x ∈# image_mset f M"
  by (metis imageI in_image_mset)

lemma inj_image_mset_mem_iff: "inj f ⟹ f x ∈# image_mset f M ⟷ x ∈# M"
  by (simp add: inj_image_mem_iff)


section ‹Move to \<^theory>‹HOL-Library.FSet››

declare wfP_pfsubset[intro]

syntax
  "_FFilter" :: "pttrn ⇒ 'a fset ⇒ bool ⇒ 'a fset" ("(1{|_ |∈| _./ _|})")

translations
  "{|x |∈| X. P|}" == "CONST ffilter (λx. P) X"

lemma fimage_ffUnion: "f |`| ffUnion SS = ffUnion ((|`|) f |`| SS)"
proof (intro fsubset_antisym fsubsetI)
  fix x assume "x |∈| f |`| ffUnion SS"
  then obtain y where "y |∈| ffUnion SS" and "x = f y"
    by auto
  thus "x |∈| ffUnion ((|`|) f |`| SS)"
    unfolding fmember_ffUnion_iff
    by (metis UN_E ffUnion.rep_eq fimage_eqI)
next
  fix x assume "x |∈| ffUnion ((|`|) f |`| SS)"
  then obtain S where "S |∈| SS" and "x |∈| f |`| S"
    unfolding fmember_ffUnion_iff by auto
  then show "x |∈| f |`| ffUnion SS"
    by (metis ffUnion_fsubset_iff fimage_mono fin_mono fsubsetI)
qed

lemma ffilter_eq_ffilter_minus_singleton:
  assumes "¬ P y"
  shows "{|x |∈| X. P x|} = {|x |∈| X - {|y|}. P x|}"
  using assms by (induction X) auto

lemma fun_upd_fimage: "f(x := y) |`| A = (if x |∈| A then finsert y (f |`| (A - {|x|})) else f |`| A)"
  using fun_upd_image
  by (smt (verit) bot_fset.rep_eq finsert.rep_eq fset.set_map fset_cong minus_fset.rep_eq)

lemma ffilter_fempty[simp]: "ffilter P {||} = {||}"
  by (metis ex_fin_conv ffmember_filter)

lemma fstrict_subset_iff_fset_strict_subset_fset:
  fixes 𝒳 𝒴 :: "_ fset"
  shows "𝒳 |⊂| 𝒴 ⟷ fset 𝒳 ⊂ fset 𝒴"
    by blast

lemma (in linorder) ex1_sorted_list_for_fset:
  "∃!xs. sorted_wrt (<) xs ∧ fset_of_list xs = X"
  using ex1_sorted_list_for_set_if_finite
  by (metis finite_fset fset_cong fset_of_list.rep_eq)

lemma (in linorder) is_least_in_fset_ffilterD:
  assumes "is_least_in_fset_wrt (<) (ffilter P X) x"
  shows "x |∈| X" "P x"
  using assms
  by (simp_all add: is_least_in_fset_wrt_iff)


section ‹Move to \<^theory>‹VeriComp.Simulation››

locale forward_simulation_with_measuring_function =
  L1: semantics step1 final1 +
  L2: semantics step2 final2
  for
    step1 :: "'state1 ⇒ 'state1 ⇒ bool" and
    step2 :: "'state2 ⇒ 'state2 ⇒ bool" and
    final1 :: "'state1 ⇒ bool" and
    final2 :: "'state2 ⇒ bool" +
  fixes
    match :: "'state1 ⇒ 'state2 ⇒ bool" and
    measure :: "'state1 ⇒ 'index" and
    order :: "'index ⇒ 'index ⇒ bool" (infix "⊏" 70)
  assumes
    wfp_order:
      "wfp (⊏)" and
    match_final:
      "match s1 s2 ⟹ final1 s1 ⟹ final2 s2" and
    simulation:
      "match s1 s2 ⟹ step1 s1 s1' ⟹
        (∃s2'. step2⇧+⇧+ s2 s2' ∧ match s1' s2') ∨ (match s1' s2 ∧ measure s1' ⊏ measure s1)"
begin

sublocale forward_simulation where
  step1 = step1 and step2 = step2 and final1 = final1 and final2 = final2 and order = order and
  match = "λi x y. i = measure x ∧ match x y"
proof unfold_locales
  show "⋀i s1 s2. i = measure s1 ∧ match s1 s2 ⟹ final1 s1 ⟹ final2 s2"
    using match_final by metis
next
  show "⋀i s1 s2 s1'. i = measure s1 ∧ match s1 s2 ⟹ step1 s1 s1' ⟹
    (∃i' s2'. step2⇧+⇧+ s2 s2' ∧ i' = measure s1' ∧ match s1' s2') ∨
    (∃i'. (i' = measure s1' ∧ match s1' s2) ∧ i' ⊏ i)"
    using simulation by metis
next
  show "wfp (⊏)"
    using wfp_order .
qed

end

locale backward_simulation_with_measuring_function =
  L1: semantics step1 final1 +
  L2: semantics step2 final2
  for
    step1 :: "'state1 ⇒ 'state1 ⇒ bool" and
    step2 :: "'state2 ⇒ 'state2 ⇒ bool" and
    final1 :: "'state1 ⇒ bool" and
    final2 :: "'state2 ⇒ bool" +
  fixes
    match :: "'state1 ⇒ 'state2 ⇒ bool" and
    measure :: "'state2 ⇒ 'index" and
    order :: "'index ⇒ 'index ⇒ bool" (infix "⊏" 70)
  assumes
    wfp_order:
      "wfp (⊏)" and
    match_final:
      "match s1 s2 ⟹ final2 s2 ⟹ final1 s1" and
    simulation:
      "match s1 s2 ⟹ step2 s2 s2' ⟹
        (∃s1'. step1⇧+⇧+ s1 s1' ∧ match s1' s2') ∨ (match s1 s2' ∧ measure s2' ⊏ measure s2)"
begin

sublocale backward_simulation where
  step1 = step1 and step2 = step2 and final1 = final1 and final2 = final2 and order = order and
  match = "λi x y. i = measure y ∧ match x y"
proof unfold_locales
  show "⋀i s1 s2. i = measure s2 ∧ match s1 s2 ⟹ final2 s2 ⟹ final1 s1"
    using match_final by metis
next
  show "⋀i1 s1 s2 s2'. i1 = measure s2 ∧ match s1 s2 ⟹ step2 s2 s2' ⟹
    (∃i2 s1'. step1⇧+⇧+ s1 s1' ∧ i2 = measure s2' ∧ match s1' s2') ∨
    (∃i2. (i2 = measure s2' ∧ match s1 s2') ∧ i2 ⊏ i1)"
    using simulation by metis
next
  show "wfp (⊏)"
    using wfp_order .
qed

end


section ‹Move to \<^theory>‹Simple_Clause_Learning.SCL_FOL››

definition trail_true_lit :: "(_ literal × _ option) list ⇒ _ literal ⇒ bool" where
  "trail_true_lit Γ L ⟷ L ∈ fst ` set Γ"

definition trail_false_lit :: "(_ literal × _ option) list ⇒ _ literal ⇒ bool" where
  "trail_false_lit Γ L ⟷ - L ∈ fst ` set Γ"

definition trail_true_cls :: "(_ literal × _ option) list ⇒ _ clause ⇒ bool" where
  "trail_true_cls Γ C ⟷ (∃L ∈# C. trail_true_lit Γ L)"

definition trail_false_cls :: "(_ literal × _ option) list ⇒ _ clause ⇒ bool" where
  "trail_false_cls Γ C ⟷ (∀L ∈# C. trail_false_lit Γ L)"

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

definition trail_defined_lit :: "(_ literal × _ option) list ⇒ _ literal ⇒ bool" where
  "trail_defined_lit Γ L ⟷ (L ∈ fst ` set Γ ∨ - L ∈ fst ` set Γ)"

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)

definition trail_defined_cls :: "(_ literal × _ option) list ⇒ _ 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 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

inductive trail_consistent :: "('a literal × 'b option) list ⇒ bool" where
  Nil[simp]: "trail_consistent []" |
  Cons: "¬ trail_defined_lit Γ L ⟹ trail_consistent Γ ⟹ trail_consistent ((L, u) # Γ)"

lemma distinct_lits_if_trail_consistent:
  "trail_consistent Γ ⟹ distinct (map fst Γ)"
  by (induction Γ rule: trail_consistent.induct)
    (simp_all add: image_comp trail_defined_lit_def)

lemma trail_true_lit_if_trail_true_suffix:
  "suffix Γ' Γ ⟹ trail_true_lit Γ' K ⟹ trail_true_lit Γ K"
  by (meson image_mono set_mono_suffix subsetD trail_true_lit_def)

lemma trail_true_cls_if_trail_true_suffix:
  "suffix Γ' Γ ⟹ trail_true_cls Γ' C ⟹ trail_true_cls Γ C"
  using trail_true_cls_def trail_true_lit_if_trail_true_suffix by metis

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_defined_lit_if_trail_defined_suffix:
  "suffix Γ' Γ ⟹ trail_defined_lit Γ' K ⟹ trail_defined_lit Γ K"
  unfolding trail_defined_lit_def
  by (metis (no_types) Un_iff image_Un set_append suffix_def)

lemma trail_defined_cls_if_trail_defined_suffix:
  "suffix Γ' Γ ⟹ trail_defined_cls Γ' C ⟹ trail_defined_cls Γ C"
  unfolding trail_defined_cls_def by (metis trail_defined_lit_if_trail_defined_suffix)

lemma not_trail_true_lit_and_trail_false_lit:
  fixes Γ :: "('a literal × 'b option) list" and L :: "'a literal"
  shows "trail_consistent Γ ⟹ ¬ (trail_true_lit Γ L ∧ trail_false_lit Γ L)"
proof (induction Γ rule: trail_consistent.induct)
  case Nil
  show ?case
    by (simp add: trail_true_cls_def trail_false_cls_def trail_true_lit_def trail_false_lit_def)
next
  case (Cons Γ K annot)
  then show ?case
    unfolding trail_defined_lit_def trail_false_lit_def trail_true_lit_def
    by (metis (no_types, opaque_lifting) fst_conv image_insert insertE list.simps(15) uminus_not_id'
        uminus_of_uminus_id)
qed

lemma not_trail_true_cls_and_trail_false_cls:
  fixes Γ :: "('a literal × 'b option) list" and C :: "'a clause"
  shows "trail_consistent Γ ⟹ ¬ (trail_true_cls Γ C ∧ trail_false_cls Γ C)"
proof (induction Γ rule: trail_consistent.induct)
  case Nil
  show ?case
    by (simp add: trail_true_cls_def trail_false_cls_def trail_true_lit_def trail_false_lit_def)
next
  case (Cons Γ L u)
  thus ?case
    using not_trail_true_lit_and_trail_false_lit
    by (metis trail_consistent.Cons trail_false_cls_def trail_true_cls_def)
qed

lemma not_lit_and_comp_lit_false_if_trail_consistent:
 assumes "trail_consistent Γ"
  shows "¬ (trail_false_lit Γ L ∧ trail_false_lit Γ (- L))"
  using assms
proof (induction Γ)
  case Nil
  show ?case
    by (simp add: trail_false_lit_def)
next
 case (Cons Γ K u)
  show ?case
  proof (cases "K = L ∨ K = - L")
    case True
    thus ?thesis
      unfolding trail_false_lit_def uminus_of_uminus_id
      unfolding de_Morgan_conj list.set image_insert prod.sel
      by (metis Cons.hyps(1) insertE trail_defined_lit_def uminus_not_id' uminus_of_uminus_id)
 next
    case False
    thus ?thesis
      unfolding trail_false_lit_def uminus_of_uminus_id
      by (metis (no_types, lifting) Cons.IH fst_conv image_iff set_ConsD trail_false_lit_def
          uminus_of_uminus_id)
  qed
qed

lemma not_both_lit_and_comp_lit_in_false_clause_if_trail_consistent:
  assumes Γ_consistent: "trail_consistent Γ" and C_false: "trail_false_cls Γ C"
  shows "¬ (L ∈# C ∧ - L ∈# C)"
proof (rule notI)
  assume "L ∈# C ∧ - L ∈# C"

  hence "trail_false_lit Γ L ∧ trail_false_lit Γ (- L)"
    using C_false unfolding trail_false_cls_def by metis

  thus False
    using Γ_consistent not_lit_and_comp_lit_false_if_trail_consistent by metis
qed


section ‹Move to ground ordered resolution›

lemma (in ground_ordered_resolution_calculus) unique_ground_resolution:
  shows "∃⇩≤⇩1C. ground_resolution P1 P2 C"
proof (intro Uniq_I)
  fix C C'
  assume "ground_resolution P1 P2 C" and "ground_resolution P1 P2 C'"
  thus "C = C'"
    unfolding ground_resolution.simps
    apply (elim exE conjE)
    apply simp
    by (metis asymp_on_less_lit is_maximal_in_mset_wrt_if_is_greatest_in_mset_wrt
        is_maximal_in_mset_wrt_iff literal.inject(1) totalpD totalp_on_less_lit transp_on_less_lit
        union_single_eq_diff)
qed

lemma (in ground_ordered_resolution_calculus) unique_ground_factoring:
  shows "∃⇩≤⇩1C. ground_factoring P C"
proof (intro Uniq_I)
  fix P C C'
  assume "ground_factoring P C" and "ground_factoring P C'"
  thus "C = C'"
    unfolding ground_factoring.simps
    by (metis asymp_on_less_lit is_maximal_in_mset_wrt_iff totalpD totalp_less_lit
        transp_on_less_lit union_single_eq_diff)
qed

lemma (in ground_ordered_resolution_calculus) termination_ground_factoring:
  shows "wfP ground_factoring¯¯"
proof (rule wfp_if_convertible_to_wfp)
  show "⋀x y. ground_factoring¯¯ x y ⟹ x ≺⇩c y"
    using ground_factoring_smaller_conclusion by simp
next
  show "wfP (≺⇩c)"
    by simp
qed

lemma (in ground_ordered_resolution_calculus) atms_of_concl_subset_if_ground_resolution:
  assumes "ground_resolution P⇩1 P⇩2 C"
  shows "atms_of C ⊆ atms_of P⇩1 ∪ atms_of P⇩2"
  using assms by (cases P⇩1 P⇩2 C rule: ground_resolution.cases) (auto simp add: atms_of_def)

lemma (in ground_ordered_resolution_calculus) strict_subset_mset_if_ground_factoring:
  assumes "ground_factoring P C"
  shows "C ⊂# P"
  using assms by (cases P C rule: ground_factoring.cases) simp

lemma (in ground_ordered_resolution_calculus) set_mset_eq_set_mset_if_ground_factoring:
  assumes "ground_factoring P C"
  shows "set_mset P = set_mset C"
  using assms by (cases P C rule: ground_factoring.cases) simp

lemma (in ground_ordered_resolution_calculus) atms_of_concl_eq_if_ground_factoring:
  assumes "ground_factoring P C"
  shows "atms_of C = atms_of P"
  using assms by (cases P C rule: ground_factoring.cases) simp

lemma (in ground_ordered_resolution_calculus) ground_factoring_preserves_maximal_literal:
  assumes "ground_factoring P C"
  shows "is_maximal_lit L P = is_maximal_lit L C"
  using assms by (cases P C rule: ground_factoring.cases) (simp add: is_maximal_in_mset_wrt_iff)

lemma (in ground_ordered_resolution_calculus) ground_factorings_preserves_maximal_literal:
  assumes "ground_factoring⇧*⇧* P C"
  shows "is_maximal_lit L P = is_maximal_lit L C"
  using assms
  by (induction P rule: converse_rtranclp_induct)
    (simp_all add: ground_factoring_preserves_maximal_literal)

lemma (in ground_ordered_resolution_calculus) ground_factoring_reduces_maximal_pos_lit:
  assumes "ground_factoring P C" and "is_pos L" and
    "is_maximal_lit L P" and "count P L = Suc (Suc n)"
  shows "is_maximal_lit L C" and "count C L = Suc n"
  unfolding atomize_conj
  using ‹ground_factoring P C›
proof (cases P C rule: ground_factoring.cases)
  case (ground_factoringI t P')
  then show "is_maximal_lit L C ∧ count C L = Suc n"
    by (metis assms(1) assms(3) assms(4) asymp_on_less_lit count_add_mset
        ground_factoring_preserves_maximal_literal is_maximal_in_mset_wrt_iff nat.inject totalpD
        totalp_less_lit transp_on_less_lit)
qed

lemma (in ground_ordered_resolution_calculus) ground_factorings_reduces_maximal_pos_lit:
  assumes "(ground_factoring ^^ m) P C" and "m ≤ Suc n" and "is_pos L" and
    "is_maximal_lit L P" and "count P L = Suc (Suc n)"
  shows "is_maximal_lit L C" and "count C L = Suc (Suc n - m)"
  unfolding atomize_conj
  using ‹(ground_factoring ^^ m) P C› ‹m ≤ Suc n›
proof (induction m arbitrary: C)
  case 0
  hence "P = C"
    by simp
  then show ?case
    using assms(4,5) by simp
next
  case (Suc m')
  then show ?case
    by (metis Suc_diff_le Suc_leD assms(3) diff_Suc_Suc ground_factoring_reduces_maximal_pos_lit(2)
        ground_factorings_preserves_maximal_literal relpowp_Suc_E relpowp_imp_rtranclp)
qed

lemma (in ground_ordered_resolution_calculus) full_ground_factorings_reduces_maximal_pos_lit:
  assumes steps: "(ground_factoring ^^ Suc n) P C" and L_pos: "is_pos L" and
    L_max: "is_maximal_lit L P" and L_count: "count P L = Suc (Suc n)"
  shows "is_maximal_lit L C" and "count C L = Suc 0"
  unfolding atomize_conj
  using steps L_max L_count
proof (induction n arbitrary: P)
  case 0
  then show ?case
    using L_pos ground_factorings_reduces_maximal_pos_lit[of "Suc 0" P C 0] by simp
next
  case (Suc n)
  from Suc.prems obtain P' where
    "ground_factoring P P'" and "(ground_factoring ^^ Suc n) P' C"
    by (metis relpowp_Suc_D2)

  from Suc.prems have "is_maximal_lit L P'" and "count P' L = Suc (Suc n)"
    using ground_factoring_reduces_maximal_pos_lit[OF ‹ground_factoring P P'› L_pos] by simp_all

  thus ?case
    using Suc.IH[OF ‹(ground_factoring ^^ Suc n) P' C›] by metis
qed


section ‹Move somewhere?›

lemma true_cls_imp_neq_mempty: "ℐ ⊫ C ⟹ C ≠ {#}"
  by blast

lemma lift_tranclp_to_pairs_with_constant_fst:
  "(R x)⇧+⇧+ y z ⟹ (λ(x, y) (x', z). x = x' ∧ R x y z)⇧+⇧+ (x, y) (x, z)"
  by (induction z arbitrary: rule: tranclp_induct) (auto simp: tranclp.trancl_into_trancl)

abbreviation (in preorder) is_lower_fset where
  "is_lower_fset X Y ≡ is_lower_set_wrt (<) (fset X) (fset Y)"

lemma lower_set_wrt_prefixI:
  assumes
    trans: "transp_on (set zs) R" and
    asym: "asymp_on (set zs) R" and
    sorted: "sorted_wrt R zs" and
    prefix: "prefix xs zs"
  shows "is_lower_set_wrt R (set xs) (set zs)"
proof -
  obtain ys where "zs = xs @ ys"
    using prefix by (auto elim: prefixE)

  show ?thesis
    using trans asym sorted
    unfolding ‹zs = xs @ ys›
    by (metis lower_set_wrt_appendI)
qed

lemmas (in preorder) lower_set_prefixI =
  lower_set_wrt_prefixI[OF transp_on_less asymp_on_less]

lemma lower_set_wrt_suffixI:
  assumes
    trans: "transp_on (set zs) R" and
    asym: "asymp_on (set zs) R" and
    sorted: "sorted_wrt R¯¯ zs" and
    suffix: "suffix ys zs"
  shows "is_lower_set_wrt R (set ys) (set zs)"
proof -
  obtain xs where "zs = xs @ ys"
    using suffix by (auto elim: suffixE)

  show ?thesis
    using trans asym sorted
    unfolding ‹zs = xs @ ys›
    by (smt (verit, del_insts) Un_iff ‹zs = xs @ ys› asymp_onD asymp_on_conversep conversepI
        is_lower_set_wrt_def set_append set_mono_suffix sorted_wrt_append suffix)
qed

lemmas (in preorder) lower_set_suffixI =
  lower_set_wrt_suffixI[OF transp_on_less asymp_on_less]


lemma true_cls_repeat_mset_Suc[simp]: "I ⊫ repeat_mset (Suc n) C ⟷ I ⊫ C"
  by (induction n) simp_all

lemma (in backward_simulation)
  assumes "match i S1 S2" and "¬ L1.inf_step S1"
  shows "¬ L2.inf_step S2"
  using assms match_inf by metis

lemma (in scl_fol_calculus) grounding_of_clss_ground:
  assumes "is_ground_clss N"
  shows "grounding_of_clss N = N"
proof -
  have "grounding_of_clss N = (⋃ C ∈ N. grounding_of_cls C)"
    unfolding grounding_of_clss_def by simp
  also have "… = (⋃ C ∈ N. {C})"
    using ‹is_ground_clss N›
    by (simp add: is_ground_clss_def grounding_of_cls_ground)
  also have "… = N"
    by simp
  finally show ?thesis .
qed

lemma (in scl_fol_calculus) 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 γ#} ⟹
    SCL_FOL.trail_false_cls Γ (C⇩0 ⋅ γ) ⟹ ¬ SCL_FOL.trail_defined_lit Γ (L ⋅l γ) ⟹
    is_imgu μ {atm_of ` set_mset (add_mset L C⇩1)} ⟹
    Γ' = trail_propagate Γ (L ⋅l μ) (C⇩0 ⋅ μ) γ ⟹
    propagate N β (Γ, U, None) (Γ', U, None)"
  using propagateI by metis

lemma (in scl_fol_calculus) decideI':
  "is_ground_lit (L ⋅l γ) ⟹ ¬ SCL_FOL.trail_defined_lit Γ (L ⋅l γ) ⟹ atm_of L ⋅a γ ≼⇩B β ⟹
    Γ' = trail_decide Γ (L ⋅l γ) ⟹
    decide N β (Γ, U, None) (Γ', U, None)"
  by (auto intro!: decideI)

lemma ground_iff_vars_term_empty: "ground t ⟷ vars_term t = {}"
proof (rule iffI)
  show "ground t ⟹ vars_term t = {}"
    by (rule ground_vars_term_empty)
next
  show "vars_term t = {} ⟹ ground t"
    by (induction t) simp_all
qed

lemma is_ground_atm_eq_ground[iff]: "is_ground_atm = ground"
proof (rule ext)
  fix t :: "('v, 'f) Term.term"
  show "is_ground_atm t = ground t"
    by (simp only: is_ground_atm_iff_vars_empty ground_iff_vars_term_empty)
qed

definition lit_of_glit :: "'f gterm literal ⇒ ('f, 'v) term literal" where
  "lit_of_glit = map_literal term_of_gterm"

definition glit_of_lit where
  "glit_of_lit = map_literal gterm_of_term"

definition cls_of_gcls where
  "cls_of_gcls = image_mset lit_of_glit"

definition gcls_of_cls where
  "gcls_of_cls = image_mset glit_of_lit"

lemma inj_lit_of_glit: "inj lit_of_glit"
proof (rule injI)
  fix L K
  show "lit_of_glit L = lit_of_glit K ⟹ L = K"
    by (metis lit_of_glit_def literal.expand literal.map_disc_iff literal.map_sel term_of_gterm_inv)
qed

lemma atm_of_lit_of_glit_conv: "atm_of (lit_of_glit L) = term_of_gterm (atm_of L)"
  by (cases L) (simp_all add: lit_of_glit_def)

lemma ground_atm_of_lit_of_glit[simp]: "Term_Context.ground (atm_of (lit_of_glit L))"
  by (simp add: atm_of_lit_of_glit_conv)

lemma is_ground_lit_lit_of_glit[simp]: "is_ground_lit (lit_of_glit L)"
  by (simp add: is_ground_lit_def atm_of_lit_of_glit_conv)

lemma is_ground_cls_cls_of_gcls[simp]: "is_ground_cls (cls_of_gcls C)"
  by (auto simp add: is_ground_cls_def cls_of_gcls_def)

lemma glit_of_lit_lit_of_glit[simp]: "glit_of_lit (lit_of_glit L) = L"
  by (simp add: glit_of_lit_def lit_of_glit_def literal.map_comp comp_def literal.map_ident)

lemma gcls_of_cls_cls_of_gcls[simp]: "gcls_of_cls (cls_of_gcls L) = L"
  by (simp add: gcls_of_cls_def cls_of_gcls_def multiset.map_comp comp_def multiset.map_ident)

lemma lit_of_glit_glit_of_lit_ident[simp]: "is_ground_lit L ⟹ lit_of_glit (glit_of_lit L) = L"
  by (simp add: is_ground_lit_def lit_of_glit_def glit_of_lit_def literal.map_comp literal.expand
      literal.map_sel)

lemma cls_of_gcls_gcls_of_cls_ident[simp]: "is_ground_cls D ⟹ cls_of_gcls (gcls_of_cls D) = D"
  by (simp add: is_ground_cls_def cls_of_gcls_def gcls_of_cls_def)

lemma vars_lit_lit_of_glit[simp]: "vars_lit (lit_of_glit L) = {}"
  by simp

lemma vars_cls_cls_of_gcls[simp]: "vars_cls (cls_of_gcls C) = {}"
  by (metis is_ground_cls_cls_of_gcls is_ground_cls_iff_vars_empty)

definition atms_of_cls :: "'a clause ⇒ 'a fset" where
  "atms_of_cls C = atm_of |`| fset_mset C"

definition atms_of_clss :: "'a clause fset ⇒ 'a fset" where
  "atms_of_clss N = ffUnion (atms_of_cls |`| N)"

lemma atms_of_clss_fempty[simp]: "atms_of_clss {||} = {||}"
  unfolding atms_of_clss_def by simp

lemma atms_of_clss_finsert[simp]:
  "atms_of_clss (finsert C N) = atms_of_cls C |∪| atms_of_clss N"
  unfolding atms_of_clss_def by simp

definition lits_of_clss :: "'a clause fset ⇒ 'a literal fset" where
  "lits_of_clss N = ffUnion (fset_mset |`| N)"

definition lit_occures_in_clss where
  "lit_occures_in_clss L N ⟷ fBex N (λC. L ∈# C)"

inductive constant_context for R where
  "R 𝒞 𝒟 𝒟' ⟹ constant_context R (𝒞, 𝒟) (𝒞, 𝒟')"

lemma rtranclp_constant_context: "(R 𝒞)⇧*⇧* 𝒟 𝒟' ⟹ (constant_context R)⇧*⇧* (𝒞, 𝒟) (𝒞, 𝒟')"
  by (induction 𝒟' rule: rtranclp_induct) (auto intro: constant_context.intros rtranclp.intros)

lemma tranclp_constant_context: "(R 𝒞)⇧+⇧+ 𝒟 𝒟' ⟹ (constant_context R)⇧+⇧+ (𝒞, 𝒟) (𝒞, 𝒟')"
  by (induction 𝒟' rule: tranclp_induct) (auto intro: constant_context.intros tranclp.intros)

lemma right_unique_constant_context:
  assumes R_ru: "⋀𝒞. right_unique (R 𝒞)"
  shows "right_unique (constant_context R)"
proof (rule right_uniqueI)
  fix x y z
  show "constant_context R x y ⟹ constant_context R x z ⟹ y = z"
    using R_ru[THEN right_uniqueD]
    by (elim constant_context.cases) (metis prod.inject)
qed

lemma safe_state_constant_context_if_invars:
  fixes N s
  assumes
    ℛ_preserves_ℐ:
      "⋀N s s'. ℛ N s s' ⟹ ℐ N s ⟹ ℐ N s'" and
    ex_ℛ_if_not_final:
      "⋀N s. ¬ ℱ (N, s) ⟹ ℐ N s ⟹ ∃s'. ℛ N s s'"
  assumes invars: "ℐ N s"
  shows "safe_state (constant_context ℛ) ℱ (N, s)"
proof -
  {
    fix S'
    assume "(constant_context ℛ)⇧*⇧* (N, s) S'" and "stuck_state (constant_context ℛ) S'"
    then obtain s' where "S' = (N, s')" and "(ℛ N)⇧*⇧* s s'" and "ℐ N s'"
      using invars
    proof (induction "(N, s)" arbitrary: N s rule: converse_rtranclp_induct)
      case base
      thus ?case by simp
    next
      case (step z)
      thus ?case
        by (metis (no_types, opaque_lifting) Pair_inject ℛ_preserves_ℐ constant_context.cases
            converse_rtranclp_into_rtranclp)
    qed
    hence "¬ ℱ (N, s') ⟹ ∃s''. ℛ N s' s''"
      using ex_ℛ_if_not_final[of N s'] by argo
    hence "¬ ℱ S' ⟹ ∃S''. constant_context ℛ S' S''"
      unfolding ‹S' = (N, s')› using constant_context.intros by metis
    hence "ℱ S'"
      by (metis ‹stuck_state (constant_context ℛ) S'› stuck_state_def)
  }
  thus ?thesis
    by (metis (no_types) safe_state_def stuck_state_def)
qed

primrec trail_atms :: "(_ literal × _) list ⇒ _ fset" where
  "trail_atms [] = {||}" |
  "trail_atms (Ln # Γ) = finsert (atm_of (fst Ln)) (trail_atms Γ)"

lemma fset_trail_atms: "fset (trail_atms Γ) = atm_of ` fst ` set Γ"
  by (induction Γ) simp_all

lemma trail_defined_lit_iff_trail_defined_atm:
  "trail_defined_lit Γ L ⟷ atm_of L |∈| trail_atms Γ"
proof (induction Γ)
  case Nil
  show ?case
    by (simp add: trail_defined_lit_def)
next
  case (Cons Ln Γ)

  have "trail_defined_lit (Ln # Γ) L ⟷ L = fst Ln ∨ - L = fst Ln ∨ trail_defined_lit Γ L"
    unfolding trail_defined_lit_def by auto

  also have "… ⟷ atm_of L = atm_of (fst Ln) ∨ trail_defined_lit Γ L"
    by (cases L; cases "fst Ln") simp_all

  also have "… ⟷ atm_of L = atm_of (fst Ln) ∨ atm_of L |∈| trail_atms Γ"
    unfolding Cons.IH ..

  also have "… ⟷ atm_of L |∈| trail_atms (Ln # Γ)"
    by simp

  finally show ?case .
qed

lemma trail_atms_subset_if_suffix:
  assumes "suffix Γ' Γ"
  shows "trail_atms Γ' |⊆| trail_atms Γ"
proof -
  obtain Γ⇩0 where "Γ = Γ⇩0 @ Γ'"
    using assms unfolding suffix_def by metis

  show ?thesis
    unfolding ‹Γ = Γ⇩0 @ Γ'›
    by (induction Γ⇩0) auto
qed

lemma dom_model_eq_trail_interp:
  assumes
    "∀A C. ℳ A = Some C ⟷ map_of Γ (Pos A) = Some (Some C)" and
    "∀Ln ∈ set Γ. ∀L. Ln = (L, None) ⟶ is_neg L"
  shows "dom ℳ = trail_interp Γ"
proof -
  have "dom ℳ = {A. ∃C. ℳ A = Some C}"
    unfolding dom_def by simp
  also have "… = {A. ∃C. map_of Γ (Pos A) = Some (Some C)}"
    using assms(1) by metis
  also have "… = {A. ∃opt. map_of Γ (Pos A) = Some opt}"
  proof (rule Collect_cong)
    show "⋀A. (∃C. map_of Γ (Pos A) = Some (Some C)) ⟷ (∃opt. map_of Γ (Pos A) = Some opt)"
      using assms(2)
      by (metis literal.disc(1) map_of_SomeD option.exhaust)
  qed
  also have "… = trail_interp Γ"
  proof (induction Γ)
    case Nil
    thus ?case
      by (simp add: trail_interp_def)
  next
    case (Cons Ln Γ)

    have "{A. ∃opt. map_of (Ln # Γ) (Pos A) = Some opt} =
      {A. ∃opt. map_of [Ln] (Pos A) = Some opt} ∪ {A. ∃opt. map_of Γ (Pos A) = Some opt}"
      by auto

    also have "… = {A. Pos A = fst Ln} ∪ trail_interp Γ"
      unfolding Cons.IH by simp

    also have "… = trail_interp [Ln] ∪ trail_interp Γ"
      by (cases "fst Ln") (simp_all add: trail_interp_def)

    also have "… = trail_interp (Ln # Γ)"
      unfolding trail_interp_Cons[of Ln Γ] ..

    finally show ?case .
  qed
  finally show ?thesis .
qed



type_synonym 'f gliteral = "'f gterm literal"
type_synonym 'f gclause = "'f gterm clause"



locale simulation_SCLFOL_ground_ordered_resolution =
  renaming_apart renaming_vars
  for renaming_vars :: "'v set ⇒ 'v ⇒ 'v" +
  fixes
    less_trm :: "'f gterm ⇒ 'f gterm ⇒ bool" (infix "≺⇩t" 50)
  assumes
    transp_less_trm[simp]: "transp (≺⇩t)" and
    asymp_less_trm[intro]: "asymp (≺⇩t)" and
    wfP_less_trm[intro]: "wfP (≺⇩t)" and
    totalp_less_trm[intro]: "totalp (≺⇩t)" and
    finite_less_trm: "⋀β. finite {x. x ≺⇩t β}" and
    less_trm_compatible_with_gctxt[simp]: "⋀ctxt t t'. t ≺⇩t t' ⟹ ctxt⟨t⟩⇩G ≺⇩t ctxt⟨t'⟩⇩G" and
    less_trm_if_subterm[simp]: "⋀t ctxt. ctxt ≠ □⇩G ⟹ t ≺⇩t ctxt⟨t⟩⇩G"



section ‹Ground ordered resolution for ground terms›

context simulation_SCLFOL_ground_ordered_resolution begin

sublocale ord_res: ground_ordered_resolution_calculus "(≺⇩t)" "λ_. {#}"
  by unfold_locales auto

sublocale linorder_trm: linorder "(≼⇩t)" "(≺⇩t)"
proof unfold_locales
  show "⋀x y. (x ≺⇩t y) = (x ≼⇩t y ∧ ¬ y ≼⇩t x)"
    by (metis asympD asymp_less_trm reflclp_iff)
next
  show "⋀x. x ≼⇩t x"
    by simp
next
  show "⋀x y z. x ≼⇩t y ⟹ y ≼⇩t z ⟹ x ≼⇩t z"
    by (meson transpE transp_less_trm transp_on_reflclp)
next
  show "⋀x y. x ≼⇩t y ⟹ y ≼⇩t x ⟹ x = y"
    by (metis asympD asymp_less_trm reflclp_iff)
next
  show "⋀x y. x ≼⇩t y ∨ y ≼⇩t x"
    by (metis reflclp_iff totalpD totalp_less_trm)
qed

sublocale linorder_lit: linorder "(≼⇩l)" "(≺⇩l)"
proof unfold_locales
  show "⋀x y. (x ≺⇩l y) = (x ≼⇩l y ∧ ¬ y ≼⇩l x)"
    by (metis asympD ord_res.asymp_less_lit reflclp_iff)
next
  show "⋀x. x ≼⇩l x"
    by simp
next
  show "⋀x y z. x ≼⇩l y ⟹ y ≼⇩l z ⟹ x ≼⇩l z"
    by (meson transpE ord_res.transp_less_lit transp_on_reflclp)
next
  show "⋀x y. x ≼⇩l y ⟹ y ≼⇩l x ⟹ x = y"
    by (metis asympD ord_res.asymp_less_lit reflclp_iff)
next
  show "⋀x y. x ≼⇩l y ∨ y ≼⇩l x"
    by (metis reflclp_iff totalpD ord_res.totalp_less_lit)
qed

sublocale linorder_cls: linorder "(≼⇩c)" "(≺⇩c)"
proof unfold_locales
  show "⋀x y. (x ≺⇩c y) = (x ≼⇩c y ∧ ¬ y ≼⇩c x)"
    by (metis asympD ord_res.asymp_less_cls reflclp_iff)
next
  show "⋀x. x ≼⇩c x"
    by simp
next
  show "⋀x y z. x ≼⇩c y ⟹ y ≼⇩c z ⟹ x ≼⇩c z"
    by (meson transpE ord_res.transp_less_cls transp_on_reflclp)
next
  show "⋀x y. x ≼⇩c y ⟹ y ≼⇩c x ⟹ x = y"
    by (metis asympD ord_res.asymp_less_cls reflclp_iff)
next
  show "⋀x y. x ≼⇩c y ∨ y ≼⇩c x"
    by (metis reflclp_iff totalpD ord_res.totalp_less_cls)
qed

declare linorder_trm.is_least_in_fset_ffilterD[no_atp]
declare linorder_lit.is_least_in_fset_ffilterD[no_atp]
declare linorder_cls.is_least_in_fset_ffilterD[no_atp]

end


section ‹Common definitions and lemmas›

context simulation_SCLFOL_ground_ordered_resolution begin

abbreviation ord_res_Interp where
  "ord_res_Interp N C ≡ ord_res.interp N C ∪ ord_res.production N C"

definition is_least_false_clause where
  "is_least_false_clause N C ⟷
    linorder_cls.is_least_in_fset {|C |∈| N. ¬ ord_res_Interp (fset N) C ⊫ C|} C"

lemma is_least_false_clause_finsert_smaller_false_clause:
  assumes
    D_least: "is_least_false_clause N D" and
    "C ≺⇩c D" and
    C_false: "¬ ord_res_Interp (fset (finsert C N)) C ⊫ C"
  shows "is_least_false_clause (finsert C N) C"
  unfolding is_least_false_clause_def linorder_cls.is_least_in_ffilter_iff
proof (intro conjI ballI impI)
  show "C |∈| finsert C N"
    by simp
next
  show "¬ ord_res_Interp (fset (finsert C N)) C ⊫ C"
    using assms by metis
next
  fix y
  assume "y |∈| finsert C N" and "y ≠ C" and y_false: "¬ ord_res_Interp (fset (finsert C N)) y ⊫ y"
  hence "y |∈| N"
    by simp

  have "¬ (y ≺⇩c C)"
  proof (rule notI)
    assume "y ≺⇩c C"
    hence "ord_res_Interp (fset (finsert C N)) y = ord_res_Interp (fset N) y"
      using ord_res.Interp_insert_greater_clause by simp

    hence "¬ ord_res_Interp (fset N) y ⊫ y"
      using y_false by argo

    moreover have "y ≺⇩c D"
      using ‹y ≺⇩c C› ‹C ≺⇩c D› by order

    ultimately show False
      using D_least
      by (metis (mono_tags, lifting) ‹y |∈| N› linorder_cls.is_least_in_ffilter_iff
          linorder_cls.less_asym' is_least_false_clause_def)
  qed
  thus "C ≺⇩c y"
    using ‹y ≠ C› by order
qed

lemma is_least_false_clause_swap_swap_compatible_fsets:
  assumes "{|x |∈| N1. x ≼⇩c C|} = {|x |∈| N2. x ≼⇩c C|}"
  shows "is_least_false_clause N1 C ⟷ is_least_false_clause N2 C"
proof -
  have "is_least_false_clause N2 C" if
    subsets_agree: "{|x |∈| N1. x ≼⇩c C|} = {|x |∈| N2. x ≼⇩c C|}" and
    C_least: "is_least_false_clause N1 C" for N1 N2 C
    unfolding is_least_false_clause_def linorder_cls.is_least_in_ffilter_iff
  proof (intro conjI ballI impI)
    have "C |∈| N1"
      using C_least
      unfolding is_least_false_clause_def linorder_cls.is_least_in_ffilter_iff
      by argo
    thus "C |∈| N2"
      using subsets_agree by auto
  next
    have "¬ ord_res_Interp (fset N1) C ⊫ C"
      using C_least
      unfolding is_least_false_clause_def linorder_cls.is_least_in_ffilter_iff
      by argo
    moreover have "ord_res_Interp (fset N1) C = ord_res_Interp (fset N2) C"
      using subsets_agree by (auto intro!: ord_res.Interp_swap_clause_set) 
    ultimately show "¬ ord_res_Interp (fset N2) C ⊫ C"
      by argo
  next
    fix y assume "y |∈| N2" and "y ≠ C"
    show "¬ ord_res_Interp (fset N2) y ⊫ y ⟹ C ≺⇩c y"
    proof (erule contrapos_np)
      assume "¬ C ≺⇩c y"
      hence "y ≼⇩c C"
        by order
      hence "y |∈| N1"
        using ‹y |∈| N2› using subsets_agree by auto
      hence "¬ ord_res_Interp (fset N1) y ⊫ y ⟶ C ≺⇩c y"
        using ‹is_least_false_clause N1 C› ‹y ≠ C›
        unfolding is_least_false_clause_def linorder_cls.is_least_in_ffilter_iff
        by metis
      moreover have "ord_res_Interp (fset N1) y = ord_res_Interp (fset N2) y"
      proof (rule ord_res.Interp_swap_clause_set)
        show "{D. D |∈| N1 ∧ (≺⇩c)⇧=⇧= D y} = {D. D |∈| N2 ∧ (≺⇩c)⇧=⇧= D y}"
          using subsets_agree ‹y ≼⇩c C› by fastforce
      qed
      ultimately show "ord_res_Interp (fset N2) y ⊫ y"
        using ‹y ≼⇩c C› by auto
    qed
  qed
  thus ?thesis
    using assms by metis
qed

lemma Uniq_is_least_false_clause: "∃⇩≤⇩1 C. is_least_false_clause N C"
proof (rule Uniq_I)
  show "⋀x y z. is_least_false_clause x y ⟹ is_least_false_clause x z ⟹ y = z"
    unfolding is_least_false_clause_def
    by (meson Uniq_D linorder_cls.Uniq_is_least_in_fset)
qed

lemma mempty_lesseq_cls[simp]: "{#} ≼⇩c C" for C
  by (cases C) (simp_all add: strict_subset_implies_multp)

lemma is_least_false_clause_mempty: "{#} |∈| N ⟹ is_least_false_clause N {#}"
  using is_least_false_clause_def linorder_cls.is_least_in_ffilter_iff mempty_lesseq_cls
  by fastforce

lemma production_union_unproductive_strong:
  assumes
    fin: "finite N1" "finite N2" and
    N2_unproductive: "∀x ∈ N2 - N1. ord_res.production (N1 ∪ N2) x = {}" and
    C_in: "C ∈ N1"
  shows "ord_res.production (N1 ∪ N2) C = ord_res.production N1 C"
  using ord_res.wfP_less_cls C_in
proof (induction C rule: wfp_induct_rule)
  case (less C)
  hence C_in_iff: "C ∈ N1 ∪ N2 ⟷ C ∈ N1"
    by simp

  have interp_eq: "ord_res.interp (N1 ∪ N2) C = ord_res.interp N1 C"
  proof -
    have "ord_res.interp (N1 ∪ N2) C = ⋃ (ord_res.production (N1 ∪ N2) ` {D ∈ N1 ∪ N2. D ≺⇩c C})"
      unfolding ord_res.interp_def ..
    also have "… = ⋃ (ord_res.production (N1 ∪ N2) ` {D ∈ N1. D ≺⇩c C} ∪
    ord_res.production (N1 ∪ N2) ` {D ∈ N2 - N1. D ≺⇩c C})"
      by auto
    also have "… = ⋃ (ord_res.production (N1 ∪ N2) ` {D ∈ N1. D ≺⇩c C})"
      using N2_unproductive by simp
    also have "… = ⋃ (ord_res.production N1 ` {D ∈ N1. D ≺⇩c C})"
      using less.IH by simp
    also have "… = ord_res.interp N1 C"
      unfolding ord_res.interp_def ..
    finally show "ord_res.interp (N1 ∪ N2) C = ord_res.interp N1 C" .
  qed

  show ?case
    unfolding ord_res.production_unfold C_in_iff interp_eq by argo
qed

lemma production_union_unproductive:
  assumes
    fin: "finite N1" "finite N2" and
    N2_unproductive: "∀x ∈ N2. ord_res.production (N1 ∪ N2) x = {}" and
    C_in: "C ∈ N1"
  shows "ord_res.production (N1 ∪ N2) C = ord_res.production N1 C"
  using production_union_unproductive_strong assms by simp

lemma interp_union_unproductive:
  assumes
    fin: "finite N1" "finite N2" and
    N2_unproductive: "∀x ∈ N2. ord_res.production (N1 ∪ N2) x = {}"
  shows "ord_res.interp (N1 ∪ N2) = ord_res.interp N1"
proof (rule ext)
  fix C
  have "ord_res.interp (N1 ∪ N2) C = ⋃ (ord_res.production (N1 ∪ N2) ` {D ∈ N1 ∪ N2. D ≺⇩c C})"
    unfolding ord_res.interp_def ..
  also have "… = ⋃ (ord_res.production (N1 ∪ N2) ` {D ∈ N1. D ≺⇩c C} ∪
    ord_res.production (N1 ∪ N2) ` {D ∈ N2. D ≺⇩c C})"
    by auto
  also have "… = ⋃ (ord_res.production (N1 ∪ N2) ` {D ∈ N1. D ≺⇩c C})"
    using N2_unproductive by simp
  also have "… = ⋃ (ord_res.production N1 ` {D ∈ N1. D ≺⇩c C})"
    using production_union_unproductive[OF fin N2_unproductive] by simp
  also have "… = ord_res.interp N1 C"
    unfolding ord_res.interp_def ..
  finally show "ord_res.interp (N1 ∪ N2) C = ord_res.interp N1 C" .
qed

lemma Interp_union_unproductive:
  assumes
    fin: "finite N1" "finite N2" and
    N2_unproductive: "∀x ∈ N2. ord_res.production (N1 ∪ N2) x = {}"
  shows "ord_res_Interp (N1 ∪ N2) C = ord_res_Interp N1 C"
  unfolding interp_union_unproductive[OF assms]
  using production_union_unproductive[OF assms]
  using N2_unproductive[rule_format]
  by (metis (no_types, lifting) Un_iff empty_Collect_eq ord_res.production_unfold)

lemma Interp_insert_unproductive:
  assumes
    fin: "finite N1" and
    x_unproductive: "ord_res.production (insert x N1) x = {}"
  shows "ord_res_Interp (insert x N1) C = ord_res_Interp N1 C"
  using assms Interp_union_unproductive
  by (metis Un_commute finite.emptyI finite.insertI insert_is_Un singletonD)

lemma extended_partial_model_entails_iff_partial_model_entails:
  assumes
    fin: "finite N" "finite N'" and
    irrelevant: "∀D ∈ N'. ∃E ∈ N. E ⊂# D ∧ set_mset D = set_mset E" and
    C_in: "C ∈ N"
  shows "ord_res_Interp (N ∪ N') C ⊫ C ⟷ ord_res_Interp N C ⊫ C"
  using ord_res.interp_add_irrelevant_clauses_to_set[OF fin C_in irrelevant]
  using ord_res.production_add_irrelevant_clauses_to_set[OF fin C_in irrelevant]
  by metis

lemma nex_strictly_maximal_pos_lit_if_factorizable:
  assumes "ord_res.ground_factoring C C'"
  shows "∄L. is_pos L ∧ ord_res.is_strictly_maximal_lit L C"
  by (metis Uniq_D add_mset_remove_trivial assms linorder_lit.Uniq_is_maximal_in_mset
      linorder_lit.dual_order.order_iff_strict linorder_lit.is_greatest_in_mset_iff
      linorder_lit.is_maximal_in_mset_if_is_greatest_in_mset linorder_lit.not_less
      ord_res.ground_factoring.cases union_single_eq_member)

lemma unproductive_if_nex_strictly_maximal_pos_lit:
  assumes "∄L. is_pos L ∧ ord_res.is_strictly_maximal_lit L C"
  shows "ord_res.production N C = {}"
  using assms by (simp add: ord_res.production_unfold)

lemma ball_unproductive_if_nex_strictly_maximal_pos_lit:
  assumes "∀C ∈ N'. ∄L. is_pos L ∧ ord_res.is_strictly_maximal_lit L C"
  shows "∀C ∈ N'. ord_res.production (N ∪ N') C = {}"
  using assms unproductive_if_nex_strictly_maximal_pos_lit by metis

lemma is_least_false_clause_finsert_cancel:
  assumes
    C_unproductive: "ord_res.production (fset (finsert C N)) C = {}" and
    C_entailed_by_smaller: "∃D |∈| N. D ≺⇩c C ∧ {D} ⊫e {C}"
  shows "is_least_false_clause (finsert C N) = is_least_false_clause N"
proof (intro ext iffI)
  fix E
  assume E_least: "is_least_false_clause (finsert C N) E"
  hence
    E_in: "E |∈| finsert C N" and
    E_false: "¬ ord_res_Interp (fset (finsert C N)) E ⊫ E" and
    E_least: "(∀y |∈| finsert C N. y ≠ E ⟶ ¬ ord_res_Interp (fset (finsert C N)) y ⊫ y ⟶ E ≺⇩c y)"
    unfolding atomize_conj is_least_false_clause_def linorder_cls.is_least_in_ffilter_iff
    by metis

  obtain D where
    "D |∈| N" and "D ≺⇩c C" and "{D} ⊫e {C}"
    using C_entailed_by_smaller by metis

  show "is_least_false_clause N E"
  proof (cases "C = E")
    case True

    have "E ≺⇩c D"
    proof (rule E_least[rule_format])
      show "D |∈| finsert C N"
        using ‹D |∈| N› by simp
    next
      show "D ≠ E"
        using ‹D ≺⇩c C› ‹C = E› by order
    next
      show "¬ ord_res_Interp (fset (finsert C N)) D ⊫ D"
        using E_false
      proof (rule contrapos_nn)
        assume "ord_res_Interp (fset (finsert C N)) D ⊫ D"
        thus "ord_res_Interp (fset (finsert C N)) E ⊫ E"
          using ‹D ≺⇩c C› ‹C = E› ‹{D} ⊫e {C}› ord_res.entailed_clause_stays_entailed by auto
      qed
    qed
    hence False
      using ‹D ≺⇩c C› ‹C = E› by order
    thus ?thesis ..
  next
    case False
    show ?thesis
      unfolding is_least_false_clause_def linorder_cls.is_least_in_ffilter_iff
    proof (intro conjI ballI impI)
      show "E |∈| N"
        using E_in ‹C ≠ E› by simp
    next
      have "ord_res_Interp (fset (finsert C N)) E = ord_res_Interp (fset N) E"
        using C_unproductive Interp_insert_unproductive by simp
      thus "¬ ord_res_Interp (fset N) E ⊫ E"
        using E_false by argo
    next
      show "⋀y. y |∈| N ⟹ y ≠ E ⟹ ¬ ord_res_Interp (fset N) y ⊫ y ⟹ E ≺⇩c y"
        using E_least C_unproductive Interp_insert_unproductive by auto
    qed
  qed
next
  fix E
  assume "is_least_false_clause N E"
  hence
    E_in: "E |∈| N" and
    E_false: "¬ ord_res_Interp (fset N) E ⊫ E" and
    E_least: "(∀y |∈| N. y ≠ E ⟶ ¬ ord_res_Interp (fset N) y ⊫ y ⟶ E ≺⇩c y)"
    unfolding atomize_conj is_least_false_clause_def linorder_cls.is_least_in_ffilter_iff
    by metis

  show "is_least_false_clause (finsert C N) E"
    unfolding is_least_false_clause_def linorder_cls.is_least_in_ffilter_iff
  proof (intro conjI ballI impI)
    show "E |∈| finsert C N"
      using E_in by simp
  next
    show "¬ ord_res_Interp (fset (finsert C N)) E ⊫ E"
      using E_least E_false C_unproductive Interp_insert_unproductive by simp
  next
    fix y
    assume "y |∈| finsert C N" and "y ≠ E" and "¬ ord_res_Interp (fset (finsert C N)) y ⊫ y"
    show "E ≺⇩c y"
    proof (cases "y = C")
      case True
      thus ?thesis
      using E_least ‹¬ ord_res_Interp (fset (finsert C N)) y ⊫ y›
      by (metis (no_types, lifting) C_entailed_by_smaller C_unproductive Interp_insert_unproductive
          finite_fset fset_simps(2) linorder_cls.dual_order.strict_trans
          ord_res.entailed_clause_stays_entailed true_clss_singleton)
    next
      case False
      thus ?thesis
        using E_least ‹y |∈| finsert C N› ‹y ≠ E› ‹¬ ord_res_Interp (fset (finsert C N)) y ⊫ y›
        using C_unproductive Interp_insert_unproductive by auto
    qed
  qed
qed

lemma is_least_false_clause_funion_cancel_right_strong:
  assumes
    "∀C |∈| N2 - N1. ∀U. ord_res.production U C = {}" and
    "∀C |∈| N2 - N1. ∃D |∈| N1. D ≺⇩c C ∧ {D} ⊫e {C}"
  shows "is_least_false_clause (N1 |∪| N2) = is_least_false_clause N1"
  using assms
proof (induction N2)
  case empty
  thus ?case
    by simp
next
  case (insert C N2)

  have IH: "is_least_false_clause (N1 |∪| N2) = is_least_false_clause N1"
  proof (rule insert.IH)
    show "∀C|∈|N2 |-| N1. ∀U. ord_res.production U C = {}"
      using insert.prems(1) by auto
  next
    show "∀C|∈|N2 |-| N1. ∃D|∈|N1. D ≺⇩c C ∧ {D} ⊫e {C}"
      using insert.prems(2) by auto
  qed

  show ?case
  proof (cases "C |∈| N1")
    case True
    hence "is_least_false_clause (N1 |∪| finsert C N2) = is_least_false_clause (N1 |∪| N2)"
      by (simp add: finsert_absorb)
    also have "… = is_least_false_clause N1"
      using IH .
    finally show ?thesis .
  next
    case False
    then show ?thesis
      using is_least_false_clause_finsert_cancel IH
      by (metis finsertCI fminusI funionI1 funion_finsert_right insert.prems(1) insert.prems(2))
  qed
qed

lemma is_least_false_clause_funion_cancel_right:
  assumes
    "∀C |∈| N2. ∀U. ord_res.production U C = {}" and
    "∀C |∈| N2. ∃D |∈| N1. D ≺⇩c C ∧ {D} ⊫e {C}"
  shows "is_least_false_clause (N1 |∪| N2) = is_least_false_clause N1"
  using assms is_least_false_clause_funion_cancel_right_strong by simp

definition ex_false_clause where
  "ex_false_clause N = (∃C ∈ N. ¬ ord_res.interp N C ∪ ord_res.production N C ⊫ C)"

lemma obtains_least_false_clause_if_ex_false_clause:
  assumes "ex_false_clause (fset N)"
  obtains C where "is_least_false_clause N C"
  using assms
  by (metis (mono_tags, lifting) bot_fset.rep_eq emptyE ex_false_clause_def ffmember_filter
      linorder_cls.ex_least_in_fset is_least_false_clause_def)

lemma ex_false_clause_if_least_false_clause:
  assumes "is_least_false_clause N C"
  shows "ex_false_clause (fset N)"
  using assms
  by (metis (no_types, lifting) ex_false_clause_def is_least_false_clause_def
      linorder_cls.is_least_in_fset_ffilterD(1) linorder_cls.is_least_in_fset_ffilterD(2))

lemma ex_false_clause_iff: "ex_false_clause (fset N) ⟷ (∃C. is_least_false_clause N C)"
  using obtains_least_false_clause_if_ex_false_clause ex_false_clause_if_least_false_clause by metis

definition ord_res_model where
  "ord_res_model N = (⋃D ∈ N. ord_res.production N D)"

lemma ord_res_model_eq_interp_union_production_of_greatest_clause:
  assumes C_greatest: "linorder_cls.is_greatest_in_set N C"
  shows "ord_res_model N = ord_res.interp N C ∪ ord_res.production N C"
proof -
  have "ord_res_model N = (⋃D ∈ N. ord_res.production N D)"
    unfolding ord_res_model_def ..
  also have "… = (⋃D ∈ {D ∈ N. D ≼⇩c C}. ord_res.production N D)"
    using C_greatest linorder_cls.is_greatest_in_set_iff by auto
  also have "… = (⋃D ∈ {D ∈ N. D ≺⇩c C} ∪ {C}. ord_res.production N D)"
    using C_greatest linorder_cls.is_greatest_in_set_iff by auto
  also have "… = (⋃D ∈ {D ∈ N. D ≺⇩c C}. ord_res.production N D) ∪ ord_res.production N C"
    by auto
  also have "… = ord_res.interp N C ∪ ord_res.production N C"
    unfolding ord_res.interp_def ..
  finally show ?thesis .
qed

lemma ord_res_model_entails_clauses_if_nex_false_clause:
  assumes "finite N" and "N ≠ {}" and "¬ ex_false_clause N"
  shows "ord_res_model N ⊫s N"
  unfolding true_clss_def
proof (intro ballI)
  from ‹¬ ex_false_clause N› have ball_true:
    "∀C ∈ N. ord_res.interp N C ∪ ord_res.production N C ⊫ C"
    by (simp add: ex_false_clause_def)

  from ‹finite N› ‹N ≠ {}› obtain D where
    D_greatest: "linorder_cls.is_greatest_in_set N D"
    using linorder_cls.ex_greatest_in_set by metis

  fix C assume "C ∈ N"
  hence "ord_res.interp N C ∪ ord_res.production N C ⊫ C"
    using ball_true by metis

  moreover have "C ≼⇩c D"
    using ‹C ∈ N› D_greatest[unfolded linorder_cls.is_greatest_in_set_iff] by auto

  ultimately have "ord_res.interp N D ∪ ord_res.production N D ⊫ C"
    using ord_res.entailed_clause_stays_entailed by auto

  thus "ord_res_model N ⊫ C"
    using ord_res_model_eq_interp_union_production_of_greatest_clause[OF D_greatest] by argo
qed

lemma pos_lit_not_greatest_if_maximal_in_least_false_clause:
  assumes
    C_least: "linorder_cls.is_least_in_fset {|C |∈| N. ¬ ord_res_Interp (fset N) C ⊫ C|} C" and
    C_max_lit: "ord_res.is_maximal_lit (Pos A) C"
  shows "¬ ord_res.is_strictly_maximal_lit (Pos A) C"
proof -
  from C_max_lit obtain C' where C_def: "C = add_mset (Pos A) C'"
    by (meson linorder_lit.is_maximal_in_mset_iff mset_add)

  from C_least have
    C_in: "C |∈| N" and
    C_false: "¬ ord_res_Interp (fset N) C ⊫ C" and
    C_lt: "∀y |∈| N. y ≠ C ⟶ ¬ ord_res_Interp (fset N) y ⊫ y ⟶ C ≺⇩c y"
    unfolding linorder_cls.is_least_in_ffilter_iff by auto

  have "∄A. A ∈ ord_res.production (fset N) C"
  proof (rule notI, elim exE)
    fix A assume A_in: "A ∈ ord_res.production (fset N) C"
    have "Pos A ∈# C"
      using A_in by (auto elim: ord_res.mem_productionE)
    moreover have "A ∈ ord_res_Interp (fset N) C"
      using A_in C_in by blast
    ultimately show False
      using C_false by auto
  qed
  hence C_unproductive: "ord_res.production (fset N) C = {}"
    using ord_res.production_eq_empty_or_singleton[of "fset N" C] by simp

  have "{D ∈ fset N. D ≼⇩c C} = {D ∈ fset N. D ≺⇩c C} ∪ {D ∈ fset N. D = C}"
    by fastforce
  with C_unproductive have
    "ord_res_Interp (fset N) C = ord_res.interp (fset N) C"
    by simp
  with C_false have C_false': "¬ ord_res.interp (fset N) C ⊫ C"
    by simp

  from C_unproductive have "A ∉ ord_res.production (fset N) C"
    by simp
  thus ?thesis
  proof (rule contrapos_nn)
    assume "ord_res.is_strictly_maximal_lit (Pos A) C"
    then show "A ∈ ord_res.production (fset N) C"
      unfolding ord_res.production_unfold[of "fset N" C] mem_Collect_eq
      using C_in C_def C_false'
      by metis
  qed
qed

lemma ex_ground_factoringI:
  assumes
    C_max_lit: "ord_res.is_maximal_lit (Pos A) C" and
    C_not_max_lit: "¬ ord_res.is_strictly_maximal_lit (Pos A) C"
  shows "∃C'. ord_res.ground_factoring C C'"
proof -
  from C_max_lit C_not_max_lit have "count C (Pos A) ≥ 2"
    using linorder_lit.count_ge_2_if_maximal_in_mset_and_not_greatest_in_mset by metis
  then obtain C' where C_def: "C = add_mset (Pos A) (add_mset (Pos A) C')"
    by (metis two_le_countE)

  show ?thesis
  proof (rule exI)
    show "ord_res.ground_factoring C (add_mset (Pos A) C')"
      using ord_res.ground_factoringI[of C A C']
      using C_def C_max_lit by metis
  qed
qed

lemma true_cls_if_true_lit_in: "L ∈# C ⟹ I ⊫l L ⟹ I ⊫ C"
  by auto

lemma bex_smaller_productive_clause_if_least_false_clause_has_negative_max_lit:
  assumes
    C_least_false: "is_least_false_clause N C" and
    Neg_A_max: "ord_res.is_maximal_lit (Neg A) C"
  shows "fBex N (λD. D ≺⇩c C ∧ ord_res.is_strictly_maximal_lit (Pos A) D ∧
    ord_res.production (fset N) D = {A})"
proof -
  from C_least_false have
    C_in: "C |∈| N" and
    C_false: "¬ ord_res_Interp (fset N) C ⊫ C" and
    C_min: "∀y |∈| N. y ≠ C ⟶ ¬ ord_res_Interp (fset N) y ⊫ y ⟶ C ≺⇩c y"
    unfolding atomize_conj is_least_false_clause_def
    unfolding linorder_cls.is_least_in_ffilter_iff
    by argo

  have "∄A. A ∈ ord_res.production (fset N) C"
  proof (rule notI, elim exE)
    fix A assume A_in: "A ∈ ord_res.production (fset N) C"
    have "Pos A ∈# C"
      using A_in by (auto elim: ord_res.mem_productionE)
    moreover have "A ∈ ord_res_Interp (fset N) C"
      using A_in C_in by blast
    ultimately show False
      using C_false by auto
  qed
  hence C_unproductive: "ord_res.production (fset N) C = {}"
    using ord_res.production_eq_empty_or_singleton[of "fset N" C] by simp

  from Neg_A_max have "Neg A ∈# C"
    by (simp add: linorder_lit.is_maximal_in_mset_iff)

  from C_false have "¬ ord_res_Interp (fset N) C ⊫l Neg A"
    using true_cls_if_true_lit_in[OF ‹Neg A ∈# C›]
    by meson
  hence "A ∈ ord_res_Interp (fset N) C"
    by simp
  with C_unproductive have "A ∈ ord_res.interp (fset N) C"
    by blast
  then obtain D where
    D_in: "D |∈| N" and D_lt_C: "D ≺⇩c C" and D_productive: "A ∈ ord_res.production (fset N) D"
    unfolding ord_res.interp_def by auto

  from D_productive have "ord_res.is_strictly_maximal_lit (Pos A) D"
    using ord_res.mem_productionE by metis

  moreover have "ord_res.production (fset N) D = {A}"
    using D_productive ord_res.production_eq_empty_or_singleton by fastforce

  ultimately show ?thesis
    using D_in D_lt_C by metis
qed

lemma bex_smaller_productive_clause_if_least_false_clause_has_negative_max_lit':
  assumes
    C_least_false: "is_least_false_clause N C" and
    L_max: "ord_res.is_maximal_lit L C" and
    L_neg: "is_neg L"
  shows "fBex N (λD. D ≺⇩c C ∧ ord_res.is_strictly_maximal_lit (- L) D ∧
    ord_res.production (fset N) D = {atm_of L})"
  using bex_smaller_productive_clause_if_least_false_clause_has_negative_max_lit[OF C_least_false]
  by (simp add: L_max L_neg uminus_literal_def)

lemma ex_ground_resolutionI:
  assumes
    C_max_lit: "ord_res.is_maximal_lit (Neg A) C" and
    D_lt: "D ≺⇩c C" and
    D_max_lit: "ord_res.is_strictly_maximal_lit (Pos A) D"
  shows "∃CD. ord_res.ground_resolution C D CD"
proof -
  from C_max_lit obtain C' where C_def: "C = add_mset (Neg A) C'"
    by (meson linorder_lit.is_maximal_in_mset_iff mset_add)

  from D_max_lit obtain D' where D_def: "D = add_mset (Pos A) D'"
    by (meson linorder_lit.is_greatest_in_mset_iff mset_add)

  show ?thesis
  proof (rule exI)
    show "ord_res.ground_resolution C D (C' + D')"
      using ord_res.ground_resolutionI[of C A C' D D']
      using C_def D_def D_lt C_max_lit D_max_lit by metis
  qed
qed

lemma
  fixes N N'
  assumes
    fin: "finite N" "finite N'" and
    irrelevant: "∀D ∈ N'. ∃E ∈ N. E ⊂# D ∧ set_mset D = set_mset E" and
    C_in: "C ∈ N" and
    C_not_entailed: "¬ ord_res.interp N C ∪ ord_res.production N C ⊫ C"
  shows "¬ ord_res.interp (N ∪ N') C ∪ ord_res.production (N ∪ N') C ⊫ C"
  using C_not_entailed
proof (rule contrapos_nn)
  assume "ord_res.interp (N ∪ N') C ∪ ord_res.production (N ∪ N') C ⊫ C"
  then show "ord_res.interp N C ∪ ord_res.production N C ⊫ C"
    using ord_res.interp_add_irrelevant_clauses_to_set[OF fin C_in irrelevant]
    using ord_res.production_add_irrelevant_clauses_to_set[OF fin C_in irrelevant]
    by metis
qed

lemma trail_consistent_if_sorted_wrt_atoms:
  assumes "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ"
  shows "trail_consistent Γ"
  using assms
proof (induction Γ)
  case Nil
  show ?case
    by simp
next
  case (Cons Ln Γ)

  obtain L opt where
    "Ln = (L, opt)"
    by fastforce

  show ?case
    unfolding ‹Ln = (L, opt)›
  proof (rule trail_consistent.Cons)
    have "∀x∈set Γ. atm_of (fst x) ≺⇩t atm_of (fst Ln)"
      using Cons.prems by simp

    hence "∀x∈set Γ. atm_of (fst x) ≠ atm_of L"
      unfolding ‹Ln = (L, opt)› by fastforce

    thus "¬ trail_defined_lit Γ L"
      unfolding trail_defined_lit_def by fastforce
  next
    show "trail_consistent Γ"
      using Cons by simp
  qed
qed


lemma mono_atms_lt: "monotone_on (set Γ) (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) (λx y. y ≤ x)
  (λx. atm_of K ≼⇩t atm_of (fst x))" for K
proof (intro monotone_onI, unfold le_bool_def, intro impI)
  fix x y
  assume "atm_of (fst y) ≺⇩t atm_of (fst x)" and "atm_of K ≼⇩t atm_of (fst y)"
  thus "atm_of K ≼⇩t atm_of (fst x)"
    by order
qed

lemma in_trail_atms_dropWhileI:
  assumes
    "sorted_wrt R Γ" and
    "monotone_on (set Γ) R (≥) (λx. P (atm_of (fst x)))" and
    "¬ P A" and
    "A |∈| trail_atms Γ"
  shows "A |∈| trail_atms (dropWhile (λLn. P (atm_of (fst Ln))) Γ)"
  using assms(1,2,4)
proof (induction Γ)
  case Nil
  thus ?case
    by simp
next
  case (Cons Ln Γ)
  show ?case
  proof (cases "P (atm_of (fst Ln))")
    case True

    have "A |∈| trail_atms (dropWhile (λLn. P (atm_of (fst Ln))) Γ)"
    proof (rule Cons.IH)
      show "sorted_wrt R Γ"
        using Cons.prems(1) by simp
    next
      show "monotone_on (set Γ) R (λx y. y ≤ x) (λx. P (atm_of (fst x)))"
        using Cons.prems(2) by (meson monotone_on_subset set_subset_Cons)
    next
      have "¬ P A"
        using assms by metis
      hence "A ≠ atm_of (fst Ln)"
        using True by metis
      moreover have "A |∈| trail_atms (Ln # Γ)"
        using Cons.prems(3) by metis
      ultimately show "A |∈| trail_atms Γ"
        by (simp add: trail_defined_lit_def)
    qed

    thus ?thesis
      using True by simp
  next
    case False
    thus ?thesis
      using Cons.prems(3) by simp
  qed
qed

lemma trail_defined_lit_dropWhileI:
  assumes
    "sorted_wrt R Γ" and
    "monotone_on (set Γ) R (≥) (λx. P (fst x))" and
    "¬ P L ∧ ¬ P (- L)" and
    "trail_defined_lit Γ L"
  shows "trail_defined_lit (dropWhile (λLn. P (fst Ln)) Γ) L"
  using assms in_trail_atms_dropWhileI
  by (smt (verit) imageE image_eqI mem_set_dropWhile_conv_if_list_sorted_and_pred_monotone
      trail_defined_lit_def trail_defined_lit_iff_trail_defined_atm)

lemma trail_defined_cls_dropWhileI:
  assumes
    "sorted_wrt R Γ" and
    "monotone_on (set Γ) R (≥) (λx. P (fst x))" and
    "∀L ∈# C. ¬ P L ∧ ¬ P (- L)" and
    "trail_defined_cls Γ C"
  shows "trail_defined_cls (dropWhile (λLn. P (fst Ln)) Γ) C"
  using assms trail_defined_lit_dropWhileI
  by (metis trail_defined_cls_def)

lemma nbex_less_than_least_in_fset: "¬ (∃w |∈| X. w ≺⇩c x)"
  if "linorder_cls.is_least_in_fset X x" for X x
  using that unfolding linorder_cls.is_least_in_fset_iff by auto

lemma clause_le_if_lt_least_greater:
  fixes N U⇩e⇩r ℱ C D
  defines
    "𝒞 ≡ The_optional (linorder_cls.is_least_in_fset (ffilter ((≺⇩c) D) N))"
  assumes
    C_lt: "⋀E. 𝒞 = Some E ⟹ C ≺⇩c E" and
    C_in: "C |∈| N"
  shows "C ≼⇩c D"
proof (cases 𝒞)
  case None

  hence "¬ (∃E. linorder_cls.is_least_in_fset (ffilter ((≺⇩c) D) N) E)"
    using 𝒞_def
    by (metis None_eq_The_optionalD Uniq_D linorder_cls.Uniq_is_least_in_fset)

  hence "¬ (∃E |∈| N. D ≺⇩c E)"
    by (metis femptyE ffmember_filter linorder_cls.ex1_least_in_fset)

  thus ?thesis
    using C_in linorder_cls.less_linear by blast
next
  case (Some E)

  hence "linorder_cls.is_least_in_fset (ffilter ((≺⇩c) D) N) E"
    using 𝒞_def by (metis Some_eq_The_optionalD)

  hence "C ≺⇩c D ∨ C = D"
    by (metis C_in C_lt Some ffmember_filter linorder_cls.neqE nbex_less_than_least_in_fset)

  thus ?thesis
    by simp
qed

end


section ‹Lemmas about going between ground and first-order terms›

context simulation_SCLFOL_ground_ordered_resolution begin

lemma ex1_gterm_of_term:
  fixes t :: "'f gterm"
  shows "∃!(t' :: ('f, 'v) term). ground t' ∧ t = gterm_of_term t'"
proof (rule ex1I)
  show "ground (term_of_gterm t) ∧ t = gterm_of_term (term_of_gterm t)"
    by simp
next
  fix t' :: "('f, 'v) term"
  show "ground t' ∧ t = gterm_of_term t' ⟹ t' = term_of_gterm t"
    by (induction t') (simp_all add: map_idI)
qed

lemma binj_betw_gterm_of_term: "bij_betw gterm_of_term {t. ground t} UNIV"
  unfolding bij_betw_def
proof (rule conjI)
  show "inj_on gterm_of_term {t. ground t}"
    by (metis gterm_of_term_inj mem_Collect_eq)
next
  show "gterm_of_term ` {t. ground t} = UNIV"
  proof (rule Set.subset_antisym)
    show "gterm_of_term ` {t. Term_Context.ground t} ⊆ UNIV"
      by simp
  next
    show "UNIV ⊆ gterm_of_term ` {t. Term_Context.ground t}"
      by (metis (mono_tags, opaque_lifting) ground_term_of_gterm image_iff mem_Collect_eq subsetI
          term_of_gterm_inv)
  qed
qed

end


section ‹SCL(FOL) for first-order terms›

context simulation_SCLFOL_ground_ordered_resolution begin

definition less_B where
  "less_B x y ⟷ ground x ∧ ground y ∧ gterm_of_term x ≺⇩t gterm_of_term y"

sublocale order_less_B: order "less_B⇧=⇧=" less_B
  by unfold_locales (auto simp add: less_B_def)

sublocale scl_fol: scl_fol_calculus renaming_vars less_B
proof unfold_locales
  fix β :: "('f, 'v) term"

  have Collect_gterms_eq: "⋀P. {y. P y} = gterm_of_term ` {t. ground t ∧ P (gterm_of_term t)}"
    using Collect_eq_image_filter_Collect_if_bij_betw[OF binj_betw_gterm_of_term subset_UNIV]
    by auto

  have "{t⇩G. t⇩G ≺⇩t gterm_of_term β} = gterm_of_term ` {x. ground x ∧ gterm_of_term x ≺⇩t gterm_of_term β}"
    using Collect_gterms_eq[of "λt⇩G. t⇩G ≺⇩t gterm_of_term β"] .
  hence "finite (gterm_of_term ` {x. ground x ∧ gterm_of_term x ≺⇩t gterm_of_term β})"
    using finite_less_trm[of "gterm_of_term β"] by metis
  moreover have "inj_on gterm_of_term {x. ground x ∧ gterm_of_term x ≺⇩t gterm_of_term β}"
    by (rule gterm_of_term_inj) simp
  ultimately have "finite {x. ground x ∧ gterm_of_term x ≺⇩t gterm_of_term β}"
    using finite_imageD by blast
  thus "finite {x. less_B x β}"
    unfolding less_B_def
    using not_finite_existsD by force
qed

end


lemma trail_atms_eq_trail_atms_if_same_lits:
  assumes "list_all2 (λx y. fst x = fst y) Γ⇩9 Γ⇩1⇩0"
  shows "trail_atms Γ⇩9 = trail_atms Γ⇩1⇩0"
  using assms
proof (induction Γ⇩9 Γ⇩1⇩0 rule: list.rel_induct)
  case Nil
  show ?case
    by (simp add: trail_atms_def)
next
  case (Cons Ln⇩9 Γ⇩9' Ln⇩1⇩0 Γ⇩1⇩0')
  thus ?case
    by (simp add: trail_atms_def)
qed

lemma trail_false_lit_eq_trail_false_lit_if_same_lits:
  assumes "list_all2 (λx y. fst x = fst y) Γ⇩9 Γ⇩1⇩0"
  shows "trail_false_lit Γ⇩9 = trail_false_lit Γ⇩1⇩0"
  using assms
proof (induction Γ⇩9 Γ⇩1⇩0 rule: list.rel_induct)
  case Nil
  show ?case
    by (simp add: trail_false_lit_def)
next
  case (Cons Ln⇩9 Γ⇩9' Ln⇩1⇩0 Γ⇩1⇩0')
  thus ?case
    unfolding trail_false_lit_def
    unfolding list.set image_insert
    by (metis insert_iff)
qed

lemma trail_false_cls_eq_trail_false_cls_if_same_lits:
  assumes "list_all2 (λx y. fst x = fst y) Γ⇩9 Γ⇩1⇩0"
  shows "trail_false_cls Γ⇩9 = trail_false_cls Γ⇩1⇩0"
  unfolding trail_false_cls_def 
  unfolding trail_false_lit_eq_trail_false_lit_if_same_lits[OF assms] ..

lemma trail_defined_lit_eq_trail_defined_lit_if_same_lits:
  assumes "list_all2 (λx y. fst x = fst y) Γ⇩9 Γ⇩1⇩0"
  shows "trail_defined_lit Γ⇩9 = trail_defined_lit Γ⇩1⇩0"
  using assms
proof (induction Γ⇩9 Γ⇩1⇩0 rule: list.rel_induct)
  case Nil
  show ?case
    by (simp add: trail_defined_lit_def)
next
  case (Cons Ln⇩9 Γ⇩9' Ln⇩1⇩0 Γ⇩1⇩0')
  thus ?case
    unfolding trail_defined_lit_def
    unfolding list.set image_insert
    by (metis (no_types, opaque_lifting) insert_iff)
qed

lemma trail_defined_cls_eq_trail_defined_cls_if_same_lits:
  assumes "list_all2 (λx y. fst x = fst y) Γ⇩9 Γ⇩1⇩0"
  shows "trail_defined_cls Γ⇩9 = trail_defined_cls Γ⇩1⇩0"
  unfolding trail_defined_cls_def
  unfolding trail_defined_lit_eq_trail_defined_lit_if_same_lits[OF assms] ..

end