# Theory Multiset_Ordering_More

```section ‹Properties of the Generalized Multiset Ordering›

theory Multiset_Ordering_More
imports
Weighted_Path_Order.Multiset_Extension2
begin

text ‹We provide characterizations of @{const s_mul_ext} and @{const ns_mul_ext} via
introduction and elimination rules that are based on lists.›

lemma s_mul_ext_intro:
assumes "xs = mset xs1 + mset xs2"
and "ys = mset ys1 + mset ys2"
and "length xs1 = length ys1"
and "⋀i. i < length ys1 ⟹ (xs1 ! i, ys1 ! i) ∈ NS"
and "xs2 ≠ []"
and "⋀y. y ∈ set ys2 ⟹ ∃a ∈ set xs2. (a, y) ∈ S"
shows "(xs, ys) ∈ s_mul_ext NS S"
by (rule s_mul_extI[OF assms(1-2) multpw_listI[OF assms(3)]], insert assms(4-), auto)

lemma ns_mul_ext_intro:
assumes "xs = mset xs1 + mset xs2"
and "ys = mset ys1 + mset ys2"
and "length xs1 = length ys1"
and "⋀i. i < length ys1 ⟹ (xs1 ! i, ys1 ! i) ∈ NS"
and "⋀y. y ∈ set ys2 ⟹ ∃x ∈ set xs2. (x, y) ∈ S"
shows "(xs, ys) ∈ ns_mul_ext NS S"
by (rule ns_mul_extI[OF assms(1-2) multpw_listI[OF assms(3)]], insert assms(4-), auto)

lemma ns_mul_ext_elim: assumes "(xs, ys) ∈ ns_mul_ext NS S"
shows "∃ xs1 xs2 ys1 ys2.
xs = mset xs1 + mset xs2
∧ ys = mset ys1 + mset ys2
∧ length xs1 = length ys1
∧ (∀ i. i < length ys1 ⟶ (xs1 ! i, ys1 ! i) ∈ NS)
∧ (∀ y ∈ set ys2. ∃x ∈ set xs2. (x, y) ∈ S)"
proof -
from ns_mul_extE[OF assms] obtain
A1 A2 B1 B2 where *: "xs = A1 + A2" "ys = B1 + B2"
and NS: "(A1, B1) ∈ multpw NS"
and S: "⋀b. b ∈# B2 ⟹ ∃a. a ∈# A2 ∧ (a, b) ∈ S"
by blast
from multpw_listE[OF NS] obtain xs1 ys1 where **: "length xs1 = length ys1" "A1 = mset xs1" "B1 = mset ys1"
and NS: "⋀ i. i < length ys1 ⟹ (xs1 ! i, ys1 ! i) ∈ NS" by auto
from surj_mset obtain xs2 where A2: "A2 = mset xs2" by auto
from surj_mset obtain ys2 where B2: "B2 = mset ys2" by auto
show ?thesis
proof (rule exI[of _ xs1], rule exI[of _ xs2], rule exI[of _ ys1], rule exI[of _ ys2], intro conjI)
show "xs = mset xs1 + mset xs2" using * ** A2 B2 by auto
show "ys = mset ys1 + mset ys2" using * ** A2 B2 by auto
show "length xs1 = length ys1"  by fact
show "∀i<length ys1. (xs1 ! i, ys1 ! i) ∈ NS" using * ** A2 B2 NS by auto
show "∀y∈set ys2. ∃x∈set xs2. (x, y) ∈ S" using * ** A2 B2 S by auto
qed
qed

lemma s_mul_ext_elim: assumes "(xs, ys) ∈ s_mul_ext NS S"
shows "∃ xs1 xs2 ys1 ys2.
xs = mset xs1 + mset xs2
∧ ys = mset ys1 + mset ys2
∧ length xs1 = length ys1
∧ xs2 ≠ []
∧ (∀ i. i < length ys1 ⟶ (xs1 ! i, ys1 ! i) ∈ NS)
∧ (∀ y ∈ set ys2. ∃x ∈ set xs2. (x, y) ∈ S)"
proof -
from s_mul_extE[OF assms] obtain
A1 A2 B1 B2 where *: "xs = A1 + A2" "ys = B1 + B2"
and NS: "(A1, B1) ∈ multpw NS" and nonempty: "A2 ≠ {#}"
and S: "⋀b. b ∈# B2 ⟹ ∃a. a ∈# A2 ∧ (a, b) ∈ S"
by blast
from multpw_listE[OF NS] obtain xs1 ys1 where **: "length xs1 = length ys1" "A1 = mset xs1" "B1 = mset ys1"
and NS: "⋀ i. i < length ys1 ⟹ (xs1 ! i, ys1 ! i) ∈ NS" by auto
from surj_mset obtain xs2 where A2: "A2 = mset xs2" by auto
from surj_mset obtain ys2 where B2: "B2 = mset ys2" by auto
show ?thesis
proof (rule exI[of _ xs1], rule exI[of _ xs2], rule exI[of _ ys1], rule exI[of _ ys2], intro conjI)
show "xs = mset xs1 + mset xs2" using * ** A2 B2 by auto
show "ys = mset ys1 + mset ys2" using * ** A2 B2 by auto
show "length xs1 = length ys1"  by fact
show "∀i<length ys1. (xs1 ! i, ys1 ! i) ∈ NS" using * ** A2 B2 NS by auto
show "∀y∈set ys2. ∃x∈set xs2. (x, y) ∈ S" using * ** A2 B2 S by auto
show "xs2 ≠ []" using nonempty A2 by auto
qed
qed

text ‹We further add a lemma that shows, that it does not matter whether one adds the
strict relation to the non-strict relation or not.›

lemma ns_mul_ext_some_S_in_NS: assumes "S' ⊆ S"
shows "ns_mul_ext (NS ∪ S') S = ns_mul_ext NS S"
proof
show "ns_mul_ext NS S ⊆ ns_mul_ext (NS ∪ S') S"
by (simp add: ns_mul_ext_mono)
show "ns_mul_ext (NS ∪ S') S ⊆ ns_mul_ext NS S"
proof
fix as bs
assume "(as, bs) ∈ ns_mul_ext (NS ∪ S') S"
from ns_mul_extE[OF this] obtain nas sas nbs sbs where
as: "as = nas + sas" and bs: "bs = nbs + sbs"
and ns: "(nas,nbs) ∈ multpw (NS ∪ S')"
and s: "(⋀b. b ∈# sbs ⟹ ∃a. a ∈# sas ∧ (a, b) ∈ S)" by blast
from ns have "∃ nas2 sas2 nbs2 sbs2. nas = nas2 + sas2 ∧ nbs = nbs2 + sbs2 ∧ (nas2,nbs2) ∈ multpw NS
∧ (∀ b ∈# sbs2. (∃a. a ∈# sas2 ∧ (a,b) ∈ S))"
proof (induct)
case (add a b nas nbs)
from add(3) obtain nas2 sas2 nbs2 sbs2 where *: "nas = nas2 + sas2 ∧ nbs = nbs2 + sbs2 ∧ (nas2,nbs2) ∈ multpw NS
∧ (∀ b ∈# sbs2. (∃a. a ∈# sas2 ∧ (a,b) ∈ S))" by blast
show ?case
proof
assume "(a,b) ∈ S'"
with assms have ab: "(a,b) ∈ S" by auto
have one: "add_mset a nas = nas2 + (add_mset a sas2)" using * by auto
have two: "add_mset b nbs = nbs2 + (add_mset b sbs2)" using * by auto
show ?thesis
by (intro exI conjI, rule one, rule two, insert ab *, auto)
next
assume ab: "(a,b) ∈ NS"
have one: "add_mset a nas = (add_mset a nas2) + sas2" using * by auto
have two: "add_mset b nbs = (add_mset b nbs2) + sbs2" using * by auto
show ?thesis
by (intro exI conjI, rule one, rule two, insert ab *, auto intro: multpw.add)
qed
qed auto
then obtain nas2 sas2 nbs2 sbs2 where *: "nas = nas2 + sas2 ∧ nbs = nbs2 + sbs2 ∧ (nas2,nbs2) ∈ multpw NS
∧ (∀ b ∈# sbs2. (∃a. a ∈# sas2 ∧ (a,b) ∈ S))" by auto
have as: "as = nas2 + (sas2 + sas)" and bs: "bs = nbs2 + (sbs2 + sbs)"
unfolding as bs using * by auto
show "(as, bs) ∈ ns_mul_ext NS S"
by (intro ns_mul_extI[OF as bs], insert * s, auto)
qed
qed

lemma ns_mul_ext_NS_union_S:  "ns_mul_ext (NS ∪ S) S = ns_mul_ext NS S"
by (rule ns_mul_ext_some_S_in_NS, auto)

text ‹Some further lemmas on multisets›

lemma mset_map_filter: "mset (map v (filter (λe. c e) t)) + mset (map v (filter (λe. ¬(c e)) t)) = mset (map v t)"
by (induct t, auto)

lemma mset_map_split: assumes "mset (map f xs) = mset ys1 + mset ys2"
shows "∃ zs1 zs2. mset xs = mset zs1 + mset zs2 ∧ ys1 = map f zs1 ∧ ys2 = map f zs2"
using assms
proof (induct xs arbitrary: ys1 ys2)
case (Cons x xs ys1 ys2)
have "f x ∈# mset (map f (x # xs))" by simp
from this[unfolded Cons(2)]
have "f x ∈ set ys1 ∪ set ys2" by auto
thus ?case
proof
let ?ys1 = ys1 let ?ys2 = ys2
assume "f x ∈ set ?ys1"
from split_list[OF this] obtain us1 us2 where ys1: "?ys1 = us1 @ f x # us2" by auto
let ?us = "us1 @ us2"
from Cons(2)[unfolded ys1] have "mset (map f xs) = mset ?us + mset ?ys2" by auto
from Cons(1)[OF this] obtain zs1 zs2 where xs: "mset xs = mset zs1 + mset zs2"
and us: "?us = map f zs1" and ys: "?ys2 = map f zs2"
by auto
let ?zs1 = "take (length us1) zs1" let ?zs2 = "drop (length us1) zs1"
show ?thesis
apply (rule exI[of _ "?zs1 @ x # ?zs2"], rule exI[of _ zs2])
apply (unfold ys1, unfold ys, intro conjI refl)
proof -
have "mset (x # xs) = {# x #} + mset xs" by simp
also have "… = mset (x # zs1) + mset zs2" using xs by simp
also have "zs1 = ?zs1 @ ?zs2" by simp
also have "mset (x # …) = mset (?zs1 @ x # ?zs2)" by (simp add: union_code)
finally show "mset (x # xs) = mset (?zs1 @ x # ?zs2) + mset zs2" .
show "us1 @ f x # us2 = map f (?zs1 @ x # ?zs2)" using us
by (smt (verit, best) ‹zs1 = take (length us1) zs1 @ drop (length us1) zs1› add_diff_cancel_left' append_eq_append_conv length_append length_drop length_map list.simps(9) map_eq_append_conv)
qed
next
let ?ys1 = ys2 let ?ys2 = ys1
assume "f x ∈ set ?ys1"
from split_list[OF this] obtain us1 us2 where ys1: "?ys1 = us1 @ f x # us2" by auto
let ?us = "us1 @ us2"
from Cons(2)[unfolded ys1] have "mset (map f xs) = mset ?us + mset ?ys2" by auto
from Cons(1)[OF this] obtain zs1 zs2 where xs: "mset xs = mset zs1 + mset zs2"
and us: "?us = map f zs1" and ys: "?ys2 = map f zs2"
by auto
let ?zs1 = "take (length us1) zs1" let ?zs2 = "drop (length us1) zs1"
show ?thesis
apply (rule exI[of _ zs2], rule exI[of _ "?zs1 @ x # ?zs2"])
apply (unfold ys1, unfold ys, intro conjI refl)
proof -
have "mset (x # xs) = {# x #} + mset xs" by simp
also have "… = mset zs2 + mset (x # zs1)" using xs by simp
also have "zs1 = ?zs1 @ ?zs2" by simp
also have "mset (x # …) = mset (?zs1 @ x # ?zs2)" by (simp add: union_code)
finally show "mset (x # xs) = mset zs2 + mset (?zs1 @ x # ?zs2)" .
show "us1 @ f x # us2 = map f (?zs1 @ x # ?zs2)" using us
by (smt (verit, best) ‹zs1 = take (length us1) zs1 @ drop (length us1) zs1› add_diff_cancel_left' append_eq_append_conv length_append length_drop length_map list.simps(9) map_eq_append_conv)
qed
qed
qed auto

lemma deciding_mult:
assumes tr: "trans S" and ir: "irrefl S"
shows "(N,M) ∈ mult S = (M ≠ N ∧ (∀ b ∈# N - M. ∃ a ∈# M - N. (b,a) ∈ S))"
proof -
define I where "I = M ∩# N"
have N: "N = (N - M) + I" unfolding I_def
by (metis add.commute diff_intersect_left_idem multiset_inter_commute subset_mset.add_diff_inverse subset_mset.inf_le1)
have M: "M = (M - N) + I" unfolding I_def
have "(N,M) ∈ mult S ⟷
((N - M) + I, (M - N) + I) ∈ mult S"
using N M by auto
also have "… ⟷ (N - M, M - N) ∈ mult S"
by (rule mult_cancel[OF tr irrefl_on_subset[OF ir, simplified]])
also have "… ⟷ (M ≠ N ∧ (∀ b ∈# N - M. ∃ a ∈# M - N. (b,a) ∈ S))"
proof
assume *: "(M ≠ N ∧ (∀ b ∈# N - M. ∃ a ∈# M - N. (b,a) ∈ S))"
have "({#} + (N - M), {#} + (M - N)) ∈ mult S"
apply (rule one_step_implies_mult, insert *, auto)
using M N by auto
thus "(N - M, M - N) ∈ mult S" by auto
next
assume "(N - M, M - N) ∈ mult S"
from mult_implies_one_step[OF tr this]
obtain E J K
where *: " M - N = E + J ∧
N - M = E + K"  and rel: "J ≠ {#} ∧ (∀k∈#K. ∃j∈#J. (k, j) ∈ S) " by auto
from * have "E = {#}"
with * have JK: "J = M - N" "K = N - M" by auto
show "(M ≠ N ∧ (∀ b ∈# N - M. ∃ a ∈# M - N. (b,a) ∈ S))"
using rel unfolding JK by auto
qed
finally show ?thesis .
qed

lemma s_mul_ext_map: "(⋀a b. a ∈ set as ⟹ b ∈ set bs ⟹ (a, b) ∈ S ⟹ (f a, f b) ∈ S') ⟹
(⋀a b. a ∈ set as ⟹ b ∈ set bs ⟹ (a, b) ∈ NS ⟹ (f a, f b) ∈ NS') ⟹
(as, bs) ∈ {(as, bs). (mset as, mset bs) ∈ s_mul_ext NS S} ⟹
(map f as, map f bs) ∈ {(as, bs). (mset as, mset bs) ∈ s_mul_ext NS' S'}"
using mult2_alt_map[of _ _ "NS¯" f f "(NS')¯" "S¯" "S'¯" False] unfolding s_mul_ext_def
by fastforce

lemma fst_mul_ext_imp_fst: assumes "fst (mul_ext f xs ys)"
and "length xs ≤ length ys"
shows "∃ x y. x ∈ set xs ∧ y ∈ set ys ∧ fst (f x y)"
proof -
from assms(1)[unfolded mul_ext_def Let_def fst_conv]
have "(mset xs, mset ys) ∈ s_mul_ext {(x, y). snd (f x y)} {(x, y). fst (f x y)}" by auto
from s_mul_ext_elim[OF this] obtain xs1 xs2 ys1 ys2
where *: "mset xs = mset xs1 + mset xs2"
"mset ys = mset ys1 + mset ys2"
"length xs1 = length ys1"
"xs2 ≠ []"
"(∀y∈set ys2. ∃x∈set xs2. (x, y) ∈ {(x, y). fst (f x y)})" by auto
from *(1-3) assms(2) have "length xs2 ≤ length ys2"
by (metis add_le_cancel_left size_mset size_union)
with *(4) have "hd ys2 ∈ set ys2" by (cases ys2, auto)
with *(5,1,2) show ?thesis
by (metis Un_iff mem_Collect_eq prod.simps(2) set_mset_mset set_mset_union)
qed

lemma ns_mul_ext_point: assumes "(as,bs) ∈ ns_mul_ext NS S"
and "b ∈# bs"
shows "∃ a ∈# as. (a,b) ∈ NS ∪ S"
proof -
from ns_mul_ext_elim[OF assms(1)]
obtain xs1 xs2 ys1 ys2
where *: "as = mset xs1 + mset xs2"
"bs = mset ys1 + mset ys2"
"length xs1 = length ys1"
"(∀i<length ys1. (xs1 ! i, ys1 ! i) ∈ NS)" "(∀y∈set ys2. ∃x∈set xs2. (x, y) ∈ S)" by auto
from assms(2)[unfolded *] have "b ∈ set ys1 ∨ b ∈ set ys2" by auto
thus ?thesis
proof
assume "b ∈ set ys2"
with * obtain a where "a ∈ set xs2" and "(a,b) ∈ S" by auto
with *(1) show ?thesis by auto
next
assume "b ∈ set ys1"
from this[unfolded set_conv_nth] obtain i where i: "i < length ys1" and "b = ys1 ! i" by auto
with *(4) have "(xs1 ! i, b) ∈ NS" by auto
moreover from i *(3) have "xs1 ! i ∈ set xs1" by auto
ultimately show ?thesis using *(1) by auto
qed
qed

lemma s_mul_ext_point: assumes "(as,bs) ∈ s_mul_ext NS S"
and "b ∈# bs"
shows "∃ a ∈# as. (a,b) ∈ NS ∪ S"
by (rule ns_mul_ext_point, insert assms s_ns_mul_ext, auto)

end
```