diff --git a/thys/Nested_Multisets_Ordinals/Multiset_More.thy b/thys/Nested_Multisets_Ordinals/Multiset_More.thy
--- a/thys/Nested_Multisets_Ordinals/Multiset_More.thy
+++ b/thys/Nested_Multisets_Ordinals/Multiset_More.thy
@@ -1,1032 +1,1032 @@
 (*  Title:       More about Multisets
     Author:      Mathias Fleury <mathias.fleury at mpi-inf.mpg.de>, 2015
     Author:      Jasmin Blanchette <blanchette at in.tum.de>, 2014, 2015
     Author:      Anders Schlichtkrull <andschl at dtu.dk>, 2017
     Author:      Dmitriy Traytel <traytel at in.tum.de>, 2014
     Maintainer:  Mathias Fleury <mathias.fleury at mpi-inf.mpg.de>
 *)
 
 section \<open>More about Multisets\<close>
 
 theory Multiset_More
   imports
     "HOL-Library.Multiset_Order"
     "HOL-Library.Sublist"
 begin
 
 text \<open>
 Isabelle's theory of finite multisets is not as developed as other areas, such as lists and sets.
 The present theory introduces some missing concepts and lemmas. Some of it is expected to move to
 Isabelle's library.
 \<close>
 
 
 subsection \<open>Basic Setup\<close>
 
 declare
   diff_single_trivial [simp]
   in_image_mset [iff]
   image_mset.compositionality [simp]
 
   (*To have the same rules as the set counter-part*)
   mset_subset_eqD[dest, intro?] (*@{thm subsetD}*)
 
   Multiset.in_multiset_in_set[simp]
   inter_add_left1[simp]
   inter_add_left2[simp]
   inter_add_right1[simp]
   inter_add_right2[simp]
 
   sum_mset_sum_list[simp]
 
 
 subsection \<open>Lemmas about Intersection, Union and Pointwise Inclusion\<close>
 
 lemma subset_mset_imp_subset_add_mset: "A \<subseteq># B \<Longrightarrow> A \<subseteq># add_mset x B"
   by (metis add_mset_diff_bothsides diff_subset_eq_self multiset_inter_def subset_mset.inf.absorb2)
 
 lemma subset_add_mset_notin_subset_mset: \<open>A \<subseteq># add_mset b B \<Longrightarrow> b \<notin># A \<Longrightarrow> A \<subseteq># B\<close>
   by (simp add: subset_mset.le_iff_sup)
 
 lemma subset_msetE: "\<lbrakk>A \<subset># B; \<lbrakk>A \<subseteq># B; \<not> B \<subseteq># A\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
   by (simp add: subset_mset.less_le_not_le)
 
 lemma Diff_triv_mset: "M \<inter># N = {#} \<Longrightarrow> M - N = M"
   by (metis diff_intersect_left_idem diff_zero)
 
 lemma diff_intersect_sym_diff: "(A - B) \<inter># (B - A) = {#}"
   unfolding multiset_inter_def
 proof -
   have "A - (B - (B - A)) = A - B"
     by (metis diff_intersect_right_idem multiset_inter_def)
   then show "A - B - (A - B - (B - A)) = {#}"
     by (metis diff_add diff_cancel diff_subset_eq_self subset_mset.diff_add)
 qed
 
 declare subset_msetE [elim!]
 
 lemma subseq_mset_subseteq_mset: "subseq xs ys \<Longrightarrow> mset xs \<subseteq># mset ys"
 proof (induct xs arbitrary: ys)
   case (Cons x xs)
   note Outer_Cons = this
   then show ?case
   proof (induct ys)
     case (Cons y ys)
     have "subseq xs ys"
       by (metis Cons.prems(2) subseq_Cons' subseq_Cons2_iff)
     then show ?case
       using Cons by (metis mset.simps(2) mset_subset_eq_add_mset_cancel subseq_Cons2_iff
           subset_mset_imp_subset_add_mset)
   qed simp
 qed simp
 
 
 subsection \<open>Lemmas about Filter and Image\<close>
 
 lemma count_image_mset_ge_count: "count (image_mset f A) (f b) \<ge> count A b"
   by (induction A) auto
 
 lemma count_image_mset_inj:
   assumes \<open>inj f\<close>
   shows \<open>count (image_mset f M) (f x) = count M x\<close>
   by (induct M) (use assms in \<open>auto simp: inj_on_def\<close>)
 
 lemma count_image_mset_le_count_inj_on:
   "inj_on f (set_mset M) \<Longrightarrow> count (image_mset f M) y \<le> count M (inv_into (set_mset M) f y)"
 proof (induct M)
   case (add x M)
   note ih = this(1) and inj_xM = this(2)
 
   have inj_M: "inj_on f (set_mset M)"
     using inj_xM by simp
 
   show ?case
   proof (cases "x \<in># M")
     case x_in_M: True
     show ?thesis
     proof (cases "y = f x")
       case y_eq_fx: True
       show ?thesis
         using x_in_M ih[OF inj_M] unfolding y_eq_fx by (simp add: inj_M insert_absorb)
     next
       case y_ne_fx: False
       show ?thesis
         using x_in_M ih[OF inj_M] y_ne_fx insert_absorb by fastforce
     qed
   next
     case x_ni_M: False
     show ?thesis
     proof (cases "y = f x")
       case y_eq_fx: True
       have "f x \<notin># image_mset f M"
         using x_ni_M inj_xM by force
       thus ?thesis
         unfolding y_eq_fx
         by (metis (no_types) inj_xM count_add_mset count_greater_eq_Suc_zero_iff count_inI
           image_mset_add_mset inv_into_f_f union_single_eq_member)
     next
       case y_ne_fx: False
       show ?thesis
       proof (rule ccontr)
         assume neg_conj: "\<not> count (image_mset f (add_mset x M)) y
           \<le> count (add_mset x M) (inv_into (set_mset (add_mset x M)) f y)"
 
         have cnt_y: "count (add_mset (f x) (image_mset f M)) y = count (image_mset f M) y"
           using y_ne_fx by simp
 
         have "inv_into (set_mset M) f y \<in># add_mset x M \<Longrightarrow>
           inv_into (set_mset (add_mset x M)) f (f (inv_into (set_mset M) f y)) =
           inv_into (set_mset M) f y"
           by (meson inj_xM inv_into_f_f)
         hence "0 < count (image_mset f (add_mset x M)) y \<Longrightarrow>
           count M (inv_into (set_mset M) f y) = 0 \<or> x = inv_into (set_mset M) f y"
           using neg_conj cnt_y ih[OF inj_M]
           by (metis (no_types) count_add_mset count_greater_zero_iff count_inI f_inv_into_f
             image_mset_add_mset set_image_mset)
         thus False
           using neg_conj cnt_y x_ni_M ih[OF inj_M]
           by (metis (no_types) count_greater_zero_iff count_inI eq_iff image_mset_add_mset
             less_imp_le)
       qed
     qed
   qed
 qed simp
 
 lemma mset_filter_compl: "mset (filter p xs) + mset (filter (Not \<circ> p) xs) = mset xs"
   by (induction xs) (auto simp: ac_simps)
 
 text \<open>Near duplicate of @{thm [source] filter_eq_replicate_mset}: @{thm filter_eq_replicate_mset}.\<close>
 
 lemma filter_mset_eq: "filter_mset ((=) L) A = replicate_mset (count A L) L"
   by (auto simp: multiset_eq_iff)
 
 lemma filter_mset_cong[fundef_cong]:
   assumes "M = M'" "\<And>a. a \<in># M \<Longrightarrow> P a = Q a"
   shows "filter_mset P M = filter_mset Q M"
 proof -
   have "M - filter_mset Q M = filter_mset (\<lambda>a. \<not>Q a) M"
     by (metis multiset_partition add_diff_cancel_left')
   then show ?thesis
     by (auto simp: filter_mset_eq_conv assms)
 qed
 
 lemma image_mset_filter_swap: "image_mset f {# x \<in># M. P (f x)#} = {# x \<in># image_mset f M. P x#}"
   by (induction M) auto
 
 lemma image_mset_cong2:
   "(\<And>x. x \<in># M \<Longrightarrow> f x = g x) \<Longrightarrow> M = N \<Longrightarrow> image_mset f M = image_mset g N"
   by (hypsubst, rule image_mset_cong)
 
 lemma filter_mset_empty_conv: \<open>(filter_mset P M = {#}) = (\<forall>L\<in>#M. \<not> P L)\<close>
   by (induction M) auto
 
 lemma multiset_filter_mono2: \<open>filter_mset P A \<subseteq># filter_mset Q A \<longleftrightarrow> (\<forall>a\<in>#A. P a \<longrightarrow> Q a)\<close>
   by (induction A) (auto intro: subset_mset.order.trans)
 
 lemma image_filter_cong:
   assumes \<open>\<And>C. C \<in># M \<Longrightarrow> P C \<Longrightarrow> f C = g C\<close>
   shows \<open>{#f C. C \<in># {#C \<in># M. P C#}#} = {#g C | C\<in># M. P C#}\<close>
   using assms by (induction M) auto
 
 lemma image_mset_filter_swap2: \<open>{#C \<in># {#P x. x \<in># D#}. Q C #} = {#P x. x \<in># {#C| C \<in># D. Q (P C)#}#}\<close>
   by (simp add: image_mset_filter_swap)
 
 declare image_mset_cong2 [cong]
 
 lemma filter_mset_empty_if_finite_and_filter_set_empty:
   assumes
     "{x \<in> X. P x} = {}" and
     "finite X"
   shows "{#x \<in># mset_set X. P x#} = {#}"
 proof -
   have empty_empty: "\<And>Y. set_mset Y = {} \<Longrightarrow> Y = {#}"
     by auto
   from assms have "set_mset {#x \<in># mset_set X. P x#} = {}"
     by auto
   then show ?thesis
     by (rule empty_empty)
 qed
 
 
 subsection \<open>Lemmas about Sum\<close>
 
 lemma sum_image_mset_sum_map[simp]: "sum_mset (image_mset f (mset xs)) = sum_list (map f xs)"
   by (metis mset_map sum_mset_sum_list)
 
 lemma sum_image_mset_mono:
   fixes f :: "'a \<Rightarrow> 'b::canonically_ordered_monoid_add"
   assumes sub: "A \<subseteq># B"
   shows "(\<Sum>m \<in># A. f m) \<le> (\<Sum>m \<in># B. f m)"
   by (metis image_mset_union le_iff_add sub subset_mset.add_diff_inverse sum_mset.union)
 
 lemma sum_image_mset_mono_mem:
   "n \<in># M \<Longrightarrow> f n \<le> (\<Sum>m \<in># M. f m)" for f :: "'a \<Rightarrow> 'b::canonically_ordered_monoid_add"
   using le_iff_add multi_member_split by fastforce
 
 lemma count_sum_mset_if_1_0: \<open>count M a = (\<Sum>x\<in>#M. if x = a then 1 else 0)\<close>
   by (induction M) auto
 
 lemma sum_mset_dvd:
   fixes k :: "'a::comm_semiring_1_cancel"
   assumes "\<forall>m \<in># M. k dvd f m"
   shows "k dvd (\<Sum>m \<in># M. f m)"
   using assms by (induct M) auto
 
 lemma sum_mset_distrib_div_if_dvd:
   fixes k :: "'a::unique_euclidean_semiring"
   assumes "\<forall>m \<in># M. k dvd f m"
   shows "(\<Sum>m \<in># M. f m) div k = (\<Sum>m \<in># M. f m div k)"
   using assms by (induct M) (auto simp: div_plus_div_distrib_dvd_left)
 
 
 subsection \<open>Lemmas about Remove\<close>
 
 lemma set_mset_minus_replicate_mset[simp]:
   "n \<ge> count A a \<Longrightarrow> set_mset (A - replicate_mset n a) = set_mset A - {a}"
   "n < count A a \<Longrightarrow> set_mset (A - replicate_mset n a) = set_mset A"
   unfolding set_mset_def by (auto split: if_split simp: not_in_iff)
 
 abbreviation removeAll_mset :: "'a \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where
   "removeAll_mset C M \<equiv> M - replicate_mset (count M C) C"
 
 lemma mset_removeAll[simp, code]: "removeAll_mset C (mset L) = mset (removeAll C L)"
   by (induction L) (auto simp: ac_simps multiset_eq_iff split: if_split_asm)
 
 lemma removeAll_mset_filter_mset: "removeAll_mset C M = filter_mset ((\<noteq>) C) M"
   by (induction M) (auto simp: ac_simps multiset_eq_iff)
 
 abbreviation remove1_mset :: "'a \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where
   "remove1_mset C M \<equiv> M - {#C#}"
 
 lemma removeAll_subseteq_remove1_mset: "removeAll_mset x M \<subseteq># remove1_mset x M"
   by (auto simp: subseteq_mset_def)
 
 lemma in_remove1_mset_neq:
   assumes ab: "a \<noteq> b"
   shows "a \<in># remove1_mset b C \<longleftrightarrow> a \<in># C"
   by (metis assms diff_single_trivial in_diffD insert_DiffM insert_noteq_member)
 
 lemma size_mset_removeAll_mset_le_iff: "size (removeAll_mset x M) < size M \<longleftrightarrow> x \<in># M"
   by (auto intro: count_inI mset_subset_size simp: subset_mset_def multiset_eq_iff)
 
 lemma size_remove1_mset_If: \<open>size (remove1_mset x M) = size M - (if x \<in># M then 1 else 0)\<close>
   by (auto simp: size_Diff_subset_Int)
 
 lemma size_mset_remove1_mset_le_iff: "size (remove1_mset x M) < size M \<longleftrightarrow> x \<in># M"
   using less_irrefl
   by (fastforce intro!: mset_subset_size elim: in_countE simp: subset_mset_def multiset_eq_iff)
 
 lemma remove_1_mset_id_iff_notin: "remove1_mset a M = M \<longleftrightarrow> a \<notin># M"
   by (meson diff_single_trivial multi_drop_mem_not_eq)
 
 lemma id_remove_1_mset_iff_notin: "M = remove1_mset a M \<longleftrightarrow> a \<notin># M"
   using remove_1_mset_id_iff_notin by metis
 
 lemma remove1_mset_eqE:
   "remove1_mset L x1 = M \<Longrightarrow>
     (L \<in># x1 \<Longrightarrow> x1 = M + {#L#} \<Longrightarrow> P) \<Longrightarrow>
     (L \<notin># x1 \<Longrightarrow> x1 = M \<Longrightarrow> P) \<Longrightarrow>
   P"
   by (cases "L \<in># x1") auto
 
 lemma image_filter_ne_mset[simp]:
   "image_mset f {#x \<in># M. f x \<noteq> y#} = removeAll_mset y (image_mset f M)"
   by (induction M) simp_all
 
 lemma image_mset_remove1_mset_if:
   "image_mset f (remove1_mset a M) =
    (if a \<in># M then remove1_mset (f a) (image_mset f M) else image_mset f M)"
   by (auto simp: image_mset_Diff)
 
 lemma filter_mset_neq: "{#x \<in># M. x \<noteq> y#} = removeAll_mset y M"
   by (metis add_diff_cancel_left' filter_eq_replicate_mset multiset_partition)
 
 lemma filter_mset_neq_cond: "{#x \<in># M. P x \<and> x \<noteq> y#} = removeAll_mset y {# x\<in>#M. P x#}"
   by (metis filter_filter_mset filter_mset_neq)
 
 lemma remove1_mset_add_mset_If:
   "remove1_mset L (add_mset L' C) = (if L = L' then C else remove1_mset L C + {#L'#})"
   by (auto simp: multiset_eq_iff)
 
 lemma minus_remove1_mset_if:
   "A - remove1_mset b B = (if b \<in># B \<and> b \<in># A \<and> count A b \<ge> count B b then {#b#} + (A - B) else A - B)"
   by (auto simp: multiset_eq_iff count_greater_zero_iff[symmetric]
     simp del: count_greater_zero_iff)
 
 lemma add_mset_eq_add_mset_ne:
   "a \<noteq> b \<Longrightarrow> add_mset a A = add_mset b B \<longleftrightarrow> a \<in># B \<and> b \<in># A \<and> A = add_mset b (B - {#a#})"
   by (metis (no_types, lifting) diff_single_eq_union diff_union_swap multi_self_add_other_not_self
     remove_1_mset_id_iff_notin union_single_eq_diff)
 
 lemma add_mset_eq_add_mset: \<open>add_mset a M = add_mset b M' \<longleftrightarrow>
   (a = b \<and> M = M') \<or> (a \<noteq> b \<and> b \<in># M \<and> add_mset a (M - {#b#}) = M')\<close>
   by (metis add_mset_eq_add_mset_ne add_mset_remove_trivial union_single_eq_member)
 
 (* TODO move to Multiset: could replace add_mset_remove_trivial_eq? *)
 lemma add_mset_remove_trivial_iff: \<open>N = add_mset a (N - {#b#}) \<longleftrightarrow> a \<in># N \<and> a = b\<close>
   by (metis add_left_cancel add_mset_remove_trivial insert_DiffM2 single_eq_single
       size_mset_remove1_mset_le_iff union_single_eq_member)
 
 lemma trivial_add_mset_remove_iff: \<open>add_mset a (N - {#b#}) = N \<longleftrightarrow> a \<in># N \<and> a = b\<close>
   by (subst eq_commute) (fact add_mset_remove_trivial_iff)
 
 lemma remove1_single_empty_iff[simp]: \<open>remove1_mset L {#L'#} = {#} \<longleftrightarrow> L = L'\<close>
   using add_mset_remove_trivial_iff by fastforce
 
 lemma add_mset_less_imp_less_remove1_mset:
   assumes xM_lt_N: "add_mset x M < N"
   shows "M < remove1_mset x N"
 proof -
   have "M < N"
     using assms le_multiset_right_total mset_le_trans by blast
   then show ?thesis
     by (metis add_less_cancel_right add_mset_add_single diff_single_trivial insert_DiffM2 xM_lt_N)
 qed
 
 
 subsection \<open>Lemmas about Replicate\<close>
 
 lemma replicate_mset_minus_replicate_mset_same[simp]:
   "replicate_mset m x - replicate_mset n x = replicate_mset (m - n) x"
   by (induct m arbitrary: n, simp, metis left_diff_repeat_mset_distrib' repeat_mset_replicate_mset)
 
 lemma replicate_mset_subset_iff_lt[simp]: "replicate_mset m x \<subset># replicate_mset n x \<longleftrightarrow> m < n"
   by (induct n m rule: diff_induct) (auto intro: subset_mset.gr_zeroI)
 
 lemma replicate_mset_subseteq_iff_le[simp]: "replicate_mset m x \<subseteq># replicate_mset n x \<longleftrightarrow> m \<le> n"
   by (induct n m rule: diff_induct) auto
 
 lemma replicate_mset_lt_iff_lt[simp]: "replicate_mset m x < replicate_mset n x \<longleftrightarrow> m < n"
   by (induct n m rule: diff_induct) (auto intro: subset_mset.gr_zeroI gr_zeroI)
 
 lemma replicate_mset_le_iff_le[simp]: "replicate_mset m x \<le> replicate_mset n x \<longleftrightarrow> m \<le> n"
   by (induct n m rule: diff_induct) auto
 
 lemma replicate_mset_eq_iff[simp]:
   "replicate_mset m x = replicate_mset n y \<longleftrightarrow> m = n \<and> (m \<noteq> 0 \<longrightarrow> x = y)"
   by (cases m; cases n; simp)
     (metis in_replicate_mset insert_noteq_member size_replicate_mset union_single_eq_diff)
 
 lemma replicate_mset_plus: "replicate_mset (a + b) C = replicate_mset a C + replicate_mset b C"
   by (induct a) (auto simp: ac_simps)
 
 lemma mset_replicate_replicate_mset: "mset (replicate n L) = replicate_mset n L"
   by (induction n) auto
 
 lemma set_mset_single_iff_replicate_mset: "set_mset U = {a} \<longleftrightarrow> (\<exists>n > 0. U = replicate_mset n a)"
   by (rule, metis count_greater_zero_iff count_replicate_mset insertI1 multi_count_eq singletonD
     zero_less_iff_neq_zero, force)
 
 lemma ex_replicate_mset_if_all_elems_eq:
   assumes "\<forall>x \<in># M. x = y"
   shows "\<exists>n. M = replicate_mset n y"
   using assms by (metis count_replicate_mset mem_Collect_eq multiset_eqI neq0_conv set_mset_def)
 
 
 subsection \<open>Multiset and Set Conversions\<close>
 
 lemma count_mset_set_if: "count (mset_set A) a = (if a \<in> A \<and> finite A then 1 else 0)"
   by auto
 
 lemma mset_set_set_mset_empty_mempty[iff]: "mset_set (set_mset D) = {#} \<longleftrightarrow> D = {#}"
   by (simp add: mset_set_empty_iff)
 
 lemma count_mset_set_le_one: "count (mset_set A) x \<le> 1"
   by (simp add: count_mset_set_if)
 
 lemma mset_set_set_mset_subseteq[simp]: "mset_set (set_mset A) \<subseteq># A"
   by (simp add: mset_set_set_mset_msubset)
 
 lemma mset_sorted_list_of_set[simp]: "mset (sorted_list_of_set A) = mset_set A"
   by (metis mset_sorted_list_of_multiset sorted_list_of_mset_set)
 
 lemma sorted_sorted_list_of_multiset[simp]:
   "sorted (sorted_list_of_multiset (M :: 'a::linorder multiset))"
   by (metis mset_sorted_list_of_multiset sorted_list_of_multiset_mset sorted_sort)
 
 lemma mset_take_subseteq: "mset (take n xs) \<subseteq># mset xs"
   apply (induct xs arbitrary: n)
    apply simp
   by (case_tac n) simp_all
 
 lemma sorted_list_of_multiset_eq_Nil[simp]: "sorted_list_of_multiset M = [] \<longleftrightarrow> M = {#}"
   by (metis mset_sorted_list_of_multiset sorted_list_of_multiset_empty)
 
 
 subsection \<open>Duplicate Removal\<close>
 
 (* TODO: use abbreviation? *)
 definition remdups_mset :: "'v multiset \<Rightarrow> 'v multiset" where
   "remdups_mset S = mset_set (set_mset S)"
 
 lemma set_mset_remdups_mset[simp]: \<open>set_mset (remdups_mset A) = set_mset A\<close>
   unfolding remdups_mset_def by auto
 
 lemma count_remdups_mset_eq_1: "a \<in># remdups_mset A \<longleftrightarrow> count (remdups_mset A) a = 1"
   unfolding remdups_mset_def by (auto simp: count_eq_zero_iff intro: count_inI)
 
 lemma remdups_mset_empty[simp]: "remdups_mset {#} = {#}"
   unfolding remdups_mset_def by auto
 
 lemma remdups_mset_singleton[simp]: "remdups_mset {#a#} = {#a#}"
   unfolding remdups_mset_def by auto
 
 lemma remdups_mset_eq_empty[iff]: "remdups_mset D = {#} \<longleftrightarrow> D = {#}"
   unfolding remdups_mset_def by blast
 
 lemma remdups_mset_singleton_sum[simp]:
   "remdups_mset (add_mset a A) = (if a \<in># A then remdups_mset A else add_mset a (remdups_mset A))"
   unfolding remdups_mset_def by (simp_all add: insert_absorb)
 
 lemma mset_remdups_remdups_mset[simp]: "mset (remdups D) = remdups_mset (mset D)"
   by (induction D) (auto simp add: ac_simps)
 
 declare mset_remdups_remdups_mset[symmetric, code]
 
 definition distinct_mset :: "'a multiset \<Rightarrow> bool" where
   "distinct_mset S \<longleftrightarrow> (\<forall>a. a \<in># S \<longrightarrow> count S a = 1)"
 
 lemma distinct_mset_count_less_1: "distinct_mset S \<longleftrightarrow> (\<forall>a. count S a \<le> 1)"
   using eq_iff nat_le_linear unfolding distinct_mset_def by fastforce
 
 lemma distinct_mset_empty[simp]: "distinct_mset {#}"
   unfolding distinct_mset_def by auto
 
 lemma distinct_mset_singleton: "distinct_mset {#a#}"
   unfolding distinct_mset_def by auto
 
 lemma distinct_mset_union:
   assumes dist: "distinct_mset (A + B)"
   shows "distinct_mset A"
   unfolding distinct_mset_count_less_1
 proof (rule allI)
   fix a
   have \<open>count A a \<le> count (A + B) a\<close> by auto
   moreover have \<open>count (A + B) a \<le> 1\<close>
     using dist unfolding distinct_mset_count_less_1 by auto
   ultimately show \<open>count A a \<le> 1\<close>
     by simp
 qed
 
 lemma distinct_mset_minus[simp]: "distinct_mset A \<Longrightarrow> distinct_mset (A - B)"
   by (metis diff_subset_eq_self mset_subset_eq_exists_conv distinct_mset_union)
 
 lemma count_remdups_mset_If: \<open>count (remdups_mset A) a = (if a \<in># A then 1 else 0)\<close>
   unfolding remdups_mset_def by auto
 
 lemma distinct_mset_rempdups_union_mset:
   assumes "distinct_mset A" and "distinct_mset B"
   shows "A \<union># B = remdups_mset (A + B)"
   using assms nat_le_linear unfolding remdups_mset_def
   by (force simp add: multiset_eq_iff max_def count_mset_set_if distinct_mset_def not_in_iff)
 
 lemma distinct_mset_add_mset[simp]: "distinct_mset (add_mset a L) \<longleftrightarrow> a \<notin># L \<and> distinct_mset L"
   unfolding distinct_mset_def
   apply (rule iffI)
    apply (auto split: if_split_asm; fail)[]
   by (auto simp: not_in_iff; fail)
 
 lemma distinct_mset_size_eq_card: "distinct_mset C \<Longrightarrow> size C = card (set_mset C)"
   by (induction C) auto
 
 lemma distinct_mset_add:
   "distinct_mset (L + L') \<longleftrightarrow> distinct_mset L \<and> distinct_mset L' \<and> L \<inter># L' = {#}"
   by (induction L arbitrary: L') auto
 
 lemma distinct_mset_set_mset_ident[simp]: "distinct_mset M \<Longrightarrow> mset_set (set_mset M) = M"
   by (induction M) auto
 
 lemma distinct_finite_set_mset_subseteq_iff[iff]:
   assumes "distinct_mset M" "finite N"
   shows "set_mset M \<subseteq> N \<longleftrightarrow> M \<subseteq># mset_set N"
   by (metis assms distinct_mset_set_mset_ident finite_set_mset msubset_mset_set_iff)
 
 lemma distinct_mem_diff_mset:
   assumes dist: "distinct_mset M" and mem: "x \<in> set_mset (M - N)"
   shows "x \<notin> set_mset N"
 proof -
   have "count M x = 1"
     using dist mem by (meson distinct_mset_def in_diffD)
   then show ?thesis
     using mem by (metis count_greater_eq_one_iff in_diff_count not_less)
 qed
 
 lemma distinct_set_mset_eq:
   assumes "distinct_mset M" "distinct_mset N" "set_mset M = set_mset N"
   shows "M = N"
   using assms distinct_mset_set_mset_ident by fastforce
 
 lemma distinct_mset_union_mset[simp]:
   \<open>distinct_mset (D \<union># C) \<longleftrightarrow> distinct_mset D \<and> distinct_mset C\<close>
   unfolding distinct_mset_count_less_1 by force
 
 lemma distinct_mset_inter_mset:
   "distinct_mset C \<Longrightarrow> distinct_mset (C \<inter># D)"
   "distinct_mset D \<Longrightarrow> distinct_mset (C \<inter># D)"
   by (simp_all add: multiset_inter_def,
     metis distinct_mset_minus multiset_inter_commute multiset_inter_def)
 
 lemma distinct_mset_remove1_All: "distinct_mset C \<Longrightarrow> remove1_mset L C = removeAll_mset L C"
   by (auto simp: multiset_eq_iff distinct_mset_count_less_1)
 
 lemma distinct_mset_size_2: "distinct_mset {#a, b#} \<longleftrightarrow> a \<noteq> b"
   by auto
 
 lemma distinct_mset_filter: "distinct_mset M \<Longrightarrow> distinct_mset {# L \<in># M. P L#}"
   by (simp add: distinct_mset_def)
 
 lemma distinct_mset_mset_distinct[simp]: \<open>distinct_mset (mset xs) = distinct xs\<close>
   by (induction xs) auto
 
 lemma distinct_image_mset_inj:
   \<open>inj_on f (set_mset M) \<Longrightarrow> distinct_mset (image_mset f M) \<longleftrightarrow> distinct_mset M\<close>
   by (induction M) (auto simp: inj_on_def)
 
 
 subsection \<open>Repeat Operation\<close>
 
 lemma repeat_mset_compower: "repeat_mset n A = (((+) A) ^^ n) {#}"
   by (induction n) auto
 
 lemma repeat_mset_prod: "repeat_mset (m * n) A = (((+) (repeat_mset n A)) ^^ m) {#}"
   by (induction m) (auto simp: repeat_mset_distrib)
 
 
 subsection \<open>Cartesian Product\<close>
 
 text \<open>Definition of the cartesian products over multisets. The construction mimics of the cartesian
   product on sets and use the same theorem names (adding only the suffix \<open>_mset\<close> to Sigma
   and Times). See file @{file \<open>~~/src/HOL/Product_Type.thy\<close>}\<close>
 
 definition Sigma_mset :: "'a multiset \<Rightarrow> ('a \<Rightarrow> 'b multiset) \<Rightarrow> ('a \<times> 'b) multiset" where
   "Sigma_mset A B \<equiv> \<Union># {#{#(a, b). b \<in># B a#}. a \<in># A #}"
 
 abbreviation Times_mset :: "'a multiset \<Rightarrow> 'b multiset \<Rightarrow> ('a \<times> 'b) multiset" (infixr "\<times>#" 80) where
   "Times_mset A B \<equiv> Sigma_mset A (\<lambda>_. B)"
 
 hide_const (open) Times_mset
 
 text \<open>Contrary to the set version @{term \<open>SIGMA x:A. B\<close>}, we use the non-ASCII symbol \<open>\<in>#\<close>.\<close>
 
 syntax
   "_Sigma_mset" :: "[pttrn, 'a multiset, 'b multiset] => ('a * 'b) multiset"
   ("(3SIGMAMSET _\<in>#_./ _)" [0, 0, 10] 10)
 translations
   "SIGMAMSET x\<in>#A. B" == "CONST Sigma_mset A (\<lambda>x. B)"
 
 text \<open>Link between the multiset and the set cartesian product:\<close>
 
 lemma Times_mset_Times: "set_mset (A \<times># B) = set_mset A \<times> set_mset B"
   unfolding Sigma_mset_def by auto
 
 lemma Sigma_msetI [intro!]: "\<lbrakk>a \<in># A; b \<in># B a\<rbrakk> \<Longrightarrow> (a, b) \<in># Sigma_mset A B"
   by (unfold Sigma_mset_def) auto
 
 lemma Sigma_msetE[elim!]: "\<lbrakk>c \<in># Sigma_mset A B; \<And>x y. \<lbrakk>x \<in># A; y \<in># B x; c = (x, y)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
   by (unfold Sigma_mset_def) auto
 
 text \<open>Elimination of @{term "(a, b) \<in># A \<times># B"} -- introduces no eigenvariables.\<close>
 
 lemma Sigma_msetD1: "(a, b) \<in># Sigma_mset A B \<Longrightarrow> a \<in># A"
   by blast
 
 lemma Sigma_msetD2: "(a, b) \<in># Sigma_mset A B \<Longrightarrow> b \<in># B a"
   by blast
 
 lemma Sigma_msetE2: "\<lbrakk>(a, b) \<in># Sigma_mset A B; \<lbrakk>a \<in># A; b \<in># B a\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
   by blast
 
 lemma Sigma_mset_cong:
   "\<lbrakk>A = B; \<And>x. x \<in># B \<Longrightarrow> C x = D x\<rbrakk> \<Longrightarrow> (SIGMAMSET x \<in># A. C x) = (SIGMAMSET x \<in># B. D x)"
   by (metis (mono_tags, lifting) Sigma_mset_def image_mset_cong)
 
 lemma count_sum_mset: "count (\<Union># M) b = (\<Sum>P \<in># M. count P b)"
   by (induction M) auto
 
 lemma Sigma_mset_plus_distrib1[simp]: "Sigma_mset (A + B) C = Sigma_mset A C + Sigma_mset B C"
   unfolding Sigma_mset_def by auto
 
 lemma Sigma_mset_plus_distrib2[simp]:
   "Sigma_mset A (\<lambda>i. B i + C i) = Sigma_mset A B + Sigma_mset A C"
   unfolding Sigma_mset_def by (induction A) (auto simp: multiset_eq_iff)
 
 lemma Times_mset_single_left: "{#a#} \<times># B = image_mset (Pair a) B"
   unfolding Sigma_mset_def by auto
 
 lemma Times_mset_single_right: "A \<times># {#b#} = image_mset (\<lambda>a. Pair a b) A"
   unfolding Sigma_mset_def by (induction A) auto
 
 lemma Times_mset_single_single[simp]: "{#a#} \<times># {#b#} = {#(a, b)#}"
   unfolding Sigma_mset_def by simp
 
 lemma count_image_mset_Pair:
   "count (image_mset (Pair a) B) (x, b) = (if x = a then count B b else 0)"
   by (induction B) auto
 
 lemma count_Sigma_mset: "count (Sigma_mset A B) (a, b) = count A a * count (B a) b"
   by (induction A) (auto simp: Sigma_mset_def count_image_mset_Pair)
 
 lemma Sigma_mset_empty1[simp]: "Sigma_mset {#} B = {#}"
   unfolding Sigma_mset_def by auto
 
 lemma Sigma_mset_empty2[simp]: "A \<times># {#} = {#}"
   by (auto simp: multiset_eq_iff count_Sigma_mset)
 
 lemma Sigma_mset_mono:
   assumes "A \<subseteq># C" and "\<And>x. x \<in># A \<Longrightarrow> B x \<subseteq># D x"
   shows "Sigma_mset A B \<subseteq># Sigma_mset C D"
 proof -
   have "count A a * count (B a) b \<le> count C a * count (D a) b" for a b
     using assms unfolding subseteq_mset_def by (metis count_inI eq_iff mult_eq_0_iff mult_le_mono)
   then show ?thesis
     by (auto simp: subseteq_mset_def count_Sigma_mset)
 qed
 
 lemma mem_Sigma_mset_iff[iff]: "((a,b) \<in># Sigma_mset A B) = (a \<in># A \<and> b \<in># B a)"
   by blast
 
 lemma mem_Times_mset_iff: "x \<in># A \<times># B \<longleftrightarrow> fst x \<in># A \<and> snd x \<in># B"
   by (induct x) simp
 
 lemma Sigma_mset_empty_iff: "(SIGMAMSET i\<in>#I. X i) = {#} \<longleftrightarrow> (\<forall>i\<in>#I. X i = {#})"
   by (auto simp: Sigma_mset_def)
 
 lemma Times_mset_subset_mset_cancel1: "x \<in># A \<Longrightarrow> (A \<times># B \<subseteq># A \<times># C) = (B \<subseteq># C)"
   by (auto simp: subseteq_mset_def count_Sigma_mset)
 
 lemma Times_mset_subset_mset_cancel2: "x \<in># C \<Longrightarrow> (A \<times># C \<subseteq># B \<times># C) = (A \<subseteq># B)"
   by (auto simp: subseteq_mset_def count_Sigma_mset)
 
 lemma Times_mset_eq_cancel2: "x \<in># C \<Longrightarrow> (A \<times># C = B \<times># C) = (A = B)"
   by (auto simp: multiset_eq_iff count_Sigma_mset dest!: in_countE)
 
 lemma split_paired_Ball_mset_Sigma_mset[simp]:
   "(\<forall>z\<in>#Sigma_mset A B. P z) \<longleftrightarrow> (\<forall>x\<in>#A. \<forall>y\<in>#B x. P (x, y))"
   by blast
 
 lemma split_paired_Bex_mset_Sigma_mset[simp]:
   "(\<exists>z\<in>#Sigma_mset A B. P z) \<longleftrightarrow> (\<exists>x\<in>#A. \<exists>y\<in>#B x. P (x, y))"
   by blast
 
 lemma sum_mset_if_eq_constant:
   "(\<Sum>x\<in>#M. if a = x then (f x) else 0) = (((+) (f a)) ^^ (count M a)) 0"
   by (induction M) (auto simp: ac_simps)
 
 lemma iterate_op_plus: "(((+) k) ^^ m) 0 = k * m"
   by (induction m) auto
 
 lemma untion_image_mset_Pair_distribute:
   "\<Union>#{#image_mset (Pair x) (C x). x \<in># J - I#} =
    \<Union># {#image_mset (Pair x) (C x). x \<in># J#} - \<Union>#{#image_mset (Pair x) (C x). x \<in># I#}"
   by (auto simp: multiset_eq_iff count_sum_mset count_image_mset_Pair sum_mset_if_eq_constant
     iterate_op_plus diff_mult_distrib2)
 
 lemma Sigma_mset_Un_distrib1: "Sigma_mset (I \<union># J) C = Sigma_mset I C \<union># Sigma_mset J C"
   by (auto simp: Sigma_mset_def sup_subset_mset_def untion_image_mset_Pair_distribute)
 
 lemma Sigma_mset_Un_distrib2: "(SIGMAMSET i\<in>#I. A i \<union># B i) = Sigma_mset I A \<union># Sigma_mset I B"
   by (auto simp: multiset_eq_iff count_sum_mset count_image_mset_Pair sum_mset_if_eq_constant
     Sigma_mset_def diff_mult_distrib2 iterate_op_plus max_def not_in_iff)
 
 lemma Sigma_mset_Int_distrib1: "Sigma_mset (I \<inter># J) C = Sigma_mset I C \<inter># Sigma_mset J C"
   by (auto simp: multiset_eq_iff count_sum_mset count_image_mset_Pair sum_mset_if_eq_constant
     Sigma_mset_def iterate_op_plus min_def not_in_iff)
 
 lemma Sigma_mset_Int_distrib2: "(SIGMAMSET i\<in>#I. A i \<inter># B i) = Sigma_mset I A \<inter># Sigma_mset I B"
   by (auto simp: multiset_eq_iff count_sum_mset count_image_mset_Pair sum_mset_if_eq_constant
     Sigma_mset_def iterate_op_plus min_def not_in_iff)
 
 lemma Sigma_mset_Diff_distrib1: "Sigma_mset (I - J) C = Sigma_mset I C - Sigma_mset J C"
   by (auto simp: multiset_eq_iff count_sum_mset count_image_mset_Pair sum_mset_if_eq_constant
     Sigma_mset_def iterate_op_plus min_def not_in_iff diff_mult_distrib2)
 
 lemma Sigma_mset_Diff_distrib2: "(SIGMAMSET i\<in>#I. A i - B i) = Sigma_mset I A - Sigma_mset I B"
   by (auto simp: multiset_eq_iff count_sum_mset count_image_mset_Pair sum_mset_if_eq_constant
     Sigma_mset_def iterate_op_plus min_def not_in_iff diff_mult_distrib)
 
 lemma Sigma_mset_Union: "Sigma_mset (\<Union>#X) B = (\<Union># (image_mset (\<lambda>A. Sigma_mset A B) X))"
   by (auto simp: multiset_eq_iff count_sum_mset count_image_mset_Pair sum_mset_if_eq_constant
     Sigma_mset_def iterate_op_plus min_def not_in_iff sum_mset_distrib_left)
 
 lemma Times_mset_Un_distrib1: "(A \<union># B) \<times># C = A \<times># C \<union># B \<times># C"
   by (fact Sigma_mset_Un_distrib1)
 
 lemma Times_mset_Int_distrib1: "(A \<inter># B) \<times># C = A \<times># C \<inter># B \<times># C"
   by (fact Sigma_mset_Int_distrib1)
 
 lemma Times_mset_Diff_distrib1: "(A - B) \<times># C = A \<times># C - B \<times># C"
   by (fact Sigma_mset_Diff_distrib1)
 
 lemma Times_mset_empty[simp]: "A \<times># B = {#} \<longleftrightarrow> A = {#} \<or> B = {#}"
   by (auto simp: Sigma_mset_empty_iff)
 
 lemma Times_insert_left: "A \<times># add_mset x B = A \<times># B + image_mset (\<lambda>a. Pair a x) A"
   unfolding add_mset_add_single[of x B] Sigma_mset_plus_distrib2
   by (simp add: Times_mset_single_right)
 
 lemma Times_insert_right: "add_mset a A \<times># B = A \<times># B + image_mset (Pair a) B"
   unfolding add_mset_add_single[of a A] Sigma_mset_plus_distrib1
   by (simp add: Times_mset_single_left)
 
 lemma fst_image_mset_times_mset [simp]:
   "image_mset fst (A \<times># B) = (if B = {#} then {#} else repeat_mset (size B) A)"
   by (induct B) (auto simp: Times_mset_single_right ac_simps Times_insert_left)
 
 lemma snd_image_mset_times_mset [simp]:
   "image_mset snd (A \<times># B) = (if A = {#} then {#} else repeat_mset (size A) B)"
   by (induct B) (auto simp add: Times_mset_single_right Times_insert_left image_mset_const_eq)
 
 lemma product_swap_mset: "image_mset prod.swap (A \<times># B) = B \<times># A"
   by (induction A) (auto simp add: Times_mset_single_left Times_mset_single_right
       Times_insert_right Times_insert_left)
 
 context
 begin
 
 qualified definition product_mset :: "'a multiset \<Rightarrow> 'b multiset \<Rightarrow> ('a \<times> 'b) multiset" where
   [code_abbrev]: "product_mset A B = A \<times># B"
 
 lemma member_product_mset: "x \<in># product_mset A B \<longleftrightarrow> x \<in># A \<times># B"
   by (simp add: Multiset_More.product_mset_def)
 
 end
 
 lemma count_Sigma_mset_abs_def: "count (Sigma_mset A B) = (\<lambda>(a, b) \<Rightarrow> count A a * count (B a) b)"
   by (auto simp: fun_eq_iff count_Sigma_mset)
 
 lemma Times_mset_image_mset1: "image_mset f A \<times># B = image_mset (\<lambda>(a, b). (f a, b)) (A \<times># B)"
   by (induct B) (auto simp: Times_insert_left)
 
 lemma Times_mset_image_mset2: "A \<times># image_mset f B = image_mset (\<lambda>(a, b). (a, f b)) (A \<times># B)"
   by (induct A) (auto simp: Times_insert_right)
 
 lemma sum_le_singleton: "A \<subseteq> {x} \<Longrightarrow> sum f A = (if x \<in> A then f x else 0)"
   by (auto simp: subset_singleton_iff elim: finite_subset)
 
 lemma Times_mset_assoc: "(A \<times># B) \<times># C = image_mset (\<lambda>(a, b, c). ((a, b), c)) (A \<times># B \<times># C)"
   by (auto simp: multiset_eq_iff count_Sigma_mset count_image_mset vimage_def Times_mset_Times
       Int_commute count_eq_zero_iff intro!: trans[OF _ sym[OF sum_le_singleton[of _ "(_, _, _)"]]]
       cong: sum.cong if_cong)
 
 
 subsection \<open>Transfer Rules\<close>
 
 lemma plus_multiset_transfer[transfer_rule]:
   "(rel_fun (rel_mset R) (rel_fun (rel_mset R) (rel_mset R))) (+) (+)"
   by (unfold rel_fun_def rel_mset_def)
     (force dest: list_all2_appendI intro: exI[of _ "_ @ _"] conjI[rotated])
 
 lemma minus_multiset_transfer[transfer_rule]:
   assumes [transfer_rule]: "bi_unique R"
   shows "(rel_fun (rel_mset R) (rel_fun (rel_mset R) (rel_mset R))) (-) (-)"
 proof (unfold rel_fun_def rel_mset_def, safe)
   fix xs ys xs' ys'
   assume [transfer_rule]: "list_all2 R xs ys" "list_all2 R xs' ys'"
   have "list_all2 R (fold remove1 xs' xs) (fold remove1 ys' ys)"
     by transfer_prover
   moreover have "mset (fold remove1 xs' xs) = mset xs - mset xs'"
     by (induct xs' arbitrary: xs) auto
   moreover have "mset (fold remove1 ys' ys) = mset ys - mset ys'"
     by (induct ys' arbitrary: ys) auto
   ultimately show "\<exists>xs'' ys''.
     mset xs'' = mset xs - mset xs' \<and> mset ys'' = mset ys - mset ys' \<and> list_all2 R xs'' ys''"
     by blast
 qed
 
 declare rel_mset_Zero[transfer_rule]
 
 lemma count_transfer[transfer_rule]:
   assumes "bi_unique R"
   shows "(rel_fun (rel_mset R) (rel_fun R (=))) count count"
 unfolding rel_fun_def rel_mset_def proof safe
   fix x y xs ys
   assume "list_all2 R xs ys" "R x y"
   then show "count (mset xs) x = count (mset ys) y"
   proof (induct xs ys rule: list.rel_induct)
     case (Cons x' xs y' ys)
     then show ?case
       using assms unfolding bi_unique_alt_def2 by (auto simp: rel_fun_def)
   qed simp
 qed
 
 lemma subseteq_multiset_transfer[transfer_rule]:
   assumes [transfer_rule]: "bi_unique R" "right_total R"
   shows "(rel_fun (rel_mset R) (rel_fun (rel_mset R) (=)))
     (\<lambda>M N. filter_mset (Domainp R) M \<subseteq># filter_mset (Domainp R) N) (\<subseteq>#)"
 proof -
   have count_filter_mset_less:
     "(\<forall>a. count (filter_mset (Domainp R) M) a \<le> count (filter_mset (Domainp R) N) a) \<longleftrightarrow>
      (\<forall>a \<in> {x. Domainp R x}. count M a \<le> count N a)" for M and N by auto
   show ?thesis unfolding subseteq_mset_def count_filter_mset_less
     by transfer_prover
 qed
 
 lemma sum_mset_transfer[transfer_rule]:
   "R 0 0 \<Longrightarrow> rel_fun R (rel_fun R R) (+) (+) \<Longrightarrow> (rel_fun (rel_mset R) R) sum_mset sum_mset"
   using sum_list_transfer[of R] unfolding rel_fun_def rel_mset_def by auto
 
 lemma Sigma_mset_transfer[transfer_rule]:
   "(rel_fun (rel_mset R) (rel_fun (rel_fun R (rel_mset S)) (rel_mset (rel_prod R S))))
      Sigma_mset Sigma_mset"
   by (unfold Sigma_mset_def) transfer_prover
 
 
 subsection \<open>Even More about Multisets\<close>
 
 subsubsection \<open>Multisets and Functions\<close>
 
 lemma range_image_mset:
   assumes "set_mset Ds \<subseteq> range f"
   shows "Ds \<in> range (image_mset f)"
 proof -
   have "\<forall>D. D \<in># Ds \<longrightarrow> (\<exists>C. f C = D)"
     using assms by blast
   then obtain f_i where
     f_p: "\<forall>D. D \<in># Ds \<longrightarrow> (f (f_i D) = D)"
     by metis
   define Cs where
     "Cs \<equiv> image_mset f_i Ds"
   from f_p Cs_def have "image_mset f Cs = Ds"
     by auto
   then show ?thesis
     by blast
 qed
 
 
 subsubsection \<open>Multisets and Lists\<close>
 
 lemma length_sorted_list_of_multiset[simp]: "length (sorted_list_of_multiset A) = size A"
   by (metis mset_sorted_list_of_multiset size_mset)
 
 definition list_of_mset :: "'a multiset \<Rightarrow> 'a list" where
   "list_of_mset m = (SOME l. m = mset l)"
 
 lemma list_of_mset_exi: "\<exists>l. m = mset l"
   using ex_mset by metis
 
-lemma mset_list_of_mset [simp]: "mset (list_of_mset m) = m"
+lemma mset_list_of_mset[simp]: "mset (list_of_mset m) = m"
   by (metis (mono_tags, lifting) ex_mset list_of_mset_def someI_ex)
 
 lemma length_list_of_mset[simp]: "length (list_of_mset A) = size A"
   unfolding list_of_mset_def by (metis (mono_tags) ex_mset size_mset someI_ex)
 
 lemma range_mset_map:
   assumes "set_mset Ds \<subseteq> range f"
   shows "Ds \<in> range (\<lambda>Cl. mset (map f Cl))"
 proof -
   have "Ds \<in> range (image_mset f)"
     by (simp add: assms range_image_mset)
   then obtain Cs where Cs_p: "image_mset f Cs = Ds"
     by auto
   define Cl where "Cl = list_of_mset Cs"
   then have "mset Cl = Cs"
     by auto
   then have "image_mset f (mset Cl) = Ds"
     using Cs_p by auto
   then have "mset (map f Cl) = Ds"
     by auto
   then show ?thesis
     by auto
 qed
 
 lemma list_of_mset_empty[iff]: "list_of_mset m = [] \<longleftrightarrow> m = {#}"
   by (metis (mono_tags, lifting) ex_mset list_of_mset_def mset_zero_iff_right someI_ex)
 
 lemma in_mset_conv_nth: "(x \<in># mset xs) = (\<exists>i<length xs. xs ! i = x)"
   by (auto simp: in_set_conv_nth)
 
 lemma in_mset_sum_list:
   assumes "L \<in># LL"
   assumes "LL \<in> set Ci"
   shows "L \<in># sum_list Ci"
   using assms by (induction Ci) auto
 
 lemma in_mset_sum_list2:
   assumes "L \<in># sum_list Ci"
   obtains LL where
     "LL \<in> set Ci"
     "L \<in># LL"
   using assms by (induction Ci) auto
 
 (* TODO: Make [simp]. *)
 lemma in_mset_sum_list_iff: "a \<in># sum_list \<A> \<longleftrightarrow> (\<exists>A \<in> set \<A>. a \<in># A)"
   by (metis in_mset_sum_list in_mset_sum_list2)
 
 lemma subseteq_list_Union_mset:
   assumes "length Ci = n"
   assumes "length CAi = n"
   assumes "\<forall>i<n.  Ci ! i \<subseteq># CAi ! i "
   shows "\<Union># (mset Ci) \<subseteq># \<Union># (mset CAi)"
   using assms proof (induction n arbitrary: Ci CAi)
   case 0
   then show ?case by auto
 next
   case (Suc n)
   from Suc have "\<forall>i<n. tl Ci ! i \<subseteq># tl CAi ! i"
     by (simp add: nth_tl)
   hence "\<Union>#(mset (tl Ci)) \<subseteq># \<Union>#(mset (tl CAi))" using Suc by auto
   moreover
   have "hd Ci \<subseteq># hd CAi" using Suc
     by (metis hd_conv_nth length_greater_0_conv zero_less_Suc)
   ultimately
   show "\<Union>#(mset Ci) \<subseteq># \<Union>#(mset CAi)"
     using Suc by (cases Ci; cases CAi) (auto intro: subset_mset.add_mono)
 qed
 
 
 subsubsection \<open>More on Multisets and Functions\<close>
 
 lemma subseteq_mset_size_eql: "X \<subseteq># Y \<Longrightarrow> size Y = size X \<Longrightarrow> X = Y"
   using mset_subset_size subset_mset_def by fastforce
 
 lemma image_mset_of_subset_list:
   assumes "image_mset \<eta> C' = mset lC"
   shows "\<exists>qC'. map \<eta> qC' = lC \<and> mset qC' = C'"
   using assms apply (induction lC arbitrary: C')
   subgoal by simp
   subgoal by (fastforce dest!: msed_map_invR intro: exI[of _ \<open>_ # _\<close>])
   done
 
 lemma image_mset_of_subset:
   assumes "A \<subseteq># image_mset \<eta> C'"
   shows "\<exists>A'. image_mset \<eta> A' = A \<and> A' \<subseteq># C'"
 proof -
   define C where "C = image_mset \<eta> C'"
 
   define lA where "lA = list_of_mset A"
   define lD where "lD = list_of_mset (C-A)"
   define lC where "lC = lA @ lD"
 
   have "mset lC = C"
     using C_def assms unfolding lD_def lC_def lA_def by auto
   then have "\<exists>qC'. map \<eta> qC' = lC \<and> mset qC' = C'"
     using assms image_mset_of_subset_list unfolding C_def by metis
   then obtain qC' where qC'_p: "map \<eta> qC' = lC \<and> mset qC' = C'"
     by auto
   let ?lA' = "take (length lA) qC'"
   have m: "map \<eta> ?lA' = lA"
     using qC'_p lC_def
     by (metis append_eq_conv_conj take_map)
   let ?A' = "mset ?lA'"
 
   have "image_mset \<eta> ?A' = A"
     using m using lA_def
     by (metis (full_types) ex_mset list_of_mset_def mset_map someI_ex)
   moreover have "?A' \<subseteq># C'"
     using qC'_p unfolding lA_def
     using mset_take_subseteq by blast
   ultimately show ?thesis by blast
 qed
 
 lemma all_the_same: "\<forall>x \<in># X. x = y \<Longrightarrow> card (set_mset X) \<le> Suc 0"
   by (metis card.empty card.insert card_mono finite.intros(1) finite_insert le_SucI singletonI subsetI)
 
 lemma Melem_subseteq_Union_mset[simp]:
   assumes "x \<in># T"
   shows "x \<subseteq># \<Union>#T"
   using assms sum_mset.remove by force
 
 lemma Melem_subset_eq_sum_list[simp]:
   assumes "x \<in># mset T"
   shows "x \<subseteq># sum_list T"
   using assms by (metis mset_subset_eq_add_left sum_mset.remove sum_mset_sum_list)
 
 lemma less_subset_eq_Union_mset[simp]:
   assumes "i < length CAi"
   shows "CAi ! i \<subseteq># \<Union>#(mset CAi)"
 proof -
   from assms have "CAi ! i \<in># mset CAi"
     by auto
   then show ?thesis
     by auto
 qed
 
 lemma less_subset_eq_sum_list[simp]:
   assumes "i < length CAi"
   shows "CAi ! i \<subseteq># sum_list CAi"
 proof -
   from assms have "CAi ! i \<in># mset CAi"
     by auto
   then show ?thesis
     by auto
 qed
 
 
 subsubsection \<open>More on Multiset Order\<close>
 
 lemma less_multiset_doubletons:
   assumes
     "y < t \<or> y < s"  
     "x < t \<or> x < s" 
   shows 
     "{#y, x#} < {#t, s#}" 
   unfolding less_multiset\<^sub>D\<^sub>M
 proof (intro exI)
   let ?X = "{#t, s#}"
   let ?Y = "{#y, x#}"
   show "?X \<noteq> {#} \<and> ?X \<subseteq># {#t, s#} \<and> {#y, x#} = {#t, s#} - ?X + ?Y
     \<and> (\<forall>k. k \<in># ?Y \<longrightarrow> (\<exists>a. a \<in># ?X \<and> k < a))"
     using add_eq_conv_diff assms by auto
 qed
 
 end
diff --git a/thys/Saturation_Framework/Lifting_to_Non_Ground_Calculi.thy b/thys/Saturation_Framework/Lifting_to_Non_Ground_Calculi.thy
--- a/thys/Saturation_Framework/Lifting_to_Non_Ground_Calculi.thy
+++ b/thys/Saturation_Framework/Lifting_to_Non_Ground_Calculi.thy
@@ -1,737 +1,754 @@
 (*  Title:       Lifting to Non-Ground Calculi of the Saturation Framework
  *  Author:      Sophie Tourret <stourret at mpi-inf.mpg.de>, 2018-2020 *)
 
 section \<open>Lifting to Non-ground Calculi\<close>
 
 text \<open>The section 3.1 to 3.3 of the report are covered by the current section.
   Various forms of lifting are proven correct. These allow to obtain the dynamic
   refutational completeness of a non-ground calculus from the static refutational
   completeness of its ground counterpart.\<close>
 
 theory Lifting_to_Non_Ground_Calculi
   imports
     Calculi
     Well_Quasi_Orders.Minimal_Elements
 begin
 
 subsection \<open>Standard Lifting\<close>
 
 locale standard_lifting = inference_system Inf_F +
   ground: calculus_with_red_crit Bot_G Inf_G entails_G Red_Inf_G Red_F_G
   for
     Bot_F :: \<open>'f set\<close> and
     Inf_F :: \<open>'f inference set\<close> and
     Bot_G :: \<open>'g set\<close> and
     Inf_G ::  \<open>'g inference set\<close> and
     entails_G ::  \<open>'g set  \<Rightarrow> 'g set  \<Rightarrow> bool\<close> (infix "\<Turnstile>G" 50) and
     Red_Inf_G :: \<open>'g set \<Rightarrow> 'g inference set\<close> and
     Red_F_G :: \<open>'g set \<Rightarrow> 'g set\<close>
   + fixes
     \<G>_F :: \<open>'f \<Rightarrow> 'g set\<close> and
     \<G>_Inf :: \<open>'f inference \<Rightarrow> 'g inference set option\<close>
   assumes
     Bot_F_not_empty: "Bot_F \<noteq> {}" and
     Bot_map_not_empty: \<open>B \<in> Bot_F \<Longrightarrow> \<G>_F B \<noteq> {}\<close> and
     Bot_map: \<open>B \<in> Bot_F \<Longrightarrow> \<G>_F B \<subseteq> Bot_G\<close> and
     Bot_cond: \<open>\<G>_F C \<inter> Bot_G \<noteq> {} \<longrightarrow> C \<in> Bot_F\<close> and
     inf_map: \<open>\<iota> \<in> Inf_F \<Longrightarrow> \<G>_Inf \<iota> \<noteq> None \<Longrightarrow> the (\<G>_Inf \<iota>) \<subseteq> Red_Inf_G (\<G>_F (concl_of \<iota>))\<close>
 begin
 
 abbreviation \<G>_set :: \<open>'f set \<Rightarrow> 'g set\<close> where
   \<open>\<G>_set N \<equiv> \<Union> (\<G>_F ` N)\<close>
 
 lemma \<G>_subset: \<open>N1 \<subseteq> N2 \<Longrightarrow> \<G>_set N1 \<subseteq> \<G>_set N2\<close> by auto
 
 abbreviation entails_\<G>  :: \<open>'f set \<Rightarrow> 'f set \<Rightarrow> bool\<close> (infix "\<Turnstile>\<G>" 50) where
   \<open>N1 \<Turnstile>\<G> N2 \<equiv> \<G>_set N1 \<Turnstile>G \<G>_set N2\<close>
 
 lemma subs_Bot_G_entails:
   assumes
     not_empty: \<open>sB \<noteq> {}\<close> and
     in_bot: \<open>sB \<subseteq> Bot_G\<close>
   shows \<open>sB \<Turnstile>G N\<close>
 proof -
   have \<open>\<exists>B. B \<in> sB\<close> using not_empty by auto
   then obtain B where B_in: \<open>B \<in> sB\<close> by auto
   then have r_trans: \<open>{B} \<Turnstile>G N\<close> using ground.bot_entails_all in_bot by auto
   have l_trans: \<open>sB \<Turnstile>G {B}\<close> using B_in ground.subset_entailed by auto
   then show ?thesis using r_trans ground.entails_trans[of sB "{B}"] by auto
 qed
 
 (* lem:derived-consequence-relation *)
 sublocale consequence_relation Bot_F entails_\<G>
 proof
   show "Bot_F \<noteq> {}" using Bot_F_not_empty .
 next
   show \<open>B\<in>Bot_F \<Longrightarrow> {B} \<Turnstile>\<G> N\<close> for B N
   proof -
     assume \<open>B \<in> Bot_F\<close>
     then show \<open>{B} \<Turnstile>\<G> N\<close>
       using Bot_map ground.bot_entails_all[of _ "\<G>_set N"] subs_Bot_G_entails Bot_map_not_empty
       by auto
   qed
 next
   fix N1 N2 :: \<open>'f set\<close>
   assume
     \<open>N2 \<subseteq> N1\<close>
   then show \<open>N1 \<Turnstile>\<G> N2\<close> using \<G>_subset ground.subset_entailed by auto
 next
   fix N1 N2
   assume
     N1_entails_C: \<open>\<forall>C \<in> N2. N1 \<Turnstile>\<G> {C}\<close>
   show \<open>N1 \<Turnstile>\<G> N2\<close> using ground.all_formulas_entailed N1_entails_C
     by (smt UN_E UN_I ground.entail_set_all_formulas singletonI)
 next
   fix N1 N2 N3
   assume
     \<open>N1 \<Turnstile>\<G> N2\<close> and \<open>N2 \<Turnstile>\<G> N3\<close>
   then show \<open>N1 \<Turnstile>\<G> N3\<close> using ground.entails_trans by blast
 qed
 
 end
 
 subsection \<open>Strong Standard Lifting\<close>
 
 (* rmk:strong-standard-lifting *)
 locale strong_standard_lifting = inference_system Inf_F +
   ground: calculus_with_red_crit Bot_G Inf_G entails_G Red_Inf_G Red_F_G
   for
     Bot_F :: \<open>'f set\<close> and
     Inf_F :: \<open>'f inference set\<close> and
     Bot_G :: \<open>'g set\<close> and
     Inf_G ::  \<open>'g inference set\<close> and
     entails_G ::  \<open>'g set  \<Rightarrow> 'g set  \<Rightarrow> bool\<close> (infix "\<Turnstile>G" 50) and
     Red_Inf_G :: \<open>'g set \<Rightarrow> 'g inference set\<close> and
     Red_F_G :: \<open>'g set \<Rightarrow> 'g set\<close>
   + fixes
     \<G>_F :: \<open>'f \<Rightarrow> 'g set\<close> and
     \<G>_Inf :: \<open>'f inference \<Rightarrow> 'g inference set option\<close>
   assumes
     Bot_F_not_empty: "Bot_F \<noteq> {}" and
     Bot_map_not_empty: \<open>B \<in> Bot_F \<Longrightarrow> \<G>_F B \<noteq> {}\<close> and
     Bot_map: \<open>B \<in> Bot_F \<Longrightarrow> \<G>_F B \<subseteq> Bot_G\<close> and
     Bot_cond: \<open>\<G>_F C \<inter> Bot_G \<noteq> {} \<longrightarrow> C \<in> Bot_F\<close> and
     strong_inf_map: \<open>\<iota> \<in> Inf_F \<Longrightarrow> \<G>_Inf \<iota> \<noteq> None \<Longrightarrow> concl_of ` (the (\<G>_Inf \<iota>)) \<subseteq> (\<G>_F (concl_of \<iota>))\<close> and
     inf_map_in_Inf: \<open>\<iota> \<in> Inf_F \<Longrightarrow> \<G>_Inf \<iota> \<noteq> None \<Longrightarrow> the (\<G>_Inf \<iota>) \<subseteq> Inf_G\<close>
 begin
 
 sublocale standard_lifting Bot_F Inf_F Bot_G Inf_G "(\<Turnstile>G)" Red_Inf_G Red_F_G \<G>_F \<G>_Inf
 proof
   show "Bot_F \<noteq> {}" using Bot_F_not_empty .
 next
   fix B
   assume b_in: "B \<in> Bot_F"
   show "\<G>_F B \<noteq> {}" using Bot_map_not_empty[OF b_in] .
 next
   fix B
   assume b_in: "B \<in> Bot_F"
   show "\<G>_F B \<subseteq> Bot_G" using Bot_map[OF b_in] .
 next
   show "\<And>C. \<G>_F C \<inter> Bot_G \<noteq> {} \<longrightarrow> C \<in> Bot_F" using Bot_cond .
 next
   fix \<iota>
   assume i_in: "\<iota> \<in> Inf_F" and
     some_g: "\<G>_Inf \<iota> \<noteq> None"
   show "the (\<G>_Inf \<iota>) \<subseteq> Red_Inf_G (\<G>_F (concl_of \<iota>))"
   proof
     fix \<iota>G
     assume ig_in1: "\<iota>G \<in> the (\<G>_Inf \<iota>)"
     then have ig_in2: "\<iota>G \<in> Inf_G" using inf_map_in_Inf[OF i_in some_g] by blast
     show "\<iota>G \<in> Red_Inf_G (\<G>_F (concl_of \<iota>))"
       using strong_inf_map[OF i_in some_g] ground.Red_Inf_of_Inf_to_N[OF ig_in2]
         ig_in1 by blast
   qed
 qed
 
 end
 
 subsection \<open>Lifting with a Family of Well-founded Orderings\<close>
 
 locale lifting_with_wf_ordering_family =
   standard_lifting Bot_F Inf_F Bot_G Inf_G entails_G Red_Inf_G Red_F_G \<G>_F \<G>_Inf
   for
     Bot_F :: \<open>'f set\<close> and
     Inf_F :: \<open>'f inference set\<close> and
     Bot_G :: \<open>'g set\<close> and
     entails_G :: \<open>'g set \<Rightarrow> 'g set \<Rightarrow> bool\<close> (infix "\<Turnstile>G" 50) and
     Inf_G :: \<open>'g inference set\<close> and
     Red_Inf_G :: \<open>'g set \<Rightarrow> 'g inference set\<close> and
     Red_F_G :: \<open>'g set \<Rightarrow> 'g set\<close> and
     \<G>_F :: "'f \<Rightarrow> 'g set" and
     \<G>_Inf :: "'f inference \<Rightarrow> 'g inference set option"
   + fixes
     Prec_F_g :: \<open>'g \<Rightarrow> 'f \<Rightarrow> 'f \<Rightarrow> bool\<close>
   assumes
     all_wf: "minimal_element (Prec_F_g g) UNIV"
 begin
 
 definition Red_Inf_\<G> :: "'f set \<Rightarrow> 'f inference set" where
   \<open>Red_Inf_\<G> N = {\<iota> \<in> Inf_F. (\<G>_Inf \<iota> \<noteq> None \<and> the (\<G>_Inf \<iota>) \<subseteq> Red_Inf_G (\<G>_set N))
     \<or> (\<G>_Inf \<iota> = None \<and> \<G>_F (concl_of \<iota>) \<subseteq> \<G>_set N \<union> Red_F_G (\<G>_set N))}\<close>
 
 definition Red_F_\<G> :: "'f set \<Rightarrow> 'f set" where
   \<open>Red_F_\<G> N = {C. \<forall>D \<in> \<G>_F C. D \<in> Red_F_G (\<G>_set N) \<or> (\<exists>E \<in> N. Prec_F_g D E C \<and> D \<in> \<G>_F E)}\<close>
 
 lemma Prec_trans:
   assumes
     \<open>Prec_F_g D A B\<close> and
     \<open>Prec_F_g D B C\<close>
   shows
     \<open>Prec_F_g D A C\<close>
   using minimal_element.po assms unfolding po_on_def transp_on_def by (smt UNIV_I all_wf)
 
 lemma prop_nested_in_set: "D \<in> P C \<Longrightarrow> C \<in> {C. \<forall>D \<in> P C. A D \<or> B C D} \<Longrightarrow> A D \<or> B C D"
   by blast
 
 (* lem:wolog-C'-nonredundant *)
 lemma Red_F_\<G>_equiv_def:
   \<open>Red_F_\<G> N = {C. \<forall>Di \<in> \<G>_F C. Di \<in> Red_F_G (\<G>_set N) \<or>
     (\<exists>E \<in> (N - Red_F_\<G> N). Prec_F_g Di E C \<and> Di \<in> \<G>_F E)}\<close>
 proof (rule; clarsimp)
   fix C D
   assume
     C_in: \<open>C \<in> Red_F_\<G> N\<close> and
     D_in: \<open>D \<in> \<G>_F C\<close> and
     not_sec_case: \<open>\<forall>E \<in> N - Red_F_\<G> N. Prec_F_g D E C \<longrightarrow> D \<notin> \<G>_F E\<close>
   have C_in_unfolded: "C \<in> {C. \<forall>Di \<in> \<G>_F C. Di \<in> Red_F_G (\<G>_set N) \<or>
     (\<exists>E\<in>N. Prec_F_g Di E C \<and> Di \<in> \<G>_F E)}"
     using C_in unfolding Red_F_\<G>_def .
   have neg_not_sec_case: \<open>\<not> (\<exists>E\<in>N - Red_F_\<G> N. Prec_F_g D E C \<and> D \<in> \<G>_F E)\<close>
     using not_sec_case by clarsimp
   have unfol_C_D: \<open>D \<in> Red_F_G (\<G>_set N) \<or> (\<exists>E\<in>N. Prec_F_g D E C \<and> D \<in> \<G>_F E)\<close>
     using prop_nested_in_set[of D \<G>_F C "\<lambda>x. x \<in> Red_F_G (\<Union> (\<G>_F ` N))"
       "\<lambda>x y. \<exists>E \<in> N. Prec_F_g y E x \<and> y \<in> \<G>_F E", OF D_in C_in_unfolded] by blast
   show \<open>D \<in> Red_F_G (\<G>_set N)\<close>
   proof (rule ccontr)
     assume contrad: \<open>D \<notin> Red_F_G (\<G>_set N)\<close>
     have non_empty: \<open>\<exists>E\<in>N. Prec_F_g D E C \<and> D \<in> \<G>_F E\<close> using contrad unfol_C_D by auto
     define B where \<open>B = {E \<in> N. Prec_F_g D E C \<and> D \<in> \<G>_F E}\<close>
     then have B_non_empty: \<open>B \<noteq> {}\<close> using non_empty by auto
     interpret minimal_element "Prec_F_g D" UNIV using all_wf[of D] .
     obtain F :: 'f where F: \<open>F = min_elt B\<close> by auto
     then have D_in_F: \<open>D \<in> \<G>_F F\<close> unfolding B_def using non_empty
       by (smt Sup_UNIV Sup_upper UNIV_I contra_subsetD empty_iff empty_subsetI mem_Collect_eq
         min_elt_mem unfol_C_D)
     have F_prec: \<open>Prec_F_g D F C\<close> using F min_elt_mem[of B, OF _ B_non_empty] unfolding B_def by auto
     have F_not_in: \<open>F \<notin> Red_F_\<G> N\<close>
     proof
       assume F_in: \<open>F \<in> Red_F_\<G> N\<close>
       have unfol_F_D: \<open>D \<in> Red_F_G (\<G>_set N) \<or> (\<exists>G\<in>N. Prec_F_g D G F \<and> D \<in> \<G>_F G)\<close>
         using F_in D_in_F unfolding Red_F_\<G>_def by auto
       then have \<open>\<exists>G\<in>N. Prec_F_g D G F \<and> D \<in> \<G>_F G\<close> using contrad D_in unfolding Red_F_\<G>_def by auto
       then obtain G where G_in: \<open>G \<in> N\<close> and G_prec: \<open>Prec_F_g D G F\<close> and G_map: \<open>D \<in> \<G>_F G\<close> by auto
       have \<open>Prec_F_g D G C\<close> using G_prec F_prec Prec_trans by blast
       then have \<open>G \<in> B\<close> unfolding B_def using G_in G_map by auto
       then show \<open>False\<close> using F G_prec min_elt_minimal[of B G, OF _ B_non_empty] by auto
     qed
     have \<open>F \<in> N\<close> using F by (metis B_def B_non_empty mem_Collect_eq min_elt_mem top_greatest)
     then have \<open>F \<in> N - Red_F_\<G> N\<close> using F_not_in by auto
     then show \<open>False\<close>
       using D_in_F neg_not_sec_case F_prec by blast
   qed
 next
   fix C
   assume only_if: \<open>\<forall>D\<in>\<G>_F C. D \<in> Red_F_G (\<G>_set N) \<or> (\<exists>E\<in>N - Red_F_\<G> N. Prec_F_g D E C \<and> D \<in> \<G>_F E)\<close>
   show \<open>C \<in> Red_F_\<G> N\<close> unfolding Red_F_\<G>_def using only_if by auto
 qed
 
 (* lem:lifting-main-technical *)
 lemma not_red_map_in_map_not_red: \<open>\<G>_set N - Red_F_G (\<G>_set N) \<subseteq> \<G>_set (N - Red_F_\<G> N)\<close>
 proof
   fix D
   assume
     D_hyp: \<open>D \<in> \<G>_set N - Red_F_G (\<G>_set N)\<close>
   interpret minimal_element "Prec_F_g D" UNIV using all_wf[of D] .
   have D_in: \<open>D \<in> \<G>_set N\<close> using D_hyp by blast
   have  D_not_in: \<open>D \<notin> Red_F_G (\<G>_set N)\<close> using D_hyp by blast
   have exist_C: \<open>\<exists>C. C \<in> N \<and> D \<in> \<G>_F C\<close> using D_in by auto
   define B where \<open>B = {C \<in> N. D \<in> \<G>_F C}\<close>
   obtain C where C: \<open>C = min_elt B\<close> by auto
   have C_in_N: \<open>C \<in> N\<close>
     using exist_C by (metis B_def C empty_iff mem_Collect_eq min_elt_mem top_greatest)
   have D_in_C: \<open>D \<in> \<G>_F C\<close>
     using exist_C by (metis B_def C empty_iff mem_Collect_eq min_elt_mem top_greatest)
   have C_not_in: \<open>C \<notin> Red_F_\<G> N\<close>
   proof
     assume C_in: \<open>C \<in> Red_F_\<G> N\<close>
     have \<open>D \<in> Red_F_G (\<G>_set N) \<or> (\<exists>E\<in>N. Prec_F_g D E C \<and> D \<in> \<G>_F E)\<close>
       using C_in D_in_C unfolding Red_F_\<G>_def by auto
     then show \<open>False\<close>
       proof
         assume \<open>D \<in> Red_F_G (\<G>_set N)\<close>
         then show \<open>False\<close> using D_not_in by simp
       next
         assume \<open>\<exists>E\<in>N. Prec_F_g D E C \<and> D \<in> \<G>_F E\<close>
         then show \<open>False\<close>
           using C by (metis (no_types, lifting) B_def UNIV_I empty_iff mem_Collect_eq
               min_elt_minimal top_greatest)
       qed
   qed
   show \<open>D \<in> \<G>_set (N - Red_F_\<G> N)\<close> using D_in_C C_not_in C_in_N by blast
 qed
 
 (* lem:nonredundant-entails-redundant *)
 lemma Red_F_Bot_F: \<open>B \<in> Bot_F \<Longrightarrow> N \<Turnstile>\<G> {B} \<Longrightarrow> N - Red_F_\<G> N \<Turnstile>\<G> {B}\<close>
 proof -
   fix B N
   assume
     B_in: \<open>B \<in> Bot_F\<close> and
     N_entails: \<open>N \<Turnstile>\<G> {B}\<close>
   then have to_bot: \<open>\<G>_set N - Red_F_G (\<G>_set N) \<Turnstile>G \<G>_F B\<close>
     using ground.Red_F_Bot Bot_map
       by (smt cSup_singleton ground.entail_set_all_formulas image_insert image_is_empty subsetCE)
   have from_f: \<open>\<G>_set (N - Red_F_\<G> N) \<Turnstile>G \<G>_set N - Red_F_G (\<G>_set N)\<close>
     using ground.subset_entailed[OF not_red_map_in_map_not_red] by blast
   then have \<open>\<G>_set (N - Red_F_\<G> N) \<Turnstile>G \<G>_F B\<close> using to_bot ground.entails_trans by blast
   then show \<open>N - Red_F_\<G> N \<Turnstile>\<G> {B}\<close> using Bot_map by simp
 qed
 
 (* lem:redundancy-monotonic-addition 1/2 *)
 lemma Red_F_of_subset_F: \<open>N \<subseteq> N' \<Longrightarrow> Red_F_\<G> N \<subseteq> Red_F_\<G> N'\<close>
   using ground.Red_F_of_subset unfolding Red_F_\<G>_def by clarsimp (meson \<G>_subset subsetD)
 
 (* lem:redundancy-monotonic-addition 2/2 *)
 lemma Red_Inf_of_subset_F: \<open>N \<subseteq> N' \<Longrightarrow> Red_Inf_\<G> N \<subseteq> Red_Inf_\<G> N'\<close>
   using Collect_mono \<G>_subset subset_iff ground.Red_Inf_of_subset unfolding Red_Inf_\<G>_def
   by (smt ground.Red_F_of_subset Un_iff)
 
 (* lem:redundancy-monotonic-deletion-forms *)
 lemma Red_F_of_Red_F_subset_F: \<open>N' \<subseteq> Red_F_\<G> N \<Longrightarrow> Red_F_\<G> N \<subseteq> Red_F_\<G> (N - N')\<close>
 proof
   fix N N' C
   assume
     N'_in_Red_F_N: \<open>N' \<subseteq> Red_F_\<G> N\<close> and
     C_in_red_F_N: \<open>C \<in> Red_F_\<G> N\<close>
   have lem8: \<open>\<forall>D \<in> \<G>_F C. D \<in> Red_F_G (\<G>_set N) \<or> (\<exists>E \<in> (N - Red_F_\<G> N). Prec_F_g D E C \<and> D \<in> \<G>_F E)\<close>
     using Red_F_\<G>_equiv_def C_in_red_F_N by blast
   show \<open>C \<in> Red_F_\<G> (N - N')\<close> unfolding Red_F_\<G>_def
   proof (rule,rule)
     fix D
     assume \<open>D \<in> \<G>_F C\<close>
     then have \<open>D \<in> Red_F_G (\<G>_set N) \<or> (\<exists>E \<in> (N - Red_F_\<G> N). Prec_F_g D E C \<and> D \<in> \<G>_F E)\<close>
       using lem8 by auto
     then show \<open>D \<in> Red_F_G (\<G>_set (N - N')) \<or> (\<exists>E\<in>N - N'. Prec_F_g D E C \<and> D \<in> \<G>_F E)\<close>
     proof
       assume \<open>D \<in> Red_F_G (\<G>_set N)\<close>
       then have \<open>D \<in> Red_F_G (\<G>_set N - Red_F_G (\<G>_set N))\<close>
         using ground.Red_F_of_Red_F_subset[of "Red_F_G (\<G>_set N)" "\<G>_set N"] by auto
       then have \<open>D \<in> Red_F_G (\<G>_set (N - Red_F_\<G> N))\<close>
         using ground.Red_F_of_subset[OF not_red_map_in_map_not_red[of N]] by auto
       then have \<open>D \<in> Red_F_G (\<G>_set (N - N'))\<close>
         using N'_in_Red_F_N \<G>_subset[of "N - Red_F_\<G> N" "N - N'"]
         by (smt DiffE DiffI ground.Red_F_of_subset subsetCE subsetI)
       then show ?thesis by blast
     next
       assume \<open>\<exists>E\<in>N - Red_F_\<G> N. Prec_F_g D E C \<and> D \<in> \<G>_F E\<close>
       then obtain E where
         E_in: \<open>E\<in>N - Red_F_\<G> N\<close> and
         E_prec_C: \<open>Prec_F_g D E C\<close> and
         D_in: \<open>D \<in> \<G>_F E\<close>
         by auto
       have \<open>E \<in> N - N'\<close> using E_in N'_in_Red_F_N by blast
       then show ?thesis using E_prec_C D_in by blast
     qed
   qed
 qed
 
 (* lem:redundancy-monotonic-deletion-infs *)
 lemma Red_Inf_of_Red_F_subset_F: \<open>N' \<subseteq> Red_F_\<G> N \<Longrightarrow> Red_Inf_\<G> N \<subseteq> Red_Inf_\<G> (N - N') \<close>
 proof
   fix N N' \<iota>
   assume
     N'_in_Red_F_N: \<open>N' \<subseteq> Red_F_\<G> N\<close> and
     i_in_Red_Inf_N: \<open>\<iota> \<in> Red_Inf_\<G> N\<close>
   have i_in: \<open>\<iota> \<in> Inf_F\<close> using i_in_Red_Inf_N unfolding Red_Inf_\<G>_def by blast
   {
     assume not_none: "\<G>_Inf \<iota> \<noteq> None"
     have \<open>\<forall>\<iota>' \<in> the (\<G>_Inf \<iota>). \<iota>' \<in> Red_Inf_G (\<G>_set N)\<close>
       using not_none i_in_Red_Inf_N unfolding Red_Inf_\<G>_def by auto
     then have \<open>\<forall>\<iota>' \<in> the (\<G>_Inf \<iota>). \<iota>' \<in> Red_Inf_G (\<G>_set N - Red_F_G (\<G>_set N))\<close>
       using not_none ground.Red_Inf_of_Red_F_subset by blast
     then have ip_in_Red_Inf_G: \<open>\<forall>\<iota>' \<in> the (\<G>_Inf \<iota>). \<iota>' \<in> Red_Inf_G (\<G>_set (N - Red_F_\<G> N))\<close>
       using not_none ground.Red_Inf_of_subset[OF not_red_map_in_map_not_red[of N]] by auto
     then have not_none_in: \<open>\<forall>\<iota>' \<in> the (\<G>_Inf \<iota>). \<iota>' \<in> Red_Inf_G (\<G>_set (N - N'))\<close>
       using not_none N'_in_Red_F_N
       by (meson Diff_mono ground.Red_Inf_of_subset \<G>_subset subset_iff subset_refl)
     then have "the (\<G>_Inf \<iota>) \<subseteq> Red_Inf_G (\<G>_set (N - N'))" by blast
   }
   moreover {
     assume none: "\<G>_Inf \<iota> = None"
     have ground_concl_subs: "\<G>_F (concl_of \<iota>) \<subseteq> (\<G>_set N \<union> Red_F_G (\<G>_set N))"
       using none i_in_Red_Inf_N unfolding Red_Inf_\<G>_def by blast
     then have d_in_imp12: "D \<in> \<G>_F (concl_of \<iota>) \<Longrightarrow> D \<in> \<G>_set N - Red_F_G (\<G>_set N) \<or> D \<in> Red_F_G (\<G>_set N)"
       by blast
     have d_in_imp1: "D \<in> \<G>_set N - Red_F_G (\<G>_set N) \<Longrightarrow> D \<in> \<G>_set (N - N')"
       using not_red_map_in_map_not_red N'_in_Red_F_N by blast
     have d_in_imp_d_in: "D \<in> Red_F_G (\<G>_set N) \<Longrightarrow> D \<in> Red_F_G (\<G>_set N - Red_F_G (\<G>_set N))"
       using ground.Red_F_of_Red_F_subset[of "Red_F_G (\<G>_set N)" "\<G>_set N"] by blast
     have g_subs1: "\<G>_set N - Red_F_G (\<G>_set N) \<subseteq> \<G>_set (N - Red_F_\<G> N)"
       using not_red_map_in_map_not_red unfolding Red_F_\<G>_def by auto
     have g_subs2: "\<G>_set (N - Red_F_\<G> N) \<subseteq> \<G>_set (N - N')"
       using N'_in_Red_F_N by blast
     have d_in_imp2: "D \<in> Red_F_G (\<G>_set N) \<Longrightarrow> D \<in> Red_F_G (\<G>_set (N - N'))"
       using ground.Red_F_of_subset ground.Red_F_of_subset[OF g_subs1]
         ground.Red_F_of_subset[OF g_subs2] d_in_imp_d_in by blast
     have "\<G>_F (concl_of \<iota>) \<subseteq> (\<G>_set (N - N') \<union> Red_F_G (\<G>_set (N - N')))"
       using d_in_imp12 d_in_imp1 d_in_imp2
       by (smt ground.Red_F_of_Red_F_subset ground.Red_F_of_subset UnCI UnE Un_Diff_cancel2
         ground_concl_subs g_subs1 g_subs2 subset_iff)
   }
   ultimately show \<open>\<iota> \<in> Red_Inf_\<G> (N - N')\<close> using i_in unfolding Red_Inf_\<G>_def by auto
 qed
 
 (* lem:concl-contained-implies-red-inf *)
 lemma Red_Inf_of_Inf_to_N_F:
   assumes
     i_in: \<open>\<iota> \<in> Inf_F\<close> and
     concl_i_in: \<open>concl_of \<iota> \<in> N\<close>
   shows
     \<open>\<iota> \<in> Red_Inf_\<G> N \<close>
 proof -
   have \<open>\<iota> \<in> Inf_F \<Longrightarrow> \<G>_Inf \<iota> \<noteq> None \<Longrightarrow> the (\<G>_Inf \<iota>) \<subseteq> Red_Inf_G (\<G>_F (concl_of \<iota>))\<close> using inf_map by simp
   moreover have \<open>Red_Inf_G (\<G>_F (concl_of \<iota>)) \<subseteq> Red_Inf_G (\<G>_set N)\<close>
     using concl_i_in ground.Red_Inf_of_subset by blast
   moreover have "\<iota> \<in> Inf_F \<Longrightarrow> \<G>_Inf \<iota> = None \<Longrightarrow> concl_of \<iota> \<in> N \<Longrightarrow> \<G>_F (concl_of \<iota>) \<subseteq> \<G>_set N"
     by blast
   ultimately show ?thesis using i_in concl_i_in unfolding Red_Inf_\<G>_def by auto
 qed
 
 (* thm:FRedsqsubset-is-red-crit and also thm:lifted-red-crit if ordering empty *)
 sublocale calculus_with_red_crit Bot_F Inf_F entails_\<G> Red_Inf_\<G> Red_F_\<G>
 proof
   fix B N N' \<iota>
   show \<open>Red_Inf_\<G> N \<subseteq> Inf_F\<close> unfolding Red_Inf_\<G>_def by blast
   show \<open>B \<in> Bot_F \<Longrightarrow> N \<Turnstile>\<G> {B} \<Longrightarrow> N - Red_F_\<G> N \<Turnstile>\<G> {B}\<close> using Red_F_Bot_F by simp
   show \<open>N \<subseteq> N' \<Longrightarrow> Red_F_\<G> N \<subseteq> Red_F_\<G> N'\<close> using Red_F_of_subset_F by simp
   show \<open>N \<subseteq> N' \<Longrightarrow> Red_Inf_\<G> N \<subseteq> Red_Inf_\<G> N'\<close> using Red_Inf_of_subset_F by simp
   show \<open>N' \<subseteq> Red_F_\<G> N \<Longrightarrow> Red_F_\<G> N \<subseteq> Red_F_\<G> (N - N')\<close> using Red_F_of_Red_F_subset_F by simp
   show \<open>N' \<subseteq> Red_F_\<G> N \<Longrightarrow> Red_Inf_\<G> N \<subseteq> Red_Inf_\<G> (N - N')\<close> using Red_Inf_of_Red_F_subset_F by simp
   show \<open>\<iota> \<in> Inf_F \<Longrightarrow> concl_of \<iota> \<in> N \<Longrightarrow> \<iota> \<in> Red_Inf_\<G> N\<close> using Red_Inf_of_Inf_to_N_F by simp
 qed
 
 lemma grounded_inf_in_ground_inf: "\<iota> \<in> Inf_F \<Longrightarrow> \<G>_Inf \<iota> \<noteq> None \<Longrightarrow> the (\<G>_Inf \<iota>) \<subseteq> Inf_G"
   using inf_map ground.Red_Inf_to_Inf by blast
 
+abbreviation ground_Inf_redundant :: "'f set \<Rightarrow> bool" where
+  "ground_Inf_redundant N \<equiv>
+   ground.Inf_from (\<G>_set N)
+   \<subseteq> {\<iota>. \<exists>\<iota>'\<in> Inf_from N. \<G>_Inf \<iota>' \<noteq> None \<and> \<iota> \<in> the (\<G>_Inf \<iota>')} \<union> Red_Inf_G (\<G>_set N)"
+
+lemma sat_inf_imp_ground_red:
+  assumes
+    "saturated N" and
+    "\<iota>' \<in> Inf_from N" and
+    "\<G>_Inf \<iota>' \<noteq> None \<and> \<iota> \<in> the (\<G>_Inf \<iota>')"
+  shows "\<iota> \<in> Red_Inf_G (\<G>_set N)"
+  using assms Red_Inf_\<G>_def unfolding saturated_def by auto
+
 (* lem:sat-wrt-finf *)
-lemma sat_imp_ground_sat: "saturated N \<Longrightarrow> ground.Inf_from (\<G>_set N) \<subseteq>
-  ({\<iota>. \<exists>\<iota>'\<in> Inf_from N. \<G>_Inf \<iota>' \<noteq> None \<and> \<iota> \<in> the (\<G>_Inf \<iota>')} \<union> Red_Inf_G (\<G>_set N)) \<Longrightarrow>
-  ground.saturated (\<G>_set N)"
-proof -
-  fix N
-  assume
-    sat_n: "saturated N" and
-    inf_grounded_in: "ground.Inf_from (\<G>_set N) \<subseteq>
-    ({\<iota>. \<exists>\<iota>'\<in> Inf_from N. \<G>_Inf \<iota>' \<noteq> None \<and> \<iota> \<in> the (\<G>_Inf \<iota>')} \<union> Red_Inf_G (\<G>_set N))"
-  show "ground.saturated (\<G>_set N)" unfolding ground.saturated_def
-  proof
-    fix \<iota>
-    assume i_in: "\<iota> \<in> ground.Inf_from (\<G>_set N)"
-    {
-      assume "\<iota> \<in> {\<iota>. \<exists>\<iota>'\<in> Inf_from N. \<G>_Inf \<iota>' \<noteq> None \<and> \<iota> \<in> the (\<G>_Inf \<iota>')}"
-      then obtain \<iota>' where "\<iota>'\<in> Inf_from N" "\<G>_Inf \<iota>' \<noteq> None" "\<iota> \<in> the (\<G>_Inf \<iota>')" by blast
-      then have "\<iota> \<in> Red_Inf_G (\<G>_set N)"
-        using Red_Inf_\<G>_def sat_n unfolding saturated_def by auto
-    }
-    then show "\<iota> \<in> Red_Inf_G (\<G>_set N)" using inf_grounded_in i_in by blast
-  qed
-qed
+lemma sat_imp_ground_sat: "saturated N \<Longrightarrow> ground_Inf_redundant N \<Longrightarrow> ground.saturated (\<G>_set N)"
+  unfolding ground.saturated_def using sat_inf_imp_ground_red by auto
 
 (* thm:finf-complete *)
 theorem stat_ref_comp_to_non_ground:
   assumes
     stat_ref_G: "static_refutational_complete_calculus Bot_G Inf_G entails_G Red_Inf_G Red_F_G" and
-    sat_n_imp: "\<And>N. saturated N \<Longrightarrow> ground.Inf_from (\<G>_set N) \<subseteq>
-      {\<iota>. \<exists>\<iota>'\<in> Inf_from N. \<G>_Inf \<iota>' \<noteq> None \<and> \<iota> \<in> the (\<G>_Inf \<iota>')} \<union> Red_Inf_G (\<G>_set N)"
+    sat_n_imp: "\<And>N. saturated N \<Longrightarrow> ground_Inf_redundant N"
   shows
     "static_refutational_complete_calculus Bot_F Inf_F entails_\<G> Red_Inf_\<G> Red_F_\<G>"
 proof
   fix B N
   assume
     b_in: "B \<in> Bot_F" and
     sat_n: "saturated N" and
     n_entails_bot: "N \<Turnstile>\<G> {B}"
   have ground_n_entails: "\<G>_set N \<Turnstile>G \<G>_F B"
     using n_entails_bot by simp
   then obtain BG where bg_in1: "BG \<in> \<G>_F B"
     using Bot_map_not_empty[OF b_in] by blast
   then have bg_in: "BG \<in> Bot_G"
     using Bot_map[OF b_in] by blast
   have ground_n_entails_bot: "\<G>_set N \<Turnstile>G {BG}"
     using ground_n_entails bg_in1 ground.entail_set_all_formulas by blast
   have "ground.Inf_from (\<G>_set N) \<subseteq>
     {\<iota>. \<exists>\<iota>'\<in> Inf_from N. \<G>_Inf \<iota>' \<noteq> None \<and> \<iota> \<in> the (\<G>_Inf \<iota>')} \<union> Red_Inf_G (\<G>_set N)"
     using sat_n_imp[OF sat_n] .
   have "ground.saturated (\<G>_set N)"
     using sat_imp_ground_sat[OF sat_n sat_n_imp[OF sat_n]] .
   then have "\<exists>BG'\<in>Bot_G. BG' \<in> (\<G>_set N)"
     using stat_ref_G ground.calculus_with_red_crit_axioms bg_in ground_n_entails_bot
     unfolding static_refutational_complete_calculus_def static_refutational_complete_calculus_axioms_def
     by blast
   then show "\<exists>B'\<in> Bot_F. B' \<in> N"
     using bg_in Bot_cond Bot_map_not_empty Bot_cond by blast
 qed
 
 end
 
 lemma wf_empty_rel: "minimal_element (\<lambda>_ _. False) UNIV"
   by (simp add: minimal_element.intro po_on_def transp_onI wfp_on_imp_irreflp_on)
 
 lemma any_to_empty_order_lifting:
   "lifting_with_wf_ordering_family Bot_F Inf_F Bot_G entails_G Inf_G Red_Inf_G Red_F_G \<G>_F
     \<G>_Inf Prec_F_g \<Longrightarrow> lifting_with_wf_ordering_family Bot_F Inf_F Bot_G entails_G Inf_G Red_Inf_G
     Red_F_G \<G>_F \<G>_Inf (\<lambda>g C C'. False)"
 proof -
   fix Bot_F Inf_F Bot_G entails_G Inf_G Red_Inf_G Red_F_G \<G>_F \<G>_Inf Prec_F_g
   assume lift: "lifting_with_wf_ordering_family Bot_F Inf_F Bot_G entails_G Inf_G Red_Inf_G
     Red_F_G \<G>_F \<G>_Inf Prec_F_g"
   then interpret lift_g:
     lifting_with_wf_ordering_family Bot_F Inf_F Bot_G entails_G Inf_G Red_Inf_G Red_F_G \<G>_F
       \<G>_Inf Prec_F_g
     by auto
   show "lifting_with_wf_ordering_family Bot_F Inf_F Bot_G entails_G Inf_G Red_Inf_G Red_F_G
     \<G>_F \<G>_Inf (\<lambda>g C C'. False)"
     by (simp add: wf_empty_rel lift_g.standard_lifting_axioms
       lifting_with_wf_ordering_family_axioms.intro lifting_with_wf_ordering_family_def)
 qed
 
 locale lifting_equivalence_with_empty_order =
   any_order_lifting: lifting_with_wf_ordering_family Bot_F Inf_F Bot_G entails_G Inf_G Red_Inf_G
     Red_F_G \<G>_F \<G>_Inf Prec_F_g +
   empty_order_lifting: lifting_with_wf_ordering_family Bot_F Inf_F Bot_G entails_G Inf_G Red_Inf_G
     Red_F_G \<G>_F \<G>_Inf "\<lambda>g C C'. False"
   for
     \<G>_F :: \<open>'f \<Rightarrow> 'g set\<close> and
     \<G>_Inf :: \<open>'f inference \<Rightarrow> 'g inference set option\<close> and
     Bot_F :: \<open>'f set\<close> and
     Inf_F :: \<open>'f inference set\<close> and
     Bot_G :: \<open>'g set\<close> and
     Inf_G :: \<open>'g inference set\<close> and
     entails_G :: \<open>'g set \<Rightarrow> 'g set \<Rightarrow> bool\<close> (infix "\<Turnstile>G" 50) and
     Red_Inf_G :: \<open>'g set \<Rightarrow> 'g inference set\<close> and
     Red_F_G :: \<open>'g set \<Rightarrow> 'g set\<close> and
     Prec_F_g :: \<open>'g \<Rightarrow> 'f \<Rightarrow> 'f \<Rightarrow> bool\<close>
 
 sublocale lifting_with_wf_ordering_family \<subseteq> lifting_equivalence_with_empty_order
 proof
   show "po_on (\<lambda>C C'. False) UNIV"
     unfolding po_on_def by (simp add: transp_onI wfp_on_imp_irreflp_on)
   show "wfp_on (\<lambda>C C'. False) UNIV"
     unfolding wfp_on_def by simp
 qed
 
 context lifting_equivalence_with_empty_order
 begin
 
 (* lem:saturation-indep-of-sqsubset *)
 lemma saturated_empty_order_equiv_saturated:
   "any_order_lifting.saturated N = empty_order_lifting.saturated N"
   by (rule refl)
 
 (* lem:static-ref-compl-indep-of-sqsubset *)
 lemma static_empty_order_equiv_static:
   "static_refutational_complete_calculus Bot_F Inf_F any_order_lifting.entails_\<G>
      empty_order_lifting.Red_Inf_\<G> empty_order_lifting.Red_F_\<G> =
    static_refutational_complete_calculus Bot_F Inf_F any_order_lifting.entails_\<G>
      any_order_lifting.Red_Inf_\<G> any_order_lifting.Red_F_\<G>"
   unfolding static_refutational_complete_calculus_def
   by (rule iffI) (standard,(standard)[],simp)+
 
 (* thm:FRedsqsubset-is-dyn-ref-compl *)
 theorem static_to_dynamic:
   "static_refutational_complete_calculus Bot_F Inf_F
     any_order_lifting.entails_\<G> empty_order_lifting.Red_Inf_\<G> empty_order_lifting.Red_F_\<G> =
     dynamic_refutational_complete_calculus Bot_F Inf_F
     any_order_lifting.entails_\<G> any_order_lifting.Red_Inf_\<G> any_order_lifting.Red_F_\<G> "
   using any_order_lifting.dyn_equiv_stat static_empty_order_equiv_static by blast
 
 end
 
 subsection \<open>Lifting with a Family of Redundancy Criteria\<close>
 
 locale standard_lifting_with_red_crit_family = inference_system Inf_F
   + ground: calculus_family_with_red_crit_family Bot_G Q Inf_G_q entails_q Red_Inf_q Red_F_q
   for
     Inf_F :: "'f inference set" and
     Bot_G :: "'g set" and
     Q :: "'q set" and
     Inf_G_q :: \<open>'q \<Rightarrow> 'g inference set\<close> and
     entails_q :: "'q \<Rightarrow> 'g set \<Rightarrow> 'g set \<Rightarrow> bool" and
     Red_Inf_q :: "'q \<Rightarrow> 'g set \<Rightarrow> 'g inference set" and
     Red_F_q :: "'q \<Rightarrow> 'g set \<Rightarrow> 'g set"
   + fixes
     Bot_F :: "'f set" and
     \<G>_F_q :: "'q \<Rightarrow> 'f \<Rightarrow> 'g set" and
     \<G>_Inf_q :: "'q \<Rightarrow> 'f inference \<Rightarrow> 'g inference set option" and
     Prec_F_g :: "'g \<Rightarrow> 'f \<Rightarrow> 'f \<Rightarrow> bool"
   assumes
     standard_lifting_family:
       "\<forall>q \<in> Q. lifting_with_wf_ordering_family Bot_F Inf_F Bot_G (entails_q q) (Inf_G_q q)
          (Red_Inf_q q) (Red_F_q q) (\<G>_F_q q) (\<G>_Inf_q q) Prec_F_g"
 begin
 
 abbreviation \<G>_set_q :: "'q \<Rightarrow> 'f set \<Rightarrow> 'g set" where
   "\<G>_set_q q N \<equiv> \<Union> (\<G>_F_q q ` N)"
 
 definition Red_Inf_\<G>_q :: "'q \<Rightarrow> 'f set \<Rightarrow> 'f inference set" where
   "Red_Inf_\<G>_q q N = {\<iota> \<in> Inf_F. (\<G>_Inf_q q \<iota> \<noteq> None \<and> the (\<G>_Inf_q q \<iota>) \<subseteq> Red_Inf_q q (\<G>_set_q q N))
    \<or> (\<G>_Inf_q q \<iota> = None \<and> \<G>_F_q q (concl_of \<iota>) \<subseteq> (\<G>_set_q q N \<union> Red_F_q q (\<G>_set_q q N)))}"
 
 definition Red_F_\<G>_empty_q :: "'q \<Rightarrow> 'f set \<Rightarrow> 'f set" where
   "Red_F_\<G>_empty_q q N = {C. \<forall>D \<in> \<G>_F_q q C. D \<in> Red_F_q q (\<G>_set_q q N)}"
 
 definition Red_F_\<G>_q_g :: "'q \<Rightarrow> 'f set \<Rightarrow> 'f set" where
   "Red_F_\<G>_q_g q N =
    {C. \<forall>D \<in> \<G>_F_q q C. D \<in> Red_F_q q (\<G>_set_q q N) \<or> (\<exists>E \<in> N. Prec_F_g D E C \<and> D \<in> \<G>_F_q q E)}"
 
 abbreviation entails_\<G>_q :: "'q \<Rightarrow> 'f set \<Rightarrow> 'f set \<Rightarrow> bool" where
   "entails_\<G>_q q N1 N2 \<equiv> entails_q q (\<G>_set_q q N1) (\<G>_set_q q N2)"
 
 lemma red_crit_lifting_family:
   assumes q_in: "q \<in> Q"
   shows "calculus_with_red_crit Bot_F Inf_F (entails_\<G>_q q) (Red_Inf_\<G>_q q) (Red_F_\<G>_q_g q)"
 proof -
   interpret wf_lift:
     lifting_with_wf_ordering_family Bot_F Inf_F Bot_G "entails_q q" "Inf_G_q q" "Red_Inf_q q"
       "Red_F_q q" "\<G>_F_q q" "\<G>_Inf_q q" Prec_F_g
     using standard_lifting_family q_in by metis
   have "Red_Inf_\<G>_q q = wf_lift.Red_Inf_\<G>"
     unfolding Red_Inf_\<G>_q_def wf_lift.Red_Inf_\<G>_def by blast
   moreover have "Red_F_\<G>_q_g q = wf_lift.Red_F_\<G>"
     unfolding Red_F_\<G>_q_g_def wf_lift.Red_F_\<G>_def by blast
   ultimately show ?thesis
     using wf_lift.calculus_with_red_crit_axioms by simp
 qed
 
 lemma red_crit_lifting_family_empty_ord:
   assumes q_in: "q \<in> Q"
   shows "calculus_with_red_crit Bot_F Inf_F (entails_\<G>_q q) (Red_Inf_\<G>_q q) (Red_F_\<G>_empty_q q)"
 proof -
   interpret wf_lift:
     lifting_with_wf_ordering_family Bot_F Inf_F Bot_G "entails_q q" "Inf_G_q q" "Red_Inf_q q"
       "Red_F_q q" "\<G>_F_q q" "\<G>_Inf_q q" Prec_F_g
     using standard_lifting_family q_in by metis
   have "Red_Inf_\<G>_q q = wf_lift.Red_Inf_\<G>"
     unfolding Red_Inf_\<G>_q_def wf_lift.Red_Inf_\<G>_def by blast
   moreover have "Red_F_\<G>_empty_q q = wf_lift.empty_order_lifting.Red_F_\<G>"
     unfolding Red_F_\<G>_empty_q_def wf_lift.empty_order_lifting.Red_F_\<G>_def by blast
   ultimately show ?thesis
     using wf_lift.empty_order_lifting.calculus_with_red_crit_axioms by simp
 qed
 
 sublocale consequence_relation_family Bot_F Q entails_\<G>_q
 proof (unfold_locales; (intro ballI)?)
   show "Q \<noteq> {}"
     by (rule ground.Q_nonempty)
 next
   fix qi
   assume qi_in: "qi \<in> Q"
 
   interpret lift: lifting_with_wf_ordering_family Bot_F Inf_F Bot_G "entails_q qi" "Inf_G_q qi"
     "Red_Inf_q qi" "Red_F_q qi" "\<G>_F_q qi" "\<G>_Inf_q qi" Prec_F_g
     using qi_in by (metis standard_lifting_family)
 
   show "consequence_relation Bot_F (entails_\<G>_q qi)"
     by unfold_locales
 qed
 
 sublocale calculus_with_red_crit_family Bot_F Inf_F Q entails_\<G>_q Red_Inf_\<G>_q Red_F_\<G>_q_g
   by unfold_locales (auto simp: Q_nonempty red_crit_lifting_family)
 
 abbreviation entails_\<G>_Q :: "'f set \<Rightarrow> 'f set \<Rightarrow> bool" (infix "\<Turnstile>\<inter>\<G>" 50) where
   "(\<Turnstile>\<inter>\<G>) \<equiv> entails_Q"
 
 abbreviation Red_Inf_\<G>_Q :: "'f set \<Rightarrow> 'f inference set" where
   "Red_Inf_\<G>_Q \<equiv> Red_Inf_Q"
 
 abbreviation Red_F_\<G>_Q :: "'f set \<Rightarrow> 'f set" where
   "Red_F_\<G>_Q \<equiv> Red_F_Q"
 
 lemmas entails_\<G>_Q_def = entails_Q_def
 lemmas Red_Inf_\<G>_Q_def = Red_Inf_Q_def
 lemmas Red_F_\<G>_Q_def = Red_F_Q_def
 
 sublocale empty_ord: calculus_with_red_crit_family Bot_F Inf_F Q entails_\<G>_q Red_Inf_\<G>_q
   Red_F_\<G>_empty_q
   by unfold_locales (auto simp: Q_nonempty red_crit_lifting_family_empty_ord)
 
 abbreviation Red_F_\<G>_empty :: "'f set \<Rightarrow> 'f set" where
   "Red_F_\<G>_empty \<equiv> empty_ord.Red_F_Q"
 
 lemmas Red_F_\<G>_empty_def = empty_ord.Red_F_Q_def
 
+lemma sat_inf_imp_ground_red_fam_inter:
+  assumes
+    sat_n: "saturated N" and
+    i'_in: "\<iota>' \<in> Inf_from N" and
+    q_in: "q \<in> Q" and
+    grounding: "\<G>_Inf_q q \<iota>' \<noteq> None \<and> \<iota> \<in> the (\<G>_Inf_q q \<iota>')"
+  shows "\<iota> \<in> Red_Inf_q q (\<G>_set_q q N)"
+proof -
+  have "\<iota>' \<in> Red_Inf_\<G>_q q N"
+    using sat_n i'_in q_in all_red_crit calculus_with_red_crit.saturated_def sat_int_to_sat_q
+    by blast
+  then have "the (\<G>_Inf_q q \<iota>') \<subseteq> Red_Inf_q q (\<G>_set_q q N)"
+    by (simp add: Red_Inf_\<G>_q_def grounding)
+  then show ?thesis
+    using grounding by blast
+qed
+
+abbreviation ground_Inf_redundant :: "'q \<Rightarrow> 'f set \<Rightarrow> bool" where
+  "ground_Inf_redundant q N \<equiv>
+   ground.Inf_from_q q (\<G>_set_q q N)
+   \<subseteq> {\<iota>. \<exists>\<iota>'\<in> Inf_from N. \<G>_Inf_q q \<iota>' \<noteq> None \<and> \<iota> \<in> the (\<G>_Inf_q q \<iota>')} \<union> Red_Inf_q q (\<G>_set_q q N)"
+
+abbreviation ground_saturated :: "'q \<Rightarrow> 'f set \<Rightarrow> bool" where
+  "ground_saturated q N \<equiv> ground.Inf_from_q q (\<G>_set_q q N) \<subseteq> Red_Inf_q q (\<G>_set_q q N)"
+
+lemma sat_imp_ground_sat_fam_inter:
+  "saturated N \<Longrightarrow> q \<in> Q \<Longrightarrow> ground_Inf_redundant q N \<Longrightarrow> ground_saturated q N"
+  using sat_inf_imp_ground_red_fam_inter by auto
+
 (* thm:intersect-finf-complete *)
 theorem stat_ref_comp_to_non_ground_fam_inter:
   assumes
     stat_ref_G:
       "\<forall>q \<in> Q. static_refutational_complete_calculus Bot_G (Inf_G_q q) (entails_q q) (Red_Inf_q q)
         (Red_F_q q)" and
-    sat_n_imp:
-      "\<And>N. saturated N \<Longrightarrow>
-         \<exists>q \<in> Q. ground.Inf_from_q q (\<G>_set_q q N) \<subseteq>
-           {\<iota>. \<exists>\<iota>'\<in> Inf_from N. \<G>_Inf_q q \<iota>' \<noteq> None \<and> \<iota> \<in> the (\<G>_Inf_q q \<iota>')}
-           \<union> Red_Inf_q q (\<G>_set_q q N)"
+    sat_n_imp: "\<And>N. saturated N \<Longrightarrow> \<exists>q \<in> Q. ground_Inf_redundant q N"
   shows
     "static_refutational_complete_calculus Bot_F Inf_F entails_\<G>_Q Red_Inf_\<G>_Q Red_F_\<G>_empty"
     using empty_ord.calculus_with_red_crit_axioms unfolding static_refutational_complete_calculus_def
       static_refutational_complete_calculus_axioms_def
 proof (standard, clarify)
   fix B N
   assume
     b_in: "B \<in> Bot_F" and
     sat_n: "saturated N" and
     entails_bot: "N \<Turnstile>\<inter>\<G> {B}"
   then obtain q where
     q_in: "q \<in> Q" and
     inf_subs: "ground.Inf_from_q q (\<G>_set_q q N) \<subseteq>
       {\<iota>. \<exists>\<iota>'\<in> Inf_from N. \<G>_Inf_q q \<iota>' \<noteq> None \<and> \<iota> \<in> the (\<G>_Inf_q q \<iota>')}
       \<union> Red_Inf_q q (\<G>_set_q q N)"
     using sat_n_imp[of N] by blast
   interpret q_calc: calculus_with_red_crit Bot_F Inf_F "entails_\<G>_q q" "Red_Inf_\<G>_q q" "Red_F_\<G>_q_g q"
     using all_red_crit[rule_format, OF q_in] .
   have n_q_sat: "q_calc.saturated N"
     using q_in sat_int_to_sat_q sat_n by simp
   interpret lifted_q_calc:
     lifting_with_wf_ordering_family Bot_F Inf_F Bot_G "entails_q q" "Inf_G_q q" "Red_Inf_q q"
       "Red_F_q q" "\<G>_F_q q" "\<G>_Inf_q q"
     using q_in by (simp add: standard_lifting_family)
   have n_lift_sat: "lifted_q_calc.empty_order_lifting.saturated N"
     using n_q_sat unfolding Red_Inf_\<G>_q_def lifted_q_calc.empty_order_lifting.Red_Inf_\<G>_def
       lifted_q_calc.saturated_def q_calc.saturated_def by auto
   have ground_sat_n: "lifted_q_calc.ground.saturated (\<G>_set_q q N)"
     by (rule lifted_q_calc.sat_imp_ground_sat[OF n_lift_sat])
       (use n_lift_sat inf_subs ground.Inf_from_q_def in auto)
   have ground_n_entails_bot: "entails_\<G>_q q N {B}"
     using q_in entails_bot unfolding entails_\<G>_Q_def by simp
   interpret static_refutational_complete_calculus Bot_G "Inf_G_q q" "entails_q q" "Red_Inf_q q"
     "Red_F_q q"
     using stat_ref_G[rule_format, OF q_in] .
   obtain BG where bg_in: "BG \<in> \<G>_F_q q B"
     using lifted_q_calc.Bot_map_not_empty[OF b_in] by blast
   then have "BG \<in> Bot_G" using lifted_q_calc.Bot_map[OF b_in] by blast
   then have "\<exists>BG'\<in>Bot_G. BG' \<in> \<G>_set_q q N"
     using ground_sat_n ground_n_entails_bot static_refutational_complete[of BG, OF _ ground_sat_n]
       bg_in lifted_q_calc.ground.entail_set_all_formulas[of "\<G>_set_q q N" "\<G>_set_q q {B}"]
     by simp
   then show "\<exists>B'\<in> Bot_F. B' \<in> N" using lifted_q_calc.Bot_cond by blast
 qed
 
 (* lem:intersect-saturation-indep-of-sqsubset *)
 lemma sat_eq_sat_empty_order: "saturated N = empty_ord.saturated N"
   by (rule refl)
 
 (* lem:intersect-static-ref-compl-indep-of-sqsubset *)
 lemma static_empty_ord_inter_equiv_static_inter:
   "static_refutational_complete_calculus Bot_F Inf_F entails_Q Red_Inf_Q Red_F_Q =
   static_refutational_complete_calculus Bot_F Inf_F entails_Q Red_Inf_Q Red_F_\<G>_empty"
   unfolding static_refutational_complete_calculus_def
   by (simp add: empty_ord.calculus_with_red_crit_axioms calculus_with_red_crit_axioms)
 
 (* thm:intersect-static-ref-compl-is-dyn-ref-compl-with-order *)
 theorem stat_eq_dyn_ref_comp_fam_inter: "static_refutational_complete_calculus Bot_F Inf_F
     entails_Q Red_Inf_Q Red_F_\<G>_empty =
   dynamic_refutational_complete_calculus Bot_F Inf_F entails_Q Red_Inf_Q Red_F_Q"
   using dyn_equiv_stat static_empty_ord_inter_equiv_static_inter by blast
 
 end
 
 end