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