Theory Multiset_Extension2

section ‹Multiset extension of order pairs in the other direction›

text ‹Many term orders are formulated in the other direction, i.e., they use
  strong normalization of $>$ instead of well-foundedness of $<$. Here, we
  flip the direction of the multiset extension of two orders, connect it to existing interfaces,
  and prove some further properties of the multiset extension.›

theory Multiset_Extension2
  imports
    List_Order
    Multiset_Extension_Pair
begin

subsection ‹List based characterization of @{const multpw}›

lemma multpw_listI:
  assumes "length xs = length ys" "X = mset xs" "Y = mset ys"
    "∀i. i < length ys ⟶ (xs ! i, ys ! i) ∈ ns"
  shows "(X, Y) ∈ multpw ns"
  using assms
proof (induct xs arbitrary: ys X Y)
  case (Nil ys) then show ?case by (cases ys) (auto intro: multpw.intros)
next
  case Cons1: (Cons x xs ys' X Y) then show ?case
  proof (cases ys')
    case (Cons y ys)
    then have "∀i. i < length ys ⟶ (xs ! i, ys ! i) ∈ ns" using Cons1(5) by fastforce
    then show ?thesis using Cons1(2,5) by (auto intro!: multpw.intros simp: Cons(1) Cons1)
  qed auto
qed

lemma multpw_listE:
  assumes "(X, Y) ∈ multpw ns"
  obtains xs ys where "length xs = length ys" "X = mset xs" "Y = mset ys"
    "∀i. i < length ys ⟶ (xs ! i, ys ! i) ∈ ns"
  using assms
proof (induct X Y arbitrary: thesis rule: multpw.induct)
  case (add x y X Y)
  then obtain xs ys where "length xs = length ys" "X = mset xs"
    "Y = mset ys" "(∀i. i < length ys ⟶ (xs ! i, ys ! i) ∈ ns)" by blast
  then show ?case using add(1) by (intro add(4)[of "x # xs" "y # ys"]) (auto, case_tac i, auto)
qed auto

subsection‹Definition of the multiset extension of $>$-orders›

text‹We define here the non-strict extension of the order pair $(\geqslant, >)$ --
  usually written as (ns, s) in the sources --
  by just flipping the directions twice.›

definition ns_mul_ext :: "'a rel ⇒ 'a rel ⇒ 'a multiset rel"
  where "ns_mul_ext ns s ≡ (mult2_alt_ns (ns¯) (s¯))¯"

lemma ns_mul_extI:
  assumes "A = A1 + A2" and "B = B1 + B2"
    and "(A1, B1) ∈ multpw ns"
    and "⋀b. b ∈# B2 ⟹ ∃a. a ∈# A2 ∧ (a, b) ∈ s"
  shows "(A, B) ∈ ns_mul_ext ns s"
  using assms by (auto simp: ns_mul_ext_def multpw_converse intro!: mult2_alt_nsI)

lemma ns_mul_extE:
  assumes "(A, B) ∈ ns_mul_ext ns s"
  obtains A1 A2 B1 B2 where "A = A1 + A2" and "B = B1 + B2"
    and "(A1, B1) ∈ multpw ns"
    and "⋀b. b ∈# B2 ⟹ ∃a. a ∈# A2 ∧ (a, b) ∈ s"
  using assms by (auto simp: ns_mul_ext_def multpw_converse elim!: mult2_alt_nsE)

lemmas ns_mul_extI_old = ns_mul_extI[OF _ _ multpw_listI[OF _ refl refl], rule_format]

text‹Same for the "greater than" order on multisets.›

definition s_mul_ext :: "'a rel ⇒ 'a rel ⇒ 'a multiset rel"
  where "s_mul_ext ns s ≡ (mult2_alt_s (ns¯) (s¯))¯"

lemma s_mul_extI:
  assumes "A = A1 + A2" and "B = B1 + B2"
    and "(A1, B1) ∈ multpw ns"
    and "A2 ≠ {#}" and "⋀b. b ∈# B2 ⟹ ∃a. a ∈# A2 ∧ (a, b) ∈ s"
  shows "(A, B) ∈ s_mul_ext ns s"
  using assms by (auto simp: s_mul_ext_def multpw_converse intro!: mult2_alt_sI)

lemma s_mul_extE:
  assumes "(A, B) ∈ s_mul_ext ns s"
  obtains A1 A2 B1 B2 where "A = A1 + A2" and "B = B1 + B2"
    and "(A1, B1) ∈ multpw ns"
    and "A2 ≠ {#}" and "⋀b. b ∈# B2 ⟹ ∃a. a ∈# A2 ∧ (a, b) ∈ s"
  using assms by (auto simp: s_mul_ext_def multpw_converse elim!: mult2_alt_sE)

lemmas s_mul_extI_old = s_mul_extI[OF _ _ multpw_listI[OF _ refl refl], rule_format]


subsection‹Basic properties›

lemma s_mul_ext_mono:
  assumes "ns ⊆ ns'" "s ⊆ s'" shows "s_mul_ext ns s ⊆ s_mul_ext ns' s'"
  unfolding s_mul_ext_def using assms mono_mult2_alt[of "ns¯" "ns'¯" "s¯" "s'¯"] by simp

lemma ns_mul_ext_mono:
  assumes "ns ⊆ ns'" "s ⊆ s'" shows "ns_mul_ext ns s ⊆ ns_mul_ext ns' s'"
  unfolding ns_mul_ext_def using assms mono_mult2_alt[of "ns¯" "ns'¯" "s¯" "s'¯"] by simp

lemma s_mul_ext_local_mono:
  assumes sub: "(set_mset xs × set_mset ys) ∩ ns ⊆ ns'" "(set_mset xs × set_mset ys) ∩ s ⊆ s'"
    and rel: "(xs,ys) ∈ s_mul_ext ns s"
  shows "(xs,ys) ∈ s_mul_ext ns' s'"
  using rel s_mul_ext_mono[OF sub] mult2_alt_local[of ys xs False "ns¯" "s¯"]
  by (auto simp: s_mul_ext_def converse_Int ac_simps converse_Times)

lemma ns_mul_ext_local_mono:
  assumes sub: "(set_mset xs × set_mset ys) ∩ ns ⊆ ns'" "(set_mset xs × set_mset ys) ∩ s ⊆ s'"
    and rel: "(xs,ys) ∈ ns_mul_ext ns s"
  shows "(xs,ys) ∈ ns_mul_ext ns' s'"
  using rel ns_mul_ext_mono[OF sub] mult2_alt_local[of ys xs True "ns¯" "s¯"]
  by (auto simp: ns_mul_ext_def converse_Int ac_simps converse_Times)


text‹The empty multiset is the minimal element for these orders›

lemma ns_mul_ext_bottom: "(A,{#}) ∈ ns_mul_ext ns s"
  by (auto intro!: ns_mul_extI)

lemma ns_mul_ext_bottom_uniqueness:
  assumes "({#},A) ∈ ns_mul_ext ns s"
  shows "A = {#}"
  using assms by (auto simp: ns_mul_ext_def mult2_alt_ns_def)

lemma ns_mul_ext_bottom2:
  assumes "(A,B) ∈ ns_mul_ext ns s"
    and "B ≠ {#}"
  shows "A ≠ {#}"
  using assms by (auto simp: ns_mul_ext_def mult2_alt_ns_def)

lemma s_mul_ext_bottom:
  assumes "A ≠ {#}"
  shows "(A,{#}) ∈ s_mul_ext ns s"
  using assms by (auto simp: s_mul_ext_def mult2_alt_s_def)

lemma s_mul_ext_bottom_strict:
  "({#},A) ∉ s_mul_ext ns s"
  by (auto simp: s_mul_ext_def mult2_alt_s_def)

text‹Obvious introduction rules.›

lemma all_ns_ns_mul_ext:
  assumes "length as = length bs"
    and "∀i. i < length bs ⟶ (as ! i, bs ! i) ∈ ns"
  shows "(mset as, mset bs) ∈ ns_mul_ext ns s"
  using assms by (auto intro!: ns_mul_extI[of _ _ "{#}" _ _ "{#}"] multpw_listI)

lemma all_s_s_mul_ext:
  assumes "A ≠ {#}"
    and "∀b. b ∈# B ⟶ (∃a. a ∈# A ∧ (a,b) ∈ s)"
  shows "(A, B) ∈ s_mul_ext ns s"
  using assms by (auto intro!: s_mul_extI[of _ "{#}" _ _ "{#}"] multpw_listI)

text‹Being stricly lesser than implies being lesser than›

lemma s_ns_mul_ext:
  assumes "(A, B) ∈ s_mul_ext ns s"
  shows "(A, B) ∈ ns_mul_ext ns s"
  using assms by (simp add: s_mul_ext_def ns_mul_ext_def mult2_alt_s_implies_mult2_alt_ns)

text‹The non-strict order is reflexive.›

lemma multpw_refl':
  assumes "locally_refl ns A"
  shows "(A, A) ∈ multpw ns"
proof -
  have "Restr Id (set_mset A) ⊆ ns" using assms by (auto simp: locally_refl_def)
  from refl_multpw[of Id] multpw_local[of A A Id] mono_multpw[OF this]
  show ?thesis by (auto simp: refl_on_def)
qed

lemma ns_mul_ext_refl_local:
  assumes "locally_refl ns A"
  shows "(A, A) ∈ ns_mul_ext ns s"
  using assms by (auto intro!:  ns_mul_extI[of A A "{#}" A A "{#}" ns s] multpw_refl')

lemma ns_mul_ext_refl:
  assumes "refl ns"
  shows "(A, A) ∈ ns_mul_ext ns s"
  using assms ns_mul_ext_refl_local[of ns A s] unfolding refl_on_def locally_refl_def by auto

text‹The orders are union-compatible›

lemma ns_s_mul_ext_union_multiset_l:
  assumes "(A, B) ∈ ns_mul_ext ns s"
    and "C ≠ {#}"
    and "∀d. d ∈# D ⟶ (∃c. c ∈# C ∧ (c,d) ∈ s)"
  shows "(A + C, B + D) ∈ s_mul_ext ns s"
  using assms unfolding ns_mul_ext_def s_mul_ext_def
  by (auto intro!: converseI mult2_alt_ns_s_add mult2_alt_sI[of _ "{#}" _ _ "{#}"])

lemma s_mul_ext_union_compat:
  assumes "(A, B) ∈ s_mul_ext ns s"
    and "locally_refl ns C"
  shows "(A + C, B + C) ∈ s_mul_ext ns s"
  using assms ns_mul_ext_refl_local[OF assms(2)] unfolding ns_mul_ext_def s_mul_ext_def
  by (auto intro!: converseI mult2_alt_s_ns_add)

lemma ns_mul_ext_union_compat:
  assumes "(A, B) ∈ ns_mul_ext ns s"
    and "locally_refl ns C"
  shows "(A + C, B + C) ∈ ns_mul_ext ns s"
  using assms ns_mul_ext_refl_local[OF assms(2)] unfolding ns_mul_ext_def s_mul_ext_def
  by (auto intro!: converseI mult2_alt_ns_ns_add)

context
  fixes NS :: "'a rel"
  assumes NS: "refl NS"
begin

lemma refl_imp_locally_refl: "locally_refl NS A" using NS unfolding refl_on_def locally_refl_def by auto

lemma supseteq_imp_ns_mul_ext:
  assumes "A ⊇# B"
  shows "(A, B) ∈ ns_mul_ext NS S"
  using assms
  by (auto intro!: ns_mul_extI[of A B "A - B" B B "{#}"] multpw_refl' refl_imp_locally_refl
      simp: subset_mset.add_diff_inverse)

lemma supset_imp_s_mul_ext:
  assumes "A ⊃# B"
  shows "(A, B) ∈ s_mul_ext NS S"
  using assms subset_mset.add_diff_inverse[of B A]
  by (auto intro!: s_mul_extI[of A B "A - B" B B "{#}"] multpw_refl' refl_imp_locally_refl
      simp: Diff_eq_empty_iff_mset)

end

definition mul_ext :: "('a ⇒ 'a ⇒ bool × bool) ⇒ 'a list ⇒ 'a list ⇒ bool × bool"
  where "mul_ext f xs ys ≡ let s = {(x,y). fst (f x y)}; ns = {(x,y). snd (f x y)}
    in ((mset xs,mset ys) ∈ s_mul_ext ns s, (mset xs, mset ys) ∈ ns_mul_ext ns s)"

definition "smulextp f m n ⟷ (m, n) ∈ s_mul_ext {(x, y). snd (f x y)} {(x, y). fst (f x y)}"
definition "nsmulextp f m n ⟷ (m, n) ∈ ns_mul_ext {(x, y). snd (f x y)} {(x, y). fst (f x y)}"


lemma smulextp_cong[fundef_cong]:
  assumes "xs1 = ys1"
    and "xs2 = ys2"
    and "⋀ x x'. x ∈# ys1 ⟹ x' ∈# ys2 ⟹ f x x' = g x x'"
  shows "smulextp f xs1 xs2 = smulextp g ys1 ys2"
  unfolding smulextp_def
proof
  assume "(xs1, xs2) ∈ s_mul_ext {(x, y). snd (f x y)} {(x, y). fst (f x y)}"
  from s_mul_ext_local_mono[OF _ _ this, of "{(x, y). snd (g x y)}" "{(x, y). fst (g x y)}"]
  show "(ys1, ys2) ∈ s_mul_ext {(x, y). snd (g x y)} {(x, y). fst (g x y)}"
    using assms by force
next
  assume "(ys1, ys2) ∈ s_mul_ext {(x, y). snd (g x y)} {(x, y). fst (g x y)}"
  from s_mul_ext_local_mono[OF _ _ this, of "{(x, y). snd (f x y)}" "{(x, y). fst (f x y)}"]
  show "(xs1, xs2) ∈ s_mul_ext {(x, y). snd (f x y)} {(x, y). fst (f x y)}"
    using assms by force
qed

lemma nsmulextp_cong[fundef_cong]:
  assumes "xs1 = ys1"
    and "xs2 = ys2"
    and "⋀ x x'. x ∈# ys1 ⟹ x' ∈# ys2 ⟹ f x x' = g x x'"
  shows "nsmulextp f xs1 xs2 = nsmulextp g ys1 ys2"
  unfolding nsmulextp_def
proof
  assume "(xs1, xs2) ∈ ns_mul_ext {(x, y). snd (f x y)} {(x, y). fst (f x y)}"
  from ns_mul_ext_local_mono[OF _ _ this, of "{(x, y). snd (g x y)}" "{(x, y). fst (g x y)}"]
  show "(ys1, ys2) ∈ ns_mul_ext {(x, y). snd (g x y)} {(x, y). fst (g x y)}"
    using assms by force
next
  assume "(ys1, ys2) ∈ ns_mul_ext {(x, y). snd (g x y)} {(x, y). fst (g x y)}"
  from ns_mul_ext_local_mono[OF _ _ this, of "{(x, y). snd (f x y)}" "{(x, y). fst (f x y)}"]
  show "(xs1, xs2) ∈ ns_mul_ext {(x, y). snd (f x y)} {(x, y). fst (f x y)}"
    using assms by force
qed


definition "mulextp f m n = (smulextp f m n, nsmulextp f m n)"

lemma mulextp_cong[fundef_cong]:
  assumes "xs1 = ys1"
    and "xs2 = ys2"
    and "⋀ x x'. x ∈# ys1 ⟹ x' ∈# ys2 ⟹ f x x' = g x x'"
  shows "mulextp f xs1 xs2 = mulextp g ys1 ys2"
  unfolding mulextp_def using assms by (auto cong: nsmulextp_cong smulextp_cong)

lemma mset_s_mul_ext:
  "(mset xs, mset ys) ∈ s_mul_ext {(x, y). snd (f x y)} {(x, y).fst (f x y)} ⟷
    fst (mul_ext f xs ys)"
  by (auto simp: mul_ext_def Let_def)

lemma mset_ns_mul_ext:
  "(mset xs, mset ys) ∈ ns_mul_ext {(x, y). snd (f x y)} {(x, y).fst (f x y)} ⟷
    snd (mul_ext f xs ys)"
  by (auto simp: mul_ext_def Let_def)

lemma smulextp_mset_code:
  "smulextp f (mset xs) (mset ys) ⟷ fst (mul_ext f xs ys)"
  unfolding smulextp_def mset_s_mul_ext ..

lemma nsmulextp_mset_code:
  "nsmulextp f (mset xs) (mset ys) ⟷ snd (mul_ext f xs ys)"
  unfolding nsmulextp_def mset_ns_mul_ext ..

lemma nstri_mul_ext_map:
  assumes "⋀s t. s ∈ set ss ⟹ t ∈ set ts ⟹ fst (order s t) ⟹ fst (order' (f s) (f t))"
    and "⋀s t. s ∈ set ss ⟹ t ∈ set ts ⟹ snd (order s t) ⟹ snd (order' (f s) (f t))"
    and "snd (mul_ext order ss ts)"
  shows "snd (mul_ext order' (map f ss) (map f ts))"
  using assms mult2_alt_map[of "mset ts" "mset ss" "{(t, s). snd (order s t)}" f f
      "{(t, s). snd (order' s t)}" "{(t, s). fst (order s t)}" "{(t, s). fst (order' s t)}" True]
  by (auto simp: mul_ext_def ns_mul_ext_def converse_unfold)

lemma stri_mul_ext_map:
  assumes "⋀s t. s ∈ set ss ⟹ t ∈ set ts ⟹ fst (order s t) ⟹ fst (order' (f s) (f t))"
    and "⋀s t. s ∈ set ss ⟹ t ∈ set ts ⟹ snd (order s t) ⟹ snd (order' (f s) (f t))"
    and "fst (mul_ext order ss ts)"
  shows "fst (mul_ext order' (map f ss) (map f ts))"
  using assms mult2_alt_map[of "mset ts" "mset ss" "{(t,s). snd (order s t)}" f f
      "{(t, s). snd (order' s t)}" "{(t, s). fst (order s t)}" "{(t, s). fst (order' s t)}" False]
  by (auto simp: mul_ext_def s_mul_ext_def converse_unfold)

text ‹The non-strict order is transitive.›

lemma ns_mul_ext_trans:
  assumes "trans s" "trans ns" "compatible_l ns s" "compatible_r ns s" "refl ns"
    and "(A, B) ∈ ns_mul_ext ns s"
    and "(B, C) ∈ ns_mul_ext ns s"
  shows "(A, C) ∈ ns_mul_ext ns s"
  using assms unfolding compatible_l_def compatible_r_def ns_mul_ext_def
  using trans_mult2_ns[of "s¯" "ns¯"]
  by (auto simp: mult2_ns_eq_mult2_ns_alt converse_relcomp[symmetric]) (metis trans_def)

text‹The strict order is trans.›

lemma s_mul_ext_trans:
  assumes "trans s" "trans ns" "compatible_l ns s" "compatible_r ns s" "refl ns"
    and "(A, B) ∈ s_mul_ext ns s"
    and "(B, C) ∈ s_mul_ext ns s"
  shows "(A, C) ∈ s_mul_ext ns s"
  using assms unfolding compatible_l_def compatible_r_def s_mul_ext_def
  using trans_mult2_s[of "s¯" "ns¯"]
  by (auto simp: mult2_s_eq_mult2_s_alt converse_relcomp[symmetric]) (metis trans_def)

text‹The strict order is compatible on the left with the non strict one›

lemma s_ns_mul_ext_trans:
  assumes "trans s" "trans ns" "compatible_l ns s" "compatible_r ns s" "refl ns"
    and "(A, B) ∈ s_mul_ext ns s"
    and "(B, C) ∈ ns_mul_ext ns s"
  shows "(A, C) ∈ s_mul_ext ns s"
  using assms unfolding compatible_l_def compatible_r_def s_mul_ext_def ns_mul_ext_def
  using compat_mult2(1)[of "s¯" "ns¯"]
  by (auto simp: mult2_s_eq_mult2_s_alt mult2_ns_eq_mult2_ns_alt converse_relcomp[symmetric])


text‹The strict order is compatible on the right with the non-strict one.›

lemma ns_s_mul_ext_trans:
  assumes "trans s" "trans ns" "compatible_l ns s" "compatible_r ns s" "refl ns"
    and "(A, B) ∈ ns_mul_ext ns s"
    and "(B, C) ∈ s_mul_ext ns s"
  shows "(A, C) ∈ s_mul_ext ns s"
  using assms unfolding compatible_l_def compatible_r_def s_mul_ext_def ns_mul_ext_def
  using compat_mult2(2)[of "s¯" "ns¯"]
  by (auto simp: mult2_s_eq_mult2_s_alt mult2_ns_eq_mult2_ns_alt converse_relcomp[symmetric])

text‹@{const s_mul_ext} is strongly normalizing›

lemma SN_s_mul_ext_strong:
  assumes "order_pair s ns"
    and "∀y. y ∈# M ⟶ SN_on s {y}"
  shows "SN_on (s_mul_ext ns s) {M}"
  using mult2_s_eq_mult2_s_alt[of "ns¯" "s¯"] assms wf_below_pointwise[of "s¯" "set_mset M"]
  unfolding SN_on_iff_wf_below s_mul_ext_def order_pair_def compat_pair_def pre_order_pair_def
  by (auto intro!: wf_below_mult2_s_local simp: converse_relcomp[symmetric])

lemma SN_s_mul_ext:
  assumes "order_pair s ns" "SN s"
  shows "SN (s_mul_ext ns s)"
  using SN_s_mul_ext_strong[OF assms(1)] assms(2)
  by (auto simp: SN_on_def)

lemma (in order_pair) mul_ext_order_pair:
  "order_pair (s_mul_ext NS S) (ns_mul_ext NS S)" (is "order_pair ?S ?NS")
proof
  from s_mul_ext_trans trans_S trans_NS compat_NS_S compat_S_NS refl_NS
  show "trans ?S" unfolding trans_def compatible_l_def compatible_r_def by blast
next
  from ns_mul_ext_trans trans_S trans_NS compat_NS_S compat_S_NS refl_NS
  show "trans ?NS" unfolding trans_def compatible_l_def compatible_r_def by blast
next
  from ns_s_mul_ext_trans trans_S trans_NS compat_NS_S compat_S_NS refl_NS
  show "?NS O ?S ⊆ ?S" unfolding trans_def compatible_l_def compatible_r_def by blast
next
  from s_ns_mul_ext_trans trans_S trans_NS compat_NS_S compat_S_NS refl_NS
  show "?S O ?NS ⊆ ?S" unfolding trans_def compatible_l_def compatible_r_def by blast
next
  from ns_mul_ext_refl[OF refl_NS, of _ S]
  show "refl ?NS" unfolding refl_on_def by fast
qed

lemma (in SN_order_pair) mul_ext_SN_order_pair: "SN_order_pair (s_mul_ext NS S) (ns_mul_ext NS S)"
  (is "SN_order_pair ?S ?NS")
proof -
  from mul_ext_order_pair
  interpret order_pair ?S ?NS .
  have "order_pair S NS" by unfold_locales
  then interpret SN_ars ?S using SN_s_mul_ext[of S NS] SN by unfold_locales
  show ?thesis by unfold_locales
qed

lemma mul_ext_compat:
  assumes compat: "⋀ s t u. ⟦s ∈ set ss; t ∈ set ts; u ∈ set us⟧ ⟹
    (snd (f s t) ∧ fst (f t u) ⟶ fst (f s u)) ∧
    (fst (f s t) ∧ snd (f t u) ⟶ fst (f s u)) ∧
    (snd (f s t) ∧ snd (f t u) ⟶ snd (f s u)) ∧
    (fst (f s t) ∧ fst (f t u) ⟶ fst (f s u))"
  shows "
    (snd (mul_ext f ss ts) ∧ fst (mul_ext f ts us) ⟶ fst (mul_ext f ss us)) ∧
    (fst (mul_ext f ss ts) ∧ snd (mul_ext f ts us) ⟶ fst (mul_ext f ss us)) ∧
    (snd (mul_ext f ss ts) ∧ snd (mul_ext f ts us) ⟶ snd (mul_ext f ss us)) ∧
    (fst (mul_ext f ss ts) ∧ fst (mul_ext f ts us) ⟶ fst (mul_ext f ss us)) "
proof -
  let ?s = "{(x, y). fst (f x y)}¯" and ?ns = "{(x, y). snd (f x y)}¯"
  have [dest]: "(mset ts, mset ss) ∈ mult2_alt b2 ?ns ?s ⟹ (mset us, mset ts) ∈ mult2_alt b1 ?ns ?s ⟹
    (mset us, mset ss) ∈ mult2_alt (b1 ∧ b2) ?ns ?s" for b1 b2
    using assms by (auto intro!: trans_mult2_alt_local[of _ "mset ts"] simp: in_multiset_in_set)
  show ?thesis by (auto simp: mul_ext_def s_mul_ext_def ns_mul_ext_def Let_def)
qed

lemma mul_ext_cong[fundef_cong]:
  assumes "mset xs1 = mset ys1"
    and "mset xs2 = mset ys2"
    and "⋀ x x'. x ∈ set ys1 ⟹ x' ∈ set ys2 ⟹ f x x' = g x x'"
  shows "mul_ext f xs1 xs2 = mul_ext g ys1 ys2"
  using assms
    mult2_alt_map[of "mset xs2" "mset xs1" "{(x, y). snd (f x y)}¯" id id "{(x, y). snd (g x y)}¯"
      "{(x, y). fst (f x y)}¯" "{(x, y). fst (g x y)}¯"]
    mult2_alt_map[of "mset ys2" "mset ys1" "{(x, y). snd (g x y)}¯" id id "{(x, y). snd (f x y)}¯"
      "{(x, y). fst (g x y)}¯" "{(x, y). fst (f x y)}¯"]
  by (auto simp: mul_ext_def s_mul_ext_def ns_mul_ext_def Let_def in_multiset_in_set)

lemma all_nstri_imp_mul_nstri:
  assumes "∀i<length ys. snd (f (xs ! i) (ys ! i))"
    and "length xs = length ys"
  shows "snd (mul_ext f xs ys)"
proof-
  from assms(1) have "∀i. i < length ys ⟶ (xs ! i, ys ! i) ∈ {(x,y). snd (f x y)}" by simp
  from all_ns_ns_mul_ext[OF assms(2) this] show ?thesis by (simp add: mul_ext_def)
qed

lemma relation_inter:
  shows "{(x,y). P x y} ∩ {(x,y). Q x y} = {(x,y). P x y ∧ Q x y}"
  by blast

lemma mul_ext_unfold:
  "(x,y) ∈ {(a,b). fst (mul_ext g a b)} ⟷ (mset x, mset y) ∈ (s_mul_ext {(a,b). snd (g a b)} {(a,b). fst (g a b)})"
  unfolding mul_ext_def by (simp add: Let_def)

text ‹The next lemma is a local version of strong-normalization of
  the multiset extension, where the base-order only has to be strongly normalizing
  on elements of the multisets. This will be crucial for orders that are defined recursively
  on terms, such as RPO or WPO.›
lemma mul_ext_SN:
  assumes "∀x. snd (g x x)"
    and "∀x y z. fst (g x y) ⟶ snd (g y z) ⟶ fst (g x z)"
    and "∀x y z. snd (g x y) ⟶ fst (g y z) ⟶ fst (g x z)"
    and "∀x y z. snd (g x y) ⟶ snd (g y z) ⟶ snd (g x z)"
    and "∀x y z. fst (g x y) ⟶ fst (g y z) ⟶ fst (g x z)"
  shows "SN {(ys, xs).
  (∀y∈set ys. SN_on {(s ,t). fst (g s t)} {y}) ∧
  fst (mul_ext g ys xs)}"
proof -
  let ?R1 = "λxs ys. ∀y∈ set ys. SN_on {(s ,t). fst (g s t)} {y}"
  let ?R2 = "λxs ys. fst (mul_ext g ys xs)"
  let ?s = "{(x,y). fst (g x y)}" and ?ns = "{(x,y). snd (g x y)}"
  have OP: "order_pair ?s ?ns" using assms(1-5)
    by unfold_locales ((unfold refl_on_def trans_def)?, blast)+
  let ?R = "{(ys, xs). ?R1 xs ys ∧ ?R2 xs ys}"
  let ?Sn = "SN_on ?R"
  {
    fix ys xs
    assume R_ys_xs: "(ys, xs) ∈ ?R"
    let ?mys = "mset ys"
    let ?mxs = "mset xs"
    from R_ys_xs have  HSN_ys: "∀y. y ∈ set ys ⟶ SN_on ?s {y}" by simp
    with in_multiset_in_set[of ys] have "∀y. y ∈# ?mys ⟶ SN_on ?s {y}" by simp
    from SN_s_mul_ext_strong[OF OP this] and mul_ext_unfold
    have "SN_on {(ys,xs). fst (mul_ext g ys xs)} {ys}" by fast
    from relation_inter[of ?R2 ?R1] and SN_on_weakening[OF this]
    have "SN_on ?R {ys}" by blast
  }
  then have Hyp: "∀ys xs. (ys,xs) ∈ ?R ⟶ SN_on ?R {ys}" by auto
  {
    fix ys
    have "SN_on ?R {ys}"
    proof (cases "∃ xs. (ys, xs) ∈ ?R")
      case True with Hyp show ?thesis by simp
    next
      case False then show ?thesis by auto
    qed
  }
  then show ?thesis unfolding SN_on_def by simp
qed

lemma mul_ext_stri_imp_nstri:
  assumes "fst (mul_ext f as bs)"
  shows "snd (mul_ext f as bs)"
  using assms and s_ns_mul_ext unfolding mul_ext_def by (auto simp: Let_def)

lemma ns_ns_mul_ext_union_compat:
  assumes "(A,B) ∈ ns_mul_ext ns s"
    and "(C,D) ∈ ns_mul_ext ns s"
  shows "(A + C, B + D) ∈ ns_mul_ext ns s"
  using assms by (auto simp: ns_mul_ext_def intro: mult2_alt_ns_ns_add)

lemma s_ns_mul_ext_union_compat:
  assumes "(A,B) ∈ s_mul_ext ns s"
    and "(C,D) ∈ ns_mul_ext ns s"
  shows "(A + C, B + D) ∈ s_mul_ext ns s"
  using assms by (auto simp: s_mul_ext_def ns_mul_ext_def intro: mult2_alt_s_ns_add)

lemma ns_ns_mul_ext_union_compat_rtrancl: assumes refl: "refl ns"
  and AB: "(A, B) ∈ (ns_mul_ext ns s)⇧*"
  and CD: "(C, D) ∈ (ns_mul_ext ns s)⇧*"
shows "(A + C, B + D) ∈ (ns_mul_ext ns s)⇧*"
proof -
  {
    fix A B C
    assume "(A, B) ∈ (ns_mul_ext ns s)⇧*"
    then have "(A + C, B + C) ∈ (ns_mul_ext ns s)⇧*"
    proof (induct rule: rtrancl_induct)
      case (step B D)
      have "(C, C) ∈ ns_mul_ext ns s"
        by (rule ns_mul_ext_refl, insert refl, auto simp: locally_refl_def refl_on_def)
      from ns_ns_mul_ext_union_compat[OF step(2) this] step(3)
      show ?case by auto
    qed auto
  }
  from this[OF AB, of C] this[OF CD, of B]
  show ?thesis by (auto simp: ac_simps)
qed

subsection ‹Multisets as order on lists›

interpretation mul_ext_list: list_order_extension
  "λs ns. {(as, bs). (mset as, mset bs) ∈ s_mul_ext ns s}"
  "λs ns. {(as, bs). (mset as, mset bs) ∈ ns_mul_ext ns s}"
proof -
  let ?m = "mset :: ('a list ⇒ 'a multiset)"
  let ?S = "λs ns. {(as, bs). (?m as, ?m bs) ∈ s_mul_ext ns s}"
  let ?NS = "λs ns. {(as, bs). (?m as, ?m bs) ∈ ns_mul_ext ns s}"
  show "list_order_extension ?S ?NS"
  proof (rule list_order_extension.intro)
    fix s ns
    let ?s = "?S s ns"
    let ?ns = "?NS s ns"
    assume "SN_order_pair s ns"
    then interpret SN_order_pair s ns .
    interpret SN_order_pair "(s_mul_ext ns s)" "(ns_mul_ext ns s)"
      by (rule mul_ext_SN_order_pair)
    show "SN_order_pair ?s ?ns"
    proof
      show "refl ?ns" using refl_NS unfolding refl_on_def by blast
      show "?ns O ?s ⊆ ?s" using compat_NS_S by blast
      show "?s O ?ns ⊆ ?s" using compat_S_NS by blast
      show "trans ?ns" using trans_NS unfolding trans_def by blast
      show "trans ?s" using trans_S unfolding trans_def by blast
      show "SN ?s" using SN_inv_image[OF SN, of ?m, unfolded inv_image_def] .
    qed
  next
    fix S f NS as bs
    assume "⋀a b. (a, b) ∈ S ⟹ (f a, f b) ∈ S"
      "⋀a b. (a, b) ∈ NS ⟹ (f a, f b) ∈ NS"
      "(as, bs) ∈ ?S S NS"
    then show "(map f as, map f bs) ∈ ?S S NS"
      using mult2_alt_map[of _ _ "NS¯" f f "NS¯" "S¯" "S¯"] by (auto simp: mset_map s_mul_ext_def)
  next
    fix S f NS as bs
    assume "⋀a b. (a, b) ∈ S ⟹ (f a, f b) ∈ S"
      "⋀a b. (a, b) ∈ NS ⟹ (f a, f b) ∈ NS"
      "(as, bs) ∈ ?NS S NS"
    then show "(map f as, map f bs) ∈ ?NS S NS"
      using mult2_alt_map[of _ _ "NS¯" f f "NS¯" "S¯" "S¯"] by (auto simp: mset_map ns_mul_ext_def)
  next
    fix as bs :: "'a list" and NS S :: "'a rel"
    assume ass: "length as = length bs"
      "⋀i. i < length bs ⟹ (as ! i, bs ! i) ∈ NS"
    show "(as, bs) ∈ ?NS S NS"
      by (rule, unfold split, rule all_ns_ns_mul_ext, insert ass, auto)
  qed
qed

lemma s_mul_ext_singleton [simp, intro]:
  assumes "(a, b) ∈ s"
  shows "({#a#}, {#b#}) ∈ s_mul_ext ns s"
  using assms by (auto simp: s_mul_ext_def mult2_alt_s_single)

lemma ns_mul_ext_singleton [simp, intro]:
  "(a, b) ∈ ns ⟹ ({#a#}, {#b#}) ∈ ns_mul_ext ns s"
  by (auto simp: ns_mul_ext_def multpw_converse intro: multpw_implies_mult2_alt_ns multpw_single)

lemma ns_mul_ext_singleton2:
  "(a, b) ∈ s ⟹ ({#a#}, {#b#}) ∈ ns_mul_ext ns s"
  by (intro s_ns_mul_ext s_mul_ext_singleton)

lemma s_mul_ext_self_extend_left:
  assumes "A ≠ {#}" and "locally_refl W B"
  shows "(A + B, B) ∈ s_mul_ext W S"
proof -
  have "(A + B, {#} + B) ∈ s_mul_ext W S"
    using assms by (intro s_mul_ext_union_compat) (auto dest: s_mul_ext_bottom)
  then show ?thesis by simp
qed

lemma s_mul_ext_ne_extend_left:
  assumes "A ≠ {#}" and "(B, C) ∈ ns_mul_ext W S"
  shows "(A + B, C) ∈ s_mul_ext W S"
  using assms
proof -
  have "(A + B, {#} + C) ∈ s_mul_ext W S"
    using assms by (intro s_ns_mul_ext_union_compat)
      (auto simp: s_mul_ext_bottom dest: s_ns_mul_ext)
  then show ?thesis by (simp add: ac_simps)
qed

lemma s_mul_ext_extend_left:
  assumes "(B, C) ∈ s_mul_ext W S"
  shows "(A + B, C) ∈ s_mul_ext W S"
  using assms
proof -
  have "(B + A, C + {#}) ∈ s_mul_ext W S"
    using assms by (intro s_ns_mul_ext_union_compat)
      (auto simp: ns_mul_ext_bottom dest: s_ns_mul_ext)
  then show ?thesis by (simp add: ac_simps)
qed

lemma mul_ext_mono:
  assumes "⋀x y. ⟦x ∈ set xs; y ∈ set ys; fst (P x y)⟧ ⟹ fst (P' x y)"
    and   "⋀x y. ⟦x ∈ set xs; y ∈ set ys; snd (P x y)⟧ ⟹ snd (P' x y)"
  shows
    "fst (mul_ext P xs ys) ⟹ fst (mul_ext P' xs ys)"
    "snd (mul_ext P xs ys) ⟹ snd (mul_ext P' xs ys)"
  unfolding mul_ext_def Let_def fst_conv snd_conv
proof -
  assume mem: "(mset xs, mset ys) ∈ s_mul_ext {(x, y). snd (P x y)} {(x, y). fst (P x y)}"
  show "(mset xs, mset ys) ∈ s_mul_ext {(x, y). snd (P' x y)} {(x, y). fst (P' x y)}"
    by (rule s_mul_ext_local_mono[OF _ _ mem], insert assms, auto)
next
  assume mem: "(mset xs, mset ys) ∈ ns_mul_ext {(x, y). snd (P x y)} {(x, y). fst (P x y)}"
  show "(mset xs, mset ys) ∈ ns_mul_ext {(x, y). snd (P' x y)} {(x, y). fst (P' x y)}"
    by (rule ns_mul_ext_local_mono[OF _ _ mem], insert assms, auto)
qed



subsection ‹Special case: non-strict order is equality›

lemma ns_mul_ext_IdE:
  assumes "(M, N) ∈ ns_mul_ext Id R"
  obtains X and Y and Z where "M = X + Z" and "N = Y + Z"
    and "∀y ∈ set_mset Y. ∃x ∈ set_mset X. (x, y) ∈ R"
  using assms
  by (auto simp: ns_mul_ext_def elim!: mult2_alt_nsE) (insert union_commute, blast)

lemma ns_mul_ext_IdI:
  assumes "M = X + Z" and "N = Y + Z" and "∀y ∈ set_mset Y. ∃x ∈ set_mset X. (x, y) ∈ R"
  shows "(M, N) ∈ ns_mul_ext Id R"
  using assms mult2_alt_nsI[of N Z Y M Z X Id "R¯"]
  by (auto simp: ns_mul_ext_def)

lemma s_mul_ext_IdE:
  assumes "(M, N) ∈ s_mul_ext Id R"
  obtains X and Y and Z where "X ≠ {#}" and "M = X + Z" and "N = Y + Z"
    and "∀y ∈ set_mset Y. ∃x ∈ set_mset X. (x, y) ∈ R"
  using assms
  by (auto simp: s_mul_ext_def elim!: mult2_alt_sE) (metis union_commute)

lemma s_mul_ext_IdI:
  assumes "X ≠ {#}" and "M = X + Z" and "N = Y + Z"
    and "∀y ∈ set_mset Y. ∃x ∈ set_mset X. (x, y) ∈ R"
  shows "(M, N) ∈ s_mul_ext Id R"
  using assms mult2_alt_sI[of N Z Y M Z X Id "R¯"]
  by (auto simp: s_mul_ext_def ac_simps)

lemma mult_s_mul_ext_conv:
  assumes "trans R"
  shows "(mult (R¯))¯ = s_mul_ext Id R"
  using mult2_s_eq_mult2_s_alt[of Id "R¯"] assms
  by (auto simp: s_mul_ext_def refl_Id mult2_s_def)

lemma ns_mul_ext_Id_eq:
  "ns_mul_ext Id R = (s_mul_ext Id R)⇧="
  by (auto simp add: ns_mul_ext_def s_mul_ext_def mult2_alt_ns_conv)

lemma subseteq_mset_imp_ns_mul_ext_Id:
  assumes "A ⊆# B"
  shows "(B, A) ∈ ns_mul_ext Id R"
proof -
  obtain C where [simp]: "B = C + A" using assms by (auto simp: mset_subset_eq_exists_conv ac_simps)
  have "(C + A, {#} + A) ∈ ns_mul_ext Id R"
    by (intro ns_mul_ext_IdI [of _ C A _ "{#}"]) auto
  then show ?thesis by simp
qed

lemma subset_mset_imp_s_mul_ext_Id:
  assumes "A ⊂# B"
  shows "(B, A) ∈ s_mul_ext Id R"
  using assms by (intro supset_imp_s_mul_ext) (auto simp: refl_Id)


end