diff --git a/thys/Lambda_Free_RPOs/Extension_Orders.thy b/thys/Lambda_Free_RPOs/Extension_Orders.thy
--- a/thys/Lambda_Free_RPOs/Extension_Orders.thy
+++ b/thys/Lambda_Free_RPOs/Extension_Orders.thy
@@ -1,2071 +1,2056 @@
 (*  Title:       Extension Orders
     Author:      Heiko Becker <heikobecker92@gmail.com>, 2016
     Author:      Jasmin Blanchette <jasmin.blanchette at inria.fr>, 2016
     Author:      Dmitriy Traytel <traytel@inf.ethz.ch>, 2014
     Maintainer:  Jasmin Blanchette <jasmin.blanchette at inria.fr>
 *)
 
 section \<open>Extension Orders\<close>
 
 theory Extension_Orders
 imports Lambda_Free_Util Infinite_Chain "HOL-Cardinals.Wellorder_Extension"
 begin
 
 text \<open>
 This theory defines locales for categorizing extension orders used for orders on
 \<open>\<lambda>\<close>-free higher-order terms and defines variants of the lexicographic and
 multiset orders.
 \<close>
 
 
 subsection \<open>Locales\<close>
 
 locale ext =
   fixes ext :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   assumes
     mono_strong: "(\<forall>y \<in> set ys. \<forall>x \<in> set xs. gt y x \<longrightarrow> gt' y x) \<Longrightarrow> ext gt ys xs \<Longrightarrow> ext gt' ys xs" and
     map: "finite A \<Longrightarrow> ys \<in> lists A \<Longrightarrow> xs \<in> lists A \<Longrightarrow> (\<forall>x \<in> A. \<not> gt (f x) (f x)) \<Longrightarrow>
       (\<forall>z \<in> A. \<forall>y \<in> A. \<forall>x \<in> A. gt (f z) (f y) \<longrightarrow> gt (f y) (f x) \<longrightarrow> gt (f z) (f x)) \<Longrightarrow>
       (\<forall>y \<in> A. \<forall>x \<in> A. gt y x \<longrightarrow> gt (f y) (f x)) \<Longrightarrow> ext gt ys xs \<Longrightarrow> ext gt (map f ys) (map f xs)"
 begin
 
 lemma mono[mono]: "gt \<le> gt' \<Longrightarrow> ext gt \<le> ext gt'"
   using mono_strong by blast
 
 end
 
 locale ext_irrefl = ext +
   assumes irrefl: "(\<forall>x \<in> set xs. \<not> gt x x) \<Longrightarrow> \<not> ext gt xs xs"
 
 locale ext_trans = ext +
   assumes trans: "zs \<in> lists A \<Longrightarrow> ys \<in> lists A \<Longrightarrow> xs \<in> lists A \<Longrightarrow>
     (\<forall>z \<in> A. \<forall>y \<in> A. \<forall>x \<in> A. gt z y \<longrightarrow> gt y x \<longrightarrow> gt z x) \<Longrightarrow> ext gt zs ys \<Longrightarrow> ext gt ys xs \<Longrightarrow>
     ext gt zs xs"
 
 locale ext_irrefl_before_trans = ext_irrefl +
   assumes trans_from_irrefl: "finite A \<Longrightarrow> zs \<in> lists A \<Longrightarrow> ys \<in> lists A \<Longrightarrow> xs \<in> lists A \<Longrightarrow>
     (\<forall>x \<in> A. \<not> gt x x) \<Longrightarrow> (\<forall>z \<in> A. \<forall>y \<in> A. \<forall>x \<in> A. gt z y \<longrightarrow> gt y x \<longrightarrow> gt z x) \<Longrightarrow> ext gt zs ys \<Longrightarrow>
     ext gt ys xs \<Longrightarrow> ext gt zs xs"
 
 locale ext_trans_before_irrefl = ext_trans +
   assumes irrefl_from_trans: "(\<forall>z \<in> set xs. \<forall>y \<in> set xs. \<forall>x \<in> set xs. gt z y \<longrightarrow> gt y x \<longrightarrow> gt z x) \<Longrightarrow>
     (\<forall>x \<in> set xs. \<not> gt x x) \<Longrightarrow> \<not> ext gt xs xs"
 
 locale ext_irrefl_trans_strong = ext_irrefl +
   assumes trans_strong: "(\<forall>z \<in> set zs. \<forall>y \<in> set ys. \<forall>x \<in> set xs. gt z y \<longrightarrow> gt y x \<longrightarrow> gt z x) \<Longrightarrow>
     ext gt zs ys \<Longrightarrow> ext gt ys xs \<Longrightarrow> ext gt zs xs"
 
 sublocale ext_irrefl_trans_strong < ext_irrefl_before_trans
   by standard (erule irrefl, metis in_listsD trans_strong)
 
 sublocale ext_irrefl_trans_strong < ext_trans
   by standard (metis in_listsD trans_strong)
 
 sublocale ext_irrefl_trans_strong < ext_trans_before_irrefl
   by standard (rule irrefl)
 
 locale ext_snoc = ext +
   assumes snoc: "ext gt (xs @ [x]) xs"
 
 locale ext_compat_cons = ext +
   assumes compat_cons: "ext gt ys xs \<Longrightarrow> ext gt (x # ys) (x # xs)"
 begin
 
 lemma compat_append_left: "ext gt ys xs \<Longrightarrow> ext gt (zs @ ys) (zs @ xs)"
   by (induct zs) (auto intro: compat_cons)
 
 end
 
 locale ext_compat_snoc = ext +
   assumes compat_snoc: "ext gt ys xs \<Longrightarrow> ext gt (ys @ [x]) (xs @ [x])"
 begin
 
 lemma compat_append_right: "ext gt ys xs \<Longrightarrow> ext gt (ys @ zs) (xs @ zs)"
   by (induct zs arbitrary: xs ys rule: rev_induct)
     (auto intro: compat_snoc simp del: append_assoc simp: append_assoc[symmetric])
 
 end
 
 locale ext_compat_list = ext +
   assumes compat_list: "y \<noteq> x \<Longrightarrow> gt y x \<Longrightarrow> ext gt (xs @ y # xs') (xs @ x # xs')"
 
 locale ext_singleton = ext +
   assumes singleton: "y \<noteq> x \<Longrightarrow> ext gt [y] [x] \<longleftrightarrow> gt y x"
 
 locale ext_compat_list_strong = ext_compat_cons + ext_compat_snoc + ext_singleton
 begin
 
 lemma compat_list: "y \<noteq> x \<Longrightarrow> gt y x \<Longrightarrow> ext gt (xs @ y # xs') (xs @ x # xs')"
   using compat_append_left[of gt "y # xs'" "x # xs'" xs]
     compat_append_right[of gt, of "[y]" "[x]" xs'] singleton[of y x gt]
   by fastforce
 
 end
 
 sublocale ext_compat_list_strong < ext_compat_list
   by standard (fact compat_list)
 
 locale ext_total = ext +
   assumes total: "(\<forall>y \<in> A. \<forall>x \<in> A. gt y x \<or> gt x y \<or> y = x) \<Longrightarrow> ys \<in> lists A \<Longrightarrow> xs \<in> lists A \<Longrightarrow>
     ext gt ys xs \<or> ext gt xs ys \<or> ys = xs"
 
 locale ext_wf = ext +
   assumes wf: "wfP (\<lambda>x y. gt y x) \<Longrightarrow> wfP (\<lambda>xs ys. ext gt ys xs)"
 
 locale ext_hd_or_tl = ext +
   assumes hd_or_tl: "(\<forall>z y x. gt z y \<longrightarrow> gt y x \<longrightarrow> gt z x) \<Longrightarrow> (\<forall>y x. gt y x \<or> gt x y \<or> y = x) \<Longrightarrow>
     length ys = length xs \<Longrightarrow> ext gt (y # ys) (x # xs) \<Longrightarrow> gt y x \<or> ext gt ys xs"
 
 locale ext_wf_bounded = ext_irrefl_before_trans + ext_hd_or_tl
 begin
 
 context
   fixes gt :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   assumes
     gt_irrefl: "\<And>z. \<not> gt z z" and
     gt_trans: "\<And>z y x. gt z y \<Longrightarrow> gt y x \<Longrightarrow> gt z x" and
     gt_total: "\<And>y x. gt y x \<or> gt x y \<or> y = x" and
     gt_wf: "wfP (\<lambda>x y. gt y x)"
 begin
 
 lemma irrefl_gt: "\<not> ext gt xs xs"
   using irrefl gt_irrefl by simp
 
 lemma trans_gt: "ext gt zs ys \<Longrightarrow> ext gt ys xs \<Longrightarrow> ext gt zs xs"
   by (rule trans_from_irrefl[of "set zs \<union> set ys \<union> set xs" zs ys xs gt])
     (auto intro: gt_trans simp: gt_irrefl)
 
 lemma hd_or_tl_gt: "length ys = length xs \<Longrightarrow> ext gt (y # ys) (x # xs) \<Longrightarrow> gt y x \<or> ext gt ys xs"
   by (rule hd_or_tl) (auto intro: gt_trans simp: gt_total)
 
 lemma wf_same_length_if_total: "wfP (\<lambda>xs ys. length ys = n \<and> length xs = n \<and> ext gt ys xs)"
 proof (induct n)
   case 0
   thus ?case
     unfolding wfP_def wf_def using irrefl by auto
 next
   case (Suc n)
   note ih = this(1)
 
   define gt_hd where "\<And>ys xs. gt_hd ys xs \<longleftrightarrow> gt (hd ys) (hd xs)"
   define gt_tl where "\<And>ys xs. gt_tl ys xs \<longleftrightarrow> ext gt (tl ys) (tl xs)"
 
   have hd_tl: "gt_hd ys xs \<or> gt_tl ys xs"
     if len_ys: "length ys = Suc n" and len_xs: "length xs = Suc n" and ys_gt_xs: "ext gt ys xs"
     for n ys xs
     using len_ys len_xs ys_gt_xs unfolding gt_hd_def gt_tl_def
     by (cases xs; cases ys) (auto simp: hd_or_tl_gt)
 
   show ?case
     unfolding wfP_iff_no_inf_chain
   proof (intro notI)
     let ?gtsn = "\<lambda>ys xs. length ys = n \<and> length xs = n \<and> ext gt ys xs"
     let ?gtsSn = "\<lambda>ys xs. length ys = Suc n \<and> length xs = Suc n \<and> ext gt ys xs"
     let ?gttlSn = "\<lambda>ys xs. length ys = Suc n \<and> length xs = Suc n \<and> gt_tl ys xs"
 
     assume "\<exists>f. inf_chain ?gtsSn f"
     then obtain xs where xs_bad: "bad ?gtsSn xs"
       unfolding inf_chain_def bad_def by blast
 
     let ?ff = "worst_chain ?gtsSn gt_hd"
 
     have wf_hd: "wf {(xs, ys). gt_hd ys xs}"
       unfolding gt_hd_def by (rule wfP_app[OF gt_wf, of hd, unfolded wfP_def])
 
     have "inf_chain ?gtsSn ?ff"
       by (rule worst_chain_bad[OF wf_hd xs_bad])
     moreover have "\<not> gt_hd (?ff i) (?ff (Suc i))" for i
       by (rule worst_chain_not_gt[OF wf_hd xs_bad]) (blast intro: trans_gt)
     ultimately have tl_bad: "inf_chain ?gttlSn ?ff"
       unfolding inf_chain_def using hd_tl by blast
 
     have "\<not> inf_chain ?gtsn (tl \<circ> ?ff)"
       using wfP_iff_no_inf_chain[THEN iffD1, OF ih] by blast
     hence tl_good: "\<not> inf_chain ?gttlSn ?ff"
       unfolding inf_chain_def gt_tl_def by force
 
     show False
       using tl_bad tl_good by sat
   qed
 qed
 
 lemma wf_bounded_if_total: "wfP (\<lambda>xs ys. length ys \<le> n \<and> length xs \<le> n \<and> ext gt ys xs)"
   unfolding wfP_iff_no_inf_chain
 proof (intro notI, induct n rule: less_induct)
   case (less n)
   note ih = this(1) and ex_bad = this(2)
 
   let ?gtsle = "\<lambda>ys xs. length ys \<le> n \<and> length xs \<le> n \<and> ext gt ys xs"
 
   obtain xs where xs_bad: "bad ?gtsle xs"
     using ex_bad unfolding inf_chain_def bad_def by blast
 
   let ?ff = "worst_chain ?gtsle (\<lambda>ys xs. length ys > length xs)"
 
   note wf_len = wf_app[OF wellorder_class.wf, of length, simplified]
 
   have ff_bad: "inf_chain ?gtsle ?ff"
     by (rule worst_chain_bad[OF wf_len xs_bad])
   have ffi_bad: "\<And>i. bad ?gtsle (?ff i)"
     by (rule inf_chain_bad[OF ff_bad])
 
   have len_le_n: "\<And>i. length (?ff i) \<le> n"
     using worst_chain_pred[OF wf_len xs_bad] by simp
   have len_le_Suc: "\<And>i. length (?ff i) \<le> length (?ff (Suc i))"
     using worst_chain_not_gt[OF wf_len xs_bad] not_le_imp_less by (blast intro: trans_gt)
 
   show False
   proof (cases "\<exists>k. length (?ff k) = n")
     case False
     hence len_lt_n: "\<And>i. length (?ff i) < n"
       using len_le_n by (blast intro: le_neq_implies_less)
     hence nm1_le: "n - 1 < n"
       by fastforce
 
     let ?gtslt = "\<lambda>ys xs. length ys \<le> n - 1 \<and> length xs \<le> n - 1 \<and> ext gt ys xs"
 
     have "inf_chain ?gtslt ?ff"
       using ff_bad len_lt_n unfolding inf_chain_def
       by (metis (no_types, lifting) Suc_diff_1 le_antisym nat_neq_iff not_less0 not_less_eq_eq)
     thus False
       using ih[OF nm1_le] by blast
   next
     case True
     then obtain k where len_eq_n: "length (?ff k) = n"
       by blast
 
     let ?gtssl = "\<lambda>ys xs. length ys = n \<and> length xs = n \<and> ext gt ys xs"
 
     have len_eq_n: "length (?ff (i + k)) = n" for i
       by (induct i) (simp add: len_eq_n,
         metis (lifting) len_le_n len_le_Suc add_Suc dual_order.antisym)
 
     have "inf_chain ?gtsle (\<lambda>i. ?ff (i + k))"
       by (rule inf_chain_offset[OF ff_bad])
     hence "inf_chain ?gtssl (\<lambda>i. ?ff (i + k))"
       unfolding inf_chain_def using len_eq_n by presburger
     hence "\<not> wfP (\<lambda>xs ys. ?gtssl ys xs)"
       using wfP_iff_no_inf_chain by blast
     thus False
       using wf_same_length_if_total[of n] by sat
   qed
 qed
 
 end
 
 context
   fixes gt :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   assumes
     gt_irrefl: "\<And>z. \<not> gt z z" and
     gt_wf: "wfP (\<lambda>x y. gt y x)"
 begin
 
 lemma wf_bounded: "wfP (\<lambda>xs ys. length ys \<le> n \<and> length xs \<le> n \<and> ext gt ys xs)"
 proof -
   obtain Ge' where
     gt_sub_Ge': "{(x, y). gt y x} \<subseteq> Ge'" and
     Ge'_wo: "Well_order Ge'" and
     Ge'_fld: "Field Ge' = UNIV"
     using total_well_order_extension[OF gt_wf[unfolded wfP_def]] by blast
 
   define gt' where "\<And>y x. gt' y x \<longleftrightarrow> y \<noteq> x \<and> (x, y) \<in> Ge'"
 
   have gt_imp_gt': "gt \<le> gt'"
     by (auto simp: gt'_def gt_irrefl intro: gt_sub_Ge'[THEN subsetD])
 
   have gt'_irrefl: "\<And>z. \<not> gt' z z"
     unfolding gt'_def by simp
 
   have gt'_trans: "\<And>z y x. gt' z y \<Longrightarrow> gt' y x \<Longrightarrow> gt' z x"
     using Ge'_wo
     unfolding gt'_def well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def
       trans_def antisym_def
     by blast
 
   have "wf {(x, y). (x, y) \<in> Ge' \<and> x \<noteq> y}"
     by (rule Ge'_wo[unfolded well_order_on_def set_diff_eq
       case_prod_eta[symmetric, of "\<lambda>xy. xy \<in> Ge' \<and> xy \<notin> Id"] pair_in_Id_conv, THEN conjunct2])
   moreover have "\<And>y x. (x, y) \<in> Ge' \<and> x \<noteq> y \<longleftrightarrow> y \<noteq> x \<and> (x, y) \<in> Ge'"
     by auto
   ultimately have gt'_wf: "wfP (\<lambda>x y. gt' y x)"
     unfolding wfP_def gt'_def by simp
 
   have gt'_total: "\<And>x y. gt' y x \<or> gt' x y \<or> y = x"
     using Ge'_wo unfolding gt'_def well_order_on_def linear_order_on_def total_on_def Ge'_fld
     by blast
 
   have "wfP (\<lambda>xs ys. length ys \<le> n \<and> length xs \<le> n \<and> ext gt' ys xs)"
     using wf_bounded_if_total gt'_total gt'_irrefl gt'_trans gt'_wf by blast
   thus ?thesis
     by (rule wfP_subset) (auto intro: mono[OF gt_imp_gt', THEN predicate2D])
 qed
 
 end
 
 end
 
 
 subsection \<open>Lexicographic Extension\<close>
 
 inductive lexext :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" for gt where
   lexext_Nil: "lexext gt (y # ys) []"
 | lexext_Cons: "gt y x \<Longrightarrow> lexext gt (y # ys) (x # xs)"
 | lexext_Cons_eq: "lexext gt ys xs \<Longrightarrow> lexext gt (x # ys) (x # xs)"
 
 lemma lexext_simps[simp]:
   "lexext gt ys [] \<longleftrightarrow> ys \<noteq> []"
   "\<not> lexext gt [] xs"
   "lexext gt (y # ys) (x # xs) \<longleftrightarrow> gt y x \<or> x = y \<and> lexext gt ys xs"
 proof
   show "lexext gt ys [] \<Longrightarrow> (ys \<noteq> [])"
     by (metis lexext.cases list.distinct(1))
 next
   show "ys \<noteq> [] \<Longrightarrow> lexext gt ys []"
     by (metis lexext_Nil list.exhaust)
 next
   show "\<not> lexext gt [] xs"
     using lexext.cases by auto
 next
   show "lexext gt (y # ys) (x # xs) = (gt y x \<or> x = y \<and> lexext gt ys xs)"
   proof -
     have fwdd: "lexext gt (y # ys) (x # xs) \<longrightarrow> gt y x \<or> x = y \<and> lexext gt ys xs"
     proof
       assume "lexext gt (y # ys) (x # xs)"
       thus "gt y x \<or> x = y \<and> lexext gt ys xs"
         using lexext.cases by blast
     qed
     have backd: "gt y x \<or> x = y \<and> lexext gt ys xs \<longrightarrow> lexext gt (y # ys) (x # xs)"
       by (simp add: lexext_Cons lexext_Cons_eq)
     show "lexext gt (y # ys) (x # xs) = (gt y x \<or> x = y \<and> lexext gt ys xs)"
       using fwdd backd by blast
   qed
 qed
 
 lemma lexext_mono_strong:
   assumes
     "\<forall>y \<in> set ys. \<forall>x \<in> set xs. gt y x \<longrightarrow> gt' y x" and
     "lexext gt ys xs"
   shows "lexext gt' ys xs"
   using assms by (induct ys xs rule: list_induct2') auto
 
 lemma lexext_map_strong:
   "(\<forall>y \<in> set ys. \<forall>x \<in> set xs. gt y x \<longrightarrow> gt (f y) (f x)) \<Longrightarrow> lexext gt ys xs \<Longrightarrow>
    lexext gt (map f ys) (map f xs)"
   by (induct ys xs rule: list_induct2') auto
 
 lemma lexext_irrefl:
   assumes "\<forall>x \<in> set xs. \<not> gt x x"
   shows "\<not> lexext gt xs xs"
   using assms by (induct xs) auto
 
 lemma lexext_trans_strong:
   assumes
     "\<forall>z \<in> set zs. \<forall>y \<in> set ys. \<forall>x \<in> set xs. gt z y \<longrightarrow> gt y x \<longrightarrow> gt z x" and
     "lexext gt zs ys" and "lexext gt ys xs"
   shows "lexext gt zs xs"
   using assms
 proof (induct zs arbitrary: ys xs)
   case (Cons z zs)
   note zs_trans = this(1)
   show ?case
     using Cons(2-4)
   proof (induct ys arbitrary: xs rule: list.induct)
     case (Cons y ys)
     note ys_trans = this(1) and gt_trans = this(2) and zzs_gt_yys = this(3) and yys_gt_xs = this(4)
     show ?case
     proof (cases xs)
       case xs: (Cons x xs)
       thus ?thesis
       proof (unfold xs)
         note yys_gt_xxs = yys_gt_xs[unfolded xs]
         note gt_trans = gt_trans[unfolded xs]
 
         let ?case = "lexext gt (z # zs) (x # xs)"
 
         {
           assume "gt z y" and "gt y x"
           hence ?case
             using gt_trans by simp
         }
         moreover
         {
           assume "gt z y" and "x = y"
           hence ?case
             by simp
         }
         moreover
         {
           assume "y = z" and "gt y x"
           hence ?case
             by simp
         }
         moreover
         {
           assume
             y_eq_z: "y = z" and
             zs_gt_ys: "lexext gt zs ys" and
             x_eq_y: "x = y" and
             ys_gt_xs: "lexext gt ys xs"
 
           have "lexext gt zs xs"
             by (rule zs_trans[OF _ zs_gt_ys ys_gt_xs]) (meson gt_trans[simplified])
           hence ?case
             by (simp add: x_eq_y y_eq_z)
         }
         ultimately show ?case
           using zzs_gt_yys yys_gt_xxs by force
       qed
     qed auto
   qed auto
 qed auto
 
 lemma lexext_snoc: "lexext gt (xs @ [x]) xs"
   by (induct xs) auto
 
 lemmas lexext_compat_cons = lexext_Cons_eq
 
 lemma lexext_compat_snoc_if_same_length:
   assumes "length ys = length xs" and "lexext gt ys xs"
   shows "lexext gt (ys @ [x]) (xs @ [x])"
   using assms(2,1) by (induct rule: lexext.induct) auto
 
 lemma lexext_compat_list: "gt y x \<Longrightarrow> lexext gt (xs @ y # xs') (xs @ x # xs')"
   by (induct xs) auto
 
 lemma lexext_singleton: "lexext gt [y] [x] \<longleftrightarrow> gt y x"
   by simp
 
 lemma lexext_total: "(\<forall>y \<in> B. \<forall>x \<in> A. gt y x \<or> gt x y \<or> y = x) \<Longrightarrow> ys \<in> lists B \<Longrightarrow> xs \<in> lists A \<Longrightarrow>
   lexext gt ys xs \<or> lexext gt xs ys \<or> ys = xs"
   by (induct ys xs rule: list_induct2') auto
 
 lemma lexext_hd_or_tl: "lexext gt (y # ys) (x # xs) \<Longrightarrow> gt y x \<or> lexext gt ys xs"
   by auto
 
 interpretation lexext: ext lexext
   by standard (fact lexext_mono_strong, rule lexext_map_strong, metis in_listsD)
 
 interpretation lexext: ext_irrefl_trans_strong lexext
   by standard (fact lexext_irrefl, fact lexext_trans_strong)
 
 interpretation lexext: ext_snoc lexext
   by standard (fact lexext_snoc)
 
 interpretation lexext: ext_compat_cons lexext
   by standard (fact lexext_compat_cons)
 
 interpretation lexext: ext_compat_list lexext
   by standard (rule lexext_compat_list)
 
 interpretation lexext: ext_singleton lexext
   by standard (rule lexext_singleton)
 
 interpretation lexext: ext_total lexext
   by standard (fact lexext_total)
 
 interpretation lexext: ext_hd_or_tl lexext
   by standard (rule lexext_hd_or_tl)
 
 interpretation lexext: ext_wf_bounded lexext
   by standard
 
 
 subsection \<open>Reverse (Right-to-Left) Lexicographic Extension\<close>
 
 abbreviation lexext_rev :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
   "lexext_rev gt ys xs \<equiv> lexext gt (rev ys) (rev xs)"
 
 lemma lexext_rev_simps[simp]:
   "lexext_rev gt ys [] \<longleftrightarrow> ys \<noteq> []"
   "\<not> lexext_rev gt [] xs"
   "lexext_rev gt (ys @ [y]) (xs @ [x]) \<longleftrightarrow> gt y x \<or> x = y \<and> lexext_rev gt ys xs"
   by simp+
 
 lemma lexext_rev_cons_cons:
   assumes "length ys = length xs"
   shows "lexext_rev gt (y # ys) (x # xs) \<longleftrightarrow> lexext_rev gt ys xs \<or> ys = xs \<and> gt y x"
   using assms
 proof (induct arbitrary: y x rule: rev_induct2)
   case Nil
   thus ?case
     by simp
 next
   case (snoc y' ys x' xs)
   show ?case
     using snoc(2) by auto
 qed
 
 lemma lexext_rev_mono_strong:
   assumes
     "\<forall>y \<in> set ys. \<forall>x \<in> set xs. gt y x \<longrightarrow> gt' y x" and
     "lexext_rev gt ys xs"
   shows "lexext_rev gt' ys xs"
   using assms by (simp add: lexext_mono_strong)
 
 lemma lexext_rev_map_strong:
   "(\<forall>y \<in> set ys. \<forall>x \<in> set xs. gt y x \<longrightarrow> gt (f y) (f x)) \<Longrightarrow> lexext_rev gt ys xs \<Longrightarrow>
    lexext_rev gt (map f ys) (map f xs)"
   by (simp add: lexext_map_strong rev_map)
 
 lemma lexext_rev_irrefl:
   assumes "\<forall>x \<in> set xs. \<not> gt x x"
   shows "\<not> lexext_rev gt xs xs"
   using assms by (simp add: lexext_irrefl)
 
 lemma lexext_rev_trans_strong:
   assumes
     "\<forall>z \<in> set zs. \<forall>y \<in> set ys. \<forall>x \<in> set xs. gt z y \<longrightarrow> gt y x \<longrightarrow> gt z x" and
     "lexext_rev gt zs ys" and "lexext_rev gt ys xs"
   shows "lexext_rev gt zs xs"
   using assms(1) lexext_trans_strong[OF _ assms(2,3), unfolded set_rev] by sat
 
 lemma lexext_rev_compat_cons_if_same_length:
   assumes "length ys = length xs" and "lexext_rev gt ys xs"
   shows "lexext_rev gt (x # ys) (x # xs)"
   using assms by (simp add: lexext_compat_snoc_if_same_length)
 
 lemma lexext_rev_compat_snoc: "lexext_rev gt ys xs \<Longrightarrow> lexext_rev gt (ys @ [x]) (xs @ [x])"
   by (simp add: lexext_compat_cons)
 
 lemma lexext_rev_compat_list: "gt y x \<Longrightarrow> lexext_rev gt (xs @ y # xs') (xs @ x # xs')"
   by (induct xs' rule: rev_induct) auto
 
 lemma lexext_rev_singleton: "lexext_rev gt [y] [x] \<longleftrightarrow> gt y x"
   by simp
 
 lemma lexext_rev_total:
   "(\<forall>y \<in> B. \<forall>x \<in> A. gt y x \<or> gt x y \<or> y = x) \<Longrightarrow> ys \<in> lists B \<Longrightarrow> xs \<in> lists A \<Longrightarrow>
    lexext_rev gt ys xs \<or> lexext_rev gt xs ys \<or> ys = xs"
   by (rule lexext_total[of _ _ _ "rev ys" "rev xs", simplified])
 
 lemma lexext_rev_hd_or_tl:
   assumes
     "length ys = length xs" and
     "lexext_rev gt (y # ys) (x # xs)"
   shows "gt y x \<or> lexext_rev gt ys xs"
   using assms lexext_rev_cons_cons by fastforce
 
 interpretation lexext_rev: ext lexext_rev
   by standard (fact lexext_rev_mono_strong, rule lexext_rev_map_strong, metis in_listsD)
 
 interpretation lexext_rev: ext_irrefl_trans_strong lexext_rev
   by standard (fact lexext_rev_irrefl, fact lexext_rev_trans_strong)
 
 interpretation lexext_rev: ext_compat_snoc lexext_rev
   by standard (fact lexext_rev_compat_snoc)
 
 interpretation lexext_rev: ext_compat_list lexext_rev
   by standard (rule lexext_rev_compat_list)
 
 interpretation lexext_rev: ext_singleton lexext_rev
   by standard (rule lexext_rev_singleton)
 
 interpretation lexext_rev: ext_total lexext_rev
   by standard (fact lexext_rev_total)
 
 interpretation lexext_rev: ext_hd_or_tl lexext_rev
   by standard (rule lexext_rev_hd_or_tl)
 
 interpretation lexext_rev: ext_wf_bounded lexext_rev
   by standard
 
 
 subsection \<open>Generic Length Extension\<close>
 
 definition lenext :: "('a list \<Rightarrow> 'a list \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
   "lenext gts ys xs \<longleftrightarrow> length ys > length xs \<or> length ys = length xs \<and> gts ys xs"
 
 lemma
   lenext_mono_strong: "(gts ys xs \<Longrightarrow> gts' ys xs) \<Longrightarrow> lenext gts ys xs \<Longrightarrow> lenext gts' ys xs" and
   lenext_map_strong: "(length ys = length xs \<Longrightarrow> gts ys xs \<Longrightarrow> gts (map f ys) (map f xs)) \<Longrightarrow>
     lenext gts ys xs \<Longrightarrow> lenext gts (map f ys) (map f xs)" and
   lenext_irrefl: "\<not> gts xs xs \<Longrightarrow> \<not> lenext gts xs xs" and
   lenext_trans: "(gts zs ys \<Longrightarrow> gts ys xs \<Longrightarrow> gts zs xs) \<Longrightarrow> lenext gts zs ys \<Longrightarrow> lenext gts ys xs \<Longrightarrow>
     lenext gts zs xs" and
   lenext_snoc: "lenext gts (xs @ [x]) xs" and
   lenext_compat_cons: "(length ys = length xs \<Longrightarrow> gts ys xs \<Longrightarrow> gts (x # ys) (x # xs)) \<Longrightarrow>
     lenext gts ys xs \<Longrightarrow> lenext gts (x # ys) (x # xs)" and
   lenext_compat_snoc: "(length ys = length xs \<Longrightarrow> gts ys xs \<Longrightarrow> gts (ys @ [x]) (xs @ [x])) \<Longrightarrow>
     lenext gts ys xs \<Longrightarrow> lenext gts (ys @ [x]) (xs @ [x])" and
   lenext_compat_list: "gts (xs @ y # xs') (xs @ x # xs') \<Longrightarrow>
     lenext gts (xs @ y # xs') (xs @ x # xs')" and
   lenext_singleton: "lenext gts [y] [x] \<longleftrightarrow> gts [y] [x]" and
   lenext_total: "(gts ys xs \<or> gts xs ys \<or> ys = xs) \<Longrightarrow>
     lenext gts ys xs \<or> lenext gts xs ys \<or> ys = xs" and
   lenext_hd_or_tl: "(length ys = length xs \<Longrightarrow> gts (y # ys) (x # xs) \<Longrightarrow> gt y x \<or> gts ys xs) \<Longrightarrow>
     lenext gts (y # ys) (x # xs) \<Longrightarrow> gt y x \<or> lenext gts ys xs"
   unfolding lenext_def by auto
 
 
 subsection \<open>Length-Lexicographic Extension\<close>
 
 abbreviation len_lexext :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
   "len_lexext gt \<equiv> lenext (lexext gt)"
 
 lemma len_lexext_mono_strong:
   "(\<forall>y \<in> set ys. \<forall>x \<in> set xs. gt y x \<longrightarrow> gt' y x) \<Longrightarrow> len_lexext gt ys xs \<Longrightarrow> len_lexext gt' ys xs"
   by (rule lenext_mono_strong[OF lexext_mono_strong])
 
 lemma len_lexext_map_strong:
   "(\<forall>y \<in> set ys. \<forall>x \<in> set xs. gt y x \<longrightarrow> gt (f y) (f x)) \<Longrightarrow> len_lexext gt ys xs \<Longrightarrow>
    len_lexext gt (map f ys) (map f xs)"
   by (rule lenext_map_strong) (metis lexext_map_strong)
 
 lemma len_lexext_irrefl: "(\<forall>x \<in> set xs. \<not> gt x x) \<Longrightarrow> \<not> len_lexext gt xs xs"
   by (rule lenext_irrefl[OF lexext_irrefl])
 
 lemma len_lexext_trans_strong:
   "(\<forall>z \<in> set zs. \<forall>y \<in> set ys. \<forall>x \<in> set xs. gt z y \<longrightarrow> gt y x \<longrightarrow> gt z x) \<Longrightarrow> len_lexext gt zs ys \<Longrightarrow>
    len_lexext gt ys xs \<Longrightarrow> len_lexext gt zs xs"
   by (rule lenext_trans[OF lexext_trans_strong])
 
 lemma len_lexext_snoc: "len_lexext gt (xs @ [x]) xs"
   by (rule lenext_snoc)
 
 lemma len_lexext_compat_cons: "len_lexext gt ys xs \<Longrightarrow> len_lexext gt (x # ys) (x # xs)"
   by (intro lenext_compat_cons lexext_compat_cons)
 
 lemma len_lexext_compat_snoc: "len_lexext gt ys xs \<Longrightarrow> len_lexext gt (ys @ [x]) (xs @ [x])"
   by (intro lenext_compat_snoc lexext_compat_snoc_if_same_length)
 
 lemma len_lexext_compat_list: "gt y x \<Longrightarrow> len_lexext gt (xs @ y # xs') (xs @ x # xs')"
   by (intro lenext_compat_list lexext_compat_list)
 
 lemma len_lexext_singleton[simp]: "len_lexext gt [y] [x] \<longleftrightarrow> gt y x"
   by (simp only: lenext_singleton lexext_singleton)
 
 lemma len_lexext_total: "(\<forall>y \<in> B. \<forall>x \<in> A. gt y x \<or> gt x y \<or> y = x) \<Longrightarrow> ys \<in> lists B \<Longrightarrow> xs \<in> lists A \<Longrightarrow>
   len_lexext gt ys xs \<or> len_lexext gt xs ys \<or> ys = xs"
   by (rule lenext_total[OF lexext_total])
 
 lemma len_lexext_iff_lenlex: "len_lexext gt ys xs \<longleftrightarrow> (xs, ys) \<in> lenlex {(x, y). gt y x}"
 proof -
   {
     assume "length xs = length ys"
     hence "lexext gt ys xs \<longleftrightarrow> (xs, ys) \<in> lex {(x, y). gt y x}"
       by (induct xs ys rule: list_induct2) auto
   }
   thus ?thesis
     unfolding lenext_def lenlex_conv by auto
 qed
 
 lemma len_lexext_wf: "wfP (\<lambda>x y. gt y x) \<Longrightarrow> wfP (\<lambda>xs ys. len_lexext gt ys xs)"
   unfolding wfP_def len_lexext_iff_lenlex by (simp add: wf_lenlex)
 
 lemma len_lexext_hd_or_tl: "len_lexext gt (y # ys) (x # xs) \<Longrightarrow> gt y x \<or> len_lexext gt ys xs"
   using lenext_hd_or_tl lexext_hd_or_tl by metis
 
 interpretation len_lexext: ext len_lexext
   by standard (fact len_lexext_mono_strong, rule len_lexext_map_strong, metis in_listsD)
 
 interpretation len_lexext: ext_irrefl_trans_strong len_lexext
   by standard (fact len_lexext_irrefl, fact len_lexext_trans_strong)
 
 interpretation len_lexext: ext_snoc len_lexext
   by standard (fact len_lexext_snoc)
 
 interpretation len_lexext: ext_compat_cons len_lexext
   by standard (fact len_lexext_compat_cons)
 
 interpretation len_lexext: ext_compat_snoc len_lexext
   by standard (fact len_lexext_compat_snoc)
 
 interpretation len_lexext: ext_compat_list len_lexext
   by standard (rule len_lexext_compat_list)
 
 interpretation len_lexext: ext_singleton len_lexext
   by standard (rule len_lexext_singleton)
 
 interpretation len_lexext: ext_total len_lexext
   by standard (fact len_lexext_total)
 
 interpretation len_lexext: ext_wf len_lexext
   by standard (fact len_lexext_wf)
 
 interpretation len_lexext: ext_hd_or_tl len_lexext
   by standard (rule len_lexext_hd_or_tl)
 
 interpretation len_lexext: ext_wf_bounded len_lexext
   by standard
 
 
 subsection \<open>Reverse (Right-to-Left) Length-Lexicographic Extension\<close>
 
 abbreviation len_lexext_rev :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
   "len_lexext_rev gt \<equiv> lenext (lexext_rev gt)"
 
 lemma len_lexext_rev_mono_strong:
   "(\<forall>y \<in> set ys. \<forall>x \<in> set xs. gt y x \<longrightarrow> gt' y x) \<Longrightarrow> len_lexext_rev gt ys xs \<Longrightarrow> len_lexext_rev gt' ys xs"
   by (rule lenext_mono_strong) (rule lexext_rev_mono_strong)
 
 lemma len_lexext_rev_map_strong:
   "(\<forall>y \<in> set ys. \<forall>x \<in> set xs. gt y x \<longrightarrow> gt (f y) (f x)) \<Longrightarrow> len_lexext_rev gt ys xs \<Longrightarrow>
    len_lexext_rev gt (map f ys) (map f xs)"
   by (rule lenext_map_strong) (rule lexext_rev_map_strong)
 
 lemma len_lexext_rev_irrefl: "(\<forall>x \<in> set xs. \<not> gt x x) \<Longrightarrow> \<not> len_lexext_rev gt xs xs"
   by (rule lenext_irrefl) (rule lexext_rev_irrefl)
 
 lemma len_lexext_rev_trans_strong:
   "(\<forall>z \<in> set zs. \<forall>y \<in> set ys. \<forall>x \<in> set xs. gt z y \<longrightarrow> gt y x \<longrightarrow> gt z x) \<Longrightarrow> len_lexext_rev gt zs ys \<Longrightarrow>
    len_lexext_rev gt ys xs \<Longrightarrow> len_lexext_rev gt zs xs"
   by (rule lenext_trans) (rule lexext_rev_trans_strong)
 
 lemma len_lexext_rev_snoc: "len_lexext_rev gt (xs @ [x]) xs"
   by (rule lenext_snoc)
 
 lemma len_lexext_rev_compat_cons: "len_lexext_rev gt ys xs \<Longrightarrow> len_lexext_rev gt (x # ys) (x # xs)"
   by (intro lenext_compat_cons lexext_rev_compat_cons_if_same_length)
 
 lemma len_lexext_rev_compat_snoc: "len_lexext_rev gt ys xs \<Longrightarrow> len_lexext_rev gt (ys @ [x]) (xs @ [x])"
   by (intro lenext_compat_snoc lexext_rev_compat_snoc)
 
 lemma len_lexext_rev_compat_list: "gt y x \<Longrightarrow> len_lexext_rev gt (xs @ y # xs') (xs @ x # xs')"
   by (intro lenext_compat_list lexext_rev_compat_list)
 
 lemma len_lexext_rev_singleton[simp]: "len_lexext_rev gt [y] [x] \<longleftrightarrow> gt y x"
   by (simp only: lenext_singleton lexext_rev_singleton)
 
 lemma len_lexext_rev_total: "(\<forall>y \<in> B. \<forall>x \<in> A. gt y x \<or> gt x y \<or> y = x) \<Longrightarrow> ys \<in> lists B \<Longrightarrow>
   xs \<in> lists A \<Longrightarrow> len_lexext_rev gt ys xs \<or> len_lexext_rev gt xs ys \<or> ys = xs"
   by (rule lenext_total[OF lexext_rev_total])
 
 lemma len_lexext_rev_iff_len_lexext: "len_lexext_rev gt ys xs \<longleftrightarrow> len_lexext gt (rev ys) (rev xs)"
   unfolding lenext_def by simp
 
 lemma len_lexext_rev_wf: "wfP (\<lambda>x y. gt y x) \<Longrightarrow> wfP (\<lambda>xs ys. len_lexext_rev gt ys xs)"
   unfolding len_lexext_rev_iff_len_lexext
   by (rule wfP_app[of "\<lambda>xs ys. len_lexext gt ys xs" rev, simplified]) (rule len_lexext_wf)
 
 lemma len_lexext_rev_hd_or_tl:
   "len_lexext_rev gt (y # ys) (x # xs) \<Longrightarrow> gt y x \<or> len_lexext_rev gt ys xs"
   using lenext_hd_or_tl lexext_rev_hd_or_tl by metis
 
 interpretation len_lexext_rev: ext len_lexext_rev
   by standard (fact len_lexext_rev_mono_strong, rule len_lexext_rev_map_strong, metis in_listsD)
 
 interpretation len_lexext_rev: ext_irrefl_trans_strong len_lexext_rev
   by standard (fact len_lexext_rev_irrefl, fact len_lexext_rev_trans_strong)
 
 interpretation len_lexext_rev: ext_snoc len_lexext_rev
   by standard (fact len_lexext_rev_snoc)
 
 interpretation len_lexext_rev: ext_compat_cons len_lexext_rev
   by standard (fact len_lexext_rev_compat_cons)
 
 interpretation len_lexext_rev: ext_compat_snoc len_lexext_rev
   by standard (fact len_lexext_rev_compat_snoc)
 
 interpretation len_lexext_rev: ext_compat_list len_lexext_rev
   by standard (rule len_lexext_rev_compat_list)
 
 interpretation len_lexext_rev: ext_singleton len_lexext_rev
   by standard (rule len_lexext_rev_singleton)
 
 interpretation len_lexext_rev: ext_total len_lexext_rev
   by standard (fact len_lexext_rev_total)
 
 interpretation len_lexext_rev: ext_wf len_lexext_rev
   by standard (fact len_lexext_rev_wf)
 
 interpretation len_lexext_rev: ext_hd_or_tl len_lexext_rev
   by standard (rule len_lexext_rev_hd_or_tl)
 
 interpretation len_lexext_rev: ext_wf_bounded len_lexext_rev
   by standard
 
 
 subsection \<open>Dershowitz--Manna Multiset Extension\<close>
 
 definition msetext_dersh where
   "msetext_dersh gt ys xs = (let N = mset ys; M = mset xs in
      (\<exists>Y X. Y \<noteq> {#} \<and> Y \<subseteq># N \<and> M = (N - Y) + X \<and> (\<forall>x. x \<in># X \<longrightarrow> (\<exists>y. y \<in># Y \<and> gt y x))))"
 
 text \<open>
 The following proof is based on that of @{thm[source] less_multiset\<^sub>D\<^sub>M_imp_mult}.
 \<close>
 
 lemma msetext_dersh_imp_mult_rel:
   assumes
     ys_a: "ys \<in> lists A" and xs_a: "xs \<in> lists A" and
     ys_gt_xs: "msetext_dersh gt ys xs"
   shows "(mset xs, mset ys) \<in> mult {(x, y). x \<in> A \<and> y \<in> A \<and> gt y x}"
 proof -
   obtain Y X where y_nemp: "Y \<noteq> {#}" and y_sub_ys: "Y \<subseteq># mset ys" and
     xs_eq: "mset xs = mset ys - Y + X" and ex_y: "\<forall>x. x \<in># X \<longrightarrow> (\<exists>y. y \<in># Y \<and> gt y x)"
     using ys_gt_xs[unfolded msetext_dersh_def Let_def] by blast
   have ex_y': "\<forall>x. x \<in># X \<longrightarrow> (\<exists>y. y \<in># Y \<and> x \<in> A \<and> y \<in> A \<and> gt y x)"
     using ex_y y_sub_ys xs_eq ys_a xs_a by (metis in_listsD mset_subset_eqD set_mset_mset union_iff)
   hence "(mset ys - Y + X, mset ys - Y + Y) \<in> mult {(x, y). x \<in> A \<and> y \<in> A \<and> gt y x}"
     using y_nemp y_sub_ys by (intro one_step_implies_mult) (auto simp: Bex_def trans_def)
   thus ?thesis
     using xs_eq y_sub_ys by (simp add: subset_mset.diff_add)
 qed
 
 lemma msetext_dersh_imp_mult: "msetext_dersh gt ys xs \<Longrightarrow> (mset xs, mset ys) \<in> mult {(x, y). gt y x}"
   using msetext_dersh_imp_mult_rel[of _ UNIV] by auto
 
 lemma mult_imp_msetext_dersh_rel:
   assumes
     ys_a: "set_mset (mset ys) \<subseteq> A" and xs_a: "set_mset (mset xs) \<subseteq> A" and
     in_mult: "(mset xs, mset ys) \<in> mult {(x, y). x \<in> A \<and> y \<in> A \<and> gt y x}" and
     trans: "\<forall>z \<in> A. \<forall>y \<in> A. \<forall>x \<in> A. gt z y \<longrightarrow> gt y x \<longrightarrow> gt z x"
   shows "msetext_dersh gt ys xs"
   using in_mult ys_a xs_a unfolding mult_def msetext_dersh_def Let_def
 proof induct
   case (base Ys)
   then obtain y M0 X where "Ys = M0 + {#y#}" and "mset xs = M0 + X" and "\<forall>a. a \<in># X \<longrightarrow> gt y a"
     unfolding mult1_def by auto
   thus ?case
     by (auto intro: exI[of _ "{#y#}"] exI[of _ X])
 next
   case (step Ys Zs)
   note ys_zs_in_mult1 = this(2) and ih = this(3) and zs_a = this(4) and xs_a = this(5)
 
   have Ys_a: "set_mset Ys \<subseteq> A"
     using ys_zs_in_mult1 zs_a unfolding mult1_def by auto
 
   obtain Y X where y_nemp: "Y \<noteq> {#}" and y_sub_ys: "Y \<subseteq># Ys" and xs_eq: "mset xs = Ys - Y + X" and
     ex_y: "\<forall>x. x \<in># X \<longrightarrow> (\<exists>y. y \<in># Y \<and> gt y x)"
     using ih[OF Ys_a xs_a] by blast
 
   obtain z M0 Ya where zs_eq: "Zs = M0 + {#z#}" and ys_eq: "Ys = M0 + Ya" and
     z_gt: "\<forall>y. y \<in># Ya \<longrightarrow> y \<in> A \<and> z \<in> A \<and> gt z y"
     using ys_zs_in_mult1[unfolded mult1_def] by auto
 
   let ?Za = "Y - Ya + {#z#}"
   let ?Xa = "X + Ya + (Y - Ya) - Y"
 
   have xa_sub_x_ya: "set_mset ?Xa \<subseteq> set_mset (X + Ya)"
     by (metis diff_subset_eq_self in_diffD subsetI subset_mset.diff_diff_right)
 
   have x_a: "set_mset X \<subseteq> A"
     using xs_a xs_eq by auto
   have ya_a: "set_mset Ya \<subseteq> A"
     by (simp add: subsetI z_gt)
 
   have ex_y': "\<exists>y. y \<in># Y - Ya + {#z#} \<and> gt y x" if x_in: "x \<in># X + Ya" for x
   proof (cases "x \<in># X")
     case True
     then obtain y where y_in: "y \<in># Y" and y_gt_x: "gt y x"
       using ex_y by blast
     show ?thesis
     proof (cases "y \<in># Ya")
       case False
       hence "y \<in># Y - Ya + {#z#}"
         using y_in by fastforce
       thus ?thesis
         using y_gt_x by blast
     next
       case True
       hence "y \<in> A" and "z \<in> A" and "gt z y"
         using z_gt by blast+
       hence "gt z x"
         using trans y_gt_x x_a ya_a x_in by (meson subsetCE union_iff)
       thus ?thesis
         by auto
     qed
   next
     case False
     hence "x \<in># Ya"
       using x_in by auto
     hence "x \<in> A" and "z \<in> A" and "gt z x"
       using z_gt by blast+
     thus ?thesis
       by auto
   qed
 
   show ?case
   proof (rule exI[of _ ?Za], rule exI[of _ ?Xa], intro conjI)
     show "Y - Ya + {#z#} \<subseteq># Zs"
       using mset_subset_eq_mono_add subset_eq_diff_conv y_sub_ys ys_eq zs_eq by fastforce
   next
     show "mset xs = Zs - (Y - Ya + {#z#}) + (X + Ya + (Y - Ya) - Y)"
       unfolding xs_eq ys_eq zs_eq by (auto simp: multiset_eq_iff)
   next
     show "\<forall>x. x \<in># X + Ya + (Y - Ya) - Y \<longrightarrow> (\<exists>y. y \<in># Y - Ya + {#z#} \<and> gt y x)"
       using ex_y' xa_sub_x_ya by blast
   qed auto
 qed
 
 lemma msetext_dersh_mono_strong:
   "(\<forall>y \<in> set ys. \<forall>x \<in> set xs. gt y x \<longrightarrow> gt' y x) \<Longrightarrow> msetext_dersh gt ys xs \<Longrightarrow>
   msetext_dersh gt' ys xs"
   unfolding msetext_dersh_def Let_def
   by (metis mset_subset_eqD mset_subset_eq_add_right set_mset_mset)
 
 lemma msetext_dersh_map_strong:
   assumes
     compat_f: "\<forall>y \<in> set ys. \<forall>x \<in> set xs. gt y x \<longrightarrow> gt (f y) (f x)" and
     ys_gt_xs: "msetext_dersh gt ys xs"
   shows "msetext_dersh gt (map f ys) (map f xs)"
 proof -
   obtain Y X where
     y_nemp: "Y \<noteq> {#}" and y_sub_ys: "Y \<subseteq># mset ys" and xs_eq: "mset xs = mset ys - Y + X" and
     ex_y: "\<forall>x. x \<in># X \<longrightarrow> (\<exists>y. y \<in># Y \<and> gt y x)"
     using ys_gt_xs[unfolded msetext_dersh_def Let_def mset_map] by blast
 
   have x_sub_xs: "X \<subseteq># mset xs"
     using xs_eq by simp
 
   let ?fY = "image_mset f Y"
   let ?fX = "image_mset f X"
 
   show ?thesis
     unfolding msetext_dersh_def Let_def mset_map
   proof (intro exI conjI)
     show "image_mset f (mset xs) = image_mset f (mset ys) - ?fY + ?fX"
       using xs_eq[THEN arg_cong, of "image_mset f"] y_sub_ys by (metis image_mset_Diff image_mset_union)
   next
     obtain y where y: "\<forall>x. x \<in># X \<longrightarrow> y x \<in># Y \<and> gt (y x) x"
       using ex_y by moura
 
     show "\<forall>fx. fx \<in># ?fX \<longrightarrow> (\<exists>fy. fy \<in># ?fY \<and> gt fy fx)"
     proof (intro allI impI)
       fix fx
       assume "fx \<in># ?fX"
       then obtain x where fx: "fx = f x" and x_in: "x \<in># X"
         by auto
       hence y_in: "y x \<in># Y" and y_gt: "gt (y x) x"
         using y[rule_format, OF x_in] by blast+
       hence "f (y x) \<in># ?fY \<and> gt (f (y x)) (f x)"
         using compat_f y_sub_ys x_sub_xs x_in
         by (metis image_eqI in_image_mset mset_subset_eqD set_mset_mset)
       thus "\<exists>fy. fy \<in># ?fY \<and> gt fy fx"
         unfolding fx by auto
     qed
   qed (auto simp: y_nemp y_sub_ys image_mset_subseteq_mono)
 qed
 
 lemma msetext_dersh_trans:
   assumes
     zs_a: "zs \<in> lists A" and
     ys_a: "ys \<in> lists A" and
     xs_a: "xs \<in> lists A" and
     trans: "\<forall>z \<in> A. \<forall>y \<in> A. \<forall>x \<in> A. gt z y \<longrightarrow> gt y x \<longrightarrow> gt z x" and
     zs_gt_ys: "msetext_dersh gt zs ys" and
     ys_gt_xs: "msetext_dersh gt ys xs"
   shows "msetext_dersh gt zs xs"
 proof (rule mult_imp_msetext_dersh_rel[OF _ _ _ trans])
   show "set_mset (mset zs) \<subseteq> A"
     using zs_a by auto
 next
   show "set_mset (mset xs) \<subseteq> A"
     using xs_a by auto
 next
   let ?Gt = "{(x, y). x \<in> A \<and> y \<in> A \<and> gt y x}"
 
   have "(mset xs, mset ys) \<in> mult ?Gt"
     by (rule msetext_dersh_imp_mult_rel[OF ys_a xs_a ys_gt_xs])
   moreover have "(mset ys, mset zs) \<in> mult ?Gt"
     by (rule msetext_dersh_imp_mult_rel[OF zs_a ys_a zs_gt_ys])
   ultimately show "(mset xs, mset zs) \<in> mult ?Gt"
     unfolding mult_def by simp
 qed
 
 lemma msetext_dersh_irrefl_from_trans:
   assumes
     trans: "\<forall>z \<in> set xs. \<forall>y \<in> set xs. \<forall>x \<in> set xs. gt z y \<longrightarrow> gt y x \<longrightarrow> gt z x" and
     irrefl: "\<forall>x \<in> set xs. \<not> gt x x"
   shows "\<not> msetext_dersh gt xs xs"
   unfolding msetext_dersh_def Let_def
 proof clarify
   fix Y X
   assume y_nemp: "Y \<noteq> {#}" and y_sub_xs: "Y \<subseteq># mset xs" and xs_eq: "mset xs = mset xs - Y + X" and
     ex_y: "\<forall>x. x \<in># X \<longrightarrow> (\<exists>y. y \<in># Y \<and> gt y x)"
 
   have x_eq_y: "X = Y"
     using y_sub_xs xs_eq by (metis diff_union_cancelL subset_mset.diff_add)
 
   let ?Gt = "{(y, x). y \<in># Y \<and> x \<in># Y \<and> gt y x}"
 
   have "?Gt \<subseteq> set_mset Y \<times> set_mset Y"
     by auto
   hence fin: "finite ?Gt"
     by (auto dest!: infinite_super)
   moreover have "irrefl ?Gt"
     unfolding irrefl_def using irrefl y_sub_xs by (fastforce dest!: set_mset_mono)
   moreover have "trans ?Gt"
     unfolding trans_def using trans y_sub_xs by (fastforce dest!: set_mset_mono)
   ultimately have acyc: "acyclic ?Gt"
     by (rule finite_irrefl_trans_imp_wf[THEN wf_acyclic])
 
   have fin_y: "finite (set_mset Y)"
     using y_sub_xs by simp
   hence cyc: "\<not> acyclic ?Gt"
     proof (rule finite_nonempty_ex_succ_imp_cyclic)
       show "\<forall>x \<in># Y. \<exists>y \<in># Y. (y, x) \<in> ?Gt"
         using ex_y[unfolded x_eq_y] by auto
     qed (auto simp: y_nemp)
 
   show False
     using acyc cyc by sat
 qed
 
 lemma msetext_dersh_snoc: "msetext_dersh gt (xs @ [x]) xs"
   unfolding msetext_dersh_def Let_def
 proof (intro exI conjI)
   show "mset xs = mset (xs @ [x]) - {#x#} + {#}"
     by simp
 qed auto
 
 lemma msetext_dersh_compat_cons:
   assumes ys_gt_xs: "msetext_dersh gt ys xs"
   shows "msetext_dersh gt (x # ys) (x # xs)"
 proof -
   obtain Y X where
     y_nemp: "Y \<noteq> {#}" and y_sub_ys: "Y \<subseteq># mset ys" and xs_eq: "mset xs = mset ys - Y + X" and
     ex_y: "\<forall>x. x \<in># X \<longrightarrow> (\<exists>y. y \<in># Y \<and> gt y x)"
     using ys_gt_xs[unfolded msetext_dersh_def Let_def mset_map] by blast
 
   show ?thesis
     unfolding msetext_dersh_def Let_def
   proof (intro exI conjI)
     show "Y \<subseteq># mset (x # ys)"
       using y_sub_ys
       by (metis add_mset_add_single mset.simps(2) mset_subset_eq_add_left
         subset_mset.add_increasing2)
   next
     show "mset (x # xs) = mset (x # ys) - Y + X"
     proof -
       have "X + (mset ys - Y) = mset xs"
         by (simp add: union_commute xs_eq)
       hence "mset (x # xs) = X + (mset (x # ys) - Y)"
         by (metis add_mset_add_single mset.simps(2) mset_subset_eq_multiset_union_diff_commute
           union_mset_add_mset_right y_sub_ys)
       thus ?thesis
         by (simp add: union_commute)
     qed
   qed (auto simp: y_nemp ex_y)
 qed
 
 lemma msetext_dersh_compat_snoc: "msetext_dersh gt ys xs \<Longrightarrow> msetext_dersh gt (ys @ [x]) (xs @ [x])"
   using msetext_dersh_compat_cons[of gt ys xs x] unfolding msetext_dersh_def by simp
 
 lemma msetext_dersh_compat_list:
   assumes y_gt_x: "gt y x"
   shows "msetext_dersh gt (xs @ y # xs') (xs @ x # xs')"
   unfolding msetext_dersh_def Let_def
 proof (intro exI conjI)
   show "mset (xs @ x # xs') = mset (xs @ y # xs') - {#y#} + {#x#}"
     by auto
 qed (auto intro: y_gt_x)
 
 lemma msetext_dersh_singleton: "msetext_dersh gt [y] [x] \<longleftrightarrow> gt y x"
   unfolding msetext_dersh_def Let_def
   by (auto dest: nonempty_subseteq_mset_eq_singleton simp: nonempty_subseteq_mset_iff_singleton)
 
 lemma msetext_dersh_wf:
   assumes wf_gt: "wfP (\<lambda>x y. gt y x)"
   shows "wfP (\<lambda>xs ys. msetext_dersh gt ys xs)"
 proof (rule wfP_subset, rule wfP_app[of "\<lambda>xs ys. (xs, ys) \<in> mult {(x, y). gt y x}" mset])
   show "wfP (\<lambda>xs ys. (xs, ys) \<in> mult {(x, y). gt y x})"
     using wf_gt unfolding wfP_def by (auto intro: wf_mult)
 next
   show "(\<lambda>xs ys. msetext_dersh gt ys xs) \<le> (\<lambda>x y. (mset x, mset y) \<in> mult {(x, y). gt y x})"
     using msetext_dersh_imp_mult by blast
 qed
 
 interpretation msetext_dersh: ext msetext_dersh
   by standard (fact msetext_dersh_mono_strong, rule msetext_dersh_map_strong, metis in_listsD)
 
 interpretation msetext_dersh: ext_trans_before_irrefl msetext_dersh
   by standard (fact msetext_dersh_trans, fact msetext_dersh_irrefl_from_trans)
 
 interpretation msetext_dersh: ext_snoc msetext_dersh
   by standard (fact msetext_dersh_snoc)
 
 interpretation msetext_dersh: ext_compat_cons msetext_dersh
   by standard (fact msetext_dersh_compat_cons)
 
 interpretation msetext_dersh: ext_compat_snoc msetext_dersh
   by standard (fact msetext_dersh_compat_snoc)
 
 interpretation msetext_dersh: ext_compat_list msetext_dersh
   by standard (rule msetext_dersh_compat_list)
 
 interpretation msetext_dersh: ext_singleton msetext_dersh
   by standard (rule msetext_dersh_singleton)
 
 interpretation msetext_dersh: ext_wf msetext_dersh
   by standard (fact msetext_dersh_wf)
 
 
 subsection \<open>Huet--Oppen Multiset Extension\<close>
 
 definition msetext_huet where
   "msetext_huet gt ys xs = (let N = mset ys; M = mset xs in
      M \<noteq> N \<and> (\<forall>x. count M x > count N x \<longrightarrow> (\<exists>y. gt y x \<and> count N y > count M y)))"
 
 lemma msetext_huet_imp_count_gt:
   assumes ys_gt_xs: "msetext_huet gt ys xs"
   shows "\<exists>x. count (mset ys) x > count (mset xs) x"
 proof -
   obtain x where "count (mset ys) x \<noteq> count (mset xs) x"
     using ys_gt_xs[unfolded msetext_huet_def Let_def] by (fastforce intro: multiset_eqI)
   moreover
   {
     assume "count (mset ys) x < count (mset xs) x"
     hence ?thesis
       using ys_gt_xs[unfolded msetext_huet_def Let_def] by blast
   }
   moreover
   {
     assume "count (mset ys) x > count (mset xs) x"
     hence ?thesis
       by fast
   }
   ultimately show ?thesis
     by fastforce
 qed
 
 lemma msetext_huet_imp_dersh:
   assumes huet: "msetext_huet gt ys xs"
   shows "msetext_dersh gt ys xs"
 proof (unfold msetext_dersh_def Let_def, intro exI conjI)
   let ?X = "mset xs - mset ys"
   let ?Y = "mset ys - mset xs"
 
   show "?Y \<noteq> {#}"
     by (metis msetext_huet_imp_count_gt[OF huet] empty_iff in_diff_count set_mset_empty)
   show "?Y \<subseteq># mset ys"
     by auto
   show "mset xs = mset ys - ?Y + ?X"
     by (metis add.commute diff_intersect_right_idem multiset_inter_def subset_mset.inf.cobounded2
       subset_mset.le_imp_diff_is_add)
   show "\<forall>x. x \<in># ?X \<longrightarrow> (\<exists>y. y \<in># ?Y \<and> gt y x)"
     using huet[unfolded msetext_huet_def Let_def, THEN conjunct2] by (meson in_diff_count)
 qed
 
 text \<open>
 The following proof is based on that of @{thm[source] mult_imp_less_multiset\<^sub>H\<^sub>O}.
 \<close>
 
 lemma mult_imp_msetext_huet:
   assumes
     irrefl: "irreflp gt" and trans: "transp gt" and
     in_mult: "(mset xs, mset ys) \<in> mult {(x, y). gt y x}"
   shows "msetext_huet gt ys xs"
   using in_mult unfolding mult_def msetext_huet_def Let_def
 proof (induct rule: trancl_induct)
   case (base Ys)
   thus ?case
     using irrefl unfolding irreflp_def msetext_huet_def Let_def mult1_def
     by (auto 0 3 split: if_splits)
 next
   case (step Ys Zs)
 
   have asym[unfolded antisym_def, simplified]: "antisymp gt"
     by (rule irreflp_transp_imp_antisymP[OF irrefl trans])
 
   from step(3) have "mset xs \<noteq> Ys" and
     **: "\<And>x. count Ys x < count (mset xs) x \<Longrightarrow> (\<exists>y. gt y x \<and> count (mset xs) y < count Ys y)"
     by blast+
   from step(2) obtain M0 a K where
     *: "Zs = M0 + {#a#}" "Ys = M0 + K" "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> gt a b"
     using irrefl unfolding mult1_def irreflp_def by force
   have "mset xs \<noteq> Zs"
   proof (cases "K = {#}")
     case True
     thus ?thesis
       using \<open>mset xs \<noteq> Ys\<close> ** *(1,2) irrefl[unfolded irreflp_def]
       by (metis One_nat_def add.comm_neutral count_single diff_union_cancelL lessI
         minus_multiset.rep_eq not_add_less2 plus_multiset.rep_eq union_commute zero_less_diff)
   next
     case False
     thus ?thesis
     proof -
       obtain aa :: "'a \<Rightarrow> 'a" where
         f1: "\<forall>a. \<not> count Ys a < count (mset xs) a \<or> gt (aa a) a \<and>
           count (mset xs) (aa a) < count Ys (aa a)"
         using "**" by moura
       have f2: "K + M0 = Ys"
         using "*"(2) union_ac(2) by blast
       have f3: "\<And>aa. count Zs aa = count M0 aa + count {#a#} aa"
         by (simp add: "*"(1))
       have f4: "\<And>a. count Ys a = count K a + count M0 a"
         using f2 by auto
       have f5: "count K a = 0"
         by (meson "*"(3) count_inI)
       have "Zs - M0 = {#a#}"
         using "*"(1) add_diff_cancel_left' by blast
       then have f6: "count M0 a < count Zs a"
         by (metis in_diff_count union_single_eq_member)
       have "\<And>m. count m a = 0 + count m a"
         by simp
       moreover
       { assume "aa a \<noteq> a"
         then have "mset xs = Zs \<and> count Zs (aa a) < count K (aa a) + count M0 (aa a) \<longrightarrow>
           count K (aa a) + count M0 (aa a) < count Zs (aa a)"
           using f5 f3 f2 f1 "*"(4) asym by (auto dest!: antisympD) }
       ultimately show ?thesis
         using f6 f5 f4 f1 by (metis less_imp_not_less)
     qed
   qed
   moreover
   {
     assume "count Zs a \<le> count (mset xs) a"
     with \<open>a \<notin># K\<close> have "count Ys a < count (mset xs) a" unfolding *(1,2)
       by (auto simp add: not_in_iff)
       with ** obtain z where z: "gt z a" "count (mset xs) z < count Ys z"
         by blast
       with * have "count Ys z \<le> count Zs z"
         using asym
         by (auto simp: intro: count_inI dest: antisympD)
       with z have "\<exists>z. gt z a \<and> count (mset xs) z < count Zs z" by auto
   }
   note count_a = this
   {
     fix y
     assume count_y: "count Zs y < count (mset xs) y"
     have "\<exists>x. gt x y \<and> count (mset xs) x < count Zs x"
     proof (cases "y = a")
       case True
       with count_y count_a show ?thesis by auto
     next
       case False
       show ?thesis
       proof (cases "y \<in># K")
         case True
         with *(4) have "gt a y" by simp
         then show ?thesis
           by (cases "count Zs a \<le> count (mset xs) a",
             blast dest: count_a trans[unfolded transp_def, rule_format], auto dest: count_a)
       next
         case False
         with \<open>y \<noteq> a\<close> have "count Zs y = count Ys y" unfolding *(1,2)
           by (simp add: not_in_iff)
         with count_y ** obtain z where z: "gt z y" "count (mset xs) z < count Ys z" by auto
         show ?thesis
         proof (cases "z \<in># K")
           case True
           with *(4) have "gt a z" by simp
           with z(1) show ?thesis
             by (cases "count Zs a \<le> count (mset xs) a")
               (blast dest: count_a not_le_imp_less trans[unfolded transp_def, rule_format])+
         next
           case False
           with \<open>a \<notin># K\<close> have "count Ys z \<le> count Zs z" unfolding *
             by (auto simp add: not_in_iff)
           with z show ?thesis by auto
         qed
       qed
     qed
   }
   ultimately show ?case
     unfolding msetext_huet_def Let_def by blast
 qed
 
 theorem msetext_huet_eq_dersh: "irreflp gt \<Longrightarrow> transp gt \<Longrightarrow> msetext_dersh gt = msetext_huet gt"
   using msetext_huet_imp_dersh msetext_dersh_imp_mult mult_imp_msetext_huet by fast
 
 lemma msetext_huet_mono_strong:
   "(\<forall>y \<in> set ys. \<forall>x \<in> set xs. gt y x \<longrightarrow> gt' y x) \<Longrightarrow> msetext_huet gt ys xs \<Longrightarrow> msetext_huet gt' ys xs"
   unfolding msetext_huet_def
   by (metis less_le_trans mem_Collect_eq not_le not_less0 set_mset_mset[unfolded set_mset_def])
 
 lemma msetext_huet_map:
   assumes
     fin: "finite A" and
     ys_a: "ys \<in> lists A" and xs_a: "xs \<in> lists A" and
     irrefl_f: "\<forall>x \<in> A. \<not> gt (f x) (f x)" and
     trans_f: "\<forall>z \<in> A. \<forall>y \<in> A. \<forall>x \<in> A. gt (f z) (f y) \<longrightarrow> gt (f y) (f x) \<longrightarrow> gt (f z) (f x)" and
     compat_f: "\<forall>y \<in> A. \<forall>x \<in> A. gt y x \<longrightarrow> gt (f y) (f x)" and
     ys_gt_xs: "msetext_huet gt ys xs"
   shows "msetext_huet gt (map f ys) (map f xs)" (is "msetext_huet _ ?fys ?fxs")
 proof -
   have irrefl: "\<forall>x \<in> A. \<not> gt x x"
     using irrefl_f compat_f by blast
 
   have
     ms_xs_ne_ys: "mset xs \<noteq> mset ys" and
     ex_gt: "\<forall>x. count (mset ys) x < count (mset xs) x \<longrightarrow>
       (\<exists>y. gt y x \<and> count (mset xs) y < count (mset ys) y)"
     using ys_gt_xs[unfolded msetext_huet_def Let_def] by blast+
 
   have ex_y: "\<exists>y. gt (f y) (f x) \<and> count (mset ?fxs) (f y) < count (mset (map f ys)) (f y)"
     if cnt_x: "count (mset xs) x > count (mset ys) x" for x
   proof -
     have x_in_a: "x \<in> A"
       using cnt_x xs_a dual_order.strict_trans2 by fastforce
 
     obtain y where y_gt_x: "gt y x" and cnt_y: "count (mset ys) y > count (mset xs) y"
       using cnt_x ex_gt by blast
     have y_in_a: "y \<in> A"
       using cnt_y ys_a dual_order.strict_trans2 by fastforce
 
     have wf_gt_f: "wfP (\<lambda>y x. y \<in> A \<and> x \<in> A \<and> gt (f y) (f x))"
       by (rule finite_irreflp_transp_imp_wfp)
         (auto elim: trans_f[rule_format] simp: fin irrefl_f Collect_case_prod_Sigma irreflp_def
            transp_def)
 
     obtain yy where
       fyy_gt_fx: "gt (f yy) (f x)" and
       cnt_yy: "count (mset ys) yy > count (mset xs) yy" and
       max_yy: "\<forall>y \<in> A. yy \<in> A \<longrightarrow> gt (f y) (f yy) \<longrightarrow> gt (f y) (f x) \<longrightarrow>
         count (mset xs) y \<ge> count (mset ys) y"
       using wfP_eq_minimal[THEN iffD1, OF wf_gt_f, rule_format,
           of y "{y. gt (f y) (f x) \<and> count (mset xs) y < count (mset ys) y}", simplified]
         y_gt_x cnt_y
       by (metis compat_f not_less x_in_a y_in_a)
     have yy_in_a: "yy \<in> A"
       using cnt_yy ys_a dual_order.strict_trans2 by fastforce
 
     {
       assume "count (mset ?fxs) (f yy) \<ge> count (mset ?fys) (f yy)"
       then obtain u where fu_eq_fyy: "f u = f yy" and cnt_u: "count (mset xs) u > count (mset ys) u"
         using count_image_mset_le_imp_lt cnt_yy mset_map by (metis (mono_tags))
       have u_in_a: "u \<in> A"
         using cnt_u xs_a dual_order.strict_trans2 by fastforce
 
       obtain v where v_gt_u: "gt v u" and cnt_v: "count (mset ys) v > count (mset xs) v"
         using cnt_u ex_gt by blast
       have v_in_a: "v \<in> A"
         using cnt_v ys_a dual_order.strict_trans2 by fastforce
 
       have fv_gt_fu: "gt (f v) (f u)"
         using v_gt_u compat_f v_in_a u_in_a by blast
       hence fv_gt_fyy: "gt (f v) (f yy)"
         by (simp only: fu_eq_fyy)
 
       have "gt (f v) (f x)"
         using fv_gt_fyy fyy_gt_fx v_in_a yy_in_a x_in_a trans_f by blast
       hence False
         using max_yy[rule_format, of v] fv_gt_fyy v_in_a yy_in_a cnt_v by linarith
     }
     thus ?thesis
       using fyy_gt_fx leI by blast
   qed
 
   show ?thesis
     unfolding msetext_huet_def Let_def
   proof (intro conjI allI impI)
     {
       assume len_eq: "length xs = length ys"
       obtain x where cnt_x: "count (mset xs) x > count (mset ys) x"
         using len_eq ms_xs_ne_ys by (metis size_eq_ex_count_lt size_mset)
       hence "mset ?fxs \<noteq> mset ?fys"
         using ex_y by fastforce
     }
     thus "mset ?fxs \<noteq> mset (map f ys)"
       by (metis length_map size_mset)
   next
     fix fx
     assume cnt_fx: "count (mset ?fxs) fx > count (mset ?fys) fx"
     then obtain x where fx: "fx = f x" and cnt_x: "count (mset xs) x > count (mset ys) x"
       using count_image_mset_lt_imp_lt mset_map by (metis (mono_tags))
     thus "\<exists>fy. gt fy fx \<and> count (mset ?fxs) fy < count (mset (map f ys)) fy"
       using ex_y[OF cnt_x] by blast
   qed
 qed
 
 lemma msetext_huet_irrefl: "(\<forall>x \<in> set xs. \<not> gt x x) \<Longrightarrow> \<not> msetext_huet gt xs xs"
   unfolding msetext_huet_def by simp
 
 lemma msetext_huet_trans_from_irrefl:
   assumes
     fin: "finite A" and
     zs_a: "zs \<in> lists A" and ys_a: "ys \<in> lists A" and xs_a: "xs \<in> lists A" and
     irrefl: "\<forall>x \<in> A. \<not> gt x x" and
     trans: "\<forall>z \<in> A. \<forall>y \<in> A. \<forall>x \<in> A. gt z y \<longrightarrow> gt y x \<longrightarrow> gt z x" and
     zs_gt_ys: "msetext_huet gt zs ys" and
     ys_gt_xs: "msetext_huet gt ys xs"
   shows "msetext_huet gt zs xs"
 proof -
   have wf_gt: "wfP (\<lambda>y x. y \<in> A \<and> x \<in> A \<and> gt y x)"
     by (rule finite_irreflp_transp_imp_wfp)
       (auto elim: trans[rule_format] simp: fin irrefl Collect_case_prod_Sigma irreflp_def
          transp_def)
 
   show ?thesis
     unfolding msetext_huet_def Let_def
   proof (intro conjI allI impI)
     obtain x where cnt_x: "count (mset zs) x > count (mset ys) x"
       using msetext_huet_imp_count_gt[OF zs_gt_ys] by blast
     have x_in_a: "x \<in> A"
       using cnt_x zs_a dual_order.strict_trans2 by fastforce
 
     obtain xx where
       cnt_xx: "count (mset zs) xx > count (mset ys) xx" and
       max_xx: "\<forall>y \<in> A. xx \<in> A \<longrightarrow> gt y xx \<longrightarrow> count (mset ys) y \<ge> count (mset zs) y"
       using wfP_eq_minimal[THEN iffD1, OF wf_gt, rule_format,
           of x "{y. count (mset ys) y < count (mset zs) y}", simplified]
         cnt_x
       by force
     have xx_in_a: "xx \<in> A"
       using cnt_xx zs_a dual_order.strict_trans2 by fastforce
 
     show "mset xs \<noteq> mset zs"
     proof (cases "count (mset ys) xx \<ge> count (mset xs) xx")
       case True
       thus ?thesis
         using cnt_xx by fastforce
     next
       case False
       hence "count (mset ys) xx < count (mset xs) xx"
         by fastforce
       then obtain z where z_gt_xx: "gt z xx" and cnt_z: "count (mset ys) z > count (mset xs) z"
         using ys_gt_xs[unfolded msetext_huet_def Let_def] by blast
       have z_in_a: "z \<in> A"
         using cnt_z ys_a dual_order.strict_trans2 by fastforce
 
       have "count (mset zs) z \<le> count (mset ys) z"
         using max_xx[rule_format, of z] z_in_a xx_in_a z_gt_xx by blast
       moreover
       {
         assume "count (mset zs) z < count (mset ys) z"
         then obtain u where u_gt_z: "gt u z" and cnt_u: "count (mset ys) u < count (mset zs) u"
           using zs_gt_ys[unfolded msetext_huet_def Let_def] by blast
         have u_in_a: "u \<in> A"
           using cnt_u zs_a dual_order.strict_trans2 by fastforce
         have u_gt_xx: "gt u xx"
           using trans u_in_a z_in_a xx_in_a u_gt_z z_gt_xx by blast
         have False
           using max_xx[rule_format, of u] u_in_a xx_in_a u_gt_xx cnt_u by fastforce
       }
       ultimately have "count (mset zs) z = count (mset ys) z"
         by fastforce
       thus ?thesis
         using cnt_z by fastforce
     qed
   next
     fix x
     assume cnt_x_xz: "count (mset zs) x < count (mset xs) x"
     have x_in_a: "x \<in> A"
       using cnt_x_xz xs_a dual_order.strict_trans2 by fastforce
 
     let ?case = "\<exists>y. gt y x \<and> count (mset zs) y > count (mset xs) y"
 
     {
       assume cnt_x: "count (mset zs) x < count (mset ys) x"
       then obtain y where y_gt_x: "gt y x" and cnt_y: "count (mset zs) y > count (mset ys) y"
         using zs_gt_ys[unfolded msetext_huet_def Let_def] by blast
       have y_in_a: "y \<in> A"
         using cnt_y zs_a dual_order.strict_trans2 by fastforce
 
       obtain yy where
         yy_gt_x: "gt yy x" and
         cnt_yy: "count (mset zs) yy > count (mset ys) yy" and
         max_yy: "\<forall>y \<in> A. yy \<in> A \<longrightarrow> gt y yy \<longrightarrow> gt y x \<longrightarrow> count (mset ys) y \<ge> count (mset zs) y"
         using wfP_eq_minimal[THEN iffD1, OF wf_gt, rule_format,
             of y "{y. gt y x \<and> count (mset ys) y < count (mset zs) y}", simplified]
           y_gt_x cnt_y
         by force
       have yy_in_a: "yy \<in> A"
         using cnt_yy zs_a dual_order.strict_trans2 by fastforce
 
       have ?case
       proof (cases "count (mset ys) yy \<ge> count (mset xs) yy")
         case True
         thus ?thesis
           using yy_gt_x cnt_yy by fastforce
       next
         case False
         hence "count (mset ys) yy < count (mset xs) yy"
           by fastforce
         then obtain z where z_gt_yy: "gt z yy" and cnt_z: "count (mset ys) z > count (mset xs) z"
           using ys_gt_xs[unfolded msetext_huet_def Let_def] by blast
         have z_in_a: "z \<in> A"
           using cnt_z ys_a dual_order.strict_trans2 by fastforce
         have z_gt_x: "gt z x"
           using trans z_in_a yy_in_a x_in_a z_gt_yy yy_gt_x by blast
 
         have "count (mset zs) z \<le> count (mset ys) z"
           using max_yy[rule_format, of z] z_in_a yy_in_a z_gt_yy z_gt_x by blast
         moreover
         {
           assume "count (mset zs) z < count (mset ys) z"
           then obtain u where u_gt_z: "gt u z" and cnt_u: "count (mset ys) u < count (mset zs) u"
             using zs_gt_ys[unfolded msetext_huet_def Let_def] by blast
           have u_in_a: "u \<in> A"
             using cnt_u zs_a dual_order.strict_trans2 by fastforce
           have u_gt_yy: "gt u yy"
             using trans u_in_a z_in_a yy_in_a u_gt_z z_gt_yy by blast
           have u_gt_x: "gt u x"
             using trans u_in_a z_in_a x_in_a u_gt_z z_gt_x by blast
           have False
             using max_yy[rule_format, of u] u_in_a yy_in_a u_gt_yy u_gt_x cnt_u by fastforce
         }
         ultimately have "count (mset zs) z = count (mset ys) z"
           by fastforce
         thus ?thesis
           using z_gt_x cnt_z by fastforce
       qed
     }
     moreover
     {
       assume "count (mset zs) x \<ge> count (mset ys) x"
       hence "count (mset ys) x < count (mset xs) x"
         using cnt_x_xz by fastforce
       then obtain y where y_gt_x: "gt y x" and cnt_y: "count (mset ys) y > count (mset xs) y"
         using ys_gt_xs[unfolded msetext_huet_def Let_def] by blast
       have y_in_a: "y \<in> A"
         using cnt_y ys_a dual_order.strict_trans2 by fastforce
 
       obtain yy where
         yy_gt_x: "gt yy x" and
         cnt_yy: "count (mset ys) yy > count (mset xs) yy" and
         max_yy: "\<forall>y \<in> A. yy \<in> A \<longrightarrow> gt y yy \<longrightarrow> gt y x \<longrightarrow> count (mset xs) y \<ge> count (mset ys) y"
         using wfP_eq_minimal[THEN iffD1, OF wf_gt, rule_format,
             of y "{y. gt y x \<and> count (mset xs) y < count (mset ys) y}", simplified]
           y_gt_x cnt_y
         by force
       have yy_in_a: "yy \<in> A"
         using cnt_yy ys_a dual_order.strict_trans2 by fastforce
 
       have ?case
       proof (cases "count (mset zs) yy \<ge> count (mset ys) yy")
         case True
         thus ?thesis
           using yy_gt_x cnt_yy by fastforce
       next
         case False
         hence "count (mset zs) yy < count (mset ys) yy"
           by fastforce
         then obtain z where z_gt_yy: "gt z yy" and cnt_z: "count (mset zs) z > count (mset ys) z"
           using zs_gt_ys[unfolded msetext_huet_def Let_def] by blast
         have z_in_a: "z \<in> A"
           using cnt_z zs_a dual_order.strict_trans2 by fastforce
         have z_gt_x: "gt z x"
           using trans z_in_a yy_in_a x_in_a z_gt_yy yy_gt_x by blast
 
         have "count (mset ys) z \<le> count (mset xs) z"
           using max_yy[rule_format, of z] z_in_a yy_in_a z_gt_yy z_gt_x by blast
         moreover
         {
           assume "count (mset ys) z < count (mset xs) z"
           then obtain u where u_gt_z: "gt u z" and cnt_u: "count (mset xs) u < count (mset ys) u"
             using ys_gt_xs[unfolded msetext_huet_def Let_def] by blast
           have u_in_a: "u \<in> A"
             using cnt_u ys_a dual_order.strict_trans2 by fastforce
           have u_gt_yy: "gt u yy"
             using trans u_in_a z_in_a yy_in_a u_gt_z z_gt_yy by blast
           have u_gt_x: "gt u x"
             using trans u_in_a z_in_a x_in_a u_gt_z z_gt_x by blast
           have False
             using max_yy[rule_format, of u] u_in_a yy_in_a u_gt_yy u_gt_x cnt_u by fastforce
         }
         ultimately have "count (mset ys) z = count (mset xs) z"
           by fastforce
         thus ?thesis
           using z_gt_x cnt_z by fastforce
       qed
     }
     ultimately show "\<exists>y. gt y x \<and> count (mset xs) y < count (mset zs) y"
       by fastforce
   qed
 qed
 
 lemma msetext_huet_snoc: "msetext_huet gt (xs @ [x]) xs"
   unfolding msetext_huet_def Let_def by simp
 
 lemma msetext_huet_compat_cons: "msetext_huet gt ys xs \<Longrightarrow> msetext_huet gt (x # ys) (x # xs)"
   unfolding msetext_huet_def Let_def by auto
 
 lemma msetext_huet_compat_snoc: "msetext_huet gt ys xs \<Longrightarrow> msetext_huet gt (ys @ [x]) (xs @ [x])"
   unfolding msetext_huet_def Let_def by auto
 
 lemma msetext_huet_compat_list: "y \<noteq> x \<Longrightarrow> gt y x \<Longrightarrow> msetext_huet gt (xs @ y # xs') (xs @ x # xs')"
   unfolding msetext_huet_def Let_def by auto
 
 lemma msetext_huet_singleton: "y \<noteq> x \<Longrightarrow> msetext_huet gt [y] [x] \<longleftrightarrow> gt y x"
   unfolding msetext_huet_def by simp
 
 lemma msetext_huet_wf: "wfP (\<lambda>x y. gt y x) \<Longrightarrow> wfP (\<lambda>xs ys. msetext_huet gt ys xs)"
   by (erule wfP_subset[OF msetext_dersh_wf]) (auto intro: msetext_huet_imp_dersh)
 
 lemma msetext_huet_hd_or_tl:
   assumes
     trans: "\<forall>z y x. gt z y \<longrightarrow> gt y x \<longrightarrow> gt z x" and
     total: "\<forall>y x. gt y x \<or> gt x y \<or> y = x" and
     len_eq: "length ys = length xs" and
     yys_gt_xxs: "msetext_huet gt (y # ys) (x # xs)"
   shows "gt y x \<or> msetext_huet gt ys xs"
 proof -
   let ?Y = "mset (y # ys)"
   let ?X = "mset (x # xs)"
 
   let ?Ya = "mset ys"
   let ?Xa = "mset xs"
 
   have Y_ne_X: "?Y \<noteq> ?X" and
     ex_gt_Y: "\<And>xa. count ?X xa > count ?Y xa \<Longrightarrow> \<exists>ya. gt ya xa \<and> count ?Y ya > count ?X ya"
     using yys_gt_xxs[unfolded msetext_huet_def Let_def] by auto
   obtain yy where
     yy: "\<And>xa. count ?X xa > count ?Y xa \<Longrightarrow> gt (yy xa) xa \<and> count ?Y (yy xa) > count ?X (yy xa)"
     using ex_gt_Y by metis
 
   have cnt_Y_pres: "count ?Ya xa > count ?Xa xa" if "count ?Y xa > count ?X xa" and "xa \<noteq> y" for xa
     using that by (auto split: if_splits)
   have cnt_X_pres: "count ?Xa xa > count ?Ya xa" if "count ?X xa > count ?Y xa" and "xa \<noteq> x" for xa
     using that by (auto split: if_splits)
 
   {
     assume y_eq_x: "y = x"
     have "?Xa \<noteq> ?Ya"
       using y_eq_x Y_ne_X by simp
     moreover have "\<And>xa. count ?Xa xa > count ?Ya xa \<Longrightarrow> \<exists>ya. gt ya xa \<and> count ?Ya ya > count ?Xa ya"
     proof -
       fix xa :: 'a
       assume a1: "count (mset ys) xa < count (mset xs) xa"
       from ex_gt_Y obtain aa :: "'a \<Rightarrow> 'a" where
         f3: "\<forall>a. \<not> count (mset (y # ys)) a < count (mset (x # xs)) a \<or> gt (aa a) a \<and>
           count (mset (x # xs)) (aa a) < count (mset (y # ys)) (aa a)"
         by (metis (full_types))
       then have f4: "\<And>a. count (mset (x # xs)) (aa a) < count (mset (x # ys)) (aa a) \<or>
           \<not> count (mset (x # ys)) a < count (mset (x # xs)) a"
         using y_eq_x by meson
       have "\<And>a as aa. count (mset ((a::'a) # as)) aa = count (mset as) aa \<or> aa = a"
         by fastforce
       then have "xa = x \<or> count (mset (x # xs)) (aa xa) < count (mset (x # ys)) (aa xa)"
         using f4 a1 by (metis (no_types))
       then show "\<exists>a. gt a xa \<and> count (mset xs) a < count (mset ys) a"
         using f3 y_eq_x a1 by (metis (no_types) Suc_less_eq count_add_mset mset.simps(2))
     qed
     ultimately have "msetext_huet gt ys xs"
       unfolding msetext_huet_def Let_def by simp
   }
   moreover
   {
     assume x_gt_y: "gt x y" and y_ngt_x: "\<not> gt y x"
     hence y_ne_x: "y \<noteq> x"
       by fast
 
     obtain z where z_cnt: "count ?X z > count ?Y z"
       using size_eq_ex_count_lt[of ?Y ?X] size_mset size_mset len_eq Y_ne_X by auto
 
     have Xa_ne_Ya: "?Xa \<noteq> ?Ya"
     proof (cases "z = x")
       case True
       hence "yy z \<noteq> y"
         using y_ngt_x yy z_cnt by blast
       hence "count ?Ya (yy z) > count ?Xa (yy z)"
         using cnt_Y_pres yy z_cnt by blast
       thus ?thesis
         by auto
     next
       case False
       hence "count ?Xa z > count ?Ya z"
         using z_cnt cnt_X_pres by blast
       thus ?thesis
         by auto
     qed
 
     have "\<exists>ya. gt ya xa \<and> count ?Ya ya > count ?Xa ya"
       if xa_cnta: "count ?Xa xa > count ?Ya xa" for xa
     proof (cases "xa = y")
       case xa_eq_y: True
 
       {
         assume "count ?Ya x > count ?Xa x"
         moreover have "gt x xa"
           unfolding xa_eq_y by (rule x_gt_y)
         ultimately have ?thesis
           by fast
       }
       moreover
       {
         assume "count ?Xa x \<ge> count ?Ya x"
         hence x_cnt: "count ?X x > count ?Y x"
           by (simp add: y_ne_x)
         hence yyx_gt_x: "gt (yy x) x" and yyx_cnt: "count ?Y (yy x) > count ?X (yy x)"
           using yy by blast+
 
         have yyx_ne_y: "yy x \<noteq> y"
           using y_ngt_x yyx_gt_x by auto
 
         have "gt (yy x) xa"
           unfolding xa_eq_y using trans yyx_gt_x x_gt_y by blast
         moreover have "count ?Ya (yy x) > count ?Xa (yy x)"
           using cnt_Y_pres yyx_cnt yyx_ne_y by blast
         ultimately have ?thesis
           by blast
       }
       ultimately show ?thesis
         by fastforce
     next
       case False
       hence xa_cnt: "count ?X xa > count ?Y xa"
         using xa_cnta by fastforce
 
       show ?thesis
       proof (cases "yy xa = y \<and> count ?Ya y \<le> count ?Xa y")
         case yyxa_ne_y_or: False
 
         have yyxa_gt_xa: "gt (yy xa) xa" and yyxa_cnt: "count ?Y (yy xa) > count ?X (yy xa)"
           using yy[OF xa_cnt] by blast+
 
         have "count ?Ya (yy xa) > count ?Xa (yy xa)"
           using cnt_Y_pres yyxa_cnt yyxa_ne_y_or by fastforce
         thus ?thesis
           using yyxa_gt_xa by blast
       next
         case True
         note yyxa_eq_y = this[THEN conjunct1] and y_cnt = this[THEN conjunct2]
 
         {
           assume "count ?Ya x > count ?Xa x"
           moreover have "gt x xa"
             using trans x_gt_y xa_cnt yy yyxa_eq_y by blast
           ultimately have ?thesis
             by fast
         }
         moreover
         {
           assume "count ?Xa x \<ge> count ?Ya x"
           hence x_cnt: "count ?X x > count ?Y x"
             by (simp add: y_ne_x)
           hence yyx_gt_x: "gt (yy x) x" and yyx_cnt: "count ?Y (yy x) > count ?X (yy x)"
             using yy by blast+
 
           have yyx_ne_y: "yy x \<noteq> y"
             using y_ngt_x yyx_gt_x by auto
 
           have "gt (yy x) xa"
             using trans x_gt_y xa_cnt yy yyx_gt_x yyxa_eq_y by blast
           moreover have "count ?Ya (yy x) > count ?Xa (yy x)"
             using cnt_Y_pres yyx_cnt yyx_ne_y by blast
           ultimately have ?thesis
             by blast
         }
         ultimately show ?thesis
           by fastforce
       qed
     qed
     hence "msetext_huet gt ys xs"
       unfolding msetext_huet_def Let_def using Xa_ne_Ya by fast
   }
   ultimately show ?thesis
     using total by blast
 qed
 
 interpretation msetext_huet: ext msetext_huet
   by standard (fact msetext_huet_mono_strong, fact msetext_huet_map)
 
 interpretation msetext_huet: ext_irrefl_before_trans msetext_huet
   by standard (fact msetext_huet_irrefl, fact msetext_huet_trans_from_irrefl)
 
 interpretation msetext_huet: ext_snoc msetext_huet
   by standard (fact msetext_huet_snoc)
 
 interpretation msetext_huet: ext_compat_cons msetext_huet
   by standard (fact msetext_huet_compat_cons)
 
 interpretation msetext_huet: ext_compat_snoc msetext_huet
   by standard (fact msetext_huet_compat_snoc)
 
 interpretation msetext_huet: ext_compat_list msetext_huet
   by standard (fact msetext_huet_compat_list)
 
 interpretation msetext_huet: ext_singleton msetext_huet
   by standard (fact msetext_huet_singleton)
 
 interpretation msetext_huet: ext_wf msetext_huet
   by standard (fact msetext_huet_wf)
 
 interpretation msetext_huet: ext_hd_or_tl msetext_huet
   by standard (rule msetext_huet_hd_or_tl)
 
 interpretation msetext_huet: ext_wf_bounded msetext_huet
   by standard
 
 
 subsection \<open>Componentwise Extension\<close>
 
 definition cwiseext :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
   "cwiseext gt ys xs \<longleftrightarrow> length ys = length xs
      \<and> (\<forall>i < length ys. gt (ys ! i) (xs ! i) \<or> ys ! i = xs ! i)
      \<and> (\<exists>i < length ys. gt (ys ! i) (xs ! i))"
 
 lemma cwiseext_imp_len_lexext:
   assumes cw: "cwiseext gt ys xs"
   shows "len_lexext gt ys xs"
 proof -
   have len_eq: "length ys = length xs"
     using cw[unfolded cwiseext_def] by sat
   moreover have "lexext gt ys xs"
   proof -
     obtain j where
       j_len: "j < length ys" and
       j_gt: "gt (ys ! j) (xs ! j)"
       using cw[unfolded cwiseext_def] by blast
     then obtain j0 where
       j0_len: "j0 < length ys" and
       j0_gt: "gt (ys ! j0) (xs ! j0)" and
       j0_min: "\<And>i. i < j0 \<Longrightarrow> \<not> gt (ys ! i) (xs ! i)"
       using wf_eq_minimal[THEN iffD1, OF wf_less, rule_format, of _ "{i. gt (ys ! i) (xs ! i)}",
         simplified, OF j_gt]
       by (metis less_trans nat_neq_iff)
 
     have j0_eq: "\<And>i. i < j0 \<Longrightarrow> ys ! i = xs ! i"
       using cw[unfolded cwiseext_def] by (metis j0_len j0_min less_trans)
 
     have "lexext gt (drop j0 ys) (drop j0 xs)"
       using lexext_Cons[of gt _ _ "drop (Suc j0) ys" "drop (Suc j0) xs", OF j0_gt]
       by (metis Cons_nth_drop_Suc j0_len len_eq)
     thus ?thesis
       using cw len_eq j0_len j0_min
     proof (induct j0 arbitrary: ys xs)
       case (Suc k)
       note ih0 = this(1) and gts_dropSk = this(2) and cw = this(3) and len_eq = this(4) and
         Sk_len = this(5) and Sk_min = this(6)
 
       have Sk_eq: "\<And>i. i < Suc k \<Longrightarrow> ys ! i = xs ! i"
         using cw[unfolded cwiseext_def] by (metis Sk_len Sk_min less_trans)
 
       have k_len: "k < length ys"
         using Sk_len by simp
       have k_min: "\<And>i. i < k \<Longrightarrow> \<not> gt (ys ! i) (xs ! i)"
         using Sk_min by simp
 
       have k_eq: "\<And>i. i < k \<Longrightarrow> ys ! i = xs ! i"
         using Sk_eq by simp
 
       note ih = ih0[OF _ cw len_eq k_len k_min]
 
       show ?case
       proof (cases "k < length ys")
         case k_lt_ys: True
         note k_lt_xs = k_lt_ys[unfolded len_eq]
 
         obtain x where x: "x = xs ! k"
           by simp
         hence y: "x = ys ! k"
           using Sk_eq[of k] by simp
 
         have dropk_xs: "drop k xs = x # drop (Suc k) xs"
           using k_lt_xs x by (simp add: Cons_nth_drop_Suc)
         have dropk_ys: "drop k ys = x # drop (Suc k) ys"
           using k_lt_ys y by (simp add: Cons_nth_drop_Suc)
 
         show ?thesis
           by (rule ih, unfold dropk_xs dropk_ys, rule lexext_Cons_eq[OF gts_dropSk])
       next
         case False
         hence "drop k xs = []" and "drop k ys = []"
           using len_eq by simp_all
         hence "lexext gt [] []"
           using gts_dropSk by simp
         hence "lexext gt (drop k ys) (drop k xs)"
           by simp
         thus ?thesis
           by (rule ih)
       qed
     qed simp
   qed
   ultimately show ?thesis
     unfolding lenext_def by sat
 qed
 
 lemma cwiseext_mono_strong:
   "(\<forall>y \<in> set ys. \<forall>x \<in> set xs. gt y x \<longrightarrow> gt' y x) \<Longrightarrow> cwiseext gt ys xs \<Longrightarrow> cwiseext gt' ys xs"
   unfolding cwiseext_def by (induct, force, fast)
 
 lemma cwiseext_map_strong:
   "(\<forall>y \<in> set ys. \<forall>x \<in> set xs. gt y x \<longrightarrow> gt (f y) (f x)) \<Longrightarrow> cwiseext gt ys xs \<Longrightarrow>
    cwiseext gt (map f ys) (map f xs)"
   unfolding cwiseext_def by auto
 
 lemma cwiseext_irrefl: "(\<forall>x \<in> set xs. \<not> gt x x) \<Longrightarrow> \<not> cwiseext gt xs xs"
   unfolding cwiseext_def by (blast intro: nth_mem)
 
 lemma cwiseext_trans_strong:
   assumes
     "\<forall>z \<in> set zs. \<forall>y \<in> set ys. \<forall>x \<in> set xs. gt z y \<longrightarrow> gt y x \<longrightarrow> gt z x" and
     "cwiseext gt zs ys" and "cwiseext gt ys xs"
   shows "cwiseext gt zs xs"
   using assms unfolding cwiseext_def by (metis (mono_tags) nth_mem)
 
 lemma cwiseext_compat_cons: "cwiseext gt ys xs \<Longrightarrow> cwiseext gt (x # ys) (x # xs)"
   unfolding cwiseext_def
 proof (elim conjE, intro conjI)
   assume
     "length ys = length xs" and
     "\<forall>i < length ys. gt (ys ! i) (xs ! i) \<or> ys ! i = xs ! i"
   thus "\<forall>i < length (x # ys). gt ((x # ys) ! i) ((x # xs) ! i) \<or> (x # ys) ! i = (x # xs) ! i"
     by (simp add: nth_Cons')
 next
   assume "\<exists>i < length ys. gt (ys ! i) (xs ! i)"
   thus "\<exists>i < length (x # ys). gt ((x # ys) ! i) ((x # xs) ! i)"
     by fastforce
 qed auto
 
 lemma cwiseext_compat_snoc: "cwiseext gt ys xs \<Longrightarrow> cwiseext gt (ys @ [x]) (xs @ [x])"
   unfolding cwiseext_def
 proof (elim conjE, intro conjI)
   assume
     "length ys = length xs" and
     "\<forall>i < length ys. gt (ys ! i) (xs ! i) \<or> ys ! i = xs ! i"
   thus "\<forall>i < length (ys @ [x]).
     gt ((ys @ [x]) ! i) ((xs @ [x]) ! i) \<or> (ys @ [x]) ! i = (xs @ [x]) ! i"
     by (simp add: nth_append)
 next
   assume
     "length ys = length xs" and
     "\<exists>i < length ys. gt (ys ! i) (xs ! i)"
   thus "\<exists>i < length (ys @ [x]). gt ((ys @ [x]) ! i) ((xs @ [x]) ! i)"
     by (metis length_append_singleton less_Suc_eq nth_append)
 qed auto
 
 lemma cwiseext_compat_list:
   assumes y_gt_x: "gt y x"
   shows "cwiseext gt (xs @ y # xs') (xs @ x # xs')"
   unfolding cwiseext_def
 proof (intro conjI)
   show "\<forall>i < length (xs @ y # xs'). gt ((xs @ y # xs') ! i) ((xs @ x # xs') ! i)
     \<or> (xs @ y # xs') ! i = (xs @ x # xs') ! i"
     using y_gt_x by (simp add: nth_Cons' nth_append)
 next
   show "\<exists>i < length (xs @ y # xs'). gt ((xs @ y # xs') ! i) ((xs @ x # xs') ! i)"
     using y_gt_x by (metis add_diff_cancel_right' append_is_Nil_conv diff_less length_append
       length_greater_0_conv list.simps(3) nth_append_length)
 qed auto
 
 lemma cwiseext_singleton: "cwiseext gt [y] [x] \<longleftrightarrow> gt y x"
   unfolding cwiseext_def by auto
 
 lemma cwiseext_wf: "wfP (\<lambda>x y. gt y x) \<Longrightarrow> wfP (\<lambda>xs ys. cwiseext gt ys xs)"
   by (auto intro: cwiseext_imp_len_lexext wfP_subset[OF len_lexext_wf])
 
 lemma cwiseext_hd_or_tl: "cwiseext gt (y # ys) (x # xs) \<Longrightarrow> gt y x \<or> cwiseext gt ys xs"
   unfolding cwiseext_def
 proof (elim conjE, intro disj_imp[THEN iffD2, rule_format] conjI)
   assume
     "\<exists>i < length (y # ys). gt ((y # ys) ! i) ((x # xs) ! i)" and
     "\<not> gt y x"
   thus "\<exists>i < length ys. gt (ys ! i) (xs ! i)"
     by (metis (no_types) One_nat_def diff_le_self diff_less dual_order.strict_trans2
       length_Cons less_Suc_eq linorder_neqE_nat not_less0 nth_Cons')
 qed auto
 
 locale ext_cwiseext = ext_compat_list + ext_compat_cons
 begin
 
 context
   fixes gt :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   assumes
     gt_irrefl: "\<not> gt x x" and
     trans_gt: "ext gt zs ys \<Longrightarrow> ext gt ys xs \<Longrightarrow> ext gt zs xs"
 begin
 
 lemma
   assumes ys_gtcw_xs: "cwiseext gt ys xs"
   shows "ext gt ys xs"
 proof -
   have "length ys = length xs"
     by (rule ys_gtcw_xs[unfolded cwiseext_def, THEN conjunct1])
   thus ?thesis
     using ys_gtcw_xs
   proof (induct rule: list_induct2)
     case Nil
     thus ?case
       unfolding cwiseext_def by simp
   next
     case (Cons y ys x xs)
     note len_ys_eq_xs = this(1) and ih = this(2) and yys_gtcw_xxs = this(3)
 
     have xys_gts_xxs: "ext gt (x # ys) (x # xs)" if ys_ne_xs: "ys \<noteq> xs"
     proof -
       have ys_gtcw_xs: "cwiseext gt ys xs"
         using yys_gtcw_xxs unfolding cwiseext_def
       proof (elim conjE, intro conjI)
         assume
           "\<forall>i < length (y # ys). gt ((y # ys) ! i) ((x # xs) ! i) \<or> (y # ys) ! i = (x # xs) ! i"
         hence ge: "\<forall>i < length ys. gt (ys ! i) (xs ! i) \<or> ys ! i = xs ! i"
           by auto
         thus "\<exists>i < length ys. gt (ys ! i) (xs ! i)"
           using ys_ne_xs len_ys_eq_xs nth_equalityI by blast
       qed auto
       hence "ext gt ys xs"
         by (rule ih)
       thus "ext gt (x # ys) (x # xs)"
         by (rule compat_cons)
     qed
 
     have "gt y x \<or> y = x"
       using yys_gtcw_xxs unfolding cwiseext_def by fastforce
     moreover
     {
       assume y_eq_x: "y = x"
       have ?case
       proof (cases "ys = xs")
         case True
         hence False
           using y_eq_x gt_irrefl yys_gtcw_xxs unfolding cwiseext_def by presburger
         thus ?thesis
           by sat
       next
         case False
         thus ?thesis
           using y_eq_x xys_gts_xxs by simp
       qed
     }
     moreover
     {
       assume "y \<noteq> x" and "gt y x"
       hence yys_gts_xys: "ext gt (y # ys) (x # ys)"
         using compat_list[of _ _ gt "[]"] by simp
 
       have ?case
       proof (cases "ys = xs")
         case ys_eq_xs: True
         thus ?thesis
           using yys_gts_xys by simp
       next
         case False
         thus ?thesis
           using yys_gts_xys xys_gts_xxs trans_gt by blast
       qed
     }
     ultimately show ?case
       by sat
   qed
 qed
 
 end
 
 end
 
 interpretation cwiseext: ext cwiseext
   by standard (fact cwiseext_mono_strong, rule cwiseext_map_strong, metis in_listsD)
 
 interpretation cwiseext: ext_irrefl_trans_strong cwiseext
   by standard (fact cwiseext_irrefl, fact cwiseext_trans_strong)
 
 interpretation cwiseext: ext_compat_cons cwiseext
   by standard (fact cwiseext_compat_cons)
 
 interpretation cwiseext: ext_compat_snoc cwiseext
   by standard (fact cwiseext_compat_snoc)
 
 interpretation cwiseext: ext_compat_list cwiseext
   by standard (rule cwiseext_compat_list)
 
 interpretation cwiseext: ext_singleton cwiseext
   by standard (rule cwiseext_singleton)
 
 interpretation cwiseext: ext_wf cwiseext
   by standard (rule cwiseext_wf)
 
 interpretation cwiseext: ext_hd_or_tl cwiseext
   by standard (rule cwiseext_hd_or_tl)
 
 interpretation cwiseext: ext_wf_bounded cwiseext
   by standard
 
-(* TODO: move ? *)
-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(1) assms(2) by auto
-qed
-
 end
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,970 +1,986 @@
 (*  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"
 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_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!]
 
 
 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: mset_filter 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]
 
 
 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>
 
 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 [simp]: "mset (list_of_mset m) = m"
   by (metis (mono_tags, lifting) ex_mset list_of_mset_def 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
 
 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(1) assms(2) by auto
+qed
+
 end