Theory Weighted_FO_Ordered_Resolution_Prover

theory Weighted_FO_Ordered_Resolution_Prover
imports FO_Ordered_Resolution_Prover
(*  Title:       A Fair Ordered Resolution Prover for First-Order Clauses with Weights
    Author:      Anders Schlichtkrull <andschl at dtu.dk>, 2017
    Author:      Jasmin Blanchette <j.c.blanchette at vu.nl>, 2017
    Maintainer:  Anders Schlichtkrull <andschl at dtu.dk>
*)

section ‹A Fair Ordered Resolution Prover for First-Order Clauses with Weights›

text ‹
The ‹weighted_RP› prover introduced below operates on finite multisets of clauses and
organizes the multiset of processed clauses as a priority queue to ensure that inferences are
performed in a fair manner, to guarantee completeness.
›

theory Weighted_FO_Ordered_Resolution_Prover
  imports Ordered_Resolution_Prover.FO_Ordered_Resolution_Prover
begin

type_synonym 'a wclause = "'a clause × nat"
type_synonym 'a wstate = "'a wclause multiset × 'a wclause multiset × 'a wclause multiset × nat"

fun state_of_wstate :: "'a wstate ⇒ 'a state" where
  "state_of_wstate (N, P, Q, n) =
   (set_mset (image_mset fst N), set_mset (image_mset fst P), set_mset (image_mset fst Q))"

locale weighted_FO_resolution_prover =
  FO_resolution_prover S subst_atm id_subst comp_subst renamings_apart atm_of_atms mgu less_atm
  for
    S :: "('a :: wellorder) clause ⇒ 'a clause" and
    subst_atm :: "'a ⇒ 's ⇒ 'a" and
    id_subst :: "'s" and
    comp_subst :: "'s ⇒ 's ⇒ 's" and
    renamings_apart :: "'a clause list ⇒ 's list" and
    atm_of_atms :: "'a list ⇒ 'a" and
    mgu :: "'a set set ⇒ 's option" and
    less_atm :: "'a ⇒ 'a ⇒ bool" +
  fixes
    weight :: "'a clause × nat ⇒ nat"
  assumes
    weight_mono: "i < j ⟹ weight (C, i) < weight (C, j)"
begin

abbreviation clss_of_wstate :: "'a wstate ⇒ 'a clause set" where
  "clss_of_wstate St ≡ clss_of_state (state_of_wstate St)"

abbreviation N_of_wstate :: "'a wstate ⇒ 'a clause set" where
  "N_of_wstate St ≡ N_of_state (state_of_wstate St)"

abbreviation P_of_wstate :: "'a wstate ⇒ 'a clause set" where
  "P_of_wstate St ≡ P_of_state (state_of_wstate St)"

abbreviation Q_of_wstate :: "'a wstate ⇒ 'a clause set" where
  "Q_of_wstate St ≡ Q_of_state (state_of_wstate St)"

fun wN_of_wstate :: "'a wstate ⇒ 'a wclause multiset" where
  "wN_of_wstate (N, P, Q, n) = N"

fun wP_of_wstate :: "'a wstate ⇒ 'a wclause multiset" where
  "wP_of_wstate (N, P, Q, n) = P"

fun wQ_of_wstate :: "'a wstate ⇒ 'a wclause multiset" where
  "wQ_of_wstate (N, P, Q, n) = Q"

fun n_of_wstate :: "'a wstate ⇒ nat" where
  "n_of_wstate (N, P, Q, n) = n"

lemma of_wstate_split[simp]:
  "(wN_of_wstate St, wP_of_wstate St, wQ_of_wstate St, n_of_wstate St) = St"
  by (cases St) auto

abbreviation grounding_of_wstate :: "'a wstate ⇒ 'a clause set" where
  "grounding_of_wstate St ≡ grounding_of_state (state_of_wstate St)"

abbreviation Liminf_wstate :: "'a wstate llist ⇒ 'a state" where
  "Liminf_wstate Sts ≡ Liminf_state (lmap state_of_wstate Sts)"

lemma timestamp_le_weight: "n ≤ weight (C, n)"
  by (induct n, simp, metis weight_mono[of k "Suc k" for k] Suc_le_eq le_less le_trans)

inductive weighted_RP :: "'a wstate ⇒ 'a wstate ⇒ bool" (infix "↝w" 50) where
  tautology_deletion: "Neg A ∈# C ⟹ Pos A ∈# C ⟹ (N + {#(C, i)#}, P, Q, n) ↝w (N, P, Q, n)"
| forward_subsumption: "D ∈# image_mset fst (P + Q) ⟹ subsumes D C ⟹
    (N + {#(C, i)#}, P, Q, n) ↝w (N, P, Q, n)"
| backward_subsumption_P: "D ∈# image_mset fst N ⟹ C ∈# image_mset fst P ⟹
    strictly_subsumes D C ⟹ (N, P, Q, n) ↝w (N, {#(E, k) ∈# P. E ≠ C#}, Q, n)"
| backward_subsumption_Q: "D ∈# image_mset fst N ⟹ strictly_subsumes D C ⟹
    (N, P, Q + {#(C, i)#}, n) ↝w (N, P, Q, n)"
| forward_reduction: "D + {#L'#} ∈# image_mset fst (P + Q) ⟹ - L = L' ⋅l σ ⟹ D ⋅ σ ⊆# C ⟹
    (N + {#(C + {#L#}, i)#}, P, Q, n) ↝w (N + {#(C, i)#}, P, Q, n)"
| backward_reduction_P: "D + {#L'#} ∈# image_mset fst N ⟹ - L = L' ⋅l σ ⟹ D ⋅ σ ⊆# C ⟹
    (∀j. (C + {#L#}, j) ∈# P ⟶ j ≤ i) ⟹
    (N, P + {#(C + {#L#}, i)#}, Q, n) ↝w (N, P + {#(C, i)#}, Q, n)"
| backward_reduction_Q: "D + {#L'#} ∈# image_mset fst N ⟹ - L = L' ⋅l σ ⟹ D ⋅ σ ⊆# C ⟹
    (N, P, Q + {#(C + {#L#}, i)#}, n) ↝w (N, P + {#(C, i)#}, Q, n)"
| clause_processing: "(N + {#(C, i)#}, P, Q, n) ↝w (N, P + {#(C, i)#}, Q, n)"
| inference_computation: "(∀(D, j) ∈# P. weight (C, i) ≤ weight (D, j)) ⟹
    N = mset_set ((λD. (D, n)) ` concls_of
      (inference_system.inferences_between (ord_FO_Γ S) (set_mset (image_mset fst Q)) C)) ⟹
    ({#}, P + {#(C, i)#}, Q, n) ↝w (N, {#(D, j) ∈# P. D ≠ C#}, Q + {#(C, i)#}, Suc n)"

lemma weighted_RP_imp_RP: "St ↝w St' ⟹ state_of_wstate St ↝ state_of_wstate St'"
proof (induction rule: weighted_RP.induct)
  case (backward_subsumption_P D N C P Q n)
  show ?case
    by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(↝)", OF _ _
          RP.backward_subsumption_P[of D "fst ` set_mset N" C "fst ` set_mset P - {C}"
            "fst ` set_mset Q"]])
      (use backward_subsumption_P in auto)
next
  case (inference_computation P C i N n Q)
  show ?case
     by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(↝)", OF _ _
           RP.inference_computation[of "fst ` set_mset N" "fst ` set_mset Q" C
             "fst ` set_mset P - {C}"]],
         use inference_computation(2) finite_ord_FO_resolution_inferences_between in
           ‹auto simp: comp_def image_comp inference_system.inferences_between_def›)
qed (use RP.intros in simp_all)

lemma final_weighted_RP: "¬ ({#}, {#}, Q, n) ↝w St"
  by (auto elim: weighted_RP.cases)

context
  fixes
    Sts :: "'a wstate llist"
  assumes
    full_deriv: "full_chain (↝w) Sts" and
    empty_P0: "P_of_wstate (lhd Sts) = {}" and
    empty_Q0: "Q_of_wstate (lhd Sts) = {}"
begin

lemma finite_Sts0: "finite (clss_of_wstate (lhd Sts))"
  by (cases "lhd Sts") auto

lemmas deriv = full_chain_imp_chain[OF full_deriv]
lemmas lhd_lmap_Sts = llist.map_sel(1)[OF chain_not_lnull[OF deriv]]

lemma deriv_RP: "chain (↝) (lmap state_of_wstate Sts)"
  using deriv weighted_RP_imp_RP by (metis chain_lmap)

lemma finite_Sts0_RP: "finite (clss_of_state (lhd (lmap state_of_wstate Sts)))"
  using finite_Sts0 chain_length_pos[OF deriv] by auto

lemma empty_P0_RP: "P_of_state (lhd (lmap state_of_wstate Sts)) = {}"
  using empty_P0 chain_length_pos[OF deriv] by auto

lemma empty_Q0_RP: "Q_of_state (lhd (lmap state_of_wstate Sts)) = {}"
  using empty_Q0 chain_length_pos[OF deriv] by auto

lemmas Sts_thms = deriv_RP finite_Sts0_RP empty_P0_RP empty_Q0_RP

theorem weighted_RP_model:
  "St ↝w St' ⟹ I ⊨s grounding_of_wstate St' ⟷ I ⊨s grounding_of_wstate St"
  using RP_model Sts_thms weighted_RP_imp_RP by (simp only: comp_def)

abbreviation S_gQ :: "'a clause ⇒ 'a clause" where
  "S_gQ ≡ S_Q (lmap state_of_wstate Sts)"

interpretation sq: selection S_gQ
  unfolding S_Q_def using S_M_selects_subseteq S_M_selects_neg_lits selection_axioms
  by unfold_locales auto

interpretation gd: ground_resolution_with_selection S_gQ
  by unfold_locales

interpretation src: standard_redundancy_criterion_reductive gd.ord_Γ
  by unfold_locales

interpretation src: standard_redundancy_criterion_counterex_reducing gd.ord_Γ
  "ground_resolution_with_selection.INTERP S_gQ"
  by unfold_locales

lemmas ord_Γ_saturated_upto_def = src.saturated_upto_def
lemmas ord_Γ_saturated_upto_complete = src.saturated_upto_complete
lemmas ord_Γ_contradiction_Rf = src.contradiction_Rf

theorem weighted_RP_sound:
  assumes "{#} ∈ clss_of_state (Liminf_wstate Sts)"
  shows "¬ satisfiable (grounding_of_wstate (lhd Sts))"
  by (rule RP_sound[OF deriv_RP assms, unfolded lhd_lmap_Sts])

abbreviation RP_filtered_measure :: "('a wclause ⇒ bool) ⇒ 'a wstate ⇒ nat × nat × nat" where
  "RP_filtered_measure ≡ λp (N, P, Q, n).
     (sum_mset (image_mset (λ(C, i). Suc (size C)) {#Di ∈# N + P + Q. p Di#}),
      size {#Di ∈# N. p Di#}, size {#Di ∈# P. p Di#})"

abbreviation RP_combined_measure :: "nat ⇒ 'a wstate ⇒ nat × (nat × nat × nat) × (nat × nat × nat)" where
  "RP_combined_measure ≡ λw St.
     (w + 1 - n_of_wstate St, RP_filtered_measure (λ(C, i). i ≤ w) St,
      RP_filtered_measure (λCi. True) St)"

abbreviation (input) RP_filtered_relation :: "((nat × nat × nat) × (nat × nat × nat)) set" where
  "RP_filtered_relation ≡ natLess <*lex*> natLess <*lex*> natLess"

abbreviation (input) RP_combined_relation :: "((nat × ((nat × nat × nat) × (nat × nat × nat))) ×
    (nat × ((nat × nat × nat) × (nat × nat × nat)))) set" where
  "RP_combined_relation ≡ natLess <*lex*> RP_filtered_relation <*lex*> RP_filtered_relation"

abbreviation "(fst3 :: 'b * 'c * 'd ⇒ 'b) ≡ fst"
abbreviation "(snd3 :: 'b * 'c * 'd ⇒ 'c) ≡ λx. fst (snd x)"
abbreviation "(trd3 :: 'b * 'c * 'd ⇒ 'd) ≡ λx. snd (snd x)"

lemma
  wf_RP_filtered_relation: "wf RP_filtered_relation" and
  wf_RP_combined_relation: "wf RP_combined_relation"
  unfolding natLess_def using wf_less wf_mult by auto

lemma multiset_sum_of_Suc_f_monotone: "N ⊂# M ⟹ (∑x ∈# N. Suc (f x)) < (∑x ∈# M. Suc (f x))"
proof (induction N arbitrary: M)
  case empty
  then obtain y where "y ∈# M"
    by force
  then have "(∑x ∈# M. 1) = (∑x ∈# M - {#y#} + {#y#}. 1)"
    by auto
  also have "... = (∑x ∈# M - {#y#}. 1) + (∑x ∈# {#y#}. 1)"
    by (metis image_mset_union sum_mset.union)
  also have "... > (0 :: nat)"
    by auto
  finally have "0 < (∑x ∈# M. Suc (f x))"
    by (fastforce intro: gr_zeroI)
  then show ?case
    using empty by auto
next
  case (add x N)
  from this(2) have "(∑y ∈# N. Suc (f y)) < (∑y ∈# M - {#x#}. Suc (f y))"
    using add(1)[of "M - {#x#}"] by (simp add: insert_union_subset_iff)
  moreover have "add_mset x (remove1_mset x M) = M"
    by (meson add.prems add_mset_remove_trivial_If mset_subset_insertD)
  ultimately show ?case
    by (metis (no_types) add.commute add_less_cancel_right sum_mset.insert)
qed

lemma multiset_sum_monotone_f':
  assumes "CC ⊂# DD"
  shows "(∑(C, i) ∈# CC. Suc (f C)) < (∑(C, i) ∈# DD. Suc (f C))"
  using multiset_sum_of_Suc_f_monotone[OF assms, of "f ∘ fst"]
  by (metis (mono_tags) comp_apply image_mset_cong2 split_beta)

lemma filter_mset_strict_subset:
  assumes "x ∈# M" and "¬ p x"
  shows "{#y ∈# M. p y#} ⊂# M"
proof -
  have subseteq: "{#E ∈# M. p E#} ⊆# M"
    by auto
  have "count {#E ∈# M. p E#} x = 0"
    using assms by auto
  moreover have "0 < count M x"
    using assms by auto
  ultimately have lt_count: "count {#y ∈# M. p y#} x < count M x"
    by auto
  then show ?thesis
    using subseteq by (metis less_not_refl2 subset_mset.le_neq_trans)
qed

lemma weighted_RP_measure_decreasing_N:
  assumes "St ↝w St'" and "(C, l) ∈# wN_of_wstate St"
  shows "(RP_filtered_measure (λCi. True) St', RP_filtered_measure (λCi. True) St)
    ∈ RP_filtered_relation"
using assms proof (induction rule: weighted_RP.induct)
  case (backward_subsumption_P D N C' P Q n)
  then obtain i' where  "(C', i') ∈# P"
    by auto
  then have "{#(E, k) ∈# P. E ≠ C'#} ⊂# P"
    using filter_mset_strict_subset[of "(C', i')" P "λX. ¬fst X =  C'"]
    by (metis (mono_tags, lifting) filter_mset_cong fst_conv prod.case_eq_if)
  then have "(∑(C, i) ∈# {#(E, k) ∈# P. E ≠ C'#}. Suc (size C)) < (∑(C, i) ∈# P. Suc (size C))"
    using multiset_sum_monotone_f'[of "{#(E, k) ∈# P. E ≠ C'#}" P size] by metis
  then show ?case
    unfolding natLess_def by auto
qed (auto simp: natLess_def)

lemma weighted_RP_measure_decreasing_P:
  assumes "St ↝w St'" and "(C, i) ∈# wP_of_wstate St"
  shows "(RP_combined_measure (weight (C, i)) St', RP_combined_measure (weight (C, i)) St)
    ∈ RP_combined_relation"
using assms proof (induction rule: weighted_RP.induct)
  case (backward_subsumption_P D N C' P Q n)

  define St where "St = (N, P, Q, n)"
  define P' where "P' = {#(E, k) ∈# P. E ≠ C'#}"
  define St' where "St' = (N, P', Q, n)"

  from backward_subsumption_P obtain i' where  "(C', i') ∈# P"
    by auto
  then have P'_sub_P: "P' ⊂# P"
    unfolding P'_def using filter_mset_strict_subset[of "(C', i')" P "λDj. fst Dj ≠ C'"]
    by (metis (no_types, lifting) filter_mset_cong fst_conv prod.case_eq_if)

  have P'_subeq_P_filter:
    "{#(Ca, ia) ∈# P'. ia ≤ weight (C, i)#} ⊆# {#(Ca, ia) ∈# P. ia ≤ weight (C, i)#}"
    using P'_sub_P by (auto intro: multiset_filter_mono)

  have "fst3 (RP_combined_measure (weight (C, i)) St')
    ≤ fst3 (RP_combined_measure (weight (C, i)) St)"
    unfolding St'_def St_def by auto
  moreover have "(∑(C, i) ∈# {#(Ca, ia) ∈# P'. ia ≤ weight (C, i)#}. Suc (size C))
    ≤ (∑x ∈# {#(Ca, ia) ∈# P. ia ≤ weight (C, i)#}. case x of (C, i) ⇒ Suc (size C))"
    using P'_subeq_P_filter by (rule sum_image_mset_mono)
  then have "fst3 (snd3 (RP_combined_measure (weight (C, i)) St'))
    ≤ fst3 (snd3 (RP_combined_measure (weight (C, i)) St))"
    unfolding St'_def St_def by auto
  moreover have "snd3 (snd3 (RP_combined_measure (weight (C, i)) St'))
    ≤ snd3 (snd3 (RP_combined_measure (weight (C, i)) St))"
    unfolding St'_def St_def by auto
  moreover from P'_subeq_P_filter have "size {#(Ca, ia) ∈# P'. ia ≤ weight (C, i)#}
    ≤ size {#(Ca, ia) ∈# P. ia ≤ weight (C, i)#}"
    by (simp add: size_mset_mono)
  then have "trd3 (snd3 (RP_combined_measure (weight (C, i)) St'))
    ≤ trd3 (snd3 (RP_combined_measure (weight (C, i)) St))"
    unfolding St'_def St_def unfolding fst_def snd_def by auto
  moreover from P'_sub_P have "(∑(C, i) ∈# P'. Suc (size C)) < (∑(C, i) ∈# P. Suc (size C))"
    using multiset_sum_monotone_f'[of "{#(E, k) ∈# P. E ≠ C'#}" P size] unfolding P'_def by metis
  then have "fst3 (trd3 (RP_combined_measure (weight (C, i)) St'))
    < fst3 (trd3 (RP_combined_measure (weight (C, i)) St))"
    unfolding P'_def St'_def St_def by auto
  ultimately show ?case
    unfolding natLess_def P'_def St'_def St_def by auto
next
  case (inference_computation P C' i' N n Q)
  then show ?case
  proof (cases "n ≤ weight (C, i)")
    case True
    then have "weight (C, i) + 1 - n > weight (C, i) + 1 - Suc n"
      by auto
    then show ?thesis
      unfolding natLess_def by auto
  next
    case n_nle_w: False

    define St :: "'a wstate" where "St = ({#}, P + {#(C', i')#}, Q, n)"
    define St' :: "'a wstate" where "St' =  (N, {#(D, j) ∈# P. D ≠ C'#}, Q + {#(C', i')#}, Suc n)"
    define concls :: "'a wclause set" where
      "concls = (λD. (D, n)) ` concls_of (inference_system.inferences_between (ord_FO_Γ S)
         (fst ` set_mset Q) C')"

    have fin: "finite concls"
      unfolding concls_def using finite_ord_FO_resolution_inferences_between by auto

    have "{(D, ia) ∈ concls. ia ≤ weight (C, i)} = {}"
      unfolding concls_def using n_nle_w by auto
    then have "{#(D, ia) ∈# mset_set concls. ia ≤ weight (C, i)#} = {#}"
      using fin filter_mset_empty_if_finite_and_filter_set_empty[of concls] by auto
    then have n_low_weight_empty: "{#(D, ia) ∈# N. ia ≤ weight (C, i)#} = {#}"
      unfolding inference_computation unfolding concls_def by auto

    have "weight (C', i') ≤ weight (C, i)"
      using inference_computation by auto
    then have i'_le_w_Ci: "i' ≤ weight (C, i)"
      using timestamp_le_weight[of i' C'] by auto

    have subs: "{#(D, ia) ∈# N + {#(D, j) ∈# P. D ≠ C'#} + (Q + {#(C', i')#}). ia ≤ weight (C, i)#}
      ⊆# {#(D, ia) ∈# {#} + (P + {#(C', i')#}) + Q. ia ≤ weight (C, i)#}"
      using n_low_weight_empty by (auto simp: multiset_filter_mono)

    have "fst3 (RP_combined_measure (weight (C, i)) St')
      ≤ fst3 (RP_combined_measure (weight (C, i)) St)"
      unfolding St'_def St_def by auto
    moreover have "fst (RP_filtered_measure ((λ(D, ia). ia ≤ weight (C, i))) St') =
      (∑(C, i) ∈# {#(D, ia) ∈# N + {#(D, j) ∈# P. D ≠ C'#} + (Q + {#(C', i')#}).
         ia ≤ weight (C, i)#}. Suc (size C))"
      unfolding St'_def by auto
    also have "... ≤ (∑(C, i) ∈# {#(D, ia) ∈# {#} + (P + {#(C', i')#}) + Q. ia ≤ weight (C, i)#}.
      Suc (size C))"
      using subs sum_image_mset_mono by blast
    also have "... = fst (RP_filtered_measure (λ(D, ia). ia ≤ weight (C, i)) St)"
      unfolding St_def by auto
    finally have "fst3 (snd3 (RP_combined_measure (weight (C, i)) St'))
      ≤ fst3 (snd3 (RP_combined_measure (weight (C, i)) St))"
      by auto
    moreover have "snd3 (snd3 (RP_combined_measure (weight (C, i)) St')) =
      snd3 (snd3 (RP_combined_measure (weight (C, i)) St))"
      unfolding St_def St'_def using n_low_weight_empty by auto
    moreover have "trd3 (snd3 (RP_combined_measure (weight (C, i)) St')) <
      trd3 (snd3 (RP_combined_measure (weight (C, i)) St))"
      unfolding St_def St'_def using i'_le_w_Ci
      by (simp add: le_imp_less_Suc multiset_filter_mono size_mset_mono)
    ultimately show ?thesis
      unfolding natLess_def St'_def St_def lex_prod_def by force
  qed
qed (auto simp: natLess_def)

lemma preserve_min_or_delete_completely:
  assumes "St ↝w St'" "(C, i) ∈# wP_of_wstate St"
    "∀k. (C, k) ∈# wP_of_wstate St ⟶ i ≤ k"
  shows "(C, i) ∈# wP_of_wstate St' ∨ (∀j. (C, j) ∉# wP_of_wstate St')"
using assms proof (induction rule: weighted_RP.induct)
  case (backward_reduction_P D L' N L σ C' P i' Q n)
  show ?case
  proof (cases "C = C' + {#L#}")
    case True_outer: True
    then have C_i_in: "(C, i) ∈# P + {#(C, i')#}"
      using backward_reduction_P by auto
    then have max: "⋀k. (C, k) ∈# P + {#(C, i')#} ⟹ k ≤ i'"
      using backward_reduction_P unfolding True_outer[symmetric] by auto
    then have "count (P + {#(C, i')#}) (C, i') ≥ 1"
      by auto
    moreover
    {
      assume asm: "count (P + {#(C, i')#}) (C, i') = 1"
      then have nin_P: "(C, i') ∉# P"
        using not_in_iff by force
      have ?thesis
      proof (cases "(C, i) = (C, i')")
        case True
        then have "i = i'"
          by auto
        then have "∀j. (C, j) ∈# P + {#(C, i')#} ⟶ j = i'"
          using max backward_reduction_P(6) unfolding True_outer[symmetric] by force
        then show ?thesis
          using True_outer[symmetric] nin_P by auto
      next
        case False
        then show ?thesis
          using C_i_in by auto
      qed
    }
    moreover
    {
      assume "count (P + {#(C, i')#}) (C, i') > 1"
      then have ?thesis
        using C_i_in by auto
    }
    ultimately show ?thesis
      by (cases "count (P + {#(C, i')#}) (C, i') = 1") auto
  next
    case False
    then show ?thesis
      using backward_reduction_P by auto
  qed
qed auto

lemma preserve_min_P:
  assumes
    "St ↝w St'" "(C, j) ∈# wP_of_wstate St'" and
    "(C, i) ∈# wP_of_wstate St" and
    "∀k. (C, k) ∈# wP_of_wstate St ⟶ i ≤ k"
  shows "(C, i) ∈# wP_of_wstate St'"
  using assms preserve_min_or_delete_completely by blast

lemma preserve_min_P_Sts:
  assumes
    "enat (Suc k) < llength Sts" and
    "(C, i) ∈# wP_of_wstate (lnth Sts k)" and
    "(C, j) ∈# wP_of_wstate (lnth Sts (Suc k))" and
    "∀j. (C, j) ∈# wP_of_wstate (lnth Sts k) ⟶ i ≤ j"
  shows "(C, i) ∈# wP_of_wstate (lnth Sts (Suc k))"
  using deriv assms chain_lnth_rel preserve_min_P by metis

lemma in_lnth_in_Supremum_ldrop:
  assumes "i < llength xs" and "x ∈# (lnth xs i)"
  shows "x ∈ Sup_llist (lmap set_mset (ldrop (enat i) xs))"
  using assms by (metis (no_types) ldrop_eq_LConsD ldropn_0 llist.simps(13) contra_subsetD
      ldrop_enat ldropn_Suc_conv_ldropn lnth_0 lnth_lmap lnth_subset_Sup_llist)

lemma persistent_wclause_in_P_if_persistent_clause_in_P:
  assumes "C ∈ Liminf_llist (lmap P_of_state (lmap state_of_wstate Sts))"
  shows "∃i. (C, i) ∈ Liminf_llist (lmap (set_mset ∘ wP_of_wstate) Sts)"
proof -
  obtain t_C where t_C_p:
    "enat t_C < llength Sts"
    "⋀t. t_C ≤ t ⟹ t < llength Sts ⟹ C ∈ P_of_state (state_of_wstate (lnth Sts t))"
    using assms unfolding Liminf_llist_def by auto
  then obtain i where i_p:
    "(C, i) ∈# wP_of_wstate (lnth Sts t_C)"
    using t_C_p by (cases "lnth Sts t_C") force

  have Ci_in_nth_wP: "∃i. (C, i) ∈# wP_of_wstate (lnth Sts (t_C + t))" if "t_C + t < llength Sts"
    for t
    using that t_C_p(2)[of "t_C + _"] by (cases "lnth Sts (t_C + t)") force

  define in_Sup_wP :: "nat ⇒ bool" where
    "in_Sup_wP = (λi. (C, i) ∈ Sup_llist (lmap (set_mset ∘ wP_of_wstate) (ldrop t_C Sts)))"

  have "in_Sup_wP i"
    using i_p assms(1) in_lnth_in_Supremum_ldrop[of t_C "lmap wP_of_wstate Sts" "(C, i)"] t_C_p
    by (simp add: in_Sup_wP_def llist.map_comp)
  then obtain j where j_p: "is_least in_Sup_wP j"
    unfolding in_Sup_wP_def[symmetric] using least_exists by metis
  then have "∀i. (C, i) ∈ Sup_llist (lmap (set_mset ∘ wP_of_wstate) (ldrop t_C Sts)) ⟶ j ≤ i"
    unfolding is_least_def in_Sup_wP_def using not_less by blast
  then have j_smallest:
    "⋀i t. enat (t_C + t) < llength Sts ⟹ (C, i) ∈# wP_of_wstate (lnth Sts (t_C + t)) ⟹ j ≤ i"
    unfolding comp_def
    by (smt add.commute ldrop_enat ldrop_eq_LConsD ldrop_ldrop ldropn_Suc_conv_ldropn
        plus_enat_simps(1)  lnth_ldropn Sup_llist_def UN_I ldrop_lmap llength_lmap lnth_lmap
        mem_Collect_eq)
  from j_p have "∃t_Cj. t_Cj < llength (ldrop (enat t_C) Sts)
    ∧ (C, j) ∈# wP_of_wstate (lnth (ldrop t_C Sts) t_Cj)"
    unfolding in_Sup_wP_def Sup_llist_def is_least_def by simp
  then obtain t_Cj where j_p:
    "(C,j) ∈# wP_of_wstate (lnth Sts (t_C + t_Cj))"
    "enat (t_C + t_Cj) < llength Sts"
    by (smt add.commute ldrop_enat ldrop_eq_LConsD ldrop_ldrop ldropn_Suc_conv_ldropn
        plus_enat_simps(1) lhd_ldropn)
  have Ci_stays:
    "t_C + t_Cj + t < llength Sts ⟹ (C,j) ∈# wP_of_wstate (lnth Sts (t_C + t_Cj + t))" for t
  proof (induction t)
    case 0
    then show ?case
      using j_p by (simp add: add.commute)
  next
    case (Suc t)
    have any_Ck_in_wP: "j ≤ k" if "(C, k) ∈# wP_of_wstate (lnth Sts (t_C + t_Cj + t))" for k
      using that j_p j_smallest Suc
      by (smt Suc_ile_eq add.commute add.left_commute add_Suc less_imp_le plus_enat_simps(1)
          the_enat.simps)
    from Suc have Cj_in_wP: "(C, j) ∈# wP_of_wstate (lnth Sts (t_C + t_Cj + t))"
      by (metis (no_types, hide_lams) Suc_ile_eq add.commute add_Suc_right less_imp_le)
    moreover have "C ∈ P_of_state (state_of_wstate (lnth Sts (Suc (t_C + t_Cj + t))))"
      using t_C_p(2) Suc.prems by auto
    then have "∃k. (C, k) ∈# wP_of_wstate (lnth Sts (Suc (t_C + t_Cj + t)))"
      by (smt Suc.prems Ci_in_nth_wP add.commute add.left_commute add_Suc_right enat_ord_code(4))
    ultimately have "(C, j) ∈# wP_of_wstate (lnth Sts (Suc (t_C + t_Cj + t)))"
      using preserve_min_P_Sts Cj_in_wP any_Ck_in_wP Suc.prems by force
    then have "(C, j) ∈# lnth (lmap wP_of_wstate Sts) (Suc (t_C + t_Cj + t))"
      using Suc.prems by auto
    then show ?case
      by (smt Suc.prems add.commute add_Suc_right lnth_lmap)
  qed
  then have "(⋀t. t_C + t_Cj ≤ t ⟹ t < llength (lmap (set_mset ∘ wP_of_wstate) Sts) ⟹
    (C, j) ∈# wP_of_wstate (lnth Sts t))"
    using Ci_stays[of "_ - (t_C + t_Cj)"] by (metis le_add_diff_inverse llength_lmap)
  then have "(C, j) ∈ Liminf_llist (lmap (set_mset ∘ wP_of_wstate) Sts)"
    unfolding Liminf_llist_def using j_p by auto
  then show "∃i. (C, i) ∈ Liminf_llist (lmap (set_mset ∘ wP_of_wstate) Sts)"
    by auto
qed

lemma lfinite_not_LNil_nth_llast:
  assumes "lfinite Sts" and "Sts ≠ LNil"
  shows "∃i < llength Sts. lnth Sts i = llast Sts ∧ (∀j < llength Sts. j ≤ i)"
using assms proof (induction rule: lfinite.induct)
  case (lfinite_LConsI xs x)
  then show ?case
  proof (cases "xs = LNil")
    case True
    show ?thesis
      using True zero_enat_def by auto
  next
    case False
    then obtain i where
      i_p: "enat i < llength xs ∧ lnth xs i = llast xs ∧ (∀j < llength xs. j ≤ enat i)"
      using lfinite_LConsI by auto
    then have "enat (Suc i) < llength (LCons x xs)"
      by (simp add: Suc_ile_eq)
    moreover from i_p have "lnth (LCons x xs) (Suc i) = llast (LCons x xs)"
      by (metis gr_implies_not_zero llast_LCons llength_lnull lnth_Suc_LCons)
    moreover from i_p have "∀j < llength (LCons x xs). j ≤ enat (Suc i)"
      by (metis antisym_conv2 eSuc_enat eSuc_ile_mono ileI1 iless_Suc_eq llength_LCons)
    ultimately show ?thesis
      by auto
  qed
qed auto

lemma fair_if_finite:
  assumes fin: "lfinite Sts"
  shows "fair_state_seq (lmap state_of_wstate Sts)"
proof (rule ccontr)
  assume unfair: "¬ fair_state_seq (lmap state_of_wstate Sts)"

  have no_inf_from_last: "∀y. ¬ llast Sts ↝w y"
    using fin full_chain_iff_chain[of "(↝w)" Sts] full_deriv by auto

  from unfair obtain C where
    "C ∈ Liminf_llist (lmap N_of_state (lmap state_of_wstate Sts))
       ∪ Liminf_llist (lmap P_of_state (lmap state_of_wstate Sts))"
    unfolding fair_state_seq_def Liminf_state_def by auto
  then obtain i where i_p:
    "enat i < llength Sts"
    "⋀j. i ≤ j ⟹ enat j < llength Sts ⟹
     C ∈ N_of_state (state_of_wstate (lnth Sts j)) ∪ P_of_state (state_of_wstate (lnth Sts j))"
    unfolding Liminf_llist_def by auto

  have C_in_llast:
    "C ∈ N_of_state (state_of_wstate (llast Sts)) ∪ P_of_state (state_of_wstate (llast Sts))"
  proof -
    obtain l where
      l_p: "enat l < llength Sts ∧ lnth Sts l = llast Sts ∧ (∀j < llength Sts. j ≤ enat l)"
      using fin lfinite_not_LNil_nth_llast i_p(1) by fastforce
    then have
      "C ∈ N_of_state (state_of_wstate (lnth Sts l)) ∪ P_of_state (state_of_wstate (lnth Sts l))"
      using i_p(1) i_p(2)[of l] by auto
    then show ?thesis
      using l_p by auto
  qed

  define N :: "'a wclause multiset" where "N = wN_of_wstate (llast Sts)"
  define P :: "'a wclause multiset" where "P = wP_of_wstate (llast Sts)"
  define Q :: "'a wclause multiset" where "Q = wQ_of_wstate (llast Sts)"
  define n :: nat where "n = n_of_wstate (llast Sts)"

  {
    assume "N_of_state (state_of_wstate (llast Sts)) ≠ {}"
    then obtain D j where "(D, j) ∈# N"
      unfolding N_def by (cases "llast Sts") auto
    then have "llast Sts ↝w (N - {#(D, j)#}, P + {#(D, j)#}, Q, n)"
      using weighted_RP.clause_processing[of "N - {#(D, j)#}" D j P Q n]
      unfolding N_def P_def Q_def n_def by auto
    then have "∃St'. llast Sts ↝w St'"
      by auto
  }
  moreover
  {
    assume a: "N_of_state (state_of_wstate (llast Sts)) = {}"
    then have b: "N = {#}"
      unfolding N_def by (cases "llast Sts") auto
    from a have "C ∈ P_of_state (state_of_wstate (llast Sts))"
      using C_in_llast by auto
    then obtain D j where "(D, j) ∈# P"
      unfolding P_def by (cases "llast Sts") auto
    then have "weight (D, j) ∈ weight ` set_mset P"
      by auto
    then have "∃w. is_least (λw. w ∈ (weight ` set_mset P)) w"
      using least_exists by auto
    then have "∃D j. (∀(D', j') ∈# P. weight (D, j) ≤ weight (D', j')) ∧ (D, j) ∈# P"
      using assms linorder_not_less unfolding is_least_def by (auto 6 0)
    then obtain D j where
      min: "(∀(D', j') ∈# P. weight (D, j) ≤ weight (D', j'))" and
      Dj_in_p: "(D, j) ∈# P"
      by auto
    from min have min: "(∀(D', j') ∈# P - {#(D, j)#}. weight (D, j) ≤ weight (D', j'))"
      using mset_subset_diff_self[OF Dj_in_p] by auto

    define N' where
      "N' = mset_set ((λD'. (D', n)) ` concls_of (inference_system.inferences_between (ord_FO_Γ S)
         (set_mset (image_mset fst Q)) D))"

    have "llast Sts ↝w (N', {#(D', j') ∈# P - {#(D, j)#}. D' ≠ D#}, Q + {#(D,j)#}, Suc n)"
      using weighted_RP.inference_computation[of "P - {#(D, j)#}" D j N' n Q, OF min N'_def]
        of_wstate_split[symmetric, of "llast Sts"] Dj_in_p
      unfolding N_def[symmetric] P_def[symmetric] Q_def[symmetric] n_def[symmetric] b by auto
    then have "∃St'. llast Sts ↝w St'"
      by auto
  }
  ultimately have "∃St'. llast Sts ↝w St'"
    by auto
  then show False
    using no_inf_from_last by metis
qed

lemma N_of_state_state_of_wstate_wN_of_wstate:
  assumes "C ∈ N_of_state (state_of_wstate St)"
  shows "∃i. (C, i) ∈# wN_of_wstate St"
  by (smt N_of_state.elims assms eq_fst_iff fstI fst_conv image_iff of_wstate_split set_image_mset
      state_of_wstate.simps)

lemma in_wN_of_wstate_in_N_of_wstate: "(C, i) ∈# wN_of_wstate St ⟹ C ∈ N_of_wstate St"
  by (metis (mono_guards_query_query) N_of_state.simps fst_conv image_eqI of_wstate_split
      set_image_mset state_of_wstate.simps)

lemma in_wP_of_wstate_in_P_of_wstate: "(C, i) ∈# wP_of_wstate St ⟹ C ∈ P_of_wstate St"
  by (metis (mono_guards_query_query) P_of_state.simps fst_conv image_eqI of_wstate_split
      set_image_mset state_of_wstate.simps)

lemma in_wQ_of_wstate_in_Q_of_wstate: "(C, i) ∈# wQ_of_wstate St ⟹ C ∈ Q_of_wstate St"
  by (metis (mono_guards_query_query) Q_of_state.simps fst_conv image_eqI of_wstate_split
      set_image_mset state_of_wstate.simps)

lemma n_of_wstate_weighted_RP_increasing: "St ↝w St' ⟹ n_of_wstate St ≤ n_of_wstate St'"
  by (induction rule: weighted_RP.induct) auto

lemma nth_of_wstate_monotonic:
  assumes "j < llength Sts" and "i ≤ j"
  shows "n_of_wstate (lnth Sts i) ≤ n_of_wstate (lnth Sts j)"
using assms proof (induction "j - i" arbitrary: i)
  case (Suc x)
  then have "x = j - (i + 1)"
    by auto
  then have "n_of_wstate (lnth Sts (i + 1)) ≤ n_of_wstate (lnth Sts j)"
    using Suc by auto
  moreover have "i < j"
    using Suc by auto
  then have "Suc i < llength Sts"
    using Suc by (metis enat_ord_simps(2) le_less_Suc_eq less_le_trans not_le)
  then have "lnth Sts i ↝w lnth Sts (Suc i)"
    using deriv chain_lnth_rel[of "(↝w)" Sts i] by auto
  then have "n_of_wstate (lnth Sts i) ≤ n_of_wstate (lnth Sts (i + 1))"
    using n_of_wstate_weighted_RP_increasing[of "lnth Sts i" "lnth Sts (i + 1)"] by auto
  ultimately show ?case
    by auto
qed auto

lemma infinite_chain_relation_measure:
  assumes
    measure_decreasing: "⋀St St'. P St ⟹ R St St' ⟹ (m St', m St) ∈ mR" and
    non_infer_chain: "chain R (ldrop (enat k) Sts)" and
    inf: "llength Sts = ∞" and
    P: "⋀i. P (lnth (ldrop (enat k) Sts) i)"
  shows "chain (λx y. (x, y) ∈ mR)¯¯ (lmap m (ldrop (enat k) Sts))"
proof (rule lnth_rel_chain)
  show "¬ lnull (lmap m (ldrop (enat k) Sts))"
    using assms by auto
next
  from inf have ldrop_inf: "llength (ldrop (enat k) Sts) = ∞ ∧ ¬ lfinite (ldrop (enat k) Sts)"
    using inf by (auto simp: llength_eq_infty_conv_lfinite)
  {
    fix j :: "nat"
    define St where "St = lnth (ldrop (enat k) Sts) j"
    define St' where "St' = lnth (ldrop (enat k) Sts) (j + 1)"
    have P': "P St ∧ P St'"
      unfolding St_def St'_def using P by auto
    from ldrop_inf have "R St St'"
      unfolding St_def St'_def
      using non_infer_chain infinite_chain_lnth_rel[of "ldrop (enat k) Sts" R j] by auto
    then have "(m St', m St) ∈ mR"
      using measure_decreasing P' by auto
    then have "(lnth (lmap m (ldrop (enat k) Sts)) (j + 1), lnth (lmap m (ldrop (enat k) Sts)) j)
      ∈ mR"
      unfolding St_def St'_def using lnth_lmap
      by (smt enat.distinct(1) enat_add_left_cancel enat_ord_simps(4) inf ldrop_lmap llength_lmap
          lnth_ldrop plus_enat_simps(3))
  }
  then show "∀j. enat (j + 1) < llength (lmap m (ldrop (enat k) Sts)) ⟶
    (λx y. (x, y) ∈ mR)¯¯ (lnth (lmap m (ldrop (enat k) Sts)) j)
      (lnth (lmap m (ldrop (enat k) Sts)) (j + 1))"
    by blast
qed

theorem weighted_RP_fair: "fair_state_seq (lmap state_of_wstate Sts)"
proof (rule ccontr)
  assume asm: "¬ fair_state_seq (lmap state_of_wstate Sts)"
  then have inff: "¬ lfinite Sts" using fair_if_finite
    by auto
  then have inf: "llength Sts = ∞"
    using llength_eq_infty_conv_lfinite by auto
  from asm obtain C where
    "C ∈ Liminf_llist (lmap N_of_state (lmap state_of_wstate Sts))
       ∪ Liminf_llist (lmap P_of_state (lmap state_of_wstate Sts))"
    unfolding fair_state_seq_def Liminf_state_def by auto
  then show False
  proof
    assume "C ∈ Liminf_llist (lmap N_of_state (lmap state_of_wstate Sts))"
    then obtain x where "enat x < llength Sts"
      "∀xa. x ≤ xa ∧ enat xa < llength Sts ⟶ C ∈ N_of_state (state_of_wstate (lnth Sts xa))"
      unfolding Liminf_llist_def by auto
    then have "∃k. ∀j. k ≤ j ⟶ (∃i. (C, i) ∈# wN_of_wstate (lnth Sts j))"
      unfolding Liminf_llist_def by (force simp add: inf N_of_state_state_of_wstate_wN_of_wstate)
    then obtain k where k_p:
      "⋀j. k ≤ j ⟹ ∃i. (C, i) ∈# wN_of_wstate (lnth Sts j)"
      unfolding Liminf_llist_def
      by auto
    have chain_drop_Sts: "chain (↝w) (ldrop k Sts)"
      using deriv inf inff by (simp add: inf_chain_ldropn_chain ldrop_enat)
    have in_N_j: "⋀j. ∃i. (C, i) ∈# wN_of_wstate (lnth (ldrop k Sts) j)"
      using k_p by (simp add: add.commute inf)
    then have "chain (λx y. (x, y) ∈ RP_filtered_relation)¯¯ (lmap (RP_filtered_measure (λCi. True))
      (ldrop k Sts))"
      using inff inf weighted_RP_measure_decreasing_N chain_drop_Sts
        infinite_chain_relation_measure[of "λSt. ∃i. (C, i) ∈# wN_of_wstate St" "(↝w)"] by blast
    then show False
      using wfP_iff_no_infinite_down_chain_llist[of "λx y. (x, y) ∈ RP_filtered_relation"]
        wf_RP_filtered_relation inff
      by (metis (no_types, lifting) inf_llist_lnth ldrop_enat_inf_llist lfinite_inf_llist
        lfinite_lmap wfPUNIVI wf_induct_rule)
  next
    assume asm: "C ∈ Liminf_llist (lmap P_of_state (lmap state_of_wstate Sts))"
    from asm obtain i where i_p:
      "enat i < llength Sts"
      "⋀j. i ≤ j ∧ enat j < llength Sts ⟹ C ∈ P_of_state (state_of_wstate (lnth Sts j))"
      unfolding Liminf_llist_def by auto
    then obtain i where "(C, i) ∈ Liminf_llist (lmap (set_mset ∘ wP_of_wstate) Sts)"
      using persistent_wclause_in_P_if_persistent_clause_in_P[of C] using asm inf by auto
    then have "∃l. ∀k ≥ l. (C, i) ∈ (set_mset ∘ wP_of_wstate) (lnth Sts k)"
      unfolding Liminf_llist_def using inff inf by auto
    then obtain k where k_p:
      "(∀k'≥k. (C, i) ∈ (set_mset ∘ wP_of_wstate) (lnth Sts k'))"
      by blast
    have Ci_in: "∀k'. (C, i) ∈ (set_mset ∘ wP_of_wstate) (lnth (ldrop k Sts) k')"
      using k_p lnth_ldrop[of k _ Sts] inf inff by force
    then have Ci_inn: "∀k'. (C, i) ∈# (wP_of_wstate) (lnth (ldrop k Sts) k')"
      by auto
    have "chain (↝w) (ldrop k Sts)"
      using deriv inf_chain_ldropn_chain inf inff by (simp add: inf_chain_ldropn_chain ldrop_enat)
    then have "chain (λx y. (x, y) ∈ RP_combined_relation)¯¯
      (lmap (RP_combined_measure (weight (C, i))) (ldrop k Sts))"
      using inff inf Ci_in weighted_RP_measure_decreasing_P
        infinite_chain_relation_measure[of "λSt. (C, i) ∈# wP_of_wstate St" "(↝w)"
          "RP_combined_measure (weight (C, i))" ]
      by auto
    then show False
      using wfP_iff_no_infinite_down_chain_llist[of "λx y. (x, y) ∈ RP_combined_relation"]
        wf_RP_combined_relation inff
      by (smt inf_llist_lnth ldrop_enat_inf_llist lfinite_inf_llist lfinite_lmap wfPUNIVI
          wf_induct_rule)
  qed
qed

corollary weighted_RP_saturated: "src.saturated_upto (Liminf_llist (lmap grounding_of_wstate Sts))"
  using RP_saturated_if_fair[OF deriv_RP weighted_RP_fair empty_Q0_RP, unfolded llist.map_comp]
  by simp

corollary weighted_RP_complete:
  "¬ satisfiable (grounding_of_wstate (lhd Sts)) ⟹ {#} ∈ Q_of_state (Liminf_wstate Sts)"
  using RP_complete_if_fair[OF deriv_RP weighted_RP_fair empty_Q0_RP, simplified lhd_lmap_Sts] .

end

end

locale weighted_FO_resolution_prover_with_size_timestamp_factors =
  FO_resolution_prover S subst_atm id_subst comp_subst renamings_apart atm_of_atms mgu less_atm
  for
    S :: "('a :: wellorder) clause ⇒ 'a clause" and
    subst_atm :: "'a ⇒ 's ⇒ 'a" and
    id_subst :: "'s" and
    comp_subst :: "'s ⇒ 's ⇒ 's" and
    renamings_apart :: "'a literal multiset list ⇒ 's list" and
    atm_of_atms :: "'a list ⇒ 'a" and
    mgu :: "'a set set ⇒ 's option" and
    less_atm :: "'a ⇒ 'a ⇒ bool" +
  fixes
    size_atm :: "'a ⇒ nat" and
    size_factor :: nat and
    timestamp_factor :: nat
  assumes
    timestamp_factor_pos: "timestamp_factor > 0"
begin

fun weight :: "'a wclause ⇒ nat" where
  "weight (C, i) = size_factor * size_multiset (size_literal size_atm) C + timestamp_factor * i"

lemma weight_mono: "i < j ⟹ weight (C, i) < weight (C, j)"
  using timestamp_factor_pos by simp

declare weight.simps [simp del]

sublocale wrp: weighted_FO_resolution_prover _ _ _ _ _ _ _ _ weight
  by unfold_locales (rule weight_mono)

notation wrp.weighted_RP (infix "↝w" 50)

end

end