Theory Lambda_Free_RPOs.Extension_Orders

(*  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 ‹Extension Orders›

theory Extension_Orders
imports Lambda_Free_Util Infinite_Chain "HOL-Cardinals.Wellorder_Extension"
begin

text ‹
This theory defines locales for categorizing extension orders used for orders on
λ›-free higher-order terms and defines variants of the lexicographic and
multiset orders.
›


subsection ‹Locales›

locale ext =
  fixes ext :: "('a  'a  bool)  'a list  'a list  bool"
  assumes
    mono_strong: "(y  set ys. x  set xs. gt y x  gt' y x)  ext gt ys xs  ext gt' ys xs" and
    map: "finite A  ys  lists A  xs  lists A  (x  A. ¬ gt (f x) (f x)) 
      (z  A. y  A. x  A. gt (f z) (f y)  gt (f y) (f x)  gt (f z) (f x)) 
      (y  A. x  A. gt y x  gt (f y) (f x))  ext gt ys xs  ext gt (map f ys) (map f xs)"
begin

lemma mono[mono]: "gt  gt'  ext gt  ext gt'"
  using mono_strong by blast

end

locale ext_irrefl = ext +
  assumes irrefl: "(x  set xs. ¬ gt x x)  ¬ ext gt xs xs"

locale ext_trans = ext +
  assumes trans: "zs  lists A  ys  lists A  xs  lists A 
    (z  A. y  A. x  A. gt z y  gt y x  gt z x)  ext gt zs ys  ext gt ys xs 
    ext gt zs xs"

locale ext_irrefl_before_trans = ext_irrefl +
  assumes trans_from_irrefl: "finite A  zs  lists A  ys  lists A  xs  lists A 
    (x  A. ¬ gt x x)  (z  A. y  A. x  A. gt z y  gt y x  gt z x)  ext gt zs ys 
    ext gt ys xs  ext gt zs xs"

locale ext_trans_before_irrefl = ext_trans +
  assumes irrefl_from_trans: "(z  set xs. y  set xs. x  set xs. gt z y  gt y x  gt z x) 
    (x  set xs. ¬ gt x x)  ¬ ext gt xs xs"

locale ext_irrefl_trans_strong = ext_irrefl +
  assumes trans_strong: "(z  set zs. y  set ys. x  set xs. gt z y  gt y x  gt z x) 
    ext gt zs ys  ext gt ys xs  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  ext gt (x # ys) (x # xs)"
begin

lemma compat_append_left: "ext gt ys xs  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  ext gt (ys @ [x]) (xs @ [x])"
begin

lemma compat_append_right: "ext gt ys xs  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  x  gt y x  ext gt (xs @ y # xs') (xs @ x # xs')"

locale ext_singleton = ext +
  assumes singleton: "y  x  ext gt [y] [x]  gt y x"

locale ext_compat_list_strong = ext_compat_cons + ext_compat_snoc + ext_singleton
begin

lemma compat_list: "y  x  gt y x  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: "(y  A. x  A. gt y x  gt x y  y = x)  ys  lists A  xs  lists A 
    ext gt ys xs  ext gt xs ys  ys = xs"

locale ext_wf = ext +
  assumes wf: "wfP (λx y. gt y x)  wfP (λxs ys. ext gt ys xs)"

locale ext_hd_or_tl = ext +
  assumes hd_or_tl: "(z y x. gt z y  gt y x  gt z x)  (y x. gt y x  gt x y  y = x) 
    length ys = length xs  ext gt (y # ys) (x # xs)  gt y x  ext gt ys xs"

locale ext_wf_bounded = ext_irrefl_before_trans + ext_hd_or_tl
begin

context
  fixes gt :: "'a  'a  bool"
  assumes
    gt_irrefl: "z. ¬ gt z z" and
    gt_trans: "z y x. gt z y  gt y x  gt z x" and
    gt_total: "y x. gt y x  gt x y  y = x" and
    gt_wf: "wfP (λx y. gt y x)"
begin

lemma irrefl_gt: "¬ ext gt xs xs"
  using irrefl gt_irrefl by simp

lemma trans_gt: "ext gt zs ys  ext gt ys xs  ext gt zs xs"
  by (rule trans_from_irrefl[of "set zs  set ys  set xs" zs ys xs gt])
    (auto intro: gt_trans simp: gt_irrefl)

lemma hd_or_tl_gt: "length ys = length xs  ext gt (y # ys) (x # xs)  gt y x  ext gt ys xs"
  by (rule hd_or_tl) (auto intro: gt_trans simp: gt_total)

lemma wf_same_length_if_total: "wfP (λxs ys. length ys = n  length xs = n  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 "ys xs. gt_hd ys xs  gt (hd ys) (hd xs)"
  define gt_tl where "ys xs. gt_tl ys xs  ext gt (tl ys) (tl xs)"

  have hd_tl: "gt_hd ys xs  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 = "λys xs. length ys = n  length xs = n  ext gt ys xs"
    let ?gtsSn = "λys xs. length ys = Suc n  length xs = Suc n  ext gt ys xs"
    let ?gttlSn = "λys xs. length ys = Suc n  length xs = Suc n  gt_tl ys xs"

    assume "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 "¬ 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 "¬ inf_chain ?gtsn (tl  ?ff)"
      using wfP_iff_no_inf_chain[THEN iffD1, OF ih] by blast
    hence tl_good: "¬ 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 (λxs ys. length ys  n  length xs  n  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 = "λys xs. length ys  n  length xs  n  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 (λ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: "i. bad ?gtsle (?ff i)"
    by (rule inf_chain_bad[OF ff_bad])

  have len_le_n: "i. length (?ff i)  n"
    using worst_chain_pred[OF wf_len xs_bad] by simp
  have len_le_Suc: "i. length (?ff i)  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 "k. length (?ff k) = n")
    case False
    hence len_lt_n: "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 = "λys xs. length ys  n - 1  length xs  n - 1  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 = "λys xs. length ys = n  length xs = n  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 (λi. ?ff (i + k))"
      by (rule inf_chain_offset[OF ff_bad])
    hence "inf_chain ?gtssl (λi. ?ff (i + k))"
      unfolding inf_chain_def using len_eq_n by presburger
    hence "¬ wfP (λ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  'a  bool"
  assumes
    gt_irrefl: "z. ¬ gt z z" and
    gt_wf: "wfP (λx y. gt y x)"
begin

lemma wf_bounded: "wfP (λxs ys. length ys  n  length xs  n  ext gt ys xs)"
proof -
  obtain Ge' where
    gt_sub_Ge': "{(x, y). gt y x}  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 "y x. gt' y x  y  x  (x, y)  Ge'"

  have gt_imp_gt': "gt  gt'"
    by (auto simp: gt'_def gt_irrefl intro: gt_sub_Ge'[THEN subsetD])

  have gt'_irrefl: "z. ¬ gt' z z"
    unfolding gt'_def by simp

  have gt'_trans: "z y x. gt' z y  gt' y x  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)  Ge'  x  y}"
    by (rule Ge'_wo[unfolded well_order_on_def set_diff_eq
      case_prod_eta[symmetric, of "λxy. xy  Ge'  xy  Id"] pair_in_Id_conv, THEN conjunct2])
  moreover have "y x. (x, y)  Ge'  x  y  y  x  (x, y)  Ge'"
    by auto
  ultimately have gt'_wf: "wfP (λx y. gt' y x)"
    unfolding wfp_def gt'_def by simp

  have gt'_total: "x y. gt' y x  gt' x y  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 (λxs ys. length ys  n  length xs  n  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 ‹Lexicographic Extension›

inductive lexext :: "('a  'a  bool)  'a list  'a list  bool" for gt where
  lexext_Nil: "lexext gt (y # ys) []"
| lexext_Cons: "gt y x  lexext gt (y # ys) (x # xs)"
| lexext_Cons_eq: "lexext gt ys xs  lexext gt (x # ys) (x # xs)"

lemma lexext_simps[simp]:
  "lexext gt ys []  ys  []"
  "¬ lexext gt [] xs"
  "lexext gt (y # ys) (x # xs)  gt y x  x = y  lexext gt ys xs"
proof
  show "lexext gt ys []  (ys  [])"
    by (metis lexext.cases list.distinct(1))
next
  show "ys  []  lexext gt ys []"
    by (metis lexext_Nil list.exhaust)
next
  show "¬ lexext gt [] xs"
    using lexext.cases by auto
next
  show "lexext gt (y # ys) (x # xs) = (gt y x  x = y  lexext gt ys xs)"
  proof -
    have fwdd: "lexext gt (y # ys) (x # xs)  gt y x  x = y  lexext gt ys xs"
    proof
      assume "lexext gt (y # ys) (x # xs)"
      thus "gt y x  x = y  lexext gt ys xs"
        using lexext.cases by blast
    qed
    have backd: "gt y x  x = y  lexext gt ys xs  lexext gt (y # ys) (x # xs)"
      by (simp add: lexext_Cons lexext_Cons_eq)
    show "lexext gt (y # ys) (x # xs) = (gt y x  x = y  lexext gt ys xs)"
      using fwdd backd by blast
  qed
qed

lemma lexext_mono_strong:
  assumes
    "y  set ys. x  set xs. gt y x  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:
  "(y  set ys. x  set xs. gt y x  gt (f y) (f x))  lexext gt ys xs 
   lexext gt (map f ys) (map f xs)"
  by (induct ys xs rule: list_induct2') auto

lemma lexext_irrefl:
  assumes "x  set xs. ¬ gt x x"
  shows "¬ lexext gt xs xs"
  using assms by (induct xs) auto

lemma lexext_trans_strong:
  assumes
    "z  set zs. y  set ys. x  set xs. gt z y  gt y x  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  lexext gt (xs @ y # xs') (xs @ x # xs')"
  by (induct xs) auto

lemma lexext_singleton: "lexext gt [y] [x]  gt y x"
  by simp

lemma lexext_total: "(y  B. x  A. gt y x  gt x y  y = x)  ys  lists B  xs  lists A 
  lexext gt ys xs  lexext gt xs ys  ys = xs"
  by (induct ys xs rule: list_induct2') auto

lemma lexext_hd_or_tl: "lexext gt (y # ys) (x # xs)  gt y x  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 ‹Reverse (Right-to-Left) Lexicographic Extension›

abbreviation lexext_rev :: "('a  'a  bool)  'a list  'a list  bool" where
  "lexext_rev gt ys xs  lexext gt (rev ys) (rev xs)"

lemma lexext_rev_simps[simp]:
  "lexext_rev gt ys []  ys  []"
  "¬ lexext_rev gt [] xs"
  "lexext_rev gt (ys @ [y]) (xs @ [x])  gt y x  x = y  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)  lexext_rev gt ys xs  ys = xs  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
    "y  set ys. x  set xs. gt y x  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:
  "(y  set ys. x  set xs. gt y x  gt (f y) (f x))  lexext_rev gt ys xs 
   lexext_rev gt (map f ys) (map f xs)"
  by (simp add: lexext_map_strong rev_map)

lemma lexext_rev_irrefl:
  assumes "x  set xs. ¬ gt x x"
  shows "¬ lexext_rev gt xs xs"
  using assms by (simp add: lexext_irrefl)

lemma lexext_rev_trans_strong:
  assumes
    "z  set zs. y  set ys. x  set xs. gt z y  gt y x  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  lexext_rev gt (ys @ [x]) (xs @ [x])"
  by (simp add: lexext_compat_cons)

lemma lexext_rev_compat_list: "gt y x  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]  gt y x"
  by simp

lemma lexext_rev_total:
  "(y  B. x  A. gt y x  gt x y  y = x)  ys  lists B  xs  lists A 
   lexext_rev gt ys xs  lexext_rev gt xs ys  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  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 ‹Generic Length Extension›

definition lenext :: "('a list  'a list  bool)  'a list  'a list  bool" where
  "lenext gts ys xs  length ys > length xs  length ys = length xs  gts ys xs"

lemma
  lenext_mono_strong: "(gts ys xs  gts' ys xs)  lenext gts ys xs  lenext gts' ys xs" and
  lenext_map_strong: "(length ys = length xs  gts ys xs  gts (map f ys) (map f xs)) 
    lenext gts ys xs  lenext gts (map f ys) (map f xs)" and
  lenext_irrefl: "¬ gts xs xs  ¬ lenext gts xs xs" and
  lenext_trans: "(gts zs ys  gts ys xs  gts zs xs)  lenext gts zs ys  lenext gts ys xs 
    lenext gts zs xs" and
  lenext_snoc: "lenext gts (xs @ [x]) xs" and
  lenext_compat_cons: "(length ys = length xs  gts ys xs  gts (x # ys) (x # xs)) 
    lenext gts ys xs  lenext gts (x # ys) (x # xs)" and
  lenext_compat_snoc: "(length ys = length xs  gts ys xs  gts (ys @ [x]) (xs @ [x])) 
    lenext gts ys xs  lenext gts (ys @ [x]) (xs @ [x])" and
  lenext_compat_list: "gts (xs @ y # xs') (xs @ x # xs') 
    lenext gts (xs @ y # xs') (xs @ x # xs')" and
  lenext_singleton: "lenext gts [y] [x]  gts [y] [x]" and
  lenext_total: "(gts ys xs  gts xs ys  ys = xs) 
    lenext gts ys xs  lenext gts xs ys  ys = xs" and
  lenext_hd_or_tl: "(length ys = length xs  gts (y # ys) (x # xs)  gt y x  gts ys xs) 
    lenext gts (y # ys) (x # xs)  gt y x  lenext gts ys xs"
  unfolding lenext_def by auto


subsection ‹Length-Lexicographic Extension›

abbreviation len_lexext :: "('a  'a  bool)  'a list  'a list  bool" where
  "len_lexext gt  lenext (lexext gt)"

lemma len_lexext_mono_strong:
  "(y  set ys. x  set xs. gt y x  gt' y x)  len_lexext gt ys xs  len_lexext gt' ys xs"
  by (rule lenext_mono_strong[OF lexext_mono_strong])

lemma len_lexext_map_strong:
  "(y  set ys. x  set xs. gt y x  gt (f y) (f x))  len_lexext gt ys xs 
   len_lexext gt (map f ys) (map f xs)"
  by (rule lenext_map_strong) (metis lexext_map_strong)

lemma len_lexext_irrefl: "(x  set xs. ¬ gt x x)  ¬ len_lexext gt xs xs"
  by (rule lenext_irrefl[OF lexext_irrefl])

lemma len_lexext_trans_strong:
  "(z  set zs. y  set ys. x  set xs. gt z y  gt y x  gt z x)  len_lexext gt zs ys 
   len_lexext gt ys xs  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  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  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  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]  gt y x"
  by (simp only: lenext_singleton lexext_singleton)

lemma len_lexext_total: "(y  B. x  A. gt y x  gt x y  y = x)  ys  lists B  xs  lists A 
  len_lexext gt ys xs  len_lexext gt xs ys  ys = xs"
  by (rule lenext_total[OF lexext_total])

lemma len_lexext_iff_lenlex: "len_lexext gt ys xs  (xs, ys)  lenlex {(x, y). gt y x}"
proof -
  {
    assume "length xs = length ys"
    hence "lexext gt ys xs  (xs, ys)  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 (λx y. gt y x)  wfP (λ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)  gt y x  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 ‹Reverse (Right-to-Left) Length-Lexicographic Extension›

abbreviation len_lexext_rev :: "('a  'a  bool)  'a list  'a list  bool" where
  "len_lexext_rev gt  lenext (lexext_rev gt)"

lemma len_lexext_rev_mono_strong:
  "(y  set ys. x  set xs. gt y x  gt' y x)  len_lexext_rev gt ys xs  len_lexext_rev gt' ys xs"
  by (rule lenext_mono_strong) (rule lexext_rev_mono_strong)

lemma len_lexext_rev_map_strong:
  "(y  set ys. x  set xs. gt y x  gt (f y) (f x))  len_lexext_rev gt ys xs 
   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: "(x  set xs. ¬ gt x x)  ¬ len_lexext_rev gt xs xs"
  by (rule lenext_irrefl) (rule lexext_rev_irrefl)

lemma len_lexext_rev_trans_strong:
  "(z  set zs. y  set ys. x  set xs. gt z y  gt y x  gt z x)  len_lexext_rev gt zs ys 
   len_lexext_rev gt ys xs  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  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  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  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]  gt y x"
  by (simp only: lenext_singleton lexext_rev_singleton)

lemma len_lexext_rev_total: "(y  B. x  A. gt y x  gt x y  y = x)  ys  lists B 
  xs  lists A  len_lexext_rev gt ys xs  len_lexext_rev gt xs ys  ys = xs"
  by (rule lenext_total[OF lexext_rev_total])

lemma len_lexext_rev_iff_len_lexext: "len_lexext_rev gt ys xs  len_lexext gt (rev ys) (rev xs)"
  unfolding lenext_def by simp

lemma len_lexext_rev_wf: "wfP (λx y. gt y x)  wfP (λxs ys. len_lexext_rev gt ys xs)"
  unfolding len_lexext_rev_iff_len_lexext
  by (rule wfP_app[of "λ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)  gt y x  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 ‹Dershowitz--Manna Multiset Extension›

definition msetext_dersh where
  "msetext_dersh gt ys xs = (let N = mset ys; M = mset xs in
     (Y X. Y  {#}  Y ⊆# N  M = (N - Y) + X  (x. x ∈# X  (y. y ∈# Y  gt y x))))"

text ‹
The following proof is based on that of @{thm[source] less_multisetDM_imp_mult}.
›

lemma msetext_dersh_imp_mult_rel:
  assumes
    ys_a: "ys  lists A" and xs_a: "xs  lists A" and
    ys_gt_xs: "msetext_dersh gt ys xs"
  shows "(mset xs, mset ys)  mult {(x, y). x  A  y  A  gt y x}"
proof -
  obtain Y X where y_nemp: "Y  {#}" and y_sub_ys: "Y ⊆# mset ys" and
    xs_eq: "mset xs = mset ys - Y + X" and ex_y: "x. x ∈# X  (y. y ∈# Y  gt y x)"
    using ys_gt_xs[unfolded msetext_dersh_def Let_def] by blast
  have ex_y': "x. x ∈# X  (y. y ∈# Y  x  A  y  A  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)  mult {(x, y). x  A  y  A  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  (mset xs, mset ys)  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)  A" and xs_a: "set_mset (mset xs)  A" and
    in_mult: "(mset xs, mset ys)  mult {(x, y). x  A  y  A  gt y x}" and
    trans: "z  A. y  A. x  A. gt z y  gt y x  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 "a. a ∈# X  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  A"
    using ys_zs_in_mult1 zs_a unfolding mult1_def by auto

  obtain Y X where y_nemp: "Y  {#}" and y_sub_ys: "Y ⊆# Ys" and xs_eq: "mset xs = Ys - Y + X" and
    ex_y: "x. x ∈# X  (y. y ∈# Y  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: "y. y ∈# Ya  y  A  z  A  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  set_mset (X + Ya)"
    by (metis diff_subset_eq_self in_diffD subsetI subset_mset.diff_diff_right)

  have x_a: "set_mset X  A"
    using xs_a xs_eq by auto
  have ya_a: "set_mset Ya  A"
    by (simp add: subsetI z_gt)

  have ex_y': "y. y ∈# Y - Ya + {#z#}  gt y x" if x_in: "x ∈# X + Ya" for x
  proof (cases "x ∈# X")
    case True
    then obtain y where y_in: "y ∈# Y" and y_gt_x: "gt y x"
      using ex_y by blast
    show ?thesis
    proof (cases "y ∈# Ya")
      case False
      hence "y ∈# Y - Ya + {#z#}"
        using y_in by fastforce
      thus ?thesis
        using y_gt_x by blast
    next
      case True
      hence "y  A" and "z  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 ∈# Ya"
      using x_in by auto
    hence "x  A" and "z  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#} ⊆# 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 "x. x ∈# X + Ya + (Y - Ya) - Y  (y. y ∈# Y - Ya + {#z#}  gt y x)"
      using ex_y' xa_sub_x_ya by blast
  qed auto
qed

lemma msetext_dersh_mono_strong:
  "(y  set ys. x  set xs. gt y x  gt' y x)  msetext_dersh gt ys xs 
  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: "y  set ys. x  set xs. gt y x  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  {#}" and y_sub_ys: "Y ⊆# mset ys" and xs_eq: "mset xs = mset ys - Y + X" and
    ex_y: "x. x ∈# X  (y. y ∈# Y  gt y x)"
    using ys_gt_xs[unfolded msetext_dersh_def Let_def mset_map] by blast

  have x_sub_xs: "X ⊆# 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: "x. x ∈# X  y x ∈# Y  gt (y x) x"
      using ex_y by moura

    show "fx. fx ∈# ?fX  (fy. fy ∈# ?fY  gt fy fx)"
    proof (intro allI impI)
      fix fx
      assume "fx ∈# ?fX"
      then obtain x where fx: "fx = f x" and x_in: "x ∈# X"
        by auto
      hence y_in: "y x ∈# Y" and y_gt: "gt (y x) x"
        using y[rule_format, OF x_in] by blast+
      hence "f (y x) ∈# ?fY  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 "fy. fy ∈# ?fY  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  lists A" and
    ys_a: "ys  lists A" and
    xs_a: "xs  lists A" and
    trans: "z  A. y  A. x  A. gt z y  gt y x  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)  A"
    using zs_a by auto
next
  show "set_mset (mset xs)  A"
    using xs_a by auto
next
  let ?Gt = "{(x, y). x  A  y  A  gt y x}"

  have "(mset xs, mset ys)  mult ?Gt"
    by (rule msetext_dersh_imp_mult_rel[OF ys_a xs_a ys_gt_xs])
  moreover have "(mset ys, mset zs)  mult ?Gt"
    by (rule msetext_dersh_imp_mult_rel[OF zs_a ys_a zs_gt_ys])
  ultimately show "(mset xs, mset zs)  mult ?Gt"
    unfolding mult_def by simp
qed

lemma msetext_dersh_irrefl_from_trans:
  assumes
    trans: "z  set xs. y  set xs. x  set xs. gt z y  gt y x  gt z x" and
    irrefl: "x  set xs. ¬ gt x x"
  shows "¬ msetext_dersh gt xs xs"
  unfolding msetext_dersh_def Let_def
proof clarify
  fix Y X
  assume y_nemp: "Y  {#}" and y_sub_xs: "Y ⊆# mset xs" and xs_eq: "mset xs = mset xs - Y + X" and
    ex_y: "x. x ∈# X  (y. y ∈# Y  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 ∈# Y  x ∈# Y  gt y x}"

  have "?Gt  set_mset Y × 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: "¬ acyclic ?Gt"
    proof (rule finite_nonempty_ex_succ_imp_cyclic)
      show "x ∈# Y. y ∈# Y. (y, x)  ?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  {#}" and y_sub_ys: "Y ⊆# mset ys" and xs_eq: "mset xs = mset ys - Y + X" and
    ex_y: "x. x ∈# X  (y. y ∈# Y  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 ⊆# 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  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]  gt y x"
  unfolding msetext_dersh_def Let_def
  by (auto dest: nonempty_subseteq_mset_eq_single simp: nonempty_subseteq_mset_iff_single)

lemma msetext_dersh_wf:
  assumes wf_gt: "wfP (λx y. gt y x)"
  shows "wfP (λxs ys. msetext_dersh gt ys xs)"
proof (rule wfp_subset, rule wfP_app[of "λxs ys. (xs, ys)  mult {(x, y). gt y x}" mset])
  show "wfP (λxs ys. (xs, ys)  mult {(x, y). gt y x})"
    using wf_gt unfolding wfp_def by (auto intro: wf_mult)
next
  show "(λxs ys. msetext_dersh gt ys xs)  (λx y. (mset x, mset y)  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 ‹Huet--Oppen Multiset Extension›

definition msetext_huet where
  "msetext_huet gt ys xs = (let N = mset ys; M = mset xs in
     M  N  (x. count M x > count N x  (y. gt y x  count N y > count M y)))"

lemma msetext_huet_imp_count_gt:
  assumes ys_gt_xs: "msetext_huet gt ys xs"
  shows "x. count (mset ys) x > count (mset xs) x"
proof -
  obtain x where "count (mset ys) x  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  {#}"
    by (metis msetext_huet_imp_count_gt[OF huet] empty_iff in_diff_count set_mset_empty)
  show "?Y ⊆# mset ys"
    by auto
  show "mset xs = mset ys - ?Y + ?X"
    by (rule multiset_eqI) simp
  show "x. x ∈# ?X  (y. y ∈# ?Y  gt y x)"
    using huet[unfolded msetext_huet_def Let_def, THEN conjunct2] by (meson in_diff_count)
qed

text ‹
The following proof is based on that of @{thm[source] mult_imp_less_multisetHO}.
›

lemma mult_imp_msetext_huet:
  assumes
    irrefl: "irreflp gt" and trans: "transp gt" and
    in_mult: "(mset xs, mset ys)  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  Ys" and
    **: "x. count Ys x < count (mset xs) x  (y. gt y x  count (mset xs) y < count Ys y)"
    by blast+
  from step(2) obtain M0 a K where
    *: "Zs = M0 + {#a#}" "Ys = M0 + K" "a ∉# K" "b. b ∈# K  gt a b"
    using irrefl unfolding mult1_def irreflp_def by force
  have "mset xs  Zs"
  proof (cases "K = {#}")
    case True
    thus ?thesis
      using mset xs  Ys ** *(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  'a" where
        f1: "a. ¬ count Ys a < count (mset xs) a  gt (aa a) a 
          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: "aa. count Zs aa = count M0 aa + count {#a#} aa"
        by (simp add: *(1))
      have f4: "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 "m. count m a = 0 + count m a"
        by simp
      moreover
      { assume "aa a  a"
        then have "mset xs = Zs  count Zs (aa a) < count K (aa a) + count M0 (aa a) 
          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  count (mset xs) a"
    with a ∉# K 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  count Zs z"
      using asym by (auto simp: intro: count_inI dest: antisympD)
    with z have "z. gt z a  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 "x. gt x y  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 ∈# K")
        case True
        with *(4) have "gt a y" by simp
        then show ?thesis
          by (cases "count Zs a  count (mset xs) a",
            blast dest: count_a trans[unfolded transp_def, rule_format], auto dest: count_a)
      next
        case False
        with y  a 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 ∈# K")
          case True
          with *(4) have "gt a z" by simp
          with z(1) show ?thesis
            by (cases "count Zs a  count (mset xs) a")
              (blast dest: count_a not_le_imp_less trans[unfolded transp_def, rule_format])+
        next
          case False
          with a ∉# K have "count Ys z  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  transp gt  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:
  "(y  set ys. x  set xs. gt y x  gt' y x)  msetext_huet gt ys xs  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  lists A" and xs_a: "xs  lists A" and
    irrefl_f: "x  A. ¬ gt (f x) (f x)" and
    trans_f: "z  A. y  A. x  A. gt (f z) (f y)  gt (f y) (f x)  gt (f z) (f x)" and
    compat_f: "y  A. x  A. gt y x  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: "x  A. ¬ gt x x"
    using irrefl_f compat_f by blast

  have
    ms_xs_ne_ys: "mset xs  mset ys" and
    ex_gt: "x. count (mset ys) x < count (mset xs) x 
      (y. gt y x  count (mset xs) y < count (mset ys) y)"
    using ys_gt_xs[unfolded msetext_huet_def Let_def] by blast+

  have ex_y: "y. gt (f y) (f x)  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  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  A"
      using cnt_y ys_a dual_order.strict_trans2 by fastforce

    have wf_gt_f: "wfP (λy x. y  A  x  A  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: "y  A. yy  A  gt (f y) (f yy)  gt (f y) (f x) 
        count (mset xs) y  count (mset ys) y"
      using wfp_eq_minimal[THEN iffD1, OF wf_gt_f, rule_format,
          of y "{y. gt (f y) (f x)  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  A"
      using cnt_yy ys_a dual_order.strict_trans2 by fastforce

    {
      assume "count (mset ?fxs) (f yy)  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  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  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  mset ?fys"
        using ex_y by fastforce
    }
    thus "mset ?fxs  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 "fy. gt fy fx  count (mset ?fxs) fy < count (mset (map f ys)) fy"
      using ex_y[OF cnt_x] by blast
  qed
qed

lemma msetext_huet_irrefl: "(x  set xs. ¬ gt x x)  ¬ 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  lists A" and ys_a: "ys  lists A" and xs_a: "xs  lists A" and
    irrefl: "x  A. ¬ gt x x" and
    trans: "z  A. y  A. x  A. gt z y  gt y x  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 (λy x. y  A  x  A  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  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: "y  A. xx  A  gt y xx  count (mset ys) y  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  A"
      using cnt_xx zs_a dual_order.strict_trans2 by fastforce

    show "mset xs  mset zs"
    proof (cases "count (mset ys) xx  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  A"
        using cnt_z ys_a dual_order.strict_trans2 by fastforce

      have "count (mset zs) z  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  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  A"
      using cnt_x_xz xs_a dual_order.strict_trans2 by fastforce

    let ?case = "y. gt y x  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  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: "y  A. yy  A  gt y yy  gt y x  count (mset ys) y  count (mset zs) y"
        using wfp_eq_minimal[THEN iffD1, OF wf_gt, rule_format,
            of y "{y. gt y x  count (mset ys) y < count (mset zs) y}", simplified]
          y_gt_x cnt_y
        by force
      have yy_in_a: "yy  A"
        using cnt_yy zs_a dual_order.strict_trans2 by fastforce

      have ?case
      proof (cases "count (mset ys) yy  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  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  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  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  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  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: "y  A. yy  A  gt y yy  gt y x  count (mset xs) y  count (mset ys) y"
        using wfp_eq_minimal[THEN iffD1, OF wf_gt, rule_format,
            of y "{y. gt y x  count (mset xs) y < count (mset ys) y}", simplified]
          y_gt_x cnt_y
        by force
      have yy_in_a: "yy  A"
        using cnt_yy ys_a dual_order.strict_trans2 by fastforce

      have ?case
      proof (cases "count (mset zs) yy  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  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  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  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 "y. gt y x  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  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  msetext_huet gt (ys @ [x]) (xs @ [x])"
  unfolding msetext_huet_def Let_def by auto

lemma msetext_huet_compat_list: "y  x  gt y x  msetext_huet gt (xs @ y # xs') (xs @ x # xs')"
  unfolding msetext_huet_def Let_def by auto

lemma msetext_huet_singleton: "y  x  msetext_huet gt [y] [x]  gt y x"
  unfolding msetext_huet_def by simp

lemma msetext_huet_wf: "wfP (λx y. gt y x)  wfP (λ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: "z y x. gt z y  gt y x  gt z x" and
    total: "y x. gt y x  gt x y  y = x" and
    len_eq: "length ys = length xs" and
    yys_gt_xxs: "msetext_huet gt (y # ys) (x # xs)"
  shows "gt y x  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  ?X" and
    ex_gt_Y: "xa. count ?X xa > count ?Y xa  ya. gt ya xa  count ?Y ya > count ?X ya"
    using yys_gt_xxs[unfolded msetext_huet_def Let_def] by auto
  obtain yy where
    yy: "xa. count ?X xa > count ?Y xa  gt (yy xa) xa  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  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  x" for xa
    using that by (auto split: if_splits)

  {
    assume y_eq_x: "y = x"
    have "?Xa  ?Ya"
      using y_eq_x Y_ne_X by simp
    moreover have "xa. count ?Xa xa > count ?Ya xa  ya. gt ya xa  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  'a" where
        f3: "a. ¬ count (mset (y # ys)) a < count (mset (x # xs)) a  gt (aa a) a 
          count (mset (x # xs)) (aa a) < count (mset (y # ys)) (aa a)"
        by (metis (full_types))
      then have f4: "a. count (mset (x # xs)) (aa a) < count (mset (x # ys)) (aa a) 
          ¬ count (mset (x # ys)) a < count (mset (x # xs)) a"
        using y_eq_x by meson
      have "a as aa. count (mset ((a::'a) # as)) aa = count (mset as) aa  aa = a"
        by fastforce
      then have "xa = x  count (mset (x # xs)) (aa xa) < count (mset (x # ys)) (aa xa)"
        using f4 a1 by (metis (no_types))
      then show "a. gt a xa  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: "¬ gt y x"
    hence y_ne_x: "y  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  ?Ya"
    proof (cases "z = x")
      case True
      hence "yy z  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 "ya. gt ya xa  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  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  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  count ?Ya y  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  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  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 ‹Componentwise Extension›

definition cwiseext :: "('a  'a  bool)  'a list  'a list  bool" where
  "cwiseext gt ys xs  length ys = length xs
      (i < length ys. gt (ys ! i) (xs ! i)  ys ! i = xs ! i)
      (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: "i. i < j0  ¬ 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: "i. i < j0  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: "i. i < Suc k  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: "i. i < k  ¬ gt (ys ! i) (xs ! i)"
        using Sk_min by simp

      have k_eq: "i. i < k  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:
  "(y  set ys. x  set xs. gt y x  gt' y x)  cwiseext gt ys xs  cwiseext gt' ys xs"
  unfolding cwiseext_def by (induct, force, fast)

lemma cwiseext_map_strong:
  "(y  set ys. x  set xs. gt y x  gt (f y) (f x))  cwiseext gt ys xs 
   cwiseext gt (map f ys) (map f xs)"
  unfolding cwiseext_def by auto

lemma cwiseext_irrefl: "(x  set xs. ¬ gt x x)  ¬ cwiseext gt xs xs"
  unfolding cwiseext_def by (blast intro: nth_mem)

lemma cwiseext_trans_strong:
  assumes
    "z  set zs. y  set ys. x  set xs. gt z y  gt y x  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  cwiseext gt (x # ys) (x # xs)"
  unfolding cwiseext_def
proof (elim conjE, intro conjI)
  assume
    "length ys = length xs" and
    "i < length ys. gt (ys ! i) (xs ! i)  ys ! i = xs ! i"
  thus "i < length (x # ys). gt ((x # ys) ! i) ((x # xs) ! i)  (x # ys) ! i = (x # xs) ! i"
    by (simp add: nth_Cons')
next
  assume "i < length ys. gt (ys ! i) (xs ! i)"
  thus "i < length (x # ys). gt ((x # ys) ! i) ((x # xs) ! i)"
    by fastforce
qed auto

lemma cwiseext_compat_snoc: "cwiseext gt ys xs  cwiseext gt (ys @ [x]) (xs @ [x])"
  unfolding cwiseext_def
proof (elim conjE, intro conjI)
  assume
    "length ys = length xs" and
    "i < length ys. gt (ys ! i) (xs ! i)  ys ! i = xs ! i"
  thus "i < length (ys @ [x]).
    gt ((ys @ [x]) ! i) ((xs @ [x]) ! i)  (ys @ [x]) ! i = (xs @ [x]) ! i"
    by (simp add: nth_append)
next
  assume
    "length ys = length xs" and
    "i < length ys. gt (ys ! i) (xs ! i)"
  thus "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 "i < length (xs @ y # xs'). gt ((xs @ y # xs') ! i) ((xs @ x # xs') ! i)
     (xs @ y # xs') ! i = (xs @ x # xs') ! i"
    using y_gt_x by (simp add: nth_Cons' nth_append)
next
  show "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]  gt y x"
  unfolding cwiseext_def by auto

lemma cwiseext_wf: "wfP (λx y. gt y x)  wfP (λ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)  gt y x  cwiseext gt ys xs"
  unfolding cwiseext_def
proof (elim conjE, intro disj_imp[THEN iffD2, rule_format] conjI)
  assume
    "i < length (y # ys). gt ((y # ys) ! i) ((x # xs) ! i)" and
    "¬ gt y x"
  thus "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  'a  bool"
  assumes
    gt_irrefl: "¬ gt x x" and
    trans_gt: "ext gt zs ys  ext gt ys xs  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  xs"
    proof -
      have ys_gtcw_xs: "cwiseext gt ys xs"
        using yys_gtcw_xxs unfolding cwiseext_def
      proof (elim conjE, intro conjI)
        assume
          "i < length (y # ys). gt ((y # ys) ! i) ((x # xs) ! i)  (y # ys) ! i = (x # xs) ! i"
        hence ge: "i < length ys. gt (ys ! i) (xs ! i)  ys ! i = xs ! i"
          by auto
        thus "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  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  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