Theory Deterministic_FO_Ordered_Resolution_Prover

(*  Title:       A Deterministic Ordered Resolution Prover for First-Order Clauses
    Author:      Jasmin Blanchette <j.c.blanchette at vu.nl>, 2017
    Author:      Anders Schlichtkrull <andschl at dtu.dk>, 2018
    Maintainer:  Anders Schlichtkrull <andschl at dtu.dk>
*)

section ‹A Deterministic Ordered Resolution Prover for First-Order Clauses›

text ‹
The deterministic_RP› prover introduced below is a deterministic program that works on finite
lists, committing to a strategy for assigning priorities to clauses. However, it is not fully
executable: It abstracts over operations on atoms and employs logical specifications instead of
executable functions for auxiliary notions.
›

theory Deterministic_FO_Ordered_Resolution_Prover
  imports
    Polynomial_Factorization.Missing_List
    Weighted_FO_Ordered_Resolution_Prover
    Lambda_Free_RPOs.Lambda_Free_Util
begin


subsection ‹Library›

lemma apfst_fst_snd: "apfst f x = (f (fst x), snd x)"
  by (rule apfst_conv[of _ "fst x" "snd x" for x, unfolded prod.collapse])

lemma apfst_comp_rpair_const: "apfst f  (λx. (x, y)) = (λx. (x, y))  f"
  by (simp add: comp_def)

(* TODO: Move to Isabelle's "List.thy"? *)
lemma length_remove1_less[termination_simp]: "x  set xs  length (remove1 x xs) < length xs"
  by (induct xs) auto

lemma map_filter_neq_eq_filter_map:
  "map f (filter (λy. f x  f y) xs) = filter (λz. f x  z) (map f xs)"
  by (induct xs) auto

lemma mset_map_remdups_gen:
  "mset (map f (remdups_gen f xs)) = mset (remdups_gen (λx. x) (map f xs))"
  by (induct f xs rule: remdups_gen.induct) (auto simp: map_filter_neq_eq_filter_map)

lemma mset_remdups_gen_ident: "mset (remdups_gen (λx. x) xs) = mset_set (set xs)"
proof -
  have "f = (λx. x)  mset (remdups_gen f xs) = mset_set (set xs)" for f
  proof (induct f xs rule: remdups_gen.induct)
    case (2 f x xs)
    note ih = this(1) and f = this(2)
    show ?case
      unfolding f remdups_gen.simps ih[OF f, unfolded f] mset.simps
      by (metis finite_set list.simps(15) mset_set.insert_remove removeAll_filter_not_eq
          remove_code(1) remove_def)
  qed simp
  then show ?thesis
    by simp
qed

(* TODO: Move to Isabelle? *)
lemma funpow_fixpoint: "f x = x  (f ^^ n) x = x"
  by (induct n) auto

lemma rtranclp_imp_eq_image: "(x y. R x y  f x = f y)  R** x y  f x = f y"
  by (erule rtranclp.induct) auto

lemma tranclp_imp_eq_image: "(x y. R x y  f x = f y)  R++ x y  f x = f y"
  by (erule tranclp.induct) auto


subsection ‹Prover›

type_synonym 'a lclause = "'a literal list"
type_synonym 'a dclause = "'a lclause × nat"
type_synonym 'a dstate = "'a dclause list × 'a dclause list × 'a dclause list × nat"

locale deterministic_FO_resolution_prover =
  weighted_FO_resolution_prover_with_size_timestamp_factors S subst_atm id_subst comp_subst
    renamings_apart atm_of_atms mgu less_atm size_atm timestamp_factor size_factor
  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" and
    size_atm :: "'a  nat" and
    timestamp_factor :: nat and
    size_factor :: nat +
  assumes
    S_empty: "S C = {#}"
begin

lemma less_atm_irrefl: "¬ less_atm A A"
  using ex_ground_subst less_atm_ground less_atm_stable unfolding is_ground_subst_def by blast

fun wstate_of_dstate :: "'a dstate  'a wstate" where
  "wstate_of_dstate (N, P, Q, n) =
   (mset (map (apfst mset) N), mset (map (apfst mset) P), mset (map (apfst mset) Q), n)"

fun state_of_dstate :: "'a dstate  'a state" where
  "state_of_dstate (N, P, Q, _) =
   (set (map (mset  fst) N), set (map (mset  fst) P), set (map (mset  fst) Q))"

abbreviation clss_of_dstate :: "'a dstate  'a clause set" where
  "clss_of_dstate St  clss_of_state (state_of_dstate St)"

fun is_final_dstate :: "'a dstate  bool" where
  "is_final_dstate (N, P, Q, n)  N = []  P = []"

declare is_final_dstate.simps [simp del]

abbreviation rtrancl_weighted_RP (infix "w*" 50) where
  "(↝w*)  (↝w)**"

abbreviation trancl_weighted_RP (infix "w+" 50) where
  "(↝w+)  (↝w)++"

definition is_tautology :: "'a lclause  bool" where
  "is_tautology C  (A  set (map atm_of C). Pos A  set C  Neg A  set C)"

definition subsume :: "'a lclause list  'a lclause  bool" where
  "subsume Ds C  (D  set Ds. subsumes (mset D) (mset C))"

definition strictly_subsume :: "'a lclause list  'a lclause  bool" where
  "strictly_subsume Ds C  (D  set Ds. strictly_subsumes (mset D) (mset C))"

definition is_reducible_on :: "'a literal  'a lclause  'a literal  'a lclause  bool" where
  "is_reducible_on M D L C  subsumes (mset D + {#- M#}) (mset C + {#L#})"

definition is_reducible_lit :: "'a lclause list  'a lclause  'a literal  bool" where
  "is_reducible_lit Ds C L 
   (D  set Ds. L'  set D. σ. - L = L' ⋅l σ  mset (remove1 L' D)  σ ⊆# mset C)"

primrec reduce :: "'a lclause list  'a lclause  'a lclause  'a lclause" where
  "reduce _ _ [] = []"
| "reduce Ds C (L # C') =
   (if is_reducible_lit Ds (C @ C') L then reduce Ds C C' else L # reduce Ds (L # C) C')"

abbreviation is_irreducible :: "'a lclause list  'a lclause  bool" where
  "is_irreducible Ds C  reduce Ds [] C = C"

abbreviation is_reducible :: "'a lclause list  'a lclause  bool" where
  "is_reducible Ds C  reduce Ds [] C  C"

definition reduce_all :: "'a lclause  'a dclause list  'a dclause list" where
  "reduce_all D = map (apfst (reduce [D] []))"

fun reduce_all2 :: "'a lclause  'a dclause list  'a dclause list × 'a dclause list" where
  "reduce_all2 _ [] = ([], [])"
| "reduce_all2 D (Ci # Cs) =
   (let
      (C, i) = Ci;
      C' = reduce [D] [] C
    in
      (if C' = C then apsnd else apfst) (Cons (C', i)) (reduce_all2 D Cs))"

fun remove_all :: "'b list  'b list  'b list" where
  "remove_all xs [] = xs"
| "remove_all xs (y # ys) = (if y  set xs then remove_all (remove1 y xs) ys else remove_all xs ys)"

lemma remove_all_mset_minus: "mset ys ⊆# mset xs  mset (remove_all xs ys) = mset xs - mset ys"
proof (induction ys arbitrary: xs)
  case (Cons y ys)
  show ?case
  proof (cases "y  set xs")
    case y_in: True
    then have subs: "mset ys ⊆# mset (remove1 y xs)"
      using Cons(2) by (simp add: insert_subset_eq_iff)
    show ?thesis
      using y_in Cons subs by auto
  next
    case False
    then show ?thesis
      using Cons by auto
  qed
qed auto

definition resolvent :: "'a lclause  'a 'a lclause  'a lclause  'a lclause" where
  "resolvent D A CA Ls =
   map (λM. M ⋅l (the (mgu {insert A (atms_of (mset Ls))}))) (remove_all CA Ls @ D)"

definition resolvable :: "'a  'a lclause  'a lclause  'a lclause  bool" where
  "resolvable A D CA Ls 
   (let σ = (mgu {insert A (atms_of (mset Ls))}) in
        σ  None
       Ls  []
       maximal_wrt (A ⋅a the σ) ((add_mset (Neg A) (mset D))  the σ)
       strictly_maximal_wrt (A ⋅a the σ) ((mset CA - mset Ls)  the σ)
       (L  set Ls. is_pos L))"

definition resolve_on :: "'a  'a lclause  'a lclause  'a lclause list" where
  "resolve_on A D CA = map (resolvent D A CA) (filter (resolvable A D CA) (subseqs CA))"

definition resolve :: "'a lclause  'a lclause  'a lclause list" where
  "resolve C D =
   concat (map (λL.
     (case L of
        Pos A  []
      | Neg A 
        if maximal_wrt A (mset D) then
          resolve_on A (remove1 L D) C
        else
          [])) D)"

definition resolve_rename :: "'a lclause  'a lclause  'a lclause list" where
  "resolve_rename C D =
   (let σs = renamings_apart [mset D, mset C] in
      resolve (map (λL. L ⋅l last σs) C) (map (λL. L ⋅l hd σs) D))"

definition resolve_rename_either_way :: "'a lclause  'a lclause  'a lclause list" where
  "resolve_rename_either_way C D = resolve_rename C D @ resolve_rename D C"

fun select_min_weight_clause :: "'a dclause  'a dclause list  'a dclause" where
  "select_min_weight_clause Ci [] = Ci"
| "select_min_weight_clause Ci (Dj # Djs) =
   select_min_weight_clause
     (if weight (apfst mset Dj) < weight (apfst mset Ci) then Dj else Ci) Djs"

lemma select_min_weight_clause_in: "select_min_weight_clause P0 P  set (P0 # P)"
  by (induct P arbitrary: P0) auto

function remdups_clss :: "'a dclause list  'a dclause list" where
  "remdups_clss [] = []"
| "remdups_clss (Ci # Cis) =
   (let
      Ci' = select_min_weight_clause Ci Cis
    in
      Ci' # remdups_clss (filter (λ(D, _). mset D  mset (fst Ci')) (Ci # Cis)))"
  by pat_completeness auto
  termination
    apply (relation "measure length")
     apply (rule wf_measure)
    by (metis (mono_tags) in_measure length_filter_less prod.case_eq_if select_min_weight_clause_in)

declare remdups_clss.simps(2) [simp del]

fun deterministic_RP_step :: "'a dstate  'a dstate" where
  "deterministic_RP_step (N, P, Q, n) =
   (if Ci  set (P @ Q). fst Ci = [] then
      ([], [], remdups_clss P @ Q, n + length (remdups_clss P))
    else
      (case N of
        [] 
        (case P of
           []  (N, P, Q, n)
         | P0 # P' 
           let
             (C, i) = select_min_weight_clause P0 P';
             N = map (λD. (D, n)) (remdups_gen mset (resolve_rename C C
               @ concat (map (resolve_rename_either_way C  fst) Q)));
             P = filter (λ(D, j). mset D  mset C) P;
             Q = (C, i) # Q;
             n = Suc n
           in
             (N, P, Q, n))
      | (C, i) # N 
        let
          C = reduce (map fst (P @ Q)) [] C
        in
          if C = [] then
            ([], [], [([], i)], Suc n)
          else if is_tautology C  subsume (map fst (P @ Q)) C then
            (N, P, Q, n)
          else
            let
              P = reduce_all C P;
              (back_to_P, Q) = reduce_all2 C Q;
              P = back_to_P @ P;
              Q = filter (Not  strictly_subsume [C]  fst) Q;
              P = filter (Not  strictly_subsume [C]  fst) P;
              P = (C, i) # P
            in
              (N, P, Q, n)))"

declare deterministic_RP_step.simps [simp del]

partial_function (option) deterministic_RP :: "'a dstate  'a lclause list option" where
  "deterministic_RP St =
   (if is_final_dstate St then
      let (_, _, Q, _) = St in Some (map fst Q)
    else
      deterministic_RP (deterministic_RP_step St))"

lemma is_final_dstate_imp_not_weighted_RP: "is_final_dstate St  ¬ wstate_of_dstate St w St'"
  using wrp.final_weighted_RP
  by (cases St) (auto intro: wrp.final_weighted_RP simp: is_final_dstate.simps)

lemma is_final_dstate_funpow_imp_deterministic_RP_neq_None:
  "is_final_dstate ((deterministic_RP_step ^^ k) St)  deterministic_RP St  None"
proof (induct k arbitrary: St)
  case (Suc k)
  note ih = this(1) and final_Sk = this(2)[simplified, unfolded funpow_swap1]
  show ?case
    using ih[OF final_Sk] by (subst deterministic_RP.simps) (simp add: prod.case_eq_if)
qed (subst deterministic_RP.simps, simp add: prod.case_eq_if)

lemma is_reducible_lit_mono_cls:
  "mset C ⊆# mset C'  is_reducible_lit Ds C L  is_reducible_lit Ds C' L"
  unfolding is_reducible_lit_def by (blast intro: subset_mset.trans)

lemma is_reducible_lit_mset_iff:
  "mset C = mset C'  is_reducible_lit Ds C' L  is_reducible_lit Ds C L"
  by (metis is_reducible_lit_mono_cls subset_mset.order_refl)

lemma is_reducible_lit_remove1_Cons_iff:
  assumes "L  set C'"
  shows "is_reducible_lit Ds (C @ remove1 L (M # C')) L 
    is_reducible_lit Ds (M # C @ remove1 L C') L"
  using assms by (subst is_reducible_lit_mset_iff, auto)

lemma reduce_mset_eq: "mset C = mset C'  reduce Ds C E = reduce Ds C' E"
proof (induct E arbitrary: C C')
  case (Cons L E)
  note ih = this(1) and mset_eq = this(2)
  have
    mset_lc_eq: "mset (L # C) = mset (L # C')" and
    mset_ce_eq: "mset (C @ E) = mset (C' @ E)"
    using mset_eq by simp+
  show ?case
    using ih[OF mset_eq] ih[OF mset_lc_eq] by (simp add: is_reducible_lit_mset_iff[OF mset_ce_eq])
qed simp

lemma reduce_rotate[simp]: "reduce Ds (C @ [L]) E = reduce Ds (L # C) E"
  by (rule reduce_mset_eq) simp

lemma mset_reduce_subset: "mset (reduce Ds C E) ⊆# mset E"
  by (induct E arbitrary: C) (auto intro: subset_mset_imp_subset_add_mset)

lemma reduce_idem: "reduce Ds C (reduce Ds C E) = reduce Ds C E"
  by (induct E arbitrary: C)
    (auto intro!: mset_reduce_subset
      dest!: is_reducible_lit_mono_cls[of "C @ reduce Ds (L # C) E" "C @ E" Ds L for L E C,
        rotated])

lemma is_reducible_lit_imp_is_reducible:
  "L  set C'  is_reducible_lit Ds (C @ remove1 L C') L  reduce Ds C C'  C'"
proof (induct C' arbitrary: C)
  case (Cons M C')
  note ih = this(1) and l_in = this(2) and l_red = this(3)

  show ?case
  proof (cases "is_reducible_lit Ds (C @ C') M")
    case True
    then show ?thesis
      by simp (metis mset.simps(2) mset_reduce_subset multi_self_add_other_not_self
          subset_mset.eq_iff subset_mset_imp_subset_add_mset)
  next
    case m_irred: False
    have
      "L  set C'" and
      "is_reducible_lit Ds (M # C @ remove1 L C') L"
      using l_in l_red m_irred is_reducible_lit_remove1_Cons_iff by auto
    then show ?thesis
      by (simp add: ih[of "M # C"] m_irred)
  qed
qed simp

lemma is_reducible_imp_is_reducible_lit:
  "reduce Ds C C'  C'  L  set C'. is_reducible_lit Ds (C @ remove1 L C') L"
proof (induct C' arbitrary: C)
  case (Cons M C')
  note ih = this(1) and mc'_red = this(2)

  show ?case
  proof (cases "is_reducible_lit Ds (C @ C') M")
    case m_irred: False
    show ?thesis
      using ih[of "M # C"] mc'_red[simplified, simplified m_irred, simplified] m_irred
        is_reducible_lit_remove1_Cons_iff
      by auto
  qed simp
qed simp

lemma is_irreducible_iff_nexists_is_reducible_lit:
  "reduce Ds C C' = C'  ¬ (L  set C'. is_reducible_lit Ds (C @ remove1 L C') L)"
  using is_reducible_imp_is_reducible_lit is_reducible_lit_imp_is_reducible by blast

lemma is_irreducible_mset_iff: "mset E = mset E'  reduce Ds C E = E  reduce Ds C E' = E'"
  unfolding is_irreducible_iff_nexists_is_reducible_lit
  by (metis (full_types) is_reducible_lit_mset_iff mset_remove1 set_mset_mset union_code)

lemma select_min_weight_clause_min_weight:
  assumes "Ci = select_min_weight_clause P0 P"
  shows "weight (apfst mset Ci) = Min ((weight  apfst mset) ` set (P0 # P))"
  using assms
proof (induct P arbitrary: P0 Ci)
  case (Cons P1 P)
  note ih = this(1) and ci = this(2)

  show ?case
  proof (cases "weight (apfst mset P1) < weight (apfst mset P0)")
    case True
    then have min: "Min ((weight  apfst mset) ` set (P0 # P1 # P)) =
      Min ((weight  apfst mset) ` set (P1 # P))"
      by (simp add: min_def)
    show ?thesis
      unfolding min by (rule ih[of Ci P1]) (simp add: ih[of Ci P1] ci True)
  next
    case False
    have "Min ((weight  apfst mset) ` set (P0 # P1 # P)) =
      Min ((weight  apfst mset) ` set (P1 # P0 # P))"
      by (rule arg_cong[of _ _ Min]) auto
    then have min: "Min ((weight  apfst mset) ` set (P0 # P1 # P)) =
      Min ((weight  apfst mset) ` set (P0 # P))"
      by (simp add: min_def) (use False eq_iff in fastforce)
    show ?thesis
      unfolding min by (rule ih[of Ci P0]) (simp add: ih[of Ci P1] ci False)
  qed
qed simp

lemma remdups_clss_Nil_iff: "remdups_clss Cs = []  Cs = []"
  by (cases Cs, simp, hypsubst, subst remdups_clss.simps(2), simp add: Let_def)

lemma empty_N_if_Nil_in_P_or_Q:
  assumes nil_in: "[]  fst ` set (P @ Q)"
  shows "wstate_of_dstate (N, P, Q, n) w* wstate_of_dstate ([], P, Q, n)"
proof (induct N)
  case ih: (Cons N0 N)
  have "wstate_of_dstate (N0 # N, P, Q, n) w wstate_of_dstate (N, P, Q, n)"
    by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(↝w)", OF _ _
          wrp.forward_subsumption[of "{#}" "mset (map (apfst mset) P)" "mset (map (apfst mset) Q)"
            "mset (fst N0)" "mset (map (apfst mset) N)" "snd N0" n]])
      (use nil_in in force simp: image_def apfst_fst_snd)+
  then show ?case
    using ih by (rule converse_rtranclp_into_rtranclp)
qed simp

lemma remove_strictly_subsumed_clauses_in_P:
  assumes
    c_in: "C  fst ` set N" and
    p_nsubs: "D  fst ` set P. ¬ strictly_subsume [C] D"
  shows "wstate_of_dstate (N, P @ P', Q, n)
    w* wstate_of_dstate (N, P @ filter (Not  strictly_subsume [C]  fst) P', Q, n)"
  using p_nsubs
proof (induct "length P'" arbitrary: P P' rule: less_induct)
  case less
  note ih = this(1) and p_nsubs = this(2)

  show ?case
  proof (cases "length P'")
    case Suc

    let ?Dj = "hd P'"
    let ?P'' = "tl P'"
    have p': "P' = hd P' # tl P'"
      using Suc by (metis length_Suc_conv list.distinct(1) list.exhaust_sel)

    show ?thesis
    proof (cases "strictly_subsume [C] (fst ?Dj)")
      case subs: True

      have p_filtered: "{#(E, k) ∈# image_mset (apfst mset) (mset P). E  mset (fst ?Dj)#} =
        image_mset (apfst mset) (mset P)"
        by (rule filter_mset_cong[OF refl, of _ _ "λ_. True", simplified],
            use subs p_nsubs in auto simp: strictly_subsume_def)
      have "{#(E, k) ∈# image_mset (apfst mset) (mset P'). E  mset (fst ?Dj)#} =
        {#(E, k) ∈# image_mset (apfst mset) (mset ?P''). E  mset (fst ?Dj)#}"
        by (subst (2) p') (simp add: case_prod_beta)
      also have " =
        image_mset (apfst mset) (mset (filter (λ(E, l). mset E  mset (fst ?Dj)) ?P''))"
        by (auto simp: image_mset_filter_swap[symmetric] case_prod_beta)
      finally have p'_filtered:
        "{#(E, k) ∈# image_mset (apfst mset) (mset P'). E  mset (fst ?Dj)#} =
        image_mset (apfst mset) (mset (filter (λ(E, l). mset E  mset (fst ?Dj)) ?P''))"
        .

      have "wstate_of_dstate (N, P @ P', Q, n)
        w wstate_of_dstate (N, P @ filter (λ(E, l). mset E  mset (fst ?Dj)) ?P'', Q, n)"
        by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(↝w)", OF _ _
              wrp.backward_subsumption_P[of "mset C" "mset (map (apfst mset) N)" "mset (fst ?Dj)"
                "mset (map (apfst mset) (P @ P'))" "mset (map (apfst mset) Q)" n]],
          use c_in subs in auto simp add: p_filtered p'_filtered arg_cong[OF p', of set]
            strictly_subsume_def)
      also have "
        w* wstate_of_dstate (N, P @ filter (Not  strictly_subsume [C]  fst) P', Q, n)"
        apply (rule arg_cong2[THEN iffD1, of _ _ _ _ "(↝w*)", OF _ _
              ih[of "filter (λ(E, l). mset E  mset (fst ?Dj)) ?P''" P]])
           apply simp_all
          apply (subst (3) p')
        using subs
          apply (simp add: case_prod_beta)
          apply (rule arg_cong[of _ _ "λx. image_mset (apfst mset) x"])
        apply (metis (no_types, opaque_lifting) strictly_subsume_def)
         apply (subst (3) p')
         apply (subst list.size)
         apply (metis (no_types, lifting) less_Suc0 less_add_same_cancel1 linorder_neqE_nat
            not_add_less1 sum_length_filter_compl trans_less_add1)
        using p_nsubs by fast
      ultimately show ?thesis
        by (rule converse_rtranclp_into_rtranclp)
    next
      case nsubs: False
      show ?thesis
        apply (rule arg_cong2[THEN iffD1, of _ _ _ _ "(↝w*)", OF _ _
              ih[of ?P'' "P @ [?Dj]"]])
        using nsubs p_nsubs
           apply (simp_all add: arg_cong[OF p', of mset] arg_cong[OF p', of "filter f" for f])
        apply (subst (1 2) p')
        by simp
    qed
  qed simp
qed

lemma remove_strictly_subsumed_clauses_in_Q:
  assumes c_in: "C  fst ` set N"
  shows "wstate_of_dstate (N, P, Q @ Q', n)
    w* wstate_of_dstate (N, P, Q @ filter (Not  strictly_subsume [C]  fst) Q', n)"
proof (induct Q' arbitrary: Q)
  case ih: (Cons Dj Q')
  have "wstate_of_dstate (N, P, Q @ Dj # Q', n) w*
    wstate_of_dstate (N, P, Q @ filter (Not  strictly_subsume [C]  fst) [Dj] @ Q', n)"
  proof (cases "strictly_subsume [C] (fst Dj)")
    case subs: True
    have "wstate_of_dstate (N, P, Q @ Dj # Q', n) w wstate_of_dstate (N, P, Q @ Q', n)"
      by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(↝w)", OF _ _
            wrp.backward_subsumption_Q[of "mset C" "mset (map (apfst mset) N)" "mset (fst Dj)"
              "mset (map (apfst mset) P)" "mset (map (apfst mset) (Q @ Q'))" "snd Dj" n]])
        (use c_in subs in auto simp: apfst_fst_snd strictly_subsume_def)
    then show ?thesis
      by auto
  qed simp
  then show ?case
    using ih[of "Q @ filter (Not  strictly_subsume [C]  fst) [Dj]"] by force
qed simp

lemma reduce_clause_in_P:
  assumes
    c_in: "C  fst ` set N" and
    p_irred: "(E, k)  set (P @ P'). k > j  is_irreducible [C] E"
  shows "wstate_of_dstate (N, P @ (D @ D', j) # P', Q, n)
    w* wstate_of_dstate (N, P @ (D @ reduce [C] D D', j) # P', Q, n)"
proof (induct D' arbitrary: D)
  case ih: (Cons L D')
  show ?case
  proof (cases "is_reducible_lit [C] (D @ D') L")
    case l_red: True
    then obtain L' :: "'a literal" and σ :: 's where
      l'_in: "L'  set C" and
      not_l: "- L = L' ⋅l σ" and
      subs: "mset (remove1 L' C)  σ ⊆# mset (D @ D')"
      unfolding is_reducible_lit_def by force

    have ldd'_red: "is_reducible [C] (L # D @ D')"
      apply (rule is_reducible_lit_imp_is_reducible)
      using l_red by auto

    have lt_imp_neq: "(E, k)  set (P @ P'). j < k  mset E  mset (L # D @ D')"
      using p_irred ldd'_red is_irreducible_mset_iff by fast

    have "wstate_of_dstate (N, P @ (D @ L # D', j) # P', Q, n)
      w wstate_of_dstate (N, P @ (D @ D', j) # P', Q, n)"
      apply (rule arg_cong2[THEN iffD1, of _ _ _ _ "(↝w)", OF _ _
            wrp.backward_reduction_P[of "mset C - {#L'#}" L' "mset (map (apfst mset) N)" L σ
              "mset (D @ D')" "mset (map (apfst mset) (P @ P'))" j "mset (map (apfst mset) Q)" n]])
      using l'_in not_l subs c_in lt_imp_neq by (simp_all add: case_prod_beta) force+
    then show ?thesis
      using ih[of D] l_red by simp
  next
    case False
    then show ?thesis
      using ih[of "D @ [L]"] by simp
  qed
qed simp

lemma reduce_clause_in_Q:
  assumes
    c_in: "C  fst ` set N" and
    p_irred: "(E, k)  set P. k > j  is_irreducible [C] E" and
    d'_red: "reduce [C] D D'  D'"
  shows "wstate_of_dstate (N, P, Q @ (D @ D', j) # Q', n)
    w* wstate_of_dstate (N, (D @ reduce [C] D D', j) # P, Q @ Q', n)"
  using d'_red
proof (induct D' arbitrary: D)
  case (Cons L D')
  note ih = this(1) and ld'_red = this(2)
  then show ?case
  proof (cases "is_reducible_lit [C] (D @ D') L")
    case l_red: True
    then obtain L' :: "'a literal" and σ :: 's where
      l'_in: "L'  set C" and
      not_l: "- L = L' ⋅l σ" and
      subs: "mset (remove1 L' C)  σ ⊆# mset (D @ D')"
      unfolding is_reducible_lit_def by force

    have "wstate_of_dstate (N, P, Q @ (D @ L # D', j) # Q', n)
      w wstate_of_dstate (N, (D @ D', j) # P, Q @ Q', n)"
      by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(↝w)", OF _ _
            wrp.backward_reduction_Q[of "mset C - {#L'#}" L' "mset (map (apfst mset) N)" L σ
              "mset (D @ D')" "mset (map (apfst mset) P)" "mset (map (apfst mset) (Q @ Q'))" j n]],
          use l'_in not_l subs c_in in auto)
    then show ?thesis
      using l_red p_irred reduce_clause_in_P[OF c_in, of "[]" P j D D' "Q @ Q'" n] by simp
  next
    case l_nred: False
    then have d'_red: "reduce [C] (D @ [L]) D'  D'"
      using ld'_red by simp
    show ?thesis
      using ih[OF d'_red] l_nred by simp
  qed
qed simp

lemma reduce_clauses_in_P:
  assumes
    c_in: "C  fst ` set N" and
    p_irred: "(E, k)  set P. is_irreducible [C] E"
  shows "wstate_of_dstate (N, P @ P', Q, n) w* wstate_of_dstate (N, P @ reduce_all C P', Q, n)"
  unfolding reduce_all_def
  using p_irred
proof (induct "length P'" arbitrary: P P')
  case (Suc l)
  note ih = this(1) and suc_l = this(2) and p_irred = this(3)

  have p'_nnil: "P'  []"
    using suc_l by auto

  define j :: nat where
    "j = Max (snd ` set P')"

  obtain Dj :: "'a dclause" where
    dj_in: "Dj  set P'" and
    snd_dj: "snd Dj = j"
    using Max_in[of "snd ` set P'", unfolded image_def, simplified]
    by (metis image_def j_def length_Suc_conv list.set_intros(1) suc_l)

  have "k  snd ` set P'. k  j"
    unfolding j_def using p'_nnil by simp
  then have j_max: "(E, k)  set P'. j  k"
    unfolding image_def by fastforce

  obtain P1' P2' :: "'a dclause list"  where
    p': "P' = P1' @ Dj # P2'"
    using split_list[OF dj_in] by blast

  have "wstate_of_dstate (N, P @ P1' @ Dj # P2', Q, n)
     w* wstate_of_dstate (N, P @ P1' @ apfst (reduce [C] []) Dj # P2', Q, n)"
    unfolding append_assoc[symmetric]
    apply (subst (1 2) surjective_pairing[of Dj, unfolded snd_dj])
    apply (simp only: apfst_conv)
    apply (rule reduce_clause_in_P[of _ _ _ _ _ "[]", unfolded append_Nil, OF c_in])
    using p_irred j_max[unfolded p'] by (force simp: case_prod_beta)
  moreover have "wstate_of_dstate (N, P @ P1' @ apfst (reduce [C] []) Dj # P2', Q, n)
     w* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) (P1' @ Dj # P2'), Q, n)"
    apply (rule arg_cong2[THEN iffD1, of _ _ _ _ "(↝w*)", OF _ _
          ih[of "P1' @ P2'" "apfst (reduce [C] []) Dj # P"]])
    using suc_l reduce_idem p_irred unfolding p' by (auto simp: case_prod_beta)
  ultimately show ?case
    unfolding p' by simp
qed simp

lemma reduce_clauses_in_Q:
  assumes
    c_in: "C  fst ` set N" and
    p_irred: "(E, k)  set P. is_irreducible [C] E"
  shows "wstate_of_dstate (N, P, Q @ Q', n)
    w* wstate_of_dstate (N, fst (reduce_all2 C Q') @ P, Q @ snd (reduce_all2 C Q'), n)"
  using p_irred
proof (induct Q' arbitrary: P Q)
  case (Cons Dj Q')
  note ih = this(1) and p_irred = this(2)
  show ?case
  proof (cases "is_irreducible [C] (fst Dj)")
    case True
    then show ?thesis
      using ih[of _ "Q @ [Dj]"] p_irred by (simp add: case_prod_beta)
  next
    case d_red: False
    have "wstate_of_dstate (N, P, Q @ Dj # Q', n)
      w* wstate_of_dstate (N, (reduce [C] [] (fst Dj), snd Dj) # P, Q @ Q', n)"
      using p_irred reduce_clause_in_Q[of _ _ P "snd Dj" "[]" _ Q Q' n, OF c_in _ d_red]
      by (cases Dj) force
    then show ?thesis
      using ih[of "(reduce [C] [] (fst Dj), snd Dj) # P" Q] d_red p_irred reduce_idem
      by (force simp: case_prod_beta)
  qed
qed simp

lemma eligible_iff:
  "eligible S σ As DA  As = []  length As = 1  maximal_wrt (hd As ⋅a σ) (DA  σ)"
  unfolding eligible.simps S_empty by (fastforce dest: hd_conv_nth)

lemma ord_resolve_one_side_prem:
  "ord_resolve S CAs DA AAs As σ E  length CAs = 1  length AAs = 1  length As = 1"
  by (force elim!: ord_resolve.cases simp: eligible_iff)

lemma ord_resolve_rename_one_side_prem:
  "ord_resolve_rename S CAs DA AAs As σ E  length CAs = 1  length AAs = 1  length As = 1"
  by (force elim!: ord_resolve_rename.cases dest: ord_resolve_one_side_prem)

abbreviation Bin_ord_resolve :: "'a clause  'a clause  'a clause set" where
  "Bin_ord_resolve C D  {E. AA A σ. ord_resolve S [C] D [AA] [A] σ E}"

abbreviation Bin_ord_resolve_rename :: "'a clause  'a clause  'a clause set" where
  "Bin_ord_resolve_rename C D  {E. AA A σ. ord_resolve_rename S [C] D [AA] [A] σ E}"

lemma resolve_on_eq_UNION_Bin_ord_resolve:
  "mset ` set (resolve_on A D CA) =
   {E. AA σ. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] σ E}"
proof
  {
    fix E :: "'a literal list"
    assume "E  set (resolve_on A D CA)"
    then have "E  resolvent D A CA ` {Ls. subseq Ls CA  resolvable A D CA Ls}"
      unfolding resolve_on_def by simp
    then obtain Ls where Ls_p: "resolvent D A CA Ls = E" "subseq Ls CA  resolvable A D CA Ls"
      by auto
    define σ where "σ = the (mgu {insert A (atms_of (mset Ls))})"
    then have σ_p:
      "mgu {insert A (atms_of (mset Ls))} = Some σ"
      "Ls  []"
      "eligible S σ [A] (add_mset (Neg A) (mset D))"
      "strictly_maximal_wrt (A ⋅a σ) ((mset CA - mset Ls)  σ)"
      "L  set Ls. is_pos L"
      using Ls_p unfolding resolvable_def unfolding Let_def eligible.simps using S_empty by auto
    from σ_p have σ_p2: "the (mgu {insert A (atms_of (mset Ls))}) = σ"
      by auto
    have Ls_sub_CA: "mset Ls ⊆# mset CA"
      using subseq_mset_subseteq_mset Ls_p by auto
    then have "mset (resolvent D A CA Ls) = sum_list [mset CA - mset Ls]  σ + mset D  σ"
      unfolding resolvent_def σ_p2 subst_cls_def using remove_all_mset_minus[of Ls CA] by auto
    moreover
    have "length [mset CA - mset Ls] = Suc 0"
      by auto
    moreover
    have "L  set Ls. is_pos L"
      using σ_p(5) list_all_iff[of is_pos] by auto
    then have "{#Pos (atm_of x). x ∈# mset Ls#} = mset Ls"
      by (induction Ls) auto
    then have "mset CA = [mset CA - mset Ls] ! 0 + {#Pos (atm_of x). x ∈# mset Ls#}"
      using Ls_sub_CA by auto
    moreover
    have "Ls  []"
      using σ_p by -
    moreover
    have "Some σ = mgu {insert A (atm_of ` set Ls)}"
      using σ_p unfolding atms_of_def by auto
    moreover
    have "eligible S σ [A] (add_mset (Neg A) (mset D))"
      using σ_p by -
    moreover
    have "strictly_maximal_wrt (A ⋅a σ) ([mset CA - mset Ls] ! 0  σ)"
      using σ_p(4) by auto
    moreover have "S (mset CA) = {#}"
      by (simp add: S_empty)
    ultimately have "Cs. mset (resolvent D A CA Ls) = sum_list Cs  σ + mset D  σ
         length Cs = Suc 0  mset CA = Cs ! 0 + {#Pos (atm_of x). x ∈# mset Ls#}
         Ls  []  Some σ = mgu {insert A (atm_of ` set Ls)}
         eligible S σ [A] (add_mset (Neg A) (mset D))  strictly_maximal_wrt (A ⋅a σ) (Cs ! 0  σ)
         S (mset CA) = {#}"
      by blast
    then have "ord_resolve S [mset CA] (add_mset (Neg A) (mset D)) [image_mset atm_of (mset Ls)] [A]
      σ (mset (resolvent D A CA Ls))"
      unfolding ord_resolve.simps by auto
    then have "AA σ. ord_resolve S [mset CA] (add_mset (Neg A) (mset D)) [AA] [A] σ (mset E)"
      using Ls_p by auto
  }
  then show "mset ` set (resolve_on A D CA)
     {E. AA σ. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] σ E}"
    by auto
next
  {
    fix E AA σ
    assume "ord_resolve S [mset CA] (add_mset (Neg A) (mset D)) [AA] [A] σ E"
    then obtain Cs where res': "E = sum_list Cs  σ + mset D  σ"
      "length Cs = Suc 0"
      "mset CA = Cs ! 0 + poss AA"
      "AA  {#}"
      "Some σ = mgu {insert A (set_mset AA)}"
      "eligible S σ [A] (add_mset (Neg A) (mset D))"
      "strictly_maximal_wrt (A ⋅a σ) (Cs ! 0  σ)"
      "S (Cs ! 0 + poss AA) = {#}"
      unfolding ord_resolve.simps by auto
    moreover define C where "C = Cs ! 0"
    ultimately have res:
      "E = sum_list Cs  σ + mset D  σ"
      "mset CA = C + poss AA"
      "AA  {#}"
      "Some σ = mgu {insert A (set_mset AA)}"
      "eligible S σ [A] (add_mset (Neg A) (mset D))"
      "strictly_maximal_wrt (A ⋅a σ) (C  σ)"
      "S (C + poss AA) = {#}"
      unfolding ord_resolve.simps by auto
    from this(1) have
      "E = C  σ + mset D  σ"
      unfolding C_def using res'(2) by (cases Cs) auto
    note res' = this res(2-7)
    have "Al. mset Al = AA  subseq (map Pos Al) CA"
      using res(2)
    proof (induction CA arbitrary: AA C)
      case Nil
      then show ?case by auto
    next
      case (Cons L CA)
      then show ?case
      proof (cases "L ∈# poss AA ")
        case True
        then have pos_L: "is_pos L"
          by auto
        have rem: "A'. Pos A' ∈# poss AA 
          remove1_mset (Pos A') (C + poss AA) = C + poss (remove1_mset A' AA)"
          by (induct AA) auto
        have "mset CA = C + (poss (AA - {#atm_of L#}))"
          using True Cons(2)
          by (metis add_mset_remove_trivial rem literal.collapse(1) mset.simps(2) pos_L)
        then have "Al. mset Al = remove1_mset (atm_of L) AA  subseq (map Pos Al) CA"
          using Cons(1)[of _ "((AA - {#atm_of L#}))"] by metis
        then obtain Al where
          "mset Al = remove1_mset (atm_of L) AA  subseq (map Pos Al) CA"
          by auto
        then have
          "mset (atm_of L # Al) = AA" and
          "subseq (map Pos (atm_of L # Al)) (L # CA)"
          using True by (auto simp add: pos_L)
        then show ?thesis
          by blast
      next
        case False
        then have "mset CA = remove1_mset L C + poss AA"
          using Cons(2)
          by (metis Un_iff add_mset_remove_trivial mset.simps(2) set_mset_union single_subset_iff
              subset_mset.add_diff_assoc2 union_single_eq_member)
        then have "Al. mset Al = AA  subseq (map Pos Al) CA"
          using Cons(1)[of "C - {#L#}" AA] Cons(2) by auto
        then show ?thesis
          by auto
      qed
    qed
    then obtain Al where Al_p: "mset Al = AA" "subseq (map Pos Al) CA"
      by auto

    define Ls :: "'a lclause" where "Ls = map Pos Al"
    have diff: "mset CA - mset Ls = C"
      unfolding Ls_def using res(2) Al_p(1) by auto
    have ls_subq_ca: "subseq Ls CA"
      unfolding Ls_def using Al_p by -
    moreover
    {
      have "y. mgu {insert A (atms_of (mset Ls))} = Some y"
        unfolding Ls_def using res(4) Al_p by (metis atms_of_poss mset_map)
      moreover have "Ls  []"
        using Al_p(1) Ls_def res'(3) by auto
      moreover have σ_p: "the (mgu {insert A (set Al)}) = σ"
        using res'(4) Al_p(1) by (metis option.sel  set_mset_mset)
      then have "eligible S (the (mgu {insert A (atms_of (mset Ls))})) [A]
        (add_mset (Neg A) (mset D))"
        unfolding Ls_def using res  by auto
      moreover have "strictly_maximal_wrt (A ⋅a the (mgu {insert A (atms_of (mset Ls))}))
        ((mset CA - mset Ls)  the (mgu {insert A (atms_of (mset Ls))}))"
        unfolding Ls_def using res σ_p Al_p by auto
      moreover have "L  set Ls. is_pos L"
        by (simp add: Ls_def)
      ultimately have "resolvable A D CA Ls"
        unfolding resolvable_def unfolding eligible.simps using S_empty by simp
    }
    moreover have ls_sub_ca: "mset Ls ⊆# mset CA"
      using ls_subq_ca subseq_mset_subseteq_mset[of Ls CA] by simp
    have "{#x ⋅l σ. x ∈# mset CA - mset Ls#} + {#M ⋅l σ. M ∈# mset D#} = C  σ + mset D  σ"
      using diff unfolding subst_cls_def by simp
    then have "{#x ⋅l σ. x ∈# mset CA - mset Ls#} + {#M ⋅l σ. M ∈# mset D#} = E"
      using res'(1) by auto
    then have "{#M ⋅l σ. M ∈# mset (remove_all CA Ls)#} + {#M ⋅l σ . M ∈# mset D#} = E"
      using remove_all_mset_minus[of Ls CA] ls_sub_ca by auto
    then have "mset (resolvent D A CA Ls) = E"
      unfolding resolvable_def Let_def resolvent_def using Al_p(1) Ls_def atms_of_poss res'(4)
      by (metis image_mset_union mset_append mset_map option.sel)
    ultimately have "E  mset ` set (resolve_on A D CA)"
      unfolding resolve_on_def by auto
  }
  then show "{E. AA σ. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] σ E}
     mset ` set (resolve_on A D CA)"
    by auto
qed

lemma set_resolve_eq_UNION_set_resolve_on:
  "set (resolve C D) =
   (L  set D.
      (case L of
         Pos _  {}
       | Neg A  if maximal_wrt A (mset D) then set (resolve_on A (remove1 L D) C) else {}))"
  unfolding resolve_def by (fastforce split: literal.splits if_splits)

lemma resolve_eq_Bin_ord_resolve: "mset ` set (resolve C D) = Bin_ord_resolve (mset C) (mset D)"
  unfolding set_resolve_eq_UNION_set_resolve_on
  apply (unfold image_UN literal.case_distrib if_distrib)
  apply (subst resolve_on_eq_UNION_Bin_ord_resolve)
  apply (rule order_antisym)
   apply (force split: literal.splits if_splits)
  apply (clarsimp split: literal.splits if_splits)
  apply (rule_tac x = "Neg A" in bexI)
   apply (rule conjI)
    apply blast
   apply clarify
   apply (rule conjI)
    apply clarify
    apply (rule_tac x = AA in exI)
    apply (rule_tac x = σ in exI)
    apply (frule ord_resolve.simps[THEN iffD1])
    apply force
   apply (drule ord_resolve.simps[THEN iffD1])
   apply (clarsimp simp: eligible_iff simp del: subst_cls_add_mset subst_cls_union)
   apply (drule maximal_wrt_subst)
   apply sat
  apply (drule ord_resolve.simps[THEN iffD1])
  using set_mset_mset by fastforce

lemma poss_in_map_clauseD:
  "poss AA ⊆# map_clause f C  AA0. poss AA0 ⊆# C  AA = {#f A. A ∈# AA0#}"
proof (induct AA arbitrary: C)
  case (add A AA)
  note ih = this(1) and aaa_sub = this(2)

  have "Pos A ∈# map_clause f C"
    using aaa_sub by auto
  then obtain A0 where
    pa0_in: "Pos A0 ∈# C" and
    a: "A = f A0"
    by clarify (metis literal.distinct(1) literal.exhaust literal.inject(1) literal.simps(9,10))

  have "poss AA ⊆# map_clause f (C - {#Pos A0#})"
    using pa0_in aaa_sub[unfolded a] by (simp add: image_mset_remove1_mset_if insert_subset_eq_iff)
  then obtain AA0 where
    paa0_sub: "poss AA0 ⊆# C - {#Pos A0#}" and
    aa: "AA = image_mset f AA0"
    using ih by meson

  have "poss (add_mset A0 AA0) ⊆# C"
    using pa0_in paa0_sub by (simp add: insert_subset_eq_iff)
  moreover have "add_mset A AA = image_mset f (add_mset A0 AA0)"
    unfolding a aa by simp
  ultimately show ?case
    by blast
qed simp

lemma poss_subset_filterD:
  "poss AA ⊆# {#L ⋅l ρ. L ∈# mset C#}  AA0. poss AA0 ⊆# mset C  AA = AA0 ⋅am ρ"
  unfolding subst_atm_mset_def subst_lit_def by (rule poss_in_map_clauseD)

lemma neg_in_map_literalD: "Neg A  map_literal f ` D  A0. Neg A0  D  A = f A0"
  unfolding image_def by (clarify, case_tac x, auto)

lemma neg_in_filterD: "Neg A ∈# {#L ⋅l ρ'. L ∈# mset D#}  A0. Neg A0 ∈# mset D  A = A0 ⋅a ρ'"
  unfolding subst_lit_def image_def by (rule neg_in_map_literalD) simp

lemma resolve_rename_eq_Bin_ord_resolve_rename:
  "mset ` set (resolve_rename C D) = Bin_ord_resolve_rename (mset C) (mset D)"
proof (intro order_antisym subsetI)
  let ?ρs = "renamings_apart [mset D, mset C]"
  define ρ' :: 's where
    "ρ' = hd ?ρs"
  define ρ :: 's where
    "ρ = last ?ρs"

  have tl_ρs: "tl ?ρs = [ρ]"
    unfolding ρ_def
    using renamings_apart_length Nitpick.size_list_simp(2) Suc_length_conv last.simps
    by (smt length_greater_0_conv list.sel(3))

  {
    fix E
    assume e_in: "E  mset ` set (resolve_rename C D)"

    from e_in obtain AA :: "'a multiset" and A :: 'a and σ :: 's where
      aa_sub: "poss AA ⊆# mset C  ρ" and
      a_in: "Neg A ∈# mset D  ρ'" and
      res_e: "ord_resolve S [mset C  ρ] {#L ⋅l ρ'. L ∈# mset D#} [AA] [A] σ E"
      unfolding ρ'_def ρ_def
      apply atomize_elim
      using e_in unfolding resolve_rename_def Let_def resolve_eq_Bin_ord_resolve
      apply clarsimp
      apply (frule ord_resolve_one_side_prem)
      apply (frule ord_resolve.simps[THEN iffD1])
      apply (rule_tac x = AA in exI)
      apply (clarsimp simp: subst_cls_def)
      apply (rule_tac x = A in exI)
      by (metis (full_types) Melem_subst_cls set_mset_mset subst_cls_def union_single_eq_member)

    obtain AA0 :: "'a multiset" where
      aa0_sub: "poss AA0 ⊆# mset C" and
      aa: "AA = AA0 ⋅am ρ"
      using aa_sub
      apply atomize_elim
      apply (rule ord_resolve.cases[OF res_e])
      by (rule poss_subset_filterD[OF aa_sub[unfolded subst_cls_def]])

    obtain A0 :: 'a where
      a0_in: "Neg A0  set D" and
      a: "A = A0 ⋅a ρ'"
      apply atomize_elim
      apply (rule ord_resolve.cases[OF res_e])
      using neg_in_filterD[OF a_in[unfolded subst_cls_def]] by simp

    show "E  Bin_ord_resolve_rename (mset C) (mset D)"
      unfolding ord_resolve_rename.simps
      using res_e
      apply clarsimp
      apply (rule_tac x = AA0 in exI)
      apply (intro conjI)
       apply (rule aa0_sub)
      apply (rule_tac x = A0 in exI)
      apply (intro conjI)
       apply (rule a0_in)
      apply (rule_tac x = σ in exI)
      unfolding aa a ρ'_def[symmetric] ρ_def[symmetric] tl_ρs by (simp add: subst_cls_def)
  }
  {
    fix E
    assume e_in: "E  Bin_ord_resolve_rename (mset C) (mset D)"
    show "E  mset ` set (resolve_rename C D)"
      using e_in
      unfolding resolve_rename_def Let_def resolve_eq_Bin_ord_resolve ord_resolve_rename.simps
      apply clarsimp
      apply (rule_tac x = "AA ⋅am ρ" in exI)
      apply (rule_tac x = "A ⋅a ρ'" in exI)
      apply (rule_tac x = σ in exI)
      unfolding tl_ρs ρ'_def ρ_def by (simp add: subst_cls_def subst_cls_lists_def)
  }
qed

lemma bin_ord_FO_Γ_def:
  "ord_FO_Γ S = {Infer {#CA#} DA E | CA DA AA A σ E. ord_resolve_rename S [CA] DA [AA] [A] σ E}"
  unfolding ord_FO_Γ_def
  apply (rule order.antisym)
   apply clarify
   apply (frule ord_resolve_rename_one_side_prem)
   apply simp
   apply (metis Suc_length_conv length_0_conv)
  by blast

lemma ord_FO_Γ_side_prem: "γ  ord_FO_Γ S  side_prems_of γ = {#THE D. D ∈# side_prems_of γ#}"
  unfolding bin_ord_FO_Γ_def by clarsimp

lemma ord_FO_Γ_infer_from_Collect_eq:
  "{γ  ord_FO_Γ S. infer_from (DD  {C}) γ  C ∈# prems_of γ} =
   {γ  ord_FO_Γ S. D  DD  {C}. prems_of γ = {#C, D#}}"
  unfolding infer_from_def
  apply (rule set_eq_subset[THEN iffD2])
  apply (rule conjI)
   apply clarify
   apply (subst (asm) (1 2) ord_FO_Γ_side_prem, assumption, assumption)
   apply (subst (1) ord_FO_Γ_side_prem, assumption)
   apply force
  apply clarify
  apply (subst (asm) (1) ord_FO_Γ_side_prem, assumption)
  apply (subst (1 2) ord_FO_Γ_side_prem, assumption)
  by force

lemma inferences_between_eq_UNION: "inference_system.inferences_between (ord_FO_Γ S) Q C =
  inference_system.inferences_between (ord_FO_Γ S) {C} C
   (D  Q. inference_system.inferences_between (ord_FO_Γ S) {D} C)"
  unfolding ord_FO_Γ_infer_from_Collect_eq inference_system.inferences_between_def by auto

lemma concls_of_inferences_between_singleton_eq_Bin_ord_resolve_rename:
  "concls_of (inference_system.inferences_between (ord_FO_Γ S) {D} C) =
   Bin_ord_resolve_rename C C  Bin_ord_resolve_rename C D  Bin_ord_resolve_rename D C"
proof (intro order_antisym subsetI)
  fix E
  assume e_in: "E  concls_of (inference_system.inferences_between (ord_FO_Γ S) {D} C)"
  then show "E  Bin_ord_resolve_rename C C  Bin_ord_resolve_rename C D
     Bin_ord_resolve_rename D C"
    unfolding inference_system.inferences_between_def ord_FO_Γ_infer_from_Collect_eq
      bin_ord_FO_Γ_def infer_from_def by (fastforce simp: add_mset_eq_add_mset)
qed (force simp: inference_system.inferences_between_def infer_from_def ord_FO_Γ_def)

lemma concls_of_inferences_between_eq_Bin_ord_resolve_rename:
  "concls_of (inference_system.inferences_between (ord_FO_Γ S) Q C) =
   Bin_ord_resolve_rename C C  (D  Q. Bin_ord_resolve_rename C D  Bin_ord_resolve_rename D C)"
  by (subst inferences_between_eq_UNION)
    (auto simp: image_Un image_UN concls_of_inferences_between_singleton_eq_Bin_ord_resolve_rename)

lemma resolve_rename_either_way_eq_congls_of_inferences_between:
  "mset ` set (resolve_rename C C)  (D  Q. mset ` set (resolve_rename_either_way C D)) =
   concls_of (inference_system.inferences_between (ord_FO_Γ S) (mset ` Q) (mset C))"
  by (simp add: resolve_rename_either_way_def image_Un resolve_rename_eq_Bin_ord_resolve_rename
      concls_of_inferences_between_eq_Bin_ord_resolve_rename UN_Un_distrib)

lemma compute_inferences:
  assumes
    ci_in: "(C, i)  set P" and
    ci_min: "(D, j) ∈# mset (map (apfst mset) P). weight (mset C, i)  weight (D, j)"
  shows
    "wstate_of_dstate ([], P, Q, n) w
     wstate_of_dstate (map (λD. (D, n)) (remdups_gen mset (resolve_rename C C @
         concat (map (resolve_rename_either_way C  fst) Q))),
       filter (λ(D, j). mset D  mset C) P, (C, i) # Q, Suc n)"
    (is "_ w wstate_of_dstate (?N, _)")
proof -
  have ms_ci_in: "(mset C, i) ∈# image_mset (apfst mset) (mset P)"
    using ci_in by force

  show ?thesis
    apply (rule arg_cong2[THEN iffD1, of _ _ _ _ "(↝w)", OF _ _
          wrp.inference_computation[of "mset (map (apfst mset) P) - {#(mset C, i)#}" "mset C" i
            "mset (map (apfst mset) ?N)" n "mset (map (apfst mset) Q)"]])
       apply (simp add: add_mset_remove_trivial_eq[THEN iffD2, OF ms_ci_in, symmetric])
    using ms_ci_in
      apply (simp add: ci_in image_mset_remove1_mset_if)
      apply (smt apfst_conv case_prodE case_prodI2 case_prod_conv filter_mset_cong
        image_mset_filter_swap mset_filter)
     apply (metis ci_min in_diffD)
    apply (simp only: list.map_comp apfst_comp_rpair_const)
    apply (simp only: list.map_comp[symmetric])
    apply (subst mset_map)
    apply (unfold mset_map_remdups_gen mset_remdups_gen_ident)
    apply (subst image_mset_mset_set)
     apply (simp add: inj_on_def)
    apply (subst mset_set_eq_iff)
      apply simp
     apply (simp add: finite_ord_FO_resolution_inferences_between)
    apply (rule arg_cong[of _ _ "λN. (λD. (D, n)) ` N"])
    apply (simp only: map_concat list.map_comp image_comp)
    using resolve_rename_either_way_eq_congls_of_inferences_between[of C "fst ` set Q", symmetric]
    by (simp add: image_comp comp_def image_UN)
qed

lemma nonfinal_deterministic_RP_step:
  assumes
    nonfinal: "¬ is_final_dstate St" and
    step: "St' = deterministic_RP_step St"
  shows "wstate_of_dstate St w+ wstate_of_dstate St'"
proof -
  obtain N P Q :: "'a dclause list" and n :: nat where
    st: "St = (N, P, Q, n)"
    by (cases St) blast
  note step = step[unfolded st deterministic_RP_step.simps, simplified]

  show ?thesis
  proof (cases "Ci  set P  set Q. fst Ci = []")
    case nil_in: True
    note step = step[simplified nil_in, simplified]

    have nil_in': "[]  fst ` set (P @ Q)"
      using nil_in by (force simp: image_def)

    have star: "[]  fst ` set (P @ Q) 
      wstate_of_dstate (N, P, Q, n)
      w* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))"
    proof (induct "length (remdups_clss P)" arbitrary: N P Q n)
      case 0
      note len_p = this(1) and nil_in' = this(2)

      have p_nil: "P = []"
        using len_p remdups_clss_Nil_iff by simp
      have "wstate_of_dstate (N, [], Q, n) w* wstate_of_dstate ([], [], Q, n)"
        by (rule empty_N_if_Nil_in_P_or_Q[OF nil_in'[unfolded p_nil]])
      then show ?case
        unfolding p_nil by simp
    next
      case (Suc k)
      note ih = this(1) and suc_k = this(2) and nil_in' = this(3)

      have "P  []"
        using suc_k remdups_clss_Nil_iff by force
      hence p_cons: "P = hd P # tl P"
        by simp

      obtain C :: "'a lclause" and i :: nat where
        ci: "(C, i) = select_min_weight_clause (hd P) (tl P)"
        by (metis prod.exhaust)

      have ci_in: "(C, i)  set P"
        unfolding ci using p_cons select_min_weight_clause_in[of "hd P" "tl P"] by simp
      have ci_min: "(D, j) ∈# mset (map (apfst mset) P). weight (mset C, i)  weight (D, j)"
        by (subst p_cons) (simp add: select_min_weight_clause_min_weight[OF ci, simplified])

      let ?P' = "filter (λ(D, j). mset D  mset C) P"

      have ms_p'_ci_q_eq: "mset (remdups_clss ?P' @ (C, i) # Q) = mset (remdups_clss P @ Q)"
        apply (subst (2) p_cons)
        apply (subst remdups_clss.simps(2))
        by (auto simp: Let_def case_prod_beta p_cons[symmetric] ci[symmetric])
      then have len_p: "length (remdups_clss P) = length (remdups_clss ?P') + 1"
        by (smt Suc_eq_plus1_left add.assoc add_right_cancel length_Cons length_append
            mset_eq_length)

      have "wstate_of_dstate (N, P, Q, n) w* wstate_of_dstate ([], P, Q, n)"
        by (rule empty_N_if_Nil_in_P_or_Q[OF nil_in'])
      also obtain N' :: "'a dclause list" where
        " w wstate_of_dstate (N', ?P', (C, i) # Q, Suc n)"
        by (atomize_elim, rule exI, rule compute_inferences[OF ci_in], use ci_min in fastforce)
      also have " w* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))"
        apply (rule arg_cong2[THEN iffD1, of _ _ _ _ "(↝w*)", OF _ _
            ih[of ?P' "(C, i) # Q" N' "Suc n"], OF refl])
        using ms_p'_ci_q_eq suc_k nil_in' ci_in
          apply (simp_all add: len_p)
         apply (metis (no_types) apfst_conv image_mset_add_mset)
        by force
      finally show ?case
        .
    qed
    show ?thesis
      unfolding st step using star[OF nil_in'] nonfinal[unfolded st is_final_dstate.simps]
      by cases simp_all
  next
    case nil_ni: False
    note step = step[simplified nil_ni, simplified]
    show ?thesis
    proof (cases N)
      case n_nil: Nil
      note step = step[unfolded n_nil, simplified]
      show ?thesis
      proof (cases P)
        case Nil
        then have False
          using n_nil nonfinal[unfolded st] by (simp add: is_final_dstate.simps)
        then show ?thesis
          using step by simp
      next
        case p_cons: (Cons P0 P')
        note step = step[unfolded p_cons list.case, folded p_cons]

        obtain C :: "'a lclause" and i :: nat where
          ci: "(C, i) = select_min_weight_clause P0 P'"
          by (metis prod.exhaust)
        note step = step[unfolded select, simplified]

        have ci_in: "(C, i)  set P"
          by (rule select_min_weight_clause_in[of P0 P', folded ci p_cons])

        show ?thesis
          unfolding st n_nil step p_cons[symmetric] ci[symmetric] prod.case
          by (rule tranclp.r_into_trancl, rule compute_inferences[OF ci_in])
            (simp add: select_min_weight_clause_min_weight[OF ci, simplified] p_cons)
      qed
    next
      case n_cons: (Cons Ci N')
      note step = step[unfolded n_cons, simplified]

      obtain C :: "'a lclause" and i :: nat where
        ci: "Ci = (C, i)"
        by (cases Ci) simp
      note step = step[unfolded ci, simplified]

      define C' :: "'a lclause" where
        "C' = reduce (map fst P @ map fst Q) [] C"
      note step = step[unfolded ci C'_def[symmetric], simplified]

      have "wstate_of_dstate ((E @ C, i) # N', P, Q, n)
           w* wstate_of_dstate ((E @ reduce (map fst P @ map fst Q) E C, i) # N', P, Q, n)" for E
        unfolding C'_def
      proof (induct C arbitrary: E)
        case (Cons L C)
        note ih = this(1)
        show ?case
        proof (cases "is_reducible_lit (map fst P @ map fst Q) (E @ C) L")
          case l_red: True
          then have red_lc:
            "reduce (map fst P @ map fst Q) E (L # C) = reduce (map fst P @ map fst Q) E C"
            by simp
          obtain D D' :: "'a literal list" and L' :: "'a literal" and σ :: 's where
            "D  set (map fst P @ map fst Q)" and
            "D' = remove1 L' D" and
            "L'  set D" and
            "- L = L' ⋅l σ" and
            "mset D'  σ ⊆# mset (E @ C)"
            using l_red unfolding is_reducible_lit_def comp_def by blast
          then have σ:
            "mset D' + {#L'#}  set (map (mset  fst) (P @ Q))"
            "- L = L' ⋅l σ  mset D'  σ ⊆# mset (E @ C)"
            unfolding is_reducible_lit_def by (auto simp: comp_def)
          have "wstate_of_dstate ((E @ L # C, i) # N', P, Q, n)
              w wstate_of_dstate ((E @ C, i) # N', P, Q, n)"
            by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(↝w)", OF _ _
                  wrp.forward_reduction[of "mset D'" L' "mset (map (apfst mset) P)"
                    "mset (map (apfst mset) Q)" L σ "mset (E @ C)" "mset (map (apfst mset) N')"
                    i n]])
              (use σ in auto simp: comp_def)
          then show ?thesis
            unfolding red_lc using ih[of E] by (rule converse_rtranclp_into_rtranclp)
        next
          case False
          then show ?thesis
            using ih[of "L # E"] by simp
        qed
      qed simp
      then have red_C:
        "wstate_of_dstate ((C, i) # N', P, Q, n) w* wstate_of_dstate ((C', i) # N', P, Q, n)"
        unfolding C'_def by (metis self_append_conv2)

      have proc_C: "wstate_of_dstate ((C', i) # N', P', Q', n')
          w wstate_of_dstate (N', (C', i) # P', Q', n')" for P' Q' n'
        by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(↝w)", OF _ _
              wrp.clause_processing[of "mset (map (apfst mset) N')" "mset C'" i
                "mset (map (apfst mset) P')" "mset (map (apfst mset) Q')" n']],
            simp+)

      show ?thesis
      proof (cases "C' = []")
        case True
        note c'_nil = this
        note step = step[simplified c'_nil, simplified]

        have
          filter_p: "filter (Not  strictly_subsume [[]]  fst) P = []" and
          filter_q: "filter (Not  strictly_subsume [[]]  fst) Q = []"
          using nil_ni unfolding strictly_subsume_def filter_empty_conv find_None_iff by force+

        note red_C[unfolded c'_nil]
        also have "wstate_of_dstate (([], i) # N', P, Q, n)
            w* wstate_of_dstate (([], i) # N', [], Q, n)"
          by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(↝w*)", OF _ _
                remove_strictly_subsumed_clauses_in_P[of "[]" _ "[]", unfolded append_Nil],
                OF refl])
            (auto simp: filter_p)
        also have " w* wstate_of_dstate (([], i) # N', [], [], n)"
          by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(↝w*)", OF _ _
                remove_strictly_subsumed_clauses_in_Q[of "[]" _ _ "[]", unfolded append_Nil],
                OF refl])
            (auto simp: filter_q)
        also note proc_C[unfolded c'_nil, THEN tranclp.r_into_trancl[of "(↝w)"]]
        also have "wstate_of_dstate (N', [([], i)], [], n)
            w* wstate_of_dstate ([], [([], i)], [], n)"
          by (rule empty_N_if_Nil_in_P_or_Q) simp
        also have " w wstate_of_dstate ([], [], [([], i)], Suc n)"
          by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(↝w)", OF _ _
                wrp.inference_computation[of "{#}" "{#}" i "{#}" n "{#}"]])
            (auto simp: ord_FO_resolution_inferences_between_empty_empty)
        finally show ?thesis
          unfolding step st n_cons ci .
      next
        case c'_nnil: False
        note step = step[simplified c'_nnil, simplified]
        show ?thesis
        proof (cases "is_tautology C'  subsume (map fst P @ map fst Q) C'")
          case taut_or_subs: True
          note step = step[simplified taut_or_subs, simplified]

          have "wstate_of_dstate ((C', i) # N', P, Q, n) w wstate_of_dstate (N', P, Q, n)"
          proof (cases "is_tautology C'")
            case True
            then obtain A :: 'a where
              neg_a: "Neg A  set C'" and pos_a: "Pos A  set C'"
              unfolding is_tautology_def by blast
            show ?thesis
              by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(↝w)", OF _ _
                    wrp.tautology_deletion[of A "mset C'" "mset (map (apfst mset) N')" i
                      "mset (map (apfst mset) P)" "mset (map (apfst mset) Q)" n]])
                (use neg_a pos_a in simp_all)
          next
            case False
            then have "subsume (map fst P @ map fst Q) C'"
              using taut_or_subs by blast
            then obtain D :: "'a lclause" where
              d_in: "D  set (map fst P @ map fst Q)" and
              subs: "subsumes (mset D) (mset C')"
              unfolding subsume_def by blast
            show ?thesis
              by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(↝w)", OF _ _
                    wrp.forward_subsumption[of "mset D" "mset (map (apfst mset) P)"
                      "mset (map (apfst mset) Q)" "mset C'" "mset (map (apfst mset) N')" i n]],
                  use d_in subs in auto simp: subsume_def)
          qed
          then show ?thesis
            unfolding step st n_cons ci using red_C by (rule rtranclp_into_tranclp1[rotated])
        next
          case not_taut_or_subs: False
          note step = step[simplified not_taut_or_subs, simplified]

          define P' :: "('a literal list × nat) list" where
            "P' = reduce_all C' P"

          obtain back_to_P Q' :: "'a dclause list" where
            red_Q: "(back_to_P, Q') = reduce_all2 C' Q"
            by (metis prod.exhaust)
          note step = step[unfolded red_Q[symmetric], simplified]

          define Q'' :: "('a literal list × nat) list" where
            "Q'' = filter (Not  strictly_subsume [C']  fst) Q'"
          define P'' :: "('a literal list × nat) list" where
            "P'' = filter (Not  strictly_subsume [C']  fst) (back_to_P @ P')"
          note step = step[unfolded P'_def[symmetric] Q''_def[symmetric] P''_def[symmetric],
              simplified]

          note red_C
          also have "wstate_of_dstate ((C', i) # N', P, Q, n)
              w* wstate_of_dstate ((C', i) # N', P', Q, n)"
            unfolding P'_def by (rule reduce_clauses_in_P[of _ _ "[]", unfolded append_Nil]) simp+
          also have " w* wstate_of_dstate ((C', i) # N', back_to_P @ P', Q', n)"
            unfolding P'_def
            by (rule reduce_clauses_in_Q[of C' _ _ "[]" Q, folded red_Q,
                  unfolded append_Nil prod.sel])
              (auto intro: reduce_idem simp: reduce_all_def)
          also have " w* wstate_of_dstate ((C', i) # N', back_to_P @ P', Q'', n)"
            unfolding Q''_def
            by (rule remove_strictly_subsumed_clauses_in_Q[of _ _ _ "[]", unfolded append_Nil])
              simp
          also have " w* wstate_of_dstate ((C', i) # N', P'', Q'', n)"
            unfolding P''_def
            by (rule remove_strictly_subsumed_clauses_in_P[of _ _ "[]", unfolded append_Nil]) auto
          also note proc_C[THEN tranclp.r_into_trancl[of "(↝w)"]]
          finally show ?thesis
            unfolding step st n_cons ci P''_def by simp
        qed
      qed
    qed
  qed
qed

lemma final_deterministic_RP_step: "is_final_dstate St  deterministic_RP_step St = St"
  by (cases St) (auto simp: deterministic_RP_step.simps is_final_dstate.simps)

lemma deterministic_RP_SomeD:
  assumes "deterministic_RP (N, P, Q, n) = Some R"
  shows "N' P' Q' n'. (k. (deterministic_RP_step ^^ k) (N, P, Q, n) = (N', P', Q', n'))
     is_final_dstate (N', P', Q', n')  R = map fst Q'"
proof (induct rule: deterministic_RP.raw_induct[OF _ assms])
  case (1 self_call St R)
  note ih = this(1) and step = this(2)

  obtain N P Q :: "'a dclause list" and n :: nat where
    st: "St = (N, P, Q, n)"
    by (cases St) blast
  note step = step[unfolded st, simplified]

  show ?case
  proof (cases "is_final_dstate (N, P, Q, n)")
    case True
    then have "(deterministic_RP_step ^^ 0) (N, P, Q, n) = (N, P, Q, n)
       is_final_dstate (N, P, Q, n)  R = map fst Q"
      using step by simp
    then show ?thesis
      unfolding st by blast
  next
    case nonfinal: False
    note step = step[simplified nonfinal, simplified]

    obtain N' P' Q' :: "'a dclause list" and n' k :: nat where
      "(deterministic_RP_step ^^ k) (deterministic_RP_step (N, P, Q, n)) = (N', P', Q', n')" and
      "is_final_dstate (N', P', Q', n')"
      "R = map fst Q'"
      using ih[OF step] by blast
    then show ?thesis
      unfolding st funpow_Suc_right[symmetric, THEN fun_cong, unfolded comp_apply] by blast
  qed
qed

context
  fixes
    N0 :: "'a dclause list" and
    n0 :: nat and
    R :: "'a lclause list"
begin

abbreviation St0 :: "'a dstate" where
  "St0  (N0, [], [], n0)"

abbreviation grounded_N0 where
  "grounded_N0  grounding_of_clss (set (map (mset  fst) N0))"

abbreviation grounded_R :: "'a clause set" where
  "grounded_R  grounding_of_clss (set (map mset R))"

primcorec derivation_from :: "'a dstate  'a dstate llist" where
  "derivation_from St =
   LCons St (if is_final_dstate St then LNil else derivation_from (deterministic_RP_step St))"

abbreviation Sts :: "'a dstate llist" where
  "Sts  derivation_from St0"

abbreviation wSts :: "'a wstate llist" where
  "wSts  lmap wstate_of_dstate Sts"

lemma full_deriv_wSts_trancl_weighted_RP: "full_chain (↝w+) wSts"
proof -
  have "Sts' = derivation_from St0'  full_chain (↝w+) (lmap wstate_of_dstate Sts')"
    for St0' Sts'
  proof (coinduction arbitrary: St0' Sts' rule: full_chain.coinduct)
    case sts': full_chain
    show ?case
    proof (cases "is_final_dstate St0'")
      case True
      then have "ltl (lmap wstate_of_dstate Sts') = LNil"
        unfolding sts' by simp
      then have "lmap wstate_of_dstate Sts' = LCons (wstate_of_dstate St0') LNil"
        unfolding sts' by (subst derivation_from.code, subst (asm) derivation_from.code, auto)
      moreover have "St''. ¬ wstate_of_dstate St0' w St''"
        using True by (rule is_final_dstate_imp_not_weighted_RP)
      ultimately show ?thesis
        by (meson tranclpD)
    next
      case nfinal: False
      have "lmap wstate_of_dstate Sts' =
        LCons (wstate_of_dstate St0') (lmap wstate_of_dstate (ltl Sts'))"
        unfolding sts' by (subst derivation_from.code) simp
      moreover have "ltl Sts' = derivation_from (deterministic_RP_step St0')"
        unfolding sts' using nfinal by (subst derivation_from.code) simp
      moreover have "wstate_of_dstate St0' w+ wstate_of_dstate (lhd (ltl Sts'))"
        unfolding sts' using nonfinal_deterministic_RP_step[OF nfinal refl] nfinal
        by (subst derivation_from.code) simp
      ultimately show ?thesis
        by fastforce
    qed
  qed
  then show ?thesis
    by blast
qed

lemmas deriv_wSts_trancl_weighted_RP = full_chain_imp_chain[OF full_deriv_wSts_trancl_weighted_RP]

definition sswSts :: "'a wstate llist" where
  "sswSts = (SOME wSts'.
     full_chain (↝w) wSts'  emb wSts wSts'  lhd wSts' = lhd wSts  llast wSts' = llast wSts)"

lemma sswSts:
  "full_chain (↝w) sswSts  emb wSts sswSts  lhd sswSts = lhd wSts  llast sswSts = llast wSts"
  unfolding sswSts_def
  by (rule someI_ex[OF full_chain_tranclp_imp_exists_full_chain[OF
          full_deriv_wSts_trancl_weighted_RP]])

lemmas full_deriv_sswSts_weighted_RP = sswSts[THEN conjunct1]
lemmas emb_sswSts = sswSts[THEN conjunct2, THEN conjunct1]
lemmas lfinite_sswSts_iff = emb_lfinite[OF emb_sswSts]
lemmas lhd_sswSts = sswSts[THEN conjunct2, THEN conjunct2, THEN conjunct1]
lemmas llast_sswSts = sswSts[THEN conjunct2, THEN conjunct2, THEN conjunct2]

lemmas deriv_sswSts_weighted_RP = full_chain_imp_chain[OF full_deriv_sswSts_weighted_RP]

lemma not_lnull_sswSts: "¬ lnull sswSts"
  using deriv_sswSts_weighted_RP by (cases rule: chain.cases) auto

lemma empty_ssgP0: "wrp.P_of_wstate (lhd sswSts) = {}"
  unfolding lhd_sswSts by (subst derivation_from.code) simp

lemma empty_ssgQ0: "wrp.Q_of_wstate (lhd sswSts) = {}"
  unfolding lhd_sswSts by (subst derivation_from.code) simp

lemmas sswSts_thms = full_deriv_sswSts_weighted_RP empty_ssgP0 empty_ssgQ0

abbreviation S_ssgQ :: "'a clause  'a clause" where
  "S_ssgQ  wrp.S_gQ sswSts"

abbreviation ord_Γ :: "'a inference set" where
  "ord_Γ  ground_resolution_with_selection.ord_Γ S_ssgQ"

abbreviation Rf :: "'a clause set  'a clause set" where
  "Rf  standard_redundancy_criterion.Rf"

abbreviation Ri :: "'a clause set  'a inference set" where
  "Ri  standard_redundancy_criterion.Ri ord_Γ"

abbreviation saturated_upto :: "'a clause set  bool" where
  "saturated_upto  redundancy_criterion.saturated_upto ord_Γ Rf Ri"

context
  assumes drp_some: "deterministic_RP St0 = Some R"
begin

lemma lfinite_Sts: "lfinite Sts"
proof (induct rule: deterministic_RP.raw_induct[OF _ drp_some])
  case (1 self_call St St')
  note ih = this(1) and step = this(2)
  show ?case
    using step by (subst derivation_from.code, auto intro: ih)
qed

lemma lfinite_wSts: "lfinite wSts"
  by (rule lfinite_lmap[THEN iffD2, OF lfinite_Sts])

lemmas lfinite_sswSts = lfinite_sswSts_iff[THEN iffD2, OF lfinite_wSts]

theorem
  deterministic_RP_saturated: "saturated_upto grounded_R" (is ?saturated) and
  deterministic_RP_model: "I ⊨s grounded_N0  I ⊨s grounded_R" (is ?model)
proof -
  obtain N' P' Q' :: "'a dclause list" and n' k :: nat where
    k_steps: "(deterministic_RP_step ^^ k) St0 = (N', P', Q', n')" (is "_ = ?Stk") and
    final: "is_final_dstate (N', P', Q', n')" and
    r: "R = map fst Q'"
    using deterministic_RP_SomeD[OF drp_some] by blast

  have wrp: "wstate_of_dstate St0 w* wstate_of_dstate (llast Sts)"
    using lfinite_chain_imp_rtranclp_lhd_llast
    by (metis (no_types) deriv_sswSts_weighted_RP derivation_from.disc_iff derivation_from.simps(2)
        lfinite_Sts lfinite_sswSts llast_lmap llist.map_sel(1) sswSts)

  have last_sts: "llast Sts = ?Stk"
  proof -
    have "(deterministic_RP_step ^^ k') St0' = ?Stk  llast (derivation_from St0') = ?Stk"
      for St0' k'
    proof (induct k' arbitrary: St0')
      case 0
      then show ?case
        using final by (subst derivation_from.code) simp
    next
      case (Suc k')
      note ih = this(1) and suc_k'_steps = this(2)
      show ?case
      proof (cases "is_final_dstate St0'")
        case True
        then show ?thesis
          using ih[of "deterministic_RP_step St0'"] suc_k'_steps final_deterministic_RP_step
            funpow_fixpoint[of deterministic_RP_step]
          by auto
      next
        case False
        then show ?thesis
          using ih[of "deterministic_RP_step St0'"] suc_k'_steps
          by (subst derivation_from.code) (simp add: llast_LCons funpow_swap1[symmetric])
      qed
    qed
    then show ?thesis
      using k_steps by blast
  qed

  have fin_gr_fgsts: "lfinite (lmap wrp.grounding_of_wstate sswSts)"
    by (rule lfinite_lmap[THEN iffD2, OF lfinite_sswSts])

  have lim_last: "Liminf_llist (lmap wrp.grounding_of_wstate sswSts) =
    wrp.grounding_of_wstate (llast sswSts)"
    unfolding lfinite_Liminf_llist[OF fin_gr_fgsts] llast_lmap[OF lfinite_sswSts not_lnull_sswSts]
    using not_lnull_sswSts by simp

  have gr_st0: "wrp.grounding_of_wstate (wstate_of_dstate St0) = grounded_N0"
    unfolding comp_def by simp

  have "?saturated  ?model"
  proof (cases "[]  set R")
    case True
    then have emp_in: "{#}  grounded_R"
      unfolding grounding_of_clss_def grounding_of_cls_def by (auto intro: ex_ground_subst)

    have "grounded_R  wrp.grounding_of_wstate (llast sswSts)"
      unfolding r llast_sswSts
      by (simp add: last_sts llast_lmap[OF lfinite_Sts] grounding_of_clss_def)
    then have gr_last_st: "grounded_R  wrp.grounding_of_wstate (wstate_of_dstate (llast Sts))"
      by (simp add: lfinite_Sts llast_lmap llast_sswSts)

    have gr_r_fls: "¬ I ⊨s grounded_R"
      using emp_in unfolding true_clss_def by force
    then have gr_last_fls: "¬ I ⊨s wrp.grounding_of_wstate (wstate_of_dstate (llast Sts))"
      using gr_last_st unfolding true_clss_def by auto

    have ?saturated
      unfolding wrp.ord_Γ_saturated_upto_def[OF sswSts_thms]
        wrp.ord_Γ_contradiction_Rf[OF sswSts_thms emp_in] inference_system.inferences_from_def
      by auto
    moreover have ?model
      unfolding gr_r_fls[THEN eq_False[THEN iffD2]]
      by (rule rtranclp_imp_eq_image[of "(↝w)" "λSt. I ⊨s wrp.grounding_of_wstate St", OF _ wrp,
            unfolded gr_st0 gr_last_fls[THEN eq_False[THEN iffD2]]])
        (use wrp.weighted_RP_model[OF sswSts_thms] in blast)
    ultimately show ?thesis
      by blast
  next
    case False
    then have gr_last: "wrp.grounding_of_wstate (llast sswSts) = grounded_R"
      using final unfolding r llast_sswSts
      by (simp add: last_sts llast_lmap[OF lfinite_Sts] comp_def is_final_dstate.simps)
    then have gr_last_st: "wrp.grounding_of_wstate (wstate_of_dstate (llast Sts)) = grounded_R"
      by (simp add: lfinite_Sts llast_lmap llast_sswSts)

    have ?saturated
      using wrp.weighted_RP_saturated[OF sswSts_thms, unfolded gr_last lim_last] by auto
    moreover have ?model
      by (rule rtranclp_imp_eq_image[of "(↝w)" "λSt. I ⊨s wrp.grounding_of_wstate St", OF _ wrp,
            unfolded gr_st0 gr_last_st])
        (use wrp.weighted_RP_model[OF sswSts_thms] in blast)
    ultimately show ?thesis
      by blast
  qed
  then show ?saturated and ?model
    by blast+
qed

corollary deterministic_RP_refutation:
  "¬ satisfiable grounded_N0  {#}  grounded_R" (is "?lhs  ?rhs")
proof
  assume ?rhs
  then have "¬ satisfiable grounded_R"
    unfolding true_clss_def true_cls_def by force
  then show ?lhs
    using deterministic_RP_model[THEN iffD1] by blast
next
  assume ?lhs
  then have "¬ satisfiable grounded_R"
    using deterministic_RP_model[THEN iffD2] by blast
  then show ?rhs
    unfolding wrp.ord_Γ_saturated_upto_complete[OF sswSts_thms deterministic_RP_saturated] .
qed

end

context
  assumes drp_none: "deterministic_RP St0 = None"
begin

theorem deterministic_RP_complete: "satisfiable grounded_N0"
proof (rule ccontr)
  assume unsat: "¬ satisfiable grounded_N0"

  have unsat_wSts0: "¬ satisfiable (wrp.grounding_of_wstate (lhd wSts))"
    using unsat by (subst derivation_from.code) (simp add: comp_def)

  have bot_in_ss: "{#}  Q_of_state (wrp.Liminf_wstate sswSts)"
    by (rule wrp.weighted_RP_complete[OF sswSts_thms unsat_wSts0[folded lhd_sswSts]])
  have bot_in_lim: "{#}  Q_of_state (wrp.Liminf_wstate wSts)"
  proof (cases "lfinite Sts")
    case fin: True
    have "wrp.Liminf_wstate sswSts = wrp.Liminf_wstate wSts"
      by (rule Liminf_state_fin, simp_all add: fin lfinite_sswSts_iff not_lnull_sswSts,
          subst (1 2) llast_lmap,
          simp_all add: lfinite_sswSts_iff fin not_lnull_sswSts llast_sswSts)
    then show ?thesis
      using bot_in_ss by simp
  next
    case False
    then show ?thesis
      using bot_in_ss Q_of_Liminf_state_inf[OF _ emb_lmap[OF emb_sswSts]] by auto
  qed
  then obtain k :: nat where
    k_lt: "enat k < llength Sts" and
    emp_in: "{#}  wrp.Q_of_wstate (lnth wSts k)"
    unfolding Liminf_state_def Liminf_llist_def by auto
  have emp_in: "{#}  Q_of_state (state_of_dstate ((deterministic_RP_step ^^ k) St0))"
  proof -
    have "enat k < llength Sts'  Sts' = derivation_from St0' 
      {#}  wrp.Q_of_wstate (lnth (lmap wstate_of_dstate Sts') k) 
      {#}  Q_of_state (state_of_dstate ((deterministic_RP_step ^^ k) St0'))" for St0' Sts' k
    proof (induction k arbitrary: St0' Sts')
      case 0
      then show ?case
        by (subst (asm) derivation_from.code, cases St0', auto simp: comp_def)
    next
      case (Suc k)
      note ih = this(1) and sk_lt = this(2) and sts' = this(3) and emp_in_sk = this(4)

      have k_lt: "enat k < llength (ltl Sts')"
        using sk_lt by (cases Sts') (auto simp: Suc_ile_eq)
      moreover have "ltl Sts' = derivation_from (deterministic_RP_step St0')"
        using sts' k_lt by (cases Sts') auto
      moreover have "{#}  wrp.Q_of_wstate (lnth (lmap wstate_of_dstate (ltl Sts')) k)"
        using emp_in_sk k_lt by (cases Sts') auto
      ultimately show ?case
        using ih[of "ltl Sts'" "deterministic_RP_step St0'"] by (simp add: funpow_swap1)
    qed
    then show ?thesis
      using k_lt emp_in by blast
  qed
  have "deterministic_RP St0  None"
    by (rule is_final_dstate_funpow_imp_deterministic_RP_neq_None[of "Suc k"],
        cases "(deterministic_RP_step ^^ k) St0",
        use emp_in in force simp: deterministic_RP_step.simps is_final_dstate.simps)
  then show False
    using drp_none ..
qed

end

end

end

end