diff --git a/thys/Functional_Ordered_Resolution_Prover/IsaFoR_Term.thy b/thys/Functional_Ordered_Resolution_Prover/IsaFoR_Term.thy
--- a/thys/Functional_Ordered_Resolution_Prover/IsaFoR_Term.thy
+++ b/thys/Functional_Ordered_Resolution_Prover/IsaFoR_Term.thy
@@ -1,781 +1,781 @@
 (*  Title:       Integration of IsaFoR Terms and the Knuth-Bendix Order
     Author:      Dmitriy Traytel <traytel at inf.ethz.ch>, 2014
     Author:      Anders Schlichtkrull <andschl at dtu.dk>, 2017
     Maintainer:  Anders Schlichtkrull <andschl at dtu.dk>
 *)
 
 section \<open>Integration of \textsf{IsaFoR} Terms and the Knuth--Bendix Order\<close>
 
 text \<open>
 This theory implements the abstract interface for atoms and substitutions using
 the \textsf{IsaFoR} library.
 \<close>
 
 theory IsaFoR_Term
   imports
     Deriving.Derive
     Ordered_Resolution_Prover.Abstract_Substitution
     First_Order_Terms.Unification
     First_Order_Terms.Subsumption
     "HOL-Cardinals.Wellorder_Extension"
     Open_Induction.Restricted_Predicates
     Knuth_Bendix_Order.KBO
 begin
 
 hide_const (open) mgu
 
 abbreviation subst_apply_literal ::
   "('f, 'v) term literal \<Rightarrow> ('f, 'v, 'w) gsubst \<Rightarrow> ('f, 'w) term literal" (infixl "\<cdot>lit" 60) where
   "L \<cdot>lit \<sigma> \<equiv> map_literal (\<lambda>A. A \<cdot> \<sigma>) L"
 
 definition subst_apply_clause ::
   "('f, 'v) term clause \<Rightarrow> ('f, 'v, 'w) gsubst \<Rightarrow> ('f, 'w) term clause" (infixl "\<cdot>cls" 60) where
   "C \<cdot>cls \<sigma> = image_mset (\<lambda>L. L \<cdot>lit \<sigma>) C"
 
 abbreviation vars_lit :: "('f, 'v) term literal \<Rightarrow> 'v set" where
   "vars_lit L \<equiv> vars_term (atm_of L)"
 
 definition vars_clause :: "('f, 'v) term clause \<Rightarrow> 'v set" where
   "vars_clause C = Union (set_mset (image_mset vars_lit C))"
 
 definition vars_clause_list :: "('f, 'v) term clause list \<Rightarrow> 'v set" where
   "vars_clause_list Cs = Union (vars_clause ` set Cs) "
 
 definition vars_partitioned :: "('f,'v) term clause list \<Rightarrow> bool" where
   "vars_partitioned Cs \<longleftrightarrow>
    (\<forall>i < length Cs. \<forall>j < length Cs. i \<noteq> j \<longrightarrow> (vars_clause (Cs ! i) \<inter> vars_clause (Cs ! j)) = {})"
 
 lemma vars_clause_mono: "S \<subseteq># C \<Longrightarrow> vars_clause S \<subseteq> vars_clause C"
   unfolding vars_clause_def by auto
 
 interpretation substitution_ops "(\<cdot>)" Var "(\<circ>\<^sub>s)" .
 
 lemma is_ground_atm_is_ground_on_var:
   assumes "is_ground_atm (A \<cdot> \<sigma>)" and "v \<in> vars_term A"
   shows "is_ground_atm (\<sigma> v)"
 using assms proof (induction A)
   case (Var x)
   then show ?case by auto
 next
   case (Fun f ts)
   then show ?case unfolding is_ground_atm_def
     by auto
 qed
 
 lemma is_ground_lit_is_ground_on_var:
   assumes ground_lit: "is_ground_lit (subst_lit L \<sigma>)" and v_in_L: "v \<in> vars_lit L"
   shows "is_ground_atm (\<sigma> v)"
 proof -
   let ?A = "atm_of L"
   from v_in_L have A_p: "v \<in> vars_term ?A"
     by auto
   then have "is_ground_atm (?A \<cdot> \<sigma>)"
     using ground_lit unfolding is_ground_lit_def by auto
   then show ?thesis
     using A_p is_ground_atm_is_ground_on_var by metis
 qed
 
 lemma is_ground_cls_is_ground_on_var:
   assumes
     ground_clause: "is_ground_cls (subst_cls C \<sigma>)" and
     v_in_C: "v \<in> vars_clause C"
   shows "is_ground_atm (\<sigma> v)"
 proof -
   from v_in_C obtain L where L_p: "L \<in># C" "v \<in> vars_lit L"
     unfolding vars_clause_def by auto
   then have "is_ground_lit (subst_lit L \<sigma>)"
     using ground_clause unfolding is_ground_cls_def subst_cls_def by auto
   then show ?thesis
     using L_p is_ground_lit_is_ground_on_var by metis
 qed
 
 lemma is_ground_cls_list_is_ground_on_var:
   assumes ground_list: "is_ground_cls_list (subst_cls_list Cs \<sigma>)"
     and v_in_Cs: "v \<in> vars_clause_list Cs"
   shows "is_ground_atm (\<sigma> v)"
 proof -
   from v_in_Cs obtain C where C_p: "C \<in> set Cs" "v \<in> vars_clause C"
     unfolding vars_clause_list_def by auto
   then have "is_ground_cls (subst_cls C \<sigma>)"
     using ground_list unfolding is_ground_cls_list_def subst_cls_list_def by auto
   then show ?thesis
     using C_p is_ground_cls_is_ground_on_var by metis
 qed
 
 lemma same_on_vars_lit:
   assumes "\<forall>v \<in> vars_lit L. \<sigma> v = \<tau> v"
   shows "subst_lit L \<sigma> = subst_lit L \<tau>"
   using assms
 proof (induction L)
   case (Pos x)
   then have "\<forall>v \<in> vars_term x. \<sigma> v = \<tau> v \<Longrightarrow> subst_atm_abbrev x \<sigma> = subst_atm_abbrev x \<tau>"
     using term_subst_eq by metis+
   then show ?case
     unfolding subst_lit_def using Pos by auto
 next
   case (Neg x)
   then have "\<forall>v \<in> vars_term x. \<sigma> v = \<tau> v \<Longrightarrow> subst_atm_abbrev x \<sigma> = subst_atm_abbrev x \<tau>"
     using term_subst_eq by metis+
   then show ?case
     unfolding subst_lit_def using Neg by auto
 qed
 
 lemma in_list_of_mset_in_S:
   assumes "i < length (list_of_mset S)"
   shows "list_of_mset S ! i \<in># S"
 proof -
   from assms have "list_of_mset S ! i \<in> set (list_of_mset S)"
     by auto
   then have "list_of_mset S ! i \<in># mset (list_of_mset S)"
     by (meson in_multiset_in_set)
   then show ?thesis
     by auto
 qed
 
 lemma same_on_vars_clause:
   assumes "\<forall>v \<in> vars_clause S. \<sigma> v = \<tau> v"
   shows "subst_cls S \<sigma> = subst_cls S \<tau>"
   by (smt assms image_eqI image_mset_cong2 mem_simps(9) same_on_vars_lit set_image_mset
       subst_cls_def vars_clause_def)
 
 lemma vars_partitioned_var_disjoint:
   assumes "vars_partitioned Cs"
   shows "var_disjoint Cs"
   unfolding var_disjoint_def
 proof (intro allI impI)
   fix \<sigma>s :: \<open>('b \<Rightarrow> ('a, 'b) term) list\<close>
   assume "length \<sigma>s = length Cs"
   with assms[unfolded vars_partitioned_def] Fun_More.fun_merge[of "map vars_clause Cs" "nth \<sigma>s"]
   obtain \<sigma> where
     \<sigma>_p: "\<forall>i < length (map vars_clause Cs). \<forall>x \<in> map vars_clause Cs ! i. \<sigma> x = (\<sigma>s ! i) x"
     by auto
   have "\<forall>i < length Cs. \<forall>S. S \<subseteq># Cs ! i \<longrightarrow> subst_cls S (\<sigma>s ! i) = subst_cls S \<sigma>"
   proof (rule, rule, rule, rule)
     fix i :: nat and S :: "('a, 'b) term literal multiset"
     assume
       "i < length Cs" and
       "S \<subseteq># Cs ! i"
     then have "\<forall>v \<in> vars_clause S. (\<sigma>s ! i) v = \<sigma> v"
       using vars_clause_mono[of S "Cs ! i"] \<sigma>_p by auto
     then show "subst_cls S (\<sigma>s ! i) = subst_cls S \<sigma>"
       using same_on_vars_clause by auto
   qed
   then show "\<exists>\<tau>. \<forall>i<length Cs. \<forall>S. S \<subseteq># Cs ! i \<longrightarrow> subst_cls S (\<sigma>s ! i) = subst_cls S \<tau>"
     by auto
 qed
 
 lemma vars_in_instance_in_range_term:
   "vars_term (subst_atm_abbrev A \<sigma>) \<subseteq> Union (image vars_term (range \<sigma>))"
   by (induction A) auto
 
 lemma vars_in_instance_in_range_lit: "vars_lit (subst_lit L \<sigma>) \<subseteq> Union (image vars_term (range \<sigma>))"
 proof (induction L)
   case (Pos A)
   have "vars_term (A \<cdot> \<sigma>) \<subseteq> Union (image vars_term (range \<sigma>))"
     using vars_in_instance_in_range_term[of A \<sigma>] by blast
   then show ?case by auto
 next
   case (Neg A)
   have "vars_term (A \<cdot> \<sigma>) \<subseteq> Union (image vars_term (range \<sigma>))"
     using vars_in_instance_in_range_term[of A \<sigma>] by blast
   then show ?case by auto
 qed
 
 lemma vars_in_instance_in_range_cls:
   "vars_clause (subst_cls C \<sigma>) \<subseteq> Union (image vars_term (range \<sigma>))"
   unfolding vars_clause_def subst_cls_def using vars_in_instance_in_range_lit[of _ \<sigma>] by auto
 
 primrec renamings_apart :: "('f, nat) term clause list \<Rightarrow> (('f, nat) subst) list" where
   "renamings_apart [] = []"
 | "renamings_apart (C # Cs) =
    (let \<sigma>s = renamings_apart Cs in
       (\<lambda>v. Var (v + Max (vars_clause_list (subst_cls_lists Cs \<sigma>s) \<union> {0}) + 1)) # \<sigma>s)"
 
 definition var_map_of_subst :: "('f, nat) subst \<Rightarrow> nat \<Rightarrow> nat" where
   "var_map_of_subst \<sigma> v = the_Var (\<sigma> v)"
 
 lemma len_renamings_apart: "length (renamings_apart Cs) = length Cs"
   by (induction Cs) (auto simp: Let_def)
 
 lemma renamings_apart_is_Var: "\<forall>\<sigma> \<in> set (renamings_apart Cs). \<forall>x. is_Var (\<sigma> x)"
   by (induction Cs) (auto simp: Let_def)
 
 lemma renamings_apart_inj: "\<forall>\<sigma> \<in> set (renamings_apart Cs). inj \<sigma>"
 proof (induction Cs)
   case (Cons a Cs)
   then have "inj (\<lambda>v. Var (Suc (v + Max (vars_clause_list
                (subst_cls_lists Cs (renamings_apart Cs)) \<union> {0}))))"
     by (meson add_right_imp_eq injI nat.inject term.inject(1))
   then show ?case
     using Cons by (auto simp: Let_def)
 qed auto
 
 lemma finite_vars_clause[simp]: "finite (vars_clause x)"
   unfolding vars_clause_def by auto
 
 lemma finite_vars_clause_list[simp]: "finite (vars_clause_list Cs)"
   unfolding vars_clause_list_def by (induction Cs) auto
 
 lemma Suc_Max_notin_set: "finite X \<Longrightarrow> Suc (v + Max (insert 0 X)) \<notin> X"
   by (metis Max.boundedE Suc_n_not_le_n empty_iff finite.insertI le_add2 vimageE vimageI
       vimage_Suc_insert_0)
 
 lemma vars_partitioned_Nil[simp]: "vars_partitioned []"
   unfolding vars_partitioned_def by auto
 
 lemma subst_cls_lists_Nil[simp]: "subst_cls_lists Cs [] = []"
   unfolding subst_cls_lists_def by auto
 
 lemma vars_clause_hd_partitioned_from_tl:
   assumes "Cs \<noteq>[]"
   shows "vars_clause (hd (subst_cls_lists Cs (renamings_apart Cs)))
     \<inter> vars_clause_list (tl (subst_cls_lists Cs (renamings_apart Cs))) = {}"
   using assms
 proof (induction Cs)
   case (Cons C Cs)
   define \<sigma>' :: "nat \<Rightarrow> nat"
     where "\<sigma>' = (\<lambda>v. (Suc (v + Max ((vars_clause_list (subst_cls_lists Cs
                         (renamings_apart Cs))) \<union> {0}))))"
   define \<sigma> :: "nat \<Rightarrow> ('a, nat) term"
     where "\<sigma> = (\<lambda>v. Var (\<sigma>' v))"
 
   have "vars_clause (subst_cls C \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)"
     using vars_in_instance_in_range_cls[of C "hd (renamings_apart (C # Cs))"] \<sigma>_def \<sigma>'_def
     by (auto simp: Let_def)
   moreover have "\<Union> (vars_term ` range \<sigma>)
     \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}"
   proof -
     have "range \<sigma>' \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}"
       unfolding \<sigma>'_def using Suc_Max_notin_set by auto
     then show ?thesis
       unfolding \<sigma>_def \<sigma>'_def by auto
   qed
   ultimately have "vars_clause (subst_cls C \<sigma>)
      \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}"
     by auto
   then show ?case
     unfolding \<sigma>_def \<sigma>'_def unfolding subst_cls_lists_def
     by (simp add: Let_def subst_cls_lists_def)
 qed auto
 
 lemma vars_partitioned_renamings_apart: "vars_partitioned (subst_cls_lists Cs (renamings_apart Cs))"
 proof (induction Cs)
   case (Cons C Cs)
   {
     fix i :: nat and j :: nat
     assume ij:
       "i < Suc (length Cs)"
       "j < i"
     have "vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter>
         vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) =
         {}"
     proof (cases i; cases j)
       fix j' :: nat
       assume i'j':
         "i = 0"
         "j = Suc j'"
       then show "vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter>
         vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) =
         {}"
         using ij by auto
     next
       fix i' :: nat
       assume i'j':
         "i = Suc i'"
         "j = 0"
       have disjoin_C_Cs: "vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! 0) \<inter>
         vars_clause_list ((subst_cls_lists Cs (renamings_apart Cs))) = {}"
         using vars_clause_hd_partitioned_from_tl[of "C # Cs"]
         by (simp add: Let_def subst_cls_lists_def)
       {
         fix x
         assume asm: "x \<in> vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i')"
         then have "(subst_cls_lists Cs (renamings_apart Cs) ! i')
           \<in> set (subst_cls_lists Cs (renamings_apart Cs))"
           using i'j' ij unfolding subst_cls_lists_def
           by (metis Suc_less_SucD length_map len_renamings_apart length_zip min_less_iff_conj
               nth_mem)
         moreover from asm have
           "x \<in> vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i')"
           using i'j' ij
           unfolding subst_cls_lists_def by simp
         ultimately have "\<exists>D \<in> set (subst_cls_lists Cs (renamings_apart Cs)). x \<in> vars_clause D"
             by auto
       }
       then have "vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i')
         \<subseteq> Union (set (map vars_clause ((subst_cls_lists Cs (renamings_apart Cs)))))"
         by auto
       then have "vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! 0) \<inter>
         vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i') =
         {}" using disjoin_C_Cs unfolding vars_clause_list_def by auto
       moreover
       have "subst_cls_lists Cs (renamings_apart Cs) ! i' =
         subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i"
         using i'j' ij unfolding subst_cls_lists_def by (simp add: Let_def)
       ultimately
       show "vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter>
         vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) =
         {}"
         using i'j' by (simp add: Int_commute)
     next
       fix i' :: nat and j' :: nat
       assume i'j':
         "i = Suc i'"
         "j = Suc j'"
       have "i'<length (subst_cls_lists Cs (renamings_apart Cs))"
         using ij i'j' unfolding subst_cls_lists_def by (auto simp: len_renamings_apart)
       moreover
       have "j'<length (subst_cls_lists Cs (renamings_apart Cs))"
         using ij i'j' unfolding subst_cls_lists_def by (auto simp: len_renamings_apart)
       moreover
       have "i' \<noteq> j'"
         using \<open>i = Suc i'\<close> \<open>j = Suc j'\<close> ij by blast
       ultimately
       have "vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! i') \<inter>
           vars_clause (subst_cls_lists Cs (renamings_apart Cs) ! j') =
           {}"
         using Cons unfolding vars_partitioned_def by auto
       then show "vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter>
         vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) =
         {}"
         unfolding i'j'
         by (simp add: subst_cls_lists_def Let_def)
     next
       assume
         \<open>i = 0\<close> and
         \<open>j = 0\<close>
       then show \<open>vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! i) \<inter>
         vars_clause (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)) ! j) =
         {}\<close> using ij by auto
     qed
   }
   then show ?case
     unfolding vars_partitioned_def
     by (metis (no_types, lifting) Int_commute Suc_lessI len_renamings_apart length_map
         length_nth_simps(2) length_zip min.idem nat.inject not_less_eq subst_cls_lists_def)
 qed auto
 
 interpretation substitution "(\<cdot>)" "Var :: _ \<Rightarrow> ('f, nat) term" "(\<circ>\<^sub>s)" renamings_apart "Fun undefined"
 proof (standard)
   show "\<And>A. A \<cdot> Var = A"
     by auto
 next
   show "\<And>A \<tau> \<sigma>. A \<cdot> \<tau> \<circ>\<^sub>s \<sigma> = A \<cdot> \<tau> \<cdot> \<sigma>"
     by auto
 next
   show "\<And>\<sigma> \<tau>. (\<And>A. A \<cdot> \<sigma> = A \<cdot> \<tau>) \<Longrightarrow> \<sigma> = \<tau>"
     by (simp add: subst_term_eqI)
 next
   fix C :: "('f, nat) term clause"
   fix \<sigma>
   assume "is_ground_cls (subst_cls C \<sigma>)"
   then have ground_atms_\<sigma>: "\<And>v. v \<in> vars_clause C \<Longrightarrow> is_ground_atm (\<sigma> v)"
     by (meson is_ground_cls_is_ground_on_var)
 
   define some_ground_trm :: "('f, nat) term" where "some_ground_trm = (Fun undefined [])"
   have ground_trm: "is_ground_atm some_ground_trm"
     unfolding is_ground_atm_def some_ground_trm_def by auto
   define \<tau> where "\<tau> = (\<lambda>v. if v \<in> vars_clause C then \<sigma> v else some_ground_trm)"
   then have \<tau>_\<sigma>: "\<forall>v \<in> vars_clause C. \<sigma> v = \<tau> v"
     unfolding \<tau>_def by auto
 
   have all_ground_\<tau>: "is_ground_atm (\<tau> v)" for v
   proof (cases "v \<in> vars_clause C")
     case True
     then show ?thesis
       using ground_atms_\<sigma> \<tau>_\<sigma> by auto
   next
     case False
     then show ?thesis
       unfolding \<tau>_def using ground_trm by auto
   qed
   have "is_ground_subst \<tau>"
     unfolding is_ground_subst_def
   proof
     fix A
     show "is_ground_atm (subst_atm_abbrev A \<tau>)"
     proof (induction A)
       case (Var v)
       then show ?case using all_ground_\<tau> by auto
     next
       case (Fun f As)
       then show ?case using all_ground_\<tau>
         by (simp add: is_ground_atm_def)
     qed
   qed
   moreover have "\<forall>v \<in> vars_clause C. \<sigma> v = \<tau> v"
     using \<tau>_\<sigma> unfolding vars_clause_list_def
     by blast
   then have "subst_cls C \<sigma> = subst_cls C \<tau>"
     using same_on_vars_clause by auto
   ultimately show "\<exists>\<tau>. is_ground_subst \<tau> \<and> subst_cls C \<tau> = subst_cls C \<sigma>"
     by auto
 next
   fix Cs :: "('f, nat) term clause list"
   show "length (renamings_apart Cs) = length Cs"
     using len_renamings_apart by auto
 next
   fix Cs :: "('f, nat) term clause list"
   fix \<rho> ::  "nat \<Rightarrow> ('f, nat) Term.term"
   assume \<rho>_renaming: "\<rho> \<in> set (renamings_apart Cs)"
   {
     have inj_is_renaming:
       "\<And>\<sigma> :: ('f, nat) subst. (\<And>x. is_Var (\<sigma> x)) \<Longrightarrow> inj \<sigma> \<Longrightarrow> is_renaming \<sigma>"
     proof -
       fix \<sigma> :: "('f, nat) subst"
       fix x
       assume is_var_\<sigma>: "\<And>x. is_Var (\<sigma> x)"
       assume inj_\<sigma>: "inj \<sigma>"
       define \<sigma>' where "\<sigma>' = var_map_of_subst \<sigma>"
       have \<sigma>: "\<sigma> = Var \<circ> \<sigma>'"
         unfolding \<sigma>'_def var_map_of_subst_def using is_var_\<sigma> by auto
 
       from is_var_\<sigma> inj_\<sigma> have "inj \<sigma>'"
         unfolding is_renaming_def unfolding subst_domain_def inj_on_def \<sigma>'_def var_map_of_subst_def
          by (metis term.collapse(1))
       then have "inv \<sigma>' \<circ> \<sigma>' = id"
         using inv_o_cancel[of \<sigma>'] by simp
       then have "Var \<circ> (inv \<sigma>' \<circ> \<sigma>') = Var"
         by simp
       then have "\<forall>x. (Var \<circ> (inv \<sigma>' \<circ> \<sigma>')) x = Var x"
         by metis
       then have "\<forall>x. ((Var \<circ> \<sigma>') \<circ>\<^sub>s (Var \<circ> (inv \<sigma>'))) x = Var x"
         unfolding subst_compose_def by auto
       then have "\<sigma> \<circ>\<^sub>s (Var \<circ> (inv \<sigma>')) = Var"
         using \<sigma> by auto
       then show "is_renaming \<sigma>"
         unfolding is_renaming_def by blast
     qed
     then have "\<forall>\<sigma> \<in> (set (renamings_apart Cs)). is_renaming \<sigma>"
       using renamings_apart_is_Var renamings_apart_inj by blast
   }
   then show "is_renaming \<rho>"
     using \<rho>_renaming by auto
 next
   fix Cs :: "('f, nat) term clause list"
   have "vars_partitioned (subst_cls_lists Cs (renamings_apart Cs))"
     using vars_partitioned_renamings_apart by auto
   then show "var_disjoint (subst_cls_lists Cs (renamings_apart Cs))"
     using vars_partitioned_var_disjoint by auto
 next
   show "\<And>\<sigma> As Bs. Fun undefined As \<cdot> \<sigma> = Fun undefined Bs \<longleftrightarrow> map (\<lambda>A. A \<cdot> \<sigma>) As = Bs"
     by simp
 next
   show "wfP (strictly_generalizes_atm :: ('f, 'v) term \<Rightarrow> _ \<Rightarrow> _)"
     unfolding wfP_def
     by (rule wf_subset[OF wf_subsumes])
       (auto simp: strictly_generalizes_atm_def generalizes_atm_def term_subsumable.subsumes_def
         subsumeseq_term.simps)
 qed
 
 fun pairs :: "'a list \<Rightarrow> ('a \<times> 'a) list" where
   "pairs (x # y # xs) = (x, y) # pairs (y # xs)" |
   "pairs _ = []"
 
 derive compare "term"
 derive compare "literal"
 
 lemma class_linorder_compare: "class.linorder (le_of_comp compare) (lt_of_comp compare)"
   apply standard
       apply (simp_all add: lt_of_comp_def le_of_comp_def split: order.splits)
      apply (metis comparator.sym comparator_compare invert_order.simps(1) order.distinct(5))
     apply (metis comparator_compare comparator_def order.distinct(5))
    apply (metis comparator.sym comparator_compare invert_order.simps(1) order.distinct(5))
   by (metis comparator.sym comparator_compare invert_order.simps(2) order.distinct(5))
 
 context begin
 interpretation compare_linorder: linorder
   "le_of_comp compare"
   "lt_of_comp compare"
   by (rule class_linorder_compare)
 
 definition Pairs where
   "Pairs AAA = concat (compare_linorder.sorted_list_of_set
      ((pairs \<circ> compare_linorder.sorted_list_of_set) ` AAA))"
 
 lemma unifies_all_pairs_iff:
   "(\<forall>p \<in> set (pairs xs). fst p \<cdot> \<sigma> = snd p \<cdot> \<sigma>) \<longleftrightarrow> (\<forall>a \<in> set xs. \<forall>b \<in> set xs. a \<cdot> \<sigma> = b \<cdot> \<sigma>)"
 proof (induct xs rule: pairs.induct)
   case (1 x y xs)
   then show ?case
     unfolding pairs.simps list.set ball_Un ball_simps simp_thms fst_conv snd_conv by metis
 qed simp_all
 
 lemma in_pair_in_set:
   assumes "(A,B) \<in> set ((pairs As))"
   shows "A \<in> set As \<and> B \<in> set As"
   using assms
 proof (induction As)
   case (Cons A As)
   note Cons_outer = this
   show ?case
   proof (cases As)
     case Nil
     then show ?thesis
       using Cons_outer by auto
   next
     case (Cons B As')
     then show ?thesis using Cons_outer by auto
   qed
 qed auto
 
 lemma in_pairs_sorted_list_of_set_in_set:
   assumes
     "finite AAA"
     "\<forall>AA \<in> AAA. finite AA"
     "AB_pairs \<in> (pairs \<circ> compare_linorder.sorted_list_of_set) ` AAA" and
     "(A :: _ :: compare, B) \<in> set AB_pairs"
   shows "\<exists>AA. AA \<in> AAA \<and> A \<in> AA \<and> B \<in> AA"
 proof -
   from assms have "AB_pairs \<in> (pairs \<circ> compare_linorder.sorted_list_of_set) ` AAA"
     by auto
   then obtain AA where
     AA_p: "AA \<in> AAA \<and> (pairs \<circ> compare_linorder.sorted_list_of_set) AA = AB_pairs"
     by auto
   have "(A, B) \<in> set (pairs (compare_linorder.sorted_list_of_set AA))"
     using AA_p[] assms(4) by auto
   then have "A \<in> set (compare_linorder.sorted_list_of_set AA)" and
     "B \<in> set (compare_linorder.sorted_list_of_set AA)"
     using in_pair_in_set[of A] by auto
   then show ?thesis
     using assms(2) AA_p by auto
 qed
 
 lemma unifiers_Pairs:
   assumes
     "finite AAA" and
     "\<forall>AA \<in> AAA. finite AA"
   shows "unifiers (set (Pairs AAA)) = {\<sigma>. is_unifiers \<sigma> AAA}"
 proof (rule; rule)
   fix \<sigma> :: "('a, 'b) subst"
   assume asm: "\<sigma> \<in> unifiers (set (Pairs AAA))"
   have "\<And>AA. AA \<in> AAA \<Longrightarrow> card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<le> Suc 0"
   proof -
     fix AA :: "('a, 'b) term set"
     assume asm': "AA \<in> AAA"
     then have "\<forall>p \<in> set (pairs (compare_linorder.sorted_list_of_set AA)).
       subst_atm_abbrev (fst p) \<sigma> = subst_atm_abbrev (snd p) \<sigma>"
       using assms asm unfolding Pairs_def by auto
     then have "\<forall>A \<in> AA. \<forall>B \<in> AA. subst_atm_abbrev A \<sigma> = subst_atm_abbrev B \<sigma>"
       using assms asm' unfolding unifies_all_pairs_iff
       using compare_linorder.sorted_list_of_set by blast
     then show "card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<le> Suc 0"
       by (smt imageE card.empty card_Suc_eq card_mono finite.intros(1) finite_insert le_SucI
            singletonI subsetI)
   qed
   then show "\<sigma> \<in> {\<sigma>. is_unifiers \<sigma> AAA}"
     using assms by (auto simp: is_unifiers_def is_unifier_def subst_atms_def)
 next
   fix \<sigma> :: "('a, 'b) subst"
   assume asm: "\<sigma> \<in> {\<sigma>. is_unifiers \<sigma> AAA}"
 
   {
     fix AB_pairs A B
     assume
       "AB_pairs \<in> set (compare_linorder.sorted_list_of_set
          ((pairs \<circ> compare_linorder.sorted_list_of_set) ` AAA))" and
       "(A, B) \<in> set AB_pairs"
     then have "\<exists>AA. AA \<in> AAA \<and> A \<in> AA \<and> B \<in> AA"
       using assms by (simp add: in_pairs_sorted_list_of_set_in_set)
     then obtain AA where
      a: "AA \<in> AAA" "A \<in> AA" "B \<in> AA"
       by blast
     from a assms asm have card_AA_\<sigma>: "card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<le> Suc 0"
       unfolding is_unifiers_def is_unifier_def subst_atms_def by auto
     have "subst_atm_abbrev A \<sigma> = subst_atm_abbrev B \<sigma>"
     proof (cases "card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) = Suc 0")
       case True
       moreover
       have "subst_atm_abbrev A \<sigma> \<in> AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>"
         using a assms asm card_AA_\<sigma> by auto
       moreover
       have "subst_atm_abbrev B \<sigma> \<in> AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>"
         using a assms asm card_AA_\<sigma> by auto
       ultimately
       show ?thesis
         using a assms asm card_AA_\<sigma> by (metis (no_types, lifting) card_Suc_eq singletonD)
     next
       case False
       then have "card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) = 0"
         using a assms asm card_AA_\<sigma>
         by arith
       then show ?thesis
         using a assms asm card_AA_\<sigma> by auto
     qed
   }
   then show "\<sigma> \<in> unifiers (set (Pairs AAA))"
     unfolding Pairs_def unifiers_def by auto
 qed
 
 end
 
 definition "mgu_sets AAA = map_option subst_of (unify (Pairs AAA) [])"
 
-interpretation mgu "(\<cdot>)" "Var :: _ \<Rightarrow> ('f :: compare, nat) term" "(\<circ>\<^sub>s)" "Fun undefined"
-  renamings_apart mgu_sets
-proof
+interpretation mgu "(\<cdot>)" "Var :: _ \<Rightarrow> ('f :: compare, nat) term" "(\<circ>\<^sub>s)" renamings_apart
+  "Fun undefined" mgu_sets
+proof unfold_locales
   fix AAA :: "('a :: compare, nat) term set set" and \<sigma> :: "('a, nat) subst"
   assume fin: "finite AAA" "\<forall>AA \<in> AAA. finite AA" and "mgu_sets AAA = Some \<sigma>"
   then have "is_imgu \<sigma> (set (Pairs AAA))"
     using unify_sound unfolding mgu_sets_def by blast
   then show "is_mgu \<sigma> AAA"
     unfolding is_imgu_def is_mgu_def unifiers_Pairs[OF fin] by auto
 next
   fix AAA :: "('a :: compare, nat) term set set" and \<sigma> :: "('a, nat) subst"
   assume fin: "finite AAA" "\<forall>AA \<in> AAA. finite AA" and "is_unifiers \<sigma> AAA"
   then have "\<sigma> \<in> unifiers (set (Pairs AAA))"
     unfolding is_mgu_def unifiers_Pairs[OF fin] by auto
   then show "\<exists>\<tau>. mgu_sets AAA = Some \<tau>"
     using unify_complete unfolding mgu_sets_def by blast
 qed
 
 derive linorder prod
 derive linorder list
 
 text \<open>
 This part extends and integrates and the Knuth--Bendix order defined in
 \textsf{IsaFoR}.
 \<close>
 
 record 'f weights =
   w :: "'f \<times> nat \<Rightarrow> nat"
   w0 :: nat
   pr_strict :: "'f \<times> nat \<Rightarrow> 'f \<times> nat \<Rightarrow> bool"
   least :: "'f \<Rightarrow> bool"
   scf :: "'f \<times> nat \<Rightarrow> nat \<Rightarrow> nat"
 
 class weighted =
   fixes weights :: "'a weights"
   assumes weights_adm:
     "admissible_kbo
        (w weights) (w0 weights) (pr_strict weights) ((pr_strict weights)\<^sup>=\<^sup>=) (least weights) (scf weights)"
   and pr_strict_total: "fi = gj \<or> pr_strict weights fi gj \<or> pr_strict weights gj fi"
   and pr_strict_asymp: "asymp (pr_strict weights)"
   and scf_ok: "i < n \<Longrightarrow> scf weights (f, n) i \<le> 1"
 
 instantiation unit :: weighted begin
 
 definition weights_unit :: "unit weights" where "weights_unit =
   \<lparr>w = Suc \<circ> snd, w0 = 1, pr_strict = \<lambda>(_, n) (_, m). n > m, least = \<lambda>_. True, scf = \<lambda>_ _. 1\<rparr>"
 
 instance
   by (intro_classes, unfold_locales) (auto simp: weights_unit_def SN_iff_wf asymp.simps irreflp_def
       intro!: wf_subset[OF wf_inv_image[OF wf], of _ snd])
 end
 
 global_interpretation KBO:
   admissible_kbo
     "w (weights :: 'f :: weighted weights)" "w0 (weights :: 'f :: weighted weights)"
     "pr_strict weights" "((pr_strict weights)\<^sup>=\<^sup>=)" "least weights" "scf weights"
     defines weight = KBO.weight
     and kbo = KBO.kbo
   by (simp add: weights_adm)
 
 lemma kbo_code[code]: "kbo s t =
   (let wt = weight t; ws = weight s in
   if vars_term_ms (KBO.SCF t) \<subseteq># vars_term_ms (KBO.SCF s) \<and> wt \<le> ws
   then
     (if wt < ws then (True, True)
     else
       (case s of
         Var y \<Rightarrow> (False, case t of Var x \<Rightarrow> True | Fun g ts \<Rightarrow> ts = [] \<and> least weights g)
       | Fun f ss \<Rightarrow>
           (case t of
             Var x \<Rightarrow> (True, True)
           | Fun g ts \<Rightarrow>
               if pr_strict weights (f, length ss) (g, length ts) then (True, True)
               else if (f, length ss) = (g, length ts) then lex_ext_unbounded kbo ss ts
               else (False, False))))
   else (False, False))"
   by (subst KBO.kbo.simps) (auto simp: Let_def split: term.splits)
 
 definition "less_kbo s t = fst (kbo t s)"
 
 lemma less_kbo_gtotal: "ground s \<Longrightarrow> ground t \<Longrightarrow> s = t \<or> less_kbo s t \<or> less_kbo t s"
   unfolding less_kbo_def using KBO.S_ground_total by (metis pr_strict_total subset_UNIV)
 
 lemma less_kbo_subst:
   fixes \<sigma> :: "('f :: weighted, 'v) subst"
   shows "less_kbo s t \<Longrightarrow> less_kbo (s \<cdot> \<sigma>) (t \<cdot> \<sigma>)"
   unfolding less_kbo_def by (rule KBO.S_subst)
 
 lemma wfP_less_kbo: "wfP less_kbo"
 proof -
   have "SN {(x, y). fst (kbo x y)}"
     using pr_strict_asymp by (fastforce simp: asymp.simps irreflp_def intro!: KBO.S_SN scf_ok)
   then show ?thesis
     unfolding SN_iff_wf wfP_def by (rule wf_subset) (auto simp: less_kbo_def)
 qed
 
 instantiation "term" :: (weighted, type) linorder begin
 
 definition "leq_term = (SOME leq. {(s,t). less_kbo s t} \<subseteq> leq \<and> Well_order leq \<and> Field leq = UNIV)"
 
 lemma less_trm_extension: "{(s,t). less_kbo s t} \<subseteq> leq_term"
   unfolding leq_term_def
   by (rule someI2_ex[OF total_well_order_extension[OF wfP_less_kbo[unfolded wfP_def]]]) auto
 
 lemma less_trm_well_order: "well_order leq_term"
   unfolding leq_term_def
   by (rule someI2_ex[OF total_well_order_extension[OF wfP_less_kbo[unfolded wfP_def]]]) auto
 
 definition less_eq_term :: "('a :: weighted, 'b) term \<Rightarrow> _ \<Rightarrow> bool" where
   "less_eq_term = in_rel leq_term"
 definition less_term :: "('a :: weighted, 'b) term \<Rightarrow> _ \<Rightarrow> bool" where
   "less_term s t = strict (\<le>) s t"
 
 lemma leq_term_minus_Id: "leq_term - Id = {(x,y). x < y}"
   using less_trm_well_order
   unfolding well_order_on_def linear_order_on_def partial_order_on_def antisym_def less_term_def less_eq_term_def
   by auto
 
 lemma less_term_alt: "(<) = in_rel (leq_term - Id)"
   by (simp add: in_rel_Collect_case_prod_eq leq_term_minus_Id)
 
 instance
 proof (standard, goal_cases less_less_eq refl trans antisym total)
   case (less_less_eq x y)
   then show ?case unfolding less_term_def ..
 next
 case (refl x)
   then show ?case using less_trm_well_order
     unfolding well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def refl_on_def
       less_eq_term_def by auto
 next
 case (trans x y z)
   then show ?case using less_trm_well_order
     unfolding well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def trans_def
       less_eq_term_def by auto
 next
   case (antisym x y)
   then show ?case using less_trm_well_order
     unfolding well_order_on_def linear_order_on_def partial_order_on_def antisym_def
       less_eq_term_def by auto
 next
   case (total x y)
   then show ?case using less_trm_well_order
     unfolding well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def refl_on_def
       Relation.total_on_def less_eq_term_def by (cases "x = y") auto
 qed
 
 end
 
 instantiation "term" :: (weighted, type) wellorder begin
 instance
   using less_trm_well_order[unfolded well_order_on_def wf_def leq_term_minus_Id, THEN conjunct2]
   by intro_classes (atomize, auto)
 end
 
 lemma ground_less_less_kbo: "ground s \<Longrightarrow> ground t \<Longrightarrow> s < t \<Longrightarrow> less_kbo s t"
   using less_kbo_gtotal[of s t] less_trm_extension
   by (auto simp: less_term_def less_eq_term_def)
 
 lemma less_kbo_less: "less_kbo s t \<Longrightarrow> s < t"
   using less_trm_extension
   by (auto simp: less_term_alt less_kbo_def KBO.S_irrefl)
 
 lemma is_ground_atm_ground: "is_ground_atm t \<longleftrightarrow> ground t"
   unfolding is_ground_atm_def
   by (induct t) (fastforce simp: in_set_conv_nth list_eq_iff_nth_eq)+
 
 end
diff --git a/thys/Ordered_Resolution_Prover/Abstract_Substitution.thy b/thys/Ordered_Resolution_Prover/Abstract_Substitution.thy
--- a/thys/Ordered_Resolution_Prover/Abstract_Substitution.thy
+++ b/thys/Ordered_Resolution_Prover/Abstract_Substitution.thy
@@ -1,1271 +1,1271 @@
 (*  Title:       Abstract Substitutions
     Author:      Dmitriy Traytel <traytel at inf.ethz.ch>, 2014
     Author:      Jasmin Blanchette <j.c.blanchette at vu.nl>, 2014, 2017
     Author:      Anders Schlichtkrull <andschl at dtu.dk>, 2016, 2017
     Maintainer:  Anders Schlichtkrull <andschl at dtu.dk>
 *)
 
 section \<open>Abstract Substitutions\<close>
 
 theory Abstract_Substitution
   imports Clausal_Logic Map2
 begin
 
 text \<open>
 Atoms and substitutions are abstracted away behind some locales, to avoid having a direct dependency
 on the IsaFoR library.
 
 Conventions: \<open>'s\<close> substitutions, \<open>'a\<close> atoms.
 \<close>
 
 
 subsection \<open>Library\<close>
 
 lemma f_Suc_decr_eventually_const:
   fixes f :: "nat \<Rightarrow> nat"
   assumes leq: "\<forall>i. f (Suc i) \<le> f i"
   shows "\<exists>l. \<forall>l' \<ge> l. f l' = f (Suc l')"
 proof (rule ccontr)
   assume a: "\<nexists>l. \<forall>l' \<ge> l. f l' = f (Suc l')"
   have "\<forall>i. \<exists>i'. i' > i \<and> f i' < f i"
   proof
     fix i
     from a have "\<exists>l' \<ge> i. f l' \<noteq> f (Suc l')"
       by auto
     then obtain l' where
       l'_p: "l' \<ge> i \<and> f l' \<noteq> f (Suc l')"
       by metis
     then have "f l' > f (Suc l')"
       using leq le_eq_less_or_eq by auto
     moreover have "f i \<ge> f l'"
       using leq l'_p by (induction l' arbitrary: i) (blast intro: lift_Suc_antimono_le)+
     ultimately show "\<exists>i' > i. f i' < f i"
       using l'_p less_le_trans by blast
   qed
   then obtain g_sm :: "nat \<Rightarrow> nat" where
     g_sm_p: "\<forall>i. g_sm i > i \<and> f (g_sm i) < f i"
     by metis
 
   define c :: "nat \<Rightarrow> nat" where
     "\<And>n. c n = (g_sm ^^ n) 0"
 
   have "f (c i) > f (c (Suc i))" for i
     by (induction i) (auto simp: c_def g_sm_p)
   then have "\<forall>i. (f \<circ> c) i > (f \<circ> c) (Suc i)"
     by auto
   then have "\<exists>fc :: nat \<Rightarrow> nat. \<forall>i. fc i > fc (Suc i)"
     by metis
   then show False
     using wf_less_than by (simp add: wf_iff_no_infinite_down_chain)
 qed
 
 
 subsection \<open>Substitution Operators\<close>
 
 locale substitution_ops =
   fixes
     subst_atm :: "'a \<Rightarrow> 's \<Rightarrow> 'a" and
     id_subst :: 's and
     comp_subst :: "'s \<Rightarrow> 's \<Rightarrow> 's"
 begin
 
 abbreviation subst_atm_abbrev :: "'a \<Rightarrow> 's \<Rightarrow> 'a" (infixl "\<cdot>a" 67) where
   "subst_atm_abbrev \<equiv> subst_atm"
 
 abbreviation comp_subst_abbrev :: "'s \<Rightarrow> 's \<Rightarrow> 's" (infixl "\<odot>" 67) where
   "comp_subst_abbrev \<equiv> comp_subst"
 
 definition comp_substs :: "'s list \<Rightarrow> 's list \<Rightarrow> 's list" (infixl "\<odot>s" 67) where
   "\<sigma>s \<odot>s \<tau>s = map2 comp_subst \<sigma>s \<tau>s"
 
 definition subst_atms :: "'a set \<Rightarrow> 's \<Rightarrow> 'a set" (infixl "\<cdot>as" 67) where
   "AA \<cdot>as \<sigma> = (\<lambda>A. A \<cdot>a \<sigma>) ` AA"
 
 definition subst_atmss :: "'a set set \<Rightarrow> 's \<Rightarrow> 'a set set" (infixl "\<cdot>ass" 67) where
   "AAA \<cdot>ass \<sigma> = (\<lambda>AA. AA \<cdot>as \<sigma>) ` AAA"
 
 definition subst_atm_list :: "'a list \<Rightarrow> 's \<Rightarrow> 'a list" (infixl "\<cdot>al" 67) where
   "As \<cdot>al \<sigma> = map (\<lambda>A. A \<cdot>a \<sigma>) As"
 
 definition subst_atm_mset :: "'a multiset \<Rightarrow> 's \<Rightarrow> 'a multiset" (infixl "\<cdot>am" 67) where
   "AA \<cdot>am \<sigma> = image_mset (\<lambda>A. A \<cdot>a \<sigma>) AA"
 
 definition
   subst_atm_mset_list :: "'a multiset list \<Rightarrow> 's \<Rightarrow> 'a multiset list" (infixl "\<cdot>aml" 67)
 where
   "AAA \<cdot>aml \<sigma> = map (\<lambda>AA. AA \<cdot>am \<sigma>) AAA"
 
 definition
   subst_atm_mset_lists :: "'a multiset list \<Rightarrow> 's list \<Rightarrow> 'a multiset list" (infixl "\<cdot>\<cdot>aml" 67)
 where
   "AAs \<cdot>\<cdot>aml \<sigma>s = map2 (\<cdot>am) AAs \<sigma>s"
 
 definition subst_lit :: "'a literal \<Rightarrow> 's \<Rightarrow> 'a literal" (infixl "\<cdot>l" 67) where
   "L \<cdot>l \<sigma> = map_literal (\<lambda>A. A \<cdot>a \<sigma>) L"
 
 lemma atm_of_subst_lit[simp]: "atm_of (L \<cdot>l \<sigma>) = atm_of L \<cdot>a \<sigma>"
   unfolding subst_lit_def by (cases L) simp+
 
 definition subst_cls :: "'a clause \<Rightarrow> 's \<Rightarrow> 'a clause" (infixl "\<cdot>" 67) where
   "AA \<cdot> \<sigma> = image_mset (\<lambda>A. A \<cdot>l \<sigma>) AA"
 
 definition subst_clss :: "'a clause set \<Rightarrow> 's \<Rightarrow> 'a clause set" (infixl "\<cdot>cs" 67) where
   "AA \<cdot>cs \<sigma> = (\<lambda>A. A \<cdot> \<sigma>) ` AA"
 
 definition subst_cls_list :: "'a clause list \<Rightarrow> 's \<Rightarrow> 'a clause list" (infixl "\<cdot>cl" 67) where
   "Cs \<cdot>cl \<sigma> = map (\<lambda>A. A \<cdot> \<sigma>) Cs"
 
 definition subst_cls_lists :: "'a clause list \<Rightarrow> 's list \<Rightarrow> 'a clause list" (infixl "\<cdot>\<cdot>cl" 67) where
   "Cs \<cdot>\<cdot>cl \<sigma>s = map2 (\<cdot>) Cs \<sigma>s"
 
 definition subst_cls_mset :: "'a clause multiset \<Rightarrow> 's \<Rightarrow> 'a clause multiset" (infixl "\<cdot>cm" 67) where
   "CC \<cdot>cm \<sigma> = image_mset (\<lambda>A. A \<cdot> \<sigma>) CC"
 
 lemma subst_cls_add_mset[simp]: "add_mset L C \<cdot> \<sigma> = add_mset (L \<cdot>l \<sigma>) (C \<cdot> \<sigma>)"
   unfolding subst_cls_def by simp
 
 lemma subst_cls_mset_add_mset[simp]: "add_mset C CC \<cdot>cm \<sigma> = add_mset (C \<cdot> \<sigma>) (CC \<cdot>cm \<sigma>)"
   unfolding subst_cls_mset_def by simp
 
 definition generalizes_atm :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
   "generalizes_atm A B \<longleftrightarrow> (\<exists>\<sigma>. A \<cdot>a \<sigma> = B)"
 
 definition strictly_generalizes_atm :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
   "strictly_generalizes_atm A B \<longleftrightarrow> generalizes_atm A B \<and> \<not> generalizes_atm B A"
 
 definition generalizes_lit :: "'a literal \<Rightarrow> 'a literal \<Rightarrow> bool" where
   "generalizes_lit L M \<longleftrightarrow> (\<exists>\<sigma>. L \<cdot>l \<sigma> = M)"
 
 definition strictly_generalizes_lit :: "'a literal \<Rightarrow> 'a literal \<Rightarrow> bool" where
   "strictly_generalizes_lit L M \<longleftrightarrow> generalizes_lit L M \<and> \<not> generalizes_lit M L"
 
 definition generalizes :: "'a clause \<Rightarrow> 'a clause \<Rightarrow> bool" where
   "generalizes C D \<longleftrightarrow> (\<exists>\<sigma>. C \<cdot> \<sigma> = D)"
 
 definition strictly_generalizes :: "'a clause \<Rightarrow> 'a clause \<Rightarrow> bool" where
   "strictly_generalizes C D \<longleftrightarrow> generalizes C D \<and> \<not> generalizes D C"
 
 definition subsumes :: "'a clause \<Rightarrow> 'a clause \<Rightarrow> bool" where
   "subsumes C D \<longleftrightarrow> (\<exists>\<sigma>. C \<cdot> \<sigma> \<subseteq># D)"
 
 definition strictly_subsumes :: "'a clause \<Rightarrow> 'a clause \<Rightarrow> bool" where
   "strictly_subsumes C D \<longleftrightarrow> subsumes C D \<and> \<not> subsumes D C"
 
 definition variants :: "'a clause \<Rightarrow> 'a clause \<Rightarrow> bool" where
   "variants C D \<longleftrightarrow> generalizes C D \<and> generalizes D C"
 
 definition is_renaming :: "'s \<Rightarrow> bool" where
   "is_renaming \<sigma> \<longleftrightarrow> (\<exists>\<tau>. \<sigma> \<odot> \<tau> = id_subst)"
 
 definition is_renaming_list :: "'s list \<Rightarrow> bool" where
   "is_renaming_list \<sigma>s \<longleftrightarrow> (\<forall>\<sigma> \<in> set \<sigma>s. is_renaming \<sigma>)"
 
 definition inv_renaming :: "'s \<Rightarrow> 's" where
   "inv_renaming \<sigma> = (SOME \<tau>. \<sigma> \<odot> \<tau> = id_subst)"
 
 definition is_ground_atm :: "'a \<Rightarrow> bool" where
   "is_ground_atm A \<longleftrightarrow> (\<forall>\<sigma>. A = A \<cdot>a \<sigma>)"
 
 definition is_ground_atms :: "'a set \<Rightarrow> bool" where
   "is_ground_atms AA = (\<forall>A \<in> AA. is_ground_atm A)"
 
 definition is_ground_atm_list :: "'a list \<Rightarrow> bool" where
   "is_ground_atm_list As \<longleftrightarrow> (\<forall>A \<in> set As. is_ground_atm A)"
 
 definition is_ground_atm_mset :: "'a multiset \<Rightarrow> bool" where
   "is_ground_atm_mset AA \<longleftrightarrow> (\<forall>A. A \<in># AA \<longrightarrow> is_ground_atm A)"
 
 definition is_ground_lit :: "'a literal \<Rightarrow> bool" where
   "is_ground_lit L \<longleftrightarrow> is_ground_atm (atm_of L)"
 
 definition is_ground_cls :: "'a clause \<Rightarrow> bool" where
   "is_ground_cls C \<longleftrightarrow> (\<forall>L. L \<in># C \<longrightarrow> is_ground_lit L)"
 
 definition is_ground_clss :: "'a clause set \<Rightarrow> bool" where
   "is_ground_clss CC \<longleftrightarrow> (\<forall>C \<in> CC. is_ground_cls C)"
 
 definition is_ground_cls_list :: "'a clause list \<Rightarrow> bool" where
   "is_ground_cls_list CC \<longleftrightarrow> (\<forall>C \<in> set CC. is_ground_cls C)"
 
 definition is_ground_subst :: "'s \<Rightarrow> bool" where
   "is_ground_subst \<sigma> \<longleftrightarrow> (\<forall>A. is_ground_atm (A \<cdot>a \<sigma>))"
 
 definition is_ground_subst_list :: "'s list \<Rightarrow> bool" where
   "is_ground_subst_list \<sigma>s \<longleftrightarrow> (\<forall>\<sigma> \<in> set \<sigma>s. is_ground_subst \<sigma>)"
 
 definition grounding_of_cls :: "'a clause \<Rightarrow> 'a clause set" where
   "grounding_of_cls C = {C \<cdot> \<sigma> |\<sigma>. is_ground_subst \<sigma>}"
 
 definition grounding_of_clss :: "'a clause set \<Rightarrow> 'a clause set" where
   "grounding_of_clss CC = (\<Union>C \<in> CC. grounding_of_cls C)"
 
 definition is_unifier :: "'s \<Rightarrow> 'a set \<Rightarrow> bool" where
   "is_unifier \<sigma> AA \<longleftrightarrow> card (AA \<cdot>as \<sigma>) \<le> 1"
 
 definition is_unifiers :: "'s \<Rightarrow> 'a set set \<Rightarrow> bool" where
   "is_unifiers \<sigma> AAA \<longleftrightarrow> (\<forall>AA \<in> AAA. is_unifier \<sigma> AA)"
 
 definition is_mgu :: "'s \<Rightarrow> 'a set set \<Rightarrow> bool" where
   "is_mgu \<sigma> AAA \<longleftrightarrow> is_unifiers \<sigma> AAA \<and> (\<forall>\<tau>. is_unifiers \<tau> AAA \<longrightarrow> (\<exists>\<gamma>. \<tau> = \<sigma> \<odot> \<gamma>))"
 
 definition var_disjoint :: "'a clause list \<Rightarrow> bool" where
   "var_disjoint Cs \<longleftrightarrow>
    (\<forall>\<sigma>s. length \<sigma>s = length Cs \<longrightarrow> (\<exists>\<tau>. \<forall>i < length Cs. \<forall>S. S \<subseteq># Cs ! i \<longrightarrow> S \<cdot> \<sigma>s ! i = S \<cdot> \<tau>))"
 
 end
 
 
 subsection \<open>Substitution Lemmas\<close>
 
 locale substitution = substitution_ops subst_atm id_subst comp_subst
   for
     subst_atm :: "'a \<Rightarrow> 's \<Rightarrow> 'a" and
     id_subst :: 's and
     comp_subst :: "'s \<Rightarrow> 's \<Rightarrow> 's" +
   fixes
     renamings_apart :: "'a clause list \<Rightarrow> 's list" and
     atm_of_atms :: "'a list \<Rightarrow> 'a"
   assumes
     subst_atm_id_subst[simp]: "A \<cdot>a id_subst = A" and
     subst_atm_comp_subst[simp]: "A \<cdot>a (\<sigma> \<odot> \<tau>) = (A \<cdot>a \<sigma>) \<cdot>a \<tau>" and
     subst_ext: "(\<And>A. A \<cdot>a \<sigma> = A \<cdot>a \<tau>) \<Longrightarrow> \<sigma> = \<tau>" and
     make_ground_subst: "is_ground_cls (C \<cdot> \<sigma>) \<Longrightarrow> \<exists>\<tau>. is_ground_subst \<tau> \<and>C \<cdot> \<tau> = C \<cdot> \<sigma>" and
     wf_strictly_generalizes_atm: "wfP strictly_generalizes_atm" and
     renamings_apart_length:  "length (renamings_apart Cs) = length Cs" and
     renamings_apart_renaming: "\<rho> \<in> set (renamings_apart Cs) \<Longrightarrow> is_renaming \<rho>" and
     renamings_apart_var_disjoint: "var_disjoint (Cs \<cdot>\<cdot>cl (renamings_apart Cs))" and
     atm_of_atms_subst:
       "\<And>As Bs. atm_of_atms As \<cdot>a \<sigma> = atm_of_atms Bs \<longleftrightarrow> map (\<lambda>A. A \<cdot>a \<sigma>) As = Bs"
 begin
 
 lemma subst_ext_iff: "\<sigma> = \<tau> \<longleftrightarrow> (\<forall>A. A \<cdot>a \<sigma> = A \<cdot>a \<tau>)"
   by (blast intro: subst_ext)
 
 
 subsubsection \<open>Identity Substitution\<close>
 
 lemma id_subst_comp_subst[simp]: "id_subst \<odot> \<sigma> = \<sigma>"
   by (rule subst_ext) simp
 
 lemma comp_subst_id_subst[simp]: "\<sigma> \<odot> id_subst = \<sigma>"
   by (rule subst_ext) simp
 
 lemma id_subst_comp_substs[simp]: "replicate (length \<sigma>s) id_subst \<odot>s \<sigma>s = \<sigma>s"
   using comp_substs_def by (induction \<sigma>s) auto
 
 lemma comp_substs_id_subst[simp]: "\<sigma>s \<odot>s replicate (length \<sigma>s) id_subst = \<sigma>s"
   using comp_substs_def by (induction \<sigma>s) auto
 
 lemma subst_atms_id_subst[simp]: "AA \<cdot>as id_subst = AA"
   unfolding subst_atms_def by simp
 
 lemma subst_atmss_id_subst[simp]: "AAA \<cdot>ass id_subst = AAA"
   unfolding subst_atmss_def by simp
 
 lemma subst_atm_list_id_subst[simp]: "As \<cdot>al id_subst = As"
   unfolding subst_atm_list_def by auto
 
 lemma subst_atm_mset_id_subst[simp]: "AA \<cdot>am id_subst = AA"
   unfolding subst_atm_mset_def by simp
 
 lemma subst_atm_mset_list_id_subst[simp]: "AAs \<cdot>aml id_subst = AAs"
   unfolding subst_atm_mset_list_def by simp
 
 lemma subst_atm_mset_lists_id_subst[simp]: "AAs \<cdot>\<cdot>aml replicate (length AAs) id_subst = AAs"
   unfolding subst_atm_mset_lists_def by (induct AAs) auto
 
 lemma subst_lit_id_subst[simp]: "L \<cdot>l id_subst = L"
   unfolding subst_lit_def by (simp add: literal.map_ident)
 
 lemma subst_cls_id_subst[simp]: "C \<cdot> id_subst = C"
   unfolding subst_cls_def by simp
 
 lemma subst_clss_id_subst[simp]: "CC \<cdot>cs id_subst = CC"
   unfolding subst_clss_def by simp
 
 lemma subst_cls_list_id_subst[simp]: "Cs \<cdot>cl id_subst = Cs"
   unfolding subst_cls_list_def by simp
 
 lemma subst_cls_lists_id_subst[simp]: "Cs \<cdot>\<cdot>cl replicate (length Cs) id_subst = Cs"
   unfolding subst_cls_lists_def by (induct Cs) auto
 
 lemma subst_cls_mset_id_subst[simp]: "CC \<cdot>cm id_subst = CC"
   unfolding subst_cls_mset_def by simp
 
 
 subsubsection \<open>Associativity of Composition\<close>
 
 lemma comp_subst_assoc[simp]: "\<sigma> \<odot> (\<tau> \<odot> \<gamma>) = \<sigma> \<odot> \<tau> \<odot> \<gamma>"
   by (rule subst_ext) simp
 
 
 subsubsection \<open>Compatibility of Substitution and Composition\<close>
 
 lemma subst_atms_comp_subst[simp]: "AA \<cdot>as (\<tau> \<odot> \<sigma>) = AA \<cdot>as \<tau> \<cdot>as \<sigma>"
   unfolding subst_atms_def by auto
 
 lemma subst_atmss_comp_subst[simp]: "AAA \<cdot>ass (\<tau> \<odot> \<sigma>) = AAA \<cdot>ass \<tau> \<cdot>ass \<sigma>"
   unfolding subst_atmss_def by auto
 
 lemma subst_atm_list_comp_subst[simp]: "As \<cdot>al (\<tau> \<odot> \<sigma>) = As \<cdot>al \<tau> \<cdot>al \<sigma>"
   unfolding subst_atm_list_def by auto
 
 lemma subst_atm_mset_comp_subst[simp]: "AA \<cdot>am (\<tau> \<odot> \<sigma>) = AA \<cdot>am \<tau> \<cdot>am \<sigma>"
   unfolding subst_atm_mset_def by auto
 
 lemma subst_atm_mset_list_comp_subst[simp]: "AAs \<cdot>aml (\<tau> \<odot> \<sigma>) = (AAs \<cdot>aml \<tau>) \<cdot>aml \<sigma>"
   unfolding subst_atm_mset_list_def by auto
 
 lemma subst_atm_mset_lists_comp_substs[simp]: "AAs \<cdot>\<cdot>aml (\<tau>s \<odot>s \<sigma>s) = AAs \<cdot>\<cdot>aml \<tau>s \<cdot>\<cdot>aml \<sigma>s"
   unfolding subst_atm_mset_lists_def comp_substs_def map_zip_map map_zip_map2 map_zip_assoc
   by (simp add: split_def)
 
 lemma subst_lit_comp_subst[simp]: "L \<cdot>l (\<tau> \<odot> \<sigma>) = L \<cdot>l \<tau> \<cdot>l \<sigma>"
   unfolding subst_lit_def by (auto simp: literal.map_comp o_def)
 
 lemma subst_cls_comp_subst[simp]: "C \<cdot> (\<tau> \<odot> \<sigma>) = C \<cdot> \<tau> \<cdot> \<sigma>"
   unfolding subst_cls_def by auto
 
 lemma subst_clsscomp_subst[simp]: "CC \<cdot>cs (\<tau> \<odot> \<sigma>) = CC \<cdot>cs \<tau> \<cdot>cs \<sigma>"
   unfolding subst_clss_def by auto
 
 lemma subst_cls_list_comp_subst[simp]: "Cs \<cdot>cl (\<tau> \<odot> \<sigma>) = Cs \<cdot>cl \<tau> \<cdot>cl \<sigma>"
   unfolding subst_cls_list_def by auto
 
 lemma subst_cls_lists_comp_substs[simp]: "Cs \<cdot>\<cdot>cl (\<tau>s \<odot>s \<sigma>s) = Cs \<cdot>\<cdot>cl \<tau>s \<cdot>\<cdot>cl \<sigma>s"
   unfolding subst_cls_lists_def comp_substs_def map_zip_map map_zip_map2 map_zip_assoc
   by (simp add: split_def)
 
 lemma subst_cls_mset_comp_subst[simp]: "CC \<cdot>cm (\<tau> \<odot> \<sigma>) = CC \<cdot>cm \<tau> \<cdot>cm \<sigma>"
   unfolding subst_cls_mset_def by auto
 
 
 subsubsection \<open>``Commutativity'' of Membership and Substitution\<close>
 
 lemma Melem_subst_atm_mset[simp]: "A \<in># AA \<cdot>am \<sigma> \<longleftrightarrow> (\<exists>B. B \<in># AA \<and> A = B \<cdot>a \<sigma>)"
   unfolding subst_atm_mset_def by auto
 
 lemma Melem_subst_cls[simp]: "L \<in># C \<cdot> \<sigma> \<longleftrightarrow> (\<exists>M. M \<in># C \<and> L = M \<cdot>l \<sigma>)"
   unfolding subst_cls_def by auto
 
 lemma Melem_subst_cls_mset[simp]: "AA \<in># CC \<cdot>cm \<sigma> \<longleftrightarrow> (\<exists>BB. BB \<in># CC \<and> AA = BB \<cdot> \<sigma>)"
   unfolding subst_cls_mset_def by auto
 
 
 subsubsection \<open>Signs and Substitutions\<close>
 
 lemma subst_lit_is_neg[simp]: "is_neg (L \<cdot>l \<sigma>) = is_neg L"
   unfolding subst_lit_def by auto
 
 lemma subst_lit_is_pos[simp]: "is_pos (L \<cdot>l \<sigma>) = is_pos L"
   unfolding subst_lit_def by auto
 
 lemma subst_minus[simp]: "(- L) \<cdot>l \<mu> = - (L  \<cdot>l \<mu>)"
   by (simp add: literal.map_sel subst_lit_def uminus_literal_def)
 
 
 subsubsection \<open>Substitution on Literal(s)\<close>
 
 lemma eql_neg_lit_eql_atm[simp]: "(Neg A' \<cdot>l \<eta>) = Neg A \<longleftrightarrow> A' \<cdot>a \<eta> = A"
   by (simp add: subst_lit_def)
 
 lemma eql_pos_lit_eql_atm[simp]: "(Pos A' \<cdot>l \<eta>) = Pos A \<longleftrightarrow> A' \<cdot>a \<eta> = A"
   by (simp add: subst_lit_def)
 
 lemma subst_cls_negs[simp]: "(negs AA) \<cdot> \<sigma> = negs (AA \<cdot>am \<sigma>)"
   unfolding subst_cls_def subst_lit_def subst_atm_mset_def by auto
 
 lemma subst_cls_poss[simp]: "(poss AA) \<cdot> \<sigma> = poss (AA \<cdot>am \<sigma>)"
   unfolding subst_cls_def subst_lit_def subst_atm_mset_def by auto
 
 lemma atms_of_subst_atms: "atms_of C \<cdot>as \<sigma> = atms_of (C \<cdot> \<sigma>)"
 proof -
   have "atms_of (C \<cdot> \<sigma>) = set_mset (image_mset atm_of (image_mset (map_literal (\<lambda>A. A \<cdot>a \<sigma>)) C))"
     unfolding subst_cls_def subst_atms_def subst_lit_def atms_of_def by auto
   also have "... = set_mset (image_mset (\<lambda>A. A \<cdot>a \<sigma>) (image_mset atm_of C))"
     by simp (meson literal.map_sel)
   finally show "atms_of C \<cdot>as \<sigma> = atms_of (C \<cdot> \<sigma>)"
     unfolding subst_atms_def atms_of_def by auto
 qed
 
 lemma in_image_Neg_is_neg[simp]: "L \<cdot>l \<sigma> \<in> Neg ` AA \<Longrightarrow> is_neg L"
   by (metis bex_imageD literal.disc(2) literal.map_disc_iff subst_lit_def)
 
 lemma subst_lit_in_negs_subst_is_neg: "L \<cdot>l \<sigma> \<in># (negs AA) \<cdot> \<tau> \<Longrightarrow> is_neg L"
   by simp
 
 lemma subst_lit_in_negs_is_neg: "L \<cdot>l \<sigma> \<in># negs AA \<Longrightarrow> is_neg L"
   by simp
 
 
 subsubsection \<open>Substitution on Empty\<close>
 
 lemma subst_atms_empty[simp]: "{} \<cdot>as \<sigma> = {}"
   unfolding subst_atms_def by auto
 
 lemma subst_atmss_empty[simp]: "{} \<cdot>ass \<sigma> = {}"
   unfolding subst_atmss_def by auto
 
 lemma comp_substs_empty_iff[simp]: "\<sigma>s \<odot>s \<eta>s = [] \<longleftrightarrow> \<sigma>s = [] \<or> \<eta>s = []"
   using comp_substs_def map2_empty_iff by auto
 
 lemma subst_atm_list_empty[simp]: "[] \<cdot>al \<sigma> = []"
   unfolding subst_atm_list_def by auto
 
 lemma subst_atm_mset_empty[simp]: "{#} \<cdot>am \<sigma> = {#}"
   unfolding subst_atm_mset_def by auto
 
 lemma subst_atm_mset_list_empty[simp]: "[] \<cdot>aml \<sigma> = []"
   unfolding subst_atm_mset_list_def by auto
 
 lemma subst_atm_mset_lists_empty[simp]: "[] \<cdot>\<cdot>aml \<sigma>s = []"
   unfolding subst_atm_mset_lists_def by auto
 
 lemma subst_cls_empty[simp]: "{#} \<cdot> \<sigma> = {#}"
   unfolding subst_cls_def by auto
 
 lemma subst_clss_empty[simp]: "{} \<cdot>cs \<sigma> = {}"
   unfolding subst_clss_def by auto
 
 lemma subst_cls_list_empty[simp]: "[] \<cdot>cl \<sigma> = []"
   unfolding subst_cls_list_def by auto
 
 lemma subst_cls_lists_empty[simp]: "[] \<cdot>\<cdot>cl \<sigma>s = []"
   unfolding subst_cls_lists_def by auto
 
 lemma subst_scls_mset_empty[simp]: "{#} \<cdot>cm \<sigma> = {#}"
   unfolding subst_cls_mset_def by auto
 
 lemma subst_atms_empty_iff[simp]: "AA \<cdot>as \<eta> = {} \<longleftrightarrow> AA = {}"
   unfolding subst_atms_def by auto
 
 lemma subst_atmss_empty_iff[simp]: "AAA \<cdot>ass \<eta> = {} \<longleftrightarrow> AAA = {}"
   unfolding subst_atmss_def by auto
 
 lemma subst_atm_list_empty_iff[simp]: "As \<cdot>al \<eta> = [] \<longleftrightarrow> As = []"
   unfolding subst_atm_list_def by auto
 
 lemma subst_atm_mset_empty_iff[simp]: "AA \<cdot>am \<eta> = {#} \<longleftrightarrow> AA = {#}"
   unfolding subst_atm_mset_def by auto
 
 lemma subst_atm_mset_list_empty_iff[simp]: "AAs \<cdot>aml \<eta> = [] \<longleftrightarrow> AAs = []"
   unfolding subst_atm_mset_list_def by auto
 
 lemma subst_atm_mset_lists_empty_iff[simp]: "AAs \<cdot>\<cdot>aml \<eta>s = [] \<longleftrightarrow> (AAs = [] \<or> \<eta>s = [])"
   using map2_empty_iff subst_atm_mset_lists_def by auto
 
 lemma subst_cls_empty_iff[simp]: "C \<cdot> \<eta> = {#} \<longleftrightarrow> C = {#}"
   unfolding subst_cls_def by auto
 
 lemma subst_clss_empty_iff[simp]: "CC \<cdot>cs \<eta> = {} \<longleftrightarrow> CC = {}"
   unfolding subst_clss_def by auto
 
 lemma subst_cls_list_empty_iff[simp]: "Cs \<cdot>cl \<eta> = [] \<longleftrightarrow> Cs = []"
   unfolding subst_cls_list_def by auto
 
 lemma subst_cls_lists_empty_iff[simp]: "Cs \<cdot>\<cdot>cl \<eta>s = [] \<longleftrightarrow> Cs = [] \<or> \<eta>s = []"
   using map2_empty_iff subst_cls_lists_def by auto
 
 lemma subst_cls_mset_empty_iff[simp]: "CC \<cdot>cm \<eta> = {#} \<longleftrightarrow> CC = {#}"
   unfolding subst_cls_mset_def by auto
 
 
 subsubsection \<open>Substitution on a Union\<close>
 
 lemma subst_atms_union[simp]: "(AA \<union> BB) \<cdot>as \<sigma> = AA \<cdot>as \<sigma> \<union> BB \<cdot>as \<sigma>"
   unfolding subst_atms_def by auto
 
 lemma subst_atmss_union[simp]: "(AAA \<union> BBB) \<cdot>ass \<sigma> = AAA \<cdot>ass \<sigma> \<union> BBB \<cdot>ass \<sigma>"
   unfolding subst_atmss_def by auto
 
 lemma subst_atm_list_append[simp]: "(As @ Bs) \<cdot>al \<sigma> = As \<cdot>al \<sigma> @ Bs \<cdot>al \<sigma>"
   unfolding subst_atm_list_def by auto
 
 lemma subst_atm_mset_union[simp]: "(AA + BB) \<cdot>am \<sigma> = AA \<cdot>am \<sigma> + BB \<cdot>am \<sigma>"
   unfolding subst_atm_mset_def by auto
 
 lemma subst_atm_mset_list_append[simp]: "(AAs @ BBs) \<cdot>aml \<sigma> = AAs \<cdot>aml \<sigma> @ BBs \<cdot>aml \<sigma>"
   unfolding subst_atm_mset_list_def by auto
 
 lemma subst_cls_union[simp]: "(C + D) \<cdot> \<sigma> = C \<cdot> \<sigma> + D \<cdot> \<sigma>"
   unfolding subst_cls_def by auto
 
 lemma subst_clss_union[simp]: "(CC \<union> DD) \<cdot>cs \<sigma> = CC \<cdot>cs \<sigma> \<union> DD \<cdot>cs \<sigma>"
   unfolding subst_clss_def by auto
 
 lemma subst_cls_list_append[simp]: "(Cs @ Ds) \<cdot>cl \<sigma> = Cs \<cdot>cl \<sigma> @ Ds \<cdot>cl \<sigma>"
   unfolding subst_cls_list_def by auto
 
 lemma subst_cls_lists_append[simp]:
   "length Cs = length \<sigma>s \<Longrightarrow> length Cs' = length \<sigma>s' \<Longrightarrow>
    (Cs @ Cs') \<cdot>\<cdot>cl (\<sigma>s @ \<sigma>s') = Cs \<cdot>\<cdot>cl \<sigma>s @ Cs' \<cdot>\<cdot>cl \<sigma>s'"
   unfolding subst_cls_lists_def by auto
 
 lemma subst_cls_mset_union[simp]: "(CC + DD) \<cdot>cm \<sigma> = CC \<cdot>cm \<sigma> + DD \<cdot>cm \<sigma>"
   unfolding subst_cls_mset_def by auto
 
 
 subsubsection \<open>Substitution on a Singleton\<close>
 
 lemma subst_atms_single[simp]: "{A} \<cdot>as \<sigma> = {A \<cdot>a \<sigma>}"
   unfolding subst_atms_def by auto
 
 lemma subst_atmss_single[simp]: "{AA} \<cdot>ass \<sigma> = {AA \<cdot>as \<sigma>}"
   unfolding subst_atmss_def by auto
 
 lemma subst_atm_list_single[simp]: "[A] \<cdot>al \<sigma> = [A \<cdot>a \<sigma>]"
   unfolding subst_atm_list_def by auto
 
 lemma subst_atm_mset_single[simp]: "{#A#} \<cdot>am \<sigma> = {#A \<cdot>a \<sigma>#}"
   unfolding subst_atm_mset_def by auto
 
 lemma subst_atm_mset_list[simp]: "[AA] \<cdot>aml \<sigma> = [AA \<cdot>am \<sigma>]"
   unfolding subst_atm_mset_list_def by auto
 
 lemma subst_cls_single[simp]: "{#L#} \<cdot> \<sigma> = {#L \<cdot>l \<sigma>#}"
   by simp
 
 lemma subst_clss_single[simp]: "{C} \<cdot>cs \<sigma> = {C \<cdot> \<sigma>}"
   unfolding subst_clss_def by auto
 
 lemma subst_cls_list_single[simp]: "[C] \<cdot>cl \<sigma> = [C \<cdot> \<sigma>]"
   unfolding subst_cls_list_def by auto
 
 lemma subst_cls_lists_single[simp]: "[C] \<cdot>\<cdot>cl [\<sigma>] = [C \<cdot> \<sigma>]"
   unfolding subst_cls_lists_def by auto
 
 lemma subst_cls_mset_single[simp]: "{#C#} \<cdot>cm \<sigma> = {#C \<cdot> \<sigma>#}"
   by simp
 
 
 subsubsection \<open>Substitution on @{term Cons}\<close>
 
 lemma subst_atm_list_Cons[simp]: "(A # As) \<cdot>al \<sigma> = A \<cdot>a \<sigma> # As \<cdot>al \<sigma>"
   unfolding subst_atm_list_def by auto
 
 lemma subst_atm_mset_list_Cons[simp]: "(A # As) \<cdot>aml \<sigma> = A \<cdot>am \<sigma> # As \<cdot>aml \<sigma>"
   unfolding subst_atm_mset_list_def by auto
 
 lemma subst_atm_mset_lists_Cons[simp]: "(C # Cs) \<cdot>\<cdot>aml (\<sigma> # \<sigma>s) = C \<cdot>am \<sigma> # Cs \<cdot>\<cdot>aml \<sigma>s"
   unfolding subst_atm_mset_lists_def by auto
 
 lemma subst_cls_list_Cons[simp]: "(C # Cs) \<cdot>cl \<sigma> = C \<cdot> \<sigma> # Cs \<cdot>cl \<sigma>"
   unfolding subst_cls_list_def by auto
 
 lemma subst_cls_lists_Cons[simp]: "(C # Cs) \<cdot>\<cdot>cl (\<sigma> # \<sigma>s) = C \<cdot> \<sigma> # Cs \<cdot>\<cdot>cl \<sigma>s"
   unfolding subst_cls_lists_def by auto
 
 
 subsubsection \<open>Substitution on @{term tl}\<close>
 
 lemma subst_atm_list_tl[simp]: "tl (As \<cdot>al \<sigma>) = tl As \<cdot>al \<sigma>"
   by (cases As) auto
 
 lemma subst_atm_mset_list_tl[simp]: "tl (AAs \<cdot>aml \<sigma>) = tl AAs \<cdot>aml \<sigma>"
   by (cases AAs) auto
 
 lemma subst_cls_list_tl[simp]: "tl (Cs \<cdot>cl \<sigma>) = tl Cs \<cdot>cl \<sigma>"
   by (cases Cs) auto
 
 lemma subst_cls_lists_tl[simp]: "length Cs = length \<sigma>s \<Longrightarrow> tl (Cs \<cdot>\<cdot>cl \<sigma>s) = tl Cs \<cdot>\<cdot>cl tl \<sigma>s"
   by (cases Cs; cases \<sigma>s) auto
 
 
 subsubsection \<open>Substitution on @{term nth}\<close>
 
 lemma comp_substs_nth[simp]:
   "length \<tau>s = length \<sigma>s \<Longrightarrow> i < length \<tau>s \<Longrightarrow> (\<tau>s \<odot>s \<sigma>s) ! i = (\<tau>s ! i) \<odot> (\<sigma>s ! i)"
   by (simp add: comp_substs_def)
 
 lemma subst_atm_list_nth[simp]: "i < length As \<Longrightarrow> (As \<cdot>al \<tau>) ! i = As ! i \<cdot>a \<tau>"
   unfolding subst_atm_list_def using less_Suc_eq_0_disj nth_map by force
 
 lemma subst_atm_mset_list_nth[simp]: "i < length AAs \<Longrightarrow> (AAs \<cdot>aml \<eta>) ! i = (AAs ! i) \<cdot>am \<eta>"
   unfolding subst_atm_mset_list_def by auto
 
 lemma subst_atm_mset_lists_nth[simp]:
   "length AAs = length \<sigma>s \<Longrightarrow> i < length AAs \<Longrightarrow> (AAs \<cdot>\<cdot>aml \<sigma>s) ! i = (AAs ! i) \<cdot>am (\<sigma>s ! i)"
   unfolding subst_atm_mset_lists_def by auto
 
 lemma subst_cls_list_nth[simp]: "i < length Cs \<Longrightarrow> (Cs \<cdot>cl \<tau>) ! i = (Cs ! i) \<cdot> \<tau>"
   unfolding subst_cls_list_def using less_Suc_eq_0_disj nth_map by (induction Cs) auto
 
 lemma subst_cls_lists_nth[simp]:
   "length Cs = length \<sigma>s \<Longrightarrow> i < length Cs \<Longrightarrow> (Cs \<cdot>\<cdot>cl \<sigma>s) ! i = (Cs ! i) \<cdot> (\<sigma>s ! i)"
   unfolding subst_cls_lists_def by auto
 
 
 subsubsection \<open>Substitution on Various Other Functions\<close>
 
 lemma subst_clss_image[simp]: "image f X \<cdot>cs \<sigma> = {f x \<cdot> \<sigma> | x. x \<in> X}"
   unfolding subst_clss_def by auto
 
 lemma subst_cls_mset_image_mset[simp]: "image_mset f X \<cdot>cm \<sigma> = {# f x \<cdot> \<sigma>. x \<in># X #}"
   unfolding subst_cls_mset_def by auto
 
 lemma mset_subst_atm_list_subst_atm_mset[simp]: "mset (As \<cdot>al \<sigma>) = mset (As) \<cdot>am \<sigma>"
   unfolding subst_atm_list_def subst_atm_mset_def by auto
 
 lemma mset_subst_cls_list_subst_cls_mset: "mset (Cs \<cdot>cl \<sigma>) = (mset Cs) \<cdot>cm \<sigma>"
   unfolding subst_cls_mset_def subst_cls_list_def by auto
 
 lemma sum_list_subst_cls_list_subst_cls[simp]: "sum_list (Cs \<cdot>cl \<eta>) = sum_list Cs \<cdot> \<eta>"
   unfolding subst_cls_list_def by (induction Cs) auto
 
 lemma set_mset_subst_cls_mset_subst_clss: "set_mset (CC \<cdot>cm \<mu>) = (set_mset CC) \<cdot>cs \<mu>"
   by (simp add: subst_cls_mset_def subst_clss_def)
 
 lemma Neg_Melem_subst_atm_subst_cls[simp]: "Neg A \<in># C \<Longrightarrow> Neg (A \<cdot>a \<sigma>) \<in># C \<cdot> \<sigma> "
   by (metis Melem_subst_cls eql_neg_lit_eql_atm)
 
 lemma Pos_Melem_subst_atm_subst_cls[simp]: "Pos A \<in># C \<Longrightarrow> Pos (A \<cdot>a \<sigma>) \<in># C \<cdot> \<sigma> "
   by (metis Melem_subst_cls eql_pos_lit_eql_atm)
 
 lemma in_atms_of_subst[simp]: "B \<in> atms_of C \<Longrightarrow> B \<cdot>a \<sigma> \<in> atms_of (C \<cdot> \<sigma>)"
   by (metis atms_of_subst_atms image_iff subst_atms_def)
 
 
 subsubsection \<open>Renamings\<close>
 
 lemma is_renaming_id_subst[simp]: "is_renaming id_subst"
   unfolding is_renaming_def by simp
 
 lemma is_renamingD: "is_renaming \<sigma> \<Longrightarrow> (\<forall>A1 A2. A1 \<cdot>a \<sigma> = A2 \<cdot>a \<sigma> \<longleftrightarrow> A1 = A2)"
   by (metis is_renaming_def subst_atm_comp_subst subst_atm_id_subst)
 
 lemma inv_renaming_cancel_r[simp]: "is_renaming r \<Longrightarrow> r \<odot> inv_renaming r = id_subst"
   unfolding inv_renaming_def is_renaming_def by (metis (mono_tags) someI_ex)
 
 lemma inv_renaming_cancel_r_list[simp]:
   "is_renaming_list rs \<Longrightarrow> rs \<odot>s map inv_renaming rs = replicate (length rs) id_subst"
   unfolding is_renaming_list_def by (induction rs) (auto simp add: comp_substs_def)
 
 lemma Nil_comp_substs[simp]: "[] \<odot>s s = []"
   unfolding comp_substs_def by auto
 
 lemma comp_substs_Nil[simp]: "s \<odot>s [] = []"
   unfolding comp_substs_def by auto
 
 lemma is_renaming_idempotent_id_subst: "is_renaming r \<Longrightarrow> r \<odot> r = r \<Longrightarrow> r = id_subst"
   by (metis comp_subst_assoc comp_subst_id_subst inv_renaming_cancel_r)
 
 lemma is_renaming_left_id_subst_right_id_subst:
   "is_renaming r \<Longrightarrow> s \<odot> r = id_subst \<Longrightarrow> r \<odot> s = id_subst"
   by (metis comp_subst_assoc comp_subst_id_subst is_renaming_def)
 
 lemma is_renaming_closure: "is_renaming r1 \<Longrightarrow> is_renaming r2 \<Longrightarrow> is_renaming (r1 \<odot> r2)"
   unfolding is_renaming_def by (metis comp_subst_assoc comp_subst_id_subst)
 
 lemma is_renaming_inv_renaming_cancel_atm[simp]: "is_renaming \<rho> \<Longrightarrow> A \<cdot>a \<rho> \<cdot>a inv_renaming \<rho> = A"
   by (metis inv_renaming_cancel_r subst_atm_comp_subst subst_atm_id_subst)
 
 lemma is_renaming_inv_renaming_cancel_atms[simp]: "is_renaming \<rho> \<Longrightarrow> AA \<cdot>as \<rho> \<cdot>as inv_renaming \<rho> = AA"
   by (metis inv_renaming_cancel_r subst_atms_comp_subst subst_atms_id_subst)
 
 lemma is_renaming_inv_renaming_cancel_atmss[simp]: "is_renaming \<rho> \<Longrightarrow> AAA \<cdot>ass \<rho> \<cdot>ass inv_renaming \<rho> = AAA"
   by (metis inv_renaming_cancel_r subst_atmss_comp_subst subst_atmss_id_subst)
 
 lemma is_renaming_inv_renaming_cancel_atm_list[simp]: "is_renaming \<rho> \<Longrightarrow> As \<cdot>al \<rho> \<cdot>al inv_renaming \<rho> = As"
   by (metis inv_renaming_cancel_r subst_atm_list_comp_subst subst_atm_list_id_subst)
 
 lemma is_renaming_inv_renaming_cancel_atm_mset[simp]: "is_renaming \<rho> \<Longrightarrow> AA \<cdot>am \<rho> \<cdot>am inv_renaming \<rho> = AA"
   by (metis inv_renaming_cancel_r subst_atm_mset_comp_subst subst_atm_mset_id_subst)
 
 lemma is_renaming_inv_renaming_cancel_atm_mset_list[simp]: "is_renaming \<rho> \<Longrightarrow> (AAs \<cdot>aml \<rho>) \<cdot>aml inv_renaming \<rho> = AAs"
   by (metis inv_renaming_cancel_r subst_atm_mset_list_comp_subst subst_atm_mset_list_id_subst)
 
 lemma is_renaming_list_inv_renaming_cancel_atm_mset_lists[simp]:
   "length AAs = length \<rho>s \<Longrightarrow> is_renaming_list \<rho>s \<Longrightarrow> AAs \<cdot>\<cdot>aml \<rho>s \<cdot>\<cdot>aml map inv_renaming \<rho>s = AAs"
   by (metis inv_renaming_cancel_r_list subst_atm_mset_lists_comp_substs
       subst_atm_mset_lists_id_subst)
 
 lemma is_renaming_inv_renaming_cancel_lit[simp]: "is_renaming \<rho> \<Longrightarrow> (L \<cdot>l \<rho>) \<cdot>l inv_renaming \<rho> = L"
   by (metis inv_renaming_cancel_r subst_lit_comp_subst subst_lit_id_subst)
 
 lemma is_renaming_inv_renaming_cancel_cls[simp]: "is_renaming \<rho> \<Longrightarrow> C  \<cdot> \<rho> \<cdot> inv_renaming \<rho> = C"
   by (metis inv_renaming_cancel_r subst_cls_comp_subst subst_cls_id_subst)
 
 lemma is_renaming_inv_renaming_cancel_clss[simp]:
   "is_renaming \<rho> \<Longrightarrow> CC \<cdot>cs \<rho> \<cdot>cs inv_renaming \<rho> = CC"
   by (metis inv_renaming_cancel_r subst_clss_id_subst subst_clsscomp_subst)
 
 lemma is_renaming_inv_renaming_cancel_cls_list[simp]:
   "is_renaming \<rho> \<Longrightarrow> Cs \<cdot>cl \<rho> \<cdot>cl inv_renaming \<rho> = Cs"
   by (metis inv_renaming_cancel_r subst_cls_list_comp_subst subst_cls_list_id_subst)
 
 lemma is_renaming_list_inv_renaming_cancel_cls_list[simp]:
   "length Cs = length \<rho>s \<Longrightarrow> is_renaming_list \<rho>s \<Longrightarrow> Cs \<cdot>\<cdot>cl \<rho>s \<cdot>\<cdot>cl map inv_renaming \<rho>s = Cs"
   by (metis inv_renaming_cancel_r_list subst_cls_lists_comp_substs subst_cls_lists_id_subst)
 
 lemma is_renaming_inv_renaming_cancel_cls_mset[simp]:
   "is_renaming \<rho> \<Longrightarrow> CC \<cdot>cm \<rho> \<cdot>cm inv_renaming \<rho> = CC"
   by (metis inv_renaming_cancel_r subst_cls_mset_comp_subst subst_cls_mset_id_subst)
 
 
 subsubsection \<open>Monotonicity\<close>
 
 lemma subst_cls_mono: "set_mset C \<subseteq> set_mset D \<Longrightarrow> set_mset (C \<cdot> \<sigma>) \<subseteq> set_mset (D \<cdot> \<sigma>)"
   by force
 
 lemma subst_cls_mono_mset: "C \<subseteq># D \<Longrightarrow> C \<cdot> \<sigma> \<subseteq># D \<cdot> \<sigma>"
   unfolding subst_clss_def by (metis mset_subset_eq_exists_conv subst_cls_union)
 
 lemma subst_subset_mono: "D \<subset># C \<Longrightarrow> D \<cdot> \<sigma> \<subset># C \<cdot> \<sigma>"
   unfolding subst_cls_def by (simp add: image_mset_subset_mono)
 
 
 subsubsection \<open>Size after Substitution\<close>
 
 lemma size_subst[simp]: "size (D \<cdot> \<sigma>) = size D"
   unfolding subst_cls_def by auto
 
 lemma subst_atm_list_length[simp]: "length (As \<cdot>al \<sigma>) = length As"
   unfolding subst_atm_list_def by auto
 
 lemma length_subst_atm_mset_list[simp]: "length (AAs \<cdot>aml \<eta>) = length AAs"
   unfolding subst_atm_mset_list_def by auto
 
 lemma subst_atm_mset_lists_length[simp]: "length (AAs \<cdot>\<cdot>aml \<sigma>s) = min (length AAs) (length \<sigma>s)"
   unfolding subst_atm_mset_lists_def by auto
 
 lemma subst_cls_list_length[simp]: "length (Cs \<cdot>cl \<sigma>) = length Cs"
   unfolding subst_cls_list_def by auto
 
 lemma comp_substs_length[simp]: "length (\<tau>s \<odot>s \<sigma>s) = min (length \<tau>s) (length \<sigma>s)"
   unfolding comp_substs_def by auto
 
 lemma subst_cls_lists_length[simp]: "length (Cs \<cdot>\<cdot>cl \<sigma>s) = min (length Cs) (length \<sigma>s)"
   unfolding subst_cls_lists_def by auto
 
 
 subsubsection \<open>Variable Disjointness\<close>
 
 lemma var_disjoint_clauses:
   assumes "var_disjoint Cs"
   shows "\<forall>\<sigma>s. length \<sigma>s = length Cs \<longrightarrow> (\<exists>\<tau>. Cs \<cdot>\<cdot>cl \<sigma>s = Cs \<cdot>cl \<tau>)"
 proof clarify
   fix \<sigma>s :: "'s list"
   assume a: "length \<sigma>s = length Cs"
   then obtain \<tau> where "\<forall>i < length Cs. \<forall>S. S \<subseteq># Cs ! i \<longrightarrow> S \<cdot> \<sigma>s ! i = S \<cdot> \<tau>"
     using assms unfolding var_disjoint_def by blast
   then have "\<forall>i < length Cs. (Cs ! i) \<cdot> \<sigma>s ! i = (Cs ! i) \<cdot> \<tau>"
     by auto
   then have "Cs \<cdot>\<cdot>cl \<sigma>s = Cs \<cdot>cl \<tau>"
     using a by (auto intro: nth_equalityI)
   then show "\<exists>\<tau>. Cs \<cdot>\<cdot>cl \<sigma>s = Cs \<cdot>cl \<tau>"
     by auto
 qed
 
 
 subsubsection \<open>Ground Expressions and Substitutions\<close>
 
 lemma ex_ground_subst: "\<exists>\<sigma>. is_ground_subst \<sigma>"
   using make_ground_subst[of "{#}"]
   by (simp add: is_ground_cls_def)
 
 lemma is_ground_cls_list_Cons[simp]:
   "is_ground_cls_list (C # Cs) = (is_ground_cls C \<and> is_ground_cls_list Cs)"
   unfolding is_ground_cls_list_def by auto
 
 
 paragraph \<open>Ground union\<close>
 
 lemma is_ground_atms_union[simp]: "is_ground_atms (AA \<union> BB) \<longleftrightarrow> is_ground_atms AA \<and> is_ground_atms BB"
   unfolding is_ground_atms_def by auto
 
 lemma is_ground_atm_mset_union[simp]:
   "is_ground_atm_mset (AA + BB) \<longleftrightarrow> is_ground_atm_mset AA \<and> is_ground_atm_mset BB"
   unfolding is_ground_atm_mset_def by auto
 
 lemma is_ground_cls_union[simp]: "is_ground_cls (C + D) \<longleftrightarrow> is_ground_cls C \<and> is_ground_cls D"
   unfolding is_ground_cls_def by auto
 
 lemma is_ground_clss_union[simp]:
   "is_ground_clss (CC \<union> DD) \<longleftrightarrow> is_ground_clss CC \<and> is_ground_clss DD"
   unfolding is_ground_clss_def by auto
 
 lemma is_ground_cls_list_is_ground_cls_sum_list[simp]:
   "is_ground_cls_list Cs \<Longrightarrow> is_ground_cls (sum_list Cs)"
   by (meson in_mset_sum_list2 is_ground_cls_def is_ground_cls_list_def)
 
 
 paragraph \<open>Grounding monotonicity\<close>
 
 lemma is_ground_cls_mono: "C \<subseteq># D \<Longrightarrow> is_ground_cls D \<Longrightarrow> is_ground_cls C"
   unfolding is_ground_cls_def by (metis set_mset_mono subsetD)
 
 lemma is_ground_clss_mono: "CC \<subseteq> DD \<Longrightarrow> is_ground_clss DD \<Longrightarrow> is_ground_clss CC"
   unfolding is_ground_clss_def by blast
 
 lemma grounding_of_clss_mono: "CC \<subseteq> DD \<Longrightarrow> grounding_of_clss CC \<subseteq> grounding_of_clss DD"
   using grounding_of_clss_def by auto
 
 lemma sum_list_subseteq_mset_is_ground_cls_list[simp]:
   "sum_list Cs \<subseteq># sum_list Ds \<Longrightarrow> is_ground_cls_list Ds \<Longrightarrow> is_ground_cls_list Cs"
   by (meson in_mset_sum_list is_ground_cls_def is_ground_cls_list_is_ground_cls_sum_list
       is_ground_cls_mono is_ground_cls_list_def)
 
 
 paragraph \<open>Substituting on ground expression preserves ground\<close>
 
 lemma is_ground_comp_subst[simp]: "is_ground_subst \<sigma> \<Longrightarrow> is_ground_subst (\<tau> \<odot> \<sigma>)"
   unfolding is_ground_subst_def is_ground_atm_def by auto
 
 lemma ground_subst_ground_atm[simp]: "is_ground_subst \<sigma> \<Longrightarrow> is_ground_atm (A \<cdot>a \<sigma>)"
   by (simp add: is_ground_subst_def)
 
 lemma ground_subst_ground_lit[simp]: "is_ground_subst \<sigma> \<Longrightarrow> is_ground_lit (L \<cdot>l \<sigma>)"
   unfolding is_ground_lit_def subst_lit_def by (cases L) auto
 
 lemma ground_subst_ground_cls[simp]: "is_ground_subst \<sigma> \<Longrightarrow> is_ground_cls (C \<cdot> \<sigma>)"
   unfolding is_ground_cls_def by auto
 
 lemma ground_subst_ground_clss[simp]: "is_ground_subst \<sigma> \<Longrightarrow> is_ground_clss (CC \<cdot>cs \<sigma>)"
   unfolding is_ground_clss_def subst_clss_def by auto
 
 lemma ground_subst_ground_cls_list[simp]: "is_ground_subst \<sigma> \<Longrightarrow> is_ground_cls_list (Cs \<cdot>cl \<sigma>)"
   unfolding is_ground_cls_list_def subst_cls_list_def by auto
 
 lemma ground_subst_ground_cls_lists[simp]:
   "\<forall>\<sigma> \<in> set \<sigma>s. is_ground_subst \<sigma> \<Longrightarrow> is_ground_cls_list (Cs \<cdot>\<cdot>cl \<sigma>s)"
   unfolding is_ground_cls_list_def subst_cls_lists_def by (auto simp: set_zip)
 
 lemma subst_cls_eq_grounding_of_cls_subset_eq:
   assumes "D \<cdot> \<sigma> = C"
   shows "grounding_of_cls C \<subseteq> grounding_of_cls D"
 proof
   fix C\<sigma>'
   assume "C\<sigma>' \<in> grounding_of_cls C"
   then obtain \<sigma>' where
     C\<sigma>': "C \<cdot> \<sigma>' = C\<sigma>'" "is_ground_subst \<sigma>'"
     unfolding grounding_of_cls_def by auto
   then have "C \<cdot> \<sigma>' = D \<cdot> \<sigma> \<cdot> \<sigma>' \<and> is_ground_subst (\<sigma> \<odot> \<sigma>')"
     using assms by auto
   then show "C\<sigma>' \<in> grounding_of_cls D"
     unfolding grounding_of_cls_def using C\<sigma>'(1) by force
 qed
 
 paragraph \<open>Substituting on ground expression has no effect\<close>
 
 lemma is_ground_subst_atm[simp]: "is_ground_atm A \<Longrightarrow> A \<cdot>a \<sigma> = A"
   unfolding is_ground_atm_def by simp
 
 lemma is_ground_subst_atms[simp]: "is_ground_atms AA \<Longrightarrow> AA \<cdot>as \<sigma> = AA"
   unfolding is_ground_atms_def subst_atms_def image_def by auto
 
 lemma is_ground_subst_atm_mset[simp]: "is_ground_atm_mset AA \<Longrightarrow> AA \<cdot>am \<sigma> = AA"
   unfolding is_ground_atm_mset_def subst_atm_mset_def by auto
 
 lemma is_ground_subst_atm_list[simp]: "is_ground_atm_list As \<Longrightarrow> As \<cdot>al \<sigma> = As"
   unfolding is_ground_atm_list_def subst_atm_list_def by (auto intro: nth_equalityI)
 
 lemma is_ground_subst_atm_list_member[simp]:
   "is_ground_atm_list As \<Longrightarrow> i < length As \<Longrightarrow> As ! i \<cdot>a \<sigma> = As ! i"
   unfolding is_ground_atm_list_def by auto
 
 lemma is_ground_subst_lit[simp]: "is_ground_lit L \<Longrightarrow> L \<cdot>l \<sigma> = L"
   unfolding is_ground_lit_def subst_lit_def by (cases L) simp_all
 
 lemma is_ground_subst_cls[simp]: "is_ground_cls C \<Longrightarrow> C \<cdot> \<sigma> = C"
   unfolding is_ground_cls_def subst_cls_def by simp
 
 lemma is_ground_subst_clss[simp]: "is_ground_clss CC \<Longrightarrow> CC \<cdot>cs \<sigma> = CC"
   unfolding is_ground_clss_def subst_clss_def image_def by auto
 
 lemma is_ground_subst_cls_lists[simp]:
   assumes "length P = length Cs" and "is_ground_cls_list Cs"
   shows "Cs \<cdot>\<cdot>cl P = Cs"
   using assms by (metis is_ground_cls_list_def is_ground_subst_cls min.idem nth_equalityI nth_mem
       subst_cls_lists_nth subst_cls_lists_length)
 
 lemma is_ground_subst_lit_iff: "is_ground_lit L \<longleftrightarrow> (\<forall>\<sigma>. L = L \<cdot>l \<sigma>)"
   using is_ground_atm_def is_ground_lit_def subst_lit_def by (cases L) auto
 
 lemma is_ground_subst_cls_iff: "is_ground_cls C \<longleftrightarrow> (\<forall>\<sigma>. C = C \<cdot> \<sigma>)"
   by (metis ex_ground_subst ground_subst_ground_cls is_ground_subst_cls)
 
 
 paragraph \<open>Members of ground expressions are ground\<close>
 
 lemma is_ground_cls_as_atms: "is_ground_cls C \<longleftrightarrow> (\<forall>A \<in> atms_of C. is_ground_atm A)"
   by (auto simp: atms_of_def is_ground_cls_def is_ground_lit_def)
 
 lemma is_ground_cls_imp_is_ground_lit: "L \<in># C \<Longrightarrow> is_ground_cls C \<Longrightarrow> is_ground_lit L"
   by (simp add: is_ground_cls_def)
 
 lemma is_ground_cls_imp_is_ground_atm: "A \<in> atms_of C \<Longrightarrow> is_ground_cls C \<Longrightarrow> is_ground_atm A"
   by (simp add: is_ground_cls_as_atms)
 
 lemma is_ground_cls_is_ground_atms_atms_of[simp]: "is_ground_cls C \<Longrightarrow> is_ground_atms (atms_of C)"
   by (simp add: is_ground_cls_imp_is_ground_atm is_ground_atms_def)
 
 lemma grounding_ground: "C \<in> grounding_of_clss M \<Longrightarrow> is_ground_cls C"
   unfolding grounding_of_clss_def grounding_of_cls_def by auto
 
 lemma in_subset_eq_grounding_of_clss_is_ground_cls[simp]:
   "C \<in> CC \<Longrightarrow> CC \<subseteq> grounding_of_clss DD \<Longrightarrow> is_ground_cls C"
   unfolding grounding_of_clss_def grounding_of_cls_def by auto
 
 lemma is_ground_cls_empty[simp]: "is_ground_cls {#}"
   unfolding is_ground_cls_def by simp
 
 lemma grounding_of_cls_ground: "is_ground_cls C \<Longrightarrow> grounding_of_cls C = {C}"
   unfolding grounding_of_cls_def by (simp add: ex_ground_subst)
 
 lemma grounding_of_cls_empty[simp]: "grounding_of_cls {#} = {{#}}"
   by (simp add: grounding_of_cls_ground)
 
 lemma union_grounding_of_cls_ground: "is_ground_clss (\<Union> (grounding_of_cls ` N))"
   by (simp add: grounding_ground grounding_of_clss_def is_ground_clss_def)
 
 
 paragraph \<open>Grounding idempotence\<close>
 
 lemma grounding_of_grounding_of_cls: "E \<in> grounding_of_cls D \<Longrightarrow> D \<in> grounding_of_cls C \<Longrightarrow> E = D"
   using grounding_of_cls_def by auto
 
 
 subsubsection \<open>Subsumption\<close>
 
 lemma subsumes_empty_left[simp]: "subsumes {#} C"
   unfolding subsumes_def subst_cls_def by simp
 
 lemma strictly_subsumes_empty_left[simp]: "strictly_subsumes {#} C \<longleftrightarrow> C \<noteq> {#}"
   unfolding strictly_subsumes_def subsumes_def subst_cls_def by simp
 
 
 subsubsection \<open>Unifiers\<close>
 
 lemma card_le_one_alt: "finite X \<Longrightarrow> card X \<le> 1 \<longleftrightarrow> X = {} \<or> (\<exists>x. X = {x})"
   by (induct rule: finite_induct) auto
 
 lemma is_unifier_subst_atm_eqI:
   assumes "finite AA"
   shows "is_unifier \<sigma> AA \<Longrightarrow> A \<in> AA \<Longrightarrow> B \<in> AA \<Longrightarrow> A \<cdot>a \<sigma> = B \<cdot>a \<sigma>"
   unfolding is_unifier_def subst_atms_def card_le_one_alt[OF finite_imageI[OF assms]]
   by (metis equals0D imageI insert_iff)
 
 lemma is_unifier_alt:
   assumes "finite AA"
   shows "is_unifier \<sigma> AA \<longleftrightarrow> (\<forall>A \<in> AA. \<forall>B \<in> AA. A \<cdot>a \<sigma> = B \<cdot>a \<sigma>)"
   unfolding is_unifier_def subst_atms_def card_le_one_alt[OF finite_imageI[OF assms(1)]]
   by (rule iffI, metis empty_iff insert_iff insert_image, blast)
 
 lemma is_unifiers_subst_atm_eqI:
   assumes "finite AA" "is_unifiers \<sigma> AAA" "AA \<in> AAA" "A \<in> AA" "B \<in> AA"
   shows "A \<cdot>a \<sigma> = B \<cdot>a \<sigma>"
   by (metis assms is_unifiers_def is_unifier_subst_atm_eqI)
 
 theorem is_unifiers_comp:
   "is_unifiers \<sigma> (set_mset ` set (map2 add_mset As Bs) \<cdot>ass \<eta>) \<longleftrightarrow>
    is_unifiers (\<eta> \<odot> \<sigma>) (set_mset ` set (map2 add_mset As Bs))"
   unfolding is_unifiers_def is_unifier_def subst_atmss_def by auto
 
 
 subsubsection \<open>Most General Unifier\<close>
 
 lemma is_mgu_is_unifiers: "is_mgu \<sigma> AAA \<Longrightarrow> is_unifiers \<sigma> AAA"
   using is_mgu_def by blast
 
 lemma is_mgu_is_most_general: "is_mgu \<sigma> AAA \<Longrightarrow> is_unifiers \<tau> AAA \<Longrightarrow> \<exists>\<gamma>. \<tau> = \<sigma> \<odot> \<gamma>"
   using is_mgu_def by blast
 
 lemma is_unifiers_is_unifier: "is_unifiers \<sigma> AAA \<Longrightarrow> AA \<in> AAA \<Longrightarrow> is_unifier \<sigma> AA"
   using is_unifiers_def by simp
 
 
 subsubsection \<open>Generalization and Subsumption\<close>
 
 lemma variants_sym: "variants D D' \<longleftrightarrow> variants D' D"
   unfolding variants_def by auto
 
 lemma variants_iff_subsumes: "variants C D \<longleftrightarrow> subsumes C D \<and> subsumes D C"
 proof
   assume "variants C D"
   then show "subsumes C D \<and> subsumes D C"
     unfolding variants_def generalizes_def subsumes_def
       by (metis subset_mset.refl)
 next
   assume sub: "subsumes C D \<and> subsumes D C"
   then have "size C = size D"
     unfolding subsumes_def by (metis antisym size_mset_mono size_subst)
   then show "variants C D"
     using sub unfolding subsumes_def variants_def generalizes_def
     by (metis leD mset_subset_size size_mset_mono size_subst
         subset_mset.not_eq_order_implies_strict)
 qed
 
 lemma wf_strictly_generalizes: "wfP strictly_generalizes"
 proof -
   {
     assume "\<exists>C_at. \<forall>i. strictly_generalizes (C_at (Suc i)) (C_at i)"
     then obtain C_at :: "nat \<Rightarrow> 'a clause" where
       sg_C: "\<And>i. strictly_generalizes (C_at (Suc i)) (C_at i)"
       by blast
 
     define n :: nat where
       "n = size (C_at 0)"
 
     have sz_C: "size (C_at i) = n" for i
     proof (induct i)
       case (Suc i)
       then show ?case
         using sg_C[of i] unfolding strictly_generalizes_def generalizes_def subst_cls_def
         by (metis size_image_mset)
     qed (simp add: n_def)
 
     obtain \<sigma>_at :: "nat \<Rightarrow> 's" where
       C_\<sigma>: "\<And>i. image_mset (\<lambda>L. L \<cdot>l \<sigma>_at i) (C_at (Suc i)) = C_at i"
       using sg_C[unfolded strictly_generalizes_def generalizes_def subst_cls_def] by metis
 
     define Ls_at :: "nat \<Rightarrow> 'a literal list" where
       "Ls_at = rec_nat (SOME Ls. mset Ls = C_at 0)
          (\<lambda>i Lsi. SOME Ls. mset Ls = C_at (Suc i) \<and> map (\<lambda>L. L \<cdot>l \<sigma>_at i) Ls = Lsi)"
 
     have
       Ls_at_0: "Ls_at 0 = (SOME Ls. mset Ls = C_at 0)" and
       Ls_at_Suc: "\<And>i. Ls_at (Suc i) =
         (SOME Ls. mset Ls = C_at (Suc i) \<and> map (\<lambda>L. L \<cdot>l \<sigma>_at i) Ls = Ls_at i)"
       unfolding Ls_at_def by simp+
 
     have mset_Lt_at_0: "mset (Ls_at 0) = C_at 0"
       unfolding Ls_at_0 by (rule someI_ex) (metis list_of_mset_exi)
 
     have "mset (Ls_at (Suc i)) = C_at (Suc i) \<and> map (\<lambda>L. L \<cdot>l \<sigma>_at i) (Ls_at (Suc i)) = Ls_at i"
       for i
     proof (induct i)
       case 0
       then show ?case
         by (simp add: Ls_at_Suc, rule someI_ex,
             metis C_\<sigma> image_mset_of_subset_list mset_Lt_at_0)
     next
       case Suc
       then show ?case
         by (subst (1 2) Ls_at_Suc) (rule someI_ex, metis C_\<sigma> image_mset_of_subset_list)
     qed
     note mset_Ls = this[THEN conjunct1] and Ls_\<sigma> = this[THEN conjunct2]
 
     have len_Ls: "\<And>i. length (Ls_at i) = n"
       by (metis mset_Ls mset_Lt_at_0 not0_implies_Suc size_mset sz_C)
 
     have is_pos_Ls: "\<And>i j. j < n \<Longrightarrow> is_pos (Ls_at (Suc i) ! j) \<longleftrightarrow> is_pos (Ls_at i ! j)"
       using Ls_\<sigma> len_Ls by (metis literal.map_disc_iff nth_map subst_lit_def)
 
     have Ls_\<tau>_strict_lit: "\<And>i \<tau>. map (\<lambda>L. L \<cdot>l \<tau>) (Ls_at i) \<noteq> Ls_at (Suc i)"
       by (metis C_\<sigma> mset_Ls Ls_\<sigma> mset_map sg_C generalizes_def strictly_generalizes_def
           subst_cls_def)
 
     have Ls_\<tau>_strict_tm:
       "map ((\<lambda>t. t \<cdot>a \<tau>) \<circ> atm_of) (Ls_at i) \<noteq> map atm_of (Ls_at (Suc i))" for i \<tau>
     proof -
       obtain j :: nat where
         j_lt: "j < n" and
         j_\<tau>: "Ls_at i ! j \<cdot>l \<tau> \<noteq> Ls_at (Suc i) ! j"
         using Ls_\<tau>_strict_lit[of \<tau> i] len_Ls
         by (metis (no_types, lifting) length_map list_eq_iff_nth_eq nth_map)
 
       have "atm_of (Ls_at i ! j) \<cdot>a \<tau> \<noteq> atm_of (Ls_at (Suc i) ! j)"
         using j_\<tau> is_pos_Ls[OF j_lt]
         by (metis (mono_guards) literal.expand literal.map_disc_iff literal.map_sel subst_lit_def)
       then show ?thesis
         using j_lt len_Ls by (metis nth_map o_apply)
     qed
 
     define tm_at :: "nat \<Rightarrow> 'a" where
       "\<And>i. tm_at i = atm_of_atms (map atm_of (Ls_at i))"
 
     have "\<And>i. generalizes_atm (tm_at (Suc i)) (tm_at i)"
       unfolding tm_at_def generalizes_atm_def atm_of_atms_subst
       using Ls_\<sigma>[THEN arg_cong, of "map atm_of"] by (auto simp: comp_def)
     moreover have "\<And>i. \<not> generalizes_atm (tm_at i) (tm_at (Suc i))"
       unfolding tm_at_def generalizes_atm_def atm_of_atms_subst by (simp add: Ls_\<tau>_strict_tm)
     ultimately have "\<And>i. strictly_generalizes_atm (tm_at (Suc i)) (tm_at i)"
       unfolding strictly_generalizes_atm_def by blast
     then have False
       using wf_strictly_generalizes_atm[unfolded wfP_def wf_iff_no_infinite_down_chain] by blast
   }
   then show "wfP (strictly_generalizes :: 'a clause \<Rightarrow> _ \<Rightarrow> _)"
     unfolding wfP_def by (blast intro: wf_iff_no_infinite_down_chain[THEN iffD2])
 qed
 
 lemma strict_subset_subst_strictly_subsumes: "C \<cdot> \<eta> \<subset># D \<Longrightarrow> strictly_subsumes C D"
   by (metis leD mset_subset_size size_mset_mono size_subst strictly_subsumes_def
       subset_mset.dual_order.strict_implies_order substitution_ops.subsumes_def)
 
 lemma generalizes_refl: "generalizes C C"
   unfolding generalizes_def by (rule exI[of _ id_subst]) auto
 
 lemma generalizes_trans: "generalizes C D \<Longrightarrow> generalizes D E \<Longrightarrow> generalizes C E"
   unfolding generalizes_def using subst_cls_comp_subst by blast
 
 lemma subsumes_refl: "subsumes C C"
   unfolding subsumes_def by (rule exI[of _ id_subst]) auto
 
 lemma subsumes_trans: "subsumes C D \<Longrightarrow> subsumes D E \<Longrightarrow> subsumes C E"
   unfolding subsumes_def
   by (metis (no_types) subset_mset.trans subst_cls_comp_subst subst_cls_mono_mset)
 
 lemma strictly_generalizes_irrefl: "\<not> strictly_generalizes C C"
   unfolding strictly_generalizes_def by blast
 
 lemma strictly_generalizes_antisym: "strictly_generalizes C D \<Longrightarrow> \<not> strictly_generalizes D C"
   unfolding strictly_generalizes_def by blast
 
 lemma strictly_generalizes_trans:
   "strictly_generalizes C D \<Longrightarrow> strictly_generalizes D E \<Longrightarrow> strictly_generalizes C E"
   unfolding strictly_generalizes_def using generalizes_trans by blast
 
 lemma strictly_subsumes_irrefl: "\<not> strictly_subsumes C C"
   unfolding strictly_subsumes_def by blast
 
 lemma strictly_subsumes_antisym: "strictly_subsumes C D \<Longrightarrow> \<not> strictly_subsumes D C"
   unfolding strictly_subsumes_def by blast
 
 lemma strictly_subsumes_trans:
   "strictly_subsumes C D \<Longrightarrow> strictly_subsumes D E \<Longrightarrow> strictly_subsumes C E"
   unfolding strictly_subsumes_def using subsumes_trans by blast
 
 lemma subset_strictly_subsumes: "C \<subset># D \<Longrightarrow> strictly_subsumes C D"
   using strict_subset_subst_strictly_subsumes[of C id_subst] by auto
 
 lemma strictly_generalizes_neq: "strictly_generalizes D' D \<Longrightarrow> D' \<noteq> D \<cdot> \<sigma>"
   unfolding strictly_generalizes_def generalizes_def by blast
 
 lemma strictly_subsumes_neq: "strictly_subsumes D' D \<Longrightarrow> D' \<noteq> D \<cdot> \<sigma>"
   unfolding strictly_subsumes_def subsumes_def by blast
 
 lemma strictly_subsumes_has_minimum:
   assumes "CC \<noteq> {}"
   shows "\<exists>C \<in> CC. \<forall>D \<in> CC. \<not> strictly_subsumes D C"
 proof (rule ccontr)
   assume "\<not> (\<exists>C \<in> CC. \<forall>D\<in>CC. \<not> strictly_subsumes D C)"
   then have "\<forall>C \<in> CC. \<exists>D \<in> CC. strictly_subsumes D C"
     by blast
   then obtain f where
     f_p: "\<forall>C \<in> CC. f C \<in> CC \<and> strictly_subsumes (f C) C"
     by metis
   from assms obtain C where
     C_p: "C \<in> CC"
     by auto
 
   define c :: "nat \<Rightarrow> 'a clause" where
     "\<And>n. c n = (f ^^ n) C"
 
   have incc: "c i \<in> CC" for i
     by (induction i) (auto simp: c_def f_p C_p)
   have ps: "\<forall>i. strictly_subsumes (c (Suc i)) (c i)"
     using incc f_p unfolding c_def by auto
   have "\<forall>i. size (c i) \<ge> size (c (Suc i))"
     using ps unfolding strictly_subsumes_def subsumes_def by (metis size_mset_mono size_subst)
   then have lte: "\<forall>i. (size \<circ> c) i \<ge> (size \<circ> c) (Suc i)"
     unfolding comp_def .
   then have "\<exists>l. \<forall>l' \<ge> l. size (c l') = size (c (Suc l'))"
     using f_Suc_decr_eventually_const comp_def by auto
   then obtain l where
     l_p: "\<forall>l' \<ge> l. size (c l') = size (c (Suc l'))"
     by metis
   then have "\<forall>l' \<ge> l. strictly_generalizes (c (Suc l')) (c l')"
     using ps unfolding strictly_generalizes_def generalizes_def
     by (metis size_subst less_irrefl strictly_subsumes_def mset_subset_size subset_mset_def
         subsumes_def strictly_subsumes_neq)
   then have "\<forall>i. strictly_generalizes (c (Suc i + l)) (c (i + l))"
     unfolding strictly_generalizes_def generalizes_def by auto
   then have "\<exists>f. \<forall>i. strictly_generalizes (f (Suc i)) (f i)"
     by (rule exI[of _ "\<lambda>x. c (x + l)"])
   then show False
     using wf_strictly_generalizes
       wf_iff_no_infinite_down_chain[of "{(x, y). strictly_generalizes x y}"]
     unfolding wfP_def by auto
 qed
 
 lemma wf_strictly_subsumes: "wfP strictly_subsumes"
   using strictly_subsumes_has_minimum by (metis equals0D wfP_eq_minimal)
 
 lemma variants_imp_exists_substitution: "variants D D' \<Longrightarrow> \<exists>\<sigma>. D \<cdot> \<sigma> = D'"
   unfolding variants_iff_subsumes subsumes_def
   by (meson strictly_subsumes_def subset_mset_def strict_subset_subst_strictly_subsumes subsumes_def)
 
 lemma strictly_subsumes_variants:
   assumes "strictly_subsumes E D" and "variants D D'"
   shows "strictly_subsumes E D'"
 proof -
   from assms obtain \<sigma> \<sigma>' where
     \<sigma>_\<sigma>'_p: "D \<cdot> \<sigma> = D' \<and> D' \<cdot> \<sigma>' = D"
     using variants_imp_exists_substitution variants_sym by metis
 
   from assms obtain \<sigma>'' where
     "E \<cdot> \<sigma>'' \<subseteq># D"
     unfolding strictly_subsumes_def subsumes_def by auto
   then have "E \<cdot> \<sigma>'' \<cdot> \<sigma> \<subseteq># D \<cdot> \<sigma>"
     using subst_cls_mono_mset by blast
   then have "E \<cdot> (\<sigma>'' \<odot> \<sigma>) \<subseteq># D'"
     using \<sigma>_\<sigma>'_p by auto
   moreover from assms have n: "\<nexists>\<sigma>. D \<cdot> \<sigma> \<subseteq># E"
     unfolding strictly_subsumes_def subsumes_def by auto
   have "\<nexists>\<sigma>. D' \<cdot> \<sigma> \<subseteq># E"
   proof
     assume "\<exists>\<sigma>'''. D' \<cdot> \<sigma>''' \<subseteq># E"
     then obtain \<sigma>''' where
       "D' \<cdot> \<sigma>''' \<subseteq># E"
       by auto
     then have "D \<cdot> (\<sigma> \<odot> \<sigma>''') \<subseteq># E"
       using \<sigma>_\<sigma>'_p by auto
     then show False
       using n by metis
   qed
   ultimately show ?thesis
     unfolding strictly_subsumes_def subsumes_def by metis
 qed
 
 lemma neg_strictly_subsumes_variants:
   assumes "\<not> strictly_subsumes E D" and "variants D D'"
   shows "\<not> strictly_subsumes E D'"
   using assms strictly_subsumes_variants variants_sym by auto
 
 end
 
 
 subsection \<open>Most General Unifiers\<close>
 
 locale mgu = substitution subst_atm id_subst comp_subst renamings_apart atm_of_atms
   for
     subst_atm :: "'a \<Rightarrow> 's \<Rightarrow> 'a" and
     id_subst :: 's and
     comp_subst :: "'s \<Rightarrow> 's \<Rightarrow> 's" and
-    atm_of_atms :: "'a list \<Rightarrow> 'a" and
-    renamings_apart :: "'a literal multiset list \<Rightarrow> 's list" +
+    renamings_apart :: "'a literal multiset list \<Rightarrow> 's list"  and
+    atm_of_atms :: "'a list \<Rightarrow> 'a"+
   fixes
     mgu :: "'a set set \<Rightarrow> 's option"
   assumes
     mgu_sound: "finite AAA \<Longrightarrow> (\<forall>AA \<in> AAA. finite AA) \<Longrightarrow> mgu AAA = Some \<sigma> \<Longrightarrow> is_mgu \<sigma> AAA" and
     mgu_complete:
       "finite AAA \<Longrightarrow> (\<forall>AA \<in> AAA. finite AA) \<Longrightarrow> is_unifiers \<sigma> AAA \<Longrightarrow> \<exists>\<tau>. mgu AAA = Some \<tau>"
 begin
 
 lemmas is_unifiers_mgu = mgu_sound[unfolded is_mgu_def, THEN conjunct1]
 lemmas is_mgu_most_general = mgu_sound[unfolded is_mgu_def, THEN conjunct2]
 
 lemma mgu_unifier:
   assumes
     aslen: "length As = n" and
     aaslen: "length AAs = n" and
     mgu: "Some \<sigma> = mgu (set_mset ` set (map2 add_mset As AAs))" and
     i_lt: "i < n" and
     a_in: "A \<in># AAs ! i"
   shows "A \<cdot>a \<sigma> = As ! i \<cdot>a \<sigma>"
 proof -
   from mgu have "is_mgu \<sigma> (set_mset ` set (map2 add_mset As AAs))"
     using mgu_sound by auto
   then have "is_unifiers \<sigma> (set_mset ` set (map2 add_mset As AAs))"
     using is_mgu_is_unifiers by auto
   then have "is_unifier \<sigma> (set_mset (add_mset (As ! i) (AAs ! i)))"
     using i_lt aslen aaslen unfolding is_unifiers_def is_unifier_def
     by simp (metis length_zip min.idem nth_mem nth_zip prod.case set_mset_add_mset_insert)
   then show ?thesis
     using aslen aaslen a_in is_unifier_subst_atm_eqI
     by (metis finite_set_mset insertCI set_mset_add_mset_insert)
 qed
 
 end
 
 end
diff --git a/thys/Ordered_Resolution_Prover/FO_Ordered_Resolution.thy b/thys/Ordered_Resolution_Prover/FO_Ordered_Resolution.thy
--- a/thys/Ordered_Resolution_Prover/FO_Ordered_Resolution.thy
+++ b/thys/Ordered_Resolution_Prover/FO_Ordered_Resolution.thy
@@ -1,1412 +1,1412 @@
 (*  Title:       First-Order Ordered Resolution Calculus with Selection
     Author:      Anders Schlichtkrull <andschl at dtu.dk>, 2016, 2017
     Author:      Jasmin Blanchette <j.c.blanchette at vu.nl>, 2014, 2017
     Author:      Dmitriy Traytel <traytel at inf.ethz.ch>, 2014
     Author:      Sophie Tourret <stourret at mpi-inf.mpg.de>, 2020
     Maintainer:  Anders Schlichtkrull <andschl at dtu.dk>
 *)
 
 section \<open>First-Order Ordered Resolution Calculus with Selection\<close>
 
 theory FO_Ordered_Resolution
   imports Abstract_Substitution Ordered_Ground_Resolution Standard_Redundancy
 begin
 
 text \<open>
 This material is based on Section 4.3 (``A Simple Resolution Prover for First-Order Clauses'') of
 Bachmair and Ganzinger's chapter. Specifically, it formalizes the ordered resolution calculus for
 first-order standard clauses presented in Figure 4 and its related lemmas and theorems, including
 soundness and Lemma 4.12 (the lifting lemma).
 
 The following corresponds to pages 41--42 of Section 4.3, until Figure 5 and its explanation.
 \<close>
 
-locale FO_resolution = mgu subst_atm id_subst comp_subst atm_of_atms renamings_apart mgu
+locale FO_resolution = mgu subst_atm id_subst comp_subst renamings_apart atm_of_atms mgu
   for
     subst_atm :: "'a :: wellorder \<Rightarrow> 's \<Rightarrow> 'a" and
     id_subst :: "'s" and
     comp_subst :: "'s \<Rightarrow> 's \<Rightarrow> 's" and
     renamings_apart :: "'a literal multiset list \<Rightarrow> 's list" and
     atm_of_atms :: "'a list \<Rightarrow> 'a" and
     mgu :: "'a set set \<Rightarrow> 's option" +
   fixes
     less_atm :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   assumes
     less_atm_stable: "less_atm A B \<Longrightarrow> less_atm (A \<cdot>a \<sigma>) (B \<cdot>a \<sigma>)" and
     less_atm_ground: "is_ground_atm A \<Longrightarrow> is_ground_atm B \<Longrightarrow> less_atm A B \<Longrightarrow> A < B"
 begin
 
 
 subsection \<open>Library\<close>
 
 lemma Bex_cartesian_product: "(\<exists>xy \<in> A \<times> B. P xy) \<equiv> (\<exists>x \<in> A. \<exists>y \<in> B. P (x, y))"
   by simp
 
 lemma eql_map_neg_lit_eql_atm:
   assumes "map (\<lambda>L. L \<cdot>l \<eta>) (map Neg As') = map Neg As"
   shows "As' \<cdot>al \<eta> = As"
   using assms by (induction As' arbitrary: As) auto
 
 lemma instance_list:
   assumes "negs (mset As) = SDA' \<cdot> \<eta>"
   shows "\<exists>As'. negs (mset As') = SDA' \<and> As' \<cdot>al \<eta> = As"
 proof -
   from assms have negL: "\<forall>L \<in># SDA'. is_neg L"
     using Melem_subst_cls subst_lit_in_negs_is_neg by metis
 
   from assms have "{#L \<cdot>l \<eta>. L \<in># SDA'#} = mset (map Neg As)"
     using subst_cls_def by auto
   then have "\<exists>NAs'. map (\<lambda>L. L \<cdot>l \<eta>) NAs' = map Neg As \<and> mset NAs' = SDA'"
     using image_mset_of_subset_list[of "\<lambda>L. L \<cdot>l \<eta>" SDA' "map Neg As"] by auto
   then obtain As' where As'_p:
     "map (\<lambda>L. L \<cdot>l \<eta>) (map Neg As') = map Neg As \<and> mset (map Neg As') = SDA'"
     by (metis (no_types, lifting) Neg_atm_of_iff negL ex_map_conv set_mset_mset)
 
   have "negs (mset As') = SDA'"
     using As'_p by auto
   moreover have "map (\<lambda>L. L \<cdot>l \<eta>) (map Neg As') = map Neg As"
     using As'_p by auto
   then have "As' \<cdot>al \<eta> = As"
     using eql_map_neg_lit_eql_atm by auto
   ultimately show ?thesis
     by blast
 qed
 
 lemma map2_add_mset_map:
   assumes "length AAs' = n" and "length As' = n"
   shows "map2 add_mset (As' \<cdot>al \<eta>) (AAs' \<cdot>aml \<eta>) = map2 add_mset As' AAs' \<cdot>aml \<eta>"
   using assms
 proof (induction n arbitrary: AAs' As')
   case (Suc n)
   then have "map2 add_mset (tl (As' \<cdot>al \<eta>)) (tl (AAs' \<cdot>aml \<eta>)) = map2 add_mset (tl As') (tl AAs') \<cdot>aml \<eta>"
     by simp
   moreover have Succ: "length (As' \<cdot>al \<eta>) = Suc n" "length (AAs' \<cdot>aml \<eta>) = Suc n"
     using Suc(3) Suc(2) by auto
   then have "length (tl (As' \<cdot>al \<eta>)) = n" "length (tl (AAs' \<cdot>aml \<eta>)) = n"
     by auto
   then have "length (map2 add_mset (tl (As' \<cdot>al \<eta>)) (tl (AAs' \<cdot>aml \<eta>))) = n"
     "length (map2 add_mset (tl As') (tl AAs') \<cdot>aml \<eta>) = n"
     using Suc(2,3) by auto
   ultimately have "\<forall>i < n. tl (map2 add_mset ( (As' \<cdot>al \<eta>)) ((AAs' \<cdot>aml \<eta>))) ! i =
     tl (map2 add_mset (As') (AAs') \<cdot>aml \<eta>) ! i"
     using Suc(2,3) Succ by (simp add: map2_tl map_tl subst_atm_mset_list_def del: subst_atm_list_tl)
   moreover have nn: "length (map2 add_mset ((As' \<cdot>al \<eta>)) ((AAs' \<cdot>aml \<eta>))) = Suc n"
     "length (map2 add_mset (As') (AAs') \<cdot>aml \<eta>) = Suc n"
     using Succ Suc by auto
   ultimately have "\<forall>i. i < Suc n \<longrightarrow> i > 0 \<longrightarrow>
     map2 add_mset (As' \<cdot>al \<eta>) (AAs' \<cdot>aml \<eta>) ! i = (map2 add_mset As' AAs' \<cdot>aml \<eta>) ! i"
     by (auto simp: subst_atm_mset_list_def gr0_conv_Suc subst_atm_mset_def)
   moreover have "add_mset (hd As' \<cdot>a \<eta>) (hd AAs' \<cdot>am \<eta>) = add_mset (hd As') (hd AAs') \<cdot>am \<eta>"
     unfolding subst_atm_mset_def by auto
   then have "(map2 add_mset (As' \<cdot>al \<eta>) (AAs' \<cdot>aml \<eta>)) ! 0  = (map2 add_mset (As') (AAs') \<cdot>aml \<eta>) ! 0"
     using Suc by (simp add: Succ(2) subst_atm_mset_def)
   ultimately have "\<forall>i < Suc n. (map2 add_mset (As' \<cdot>al \<eta>) (AAs' \<cdot>aml \<eta>)) ! i =
     (map2 add_mset (As') (AAs') \<cdot>aml \<eta>) ! i"
     using Suc by auto
   then show ?case
     using nn list_eq_iff_nth_eq by metis
 qed auto
 
 context
   fixes S :: "'a clause \<Rightarrow> 'a clause"
 begin
 
 
 subsection \<open>Calculus\<close>
 
 text \<open>
 The following corresponds to Figure 4.
 \<close>
 
 definition maximal_wrt :: "'a \<Rightarrow> 'a literal multiset \<Rightarrow> bool" where
   "maximal_wrt A C \<longleftrightarrow> (\<forall>B \<in> atms_of C. \<not> less_atm A B)"
 
 definition strictly_maximal_wrt :: "'a \<Rightarrow> 'a literal multiset \<Rightarrow> bool" where
   "strictly_maximal_wrt A C \<equiv> \<forall>B \<in> atms_of C. A \<noteq> B \<and> \<not> less_atm A B"
 
 lemma strictly_maximal_wrt_maximal_wrt: "strictly_maximal_wrt A C \<Longrightarrow> maximal_wrt A C"
   unfolding maximal_wrt_def strictly_maximal_wrt_def by auto
 
 lemma maximal_wrt_subst: "maximal_wrt (A \<cdot>a \<sigma>) (C \<cdot> \<sigma>) \<Longrightarrow> maximal_wrt A C"
   unfolding maximal_wrt_def using in_atms_of_subst less_atm_stable by blast
 
 lemma strictly_maximal_wrt_subst:
   "strictly_maximal_wrt (A \<cdot>a \<sigma>) (C \<cdot> \<sigma>) \<Longrightarrow> strictly_maximal_wrt A C"
   unfolding strictly_maximal_wrt_def using in_atms_of_subst less_atm_stable by blast
 
 inductive eligible :: "'s \<Rightarrow> 'a list \<Rightarrow> 'a clause \<Rightarrow> bool" where
   eligible:
     "S DA = negs (mset As) \<or> S DA = {#} \<and> length As = 1 \<and> maximal_wrt (As ! 0 \<cdot>a \<sigma>) (DA \<cdot> \<sigma>) \<Longrightarrow>
      eligible \<sigma> As DA"
 
 inductive
   ord_resolve
   :: "'a clause list \<Rightarrow> 'a clause \<Rightarrow> 'a multiset list \<Rightarrow> 'a list \<Rightarrow> 's \<Rightarrow> 'a clause \<Rightarrow> bool"
 where
   ord_resolve:
     "length CAs = n \<Longrightarrow>
      length Cs = n \<Longrightarrow>
      length AAs = n \<Longrightarrow>
      length As = n \<Longrightarrow>
      n \<noteq> 0 \<Longrightarrow>
      (\<forall>i < n. CAs ! i = Cs ! i + poss (AAs ! i)) \<Longrightarrow>
      (\<forall>i < n. AAs ! i \<noteq> {#}) \<Longrightarrow>
      Some \<sigma> = mgu (set_mset ` set (map2 add_mset As AAs)) \<Longrightarrow>
      eligible \<sigma> As (D + negs (mset As)) \<Longrightarrow>
      (\<forall>i < n. strictly_maximal_wrt (As ! i \<cdot>a \<sigma>) (Cs ! i \<cdot> \<sigma>)) \<Longrightarrow>
      (\<forall>i < n. S (CAs ! i) = {#}) \<Longrightarrow>
      ord_resolve CAs (D + negs (mset As)) AAs As \<sigma> ((\<Sum>\<^sub># (mset Cs) + D) \<cdot> \<sigma>)"
 
 inductive
   ord_resolve_rename
   :: "'a clause list \<Rightarrow> 'a clause \<Rightarrow> 'a multiset list \<Rightarrow> 'a list \<Rightarrow> 's \<Rightarrow> 'a clause \<Rightarrow> bool"
 where
   ord_resolve_rename:
     "length CAs = n \<Longrightarrow>
      length AAs = n \<Longrightarrow>
      length As = n \<Longrightarrow>
      (\<forall>i < n. poss (AAs ! i) \<subseteq># CAs ! i) \<Longrightarrow>
      negs (mset As) \<subseteq># DA \<Longrightarrow>
      \<rho> = hd (renamings_apart (DA # CAs)) \<Longrightarrow>
      \<rho>s = tl (renamings_apart (DA # CAs)) \<Longrightarrow>
      ord_resolve (CAs \<cdot>\<cdot>cl \<rho>s) (DA \<cdot> \<rho>) (AAs \<cdot>\<cdot>aml \<rho>s) (As \<cdot>al \<rho>) \<sigma> E \<Longrightarrow>
      ord_resolve_rename CAs DA AAs As \<sigma> E"
 
 lemma ord_resolve_empty_main_prem: "\<not> ord_resolve Cs {#} AAs As \<sigma> E"
   by (simp add: ord_resolve.simps)
 
 lemma ord_resolve_rename_empty_main_prem: "\<not> ord_resolve_rename Cs {#} AAs As \<sigma> E"
   by (simp add: ord_resolve_empty_main_prem ord_resolve_rename.simps)
 
 
 subsection \<open>Soundness\<close>
 
 text \<open>
 Soundness is not discussed in the chapter, but it is an important property.
 \<close>
 
 lemma ord_resolve_ground_inst_sound:
   assumes
     res_e: "ord_resolve CAs DA AAs As \<sigma> E" and
     cc_inst_true: "I \<Turnstile>m mset CAs \<cdot>cm \<sigma> \<cdot>cm \<eta>" and
     d_inst_true: "I \<Turnstile> DA \<cdot> \<sigma> \<cdot> \<eta>" and
     ground_subst_\<eta>: "is_ground_subst \<eta>"
   shows "I \<Turnstile> E \<cdot> \<eta>"
   using res_e
 proof (cases rule: ord_resolve.cases)
   case (ord_resolve n Cs D)
   note da = this(1) and e = this(2) and cas_len = this(3) and cs_len = this(4) and
     aas_len = this(5) and as_len = this(6) and cas = this(8) and mgu = this(10) and
     len = this(1)
 
   have len: "length CAs = length As"
     using as_len cas_len by auto
   have "is_ground_subst (\<sigma> \<odot> \<eta>)"
     using ground_subst_\<eta> by (rule is_ground_comp_subst)
   then have cc_true: "I \<Turnstile>m mset CAs \<cdot>cm \<sigma> \<cdot>cm \<eta>" and d_true: "I \<Turnstile> DA \<cdot> \<sigma> \<cdot> \<eta>"
     using cc_inst_true d_inst_true by auto
 
   from mgu have unif: "\<forall>i < n. \<forall>A\<in>#AAs ! i. A \<cdot>a \<sigma> = As ! i \<cdot>a \<sigma>"
     using mgu_unifier as_len aas_len by blast
 
   show "I \<Turnstile> E \<cdot> \<eta>"
   proof (cases "\<forall>A \<in> set As. A \<cdot>a \<sigma> \<cdot>a \<eta> \<in> I")
     case True
     then have "\<not> I \<Turnstile> negs (mset As) \<cdot> \<sigma> \<cdot> \<eta>"
       unfolding true_cls_def[of I] by auto
     then have "I \<Turnstile> D \<cdot> \<sigma> \<cdot> \<eta>"
       using d_true da by auto
     then show ?thesis
       unfolding e by auto
   next
     case False
     then obtain i where a_in_aa: "i < length CAs" and a_false: "(As ! i) \<cdot>a \<sigma> \<cdot>a \<eta> \<notin> I"
       using da len by (metis in_set_conv_nth)
     define C where "C \<equiv> Cs ! i"
     define BB where "BB \<equiv> AAs ! i"
     have c_cf': "C \<subseteq># \<Sum>\<^sub># (mset CAs)"
       unfolding C_def using a_in_aa cas cas_len
       by (metis less_subset_eq_Union_mset mset_subset_eq_add_left subset_mset.trans)
     have c_in_cc: "C + poss BB \<in># mset CAs"
       using C_def BB_def a_in_aa cas_len in_set_conv_nth cas by fastforce
     {
       fix B
       assume "B \<in># BB"
       then have "B \<cdot>a \<sigma> = (As ! i) \<cdot>a \<sigma>"
         using unif a_in_aa cas_len unfolding BB_def by auto
     }
     then have "\<not> I \<Turnstile> poss BB \<cdot> \<sigma> \<cdot> \<eta>"
       using a_false by (auto simp: true_cls_def)
     moreover have "I \<Turnstile> (C + poss BB) \<cdot> \<sigma> \<cdot> \<eta>"
       using c_in_cc cc_true true_cls_mset_true_cls[of I "mset CAs \<cdot>cm \<sigma> \<cdot>cm \<eta>"] by force
     ultimately have "I \<Turnstile> C \<cdot> \<sigma> \<cdot> \<eta>"
       by simp
     then show ?thesis
       unfolding e subst_cls_union using c_cf' C_def a_in_aa cas_len cs_len
       by (metis (no_types, lifting) mset_subset_eq_add_left nth_mem_mset set_mset_mono sum_mset.remove true_cls_mono subst_cls_mono)
   qed
 qed
 
 text \<open>
 The previous lemma is not only used to prove soundness, but also the following lemma which is
 used to prove Lemma 4.10.
 \<close>
 
 lemma ord_resolve_rename_ground_inst_sound:
   assumes
     "ord_resolve_rename CAs DA AAs As \<sigma> E" and
     "\<rho>s = tl (renamings_apart (DA # CAs))" and
     "\<rho> = hd (renamings_apart (DA # CAs))" and
     "I \<Turnstile>m (mset (CAs \<cdot>\<cdot>cl \<rho>s)) \<cdot>cm \<sigma> \<cdot>cm \<eta>" and
     "I \<Turnstile> DA \<cdot> \<rho> \<cdot> \<sigma> \<cdot> \<eta>" and
     "is_ground_subst \<eta>"
   shows "I \<Turnstile> E \<cdot> \<eta>"
   using assms by (cases rule: ord_resolve_rename.cases) (fast intro: ord_resolve_ground_inst_sound)
 
 text \<open>
 Here follows the soundness theorem for the resolution rule.
 \<close>
 
 theorem ord_resolve_sound:
  assumes
    res_e: "ord_resolve CAs DA AAs As \<sigma> E" and
    cc_d_true: "\<And>\<sigma>. is_ground_subst \<sigma> \<Longrightarrow> I \<Turnstile>m (mset CAs + {#DA#}) \<cdot>cm \<sigma>" and
    ground_subst_\<eta>: "is_ground_subst \<eta>"
  shows "I \<Turnstile> E \<cdot> \<eta>"
 proof (use res_e in \<open>cases rule: ord_resolve.cases\<close>)
   case (ord_resolve n Cs D)
   note da = this(1) and e = this(2) and cas_len = this(3) and cs_len = this(4)
     and aas_len = this(5) and as_len = this(6) and cas = this(8) and mgu = this(10)
   have ground_subst_\<sigma>_\<eta>: "is_ground_subst (\<sigma> \<odot> \<eta>)"
     using ground_subst_\<eta> by (rule is_ground_comp_subst)
   have cas_true: "I \<Turnstile>m mset CAs \<cdot>cm \<sigma> \<cdot>cm \<eta>"
     using cc_d_true ground_subst_\<sigma>_\<eta> by fastforce
   have da_true: "I \<Turnstile> DA \<cdot> \<sigma> \<cdot> \<eta>"
     using cc_d_true ground_subst_\<sigma>_\<eta> by fastforce
   show "I \<Turnstile> E \<cdot> \<eta>"
     using ord_resolve_ground_inst_sound[OF res_e cas_true da_true] ground_subst_\<eta> by auto
 qed
 
 lemma subst_sound:
   assumes
     "\<And>\<sigma>. is_ground_subst \<sigma> \<Longrightarrow> I \<Turnstile> C \<cdot> \<sigma>" and
     "is_ground_subst \<eta>"
   shows "I \<Turnstile> C \<cdot> \<rho> \<cdot> \<eta>"
   using assms is_ground_comp_subst subst_cls_comp_subst by metis
 
 lemma subst_sound_scl:
   assumes
     len: "length P = length CAs" and
     true_cas: "\<And>\<sigma>. is_ground_subst \<sigma> \<Longrightarrow> I \<Turnstile>m mset CAs \<cdot>cm \<sigma>" and
     ground_subst_\<eta>: "is_ground_subst \<eta>"
   shows "I \<Turnstile>m mset (CAs \<cdot>\<cdot>cl P) \<cdot>cm \<eta>"
 proof -
   from true_cas have "\<And>CA. CA\<in># mset CAs \<Longrightarrow> (\<And>\<sigma>. is_ground_subst \<sigma> \<Longrightarrow> I \<Turnstile> CA \<cdot> \<sigma>)"
     unfolding true_cls_mset_def by force
   then have "\<forall>i < length CAs. \<forall>\<sigma>. is_ground_subst \<sigma> \<longrightarrow> (I \<Turnstile> CAs ! i \<cdot> \<sigma>)"
     using in_set_conv_nth by auto
   then have true_cp: "\<forall>i < length CAs. \<forall>\<sigma>. is_ground_subst \<sigma> \<longrightarrow> I \<Turnstile> CAs ! i \<cdot> P ! i \<cdot> \<sigma>"
     using subst_sound len by auto
 
   {
     fix CA
     assume "CA \<in># mset (CAs \<cdot>\<cdot>cl P)"
     then obtain i where
       i_x: "i < length (CAs \<cdot>\<cdot>cl P)" "CA = (CAs \<cdot>\<cdot>cl P) ! i"
       by (metis in_mset_conv_nth)
     then have "\<forall>\<sigma>. is_ground_subst \<sigma> \<longrightarrow> I \<Turnstile> CA \<cdot> \<sigma>"
       using true_cp unfolding subst_cls_lists_def by (simp add: len)
   }
   then show ?thesis
     using assms unfolding true_cls_mset_def by auto
 qed
 
 text \<open>
 Here follows the soundness theorem for the resolution rule with renaming.
 \<close>
 
 lemma ord_resolve_rename_sound:
   assumes
     res_e: "ord_resolve_rename CAs DA AAs As \<sigma> E" and
     cc_d_true: "\<And>\<sigma>. is_ground_subst \<sigma> \<Longrightarrow> I \<Turnstile>m ((mset CAs) + {#DA#}) \<cdot>cm \<sigma>" and
     ground_subst_\<eta>: "is_ground_subst \<eta>"
   shows "I \<Turnstile> E \<cdot> \<eta>"
   using res_e
 proof (cases rule: ord_resolve_rename.cases)
   case (ord_resolve_rename n \<rho> \<rho>s)
   note \<rho>s = this(7) and res = this(8)
   have len: "length \<rho>s = length CAs"
     using \<rho>s renamings_apart_length by auto
   have "\<And>\<sigma>. is_ground_subst \<sigma> \<Longrightarrow> I \<Turnstile>m (mset (CAs \<cdot>\<cdot>cl \<rho>s) + {#DA \<cdot> \<rho>#}) \<cdot>cm \<sigma>"
     using subst_sound_scl[OF len, of I] subst_sound cc_d_true by auto
   then show "I \<Turnstile> E \<cdot> \<eta>"
     using ground_subst_\<eta> ord_resolve_sound[OF res] by simp
 qed
 
 
 subsection \<open>Other Basic Properties\<close>
 
 lemma ord_resolve_unique:
   assumes
     "ord_resolve CAs DA AAs As \<sigma> E" and
     "ord_resolve CAs DA AAs As \<sigma>' E'"
   shows "\<sigma> = \<sigma>' \<and> E = E'"
   using assms
 proof (cases rule: ord_resolve.cases[case_product ord_resolve.cases], intro conjI)
   case (ord_resolve_ord_resolve CAs n Cs AAs As \<sigma>'' DA CAs' n' Cs' AAs' As' \<sigma>''' DA')
   note res = this(1-17) and res' = this(18-34)
 
   show \<sigma>: "\<sigma> = \<sigma>'"
     using res(3-5,14) res'(3-5,14) by (metis option.inject)
 
   have "Cs = Cs'"
     using res(1,3,7,8,12) res'(1,3,7,8,12) by (metis add_right_imp_eq nth_equalityI)
   moreover have "DA = DA'"
     using res(2,4) res'(2,4) by fastforce
   ultimately show "E = E'"
     using res(5,6) res'(5,6) \<sigma> by blast
 qed
 
 lemma ord_resolve_rename_unique:
   assumes
     "ord_resolve_rename CAs DA AAs As \<sigma> E" and
     "ord_resolve_rename CAs DA AAs As \<sigma>' E'"
   shows "\<sigma> = \<sigma>' \<and> E = E'"
   using assms unfolding ord_resolve_rename.simps using ord_resolve_unique by meson
 
 lemma ord_resolve_max_side_prems: "ord_resolve CAs DA AAs As \<sigma> E \<Longrightarrow> length CAs \<le> size DA"
   by (auto elim!: ord_resolve.cases)
 
 lemma ord_resolve_rename_max_side_prems:
   "ord_resolve_rename CAs DA AAs As \<sigma> E \<Longrightarrow> length CAs \<le> size DA"
   by (elim ord_resolve_rename.cases, drule ord_resolve_max_side_prems, simp add: renamings_apart_length)
 
 
 subsection \<open>Inference System\<close>
 
 definition ord_FO_\<Gamma> :: "'a inference set" where
   "ord_FO_\<Gamma> = {Infer (mset CAs) DA E | CAs DA AAs As \<sigma> E. ord_resolve_rename CAs DA AAs As \<sigma> E}"
 
 interpretation ord_FO_resolution: inference_system ord_FO_\<Gamma> .
 
 lemma finite_ord_FO_resolution_inferences_between:
   assumes fin_cc: "finite CC"
   shows "finite (ord_FO_resolution.inferences_between CC C)"
 proof -
   let ?CCC = "CC \<union> {C}"
 
   define all_AA where "all_AA = (\<Union>D \<in> ?CCC. atms_of D)"
   define max_ary where "max_ary = Max (size ` ?CCC)"
   define CAS where "CAS = {CAs. CAs \<in> lists ?CCC \<and> length CAs \<le> max_ary}"
   define AS where "AS = {As. As \<in> lists all_AA \<and> length As \<le> max_ary}"
   define AAS where "AAS = {AAs. AAs \<in> lists (mset ` AS) \<and> length AAs \<le> max_ary}"
 
   note defs = all_AA_def max_ary_def CAS_def AS_def AAS_def
 
   let ?infer_of =
     "\<lambda>CAs DA AAs As. Infer (mset CAs) DA (THE E. \<exists>\<sigma>. ord_resolve_rename CAs DA AAs As \<sigma> E)"
 
   let ?Z = "{\<gamma> | CAs DA AAs As \<sigma> E \<gamma>. \<gamma> = Infer (mset CAs) DA E
     \<and> ord_resolve_rename CAs DA AAs As \<sigma> E \<and> infer_from ?CCC \<gamma> \<and> C \<in># prems_of \<gamma>}"
   let ?Y = "{Infer (mset CAs) DA E | CAs DA AAs As \<sigma> E.
     ord_resolve_rename CAs DA AAs As \<sigma> E \<and> set CAs \<union> {DA} \<subseteq> ?CCC}"
   let ?X = "{?infer_of CAs DA AAs As | CAs DA AAs As. CAs \<in> CAS \<and> DA \<in> ?CCC \<and> AAs \<in> AAS \<and> As \<in> AS}"
   let ?W = "CAS \<times> ?CCC \<times> AAS \<times> AS"
 
   have fin_w: "finite ?W"
     unfolding defs using fin_cc by (simp add: finite_lists_length_le lists_eq_set)
 
   have "?Z \<subseteq> ?Y"
     by (force simp: infer_from_def)
   also have "\<dots> \<subseteq> ?X"
   proof -
     {
       fix CAs DA AAs As \<sigma> E
       assume
         res_e: "ord_resolve_rename CAs DA AAs As \<sigma> E" and
         da_in: "DA \<in> ?CCC" and
         cas_sub: "set CAs \<subseteq> ?CCC"
 
       have "E = (THE E. \<exists>\<sigma>. ord_resolve_rename CAs DA AAs As \<sigma> E)
         \<and> CAs \<in> CAS \<and> AAs \<in> AAS \<and> As \<in> AS" (is "?e \<and> ?cas \<and> ?aas \<and> ?as")
       proof (intro conjI)
         show ?e
           using res_e ord_resolve_rename_unique by (blast intro: the_equality[symmetric])
       next
         show ?cas
           unfolding CAS_def max_ary_def using cas_sub
             ord_resolve_rename_max_side_prems[OF res_e] da_in fin_cc
           by (auto simp add: Max_ge_iff)
       next
         show ?aas
           using res_e
         proof (cases rule: ord_resolve_rename.cases)
           case (ord_resolve_rename n \<rho> \<rho>s)
           note len_cas = this(1) and len_aas = this(2) and len_as = this(3) and
             aas_sub = this(4) and as_sub = this(5) and res_e' = this(8)
 
           show ?thesis
             unfolding AAS_def
           proof (clarify, intro conjI)
             show "AAs \<in> lists (mset ` AS)"
               unfolding AS_def image_def
             proof clarsimp
               fix AA
               assume "AA \<in> set AAs"
               then obtain i where
                 i_lt: "i < n" and
                 aa: "AA = AAs ! i"
                 by (metis in_set_conv_nth len_aas)
 
               have casi_in: "CAs ! i \<in> ?CCC"
                 using i_lt len_cas cas_sub nth_mem by blast
 
               have pos_aa_sub: "poss AA \<subseteq># CAs ! i"
                 using aa aas_sub i_lt by blast
               then have "set_mset AA \<subseteq> atms_of (CAs ! i)"
                 by (metis atms_of_poss lits_subseteq_imp_atms_subseteq set_mset_mono)
               also have aa_sub: "\<dots> \<subseteq> all_AA"
                 unfolding all_AA_def using casi_in by force
               finally have aa_sub: "set_mset AA \<subseteq> all_AA"
                 .
 
               have "size AA = size (poss AA)"
                 by simp
               also have "\<dots> \<le> size (CAs ! i)"
                 by (rule size_mset_mono[OF pos_aa_sub])
               also have "\<dots> \<le> max_ary"
                 unfolding max_ary_def using fin_cc casi_in by auto
               finally have sz_aa: "size AA \<le> max_ary"
                 .
 
               let ?As' = "sorted_list_of_multiset AA"
 
               have "?As' \<in> lists all_AA"
                 using aa_sub by auto
               moreover have "length ?As' \<le> max_ary"
                 using sz_aa by simp
               moreover have "AA = mset ?As'"
                 by simp
               ultimately show "\<exists>xa. xa \<in> lists all_AA \<and> length xa \<le> max_ary \<and> AA = mset xa"
                 by blast
             qed
           next
             have "length AAs = length As"
               unfolding len_aas len_as ..
             also have "\<dots> \<le> size DA"
               using as_sub size_mset_mono by fastforce
             also have "\<dots> \<le> max_ary"
               unfolding max_ary_def using fin_cc da_in by auto
             finally show "length AAs \<le> max_ary"
               .
           qed
         qed
       next
         show ?as
           unfolding AS_def
         proof (clarify, intro conjI)
           have "set As \<subseteq> atms_of DA"
             using res_e[simplified ord_resolve_rename.simps]
             by (metis atms_of_negs lits_subseteq_imp_atms_subseteq set_mset_mono set_mset_mset)
           also have "\<dots> \<subseteq> all_AA"
             unfolding all_AA_def using da_in by blast
           finally show "As \<in> lists all_AA"
             unfolding lists_eq_set by simp
         next
           have "length As \<le> size DA"
             using res_e[simplified ord_resolve_rename.simps]
               ord_resolve_rename_max_side_prems[OF res_e] by auto
           also have "size DA \<le> max_ary"
             unfolding max_ary_def using fin_cc da_in by auto
           finally show "length As \<le> max_ary"
             .
         qed
       qed
     }
     then show ?thesis
       by simp fast
   qed
   also have "\<dots> \<subseteq> (\<lambda>(CAs, DA, AAs, As). ?infer_of CAs DA AAs As) ` ?W"
     unfolding image_def Bex_cartesian_product by fast
   finally show ?thesis
     unfolding inference_system.inferences_between_def ord_FO_\<Gamma>_def mem_Collect_eq
     by (fast intro: rev_finite_subset[OF finite_imageI[OF fin_w]])
 qed
 
 lemma ord_FO_resolution_inferences_between_empty_empty:
   "ord_FO_resolution.inferences_between {} {#} = {}"
   unfolding ord_FO_resolution.inferences_between_def inference_system.inferences_between_def
     infer_from_def ord_FO_\<Gamma>_def
   using ord_resolve_rename_empty_main_prem by auto
 
 
 subsection \<open>Lifting\<close>
 
 text \<open>
 The following corresponds to the passage between Lemmas 4.11 and 4.12.
 \<close>
 
 context
   fixes M :: "'a clause set"
   assumes select: "selection S"
 begin
 
 interpretation selection
   by (rule select)
 
 definition S_M :: "'a literal multiset \<Rightarrow> 'a literal multiset" where
   "S_M C =
    (if C \<in> grounding_of_clss M then
       (SOME C'. \<exists>D \<sigma>. D \<in> M \<and> C = D \<cdot> \<sigma> \<and> C' = S D \<cdot> \<sigma> \<and> is_ground_subst \<sigma>)
     else
       S C)"
 
 lemma S_M_grounding_of_clss:
   assumes "C \<in> grounding_of_clss M"
   obtains D \<sigma> where
     "D \<in> M \<and> C = D \<cdot> \<sigma> \<and> S_M C = S D \<cdot> \<sigma> \<and> is_ground_subst \<sigma>"
 proof (atomize_elim, unfold S_M_def eqTrueI[OF assms] if_True, rule someI_ex)
   from assms show "\<exists>C' D \<sigma>. D \<in> M \<and> C = D \<cdot> \<sigma> \<and> C' = S D \<cdot> \<sigma> \<and> is_ground_subst \<sigma>"
     by (auto simp: grounding_of_clss_def grounding_of_cls_def)
 qed
 
 lemma S_M_not_grounding_of_clss: "C \<notin> grounding_of_clss M \<Longrightarrow> S_M C = S C"
   unfolding S_M_def by simp
 
 lemma S_M_selects_subseteq: "S_M C \<subseteq># C"
   by (metis S_M_grounding_of_clss S_M_not_grounding_of_clss S_selects_subseteq subst_cls_mono_mset)
 
 lemma S_M_selects_neg_lits: "L \<in># S_M C \<Longrightarrow> is_neg L"
   by (metis Melem_subst_cls S_M_grounding_of_clss S_M_not_grounding_of_clss S_selects_neg_lits
       subst_lit_is_neg)
 
 end
 
 end
 
 text \<open>
 The following corresponds to Lemma 4.12:
 \<close>
 
 lemma ground_resolvent_subset:
   assumes
     gr_cas: "is_ground_cls_list CAs" and
     gr_da: "is_ground_cls DA" and
     res_e: "ord_resolve S CAs DA AAs As \<sigma> E"
   shows "E \<subseteq># \<Sum>\<^sub># (mset CAs) + DA"
   using res_e
 proof (cases rule: ord_resolve.cases)
   case (ord_resolve n Cs D)
   note da = this(1) and e = this(2) and cas_len = this(3) and cs_len = this(4)
     and aas_len = this(5) and as_len = this(6) and cas = this(8) and mgu = this(10)
   then have cs_sub_cas: "\<Sum>\<^sub># (mset Cs) \<subseteq># \<Sum>\<^sub># (mset CAs)"
     using subseteq_list_Union_mset cas_len cs_len by force
   then have cs_sub_cas: "\<Sum>\<^sub># (mset Cs) \<subseteq># \<Sum>\<^sub># (mset CAs)"
     using subseteq_list_Union_mset cas_len cs_len by force
   then have gr_cs: "is_ground_cls_list Cs"
     using gr_cas by simp
   have d_sub_da: "D \<subseteq># DA"
     by (simp add: da)
   then have gr_d: "is_ground_cls D"
     using gr_da is_ground_cls_mono by auto
 
   have "is_ground_cls (\<Sum>\<^sub># (mset Cs) + D)"
     using gr_cs gr_d by auto
   with e have "E = \<Sum>\<^sub># (mset Cs) + D"
     by auto
   then show ?thesis
     using cs_sub_cas d_sub_da by (auto simp: subset_mset.add_mono)
 qed
 
 lemma ord_resolve_obtain_clauses:
   assumes
     res_e: "ord_resolve (S_M S M) CAs DA AAs As \<sigma> E" and
     select: "selection S" and
     grounding: "{DA} \<union> set CAs \<subseteq> grounding_of_clss M" and
     n: "length CAs = n" and
     d: "DA = D + negs (mset As)" and
     c: "(\<forall>i < n. CAs ! i = Cs ! i + poss (AAs ! i))" "length Cs = n" "length AAs = n"
   obtains DA0 \<eta>0 CAs0 \<eta>s0 As0 AAs0 D0 Cs0 where
     "length CAs0 = n"
     "length \<eta>s0 = n"
     "DA0 \<in> M"
     "DA0 \<cdot> \<eta>0 = DA"
     "S DA0 \<cdot> \<eta>0 = S_M S M DA"
     "\<forall>CA0 \<in> set CAs0. CA0 \<in> M"
     "CAs0 \<cdot>\<cdot>cl \<eta>s0 = CAs"
     "map S CAs0 \<cdot>\<cdot>cl \<eta>s0 = map (S_M S M) CAs"
     "is_ground_subst \<eta>0"
     "is_ground_subst_list \<eta>s0"
     "As0  \<cdot>al \<eta>0 = As"
     "AAs0 \<cdot>\<cdot>aml \<eta>s0 = AAs"
     "length As0 = n"
     "D0 \<cdot> \<eta>0 = D"
     "DA0 = D0 + (negs (mset As0))"
     "S_M S M (D + negs (mset As)) \<noteq> {#} \<Longrightarrow> negs (mset As0) = S DA0"
     "length Cs0 = n"
     "Cs0 \<cdot>\<cdot>cl \<eta>s0 = Cs"
     "\<forall>i < n. CAs0 ! i = Cs0 ! i + poss (AAs0 ! i)"
     "length AAs0 = n"
   using res_e
 proof (cases rule: ord_resolve.cases)
   case (ord_resolve n_twin Cs_twins D_twin)
   note da = this(1) and e = this(2) and cas = this(8) and mgu = this(10) and eligible = this(11)
   from ord_resolve have "n_twin = n" "D_twin = D"
     using n d by auto
   moreover have "Cs_twins = Cs"
     using c cas n calculation(1) \<open>length Cs_twins = n_twin\<close> by (auto simp add: nth_equalityI)
   ultimately
   have nz: "n \<noteq> 0" and cs_len: "length Cs = n" and aas_len: "length AAs = n" and as_len: "length As = n"
     and da: "DA = D + negs (mset As)" and eligible: "eligible (S_M S M) \<sigma> As (D + negs (mset As))"
     and cas: "\<forall>i<n. CAs ! i = Cs ! i + poss (AAs ! i)"
     using ord_resolve by force+
 
   note n = \<open>n \<noteq> 0\<close> \<open>length CAs = n\<close> \<open>length Cs = n\<close> \<open>length AAs = n\<close> \<open>length As = n\<close>
 
   interpret S: selection S by (rule select)
 
   \<comment> \<open>Obtain FO side premises\<close>
   have "\<forall>CA \<in> set CAs. \<exists>CA0 \<eta>c0. CA0 \<in> M \<and> CA0 \<cdot> \<eta>c0 = CA \<and> S CA0 \<cdot> \<eta>c0 = S_M S M CA \<and> is_ground_subst \<eta>c0"
     using grounding S_M_grounding_of_clss select by (metis (no_types) le_supE subset_iff)
   then have "\<forall>i < n. \<exists>CA0 \<eta>c0. CA0 \<in> M \<and> CA0 \<cdot> \<eta>c0 = (CAs ! i) \<and> S CA0 \<cdot> \<eta>c0 = S_M S M (CAs ! i) \<and> is_ground_subst \<eta>c0"
     using n by force
   then obtain \<eta>s0f CAs0f where f_p:
     "\<forall>i < n. CAs0f i \<in> M"
     "\<forall>i < n. (CAs0f i) \<cdot> (\<eta>s0f i) = (CAs ! i)"
     "\<forall>i < n. S (CAs0f i)  \<cdot> (\<eta>s0f i) = S_M S M (CAs ! i)"
     "\<forall>i < n. is_ground_subst (\<eta>s0f i)"
     using n by (metis (no_types))
 
   define \<eta>s0 where
     "\<eta>s0 = map \<eta>s0f [0 ..<n]"
   define CAs0 where
     "CAs0 = map CAs0f [0 ..<n]"
 
   have "length \<eta>s0 = n" "length CAs0 = n"
     unfolding \<eta>s0_def CAs0_def by auto
   note n = \<open>length \<eta>s0 = n\<close> \<open>length CAs0 = n\<close> n
 
   \<comment> \<open>The properties we need of the FO side premises\<close>
   have CAs0_in_M: "\<forall>CA0 \<in> set CAs0. CA0 \<in> M"
     unfolding CAs0_def using f_p(1) by auto
   have CAs0_to_CAs: "CAs0 \<cdot>\<cdot>cl \<eta>s0 = CAs"
     unfolding CAs0_def \<eta>s0_def using f_p(2)  by (auto simp: n intro: nth_equalityI)
   have SCAs0_to_SMCAs: "(map S CAs0) \<cdot>\<cdot>cl \<eta>s0 = map (S_M S M) CAs"
     unfolding CAs0_def \<eta>s0_def using f_p(3) n by (force intro: nth_equalityI)
   have sub_ground: "\<forall>\<eta>c0 \<in> set \<eta>s0. is_ground_subst \<eta>c0"
     unfolding \<eta>s0_def using f_p n by force
   then have "is_ground_subst_list \<eta>s0"
     using n unfolding is_ground_subst_list_def by auto
 
   \<comment> \<open>Split side premises CAs0 into Cs0 and AAs0\<close>
   obtain AAs0 Cs0 where AAs0_Cs0_p:
    "AAs0 \<cdot>\<cdot>aml \<eta>s0 = AAs" "length Cs0 = n" "Cs0 \<cdot>\<cdot>cl \<eta>s0 = Cs"
    "\<forall>i < n. CAs0 ! i = Cs0 ! i + poss (AAs0 ! i)" "length AAs0 = n"
   proof -
     have "\<forall>i < n. \<exists>AA0. AA0 \<cdot>am \<eta>s0 ! i = AAs ! i \<and> poss AA0 \<subseteq># CAs0 ! i"
     proof (rule, rule)
       fix i
       assume "i < n"
       have "CAs0 ! i \<cdot> \<eta>s0 ! i = CAs ! i"
         using \<open>i < n\<close> \<open>CAs0 \<cdot>\<cdot>cl \<eta>s0 = CAs\<close> n by force
       moreover have "poss (AAs ! i) \<subseteq># CAs !i"
         using \<open>i < n\<close> cas by auto
       ultimately obtain poss_AA0 where
         nn: "poss_AA0 \<cdot> \<eta>s0 ! i = poss (AAs ! i) \<and> poss_AA0 \<subseteq># CAs0 ! i"
         using cas image_mset_of_subset unfolding subst_cls_def by metis
       then have l: "\<forall>L \<in># poss_AA0. is_pos L"
         unfolding subst_cls_def by (metis Melem_subst_cls imageE literal.disc(1)
             literal.map_disc_iff set_image_mset subst_cls_def subst_lit_def)
 
       define AA0 where
         "AA0 = image_mset atm_of poss_AA0"
 
       have na: "poss AA0 = poss_AA0"
         using l unfolding AA0_def by auto
       then have "AA0 \<cdot>am \<eta>s0 ! i = AAs ! i"
         using nn by (metis (mono_tags) literal.inject(1) multiset.inj_map_strong subst_cls_poss)
       moreover have "poss AA0 \<subseteq># CAs0 ! i"
         using na nn by auto
       ultimately show "\<exists>AA0. AA0 \<cdot>am \<eta>s0 ! i = AAs ! i \<and> poss AA0 \<subseteq># CAs0 ! i"
         by blast
     qed
     then obtain AAs0f where
       AAs0f_p: "\<forall>i < n. AAs0f i \<cdot>am \<eta>s0 ! i = AAs ! i \<and> (poss (AAs0f i)) \<subseteq># CAs0 ! i"
       by metis
 
     define AAs0 where "AAs0 = map AAs0f [0 ..<n]"
 
     then have "length AAs0 = n"
       by auto
     note n = n \<open>length AAs0 = n\<close>
 
     from AAs0_def have "\<forall>i < n. AAs0 ! i \<cdot>am \<eta>s0 ! i = AAs ! i"
       using AAs0f_p by auto
     then have AAs0_AAs: "AAs0 \<cdot>\<cdot>aml \<eta>s0 = AAs"
       using n by (auto intro: nth_equalityI)
 
     from AAs0_def have AAs0_in_CAs0: "\<forall>i < n. poss (AAs0 ! i) \<subseteq># CAs0 ! i"
       using AAs0f_p by auto
 
     define Cs0 where
       "Cs0 = map2 (-) CAs0 (map poss AAs0)"
 
     have "length Cs0 = n"
       using Cs0_def n by auto
     note n = n \<open>length Cs0 = n\<close>
 
     have "\<forall>i < n. CAs0 ! i = Cs0 ! i + poss (AAs0 ! i)"
       using AAs0_in_CAs0 Cs0_def n by auto
     then have "Cs0 \<cdot>\<cdot>cl \<eta>s0 = Cs"
       using \<open>CAs0 \<cdot>\<cdot>cl \<eta>s0 = CAs\<close> AAs0_AAs cas n by (auto intro: nth_equalityI)
 
     show ?thesis
       using that
         \<open>AAs0 \<cdot>\<cdot>aml \<eta>s0 = AAs\<close> \<open>Cs0 \<cdot>\<cdot>cl \<eta>s0 = Cs\<close> \<open>\<forall>i < n. CAs0 ! i = Cs0 ! i + poss (AAs0 ! i)\<close>
         \<open>length AAs0 = n\<close> \<open>length Cs0 = n\<close>
       by blast
   qed
 
   \<comment> \<open>Obtain FO main premise\<close>
   have "\<exists>DA0 \<eta>0. DA0 \<in> M \<and> DA = DA0 \<cdot> \<eta>0 \<and> S DA0 \<cdot> \<eta>0 = S_M S M DA \<and> is_ground_subst \<eta>0"
     using grounding S_M_grounding_of_clss select by (metis le_supE singletonI subsetCE)
   then obtain DA0 \<eta>0 where
     DA0_\<eta>0_p: "DA0 \<in> M \<and> DA = DA0 \<cdot> \<eta>0 \<and> S DA0 \<cdot> \<eta>0 = S_M S M DA \<and> is_ground_subst \<eta>0"
     by auto
   \<comment> \<open>The properties we need of the FO main premise\<close>
   have DA0_in_M: "DA0 \<in> M"
     using DA0_\<eta>0_p by auto
   have DA0_to_DA: "DA0 \<cdot> \<eta>0 = DA"
     using DA0_\<eta>0_p by auto
   have SDA0_to_SMDA: "S DA0 \<cdot> \<eta>0 = S_M S M DA"
     using DA0_\<eta>0_p by auto
   have "is_ground_subst \<eta>0"
     using DA0_\<eta>0_p by auto
 
   \<comment> \<open>Split main premise DA0 into D0 and As0\<close>
   obtain D0 As0 where D0As0_p:
      "As0  \<cdot>al \<eta>0 = As" "length As0 = n" "D0 \<cdot> \<eta>0 = D" "DA0 = D0 + (negs (mset As0))"
     "S_M S M (D + negs (mset As)) \<noteq> {#} \<Longrightarrow> negs (mset As0) = S DA0"
   proof -
     {
       assume a: "S_M S M (D + negs (mset As)) = {#} \<and> length As = (Suc 0)
         \<and> maximal_wrt (As ! 0 \<cdot>a \<sigma>) ((D + negs (mset As)) \<cdot> \<sigma>)"
       then have as: "mset As = {#As ! 0#}"
         by (auto intro: nth_equalityI)
       then have "negs (mset As) = {#Neg (As ! 0)#}"
         by (simp add: \<open>mset As = {#As ! 0#}\<close>)
       then have "DA = D + {#Neg (As ! 0)#}"
         using da by auto
       then obtain L where "L \<in># DA0 \<and> L \<cdot>l \<eta>0 = Neg (As ! 0)"
         using DA0_to_DA by (metis Melem_subst_cls mset_subset_eq_add_right single_subset_iff)
       then have "Neg (atm_of L) \<in># DA0 \<and> Neg (atm_of L) \<cdot>l \<eta>0 = Neg (As ! 0)"
         by (metis Neg_atm_of_iff literal.sel(2) subst_lit_is_pos)
       then have "[atm_of L] \<cdot>al \<eta>0 = As \<and> negs (mset [atm_of L]) \<subseteq># DA0"
         using as subst_lit_def by auto
       then have "\<exists>As0. As0 \<cdot>al \<eta>0 = As \<and> negs (mset As0) \<subseteq># DA0
         \<and> (S_M S M (D + negs (mset As)) \<noteq> {#} \<longrightarrow> negs (mset As0) = S DA0)"
         using a by blast
     }
     moreover
     {
       assume "S_M S M (D + negs (mset As)) = negs (mset As)"
       then have "negs (mset As) = S DA0 \<cdot> \<eta>0"
         using da \<open>S DA0 \<cdot> \<eta>0 = S_M S M DA\<close> by auto
       then have "\<exists>As0. negs (mset As0) = S DA0 \<and> As0 \<cdot>al \<eta>0 = As"
         using instance_list[of As "S DA0" \<eta>0] S.S_selects_neg_lits by auto
       then have "\<exists>As0. As0 \<cdot>al \<eta>0 = As \<and> negs (mset As0) \<subseteq># DA0
         \<and> (S_M S M (D + negs (mset As)) \<noteq> {#} \<longrightarrow> negs (mset As0) = S DA0)"
         using S.S_selects_subseteq by auto
     }
     ultimately have "\<exists>As0. As0 \<cdot>al \<eta>0 = As \<and> (negs (mset As0)) \<subseteq># DA0
       \<and> (S_M S M (D + negs (mset As)) \<noteq> {#} \<longrightarrow> negs (mset As0) = S DA0)"
       using eligible unfolding eligible.simps by auto
     then obtain As0 where
       As0_p: "As0 \<cdot>al \<eta>0 = As \<and> negs (mset As0) \<subseteq># DA0
       \<and> (S_M S M (D + negs (mset As)) \<noteq> {#} \<longrightarrow> negs (mset As0) = S DA0)"
       by blast
     then have "length As0 = n"
       using as_len by auto
     note n = n this
 
     have "As0 \<cdot>al \<eta>0 = As"
       using As0_p by auto
 
     define D0 where
       "D0 = DA0 - negs (mset As0)"
     then have "DA0 = D0 + negs (mset As0)"
       using As0_p by auto
     then have "D0 \<cdot> \<eta>0 = D"
       using DA0_to_DA da As0_p by auto
 
     have "S_M S M (D + negs (mset As)) \<noteq> {#} \<Longrightarrow> negs (mset As0) = S DA0"
       using As0_p by blast
     then show ?thesis
       using that \<open>As0 \<cdot>al \<eta>0 = As\<close> \<open>D0 \<cdot> \<eta>0= D\<close> \<open>DA0 = D0 +  (negs (mset As0))\<close> \<open>length As0 = n\<close>
       by metis
   qed
 
   show ?thesis
     using that[OF n(2,1) DA0_in_M  DA0_to_DA SDA0_to_SMDA CAs0_in_M CAs0_to_CAs SCAs0_to_SMCAs
         \<open>is_ground_subst \<eta>0\<close> \<open>is_ground_subst_list \<eta>s0\<close> \<open>As0  \<cdot>al \<eta>0 = As\<close>
         \<open>AAs0 \<cdot>\<cdot>aml \<eta>s0 = AAs\<close>
         \<open>length As0 = n\<close>
         \<open>D0 \<cdot> \<eta>0 = D\<close>
         \<open>DA0 = D0 + (negs (mset As0))\<close>
         \<open>S_M S M (D + negs (mset As)) \<noteq> {#} \<Longrightarrow> negs (mset As0) = S DA0\<close>
         \<open>length Cs0 = n\<close>
         \<open>Cs0 \<cdot>\<cdot>cl \<eta>s0 = Cs\<close>
         \<open>\<forall>i < n. CAs0 ! i = Cs0 ! i + poss (AAs0 ! i)\<close>
         \<open>length AAs0 = n\<close>]
     by auto
 qed
 
 lemma ord_resolve_rename_lifting:
   assumes
     sel_stable: "\<And>\<rho> C. is_renaming \<rho> \<Longrightarrow> S (C \<cdot> \<rho>) = S C \<cdot> \<rho>" and
     res_e: "ord_resolve (S_M S M) CAs DA AAs As \<sigma> E" and
     select: "selection S" and
     grounding: "{DA} \<union> set CAs \<subseteq> grounding_of_clss M"
   obtains \<eta>s \<eta> \<eta>2 CAs0 DA0 AAs0 As0 E0 \<tau> where
     "is_ground_subst \<eta>"
     "is_ground_subst_list \<eta>s"
     "is_ground_subst \<eta>2"
     "ord_resolve_rename S CAs0 DA0 AAs0 As0 \<tau> E0"
     "CAs0 \<cdot>\<cdot>cl \<eta>s = CAs" "DA0 \<cdot> \<eta> = DA" "E0 \<cdot> \<eta>2 = E"
     "{DA0} \<union> set CAs0 \<subseteq> M"
     "length CAs0 = length CAs"
     "length \<eta>s = length CAs"
   using res_e
 proof (cases rule: ord_resolve.cases)
   case (ord_resolve n Cs D)
   note da = this(1) and e = this(2) and cas_len = this(3) and cs_len = this(4) and
     aas_len = this(5) and as_len = this(6) and nz = this(7) and cas = this(8) and
     aas_not_empt = this(9) and mgu = this(10) and eligible = this(11) and str_max = this(12) and
     sel_empt = this(13)
 
   have sel_ren_list_inv:
     "\<And>\<rho>s Cs. length \<rho>s = length Cs \<Longrightarrow> is_renaming_list \<rho>s \<Longrightarrow> map S (Cs \<cdot>\<cdot>cl \<rho>s) = map S Cs \<cdot>\<cdot>cl \<rho>s"
     using sel_stable unfolding is_renaming_list_def by (auto intro: nth_equalityI)
 
   note n = \<open>n \<noteq> 0\<close> \<open>length CAs = n\<close> \<open>length Cs = n\<close> \<open>length AAs = n\<close> \<open>length As = n\<close>
 
   interpret S: selection S by (rule select)
 
   obtain DA0 \<eta>0 CAs0 \<eta>s0 As0 AAs0 D0 Cs0 where as0:
     "length CAs0 = n"
     "length \<eta>s0 = n"
     "DA0 \<in> M"
     "DA0 \<cdot> \<eta>0 = DA"
     "S DA0 \<cdot> \<eta>0 = S_M S M DA"
     "\<forall>CA0 \<in> set CAs0. CA0 \<in> M"
     "CAs0 \<cdot>\<cdot>cl \<eta>s0 = CAs"
     "map S CAs0 \<cdot>\<cdot>cl \<eta>s0 = map (S_M S M) CAs"
     "is_ground_subst \<eta>0"
     "is_ground_subst_list \<eta>s0"
     "As0 \<cdot>al \<eta>0 = As"
     "AAs0 \<cdot>\<cdot>aml \<eta>s0 = AAs"
     "length As0 = n"
     "D0 \<cdot> \<eta>0 = D"
     "DA0 = D0 + (negs (mset As0))"
     "S_M S M (D + negs (mset As)) \<noteq> {#} \<Longrightarrow> negs (mset As0) = S DA0"
     "length Cs0 = n"
     "Cs0 \<cdot>\<cdot>cl \<eta>s0 = Cs"
     "\<forall>i < n. CAs0 ! i = Cs0 ! i + poss (AAs0 ! i)"
     "length AAs0 = n"
     using ord_resolve_obtain_clauses[of S M CAs DA, OF res_e select grounding n(2) \<open>DA = D + negs (mset As)\<close>
       \<open>\<forall>i<n. CAs ! i = Cs ! i + poss (AAs ! i)\<close> \<open>length Cs = n\<close> \<open>length AAs = n\<close>, of thesis] by blast
 
   note n = \<open>length CAs0 = n\<close> \<open>length \<eta>s0 = n\<close> \<open>length As0 = n\<close> \<open>length AAs0 = n\<close> \<open>length Cs0 = n\<close> n
 
   have "length (renamings_apart (DA0 # CAs0)) = Suc n"
     using n renamings_apart_length by auto
 
   note n = this n
 
   define \<rho> where
     "\<rho> = hd (renamings_apart (DA0 # CAs0))"
   define \<rho>s where
     "\<rho>s = tl (renamings_apart (DA0 # CAs0))"
   define DA0' where
     "DA0' = DA0 \<cdot> \<rho>"
   define D0' where
     "D0' = D0 \<cdot> \<rho>"
   define As0' where
     "As0' = As0 \<cdot>al \<rho>"
   define CAs0' where
     "CAs0' = CAs0 \<cdot>\<cdot>cl \<rho>s"
   define Cs0' where
     "Cs0' = Cs0 \<cdot>\<cdot>cl \<rho>s"
   define AAs0' where
     "AAs0' = AAs0 \<cdot>\<cdot>aml \<rho>s"
   define \<eta>0' where
     "\<eta>0' = inv_renaming \<rho> \<odot> \<eta>0"
   define \<eta>s0' where
     "\<eta>s0' = map inv_renaming \<rho>s \<odot>s \<eta>s0"
 
   have renames_DA0: "is_renaming \<rho>"
     using renamings_apart_length renamings_apart_renaming unfolding \<rho>_def
     by (metis length_greater_0_conv list.exhaust_sel list.set_intros(1) list.simps(3))
 
   have renames_CAs0: "is_renaming_list \<rho>s"
     using renamings_apart_length renamings_apart_renaming unfolding \<rho>s_def
     by (metis is_renaming_list_def length_greater_0_conv list.set_sel(2) list.simps(3))
 
   have "length \<rho>s = n"
     unfolding \<rho>s_def using n by auto
   note n = n \<open>length \<rho>s = n\<close>
   have "length As0' = n"
     unfolding As0'_def using n by auto
   have "length CAs0' = n"
     using as0(1) n unfolding CAs0'_def by auto
   have "length Cs0' = n"
     unfolding Cs0'_def using n by auto
   have "length AAs0' = n"
     unfolding AAs0'_def using n by auto
   have "length \<eta>s0' = n"
     using as0(2) n unfolding \<eta>s0'_def by auto
   note n = \<open>length CAs0' = n\<close> \<open>length \<eta>s0' = n\<close> \<open>length As0' = n\<close> \<open>length AAs0' = n\<close> \<open>length Cs0' = n\<close> n
 
   have DA0'_DA: "DA0' \<cdot> \<eta>0' = DA"
     using as0(4) unfolding \<eta>0'_def DA0'_def using renames_DA0 by simp
   have D0'_D: "D0' \<cdot> \<eta>0' = D"
     using as0(14) unfolding \<eta>0'_def D0'_def using renames_DA0 by simp
   have As0'_As: "As0' \<cdot>al \<eta>0' = As"
     using as0(11) unfolding \<eta>0'_def As0'_def using renames_DA0 by auto
   have "S DA0' \<cdot> \<eta>0' = S_M S M DA"
     using as0(5) unfolding \<eta>0'_def DA0'_def using renames_DA0 sel_stable by auto
   have CAs0'_CAs: "CAs0' \<cdot>\<cdot>cl \<eta>s0' = CAs"
     using as0(7) unfolding CAs0'_def \<eta>s0'_def using renames_CAs0 n by auto
   have Cs0'_Cs: "Cs0' \<cdot>\<cdot>cl \<eta>s0' = Cs"
     using as0(18) unfolding Cs0'_def \<eta>s0'_def using renames_CAs0 n by auto
   have AAs0'_AAs: "AAs0' \<cdot>\<cdot>aml \<eta>s0' = AAs"
     using as0(12) unfolding \<eta>s0'_def AAs0'_def using renames_CAs0 using n by auto
   have "map S CAs0' \<cdot>\<cdot>cl \<eta>s0' = map (S_M S M) CAs"
     unfolding CAs0'_def \<eta>s0'_def using as0(8) n renames_CAs0 sel_ren_list_inv by auto
 
   have DA0'_split: "DA0' = D0' + negs (mset As0')"
     using as0(15) DA0'_def D0'_def As0'_def by auto
   then have D0'_subset_DA0': "D0' \<subseteq># DA0'"
     by auto
   from DA0'_split have negs_As0'_subset_DA0': "negs (mset As0') \<subseteq># DA0'"
     by auto
 
   have CAs0'_split: "\<forall>i<n. CAs0' ! i = Cs0' ! i + poss (AAs0' ! i)"
     using as0(19) CAs0'_def Cs0'_def AAs0'_def n by auto
   then have "\<forall>i<n. Cs0' ! i \<subseteq># CAs0' ! i"
     by auto
   from CAs0'_split have poss_AAs0'_subset_CAs0': "\<forall>i<n. poss (AAs0' ! i) \<subseteq># CAs0' ! i"
     by auto
   then have AAs0'_in_atms_of_CAs0': "\<forall>i < n. \<forall>A\<in>#AAs0' ! i. A \<in> atms_of (CAs0' ! i)"
     by (auto simp add: atm_iff_pos_or_neg_lit)
 
   have as0':
     "S_M S M (D + negs (mset As)) \<noteq> {#} \<Longrightarrow> negs (mset As0') = S DA0'"
   proof -
     assume a: "S_M S M (D + negs (mset As)) \<noteq> {#}"
     then have "negs (mset As0) \<cdot> \<rho> = S DA0 \<cdot> \<rho>"
       using as0(16) unfolding \<rho>_def by metis
     then show "negs (mset As0') = S DA0'"
       using  As0'_def DA0'_def using sel_stable[of \<rho> DA0] renames_DA0 by auto
   qed
 
   have vd: "var_disjoint (DA0' # CAs0')"
     unfolding DA0'_def CAs0'_def using renamings_apart_var_disjoint
     unfolding \<rho>_def \<rho>s_def
     by (metis length_greater_0_conv list.exhaust_sel n(6) substitution.subst_cls_lists_Cons
         substitution_axioms zero_less_Suc)
 
   \<comment> \<open>Introduce ground substitution\<close>
   from vd DA0'_DA CAs0'_CAs have "\<exists>\<eta>. \<forall>i < Suc n. \<forall>S. S \<subseteq># (DA0' # CAs0') ! i \<longrightarrow> S \<cdot> (\<eta>0'#\<eta>s0') ! i = S \<cdot> \<eta>"
     unfolding var_disjoint_def using n by auto
   then obtain \<eta> where \<eta>_p: "\<forall>i < Suc n. \<forall>S. S \<subseteq># (DA0' # CAs0') ! i \<longrightarrow> S \<cdot> (\<eta>0'#\<eta>s0') ! i = S \<cdot> \<eta>"
     by auto
   have \<eta>_p_lit: "\<forall>i < Suc n. \<forall>L. L \<in># (DA0' # CAs0') ! i \<longrightarrow> L \<cdot>l (\<eta>0'#\<eta>s0') ! i = L \<cdot>l \<eta>"
   proof (rule, rule, rule, rule)
     fix i :: "nat" and L :: "'a literal"
     assume a:
       "i < Suc n"
       "L \<in># (DA0' # CAs0') ! i"
     then have "\<forall>S. S \<subseteq># (DA0' # CAs0') ! i \<longrightarrow> S \<cdot> (\<eta>0' # \<eta>s0') ! i = S \<cdot> \<eta>"
       using \<eta>_p by auto
     then have "{# L #} \<cdot> (\<eta>0' # \<eta>s0') ! i = {# L #} \<cdot> \<eta>"
       using a by (meson single_subset_iff)
     then show "L \<cdot>l (\<eta>0' # \<eta>s0') ! i = L \<cdot>l \<eta>" by auto
   qed
   have \<eta>_p_atm: "\<forall>i < Suc n. \<forall>A. A \<in> atms_of ((DA0' # CAs0') ! i) \<longrightarrow> A \<cdot>a (\<eta>0'#\<eta>s0') ! i = A \<cdot>a \<eta>"
   proof (rule, rule, rule, rule)
     fix i :: "nat" and A :: "'a"
     assume a:
       "i < Suc n"
       "A \<in> atms_of ((DA0' # CAs0') ! i)"
     then obtain L where L_p: "atm_of L = A \<and> L \<in># (DA0' # CAs0') ! i"
       unfolding atms_of_def by auto
     then have "L \<cdot>l (\<eta>0'#\<eta>s0') ! i = L \<cdot>l \<eta>"
       using \<eta>_p_lit a by auto
     then show "A \<cdot>a (\<eta>0' # \<eta>s0') ! i = A \<cdot>a \<eta>"
       using L_p unfolding subst_lit_def by (cases L) auto
   qed
 
   have DA0'_DA: "DA0' \<cdot> \<eta> = DA"
     using DA0'_DA \<eta>_p by auto
   have "D0' \<cdot> \<eta> = D" using \<eta>_p D0'_D n D0'_subset_DA0' by auto
   have "As0' \<cdot>al \<eta> = As"
   proof (rule nth_equalityI)
     show "length (As0' \<cdot>al \<eta>) = length As"
       using n by auto
   next
     fix i
     show "i<length (As0' \<cdot>al \<eta>) \<Longrightarrow> (As0' \<cdot>al \<eta>) ! i = As ! i"
     proof -
       assume a: "i < length (As0' \<cdot>al \<eta>)"
       have A_eq: "\<forall>A. A \<in> atms_of DA0' \<longrightarrow> A \<cdot>a \<eta>0' = A \<cdot>a \<eta>"
         using \<eta>_p_atm n by force
       have "As0' ! i \<in> atms_of DA0'"
         using negs_As0'_subset_DA0' unfolding atms_of_def
         using a n by force
       then have "As0' ! i \<cdot>a \<eta>0' = As0' ! i \<cdot>a \<eta>"
          using A_eq by simp
       then show "(As0' \<cdot>al \<eta>) ! i = As ! i"
         using As0'_As \<open>length As0' = n\<close> a by auto
     qed
   qed
 
   interpret selection
     by (rule select)
 
   have "S DA0' \<cdot> \<eta> = S_M S M DA"
     using \<open>S DA0' \<cdot> \<eta>0' = S_M S M DA\<close> \<eta>_p S.S_selects_subseteq by auto
 
   from \<eta>_p have \<eta>_p_CAs0': "\<forall>i < n. (CAs0' ! i) \<cdot> (\<eta>s0' ! i) = (CAs0'! i) \<cdot> \<eta>"
     using n by auto
   then have "CAs0' \<cdot>\<cdot>cl \<eta>s0' = CAs0' \<cdot>cl \<eta>"
     using n by (auto intro: nth_equalityI)
   then have CAs0'_\<eta>_fo_CAs: "CAs0' \<cdot>cl \<eta> = CAs"
     using CAs0'_CAs \<eta>_p n by auto
 
   from \<eta>_p have "\<forall>i < n. S (CAs0' ! i) \<cdot> \<eta>s0' ! i = S (CAs0' ! i) \<cdot> \<eta>"
     using S.S_selects_subseteq n by auto
   then have "map S CAs0' \<cdot>\<cdot>cl \<eta>s0' = map S CAs0' \<cdot>cl \<eta>"
     using n by (auto intro: nth_equalityI)
   then have SCAs0'_\<eta>_fo_SMCAs: "map S CAs0' \<cdot>cl \<eta> = map (S_M S M) CAs"
     using \<open>map S CAs0' \<cdot>\<cdot>cl \<eta>s0' = map (S_M S M) CAs\<close> by auto
 
   have "Cs0' \<cdot>cl \<eta> = Cs"
   proof (rule nth_equalityI)
     show "length (Cs0' \<cdot>cl \<eta>) = length Cs"
       using n by auto
   next
     fix i
     show "i<length (Cs0' \<cdot>cl \<eta>) \<Longrightarrow> (Cs0' \<cdot>cl \<eta>) ! i = Cs ! i"
     proof -
       assume "i < length (Cs0' \<cdot>cl \<eta>)"
       then have a: "i < n"
         using n by force
       have "(Cs0' \<cdot>\<cdot>cl \<eta>s0') ! i = Cs ! i"
         using Cs0'_Cs a n by force
       moreover
       have \<eta>_p_CAs0': "\<forall>S. S \<subseteq># CAs0' ! i \<longrightarrow> S \<cdot> \<eta>s0' ! i = S \<cdot> \<eta>"
         using \<eta>_p a by force
       have "Cs0' ! i \<cdot> \<eta>s0' ! i = (Cs0' \<cdot>cl \<eta>) ! i"
         using \<eta>_p_CAs0' \<open>\<forall>i<n. Cs0' ! i \<subseteq># CAs0' ! i\<close> a n by force
       then have "(Cs0' \<cdot>\<cdot>cl \<eta>s0') ! i = (Cs0' \<cdot>cl \<eta>) ! i "
         using a n by force
       ultimately show "(Cs0' \<cdot>cl \<eta>) ! i = Cs ! i"
         by auto
     qed
   qed
 
   have AAs0'_AAs: "AAs0' \<cdot>aml \<eta> = AAs"
   proof (rule nth_equalityI)
     show "length (AAs0' \<cdot>aml \<eta>) = length AAs"
       using n by auto
   next
     fix i
     show "i<length (AAs0' \<cdot>aml \<eta>) \<Longrightarrow> (AAs0' \<cdot>aml \<eta>) ! i = AAs ! i"
     proof -
       assume a: "i < length (AAs0' \<cdot>aml \<eta>)"
       then have "i < n"
         using n by force
       then have "\<forall>A. A \<in> atms_of ((DA0' # CAs0') ! Suc i) \<longrightarrow> A \<cdot>a (\<eta>0' # \<eta>s0') ! Suc i = A \<cdot>a \<eta>"
         using \<eta>_p_atm n by force
       then have A_eq: "\<forall>A. A \<in> atms_of (CAs0' ! i) \<longrightarrow> A \<cdot>a \<eta>s0' ! i = A \<cdot>a \<eta>"
         by auto
       have AAs_CAs0': "\<forall>A \<in># AAs0' ! i. A \<in> atms_of (CAs0' ! i)"
         using AAs0'_in_atms_of_CAs0' unfolding atms_of_def
         using a n by force
       then have "AAs0' ! i \<cdot>am  \<eta>s0' ! i = AAs0' ! i \<cdot>am \<eta>"
         unfolding subst_atm_mset_def using A_eq unfolding subst_atm_mset_def by auto
       then show "(AAs0' \<cdot>aml \<eta>) ! i = AAs ! i"
          using AAs0'_AAs \<open>length AAs0' = n\<close> \<open>length \<eta>s0' = n\<close> a by auto
     qed
   qed
 
   \<comment> \<open>Obtain MGU and substitution\<close>
   obtain \<tau> \<phi> where \<tau>\<phi>:
     "Some \<tau> = mgu (set_mset ` set (map2 add_mset As0' AAs0'))"
     "\<tau> \<odot> \<phi> = \<eta> \<odot> \<sigma>"
   proof -
     have uu: "is_unifiers \<sigma> (set_mset ` set (map2 add_mset (As0' \<cdot>al \<eta>) (AAs0' \<cdot>aml \<eta>)))"
       using mgu mgu_sound is_mgu_def unfolding \<open>AAs0' \<cdot>aml \<eta> = AAs\<close> using \<open>As0' \<cdot>al \<eta> = As\<close> by auto
     have \<eta>\<sigma>uni: "is_unifiers (\<eta> \<odot> \<sigma>) (set_mset ` set (map2 add_mset As0' AAs0'))"
     proof -
       have "set_mset ` set (map2 add_mset As0' AAs0' \<cdot>aml \<eta>) =
         set_mset ` set (map2 add_mset As0' AAs0') \<cdot>ass \<eta>"
         unfolding subst_atmss_def subst_atm_mset_list_def using subst_atm_mset_def subst_atms_def
         by (simp add: image_image subst_atm_mset_def subst_atms_def)
       then have "is_unifiers \<sigma> (set_mset ` set (map2 add_mset As0' AAs0') \<cdot>ass \<eta>)"
         using uu by (auto simp: n map2_add_mset_map)
       then show ?thesis
         using is_unifiers_comp by auto
     qed
     then obtain \<tau> where
       \<tau>_p: "Some \<tau> = mgu (set_mset ` set (map2 add_mset As0' AAs0'))"
       using mgu_complete
       by (metis (mono_tags, opaque_lifting) List.finite_set finite_imageI finite_set_mset image_iff)
     moreover then obtain \<phi> where \<phi>_p: "\<tau> \<odot> \<phi> = \<eta> \<odot> \<sigma>"
       by (metis (mono_tags, opaque_lifting) finite_set \<eta>\<sigma>uni finite_imageI finite_set_mset image_iff
           mgu_sound set_mset_mset substitution_ops.is_mgu_def) (* should be simpler *)
     ultimately show thesis
       using that by auto
   qed
 
   \<comment> \<open>Lifting eligibility\<close>
   have eligible0': "eligible S \<tau> As0' (D0' + negs (mset As0'))"
   proof -
     have "S_M S M (D + negs (mset As)) = negs (mset As) \<or> S_M S M (D + negs (mset As)) = {#} \<and>
       length As = 1 \<and> maximal_wrt (As ! 0 \<cdot>a \<sigma>) ((D + negs (mset As)) \<cdot> \<sigma>)"
       using eligible unfolding eligible.simps by auto
     then show ?thesis
     proof
       assume "S_M S M (D + negs (mset As)) = negs (mset As)"
       then have "S_M S M (D + negs (mset As)) \<noteq> {#}"
         using n by force
       then have "S (D0' + negs (mset As0')) = negs (mset As0')"
         using as0' DA0'_split by auto
       then show ?thesis
         unfolding eligible.simps[simplified]  by auto
     next
       assume asm: "S_M S M (D + negs (mset As)) = {#} \<and> length As = 1 \<and>
         maximal_wrt (As ! 0 \<cdot>a \<sigma>) ((D + negs (mset As)) \<cdot> \<sigma>)"
       then have "S (D0' + negs (mset As0')) = {#}"
         using \<open>D0' \<cdot> \<eta> = D\<close>[symmetric] \<open>As0' \<cdot>al \<eta> = As\<close>[symmetric] \<open>S (DA0') \<cdot> \<eta> = S_M S M (DA)\<close>
           da DA0'_split subst_cls_empty_iff by metis
       moreover from asm have l: "length As0' = 1"
         using \<open>As0' \<cdot>al \<eta> = As\<close> by auto
       moreover from asm have "maximal_wrt (As0' ! 0 \<cdot>a (\<tau> \<odot> \<phi>)) ((D0' + negs (mset As0')) \<cdot> (\<tau> \<odot> \<phi>))"
         using \<open>As0' \<cdot>al \<eta> = As\<close> \<open>D0' \<cdot> \<eta> = D\<close> using l \<tau>\<phi> by auto
       then have "maximal_wrt (As0' ! 0 \<cdot>a \<tau> \<cdot>a \<phi>) ((D0' + negs (mset As0')) \<cdot> \<tau> \<cdot> \<phi>)"
         by auto
       then have "maximal_wrt (As0' ! 0 \<cdot>a \<tau>) ((D0' + negs (mset As0')) \<cdot> \<tau>)"
         using maximal_wrt_subst by blast
       ultimately show ?thesis
         unfolding eligible.simps[simplified] by auto
     qed
   qed
 
   \<comment> \<open>Lifting maximality\<close>
   have maximality: "\<forall>i < n. strictly_maximal_wrt (As0' ! i \<cdot>a \<tau>) (Cs0' ! i \<cdot> \<tau>)"
     (* Reformulate in list notation? *)
   proof -
     from str_max have "\<forall>i < n. strictly_maximal_wrt ((As0' \<cdot>al \<eta>) ! i \<cdot>a \<sigma>) ((Cs0' \<cdot>cl \<eta>) ! i \<cdot> \<sigma>)"
       using \<open>As0' \<cdot>al \<eta> = As\<close>  \<open>Cs0' \<cdot>cl \<eta> = Cs\<close> by simp
     then have "\<forall>i < n. strictly_maximal_wrt (As0' ! i \<cdot>a (\<tau> \<odot> \<phi>)) (Cs0' ! i \<cdot> (\<tau> \<odot> \<phi>))"
       using n \<tau>\<phi> by simp
     then have "\<forall>i < n. strictly_maximal_wrt (As0' ! i \<cdot>a \<tau> \<cdot>a \<phi>) (Cs0' ! i \<cdot> \<tau> \<cdot> \<phi>)"
       by auto
     then show "\<forall>i < n. strictly_maximal_wrt (As0' ! i \<cdot>a \<tau>) (Cs0' ! i \<cdot> \<tau>)"
       using strictly_maximal_wrt_subst \<tau>\<phi> by blast
   qed
 
   \<comment> \<open>Lifting nothing being selected\<close>
   have nothing_selected: "\<forall>i < n. S (CAs0' ! i) = {#}"
   proof -
     have "\<forall>i < n. (map S CAs0' \<cdot>cl \<eta>) ! i = map (S_M S M) CAs ! i"
       by (simp add: \<open>map S CAs0' \<cdot>cl \<eta> = map (S_M S M) CAs\<close>)
     then have "\<forall>i < n. S (CAs0' ! i) \<cdot> \<eta> = S_M S M (CAs ! i)"
       using n by auto
     then have "\<forall>i < n. S (CAs0' ! i)  \<cdot> \<eta> = {#}"
       using sel_empt \<open>\<forall>i < n.  S (CAs0' ! i) \<cdot> \<eta> = S_M S M (CAs ! i)\<close> by auto
     then show "\<forall>i < n. S (CAs0' ! i) = {#}"
       using subst_cls_empty_iff by blast
   qed
 
   \<comment> \<open>Lifting AAs0's non-emptiness\<close>
   have "\<forall>i < n. AAs0' ! i \<noteq> {#}"
     using n aas_not_empt \<open>AAs0' \<cdot>aml \<eta> = AAs\<close> by auto
 
   \<comment> \<open>Resolve the lifted clauses\<close>
   define E0' where
     "E0' = ((\<Sum>\<^sub># (mset Cs0')) + D0') \<cdot> \<tau>"
 
   have res_e0': "ord_resolve S CAs0' DA0' AAs0' As0' \<tau> E0'"
     using ord_resolve.intros[of CAs0' n Cs0' AAs0' As0' \<tau> S D0',
       OF _ _ _ _ _ _ \<open>\<forall>i < n. AAs0' ! i \<noteq> {#}\<close> \<tau>\<phi>(1) eligible0'
         \<open>\<forall>i < n. strictly_maximal_wrt (As0' ! i \<cdot>a \<tau>) (Cs0' ! i \<cdot> \<tau>)\<close> \<open>\<forall>i < n. S (CAs0' ! i) = {#}\<close>]
     unfolding E0'_def using DA0'_split n \<open>\<forall>i<n. CAs0' ! i = Cs0' ! i + poss (AAs0' ! i)\<close> by blast
 
   \<comment> \<open>Prove resolvent instantiates to ground resolvent\<close>
   have e0'\<phi>e: "E0' \<cdot> \<phi> = E"
   proof -
     have "E0' \<cdot> \<phi> = ((\<Sum>\<^sub># (mset Cs0')) + D0') \<cdot> (\<tau> \<odot> \<phi>)"
       unfolding E0'_def by auto
     also have "\<dots> = (\<Sum>\<^sub># (mset Cs0') + D0') \<cdot> (\<eta> \<odot> \<sigma>)"
       using \<tau>\<phi> by auto
     also have "\<dots> = (\<Sum>\<^sub># (mset Cs) + D) \<cdot> \<sigma>"
       using \<open>Cs0' \<cdot>cl \<eta> = Cs\<close> \<open>D0' \<cdot> \<eta> = D\<close> by auto
     also have "\<dots> = E"
       using e by auto
     finally show e0'\<phi>e: "E0' \<cdot> \<phi> = E"
       .
   qed
 
   \<comment> \<open>Replace @{term \<phi>} with a true ground substitution\<close>
   obtain \<eta>2 where
     ground_\<eta>2: "is_ground_subst \<eta>2" "E0' \<cdot> \<eta>2 = E"
   proof -
     have "is_ground_cls_list CAs" "is_ground_cls DA"
       using grounding grounding_ground unfolding is_ground_cls_list_def by auto
     then have "is_ground_cls E"
       using res_e ground_resolvent_subset by (force intro: is_ground_cls_mono)
     then show thesis
       using that e0'\<phi>e make_ground_subst by auto
   qed
 
   have \<open>length CAs0 = length CAs\<close>
     using n by simp
 
   have \<open>length \<eta>s0 = length CAs\<close>
     using n by simp
 
   \<comment> \<open>Wrap up the proof\<close>
   have "ord_resolve S (CAs0 \<cdot>\<cdot>cl \<rho>s) (DA0 \<cdot> \<rho>) (AAs0 \<cdot>\<cdot>aml \<rho>s) (As0 \<cdot>al \<rho>) \<tau> E0'"
     using res_e0' As0'_def \<rho>_def AAs0'_def \<rho>s_def DA0'_def \<rho>_def CAs0'_def \<rho>s_def by simp
   moreover have "\<forall>i<n. poss (AAs0 ! i) \<subseteq># CAs0 ! i"
     using as0(19) by auto
   moreover have "negs (mset As0) \<subseteq># DA0"
     using local.as0(15) by auto
   ultimately have "ord_resolve_rename S CAs0 DA0 AAs0 As0 \<tau> E0'"
     using ord_resolve_rename[of CAs0 n AAs0 As0 DA0 \<rho> \<rho>s S \<tau> E0'] \<rho>_def \<rho>s_def n by auto
   then show thesis
     using that[of \<eta>0 \<eta>s0 \<eta>2 CAs0 DA0] \<open>is_ground_subst \<eta>0\<close> \<open>is_ground_subst_list \<eta>s0\<close>
       \<open>is_ground_subst \<eta>2\<close> \<open>CAs0 \<cdot>\<cdot>cl \<eta>s0 = CAs\<close> \<open>DA0 \<cdot> \<eta>0 = DA\<close> \<open>E0' \<cdot> \<eta>2 = E\<close> \<open>DA0 \<in> M\<close>
       \<open>\<forall>CA \<in> set CAs0. CA \<in> M\<close> \<open>length CAs0 = length CAs\<close> \<open>length \<eta>s0 = length CAs\<close>
     by blast
 qed
 
 lemma ground_ord_resolve_ground:
   assumes
     select: "selection S" and
     CAs_p: "ground_resolution_with_selection.ord_resolve S CAs DA AAs As E" and
     ground_cas: "is_ground_cls_list CAs" and
     ground_da: "is_ground_cls DA"
   shows "is_ground_cls E"
 proof -
   have a1: "atms_of E \<subseteq> (\<Union>CA \<in> set CAs. atms_of CA) \<union> atms_of DA"
     using ground_resolution_with_selection.ord_resolve_atms_of_concl_subset[OF _ CAs_p]
       ground_resolution_with_selection.intro[OF select] by blast
   {
     fix L :: "'a literal"
     assume "L \<in># E"
     then have "atm_of L \<in> atms_of E"
       by (meson atm_of_lit_in_atms_of)
     then have "is_ground_atm (atm_of L)"
       using a1 ground_cas ground_da is_ground_cls_imp_is_ground_atm is_ground_cls_list_def
       by auto
   }
   then show ?thesis
     unfolding is_ground_cls_def is_ground_lit_def by simp
 qed
 
 lemma ground_ord_resolve_imp_ord_resolve:
   assumes
     ground_da: \<open>is_ground_cls DA\<close> and
     ground_cas: \<open>is_ground_cls_list CAs\<close> and
     gr: "ground_resolution_with_selection S_G" and
     gr_res: \<open>ground_resolution_with_selection.ord_resolve S_G CAs DA AAs As E\<close>
   shows \<open>\<exists>\<sigma>. ord_resolve S_G CAs DA AAs As \<sigma> E\<close>
 proof (cases rule: ground_resolution_with_selection.ord_resolve.cases[OF gr gr_res])
   case (1 CAs n Cs AAs As D)
   note cas = this(1) and da = this(2) and aas = this(3) and as = this(4) and e = this(5) and
     cas_len = this(6) and cs_len = this(7) and aas_len = this(8) and as_len = this(9) and
     nz = this(10) and casi = this(11) and aas_not_empt = this(12) and as_aas = this(13) and
     eligibility = this(14) and str_max = this(15) and sel_empt = this(16)
 
   have len_aas_len_as: "length AAs = length As"
     using aas_len as_len by auto
 
   from as_aas have "\<forall>i < n. \<forall>A \<in># add_mset (As ! i) (AAs ! i). A = As ! i"
     by simp
   then have "\<forall>i < n. card (set_mset (add_mset (As ! i) (AAs ! i))) \<le> Suc 0"
     using all_the_same by metis
   then have "\<forall>i < length AAs. card (set_mset (add_mset (As ! i) (AAs ! i))) \<le> Suc 0"
     using aas_len by auto
   then have "\<forall>AA \<in> set (map2 add_mset As AAs). card (set_mset AA) \<le> Suc 0"
     using set_map2_ex[of AAs As add_mset, OF len_aas_len_as] by auto
   then have "is_unifiers id_subst (set_mset ` set (map2 add_mset As AAs))"
     unfolding is_unifiers_def is_unifier_def by auto
   moreover have "finite (set_mset ` set (map2 add_mset As AAs))"
     by auto
   moreover have "\<forall>AA \<in> set_mset ` set (map2 add_mset As AAs). finite AA"
     by auto
   ultimately obtain \<sigma> where
     \<sigma>_p: "Some \<sigma> = mgu (set_mset ` set (map2 add_mset As AAs))"
     using mgu_complete by metis
 
   have ground_elig: "ground_resolution_with_selection.eligible S_G As (D + negs (mset As))"
     using eligibility by simp
   have ground_cs: "\<forall>i < n. is_ground_cls (Cs ! i)"
     using cas cas_len cs_len casi ground_cas nth_mem unfolding is_ground_cls_list_def by force
   have ground_set_as: "is_ground_atms (set As)"
     using da ground_da by (metis atms_of_negs is_ground_cls_is_ground_atms_atms_of
         is_ground_cls_union set_mset_mset)
   then have ground_mset_as: "is_ground_atm_mset (mset As)"
     unfolding is_ground_atm_mset_def is_ground_atms_def by auto
   have ground_as: "is_ground_atm_list As"
     using ground_set_as is_ground_atm_list_def is_ground_atms_def by auto
   have ground_d: "is_ground_cls D"
     using ground_da da by simp
 
   from as_len nz have atms:
     "atms_of D \<union> set As \<noteq> {}"
     "finite (atms_of D \<union> set As)"
     by auto
   then have "Max (atms_of D \<union> set As) \<in> atms_of D \<union> set As"
     using Max_in by metis
   then have is_ground_Max: "is_ground_atm (Max (atms_of D \<union> set As))"
     using ground_d ground_mset_as is_ground_cls_imp_is_ground_atm
     unfolding is_ground_atm_mset_def by auto
 
   have "maximal_wrt (Max (atms_of D \<union> set As)) (D + negs (mset As))"
     unfolding maximal_wrt_def
     by clarsimp (metis atms Max_less_iff UnCI ground_d ground_set_as infinite_growing
         is_ground_Max is_ground_atms_def is_ground_cls_imp_is_ground_atm less_atm_ground)
   moreover have
     "Max (atms_of D \<union> set As) \<cdot>a \<sigma> = Max (atms_of D \<union> set As)" and
     "D \<cdot> \<sigma> + negs (mset As \<cdot>am \<sigma>) = D + negs (mset As)"
     using ground_elig is_ground_Max ground_mset_as ground_d by auto
   ultimately have fo_elig: "eligible S_G \<sigma> As (D + negs (mset As))"
     using ground_elig unfolding ground_resolution_with_selection.eligible.simps[OF gr]
       ground_resolution_with_selection.maximal_wrt_def[OF gr] eligible.simps
     by auto
 
   have "\<forall>i < n. strictly_maximal_wrt (As ! i) (Cs ! i)"
     using str_max[unfolded ground_resolution_with_selection.strictly_maximal_wrt_def[OF gr]]
       ground_as[unfolded is_ground_atm_list_def] ground_cs as_len less_atm_ground
     unfolding strictly_maximal_wrt_def by clarsimp (fastforce simp: is_ground_cls_as_atms)+
   then have ll: "\<forall>i < n. strictly_maximal_wrt (As ! i \<cdot>a \<sigma>) (Cs ! i \<cdot> \<sigma>)"
     by (simp add: ground_as ground_cs as_len)
 
   have ground_e: "is_ground_cls E"
     using ground_d ground_cs cs_len unfolding e is_ground_cls_def
     by simp (metis in_mset_sum_list2 in_set_conv_nth)
 
   show ?thesis
     using cas da aas as e ground_e ord_resolve.intros[OF cas_len cs_len aas_len as_len nz casi
         aas_not_empt \<sigma>_p fo_elig ll sel_empt]
     by auto
 qed
 
 end
 
 end