Theory Multiset_Extension2

(*
Author:  Christian Sternagel <c.sternagel@gmail.com> (2011-2015)
Author:  Guillaume Allais (2011)
Author:  René Thiemann <rene.thiemann@uibk.ac.at> (2011-2015)
License: LGPL (see file COPYING.LESSER)
*)
section‹Multiset extension of the (non-)strict order›

theory Multiset_Extension2
imports
  QTRS.Multiset2
  "Multiset_Extension_Pair"
  QTRS.Relations  
  QTRS.List_Order
  "HOL-Library.Permutation"
begin

section ‹List based characterization of 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) thus ?case by (cases ys) (auto intro: multpw.intros)
next
  case Cons1: (Cons x xs ys' X Y) thus ?case
  proof (cases ys')
    case (Cons y ys)
    hence "∀i. i < length ys ⟶ (xs ! i, ys ! i) ∈ ns" using Cons1(5) by fastforce
    thus ?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
  thus ?case using add(1) by (intro add(4)[of "x # xs" "y # ys"]) (auto, case_tac i, auto)
qed auto

subsection‹Definition of the orders›

text‹We define here A ≥# B: the non-strict extension of the
 order "greater than" on multisets.›

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‹We define here A ># B: the strict extension of the
 order "greater than" 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 subset_mset.order.strict_iff_order)

end


text ‹mapping a function preserves the order›

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)"

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‹s_mul_ext is well-founded›

lemma SN_on_Image_rtrancl_conv:
  "SN_on r A ⟷ SN_on r (r⇧* `` A)" (is "?L ⟷ ?R")
proof
  assume ?L thus ?R by (auto simp: SN_on_Image_rtrancl)
next
  assume ?R thus ?L by (auto simp: SN_on_def)
qed

lemma SN_on_iff_wf_below:
  "SN_on r A ⟷ wf_below (r¯) A"
proof -
  { fix f
    assume "f 0 ∈ r⇧* `` A" and **: "(f i, f (Suc i)) ∈ r" for i
    then have "f i ∈ r⇧* `` A" for i
      by (induct i) (auto simp: Image_def, metis UnCI relcomp.relcompI rtrancl_unfold)
    then have "(f i, f (Suc i)) ∈ Restr r (r⇧* `` A)" for i using ** by auto
  }
  moreover then have "SN_on r (r⇧* `` A) ⟷ SN_on (Restr r (r⇧* `` A)) (r⇧* `` A)"
    unfolding SN_on_def by auto blast
  moreover have "(⋀i. (f i, f (Suc i)) ∈ Restr r (r⇧* `` A)) ⟹ f 0 ∈ r⇧* `` A" for f by auto
  then have "SN_on (Restr r (r⇧* `` A)) (r⇧* `` A) ⟷ SN_on (Restr r (r⇧* `` A)) UNIV"
    unfolding SN_on_def by auto
  ultimately show ?thesis  unfolding SN_on_Image_rtrancl_conv [of _ A]
    by (simp add: wf_below_def SN_iff_wf rtrancl_converse converse_Int converse_Times)
qed

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)

(* FIXME: This lemma is ugly, because it mixes the well-foundedness of the multiset extension
   (SN_s_mul_ext_strong) with the construction of the accessible part of the strict order of g *)
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
  }
  hence 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 thus ?thesis by auto
    qed
  }
  thus ?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)⇧*"
    hence "(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


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