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 from add(1) 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 by (metis add.commute diff_intersect_left_idem subset_mset.add_diff_inverse subset_mset.inf_le1) 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 = {#}" by (metis (full_types) M N add_diff_cancel_right add_implies_diff cancel_ab_semigroup_add_class.diff_right_commute diff_add_zero) 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