Theory Weighted_Path_Order.Multiset_Extension_Pair

section ‹Multiset extension of an order pair›

text ‹Given a well-founded order $\prec$ and a compatible non-strict order $\precsim$,
  we define the corresponding multiset-extension of these orders.›

theory Multiset_Extension_Pair
  imports 
    "HOL-Library.Multiset" 
    "Regular-Sets.Regexp_Method"
    "Abstract-Rewriting.Abstract_Rewriting" 
    Relations
begin

(* Possible to generalize by assuming trans locally *)

lemma mult_locally_cancel:
  assumes "trans s " and "locally_irrefl s (X + Z)" and "locally_irrefl s (Y + Z)"
  shows "(X + Z, Y + Z) ∈ mult s ⟷ (X, Y) ∈ mult s" (is "?L ⟷ ?R")
proof
  assume ?L thus ?R using assms(2, 3)
  proof (induct Z arbitrary: X Y)
    case (add z Z)
    obtain X' Y' Z' where *: "add_mset z X + Z = Z' + X'" "add_mset z Y + Z = Z' + Y'" "Y' ≠ {#}"
      "∀x ∈ set_mset X'. ∃y ∈ set_mset Y'. (x, y) ∈ s"
      using mult_implies_one_step[OF ‹trans s› add(2)] by auto
    consider Z2 where "Z' = add_mset z Z2" | X2 Y2 where "X' = add_mset z X2" "Y' = add_mset z Y2"
      using *(1,2) by (metis add_mset_remove_trivial_If insert_iff set_mset_add_mset_insert union_iff)
    thus ?case
    proof (cases)
      case 1 thus ?thesis using * one_step_implies_mult[of Y' X' s Z2] 
        by (auto simp: add.commute[of _ "{#_#}"] add.assoc intro: add(1))
          (metis add.hyps add.prems(2) add.prems(3) add_mset_add_single li_trans_l union_mset_add_mset_right) 
    next
      case 2 then obtain y where "y ∈ set_mset Y2" "(z, y) ∈ s" using *(4) add(3, 4)
        by (auto simp: locally_irrefl_def)
      moreover from this transD[OF ‹trans s› _ this(2)]
      have "x' ∈ set_mset X2 ⟹ ∃y ∈ set_mset Y2. (x', y) ∈ s" for x'
        using 2 *(4)[rule_format, of x'] by auto
      ultimately show ?thesis using  * one_step_implies_mult[of Y2 X2 s Z'] 2 add(3, 4)
        by (force simp: locally_irrefl_def add.commute[of "{#_#}"] add.assoc[symmetric] intro: add(1))
    qed
  qed auto
next
  assume ?R then obtain I J K
    where "Y = I + J" "X = I + K" "J ≠ {#}" "∀k ∈ set_mset K. ∃j ∈ set_mset J. (k, j) ∈ s"
    using mult_implies_one_step[OF ‹trans s›] by blast
  thus ?L using one_step_implies_mult[of J K s "I + Z"] by (auto simp: ac_simps)
qed

lemma mult_locally_cancelL:
  assumes "trans s" "locally_irrefl s (X + Z)" "locally_irrefl s (Y + Z)"
  shows "(Z + X, Z + Y) ∈ mult s ⟷ (X, Y) ∈ mult s"
  using mult_locally_cancel[OF assms] by (simp only: union_commute)

lemma mult_cancelL:
  assumes "trans s" "irrefl s" shows "(Z + X, Z + Y) ∈ mult s ⟷ (X, Y) ∈ mult s"
  using assms
  by (auto simp: union_commute intro!: mult_cancel elim: irrefl_on_subset) 

lemma wf_trancl_conv:
  shows "wf (r⇧+) ⟷ wf r"
  using wf_subset[of "r⇧+" r] by (force simp: wf_trancl)

subsection ‹Pointwise multiset order›

inductive_set multpw :: "'a rel ⇒ 'a multiset rel" for ns :: "'a rel" where
  empty: "({#}, {#}) ∈ multpw ns"
| add: "(x, y) ∈ ns ⟹ (X, Y) ∈ multpw ns ⟹ (add_mset x X, add_mset y Y) ∈ multpw ns"

lemma multpw_emptyL [simp]:
  "({#}, X) ∈ multpw ns ⟷ X = {#}"
  by (cases X) (auto elim: multpw.cases intro: multpw.intros)

lemma multpw_emptyR [simp]:
  "(X, {#}) ∈ multpw ns ⟷ X = {#}"
  by (cases X) (auto elim: multpw.cases intro: multpw.intros)

lemma refl_multpw:
  assumes "refl ns" shows "refl (multpw ns)"
proof -
  have "(X, X) ∈ multpw ns" for X using assms
    by (induct X) (auto intro: multpw.intros simp: refl_on_def)
  then show ?thesis by (auto simp: refl_on_def)
qed

lemma multpw_Id_Id [simp]:
  "multpw Id = Id"
proof -
  have "(X, Y) ∈ multpw (Id :: 'a rel) ⟹ X = Y" for X Y by (induct X Y rule: multpw.induct) auto
  then show ?thesis using refl_multpw[of Id] by (auto simp: refl_on_def)
qed

lemma mono_multpw:
  assumes "ns ⊆ ns'" shows "multpw ns ⊆ multpw ns'"
proof -
  have "(X, Y) ∈ multpw ns ⟹ (X, Y) ∈ multpw ns'" for X Y
    by (induct X Y rule: multpw.induct) (insert assms, auto intro: multpw.intros)
  then show ?thesis by auto
qed

lemma multpw_converse:
  "multpw (ns¯) = (multpw ns)¯"
proof -
  have "(X, Y) ∈ multpw (ns¯) ⟹ (X, Y) ∈ (multpw ns)¯" for X Y and ns :: "'a rel"
    by (induct X Y rule: multpw.induct) (auto intro: multpw.intros)
  then show ?thesis by auto
qed

lemma multpw_local:
  "(X, Y) ∈ multpw ns ⟹ (X, Y) ∈ multpw (ns ∩ set_mset X × set_mset Y)"
proof (induct X Y rule: multpw.induct)
  case (add x y X Y) then show ?case
    using mono_multpw[of "ns ∩ set_mset X × set_mset Y" "ns ∩ insert x (set_mset X) × insert y (set_mset Y)"]
    by (auto intro: multpw.intros)
qed auto

lemma multpw_split1R:
  assumes "(add_mset x X, Y) ∈ multpw ns"
  obtains z Z where "Y = add_mset z Z" and "(x, z) ∈ ns" and "(X, Z) ∈ multpw ns"
  using assms
proof (induct  "add_mset x X" Y arbitrary: X thesis rule: multpw.induct)
  case (add x' y' X' Y') then show ?case
  proof (cases "x = x'")
    case False
    obtain X'' where [simp]: "X = add_mset x' X''"
      using add(4) False
      by (metis add_eq_conv_diff)
    have "X' = add_mset x X''" using add(4) by (auto simp: add_eq_conv_ex)
    with add(2) obtain Y'' y where "Y' = add_mset y Y''" "(x,y) ∈ ns" "(X'', Y'') ∈ multpw ns"
      by (auto intro: add(3))
    then show ?thesis using add(1) add(5)[of y "add_mset y' Y''"]
      by (auto simp: ac_simps intro: multpw.intros)
  qed auto
qed auto

lemma multpw_splitR:
  assumes "(X1 + X2, Y) ∈ multpw ns"
  obtains Y1 Y2 where "Y = Y1 + Y2" and "(X1, Y1) ∈ multpw ns" and "(X2, Y2) ∈ multpw ns"
  using assms
proof (induct X2 arbitrary: Y thesis)
  case (add x2 X2)
  from add(3) obtain Y' y2 where "(X1 + X2, Y') ∈ multpw ns" "(x2, y2) ∈ ns" "Y = add_mset y2 Y'"
    by (auto elim: multpw_split1R simp: union_assoc[symmetric])
  moreover then obtain Y1 Y2 where "(X1, Y1) ∈ multpw ns" "(X2, Y2) ∈ multpw ns" "Y' = Y1 + Y2"
    by (auto elim: add(1)[rotated])
  ultimately show ?case by (intro add(2)) (auto simp: union_assoc intro: multpw.intros)
qed auto

lemma multpw_split1L:
  assumes "(X, add_mset y Y) ∈ multpw ns"
  obtains z Z where "X = add_mset z Z" and "(z, y) ∈ ns" and "(Z, Y) ∈ multpw ns"
  using assms multpw_split1R[of y Y X "ns¯" thesis] by (auto simp: multpw_converse)

lemma multpw_splitL:
  assumes "(X, Y1 + Y2) ∈ multpw ns"
  obtains X1 X2 where "X = X1 + X2" and "(X1, Y1) ∈ multpw ns" and "(X2, Y2) ∈ multpw ns"
  using assms multpw_splitR[of Y1 Y2 X "ns¯" thesis] by (auto simp: multpw_converse)

lemma locally_trans_multpw:
  assumes "locally_trans ns S T U"
    and "(S, T) ∈ multpw ns"
    and "(T, U) ∈ multpw ns"
  shows "(S, U) ∈ multpw ns"
  using assms(2,3,1)
proof (induct S T arbitrary: U rule: multpw.induct)
  case (add x y X Y)
  then show ?case unfolding locally_trans_def
    by (auto 0 3 intro: multpw.intros elim: multpw_split1R)
qed blast

lemma trans_multpw:
  assumes "trans ns" shows "trans (multpw ns)"
  using locally_trans_multpw unfolding locally_trans_def trans_def
  by (meson assms locally_trans_multpw tr_ltr)

lemma multpw_add:
  assumes "(X1, Y1) ∈ multpw ns" "(X2, Y2) ∈ multpw ns" shows "(X1 + X2, Y1 + Y2) ∈ multpw ns"
  using assms(2,1)
  by (induct X2 Y2 rule: multpw.induct) (auto intro: multpw.intros simp: add.assoc[symmetric])

lemma multpw_single:
  "(x, y) ∈ ns ⟹ ({#x#}, {#y#}) ∈ multpw ns"
  using multpw.intros(2)[OF _ multpw.intros(1)] .

lemma multpw_mult1_commute:
  assumes compat: "s O ns ⊆ s" and reflns: "refl ns"
  shows "mult1 s O multpw ns ⊆ multpw ns O mult1 s"
proof -
  { fix X Y Z assume 1: "(X, Y) ∈ mult1 s" "(Y, Z) ∈ multpw ns"
    then obtain X' Y' y where 2: "X = Y' + X'" "Y = add_mset y Y'" "∀x. x ∈# X' ⟶ (x, y) ∈ s"
      by (auto simp: mult1_def)
    moreover obtain Z' z where 3: "Z = add_mset z Z'" "(y, z) ∈ ns" "(Y', Z') ∈ multpw ns"
      using 1(2) 2(2) by (auto elim: multpw_split1R)
    moreover have "∀x. x ∈# X' ⟶ (x, z) ∈ s" using 2(3) 3(2) compat by blast
    ultimately have "∃Y'. (X, Y') ∈ multpw ns ∧ (Y', Z) ∈ mult1 s" unfolding mult1_def
      using refl_multpw[OF reflns]
      by (intro exI[of _ "Z' + X'"]) (auto intro: multpw_add simp: refl_on_def)
  }
  then show ?thesis by fast
qed

lemma multpw_mult_commute:
  assumes "s O ns ⊆ s" "refl ns" shows "mult s O multpw ns ⊆ multpw ns O mult s"
proof -
  { fix X Y Z assume 1: "(X, Y) ∈ mult s" "(Y, Z) ∈ multpw ns"
    then have "∃Y'. (X, Y') ∈ multpw ns ∧ (Y', Z) ∈ mult s" unfolding mult_def
      using multpw_mult1_commute[OF assms] by (induct rule: converse_trancl_induct) (auto 0 3)
  }
  then show ?thesis by fast
qed

lemma wf_mult_rel_multpw:
  assumes "wf s" "s O ns ⊆ s" "refl ns" shows "wf ((multpw ns)⇧* O mult s O (multpw ns)⇧*)"
  using assms(1) multpw_mult_commute[OF assms(2,3)] by (subst qc_wf_relto_iff) (auto simp: wf_mult)

lemma multpw_cancel1:
  assumes "trans ns" "(y, x) ∈ ns"
  shows "(add_mset x X, add_mset y Y) ∈ multpw ns ⟹ (X, Y) ∈ multpw ns" (is "?L ⟹ ?R")
proof -
  assume ?L then obtain x' X' where X: "(x', y) ∈ ns" "add_mset x' X' = add_mset x X" "(X', Y) ∈ multpw ns"
    by (auto elim: multpw_split1L simp: union_assoc[symmetric])
  then show ?R
  proof (cases "x = x'")
    case False then obtain X2 where X2: "X' = add_mset x X2" "X = add_mset x' X2"
      using X(2) by (auto simp: add_eq_conv_ex)
    then obtain y' Y' where Y: "(x, y') ∈ ns" "Y = add_mset y' Y'" "(X2, Y') ∈ multpw ns"
      using X(3) by (auto elim: multpw_split1R)
    have "(x', y') ∈ ns" using X(1) Y(1) ‹trans ns› assms(2) by (metis trans_def)
    then show ?thesis using Y by (auto intro: multpw.intros simp: X2)
  qed auto
qed

lemma multpw_cancel:
  assumes "refl ns" "trans ns"
  shows "(X + Z, Y + Z) ∈ multpw ns ⟷ (X, Y) ∈ multpw ns" (is "?L ⟷ ?R")
proof
  assume ?L then show ?R
  proof (induct Z)
    case (add z Z) then show ?case using multpw_cancel1[of ns z z "X + Z" "Y + Z"] assms
      by (auto simp: refl_on_def union_assoc)
  qed auto
next
  assume ?R then show ?L using assms refl_multpw by (auto intro: multpw_add simp: refl_on_def)
qed

lemma multpw_cancelL:
  assumes "refl ns" "trans ns" shows "(Z + X, Z + Y) ∈ multpw ns ⟷ (X, Y) ∈ multpw ns"
  using multpw_cancel[OF assms, of X Z Y] by (simp only: union_commute)

subsection ‹Multiset extension for order pairs via the pointwise order and @{const mult}›

definition "mult2_s ns s ≡ multpw ns O mult s"
definition "mult2_ns ns s ≡ multpw ns O (mult s)⇧="

lemma mult2_ns_conv:
  shows "mult2_ns ns s = mult2_s ns s ∪ multpw ns"
  by (auto simp: mult2_s_def mult2_ns_def)

lemma mono_mult2_s:
  assumes "ns ⊆ ns'" "s ⊆ s'" shows "mult2_s ns s ⊆ mult2_s ns' s'"
  using mono_multpw[OF assms(1)] mono_mult[OF assms(2)] unfolding mult2_s_def by auto

lemma mono_mult2_ns:
  assumes "ns ⊆ ns'" "s ⊆ s'" shows "mult2_ns ns s ⊆ mult2_ns ns' s'"
  using mono_multpw[OF assms(1)] mono_mult[OF assms(2)] unfolding mult2_ns_def by auto

lemma wf_mult2_s:
  assumes "wf s" "s O ns ⊆ s" "refl ns"
  shows "wf (mult2_s ns s)"
  using wf_mult_rel_multpw[OF assms] assms by (auto simp: mult2_s_def wf_mult intro: wf_subset)

lemma refl_mult2_ns:
  assumes "refl ns" shows "refl (mult2_ns ns s)"
  using refl_multpw[OF assms] unfolding mult2_ns_def refl_on_def by fast

lemma trans_mult2_s:
  assumes "s O ns ⊆ s" "refl ns" "trans ns"
  shows "trans (mult2_s ns s)"
  using trans_multpw[OF assms(3)] trans_trancl[of "mult1 s", folded mult_def] multpw_mult_commute[OF assms(1,2)]
  unfolding mult2_s_def trans_O_iff by (blast 8)

lemma trans_mult2_ns:
  assumes "s O ns ⊆ s" "refl ns" "trans ns"
  shows "trans (mult2_ns ns s)"
  using trans_multpw[OF assms(3)] trans_trancl[of "mult1 s", folded mult_def] multpw_mult_commute[OF assms(1,2)]
  unfolding mult2_ns_def trans_O_iff by (blast 8)

lemma compat_mult2:
  assumes "s O ns ⊆ s" "refl ns" "trans ns"
  shows "mult2_ns ns s O mult2_s ns s ⊆ mult2_s ns s" "mult2_s ns s O mult2_ns ns s ⊆ mult2_s ns s"
  using trans_multpw[OF assms(3)] trans_trancl[of "mult1 s", folded mult_def] multpw_mult_commute[OF assms(1,2)]
  unfolding mult2_s_def mult2_ns_def trans_O_iff by (blast 8)+

text ‹Trivial inclusions›

lemma mult_implies_mult2_s:
  assumes "refl ns" "(X, Y) ∈ mult s"
  shows "(X, Y) ∈ mult2_s ns s"
  using refl_multpw[of ns] assms unfolding mult2_s_def refl_on_def by blast

lemma mult_implies_mult2_ns:
  assumes "refl ns" "(X, Y) ∈ (mult s)⇧="
  shows "(X, Y) ∈ mult2_ns ns s"
  using refl_multpw[of ns] assms unfolding mult2_ns_def refl_on_def by blast

lemma multpw_implies_mult2_ns:
  assumes "(X, Y) ∈ multpw ns"
  shows "(X, Y) ∈ mult2_ns ns s"
  unfolding mult2_ns_def using assms by simp

subsection ‹One-step versions of the multiset extensions›

lemma mult2_s_one_step:
  assumes "ns O s ⊆ s" "refl ns" "trans s"
  shows "(X, Y) ∈ mult2_s ns s ⟷ (∃X1 X2 Y1 Y2. X = X1 + X2 ∧ Y = Y1 + Y2 ∧
    (X1, Y1) ∈ multpw ns ∧ Y2 ≠ {#} ∧ (∀x. x ∈# X2 ⟶ (∃y. y ∈# Y2 ∧ (x, y) ∈ s)))" (is "?L ⟷ ?R")
proof
  assume ?R then obtain X1 X2 Y1 Y2 where *: "X = X1 + X2" "Y = Y1 + Y2" "(X1, Y1) ∈ multpw ns" and
    "Y2 ≠ {#}" "∀x. x ∈# X2 ⟶ (∃y. y ∈# Y2 ∧ (x, y) ∈ s)" by blast
  then have "(Y1 + X2, Y1 + Y2) ∈ mult s"
    using ‹trans s› by (auto intro: one_step_implies_mult)
  moreover have "(X1 + X2, Y1 + X2) ∈ multpw ns"
    using ‹refl ns› refl_multpw[of ns] by (auto intro: multpw_add simp: refl_on_def *)
  ultimately show ?L by (auto simp: mult2_s_def *)
next
  assume ?L then obtain X1 X2 Z1 Z2 Y2 where *: "X = X1 + X2" "Y = Z1 + Y2" "(X1, Z1) ∈ multpw ns"
    "(X2, Z2) ∈ multpw ns" "Y2 ≠ {#}" "∀x. x ∈# Z2 ⟶ (∃y. y ∈# Y2 ∧ (x, y) ∈ s)"
    by (auto 0 3 dest!: mult_implies_one_step[OF ‹trans s›] simp: mult2_s_def elim!: multpw_splitL) metis
  have "∀x. x ∈# X2 ⟶ (∃y. y ∈# Y2 ∧ (x,y) ∈ s)"
  proof (intro allI impI)
    fix x assume "x ∈# X2"
    then obtain X2' where "X2 = add_mset x X2'" by (metis multi_member_split)
    then obtain z Z2' where "Z2 = add_mset z Z2'" "(x, z) ∈ ns" using *(4) by (auto elim: multpw_split1R)
    then have "z ∈# Z2" "(x, z) ∈ ns" by auto
    then show "∃y. y ∈# Y2 ∧ (x,y) ∈ s" using *(6) ‹ns O s ⊆ s› by blast
  qed
  then show ?R using * by auto
qed

lemma mult2_ns_one_step:
  assumes "ns O s ⊆ s" "refl ns" "trans s"
  shows "(X, Y) ∈ mult2_ns ns s ⟷ (∃X1 X2 Y1 Y2. X = X1 + X2 ∧ Y = Y1 + Y2 ∧
    (X1, Y1) ∈ multpw ns ∧ (∀x. x ∈# X2 ⟶ (∃y. y ∈# Y2 ∧ (x, y) ∈ s)))" (is "?L ⟷ ?R")
proof
  assume ?L then consider "(X, Y) ∈ multpw ns" | "(X, Y) ∈ mult2_s ns s"
    by (auto simp: mult2_s_def mult2_ns_def)
  then show ?R using mult2_s_one_step[OF assms]
    by (cases, intro exI[of _ "{#}", THEN exI[of _ Y, THEN exI[of _ "{#}", THEN exI[of _ X]]]]) auto
next
  assume ?R then obtain X1 X2 Y1 Y2 where "X = X1 + X2" "Y = Y1 + Y2"
    "(X1, Y1) ∈ multpw ns" "∀x. x ∈# X2 ⟶ (∃y. y ∈# Y2 ∧ (x, y) ∈ s)" by blast
  then show ?L using mult2_s_one_step[OF assms, of X Y] count_inject[of X2 "{#}"]
    by (cases "Y2 = {#}") (auto simp: mult2_s_def mult2_ns_def)
qed

lemma mult2_s_locally_one_step':
  assumes "ns O s ⊆ s" "refl ns" "locally_irrefl s X" "locally_irrefl s Y" "trans s"
  shows "(X, Y) ∈ mult2_s ns s ⟷ (∃X1 X2 Y1 Y2. X = X1 + X2 ∧ Y = Y1 + Y2 ∧
    (X1, Y1) ∈ multpw ns ∧ (X2, Y2) ∈ mult s)" (is "?L ⟷ ?R")
proof
  assume ?L then show ?R unfolding mult2_s_one_step[OF assms(1,2,5)]
    using one_step_implies_mult[of _ _ s "{#}"] by auto metis
next
  assume ?R then obtain X1 X2 Y1 Y2 where x: "X = X1 + X2" and y: "Y = Y1 + Y2" and
    ns: "(X1, Y1) ∈ multpw ns" and s: "(X2, Y2) ∈ mult s" by blast
  then have l: "locally_irrefl s (X2 + Y1)" and r: "locally_irrefl s (Y2 + Y1)"
    using assms(3, 4) by (auto simp add: locally_irrefl_def)
  show ?L using ns s mult_locally_cancelL[OF assms(5) l r] multpw_add[OF ns, of X2 X2] refl_multpw[OF ‹refl ns›]
    unfolding mult2_s_def refl_on_def x y by auto
qed

lemma mult2_s_one_step':
  assumes "ns O s ⊆ s" "refl ns" "irrefl s" "trans s"
  shows "(X, Y) ∈ mult2_s ns s ⟷ (∃X1 X2 Y1 Y2. X = X1 + X2 ∧ Y = Y1 + Y2 ∧
    (X1, Y1) ∈ multpw ns ∧ (X2, Y2) ∈ mult s)" (is "?L ⟷ ?R")
  using assms mult2_s_locally_one_step' by (simp add: mult2_s_locally_one_step' irrefl_def locally_irrefl_def) 

lemma mult2_ns_one_step':
  assumes "ns O s ⊆ s" "refl ns" "irrefl s" "trans s"
  shows "(X, Y) ∈ mult2_ns ns s ⟷ (∃X1 X2 Y1 Y2. X = X1 + X2 ∧ Y = Y1 + Y2 ∧
    (X1, Y1) ∈ multpw ns ∧ (X2, Y2) ∈ (mult s)⇧=)" (is "?L ⟷ ?R")
proof -
  have "(X, Y) ∈ multpw ns ⟹ ?R"
    by (intro exI[of _ "{#}", THEN exI[of _ Y, THEN exI[of _ "{#}", THEN exI[of _ X]]]]) auto
  moreover have "X = X1 + Y2 ∧ Y = Y1 + Y2 ∧ (X1, Y1) ∈ multpw ns ⟹ ?L" for X1 Y1 Y2
    using multpw_add[of X1 Y1 ns Y2 Y2] refl_multpw[OF ‹refl ns›] by (auto simp: mult2_ns_def refl_on_def)
  ultimately show ?thesis using mult2_s_one_step'[OF assms] unfolding mult2_ns_conv
    by auto blast
qed

subsection ‹Cancellation›

lemma mult2_s_locally_cancel1:
  assumes "s O ns ⊆ s" "ns O s ⊆ s" "refl ns" "trans ns" "locally_irrefl s (add_mset z X)" "locally_irrefl s (add_mset z Y)" "trans s"
    "(add_mset z X, add_mset z Y) ∈ mult2_s ns s"
  shows "(X, Y) ∈ mult2_s ns s"
proof -
  obtain X1 X2 Y1 Y2 where *: "add_mset z X = X1 + X2" "add_mset z Y = Y1 + Y2" "(X1, Y1) ∈ multpw ns"
    "(X2, Y2) ∈ mult s" using assms(8) unfolding mult2_s_locally_one_step'[OF assms(2,3,5,6,7)] by blast    
  from union_single_eq_member[OF this(1)] union_single_eq_member[OF this(2)] multi_member_split
  consider X1' where "X1 = add_mset z X1'" | Y1' where "Y1 = add_mset z Y1'"
    | X2' Y2' where "X2 = add_mset z X2'" "Y2 = add_mset z Y2'"
    unfolding set_mset_union Un_iff by metis
  then show ?thesis
  proof (cases)
    case 1 then obtain Y1' z' where **: "(X1', Y1') ∈ multpw ns" "Y1 = add_mset z' Y1'" "(z, z') ∈ ns"
      using * by (auto elim: multpw_split1R)
    then have "(X, Y1' + Y2) ∈ mult2_s ns s" using * 1
      by auto (metis add_mset_add_single assms(2 - 7) li_trans_l mult2_s_locally_one_step') 
    moreover
    have "(Y1' + Y2, Y) ∈ multpw ns"
      using refl_multpw[OF ‹refl ns›] * ** multpw_cancel1[OF ‹trans ns› **(3), of "Y1' + Y2" Y]
      by (auto simp: refl_on_def)
    ultimately show ?thesis using compat_mult2[OF assms(1,3,4)] unfolding mult2_ns_conv by blast
  next
    case 2 then obtain X1' z' where **: "(X1', Y1') ∈ multpw ns" "X1 = add_mset z' X1'" "(z', z) ∈ ns"
      using * by (auto elim: multpw_split1L)
    then have "(X1' + X2, Y) ∈ mult2_s ns s" using * 2
      by auto (metis add_mset_add_single assms(2 - 7) li_trans_l mult2_s_locally_one_step')
    moreover
    have "(X, X1' + X2) ∈ multpw ns"
      using refl_multpw[OF ‹refl ns›] * ** multpw_cancel1[OF ‹trans ns› **(3), of X "X1' + X2"]
      by (auto simp: refl_on_def)
    ultimately show ?thesis using compat_mult2[OF assms(1,3,4)] unfolding mult2_ns_conv by blast
  next
    case 3 then show ?thesis using assms *
      by (auto simp: mult2_s_locally_one_step' union_commute[of "{#_#}"] union_assoc[symmetric] mult_cancel mult_cancel_add_mset)
        (metis "*"(1) "*"(2) add_mset_add_single li_trans_l li_trans_r mult2_s_locally_one_step' mult_locally_cancel)
  qed
qed

lemma mult2_s_cancel1:
  assumes "s O ns ⊆ s" "ns O s ⊆ s" "refl ns" "trans ns" "irrefl s" "trans s" "(add_mset z X, add_mset z Y) ∈ mult2_s ns s"
  shows "(X, Y) ∈ mult2_s ns s"
  using assms mult2_s_locally_cancel1 by (metis irrefl_def locally_irrefl_def) 

lemma mult2_s_locally_cancel:
  assumes "s O ns ⊆ s" "ns O s ⊆ s" "refl ns" "trans ns" "locally_irrefl s (X + Z)" "locally_irrefl s (Y + Z)" "trans s"
  shows "(X + Z, Y + Z) ∈ mult2_s ns s ⟹ (X, Y) ∈ mult2_s ns s"
  using assms(5, 6)
proof (induct Z)
  case (add z Z) then show ?case
    using mult2_s_locally_cancel1[OF assms(1-4), of z "X + Z" "Y + Z"] 
    by auto (metis add_mset_add_single assms(7) li_trans_l) 
qed auto

lemma mult2_s_cancel:
  assumes "s O ns ⊆ s" "ns O s ⊆ s" "refl ns" "trans ns" "irrefl s" "trans s"
  shows "(X + Z, Y + Z) ∈ mult2_s ns s ⟹ (X, Y) ∈ mult2_s ns s"
  using mult2_s_locally_cancel assms by (metis irrefl_def locally_irrefl_def) 

lemma mult2_ns_cancel:
  assumes "s O ns ⊆ s" "ns O s ⊆ s" "refl ns" "trans s" "irrefl s" "trans ns"
  shows "(X + Z, Y + Z) ∈ mult2_s ns s ⟹ (X, Y) ∈ mult2_ns ns s"
  unfolding mult2_ns_conv using assms mult2_s_cancel multpw_cancel by blast

subsection ‹Implementation friendly versions of @{const mult2_s} and @{const mult2_ns}›

definition mult2_alt :: "bool ⇒ 'a rel ⇒ 'a rel ⇒ 'a multiset rel" where
  "mult2_alt b ns s = {(X, Y). (∃X1 X2 Y1 Y2. X = X1 + X2 ∧ Y = Y1 + Y2 ∧
    (X1, Y1) ∈ multpw ns ∧ (b ∨ Y2 ≠ {#}) ∧ (∀x. x ∈# X2 ⟶ (∃y. y ∈# Y2 ∧ (x, y) ∈ s)))}"

lemma mult2_altI:
  assumes "X = X1 + X2" "Y = Y1 + Y2" "(X1, Y1) ∈ multpw ns"
    "b ∨ Y2 ≠ {#}" "∀x. x ∈# X2 ⟶ (∃y. y ∈# Y2 ∧ (x, y) ∈ s)"
  shows "(X, Y) ∈ mult2_alt b ns s"
  using assms unfolding mult2_alt_def by blast

lemma mult2_altE:
  assumes "(X, Y) ∈ mult2_alt b ns s"
  obtains X1 X2 Y1 Y2 where "X = X1 + X2" "Y = Y1 + Y2" "(X1, Y1) ∈ multpw ns"
    "b ∨ Y2 ≠ {#}" "∀x. x ∈# X2 ⟶ (∃y. y ∈# Y2 ∧ (x, y) ∈ s)"
  using assms unfolding mult2_alt_def by blast

lemma mono_mult2_alt:
  assumes "ns ⊆ ns'" "s ⊆ s'" shows "mult2_alt b ns s ⊆ mult2_alt b ns' s'"
  unfolding mult2_alt_def using mono_multpw[OF assms(1)] assms by (blast 19)

abbreviation "mult2_alt_s ≡ mult2_alt False"
abbreviation "mult2_alt_ns ≡ mult2_alt True"

lemmas mult2_alt_s_def = mult2_alt_def[where b = False, unfolded simp_thms]
lemmas mult2_alt_ns_def = mult2_alt_def[where b = True, unfolded simp_thms]
lemmas mult2_alt_sI = mult2_altI[where b = False, unfolded simp_thms]
lemmas mult2_alt_nsI = mult2_altI[where b = True, unfolded simp_thms True_implies_equals]
lemmas mult2_alt_sE = mult2_altE[where b = False, unfolded simp_thms]
lemmas mult2_alt_nsE = mult2_altE[where b = True, unfolded simp_thms True_implies_equals]

paragraph ‹Equivalence to @{const mult2_s} and @{const mult2_ns}›

lemma mult2_s_eq_mult2_s_alt:
  assumes "ns O s ⊆ s" "refl ns" "trans s"
  shows "mult2_alt_s ns s = mult2_s ns s"
  using mult2_s_one_step[OF assms] unfolding mult2_alt_s_def by blast

lemma mult2_ns_eq_mult2_ns_alt:
  assumes "ns O s ⊆ s" "refl ns" "trans s"
  shows "mult2_alt_ns ns s = mult2_ns ns s"
  using mult2_ns_one_step[OF assms] unfolding mult2_alt_ns_def by blast

lemma mult2_alt_local:
  assumes "(X, Y) ∈ mult2_alt b ns s"
  shows "(X, Y) ∈ mult2_alt b (ns ∩ set_mset X × set_mset Y) (s ∩ set_mset X × set_mset Y)"
proof -
  from assms obtain X1 X2 Y1 Y2 where *: "X = X1 + X2" "Y = Y1 + Y2" and
    "(X1, Y1) ∈ multpw ns" "(b ∨ Y2 ≠ {#})" "(∀x. x ∈# X2 ⟶ (∃y. y ∈# Y2 ∧ (x, y) ∈ s))"
    unfolding mult2_alt_def by blast
  then have "X = X1 + X2 ∧ Y = Y1 + Y2 ∧
    (X1, Y1) ∈ multpw (ns ∩ set_mset X × set_mset Y) ∧ (b ∨ Y2 ≠ {#}) ∧
    (∀x. x ∈# X2 ⟶ (∃y. y ∈# Y2 ∧ (x, y) ∈ s ∩ set_mset X × set_mset Y))"
    using multpw_local[of X1 Y1 ns]
      mono_multpw[of "ns ∩ set_mset X1 × set_mset Y1" "ns ∩ set_mset X × set_mset Y"] assms
    unfolding * set_mset_union unfolding set_mset_def by blast
  then show ?thesis unfolding mult2_alt_def by blast
qed

subsection ‹Local well-foundedness: restriction to downward closure of a set›

definition wf_below :: "'a rel ⇒ 'a set ⇒ bool" where
  "wf_below r A = wf (Restr r ((r⇧*)¯ `` A))"

lemma wf_below_UNIV[simp]:
  shows "wf_below r UNIV ⟷ wf r"
  by (auto simp: wf_below_def rtrancl_converse[symmetric] Image_closed_trancl[OF subset_UNIV])

lemma wf_below_mono1:
  assumes "r ⊆ r'" "wf_below r' A" shows "wf_below r A"
  using assms unfolding wf_below_def
  by (intro wf_subset[OF assms(2)[unfolded wf_below_def]] Int_mono Sigma_mono Image_mono
      iffD2[OF converse_mono] rtrancl_mono subset_refl)

lemma wf_below_mono2:
  assumes "A ⊆ A'" "wf_below r A'" shows "wf_below r A"
  using assms unfolding wf_below_def
  by (intro wf_subset[OF assms(2)[unfolded wf_below_def]]) blast

lemma wf_below_pointwise:
  "wf_below r A ⟷ (∀a. a ∈ A ⟶ wf_below r {a})" (is "?L ⟷ ?R")
proof
  assume ?L then show ?R using wf_below_mono2[of "{_}" A r] by blast
next
  have *: "(r⇧*)¯ `` A = ⋃{(r⇧*)¯ `` {a} |a. a ∈ A}" unfolding Image_def by blast
  assume ?R
  { fix x X assume *: "X ⊆ Restr r ((r⇧*)¯ `` A) `` X" "x ∈ X"
    then obtain a where **: "a ∈ A" "(x, a) ∈ r⇧*" unfolding Image_def by blast
    from * have "X ∩ ((r⇧*)¯ `` {a}) ⊆ (Restr r ((r⇧*)¯ `` A) `` X) ∩ ((r⇧*)¯ `` {a})" by auto
    also have "... ⊆ Restr r ((r⇧*)¯ `` {a}) `` (X  ∩ ((r⇧*)¯ `` {a}))" unfolding Image_def by fastforce
    finally have "X ∩ ((r⇧*)¯ `` {a}) = {}" using ‹?R› **(1) unfolding wf_below_def
      by (intro wfE_pf[of "Restr r ((r⇧*)¯ `` {a})"]) (auto simp: Image_def)
    then have False using *(2) ** unfolding Image_def by blast
  }
  then show ?L unfolding wf_below_def by (intro wfI_pf) auto
qed

lemma SN_on_Image_rtrancl_conv:
  "SN_on r A ⟷ SN_on r (r⇧* `` A)" (is "?L ⟷ ?R")
proof
  assume ?L then show ?R by (auto simp: SN_on_Image_rtrancl)
next
  assume ?R then show ?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 restr_trancl_under:
  shows "Restr (r⇧+) ((r⇧*)¯ `` A) = (Restr r ((r⇧*)¯ `` A))⇧+"
proof (intro equalityI subrelI, elim IntE conjE[OF iffD1[OF mem_Sigma_iff]])
  fix a b assume *: "(a, b) ∈ r⇧+" "b ∈ (r⇧*)¯ `` A"
  then have "(a, b) ∈ (Restr r ((r⇧*)¯ `` A))⇧+ ∧ a ∈ (r⇧*)¯ `` A"
  proof (induct rule: trancl_trans_induct[consumes 1])
    case 1 then show ?case by (auto simp: Image_def intro: converse_rtrancl_into_rtrancl)
  next
    case 2 then show ?case by (auto simp del: Int_iff del: ImageE)
  qed
  then show "(a, b) ∈ (Restr r ((r⇧*)¯ `` A))⇧+" by simp
next
  fix a b assume "(a, b) ∈ (Restr r ((r⇧*)¯ `` A))⇧+"
  then show "(a, b) : Restr (r⇧+) ((r⇧*)¯ `` A)" by induct auto
qed

lemma wf_below_trancl:
  shows "wf_below (r⇧+) A ⟷ wf_below r A"
  using restr_trancl_under[of r A] by (simp add: wf_below_def wf_trancl_conv)

lemma wf_below_mult_local:
  assumes "wf_below r (set_mset X)" shows "wf_below (mult r) {X}"
    (* this is actually an equivalence; is the other direction useful as well? *)
proof -
  have foo: "mult r ⊆ mult (r⇧+)" using mono_mult[of r "r⇧+"] by force
  have "(Y, X) ∈ (mult (r⇧+))⇧* ⟹ set_mset Y ⊆ ((r⇧+)⇧*)¯ `` set_mset X" for Y
  proof (induct rule: converse_rtrancl_induct)
    case (step Z Y)
    obtain I J K where *: "Y = I + J" "Z = I + K" "(∀k ∈ set_mset K. ∃j ∈ set_mset J. (k, j) ∈ r⇧+)"
      using mult_implies_one_step[OF _ step(1)] by auto
    { fix k assume "k ∈# K"
      then obtain j where "j ∈# J" "(k, j) ∈ r⇧+" using *(3) by auto
      moreover then obtain x where "x ∈# X" "(j, x) ∈ r⇧*" using step(3) by (auto simp: *)
      ultimately have "∃x. x ∈# X ∧ (k, x) ∈ r⇧*" by auto
    }
    then show ?case using * step(3) by (auto simp: Image_def) metis
  qed auto
  then have q: "(Y, X) ∈ (mult (r⇧+))⇧* ⟹ y ∈# Y  ⟹ y ∈ ((r⇧+)⇧*)¯ `` set_mset X" for Y y by force
  have "Restr (mult (r⇧+)) (((mult (r⇧+))⇧*)¯ `` {X}) ⊆ mult (Restr (r⇧+) (((r⇧+)⇧*)¯ `` set_mset X))"
  proof (intro subrelI)
    fix N M assume "(N, M) ∈ Restr (mult (r⇧+)) (((mult (r⇧+))⇧*)¯ `` {X})"
    then have **:  "(N, X) ∈ (mult (r⇧+))⇧*" "(M, X) ∈ (mult (r⇧+))⇧*" "(N, M) ∈ mult (r⇧+)" by auto
    obtain I J K where *: "M = I + J" "N = I + K" "J ≠ {#}" "∀k ∈ set_mset K. ∃j ∈ set_mset J. (k, j) ∈ r⇧+"
      using mult_implies_one_step[OF _ ‹(N, M) ∈ mult (r⇧+)›] by auto
    then show "(N, M) ∈ mult (Restr (r⇧+) (((r⇧+)⇧*)¯ `` set_mset X))"
      using q[OF **(1)] q[OF **(2)] unfolding * by (auto intro: one_step_implies_mult)
  qed
  note bar = subset_trans[OF Int_mono[OF foo Sigma_mono] this]
  have "((mult r)⇧*)¯ `` {X} ⊆ ((mult (r⇧+))⇧*)¯ `` {X}" using foo by (simp add: Image_mono rtrancl_mono)
  then have "Restr (mult r) (((mult r)⇧*)¯ `` {X}) ⊆ mult (Restr (r⇧+) (((r⇧+)⇧*)¯ `` set_mset X))"
    by (intro bar) auto
  then show ?thesis using wf_mult assms wf_subset
    unfolding wf_below_trancl[of r, symmetric] unfolding wf_below_def by blast
qed

lemma qc_wf_below:
  assumes "s O ns ⊆ (s ∪ ns)⇧* O s" "wf_below s A"
  shows "wf_below (ns⇧* O s O ns⇧*) A"
  unfolding wf_below_def
proof (intro wfI_pf)
  let ?A' = "((ns⇧* O s O ns⇧*)⇧*)¯ `` A"
  fix X assume X: "X ⊆ Restr (ns⇧* O s O ns⇧*) ?A' `` X"
  let ?X' = "((s ∪ ns)⇧* ∩ UNIV × ((s⇧*)¯ `` A)) `` X"
  have *: "s O (s ∪ ns)⇧* ⊆ (s ∪ ns)⇧* O s"
  proof - (* taken from the proof of qc_wf_relto_iff *)
    { fix x y z assume "(y, z) ∈ (s ∪ ns)⇧*" and "(x, y) ∈ s"
      then have "(x, z) ∈ (s ∪ ns)⇧* O s"
      proof (induct y z)
        case rtrancl_refl then show ?case by auto
      next
        case (rtrancl_into_rtrancl a b c)
        then have "(x, c) ∈ ((s ∪ ns)⇧* O (s ∪ ns)⇧*) O s" using assms by blast
        then show ?case by simp
      qed }
    then show ?thesis by auto
  qed
  { fix x assume "x ∈ Restr (ns⇧* O s O ns⇧*) ?A' `` X"
    then obtain y z where **: "y ∈ X" "z ∈ A" "(y, x) ∈ ns⇧* O s O ns⇧*" "(x, z) ∈ (ns⇧* O s O ns⇧*)⇧*" by blast
    have "(ns⇧* O s O ns⇧*) O (ns⇧* O s O ns⇧*)⇧* ⊆ (s ∪ ns)⇧*" by regexp 
    then have "(y, z) ∈ (s ∪ ns)⇧*" using **(3,4) by blast
    moreover have "?X' = {}"
    proof (intro wfE_pf[OF assms(2)[unfolded wf_below_def]] subsetI)
      fix x assume "x ∈ ?X'"
      then have "x ∈ ((s ∪ ns)⇧* ∩ UNIV × ((s⇧*)¯ `` A)) `` Restr (ns⇧* O s O ns⇧*) ?A' `` X" using X by auto
      then obtain x0 y z where **: "z ∈ X" "x0 ∈ A" "(z, y) ∈ ns⇧* O s O ns⇧*" "(y, x) ∈ (s ∪ ns)⇧*" "(x, x0) ∈ s⇧*"
        unfolding Image_def by blast
      have "(ns⇧* O s O ns⇧*) O (s ∪ ns)⇧* ⊆ ns⇧* O (s O (s ∪ ns)⇧*)" by regexp
      with **(3,4) have "(z, x) ∈ ns⇧* O (s O (s ∪ ns)⇧*)" by blast
      moreover have "ns⇧* O ((s ∪ ns)⇧* O s) ⊆ (s ∪ ns)⇧* O s" by regexp
      ultimately have "(z, x) ∈ (s ∪ ns)⇧* O s" using * by blast
      then obtain x' where "z ∈ X" "(z, x') ∈ (s ∪ ns)⇧*"  "(x', x) ∈ s" "(x', x0) ∈ s⇧*" "(x, x0) ∈ s⇧*" "x0 ∈ A"
        using **(1,2,5) converse_rtrancl_into_rtrancl[OF _ **(5)] by blast
      then show "x ∈ Restr s ((s⇧*)¯ `` A) `` ?X'"
        unfolding Image_def by blast
    qed
    ultimately have False using **(1,2) unfolding Image_def by blast 
  }
  then show "X = {}" using X by blast
qed

lemma wf_below_mult2_s_local:
  assumes "wf_below s (set_mset X)" "s O ns ⊆ s" "refl ns" "trans ns"
  shows "wf_below (mult2_s ns s) {X}"
  using wf_below_mult_local[of s X] assms multpw_mult_commute[of s ns]
    wf_below_mono1[of "multpw ns O mult s" "(multpw ns)⇧* O mult s O (multpw ns)⇧*" "{X}"]
    qc_wf_below[of "mult s" "multpw ns" "{X}"]
  unfolding mult2_s_def by blast


subsection ‹Trivial cases›

lemma mult2_alt_emptyL:
  "({#}, Y) ∈ mult2_alt b ns s ⟷ b ∨ Y ≠ {#}"
  unfolding mult2_alt_def by auto

lemma mult2_alt_emptyR:
  "(X, {#}) ∈ mult2_alt b ns s ⟷ b ∧ X = {#}"
  unfolding mult2_alt_def by (auto intro: multiset_eqI)

lemma mult2_alt_s_single:
  "(a, b) ∈ s ⟹ ({#a#}, {#b#}) ∈ mult2_alt_s ns s"
  using mult2_altI[of _ "{#}" _ _ "{#}" _ ns False s] by auto

lemma multpw_implies_mult2_alt_ns:
  assumes "(X, Y) ∈ multpw ns"
  shows "(X, Y) ∈ mult2_alt_ns ns s"
  using assms by (intro mult2_alt_nsI[of X X "{#}" Y Y "{#}"]) auto

lemma mult2_alt_ns_conv:
  "mult2_alt_ns ns s = mult2_alt_s ns s ∪ multpw ns" (is "?l = ?r")
proof (intro equalityI subrelI)
  fix X Y assume "(X, Y) ∈ ?l"
  thm mult2_alt_nsE
  then obtain X1 X2 Y1 Y2 where "X = X1 + X2" "Y = Y1 + Y2" "(X1, Y1) ∈ multpw ns"
    "∀x. x ∈# X2 ⟶ (∃y. y ∈# Y2 ∧ (x, y) ∈ s)" by (auto elim: mult2_alt_nsE)
  then show "(X, Y) ∈ ?r" using count_inject[of X2 "{#}"]
    by (cases "Y2 = {#}") (auto intro: mult2_alt_sI elim: mult2_alt_nsE mult2_alt_sE)
next
  fix X Y assume "(X, Y) ∈ ?r" then show "(X, Y) ∈ ?l"
    by (auto intro: mult2_alt_nsI multpw_implies_mult2_alt_ns elim: mult2_alt_sE)
qed

lemma mult2_alt_s_implies_mult2_alt_ns:
  assumes "(X, Y) ∈ mult2_alt_s ns s"
  shows "(X, Y) ∈ mult2_alt_ns ns s"
  using assms by (auto intro: mult2_alt_nsI elim: mult2_alt_sE)

lemma mult2_alt_add:
  assumes "(X1, Y1) ∈ mult2_alt b1 ns s" and "(X2, Y2) ∈ mult2_alt b2 ns s"
  shows "(X1 + X2, Y1 + Y2) ∈ mult2_alt (b1 ∧ b2) ns s"
proof -
  from assms obtain X11 X12 Y11 Y12 X21 X22 Y21 Y22 where
    "X1 = X11 + X12" "Y1 = Y11 + Y12"
    "(X11, Y11) ∈ multpw ns" "(b1 ∨ Y12 ≠ {#})" "(∀x. x ∈# X12 ⟶ (∃y. y ∈# Y12 ∧ (x, y) ∈ s))"
    "X2 = X21 + X22" "Y2 = Y21 + Y22"
    "(X21, Y21) ∈ multpw ns" "(b2 ∨ Y22 ≠ {#})" "(∀x. x ∈# X22 ⟶ (∃y. y ∈# Y22 ∧ (x, y) ∈ s))"
    unfolding mult2_alt_def by (blast 9)
  then show ?thesis
    by (intro mult2_altI[of _ "X11 + X21" "X12 + X22" _ "Y11 + Y21" "Y12 + Y22"])
      (auto intro: multpw_add simp: ac_simps)
qed

lemmas mult2_alt_s_s_add = mult2_alt_add[of _ _ False _ _ _ _ False, unfolded simp_thms]
lemmas mult2_alt_ns_s_add = mult2_alt_add[of _ _ True _ _ _ _ False, unfolded simp_thms]
lemmas mult2_alt_s_ns_add = mult2_alt_add[of _ _ False _ _ _ _ True, unfolded simp_thms]
lemmas mult2_alt_ns_ns_add = mult2_alt_add[of _ _ True _ _ _ _ True, unfolded simp_thms]


lemma multpw_map:
  assumes "⋀x y. x ∈# X ⟹ y ∈# Y ⟹ (x, y) ∈ ns ⟹ (f x, g y) ∈ ns'"
    and "(X, Y) ∈ multpw ns"
  shows "(image_mset f X, image_mset g Y) ∈ multpw ns'"
  using assms(2,1) by (induct X Y rule: multpw.induct) (auto intro: multpw.intros)

lemma mult2_alt_map:
  assumes "⋀x y. x ∈# X ⟹ y ∈# Y ⟹ (x, y) ∈ ns ⟹ (f x, g y) ∈ ns'"
    and "⋀x y. x ∈# X ⟹ y ∈# Y ⟹ (x, y) ∈ s ⟹ (f x, g y) ∈ s'"
    and "(X, Y) ∈ mult2_alt b ns s"
  shows "(image_mset f X, image_mset g Y) ∈ mult2_alt b ns' s'"
proof -
  from assms(3) obtain X1 X2 Y1 Y2 where "X = X1 + X2" "Y = Y1 + Y2" "(X1, Y1) ∈ multpw ns"
    "b ∨ Y2 ≠ {#}" "∀x. x ∈# X2 ⟶ (∃y. y ∈# Y2 ∧ (x, y) ∈ s)" by (auto elim: mult2_altE)
  moreover from this(1,2,5) have "∀x. x ∈# image_mset f X2 ⟶ (∃y. y ∈# image_mset g Y2 ∧ (x, y) ∈ s')"
    using assms(2) by (simp add: in_image_mset image_iff) blast
  ultimately show ?thesis using assms multpw_map[of X1 Y1 ns f g]
    by (intro mult2_altI[of _ "image_mset f X1" "image_mset f X2" _ "image_mset g Y1" "image_mset g Y2"]) auto
qed

text ‹Local transitivity of @{const mult2_alt}›

lemma trans_mult2_alt_local:
  assumes ss: "⋀x y z. x ∈# X ⟹ y ∈# Y ⟹ z ∈# Z ⟹ (x, y) ∈ s ⟹ (y, z) ∈ s ⟹ (x, z) ∈ s"
    and ns: "⋀x y z. x ∈# X ⟹ y ∈# Y ⟹ z ∈# Z ⟹ (x, y) ∈ ns ⟹ (y, z) ∈ s ⟹ (x, z) ∈ s"
    and sn: "⋀x y z. x ∈# X ⟹ y ∈# Y ⟹ z ∈# Z ⟹ (x, y) ∈ s ⟹ (y, z) ∈ ns ⟹ (x, z) ∈ s"
    and nn: "⋀x y z. x ∈# X ⟹ y ∈# Y ⟹ z ∈# Z ⟹ (x, y) ∈ ns ⟹ (y, z) ∈ ns ⟹ (x, z) ∈ ns"
    and xyz: "(X, Y) ∈ mult2_alt b1 ns s" "(Y, Z) ∈ mult2_alt b2 ns s"
  shows "(X, Z) ∈ mult2_alt (b1 ∧ b2) ns s"
proof -
  let ?a1 = Enum.finite_3.a⇩1 and ?a2 = Enum.finite_3.a⇩2 and ?a3 = Enum.finite_3.a⇩3
  let ?t = "{(?a1, ?a2), (?a1, ?a3), (?a2, ?a3)}"
  let ?A = "{(?a1, x) |x. x ∈# X} ∪ {(?a2, y) |y. y ∈# Y} ∪ {(?a3, z) |z. z ∈# Z}"
  define s' where "s' = Restr {((a, x), (b, y)) |a x b y. (a, b) ∈ ?t ∧ (x, y) ∈ s} ?A"
  define ns' where "ns' = (Restr {((a, x), (b, y)) |a x b y. (a, b) ∈ ?t ∧ (x, y) ∈ ns} ?A)⇧="
  have *: "refl ns'" "trans ns'" "trans s'" "s' O ns' ⊆ s'" "ns' O s' ⊆ s'"
    by (force simp: trans_def ss ns sn nn s'_def ns'_def)+
  have "({#(?a1, x). x ∈# X#}, {#(?a2, y). y ∈# Y#}) ∈ mult2_alt b1 ns' s'"
    by (auto intro: mult2_alt_map[OF _ _ xyz(1)] simp: s'_def ns'_def)
  moreover have "({#(?a2, y). y ∈# Y#}, {#(?a3, z). z ∈# Z#}) ∈ mult2_alt b2 ns' s'"
    by (auto intro: mult2_alt_map[OF _ _ xyz(2)] simp: s'_def ns'_def)
  ultimately have "({#(?a1, x). x ∈# X#}, {#(?a3, z). z ∈# Z#}) ∈ mult2_alt (b1 ∧ b2) ns' s'"
    using mult2_s_eq_mult2_s_alt[OF *(5,1,3)] mult2_ns_eq_mult2_ns_alt[OF *(5,1,3)]
      trans_mult2_s[OF *(4,1,2)] trans_mult2_ns[OF *(4,1,2)] compat_mult2[OF *(4,1,2)]
    by (cases b1; cases b2) (auto simp: trans_O_iff)
  from mult2_alt_map[OF _ _ this, of snd snd ns s]
  show ?thesis by (auto simp: s'_def ns'_def image_mset.compositionality comp_def in_image_mset image_iff)
qed

lemmas trans_mult2_alt_s_s_local = trans_mult2_alt_local[of _ _ _ _ _ False False, unfolded simp_thms]
lemmas trans_mult2_alt_ns_s_local = trans_mult2_alt_local[of _ _ _ _ _ True False, unfolded simp_thms]
lemmas trans_mult2_alt_s_ns_local = trans_mult2_alt_local[of _ _ _ _ _ False True, unfolded simp_thms]
lemmas trans_mult2_alt_ns_ns_local = trans_mult2_alt_local[of _ _ _ _ _ True True, unfolded simp_thms]

end