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,2054 +1,2054 @@
 (*  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)
+  by (auto dest: nonempty_subseteq_mset_eq_single simp: nonempty_subseteq_mset_iff_single)
 
 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 (rule multiset_eqI) simp
   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
 
 end
diff --git a/thys/Lambda_Free_RPOs/Lambda_Free_Util.thy b/thys/Lambda_Free_RPOs/Lambda_Free_Util.thy
--- a/thys/Lambda_Free_RPOs/Lambda_Free_Util.thy
+++ b/thys/Lambda_Free_RPOs/Lambda_Free_Util.thy
@@ -1,626 +1,347 @@
 (*  Title:       Utilities for Lambda-Free Orders
     Author:      Jasmin Blanchette <jasmin.blanchette at inria.fr>, 2016
     Maintainer:  Jasmin Blanchette <jasmin.blanchette at inria.fr>
 *)
 
 section \<open>Utilities for Lambda-Free Orders\<close>
 
 theory Lambda_Free_Util
 imports "HOL-Library.Extended_Nat" "HOL-Library.Multiset_Order"
 begin
 
 text \<open>
 This theory gathers various lemmas that likely belong elsewhere in Isabelle or
 the \emph{Archive of Formal Proofs}. Most (but certainly not all) of them are
 used to formalize orders on \<open>\<lambda>\<close>-free higher-order terms.
 \<close>
 
-subsection \<open>Finite Sets\<close>
-
-lemma finite_set_fold_singleton[simp]: "Finite_Set.fold f z {x} = f x z"
-proof -
-  have "fold_graph f z {x} (f x z)"
-    by (auto intro: fold_graph.intros)
-  moreover
-  {
-    fix X y
-    have "fold_graph f z X y \<Longrightarrow> (X = {} \<longrightarrow> y = z) \<and> (X = {x} \<longrightarrow> y = f x z)"
-      by (induct rule: fold_graph.induct) auto
-  }
-  ultimately have "(THE y. fold_graph f z {x} y) = f x z"
-    by blast
-  thus ?thesis
-    by (simp add: Finite_Set.fold_def)
-qed
-
-
 subsection \<open>Function Power\<close>
 
 lemma funpow_lesseq_iter:
   fixes f :: "('a::order) \<Rightarrow> 'a"
   assumes mono: "\<And>k. k \<le> f k" and m_le_n: "m \<le> n"
   shows "(f ^^ m) k \<le> (f ^^ n) k"
   using m_le_n by (induct n) (fastforce simp: le_Suc_eq intro: mono order_trans)+
 
 lemma funpow_less_iter:
   fixes f :: "('a::order) \<Rightarrow> 'a"
   assumes mono: "\<And>k. k < f k" and m_lt_n: "m < n"
   shows "(f ^^ m) k < (f ^^ n) k"
   using m_lt_n by (induct n) (auto, blast intro: mono less_trans dest: less_antisym)
 
 
 subsection \<open>Least Operator\<close>
 
 lemma Least_eq[simp]: "(LEAST y. y = x) = x" and "(LEAST y. x = y) = x" for x :: "'a::order"
   by (blast intro: Least_equality)+
 
 lemma Least_in_nonempty_set_imp_ex:
   fixes f :: "'b \<Rightarrow> ('a::wellorder)"
   assumes
     A_nemp: "A \<noteq> {}" and
     P_least: "P (LEAST y. \<exists>x \<in> A. y = f x)"
   shows "\<exists>x \<in> A. P (f x)"
 proof -
   obtain a where a: "a \<in> A"
     using A_nemp by fast
   have "\<exists>x. x \<in> A \<and> (LEAST y. \<exists>x. x \<in> A \<and> y = f x) = f x"
     by (rule LeastI[of _ "f a"]) (fast intro: a)
   thus ?thesis
     by (metis P_least)
 qed
 
 lemma Least_eq_0_enat: "P 0 \<Longrightarrow> (LEAST x :: enat. P x) = 0"
   by (simp add: Least_equality)
 
 
 subsection \<open>Antisymmetric Relations\<close>
 
 lemma irrefl_trans_imp_antisym: "irrefl r \<Longrightarrow> trans r \<Longrightarrow> antisym r"
   unfolding irrefl_def trans_def antisym_def by fast
 
 lemma irreflp_transp_imp_antisymP: "irreflp p \<Longrightarrow> transp p \<Longrightarrow> antisymp p"
   by (fact irrefl_trans_imp_antisym [to_pred])
 
 
 subsection \<open>Acyclic Relations\<close>
 
 lemma finite_nonempty_ex_succ_imp_cyclic:
   assumes
     fin: "finite A" and
     nemp: "A \<noteq> {}" and
     ex_y: "\<forall>x \<in> A. \<exists>y \<in> A. (y, x) \<in> r"
   shows "\<not> acyclic r"
 proof -
   let ?R = "{(x, y). x \<in> A \<and> y \<in> A \<and> (x, y) \<in> r}"
 
   have R_sub_r: "?R \<subseteq> r"
     by auto
 
   have "?R \<subseteq> A \<times> A"
     by auto
   hence fin_R: "finite ?R"
     by (auto intro: fin dest!: infinite_super)
 
   have "\<not> acyclic ?R"
     by (rule notI, drule finite_acyclic_wf[OF fin_R], unfold wf_eq_minimal, drule spec[of _ A],
       use ex_y nemp in blast)
   thus ?thesis
     using R_sub_r acyclic_subset by auto
 qed
 
 
 subsection \<open>Reflexive, Transitive Closure\<close>
 
 lemma relcomp_subset_left_imp_relcomp_trancl_subset_left:
   assumes sub: "R O S \<subseteq> R"
   shows "R O S\<^sup>* \<subseteq> R"
 proof
   fix x
   assume "x \<in> R O S\<^sup>*"
   then obtain n where "x \<in> R O S ^^ n"
     using rtrancl_imp_relpow by fastforce
   thus "x \<in> R"
   proof (induct n)
     case (Suc m)
     thus ?case
       by (metis (no_types) O_assoc inf_sup_ord(3) le_iff_sup relcomp_distrib2 relpow.simps(2)
         relpow_commute sub subsetCE)
   qed auto
 qed
 
 lemma f_chain_in_rtrancl:
   assumes m_le_n: "m \<le> n" and f_chain: "\<forall>i \<in> {m..<n}. (f i, f (Suc i)) \<in> R"
   shows "(f m, f n) \<in> R\<^sup>*"
 proof (rule relpow_imp_rtrancl, rule relpow_fun_conv[THEN iffD2], intro exI conjI)
   let ?g = "\<lambda>i. f (m + i)"
   let ?k = "n - m"
 
   show "?g 0 = f m"
     by simp
   show "?g ?k = f n"
     using m_le_n by force
   show "(\<forall>i < ?k. (?g i, ?g (Suc i)) \<in> R)"
     by (simp add: f_chain)
 qed
 
 lemma f_rev_chain_in_rtrancl:
   assumes m_le_n: "m \<le> n" and f_chain: "\<forall>i \<in> {m..<n}. (f (Suc i), f i) \<in> R"
   shows "(f n, f m) \<in> R\<^sup>*"
   by (rule f_chain_in_rtrancl[OF m_le_n, of "\<lambda>i. f (n + m - i)", simplified])
     (metis f_chain le_add_diff Suc_diff_Suc Suc_leI atLeastLessThan_iff diff_Suc_diff_eq1 diff_less
       le_add1 less_le_trans zero_less_Suc)
 
 
 subsection \<open>Well-Founded Relations\<close>
 
 lemma wf_app: "wf r \<Longrightarrow> wf {(x, y). (f x, f y) \<in> r}"
   unfolding wf_eq_minimal by (intro allI, drule spec[of _ "f ` Q" for Q]) fast
 
 lemma wfP_app: "wfP p \<Longrightarrow> wfP (\<lambda>x y. p (f x) (f y))"
   unfolding wfP_def by (rule wf_app[of "{(x, y). p x y}" f, simplified])
 
 lemma wf_exists_minimal:
   assumes wf: "wf r" and Q: "Q x"
   shows "\<exists>x. Q x \<and> (\<forall>y. (f y, f x) \<in> r \<longrightarrow> \<not> Q y)"
   using wf_eq_minimal[THEN iffD1, OF wf_app[OF wf], rule_format, of _ "{x. Q x}", simplified, OF Q]
   by blast
 
 lemma wfP_exists_minimal:
   assumes wf: "wfP p" and Q: "Q x"
   shows "\<exists>x. Q x \<and> (\<forall>y. p (f y) (f x) \<longrightarrow> \<not> Q y)"
   by (rule wf_exists_minimal[of "{(x, y). p x y}" Q x, OF wf[unfolded wfP_def] Q, simplified])
 
 lemma finite_irrefl_trans_imp_wf: "finite r \<Longrightarrow> irrefl r \<Longrightarrow> trans r \<Longrightarrow> wf r"
   by (erule finite_acyclic_wf) (simp add: acyclic_irrefl)
 
 lemma finite_irreflp_transp_imp_wfp:
   "finite {(x, y). p x y} \<Longrightarrow> irreflp p \<Longrightarrow> transp p \<Longrightarrow> wfP p"
   using finite_irrefl_trans_imp_wf[of "{(x, y). p x y}"]
   unfolding wfP_def transp_def irreflp_def trans_def irrefl_def mem_Collect_eq prod.case
   by assumption
 
 lemma wf_infinite_down_chain_compatible:
   assumes
     wf_R: "wf R" and
     inf_chain_RS: "\<forall>i. (f (Suc i), f i) \<in> R \<union> S" and
     O_subset: "R O S \<subseteq> R"
   shows "\<exists>k. \<forall>i. (f (Suc (i + k)), f (i + k)) \<in> S"
 proof (rule ccontr)
   assume "\<nexists>k. \<forall>i. (f (Suc (i + k)), f (i + k)) \<in> S"
   hence "\<forall>k. \<exists>i. (f (Suc (i + k)), f (i + k)) \<notin> S"
     by blast
   hence "\<forall>k. \<exists>i > k. (f (Suc i), f i) \<notin> S"
     by (metis add.commute add_Suc less_add_Suc1)
   hence "\<forall>k. \<exists>i > k. (f (Suc i), f i) \<in> R"
     using inf_chain_RS by blast
   hence "\<exists>i > k. (f (Suc i), f i) \<in> R \<and> (\<forall>j > k. (f (Suc j), f j) \<in> R \<longrightarrow> j \<ge> i)" for k
     using wf_eq_minimal[THEN iffD1, OF wf_less, rule_format,
       of _ "{i. i > k \<and> (f (Suc i), f i) \<in> R}", simplified]
     by (meson not_less)
   then obtain j_of where
     j_of_gt: "\<And>k. j_of k > k" and
     j_of_in_R: "\<And>k. (f (Suc (j_of k)), f (j_of k)) \<in> R" and
     j_of_min: "\<And>k. \<forall>j > k. (f (Suc j), f j) \<in> R \<longrightarrow> j \<ge> j_of k"
     by moura
 
   have j_of_min_s: "\<And>k j. j > k \<Longrightarrow> j < j_of k \<Longrightarrow> (f (Suc j), f j) \<in> S"
     using j_of_min inf_chain_RS by fastforce
 
   define g :: "nat \<Rightarrow> 'a" where "\<And>k. g k = f (Suc ((j_of ^^ k) 0))"
 
   have between_g[simplified]: "(f ((j_of ^^ (Suc i)) 0), f (Suc ((j_of ^^ i) 0))) \<in> S\<^sup>*" for i
   proof (rule f_rev_chain_in_rtrancl; clarify?)
     show "Suc ((j_of ^^ i) 0) \<le> (j_of ^^ Suc i) 0"
       using j_of_gt by (simp add: Suc_leI)
   next
     fix ia
     assume ia: "ia \<in> {Suc ((j_of ^^ i) 0)..<(j_of ^^ Suc i) 0}"
     have ia_gt: "ia > (j_of ^^ i) 0"
       using ia by auto
     have ia_lt: "ia < j_of ((j_of ^^ i) 0)"
       using ia by auto
     show "(f (Suc ia), f ia) \<in> S"
       by (rule j_of_min_s[OF ia_gt ia_lt])
   qed
 
   have "\<And>i. (g (Suc i), g i) \<in> R"
     unfolding g_def funpow.simps comp_def
     by (rule subsetD[OF relcomp_subset_left_imp_relcomp_trancl_subset_left[OF O_subset]])
       (rule relcompI[OF j_of_in_R between_g])
   moreover have "\<forall>f. \<exists>i. (f (Suc i), f i) \<notin> R"
     using wf_R[unfolded wf_iff_no_infinite_down_chain] by blast
   ultimately show False
     by blast
 qed
 
 
 subsection \<open>Wellorders\<close>
 
 lemma (in wellorder) exists_minimal:
   fixes x :: 'a
   assumes "P x"
   shows "\<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> y \<ge> x)"
   using assms by (auto intro: LeastI Least_le)
 
 
 subsection \<open>Lists\<close>
 
 lemma rev_induct2[consumes 1, case_names Nil snoc]:
   "length xs = length ys \<Longrightarrow> P [] [] \<Longrightarrow>
    (\<And>x xs y ys. length xs = length ys \<Longrightarrow> P xs ys \<Longrightarrow> P (xs @ [x]) (ys @ [y])) \<Longrightarrow> P xs ys"
 proof (induct xs arbitrary: ys rule: rev_induct)
   case (snoc x xs ys)
   thus ?case
     by (induct ys rule: rev_induct) simp_all
 qed auto
 
 lemma hd_in_set: "length xs \<noteq> 0 \<Longrightarrow> hd xs \<in> set xs"
   by (cases xs) auto
 
 lemma in_lists_iff_set: "xs \<in> lists A \<longleftrightarrow> set xs \<subseteq> A"
   by fast
 
 lemma butlast_append_Cons[simp]: "butlast (xs @ y # ys) = xs @ butlast (y # ys)"
   using butlast_append[of xs "y # ys", simplified] by simp
 
 lemma rev_in_lists[simp]: "rev xs \<in> lists A \<longleftrightarrow> xs \<in> lists A"
   by auto
 
 lemma hd_le_sum_list:
   fixes xs :: "'a::ordered_ab_semigroup_monoid_add_imp_le list"
   assumes "xs \<noteq> []" and "\<forall>i < length xs. xs ! i \<ge> 0"
   shows "hd xs \<le> sum_list xs"
   using assms
   by (induct xs rule: rev_induct, simp_all,
     metis add_cancel_right_left add_increasing2 hd_append2 lessI less_SucI list.sel(1) nth_append
       nth_append_length order_refl self_append_conv2 sum_list.Nil)
 
 lemma sum_list_ge_length_times:
   fixes a :: "'a::{ordered_ab_semigroup_add,semiring_1}"
   assumes "\<forall>i < length xs. xs ! i \<ge> a"
   shows "sum_list xs \<ge> of_nat (length xs) * a"
   using assms
 proof (induct xs)
   case (Cons x xs)
   note ih = this(1) and xxs_i_ge_a = this(2)
 
   have xs_i_ge_a: "\<forall>i < length xs. xs ! i \<ge> a"
     using xxs_i_ge_a by auto
 
   have "x \<ge> a"
     using xxs_i_ge_a by auto
   thus ?case
     using ih[OF xs_i_ge_a] by (simp add: ring_distribs ordered_ab_semigroup_add_class.add_mono)
 qed auto
 
 lemma prod_list_nonneg:
   fixes xs :: "('a :: {ordered_semiring_0,linordered_nonzero_semiring}) list"
   assumes "\<And>x. x \<in> set xs \<Longrightarrow> x \<ge> 0"
   shows "prod_list xs \<ge> 0"
   using assms by (induct xs) auto
 
 lemma zip_append_0_upt:
   "zip (xs @ ys) [0..<length xs + length ys] =
    zip xs [0..<length xs] @ zip ys [length xs..<length xs + length ys]"
 proof (induct ys arbitrary: xs)
   case (Cons y ys)
   note ih = this
   show ?case
     using ih[of "xs @ [y]"] by (simp, cases ys, simp, simp add: upt_rec)
 qed auto
 
 lemma zip_eq_butlast_last:
   assumes len_gt0: "length xs > 0" and len_eq: "length xs = length ys"
   shows "zip xs ys = zip (butlast xs) (butlast ys) @ [(last xs, last ys)]"
   using len_eq len_gt0 by (induct rule: list_induct2) auto
 
 
 subsection \<open>Extended Natural Numbers\<close>
 
 lemma the_enat_0[simp]: "the_enat 0 = 0"
   by (simp add: zero_enat_def)
 
 lemma the_enat_1[simp]: "the_enat 1 = 1"
   by (simp add: one_enat_def)
 
 lemma enat_le_minus_1_imp_lt: "m \<le> n - 1 \<Longrightarrow> n \<noteq> \<infinity> \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> m < n" for m n :: enat
   by (cases m; cases n; simp add: zero_enat_def one_enat_def)
 
 lemma enat_diff_diff_eq: "k - m - n = k - (m + n)" for k m n :: enat
   by (cases k; cases m; cases n) auto
 
 lemma enat_sub_add_same[intro]: "n \<le> m \<Longrightarrow> m = m - n + n" for m n :: enat
   by (cases m; cases n) auto
 
 lemma enat_the_enat_iden[simp]: "n \<noteq> \<infinity> \<Longrightarrow> enat (the_enat n) = n"
   by auto
 
 lemma the_enat_minus_nat: "m \<noteq> \<infinity> \<Longrightarrow> the_enat (m - enat n) = the_enat m - n"
   by auto
 
 lemma enat_the_enat_le: "enat (the_enat x) \<le> x"
   by (cases x; simp)
 
 lemma enat_the_enat_minus_le: "enat (the_enat (x - y)) \<le> x"
   by (cases x; cases y; simp)
 
 lemma enat_le_imp_minus_le: "k \<le> m \<Longrightarrow> k - n \<le> m" for k m n :: enat
   by (metis Groups.add_ac(2) enat_diff_diff_eq enat_ord_simps(3) enat_sub_add_same
     enat_the_enat_iden enat_the_enat_minus_le idiff_0_right idiff_infinity idiff_infinity_right
     order_trans_rules(23) plus_enat_simps(3))
 
 lemma add_diff_assoc2_enat: "m \<ge> n \<Longrightarrow> m - n + p = m + p - n" for m n p :: enat
   by (cases m; cases n; cases p; auto)
 
 lemma enat_mult_minus_distrib: "enat x * (y - z) = enat x * y - enat x * z"
   by (cases y; cases z; auto simp: enat_0 right_diff_distrib')
 
 
 subsection \<open>Multisets\<close>
 
-lemma add_mset_lt_left_lt: "a < b \<Longrightarrow> add_mset a A < add_mset b A"
-  unfolding less_multiset\<^sub>H\<^sub>O by auto
-
-lemma add_mset_le_left_le: "a \<le> b \<Longrightarrow> add_mset a A \<le> add_mset b A" for a :: "'a :: linorder"
-  unfolding less_multiset\<^sub>H\<^sub>O by auto
-
-lemma add_mset_lt_right_lt: "A < B \<Longrightarrow> add_mset a A < add_mset a B"
-  unfolding less_multiset\<^sub>H\<^sub>O by auto
-
-lemma add_mset_le_right_le: "A \<le> B \<Longrightarrow> add_mset a A \<le> add_mset a B"
-  unfolding less_multiset\<^sub>H\<^sub>O by auto
-
-lemma add_mset_lt_lt_lt:
-  assumes a_lt_b: "a < b" and A_le_B: "A < B"
-  shows "add_mset a A < add_mset b B"
-  by (rule less_trans[OF add_mset_lt_left_lt[OF a_lt_b] add_mset_lt_right_lt[OF A_le_B]])
-
-lemma add_mset_lt_lt_le: "a < b \<Longrightarrow> A \<le> B \<Longrightarrow> add_mset a A < add_mset b B"
-  using add_mset_lt_lt_lt le_neq_trans by fastforce
-
-lemma add_mset_lt_le_lt: "a \<le> b \<Longrightarrow> A < B \<Longrightarrow> add_mset a A < add_mset b B" for a :: "'a :: linorder"
-  using add_mset_lt_lt_lt by (metis add_mset_lt_right_lt le_less)
-
-lemma add_mset_le_le_le:
-  fixes a :: "'a :: linorder"
-  assumes a_le_b: "a \<le> b" and A_le_B: "A \<le> B"
-  shows "add_mset a A \<le> add_mset b B"
-  by (rule order.trans[OF add_mset_le_left_le[OF a_le_b] add_mset_le_right_le[OF A_le_B]])
-
-declare filter_eq_replicate_mset [simp] image_mset_subseteq_mono [intro]
-
-lemma nonempty_subseteq_mset_eq_singleton: "M \<noteq> {#} \<Longrightarrow> M \<subseteq># {#x#} \<Longrightarrow> M = {#x#}"
-  by (cases M) (auto dest: subset_mset.diff_add)
-
-lemma nonempty_subseteq_mset_iff_singleton: "(M \<noteq> {#} \<and> M \<subseteq># {#x#} \<and> P) \<longleftrightarrow> M = {#x#} \<and> P"
-  by (cases M) (auto dest: subset_mset.diff_add)
-
-lemma count_gt_imp_in_mset[intro]: "count M x > n \<Longrightarrow> x \<in># M"
-  using count_greater_zero_iff by fastforce
-
-lemma size_lt_imp_ex_count_lt: "size M < size N \<Longrightarrow> \<exists>x \<in># N. count M x < count N x"
-  by (metis count_eq_zero_iff leD not_le_imp_less not_less_zero size_mset_mono subseteq_mset_def)
-
-lemma filter_filter_mset[simp]: "{#x \<in># {#x \<in># M. Q x#}. P x#} = {#x \<in># M. P x \<and> Q x#}"
-  by (induct M) auto
-
-lemma size_filter_unsat_elem:
-  assumes "x \<in># M" and "\<not> P x"
-  shows "size {#x \<in># M. P x#} < size M"
-proof -
-  have "size (filter_mset P M) \<noteq> size M"
-    using assms by (metis add.right_neutral add_diff_cancel_left' count_filter_mset mem_Collect_eq
-      multiset_partition nonempty_has_size set_mset_def size_union)
-  then show ?thesis
-    by (meson leD nat_neq_iff size_filter_mset_lesseq)
-qed
-
-lemma size_filter_ne_elem: "x \<in># M \<Longrightarrow> size {#y \<in># M. y \<noteq> x#} < size M"
-  by (simp add: size_filter_unsat_elem[of x M "\<lambda>y. y \<noteq> x"])
-
-lemma size_eq_ex_count_lt:
-  assumes
-    sz_m_eq_n: "size M = size N" and
-    m_eq_n: "M \<noteq> N"
-  shows "\<exists>x. count M x < count N x"
-proof -
-  obtain x where "count M x \<noteq> count N x"
-    using m_eq_n by (meson multiset_eqI)
-  moreover
-  {
-    assume "count M x < count N x"
-    hence ?thesis
-      by blast
-  }
-  moreover
-  {
-    assume cnt_x: "count M x > count N x"
-
-    have "size {#y \<in># M. y = x#} + size {#y \<in># M. y \<noteq> x#} =
-      size {#y \<in># N. y = x#} + size {#y \<in># N. y \<noteq> x#}"
-      using sz_m_eq_n multiset_partition by (metis size_union)
-    hence sz_m_minus_x: "size {#y \<in># M. y \<noteq> x#} < size {#y \<in># N. y \<noteq> x#}"
-      using cnt_x by simp
-    then obtain y where "count {#y \<in># M. y \<noteq> x#} y < count {#y \<in># N. y \<noteq> x#} y"
-      using size_lt_imp_ex_count_lt[OF sz_m_minus_x] by blast
-    hence "count M y < count N y"
-      by (metis count_filter_mset less_asym)
-    hence ?thesis
-      by blast
-  }
-  ultimately show ?thesis
-    by fastforce
-qed
-
-lemma count_image_mset_lt_imp_lt_raw:
-  assumes
-    "finite A" and
-    "A = set_mset M \<union> set_mset N" and
-    "count (image_mset f M) b < count (image_mset f N) b"
-  shows "\<exists>x. f x = b \<and> count M x < count N x"
-  using assms
-proof (induct A arbitrary: M N b rule: finite_induct)
-  case (insert x F)
-  note fin = this(1) and x_ni_f = this(2) and ih = this(3) and x_f_eq_m_n = this(4) and
-    cnt_b = this(5)
-
-  let ?Ma = "{#y \<in># M. y \<noteq> x#}"
-  let ?Mb = "{#y \<in># M. y = x#}"
-  let ?Na = "{#y \<in># N. y \<noteq> x#}"
-  let ?Nb = "{#y \<in># N. y = x#}"
-
-  have m_part: "M = ?Mb + ?Ma" and n_part: "N = ?Nb + ?Na"
-    using multiset_partition by blast+
-
-  have f_eq_ma_na: "F = set_mset ?Ma \<union> set_mset ?Na"
-    using x_f_eq_m_n x_ni_f by auto
-
-  show ?case
-  proof (cases "count (image_mset f ?Ma) b < count (image_mset f ?Na) b")
-    case cnt_ba: True
-    obtain xa where "f xa = b" and "count ?Ma xa < count ?Na xa"
-      using ih[OF f_eq_ma_na cnt_ba] by blast
-    thus ?thesis
-      by (metis count_filter_mset not_less0)
-  next
-    case cnt_ba: False
-    have fx_eq_b: "f x = b"
-      using cnt_b cnt_ba by (subst (asm) m_part, subst (asm) n_part, auto, presburger)
-    moreover have "count M x < count N x"
-      using cnt_b cnt_ba by (subst (asm) m_part, subst (asm) n_part, auto simp: fx_eq_b)
-    ultimately show ?thesis
-      by blast
-  qed
-qed auto
-
-lemma count_image_mset_lt_imp_lt:
-  assumes cnt_b: "count (image_mset f M) b < count (image_mset f N) b"
-  shows "\<exists>x. f x = b \<and> count M x < count N x"
-  by (rule count_image_mset_lt_imp_lt_raw[of "set_mset M \<union> set_mset N", OF _ refl cnt_b]) auto
-
-lemma count_image_mset_le_imp_lt_raw:
-  assumes
-    "finite A" and
-    "A = set_mset M \<union> set_mset N" and
-    "count (image_mset f M) (f a) + count N a < count (image_mset f N) (f a) + count M a"
-  shows "\<exists>b. f b = f a \<and> count M b < count N b"
-  using assms
-proof (induct A arbitrary: M N rule: finite_induct)
-  case (insert x F)
-  note fin = this(1) and x_ni_f = this(2) and ih = this(3) and x_f_eq_m_n = this(4) and
-    cnt_lt = this(5)
-
-  let ?Ma = "{#y \<in># M. y \<noteq> x#}"
-  let ?Mb = "{#y \<in># M. y = x#}"
-  let ?Na = "{#y \<in># N. y \<noteq> x#}"
-  let ?Nb = "{#y \<in># N. y = x#}"
-
-  have m_part: "M = ?Mb + ?Ma" and n_part: "N = ?Nb + ?Na"
-    using multiset_partition by blast+
-
-  have f_eq_ma_na: "F = set_mset ?Ma \<union> set_mset ?Na"
-    using x_f_eq_m_n x_ni_f by auto
-
-  show ?case
-  proof (cases "f x = f a")
-    case fx_ne_fa: False
-
-    have cnt_fma_fa: "count (image_mset f ?Ma) (f a) = count (image_mset f M) (f a)"
-      using fx_ne_fa by (subst (2) m_part) auto
-    have cnt_fna_fa: "count (image_mset f ?Na) (f a) = count (image_mset f N) (f a)"
-      using fx_ne_fa by (subst (2) n_part) auto
-    have cnt_ma_a: "count ?Ma a = count M a"
-      using fx_ne_fa by (subst (2) m_part) auto
-    have cnt_na_a: "count ?Na a = count N a"
-      using fx_ne_fa by (subst (2) n_part) auto
-
-    obtain b where fb_eq_fa: "f b = f a" and cnt_b: "count ?Ma b < count ?Na b"
-      using ih[OF f_eq_ma_na] cnt_lt unfolding cnt_fma_fa cnt_fna_fa cnt_ma_a cnt_na_a by blast
-    have fx_ne_fb: "f x \<noteq> f b"
-      using fb_eq_fa fx_ne_fa by simp
-
-    have cnt_ma_b: "count ?Ma b = count M b"
-      using fx_ne_fb by (subst (2) m_part) auto
-    have cnt_na_b: "count ?Na b = count N b"
-      using fx_ne_fb by (subst (2) n_part) auto
-
-    show ?thesis
-      using fb_eq_fa cnt_b unfolding cnt_ma_b cnt_na_b by blast
-  next
-    case fx_eq_fa: True
-    show ?thesis
-    proof (cases "x = a")
-      case x_eq_a: True
-      have "count (image_mset f ?Ma) (f a) + count ?Na a
-        < count (image_mset f ?Na) (f a) + count ?Ma a"
-        using cnt_lt x_eq_a by (subst (asm) (1 2) m_part, subst (asm) (1 2) n_part, auto)
-      thus ?thesis
-        using ih[OF f_eq_ma_na] by (metis count_filter_mset nat_neq_iff)
-    next
-      case x_ne_a: False
-      show ?thesis
-      proof (cases "count M x < count N x")
-        case True
-        thus ?thesis
-          using fx_eq_fa by blast
-     next
-        case False
-        hence cnt_x: "count M x \<ge> count N x"
-          by fastforce
-        have "count M x + count (image_mset f ?Ma) (f a) + count ?Na a
-          < count N x + count (image_mset f ?Na) (f a) + count ?Ma a"
-          using cnt_lt x_ne_a fx_eq_fa by (subst (asm) (1 2) m_part, subst (asm) (1 2) n_part, auto)
-        hence "count (image_mset f ?Ma) (f a) + count ?Na a
-          < count (image_mset f ?Na) (f a) + count ?Ma a"
-          using cnt_x by linarith
-        thus ?thesis
-          using ih[OF f_eq_ma_na] by (metis count_filter_mset nat_neq_iff)
-      qed
-    qed
-  qed
-qed auto
-
-lemma count_image_mset_le_imp_lt:
-  assumes
-    "count (image_mset f M) (f a) \<le> count (image_mset f N) (f a)" and
-    "count M a > count N a"
-  shows "\<exists>b. f b = f a \<and> count M b < count N b"
-  using assms by (auto intro: count_image_mset_le_imp_lt_raw[of "set_mset M \<union> set_mset N"])
-
-lemma Max_in_mset: "M \<noteq> {#} \<Longrightarrow> Max_mset M \<in># M"
-  by simp
-
-lemma Max_lt_imp_lt_mset:
-  assumes n_nemp: "N \<noteq> {#}" and max: "Max_mset M < Max_mset N" (is "?max_M < ?max_N")
-  shows "M < N"
-proof (cases "M = {#}")
-  case m_nemp: False
-
-  have max_n_in_n: "?max_N \<in># N"
-    using n_nemp by simp
-  have max_n_nin_m: "?max_N \<notin># M"
-    using max Max_ge leD by auto
-
-  have "M \<noteq> N"
-    using max by auto
-  moreover
-  {
-    fix y
-    assume "count N y < count M y"
-    hence "y \<in># M"
-      by blast
-    hence "?max_M \<ge> y"
-      by simp
-    hence "?max_N > y"
-      using max by auto
-    hence "\<exists>x > y. count M x < count N x"
-      using max_n_nin_m max_n_in_n by fastforce
-  }
-  ultimately show ?thesis
-    unfolding less_multiset\<^sub>H\<^sub>O by blast
-qed (auto simp: n_nemp)
-
-lemma fold_mset_singleton[simp]: "fold_mset f z {#x#} = f x z"
-  by (simp add: fold_mset_def)
+declare
+  filter_eq_replicate_mset [simp]
+  image_mset_subseteq_mono [intro]
+  count_gt_imp_in_mset [intro]
 
 end
diff --git a/thys/Pratt_Certificate/Pratt_Certificate.thy b/thys/Pratt_Certificate/Pratt_Certificate.thy
--- a/thys/Pratt_Certificate/Pratt_Certificate.thy
+++ b/thys/Pratt_Certificate/Pratt_Certificate.thy
@@ -1,889 +1,889 @@
 section \<open>Pratt's Primality Certificates\<close>
 text_raw \<open>\label{sec:pratt}\<close>
 theory Pratt_Certificate
 imports
   Complex_Main
   Lehmer.Lehmer
 begin
 
 text \<open>
   This work formalizes Pratt's proof system as described in his article
   ``Every Prime has a Succinct Certificate''\<^cite>\<open>"pratt1975certificate"\<close>.
 
   The proof system makes use of two types of predicates:
   \begin{itemize}
     \item $\text{Prime}(p)$: $p$ is a prime number
     \item $(p, a, x)$: \<open>\<forall>q \<in> prime_factors(x). [a^((p - 1) div q) \<noteq> 1] (mod p)\<close>
   \end{itemize}
   We represent these predicates with the following datatype:
 \<close>
 
 datatype pratt = Prime nat | Triple nat nat nat
 
 text \<open>
   Pratt describes an inference system consisting of the axiom $(p, a, 1)$
   and the following inference rules:
   \begin{itemize}
   \item R1: If we know that $(p, a, x)$ and \<open>[a^((p - 1) div q) \<noteq> 1] (mod p)\<close> hold for some
               prime number $q$ we can conclude $(p, a, qx)$ from that.
   \item R2: If we know that $(p, a, p - 1)$ and  \<open>[a^(p - 1) = 1] (mod p)\<close> hold, we can
               infer $\text{Prime}(p)$.
   \end{itemize}
   Both rules follow from Lehmer's theorem as we will show later on.
 
   A list of predicates (i.e., values of type @{type pratt}) is a \emph{certificate}, if it is
   built according to the inference system described above. I.e., a list @{term "x # xs :: pratt list"}
   is a certificate if @{term "xs :: pratt list"} is a certificate and @{term "x :: pratt"} is
   either an axiom or all preconditions of @{term "x :: pratt"} occur in @{term "xs :: pratt list"}.
 
   We call a certificate @{term "xs :: pratt list"} a \emph{certificate for @{term p}},
   if @{term "Prime p"} occurs in @{term "xs :: pratt list"}.
 
   The function \<open>valid_cert\<close> checks whether a list is a certificate.
 \<close>
 
 fun valid_cert :: "pratt list \<Rightarrow> bool" where
   "valid_cert [] = True"
 | R2: "valid_cert (Prime p#xs) \<longleftrightarrow> 1 < p \<and> valid_cert xs
     \<and> (\<exists> a . [a^(p - 1) = 1] (mod p) \<and> Triple p a (p - 1) \<in> set xs)"
 | R1: "valid_cert (Triple p a x # xs) \<longleftrightarrow> p > 1 \<and> 0 < x  \<and> valid_cert xs \<and> (x=1 \<or>
     (\<exists>q y. x = q * y \<and> Prime q \<in> set xs \<and> Triple p a y \<in> set xs
       \<and> [a^((p - 1) div q) \<noteq> 1] (mod p)))"
 
 text \<open>
   We define a function @{term size_cert} to measure the size of a certificate, assuming
   a binary encoding of numbers. We will use this to show that there is a certificate for a
   prime number $p$ such that the size of the certificate is polynomially bounded in the size
   of the binary representation of $p$.
 \<close>
 fun size_pratt :: "pratt \<Rightarrow> real" where
   "size_pratt (Prime p) = log 2 p" |
   "size_pratt (Triple p a x) = log 2 p + log 2 a + log 2 x"
 
 fun size_cert :: "pratt list \<Rightarrow> real" where
   "size_cert [] = 0" |
   "size_cert (x # xs) = 1 + size_pratt x + size_cert xs"
 
 
 subsection \<open>Soundness\<close>
 
 text \<open>
   In Section \ref{sec:pratt} we introduced the predicates $\text{Prime}(p)$ and $(p, a, x)$.
   In this section we show that for a certificate every predicate occurring in this certificate
   holds. In particular, if $\text{Prime}(p)$ occurs in a certificate, $p$ is prime.
 \<close>
 
 lemma prime_factors_one [simp]: shows "prime_factors (Suc 0) = {}"
   using prime_factorization_1 [where ?'a = nat] by simp
 
 lemma prime_factors_of_prime: fixes p :: nat assumes "prime p" shows "prime_factors p = {p}"
   using assms by (fact prime_prime_factors)
 
 definition pratt_triple :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
   "pratt_triple p a x \<longleftrightarrow> x > 0 \<and> (\<forall>q\<in>prime_factors x. [a ^ ((p - 1) div q) \<noteq> 1] (mod p))"
 
 lemma pratt_triple_1: "p > 1 \<Longrightarrow> x = 1 \<Longrightarrow> pratt_triple p a x"
   by (auto simp: pratt_triple_def)
 
 lemma pratt_triple_extend:
   assumes "prime q" "pratt_triple p a y"
           "p > 1" "x > 0" "x = q * y" "[a ^ ((p - 1) div q) \<noteq> 1] (mod p)"
   shows   "pratt_triple p a x"
 proof -
   have "prime_factors x = insert q (prime_factors y)"
     using assms by (simp add: prime_factors_product prime_prime_factors)
   also have "\<forall>r\<in>\<dots>. [a ^ ((p - 1) div r) \<noteq> 1] (mod p)"
     using assms by (auto simp: pratt_triple_def)
   finally show ?thesis using assms
     unfolding pratt_triple_def by blast
 qed
 
 lemma pratt_triple_imp_prime:
   assumes "pratt_triple p a x" "p > 1" "x = p - 1" "[a ^ (p - 1) = 1] (mod p)"
   shows   "prime p"
   using lehmers_theorem[of p a] assms by (auto simp: pratt_triple_def)
 
 theorem pratt_sound:
   assumes 1: "valid_cert c"
   assumes 2: "t \<in> set c"
   shows "(t = Prime p \<longrightarrow> prime p) \<and>
          (t = Triple p a x \<longrightarrow> ((\<forall>q \<in> prime_factors x . [a^((p - 1) div q) \<noteq> 1] (mod p)) \<and> 0<x))"
 using assms
 proof (induction c arbitrary: p a x t)
   case Nil then show ?case by force
   next
   case (Cons y ys)
   { assume "y=Triple p a x" "x=1"
     then have "(\<forall> q \<in> prime_factors x . [a^((p - 1) div q) \<noteq> 1] (mod p)) \<and> 0<x" by simp
     }
   moreover
   { assume x_y: "y=Triple p a x" "x~=1"
     hence "x>0" using Cons.prems by auto
     obtain q z where "x=q*z" "Prime q \<in> set ys \<and> Triple p a z \<in> set ys"
                and cong:"[a^((p - 1) div q) \<noteq> 1] (mod p)" using Cons.prems x_y by auto
     then have factors_IH:"(\<forall> r \<in> prime_factors z . [a^((p - 1) div r) \<noteq> 1] (mod p))" "prime q" "z>0"
       using Cons.IH Cons.prems \<open>x>0\<close> \<open>y=Triple p a x\<close>
       by force+
     then have "prime_factors x = prime_factors z \<union> {q}"  using \<open>x =q*z\<close> \<open>x>0\<close>
       by (simp add: prime_factors_product prime_factors_of_prime)
     then have "(\<forall> q \<in> prime_factors x . [a^((p - 1) div q) \<noteq> 1] (mod p)) \<and> 0 < x"
       using factors_IH cong by (simp add: \<open>x>0\<close>)
     }
   ultimately have y_Triple:"y=Triple p a x \<Longrightarrow> (\<forall> q \<in> prime_factors x .
                                                 [a^((p - 1) div q) \<noteq> 1] (mod p)) \<and> 0<x" by linarith
   { assume y: "y=Prime p" "p>2" then
     obtain a where a:"[a^(p - 1) = 1] (mod p)" "Triple p a (p - 1) \<in> set ys"
       using Cons.prems by auto
     then have Bier:"(\<forall>q\<in>prime_factors (p - 1). [a^((p - 1) div q) \<noteq> 1] (mod p))"
       using Cons.IH Cons.prems(1) by (simp add:y(1))
     then have "prime p" using lehmers_theorem[OF _ _a(1)] \<open>p>2\<close> by fastforce
     }
   moreover
   { assume "y=Prime p" "p=2" hence "prime p" by simp }
   moreover
   { assume "y=Prime p" then have "p>1"  using Cons.prems  by simp }
   ultimately have y_Prime:"y = Prime p \<Longrightarrow> prime p" by linarith
 
   show ?case
   proof (cases "t \<in> set ys")
     case True
       show ?thesis using Cons.IH[OF _ True] Cons.prems(1) by (cases y) auto
     next
     case False
       thus ?thesis using Cons.prems(2) y_Prime y_Triple by force
   qed
 qed
 
 corollary pratt_primeI:
   assumes "valid_cert xs" "Prime p \<in> set xs"
   shows   "prime p"
   using pratt_sound[OF assms] by simp
 
 
 subsection \<open>Completeness\<close>
 
 text \<open>
   In this section we show completeness of Pratt's proof system, i.e., we show that for
   every prime number $p$ there exists a certificate for $p$. We also give an upper
   bound for the size of a minimal certificate
 
   The prove we give is constructive. We assume that we have certificates for all prime
   factors of $p - 1$ and use these to build a certificate for $p$ from that. It is
   important to note that certificates can be concatenated.
 \<close>
 
 lemma valid_cert_appendI:
   assumes "valid_cert r"
   assumes "valid_cert s"
   shows "valid_cert (r @ s)"
   using assms
 proof (induction r)
   case (Cons y ys) then show ?case by (cases y) auto
 qed simp
 
 lemma valid_cert_concatI: "(\<forall>x \<in> set xs . valid_cert x) \<Longrightarrow> valid_cert (concat xs)"
   by (induction xs) (auto simp add: valid_cert_appendI)
 
 lemma size_pratt_le:
  fixes d::real
  assumes "\<forall> x \<in> set c. size_pratt x \<le> d"
  shows "size_cert c \<le> length c * (1 + d)" using assms
  by (induction c) (simp_all add: algebra_simps)
 
 fun build_fpc :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> pratt list" where
   "build_fpc p a r [] = [Triple p a r]" |
   "build_fpc p a r (y # ys) = Triple p a r # build_fpc p a (r div y) ys"
 
 text \<open>
   The function @{term build_fpc} helps us to construct a certificate for $p$ from
   the certificates for the prime factors of $p - 1$. Called as
   @{term "build_fpc p a (p - 1) qs"} where $@{term "qs"} = q_1 \ldots q_n$
   is prime decomposition of $p - 1$ such that $q_1 \cdot \dotsb \cdot q_n = @{term "p - 1 :: nat"}$,
   it returns the following list of predicates:
   \[
   (p,a,p-1), (p,a,\frac{p - 1}{q_1}), (p,a,\frac{p - 1}{q_1 q_2}), \ldots, (p,a,\frac{p-1}{q_1 \ldots q_n}) = (p,a,1)
   \]
 
   I.e., if there is an appropriate $a$ and and a certificate @{term rs} for all
   prime factors of $p$, then we can construct a certificate for $p$ as
   @{term [display] "Prime p # build_fpc p a (p - 1) qs @ rs"}
 \<close>
 
 text \<open>
   The following lemma shows that \<open>build_fpc\<close> extends a certificate that
   satisfies the preconditions described before to a correct certificate.
 \<close>
 
 lemma correct_fpc:
   assumes "valid_cert xs" "p > 1"
   assumes "prod_list qs = r" "r \<noteq> 0"
   assumes "\<forall> q \<in> set qs . Prime q \<in> set xs"
   assumes "\<forall> q \<in> set qs . [a^((p - 1) div q) \<noteq> 1] (mod p)"
   shows "valid_cert (build_fpc p a r qs @ xs)"
   using assms
 proof (induction qs arbitrary: r)
   case Nil thus ?case by auto
 next
   case (Cons y ys)
   have "prod_list ys = r div y" using Cons.prems by auto
   then have T_in: "Triple p a (prod_list ys) \<in> set (build_fpc p a (r div y) ys @ xs)"
     by (cases ys) auto
 
   have "valid_cert (build_fpc p a (r div y) ys @ xs)"
     using Cons.prems by (intro Cons.IH) auto
   then have "valid_cert (Triple p a r # build_fpc p a (r div y) ys @ xs)"
     using \<open>r \<noteq> 0\<close> T_in Cons.prems by auto
   then show ?case by simp
 qed
 
 lemma length_fpc:
   "length (build_fpc p a r qs) = length qs + 1" by (induction qs arbitrary: r) auto
 
 lemma div_gt_0:
   fixes m n :: nat assumes "m \<le> n" "0 < m" shows "0 < n div m"
 proof -
   have "0 < m div m" using \<open>0 < m\<close> div_self by auto
   also have "m div m \<le> n div m" using \<open>m \<le> n\<close> by (rule div_le_mono)
   finally show ?thesis .
 qed
 
 lemma size_pratt_fpc:
   assumes "a \<le> p" "r \<le> p" "0 < a" "0 < r" "0 < p" "prod_list qs = r"
   shows "\<forall>x \<in> set (build_fpc p a r qs) . size_pratt x \<le> 3 * log 2 p" using assms
 proof (induction qs arbitrary: r)
   case Nil
   then have "log 2 a \<le> log 2 p" "log 2 r \<le> log 2 p" by auto
   then show ?case by simp
 next
   case (Cons q qs)
   then have "log 2 a \<le> log 2 p" "log 2 r \<le> log 2 p" by auto
   then have  "log 2 a + log 2 r \<le> 2 * log 2 p" by arith
   moreover have "r div q > 0" using Cons.prems by (fastforce intro: div_gt_0)
   moreover hence "prod_list qs = r div q" using Cons.prems(6) by auto
   moreover have "r div q \<le> p" using \<open>r\<le>p\<close> div_le_dividend[of r q] by linarith
   ultimately show ?case using Cons by simp
 qed
 
 lemma concat_set:
   assumes "\<forall> q \<in> qs . \<exists> c \<in> set cs . Prime q \<in> set c"
   shows "\<forall> q \<in> qs . Prime q \<in> set (concat cs)"
   using assms by (induction cs) auto
 
 lemma p_in_prime_factorsE:
   fixes n :: nat
   assumes "p \<in> prime_factors n" "0 < n"
   obtains "2 \<le> p" "p \<le> n" "p dvd n" "prime p"
 proof
   from assms show "prime p" by auto
   then show "2 \<le> p" by (auto dest: prime_gt_1_nat)
 
   from assms show "p dvd n" by auto
   then show "p \<le> n" using  \<open>0 < n\<close> by (rule dvd_imp_le)
 qed
 
 lemma prime_factors_list_prime:
   fixes n :: nat
   assumes "prime n"
   shows "\<exists> qs. prime_factors n = set qs \<and> prod_list qs = n \<and> length qs = 1"
   using assms by (auto simp add: prime_factorization_prime intro: exI [of _ "[n]"])
 
 lemma prime_factors_list:
   fixes n :: nat assumes "3 < n" "\<not> prime n"
   shows "\<exists> qs. prime_factors n = set qs \<and> prod_list qs = n \<and> length qs \<ge> 2"
   using assms
 proof (induction n rule: less_induct)
   case (less n)
     obtain p where "p \<in> prime_factors n" using \<open>n > 3\<close> prime_factors_elem by force
     then have p':"2 \<le> p" "p \<le> n" "p dvd n" "prime p"
       using \<open>3 < n\<close> by (auto elim: p_in_prime_factorsE)
     { assume "n div p > 3" "\<not> prime (n div p)"
       then obtain qs
         where "prime_factors (n div p) = set qs" "prod_list qs = (n div p)" "length qs \<ge> 2"
         using p' by atomize_elim (auto intro: less simp: div_gt_0)
       moreover
       have "prime_factors (p * (n div p)) = insert p (prime_factors (n div p))"
         using \<open>3 < n\<close> \<open>2 \<le> p\<close> \<open>p \<le> n\<close> \<open>prime p\<close>
       by (auto simp: prime_factors_product div_gt_0 prime_factors_of_prime)
       ultimately
       have "prime_factors n = set (p # qs)" "prod_list (p # qs) = n" "length (p#qs) \<ge> 2"
         using \<open>p dvd n\<close> by simp_all
       hence ?case by blast
     }
     moreover
     { assume "prime (n div p)"
       then obtain qs
         where "prime_factors (n div p) = set qs" "prod_list qs = (n div p)" "length qs = 1"
         using prime_factors_list_prime by blast
       moreover
       have "prime_factors (p * (n div p)) = insert p (prime_factors (n div p))"
         using \<open>3 < n\<close> \<open>2 \<le> p\<close> \<open>p \<le> n\<close> \<open>prime p\<close>
       by (auto simp: prime_factors_product div_gt_0 prime_factors_of_prime)
       ultimately
       have "prime_factors n = set (p # qs)" "prod_list (p # qs) = n" "length (p#qs) \<ge> 2"
         using \<open>p dvd n\<close> by simp_all
       hence ?case by blast
     } note case_prime = this
     moreover
     { assume "n div p = 1"
       hence "n = p" using \<open>n>3\<close>  using One_leq_div[OF \<open>p dvd n\<close>] p'(2) by force
       hence ?case using \<open>prime p\<close> \<open>\<not> prime n\<close> by auto
     }
     moreover
     { assume "n div p = 2"
       hence ?case using case_prime by force
     }
     moreover
     { assume "n div p = 3"
       hence ?case using p' case_prime by force
     }
     ultimately show ?case using p' div_gt_0[of p n] case_prime by fastforce
 
 qed
 
 lemma prod_list_ge:
   fixes xs::"nat list"
   assumes "\<forall> x \<in> set xs . x \<ge> 1"
   shows "prod_list xs \<ge> 1" using assms by (induction xs) auto
 
 lemma sum_list_log:
   fixes b::real
   fixes xs::"nat list"
   assumes b: "b > 0" "b \<noteq> 1"
   assumes xs:"\<forall> x \<in> set xs . x \<ge> b"
   shows "(\<Sum>x\<leftarrow>xs. log b x) = log b (prod_list xs)"
   using assms
 proof (induction xs)
   case Nil
     thus ?case by simp
   next
   case (Cons y ys)
     have "real (prod_list ys) > 0" using prod_list_ge Cons.prems by fastforce
-    thus ?case using log_mult[OF Cons.prems(1-2)] Cons by force
+    thus ?case using log_mult Cons.prems(1-2) Cons by simp
 qed
 
 lemma concat_length_le:
   fixes g :: "nat \<Rightarrow> real"
   assumes "\<forall> x \<in> set xs . real (length (f x)) \<le> g x"
   shows "length (concat (map f xs)) \<le> (\<Sum>x\<leftarrow>xs. g x)" using assms
   by (induction xs) force+
 
 lemma prime_gt_3_impl_p_minus_one_not_prime:
   fixes p::nat
   assumes "prime p" "p>3"
   shows "\<not> prime (p - 1)"
 proof
   assume "prime (p - 1)"
   have "\<not> even p" using assms by (simp add: prime_odd_nat)
   hence "2 dvd (p - 1)" by presburger
   then obtain q where "p - 1 = 2 * q" ..
   then have "2 \<in> prime_factors (p - 1)" using \<open>p>3\<close>
     by (auto simp: prime_factorization_times_prime)
   thus False using prime_factors_of_prime \<open>p>3\<close> \<open>prime (p - 1)\<close> by auto
 qed
 
 text \<open>
   We now prove that Pratt's proof system is complete and derive upper bounds for
   the length and the size of the entries of a minimal certificate.
 \<close>
 
 theorem pratt_complete':
   assumes "prime p"
   shows "\<exists>c. Prime p \<in> set c \<and> valid_cert c \<and> length c \<le> 6*log 2 p - 4 \<and> (\<forall> x \<in> set c. size_pratt x \<le> 3 * log 2 p)" using assms
 proof (induction p rule: less_induct)
   case (less p)
   from \<open>prime p\<close> have "p > 1" by (rule prime_gt_1_nat)
   then consider "p = 2" | " p = 3" | "p > 3" by force
   thus ?case
   proof cases
     assume [simp]: "p = 2"
     have "Prime p \<in> set [Prime 2, Triple 2 1 1]" by simp
     thus ?case by fastforce
   next
     assume [simp]: "p = 3"
     let ?cert = "[Prime 3, Triple 3 2 2, Triple 3 2 1, Prime 2, Triple 2 1 1]"
 
     have "length ?cert \<le> 6*log 2 p - 4 \<longleftrightarrow> 3 \<le> 2 * log 2 3" by simp
     also have "2 * log 2 3 = log 2 (3 ^ 2 :: real)" by (subst log_nat_power) simp_all
     also have "\<dots> = log 2 9" by simp
     also have "3 \<le> log 2 9 \<longleftrightarrow> True" by (subst le_log_iff) simp_all
     finally show ?case
       by (intro exI[where x = "?cert"]) (simp add: cong_def)
   next
     assume "p > 3"
     have qlp: "\<forall>q \<in> prime_factors (p - 1) . q < p" using \<open>prime p\<close>
       by (metis One_nat_def Suc_pred le_imp_less_Suc lessI less_trans p_in_prime_factorsE prime_gt_1_nat zero_less_diff)
     hence factor_certs:"\<forall>q \<in> prime_factors (p - 1) . (\<exists>c . ((Prime q \<in> set c) \<and> (valid_cert c)
                                                       \<and> length c \<le> 6*log 2 q - 4) \<and> (\<forall> x \<in> set c. size_pratt x \<le> 3 * log 2 q))"
       by (auto intro: less.IH)
     obtain a where a:"[a^(p - 1) = 1] (mod p) \<and> (\<forall> q. q \<in> prime_factors (p - 1)
               \<longrightarrow> [a^((p - 1) div q) \<noteq> 1] (mod p))" and a_size: "a > 0" "a < p"
       using converse_lehmer[OF \<open>prime p\<close>] by blast
 
     have "\<not> prime (p - 1)" using \<open>p>3\<close> prime_gt_3_impl_p_minus_one_not_prime \<open>prime p\<close> by auto
     have "p \<noteq> 4" using \<open>prime p\<close> by auto
     hence "p - 1 > 3" using \<open>p > 3\<close> by auto
 
     then obtain qs where prod_qs_eq:"prod_list qs = p - 1"
         and qs_eq:"set qs = prime_factors (p - 1)" and qs_length_eq: "length qs \<ge> 2"
       using prime_factors_list[OF _ \<open>\<not> prime (p - 1)\<close>] by auto
     obtain f where f:"\<forall>q \<in> prime_factors (p - 1) . \<exists> c. f q = c
                      \<and> ((Prime q \<in> set c) \<and> (valid_cert c) \<and> length c \<le> 6*log 2 q - 4)
                      \<and> (\<forall> x \<in> set c. size_pratt x \<le> 3 * log 2 q)"
       using factor_certs by metis
     let ?cs = "map f qs"
     have cs: "\<forall>q \<in> prime_factors (p - 1) . (\<exists>c \<in> set ?cs . (Prime q \<in> set c) \<and> (valid_cert c)
                                            \<and> length c \<le> 6*log 2 q - 4
                                            \<and> (\<forall> x \<in> set c. size_pratt x \<le> 3 * log 2 q))"
       using f qs_eq by auto
 
     have cs_cert_size: "\<forall>c \<in> set ?cs . \<forall> x \<in> set c. size_pratt x \<le> 3 * log 2 p"
     proof
       fix c assume "c \<in> set (map f qs)"
       then obtain q where "c = f q" and "q \<in> set qs" by auto
       hence *:"\<forall> x \<in> set c. size_pratt x \<le> 3 * log 2 q" using f qs_eq by blast
       have "q < p" "q > 0" using qlp \<open>q \<in> set qs\<close> qs_eq prime_factors_gt_0_nat by auto
       show "\<forall> x \<in> set c. size_pratt x \<le> 3 * log 2 p"
       proof
         fix x assume "x \<in> set c"
         hence "size_pratt x \<le> 3 * log 2 q" using * by fastforce
         also have "\<dots> \<le> 3 * log 2 p" using \<open>q < p\<close> \<open>q > 0\<close> \<open>p > 3\<close> by simp
         finally show "size_pratt x \<le> 3 * log 2 p" .
       qed
     qed
 
     have cs_valid_all: "\<forall>c \<in> set ?cs . valid_cert c"
       using f qs_eq by fastforce
 
     have "\<forall>x \<in> set (build_fpc p a (p - 1) qs). size_pratt x \<le> 3 * log 2 p"
       using cs_cert_size a_size \<open>p > 3\<close> prod_qs_eq by (intro size_pratt_fpc) auto
     hence "\<forall>x \<in> set (build_fpc p a (p - 1) qs @ concat ?cs) . size_pratt x \<le> 3 * log 2 p"
       using cs_cert_size by auto
     moreover
     have "Triple p a (p - 1) \<in> set (build_fpc p a (p - 1) qs @ concat ?cs)" by (cases qs) auto
     moreover
     have "valid_cert ((build_fpc p a (p - 1) qs)@ concat ?cs)"
     proof (rule correct_fpc)
       show "valid_cert (concat ?cs)"
         using cs_valid_all by (auto simp: valid_cert_concatI)
       show "prod_list qs = p - 1" by (rule prod_qs_eq)
       show "p - 1 \<noteq> 0" using prime_gt_1_nat[OF \<open>prime p\<close>] by arith
       show "\<forall> q \<in> set qs . Prime q \<in> set (concat ?cs)"
         using concat_set[of "prime_factors (p - 1)"] cs qs_eq by blast
       show "\<forall> q \<in> set qs . [a^((p - 1) div q) \<noteq> 1] (mod p)" using qs_eq a by auto
     qed (insert \<open>p > 3\<close>, simp_all)
     moreover
     { let ?k = "length qs"
 
       have qs_ge_2:"\<forall>q \<in> set qs . q \<ge> 2" using qs_eq
         by (auto intro: prime_ge_2_nat)
 
       have "\<forall>x\<in>set qs. real (length (f x)) \<le> 6 * log 2 (real x) - 4" using f qs_eq by blast
       hence "length (concat ?cs) \<le> (\<Sum>q\<leftarrow>qs. 6*log 2 q - 4)" using concat_length_le
         by fast
       hence "length (Prime p # ((build_fpc p a (p - 1) qs)@ concat ?cs))
             \<le> ((\<Sum>q\<leftarrow>(map real qs). 6*log 2 q - 4) + ?k + 2)"
             by (simp add: o_def length_fpc)
       also have "\<dots> = (6*(\<Sum>q\<leftarrow>(map real qs). log 2 q) + (-4 * real ?k) + ?k + 2)"
         by (simp add: o_def sum_list_subtractf sum_list_triv sum_list_const_mult)
       also have "\<dots> \<le> 6*log 2 (p - 1) - 4" using \<open>?k\<ge>2\<close> prod_qs_eq sum_list_log[of 2 qs] qs_ge_2
         by force
       also have "\<dots> \<le> 6*log 2 p - 4" using log_le_cancel_iff[of 2 "p - 1" p] \<open>p>3\<close> by force
       ultimately have "length (Prime p # ((build_fpc p a (p - 1) qs)@ concat ?cs))
                        \<le> 6*log 2 p - 4" by linarith }
     ultimately obtain c where c:"Triple p a (p - 1) \<in> set c" "valid_cert c"
                                "length (Prime p #c) \<le> 6*log 2 p - 4"
                                "(\<forall> x \<in> set c. size_pratt x \<le> 3 * log 2 p)" by blast
     hence "Prime p \<in> set (Prime p # c)" "valid_cert (Prime p # c)"
          "(\<forall> x \<in> set (Prime p # c). size_pratt x \<le> 3 * log 2 p)"
     using a \<open>prime p\<close> by (auto simp: Primes.prime_gt_Suc_0_nat)
     thus ?case using c by blast
   qed
 qed
 
 text \<open>
   We now recapitulate our results. A number $p$ is prime if and only if there
   is a certificate for $p$. Moreover, for a prime $p$ there always is a certificate
   whose size is polynomially bounded in the logarithm of $p$.
 \<close>
 
 corollary pratt:
   "prime p \<longleftrightarrow> (\<exists>c. Prime p \<in> set c \<and> valid_cert c)"
   using pratt_complete' pratt_sound(1) by blast
 
 corollary pratt_size:
   assumes "prime p"
   shows "\<exists>c. Prime p \<in> set c \<and> valid_cert c \<and> size_cert c \<le> (6 * log 2 p - 4) * (1 + 3 * log 2 p)"
 proof -
   obtain c where c: "Prime p \<in> set c" "valid_cert c"
       and len: "length c \<le> 6*log 2 p - 4" and "(\<forall> x \<in> set c. size_pratt x \<le> 3 * log 2 p)"
     using pratt_complete' assms by blast
   hence "size_cert c \<le> length c * (1 + 3 * log 2 p)" by (simp add: size_pratt_le)
   also have "\<dots> \<le> (6*log 2 p - 4) * (1 + 3 * log 2 p)" using len by simp
   finally show ?thesis using c by blast
 qed
 
 
 subsection \<open>Efficient modular exponentiation\<close>
 
 locale efficient_power =
   fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
   assumes f_assoc: "\<And>x z. f x (f x z) = f (f x x) z"
 begin
 
 function efficient_power :: "'a \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a" where
   "efficient_power y x 0 = y"
 | "efficient_power y x (Suc 0) = f x y"
 | "n \<noteq> 0 \<Longrightarrow> even n \<Longrightarrow> efficient_power y x n = efficient_power y (f x x) (n div 2)"
 | "n \<noteq> 1 \<Longrightarrow> odd n \<Longrightarrow> efficient_power y x n = efficient_power (f x y) (f x x) (n div 2)"
   by force+
 termination by (relation "measure (snd \<circ> snd)") (auto elim: oddE)
 
 lemma efficient_power_code:
   "efficient_power y x n =
      (if n = 0 then y
       else if n = 1 then f x y
       else if even n then efficient_power y (f x x) (n div 2)
       else efficient_power (f x y) (f x x) (n div 2))"
   by (induction y x n rule: efficient_power.induct) auto
 
 lemma efficient_power_correct: "efficient_power y x n = (f x ^^ n) y"
 proof -
   have [simp]: "f ^^ 2 = (\<lambda>x. f (f x))" for f :: "'a \<Rightarrow> 'a"
     by (simp add: eval_nat_numeral o_def)
   show ?thesis
     by (induction y x n rule: efficient_power.induct)
        (auto elim!: evenE oddE simp: funpow_mult [symmetric] funpow_Suc_right f_assoc
              simp del: funpow.simps(2))
 qed
 
 end
 
 interpretation mod_exp_nat: efficient_power "\<lambda>x y :: nat. (x * y) mod m"
   by standard (simp add: mod_mult_left_eq mod_mult_right_eq mult_ac)
 
 definition mod_exp_nat_aux where "mod_exp_nat_aux = mod_exp_nat.efficient_power"
 
 lemma mod_exp_nat_aux_code [code]:
   "mod_exp_nat_aux m y x n =
      (if n = 0 then y
       else if n = 1 then (x * y) mod m
       else if even n then mod_exp_nat_aux m y ((x * x) mod m) (n div 2)
       else mod_exp_nat_aux m ((x * y) mod m) ((x * x) mod m) (n div 2))"
   unfolding mod_exp_nat_aux_def by (rule mod_exp_nat.efficient_power_code)
 
 lemma mod_exp_nat_aux_correct:
   "mod_exp_nat_aux m y x n mod m = (x ^ n * y) mod m"
 proof -
   have "mod_exp_nat_aux m y x n = ((\<lambda>y. x * y mod m) ^^ n) y"
     by (simp add: mod_exp_nat_aux_def mod_exp_nat.efficient_power_correct)
   also have "((\<lambda>y. x * y mod m) ^^ n) y mod m = (x ^ n * y) mod m"
   proof (induction n)
     case (Suc n)
     hence "x * ((\<lambda>y. x * y mod m) ^^ n) y mod m = x * x ^ n * y mod m"
       by (metis mod_mult_right_eq mult.assoc)
     thus ?case by auto
   qed auto
   finally show ?thesis .
 qed
 
 definition mod_exp_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
   where [code_abbrev]: "mod_exp_nat b e m = (b ^ e) mod m"
 
 lemma mod_exp_nat_code [code]: "mod_exp_nat b e m = mod_exp_nat_aux m 1 b e mod m"
   by (simp add: mod_exp_nat_def mod_exp_nat_aux_correct)
 
 lemmas [code_unfold] = cong_def
 
 lemma eval_mod_exp_nat_aux [simp]:
   "mod_exp_nat_aux m y x 0 = y"
   "mod_exp_nat_aux m y x (Suc 0) = (x * y) mod m"
   "mod_exp_nat_aux m y x (numeral (num.Bit0 n)) =
      mod_exp_nat_aux m y (x\<^sup>2 mod m) (numeral n)"
   "mod_exp_nat_aux m y x (numeral (num.Bit1 n)) =
      mod_exp_nat_aux m ((x * y) mod m) (x\<^sup>2 mod m) (numeral n)"
 proof -
   define n' where "n' = (numeral n :: nat)"
   have [simp]: "n' \<noteq> 0" by (auto simp: n'_def)
   
   show "mod_exp_nat_aux m y x 0 = y" and "mod_exp_nat_aux m y x (Suc 0) = (x * y) mod m"
     by (simp_all add: mod_exp_nat_aux_def)
 
   have "numeral (num.Bit0 n) = (2 * n')"
     by (subst numeral.numeral_Bit0) (simp del: arith_simps add: n'_def)
   also have "mod_exp_nat_aux m y x \<dots> = mod_exp_nat_aux m y (x^2 mod m) n'"
     by (subst mod_exp_nat_aux_code) (simp_all add: power2_eq_square)
   finally show "mod_exp_nat_aux m y x (numeral (num.Bit0 n)) =
                   mod_exp_nat_aux m y (x\<^sup>2 mod m) (numeral n)"
     by (simp add: n'_def)
 
   have "numeral (num.Bit1 n) = Suc (2 * n')"
     by (subst numeral.numeral_Bit1) (simp del: arith_simps add: n'_def)
   also have "mod_exp_nat_aux m y x \<dots> = mod_exp_nat_aux m ((x * y) mod m) (x^2 mod m) n'"
     by (subst mod_exp_nat_aux_code) (simp_all add: power2_eq_square)
   finally show "mod_exp_nat_aux m y x (numeral (num.Bit1 n)) =
                   mod_exp_nat_aux m ((x * y) mod m) (x\<^sup>2 mod m) (numeral n)"
     by (simp add: n'_def)
 qed
 
 lemma eval_mod_exp [simp]:
   "mod_exp_nat b' 0 m' = 1 mod m'"
   "mod_exp_nat b' 1 m' = b' mod m'"
   "mod_exp_nat b' (Suc 0) m' = b' mod m'"
   "mod_exp_nat b' e' 0 = b' ^ e'"  
   "mod_exp_nat b' e' 1 = 0"
   "mod_exp_nat b' e' (Suc 0) = 0"
   "mod_exp_nat 0 1 m' = 0"
   "mod_exp_nat 0 (Suc 0) m' = 0"
   "mod_exp_nat 0 (numeral e) m' = 0"
   "mod_exp_nat 1 e' m' = 1 mod m'"
   "mod_exp_nat (Suc 0) e' m' = 1 mod m'"
   "mod_exp_nat (numeral b) (numeral e) (numeral m) =
      mod_exp_nat_aux (numeral m) 1 (numeral b) (numeral e) mod numeral m"
   by (simp_all add: mod_exp_nat_def mod_exp_nat_aux_correct)
 
 
 
 subsection \<open>Executable certificate checker\<close>
 
 lemmas [code] = valid_cert.simps(1)
 
 context
 begin
 
 lemma valid_cert_Cons1 [code]:
   "valid_cert (Prime p # xs) \<longleftrightarrow>
      p > 1 \<and> (\<exists>t\<in>set xs. case t of Prime _ \<Rightarrow> False | 
      Triple p' a x \<Rightarrow> p' = p \<and> x = p - 1 \<and> mod_exp_nat a (p-1) p = 1 ) \<and> valid_cert xs"
   (is "?lhs = ?rhs")
 proof
   assume ?lhs thus ?rhs by (auto simp: mod_exp_nat_def cong_def split: pratt.splits)
 next
   assume ?rhs
   hence "p > 1" "valid_cert xs" by blast+
   moreover from \<open>?rhs\<close> obtain t where "t \<in> set xs" "case t of Prime _ \<Rightarrow> False | 
      Triple p' a x \<Rightarrow> p' = p \<and> x = p - 1 \<and> [a^(p-1) = 1] (mod p)" 
      by (auto simp: cong_def mod_exp_nat_def cong: pratt.case_cong)
   ultimately show ?lhs by (cases t) auto
 qed
 
 private lemma Suc_0_mod_eq_Suc_0_iff:
   "Suc 0 mod n = Suc 0 \<longleftrightarrow> n \<noteq> Suc 0"
 proof -
   consider "n = 0" | "n = Suc 0" | "n > 1" by (cases n) auto
   thus ?thesis by cases auto
 qed
 
 private lemma Suc_0_eq_Suc_0_mod_iff:
   "Suc 0 = Suc 0 mod n \<longleftrightarrow> n \<noteq> Suc 0"
   using Suc_0_mod_eq_Suc_0_iff by (simp add: eq_commute)
 
 lemma valid_cert_Cons2 [code]:
   "valid_cert (Triple p a x # xs) \<longleftrightarrow> x > 0 \<and> p > 1 \<and> (x = 1 \<or> (
      (\<exists>t\<in>set xs. case t of Prime _ \<Rightarrow> False |
         Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> 
         (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p-1) div q) p \<noteq> 1)))) \<and> valid_cert xs"
   (is "?lhs = ?rhs")
 proof
   assume ?lhs
   from \<open>?lhs\<close> have pos: "x > 0" and gt_1: "p > 1" and valid: "valid_cert xs" by simp_all
   show ?rhs
   proof (cases "x = 1")
     case True
     with \<open>?lhs\<close> show ?thesis by auto
   next
     case False
     with \<open>?lhs\<close> have "(\<exists>q y. x = q * y \<and> Prime q \<in> set xs \<and> Triple p a y \<in> set xs
       \<and> [a^((p - 1) div q) \<noteq> 1] (mod p))" by auto
     then obtain q y where qy:
       "x = q * y"
       "Prime q \<in> set xs"
       "Triple p a y \<in> set xs"
       "[a ^ ((p - 1) div q) \<noteq> 1] (mod p)"
       by blast
     hence "(\<exists>t\<in>set xs. case t of Prime _ \<Rightarrow> False |
         Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> 
         (let q = x div y in Prime q \<in> set xs \<and> mod_exp_nat a ((p-1) div q) p \<noteq> 1))"
     using pos gt_1 by (intro bexI [of _ "Triple p a y"]) 
       (auto simp: Suc_0_mod_eq_Suc_0_iff Suc_0_eq_Suc_0_mod_iff cong_def mod_exp_nat_def)
     with pos gt_1 valid show ?thesis by blast
   qed
 next
   assume ?rhs
   hence pos: "x > 0" and gt_1: "p > 1" and valid: "valid_cert xs" by simp_all
   show ?lhs
   proof (cases "x = 1")
     case True
     with \<open>?rhs\<close> show ?thesis by auto
   next
     case False
     with \<open>?rhs\<close> obtain t where t: "t \<in> set xs" "case t of Prime x \<Rightarrow> False
          | Triple p' a' y \<Rightarrow> p' = p \<and> a' = a \<and> y dvd x \<and> (let q = x div y
               in Prime q \<in> set xs \<and> mod_exp_nat a ((p - 1) div q) p \<noteq> 1)" by auto
     then obtain y where y: "t = Triple p a y" "y dvd x" "let q = x div y in Prime q \<in> set xs \<and> 
                               mod_exp_nat a ((p - 1) div q) p \<noteq> 1" 
       by (cases t rule: pratt.exhaust) auto
     with gt_1 have y': "let q = x div y in Prime q \<in> set xs \<and> [a^((p - 1) div q) \<noteq> 1] (mod p)"
       by (auto simp: cong_def Let_def mod_exp_nat_def Suc_0_mod_eq_Suc_0_iff Suc_0_eq_Suc_0_mod_iff)
     define q where "q = x div y"
     have "\<exists>q y. x = q * y \<and> Prime q \<in> set xs \<and> Triple p a y \<in> set xs
                      \<and> [a^((p - 1) div q) \<noteq> 1] (mod p)"
       by (rule exI[of _ q], rule exI[of _ y]) (insert t y y', auto simp: Let_def q_def)
     with pos gt_1 valid show ?thesis by simp
   qed
 qed
 
 declare valid_cert.simps(2,3) [simp del]
 
 lemmas eval_valid_cert = valid_cert.simps(1) valid_cert_Cons1 valid_cert_Cons2
 
 end
 
 
 text \<open>
   The following alternative tree representation of certificates is better suited for 
   efficient checking.
 \<close>
 
 datatype pratt_tree = Pratt_Node "nat \<times> nat \<times> pratt_tree list"
 
 fun pratt_tree_number where
   "pratt_tree_number (Pratt_Node (n, _, _)) = n"
 
 
 text \<open>
   The following function checks that a given list contains all the prime factors of the given
   number.
 \<close>
 
 fun check_prime_factors_subset :: "nat \<Rightarrow> nat list \<Rightarrow> bool" where
   "check_prime_factors_subset n [] \<longleftrightarrow> n = 1"
 | "check_prime_factors_subset n (p # ps) \<longleftrightarrow> (if n = 0 then False else
      (if p > 1 \<and> p dvd n then check_prime_factors_subset (n div p) (p # ps)
                          else check_prime_factors_subset n ps))"
 
 lemma check_prime_factors_subset_0 [simp]: "\<not>check_prime_factors_subset 0 ps"
   by (induction ps) auto
 
 lemmas [simp del] = check_prime_factors_subset.simps(2)
 
 lemma check_prime_factors_subset_Cons [simp]:
   "check_prime_factors_subset (Suc 0) (p # ps) \<longleftrightarrow> check_prime_factors_subset (Suc 0) ps"
   "check_prime_factors_subset 1 (p # ps) \<longleftrightarrow> check_prime_factors_subset 1 ps"
   "p > 1 \<Longrightarrow> p dvd numeral n \<Longrightarrow> check_prime_factors_subset (numeral n) (p # ps) \<longleftrightarrow>
                            check_prime_factors_subset (numeral n div p) (p # ps)"
   "p \<le> 1 \<or> \<not>p dvd numeral n \<Longrightarrow> check_prime_factors_subset (numeral n) (p # ps) \<longleftrightarrow>
                            check_prime_factors_subset (numeral n) ps"
  by (subst check_prime_factors_subset.simps; force)+
 
 lemma check_prime_factors_subset_correct:
   assumes "check_prime_factors_subset n ps" "list_all prime ps"
   shows   "prime_factors n \<subseteq> set ps"
   using assms
 proof (induction n ps rule: check_prime_factors_subset.induct)
   case (2 n p ps)
   note * = this
   from "2.prems" have "prime p" and "p > 1"
     by (auto simp: prime_gt_Suc_0_nat)
 
   consider "n = 0" | "n > 0" "p dvd n" | "n > 0" "\<not>(p dvd n)"
     by blast
   thus ?case
   proof cases
     case 2
     hence "n div p > 0" by auto
     hence "prime_factors ((n div p) * p) = insert p (prime_factors (n div p))"
       using \<open>p > 1\<close> \<open>prime p\<close> by (auto simp: prime_factors_product prime_prime_factors)
     also have "(n div p) * p = n"
       using 2 by auto
     finally show ?thesis using 2 \<open>p > 1\<close> *
       by (auto simp: check_prime_factors_subset.simps(2)[of n])
   next
     case 3
     with * and \<open>p > 1\<close> show ?thesis
       by (auto simp: check_prime_factors_subset.simps(2)[of n])
   qed auto
 qed auto
 
 
 fun valid_pratt_tree where
   "valid_pratt_tree (Pratt_Node (n, a, ts)) \<longleftrightarrow>
      n \<ge> 2 \<and>
      check_prime_factors_subset (n - 1) (map pratt_tree_number ts) \<and>
      [a ^ (n - 1) = 1] (mod n) \<and>
      (\<forall>t\<in>set ts. [a ^ ((n - 1) div pratt_tree_number t) \<noteq> 1] (mod n)) \<and>
      (\<forall>t\<in>set ts. valid_pratt_tree t)"
 
 lemma valid_pratt_tree_code [code]:
   "valid_pratt_tree (Pratt_Node (n, a, ts)) \<longleftrightarrow>
      n \<ge> 2 \<and>
      check_prime_factors_subset (n - 1) (map pratt_tree_number ts) \<and>
      mod_exp_nat a (n - 1) n = 1 \<and>
      (\<forall>t\<in>set ts. mod_exp_nat a ((n - 1) div pratt_tree_number t) n \<noteq> 1) \<and>
      (\<forall>t\<in>set ts. valid_pratt_tree t)"
   by (simp add: mod_exp_nat_def cong_def)
 
 lemma valid_pratt_tree_imp_prime:
   assumes "valid_pratt_tree t"
   shows   "prime (pratt_tree_number t)"
   using assms
 proof (induction t rule: valid_pratt_tree.induct)
   case (1 n a ts)
   from 1 have "prime_factors (n - 1) \<subseteq> set (map pratt_tree_number ts)"
     by (intro check_prime_factors_subset_correct) (auto simp: list.pred_set)
   with 1 show ?case
     by (intro lehmers_theorem[where a = a]) auto
 qed
 
 lemma valid_pratt_tree_imp_prime':
   assumes "PROP (Trueprop (valid_pratt_tree (Pratt_Node (n, a, ts)))) \<equiv> PROP (Trueprop True)"
   shows   "prime n"
 proof -
   have "valid_pratt_tree (Pratt_Node (n, a, ts))"
     by (subst assms) auto
   from valid_pratt_tree_imp_prime[OF this] show ?thesis by simp
 qed
 
 
 subsection \<open>Proof method setup\<close>
 
 theorem lehmers_theorem':
   fixes p :: nat
   assumes "list_all prime ps" "a \<equiv> a" "n \<equiv> n"
   assumes "list_all (\<lambda>p. mod_exp_nat a ((n - 1) div p) n \<noteq> 1) ps" "mod_exp_nat a (n - 1) n = 1"
   assumes "check_prime_factors_subset (n - 1) ps" "2 \<le> n"
   shows "prime n"
   using assms check_prime_factors_subset_correct[OF assms(6,1)]
   by (intro lehmers_theorem[where a = a]) (auto simp: cong_def mod_exp_nat_def list.pred_set)
 
 lemma list_all_ConsI: "P x \<Longrightarrow> list_all P xs \<Longrightarrow> list_all P (x # xs)"
   by simp
 
 ML_file \<open>pratt.ML\<close>
 
 method_setup pratt = \<open>
   Scan.lift (Pratt.tac_config_parser -- Scan.option Pratt.cert_cartouche) >> 
     (fn (config, cert) => fn ctxt => SIMPLE_METHOD (HEADGOAL (Pratt.tac config cert ctxt)))
 \<close> "Prove primality of natural numbers using Pratt certificates."
 
 text \<open>
   The proof method replays a given Pratt certificate to prove the primality of a given number.
   If no certificate is given, the method attempts to compute one. The computed certificate is then
   also printed with a prompt to insert it into the proof document so that it does not have to
   be recomputed the next time.
 
   The format of the certificates is compatible with those generated by Mathematica. Therefore,
   for larger numbers, certificates generated by Mathematica can be used with this method directly.
 \<close>
 lemma "prime (47 :: nat)"
   by (pratt (silent))
 
 lemma "prime (2503 :: nat)"
   by pratt
 
 lemma "prime (7919 :: nat)"
   by pratt
 
 lemma "prime (131059 :: nat)"
   by (pratt \<open>{131059, 2, {2, {3, 2, {2}}, {809, 3, {2, {101, 2, {2, {5, 2, {2}}}}}}}}\<close>)
 
 end