Theory Well_Quasi_Orders.Multiset_Extension

(*  Title:      Well-Quasi-Orders
    Author:     Christian Sternagel <c.sternagel@gmail.com>
    Maintainer: Christian Sternagel
    License:    LGPL
*)

section ‹Multiset Extension of Orders (as Binary Predicates)›

(*TODO: move theory (and maybe rename)*)

theory Multiset_Extension
imports
  Open_Induction.Restricted_Predicates
  "HOL-Library.Multiset"
begin

definition multisets :: "'a set  'a multiset set" where
  "multisets A = {M. set_mset M  A}"

lemma in_multisets_iff:
  "M  multisets A  set_mset M  A"
  by (simp add: multisets_def)

lemma empty_multisets [simp]:
  "{#}  multisets F"
  by (simp add: in_multisets_iff)

lemma multisets_union [simp]:
  "M  multisets A  N  multisets A  M + N  multisets A"
  by (auto simp add: in_multisets_iff)

definition mulex1 :: "('a  'a  bool)  'a multiset  'a multiset  bool" where
  "mulex1 P = (λM N. (M, N)  mult1 {(x, y). P x y})"

lemma mulex1_empty [iff]:
  "mulex1 P M {#}  False"
  using not_less_empty [of M "{(x, y). P x y}"]
  by (auto simp: mulex1_def)

lemma mulex1_add: "mulex1 P N (M0 + {#a#}) 
  (M. mulex1 P M M0  N = M + {#a#}) 
  (K. (b. b ∈# K  P b a)  N = M0 + K)"
  using less_add [of N a M0 "{(x, y). P x y}"]
  by (auto simp: mulex1_def)

lemma mulex1_self_add_right [simp]:
  "mulex1 P A (add_mset a A)"
proof -
  let ?R = "{(x, y). P x y}"
  thm mult1_def
  have "A + {#a#} = A + {#a#}" by simp
  moreover have "A = A + {#}" by simp
  moreover have "b. b ∈# {#}  (b, a)  ?R" by simp
  ultimately have "(A, add_mset a A)  mult1 ?R"
    unfolding mult1_def by blast
  then show ?thesis by (simp add: mulex1_def)
qed

lemma empty_mult1 [simp]:
  "({#}, {#a#})  mult1 R"
proof -
  have "{#a#} = {#} + {#a#}" by simp
  moreover have "{#} = {#} + {#}" by simp
  moreover have "b. b ∈# {#}  (b, a)  R" by simp
  ultimately show ?thesis unfolding mult1_def by force
qed

lemma empty_mulex1 [simp]:
  "mulex1 P {#} {#a#}"
  using empty_mult1 [of a "{(x, y). P x y}"] by (simp add: mulex1_def)

definition mulex_on :: "('a  'a  bool)  'a set  'a multiset  'a multiset  bool" where
  "mulex_on P A = (restrict_to (mulex1 P) (multisets A))++"

abbreviation mulex :: "('a  'a  bool)  'a multiset  'a multiset  bool" where
  "mulex P  mulex_on P UNIV"

lemma mulex_on_induct [consumes 1, case_names base step, induct pred: mulex_on]:
  assumes "mulex_on P A M N"
    and "M N. M  multisets A; N  multisets A; mulex1 P M N  Q M N"
    and "L M N. mulex_on P A L M; Q L M; N  multisets A; mulex1 P M N  Q L N"
  shows "Q M N"
  using assms unfolding mulex_on_def by (induct) blast+

lemma mulex_on_self_add_singleton_right [simp]:
  assumes "a  A" and "M  multisets A"
  shows "mulex_on P A M (add_mset a M)"
proof -
  have "mulex1 P M (M + {#a#})" by simp
  with assms have "restrict_to (mulex1 P) (multisets A) M (add_mset a M)"
    by (auto simp: multisets_def)
  then show ?thesis unfolding mulex_on_def by blast
qed

lemma singleton_multisets [iff]:
  "{#x#}  multisets A  x  A"
  by (auto simp: multisets_def)

lemma union_multisetsD:
  assumes "M + N  multisets A"
  shows "M  multisets A  N  multisets A"
  using assms by (auto simp: multisets_def)

lemma mulex_on_multisetsD [dest]:
  assumes "mulex_on P F M N"
  shows "M  multisets F" and "N  multisets F"
  using assms by (induct) auto

lemma union_multisets_iff [iff]:
  "M + N  multisets A  M  multisets A  N  multisets A"
  by (auto dest: union_multisetsD)

lemma add_mset_multisets_iff [iff]:
  "add_mset a M  multisets A  a  A  M  multisets A"
  unfolding add_mset_add_single[of a M] union_multisets_iff by auto

lemma mulex_on_trans:
  "mulex_on P A L M  mulex_on P A M N  mulex_on P A L N"
  by (auto simp: mulex_on_def)

lemma transp_on_mulex_on:
  "transp_on B (mulex_on P A)"
  using mulex_on_trans [of P A] by (auto simp: transp_on_def)
  
lemma mulex_on_add_right [simp]:
  assumes "mulex_on P A M N" and "a  A"
  shows "mulex_on P A M (add_mset a N)"
proof -
  from assms have "a  A" and "N  multisets A" by auto
  then have "mulex_on P A N (add_mset a N)" by simp
  with mulex_on P A M N show ?thesis by (rule mulex_on_trans)
qed

lemma empty_mulex_on [simp]:
  assumes "M  {#}" and "M  multisets A"
  shows "mulex_on P A {#} M"
using assms
proof (induct M)
  case (add a M)
  show ?case
  proof (cases "M = {#}")
    assume "M = {#}"
    with add show ?thesis by (auto simp: mulex_on_def)
  next
    assume "M  {#}"
    with add show ?thesis by (auto intro: mulex_on_trans)
  qed
qed simp

lemma mulex_on_self_add_right [simp]:
  assumes "M  multisets A" and "K  multisets A" and "K  {#}"
  shows "mulex_on P A M (M + K)"
using assms
proof (induct K)
  case empty
  then show ?case by (cases "K = {#}") auto
next
  case (add a M)
  show ?case
  proof (cases "M = {#}")
    assume "M = {#}" with add show ?thesis by auto
  next
    assume "M  {#}" with add show ?thesis
      by (auto dest: mulex_on_add_right simp add: ac_simps)
  qed
qed

lemma mult1_singleton [iff]:
  "({#x#}, {#y#})  mult1 R  (x, y)  R"
proof
  assume "(x, y)  R"
  then have "{#y#} = {#} + {#y#}"
    and "{#x#} = {#} + {#x#}"
    and "b. b ∈# {#x#}  (b, y)  R" by auto
  then show "({#x#}, {#y#})  mult1 R" unfolding mult1_def by blast
next
  assume "({#x#}, {#y#})  mult1 R"
  then obtain M0 K a
    where "{#y#} = add_mset a M0"
    and "{#x#} = M0 + K"
    and "b. b ∈# K  (b, a)  R"
    unfolding mult1_def by blast
  then show "(x, y)  R" by (auto simp: add_eq_conv_diff)
qed

lemma mulex1_singleton [iff]:
  "mulex1 P {#x#} {#y#}  P x y"
  using mult1_singleton [of x y "{(x, y). P x y}"] by (simp add: mulex1_def)

lemma singleton_mulex_onI:
  "P x y  x  A  y  A  mulex_on P A {#x#} {#y#}"
  by (auto simp: mulex_on_def)

lemma reflclp_mulex_on_add_right [simp]:
  assumes "(mulex_on P A)== M N" and "M  multisets A" and "a  A"
  shows "mulex_on P A M (N + {#a#})"
  using assms by (cases "M = N") simp_all

lemma reflclp_mulex_on_add_right' [simp]:
  assumes "(mulex_on P A)== M N" and "M  multisets A" and "a  A"
  shows "mulex_on P A M ({#a#} + N)"
  using reflclp_mulex_on_add_right [OF assms] by (simp add: ac_simps)

lemma mulex_on_union_right [simp]:
  assumes "mulex_on P F A B" and "K  multisets F"
  shows "mulex_on P F A (K + B)"
using assms
proof (induct K)
  case (add a K)
  then have "a  F" and "mulex_on P F A (B + K)" by (auto simp: multisets_def ac_simps)
  then have "mulex_on P F A ((B + K) + {#a#})" by simp
  then show ?case by (simp add: ac_simps)
qed simp

lemma mulex_on_union_right' [simp]:
  assumes "mulex_on P F A B" and "K  multisets F"
  shows "mulex_on P F A (B + K)"
  using mulex_on_union_right [OF assms] by (simp add: ac_simps)

text ‹Adapted from @{thm all_accessible} in @{theory "HOL-Library.Multiset"}.›
lemma accessible_on_mulex1_multisets:
  assumes wf: "wfp_on P A"
  shows "Mmultisets A. accessible_on (mulex1 P) (multisets A) M"
proof
  let ?P = "mulex1 P"
  let ?A = "multisets A"
  let ?acc = "accessible_on ?P ?A"
  {
    fix M M0 a
    assume M0: "?acc M0"
      and "a  A"
      and "M0  ?A"
      and wf_hyp: "b. b  A; P b a  (M. ?acc (M)  ?acc (M + {#b#}))"
      and acc_hyp: "M. M  ?A  ?P M M0  ?acc (M + {#a#})"
    then have "add_mset a M0  ?A" by (auto simp: multisets_def)
    then have "?acc (add_mset a M0)"
    proof (rule accessible_onI [of "add_mset a M0"])
      fix N
      assume "N  ?A"
        and "?P N (add_mset a M0)"
      then have "((M. M  ?A  ?P M M0  N = M + {#a#}) 
          (K. (b. b ∈# K  P b a)  N = M0 + K))"
        using mulex1_add [of P N M0 a] by (auto simp: multisets_def)
      then show "?acc (N)"
      proof (elim exE disjE conjE)
        fix M assume "M  ?A" and "?P M M0" and N: "N = M + {#a#}"
        from acc_hyp have "M  ?A  ?P M M0  ?acc (M + {#a#})" ..
        with M  ?A and ?P M M0 have "?acc (M + {#a#})" by blast
        then show "?acc (N)" by (simp only: N)
      next
        fix K
        assume N: "N = M0 + K"
        assume "b. b ∈# K  P b a"
        moreover from N and N  ?A have "K  ?A" by (auto simp: multisets_def)
        ultimately have "?acc (M0 + K)"
        proof (induct K)
          case empty
          from M0 show "?acc (M0 + {#})" by simp
        next
          case (add x K)
          from add.prems have "x  A" and "P x a" by (auto simp: multisets_def)
          with wf_hyp have "M. ?acc M  ?acc (M + {#x#})" by blast
          moreover from add have "?acc (M0 + K)" by (auto simp: multisets_def)
          ultimately show "?acc (M0 + (add_mset x K))" by simp
        qed
        then show "?acc N" by (simp only: N)
      qed
    qed
  } note tedious_reasoning = this

  fix M
  assume "M  ?A"
  then show "?acc M"
  proof (induct M)
    show "?acc {#}"
    proof (rule accessible_onI)
      show "{#}  ?A" by (auto simp: multisets_def)
    next
      fix b assume "?P b {#}" then show "?acc b" by simp
    qed
  next
    case (add a M)
    then have "?acc M" by (auto simp: multisets_def)
    from add have "a  A" by (auto simp: multisets_def)
    with wf have "M. ?acc M  ?acc (add_mset a M)"
    proof (induct)
      case (less a)
      then have r: "b. b  A; P b a  (M. ?acc M  ?acc (M + {#b#}))" by auto
      show "M. ?acc M  ?acc (add_mset a M)"
      proof (intro allI impI)
        fix M'
        assume "?acc M'"
        moreover then have "M'  ?A" by (blast dest: accessible_on_imp_mem)
        ultimately show "?acc (add_mset a M')"
          by (induct) (rule tedious_reasoning [OF _ a  A _ r], auto)
      qed
    qed
    with ?acc (M) show "?acc (add_mset a M)" by blast
  qed
qed

lemmas wfp_on_mulex1_multisets =
  accessible_on_mulex1_multisets [THEN accessible_on_imp_wfp_on]

lemmas irreflp_on_mulex1 =
  wfp_on_mulex1_multisets [THEN wfp_on_imp_irreflp_on]

lemma wfp_on_mulex_on_multisets:
  assumes "wfp_on P A"
  shows "wfp_on (mulex_on P A) (multisets A)"
  using wfp_on_mulex1_multisets [OF assms]
  by (simp only: mulex_on_def wfp_on_restrict_to_tranclp_wfp_on_conv)

lemmas irreflp_on_mulex_on =
  wfp_on_mulex_on_multisets [THEN wfp_on_imp_irreflp_on]

lemma mulex1_union:
  "mulex1 P M N  mulex1 P (K + M) (K + N)"
  by (auto simp: mulex1_def mult1_union)

lemma mulex_on_union:
  assumes "mulex_on P A M N" and "K  multisets A"
  shows "mulex_on P A (K + M) (K + N)"
using assms
proof (induct)
  case (base M N)
  then have "mulex1 P (K + M) (K + N)" by (blast dest: mulex1_union)
  moreover from base have "(K + M)  multisets A"
    and "(K + N)  multisets A" by (auto simp: multisets_def)
  ultimately have "restrict_to (mulex1 P) (multisets A) (K + M) (K + N)" by auto
  then show ?case by (auto simp: mulex_on_def)
next
  case (step L M N)
  then have "mulex1 P (K + M) (K + N)" by (blast dest: mulex1_union)
  moreover from step have "(K + M)  multisets A" and "(K + N)  multisets A" by blast+
  ultimately have "(restrict_to (mulex1 P) (multisets A))++ (K + M) (K + N)" by auto
  moreover have "mulex_on P A (K + L) (K + M)" using step by blast
  ultimately show ?case by (auto simp: mulex_on_def)
qed

lemma mulex_on_union':
  assumes "mulex_on P A M N" and "K  multisets A"
  shows "mulex_on P A (M + K) (N + K)"
  using mulex_on_union [OF assms] by (simp add: ac_simps)

lemma mulex_on_add_mset:
  assumes "mulex_on P A M N" and "m  A"
  shows "mulex_on P A (add_mset m M) (add_mset m N)"
  unfolding add_mset_add_single[of m M] add_mset_add_single[of m N]
  apply (rule mulex_on_union')
  using assms by auto

lemma union_mulex_on_mono:
  "mulex_on P F A C  mulex_on P F B D  mulex_on P F (A + B) (C + D)"
  by (metis mulex_on_multisetsD mulex_on_trans mulex_on_union mulex_on_union')

lemma mulex_on_add_mset':
  assumes "P m n" and "m  A" and "n  A" and "M  multisets A"
  shows "mulex_on P A (add_mset m M) (add_mset n M)"
  unfolding add_mset_add_single[of m M] add_mset_add_single[of n M]
  apply (rule mulex_on_union)
  using assms by (auto simp: mulex_on_def)

lemma mulex_on_add_mset_mono:
  assumes "P m n" and "m  A" and "n  A" and "mulex_on P A M N"
  shows "mulex_on P A (add_mset m M) (add_mset n N)"
  unfolding add_mset_add_single[of m M] add_mset_add_single[of n N]
  apply (rule union_mulex_on_mono)
  using assms by (auto simp: mulex_on_def)

lemma union_mulex_on_mono1:
  "A  multisets F  (mulex_on P F)== A C  mulex_on P F B D 
    mulex_on P F (A + B) (C + D)"
  by (auto intro: union_mulex_on_mono mulex_on_union)

lemma union_mulex_on_mono2:
  "B  multisets F  mulex_on P F A C  (mulex_on P F)== B D 
    mulex_on P F (A + B) (C + D)"
  by (auto intro: union_mulex_on_mono mulex_on_union')

lemma mult1_mono:
  assumes "x y. x  A; y  A; (x, y)  R  (x, y)  S"
    and "M  multisets A"
    and "N  multisets A"
    and "(M, N)  mult1 R"
  shows "(M, N)  mult1 S"
  using assms unfolding mult1_def multisets_def
  by auto (metis (full_types) subsetD)

lemma mulex1_mono:
  assumes "x y. x  A; y  A; P x y  Q x y"
    and "M  multisets A"
    and "N  multisets A"
    and "mulex1 P M N"
  shows "mulex1 Q M N"
  using mult1_mono [of A "{(x, y). P x y}" "{(x, y). Q x y}" M N]
    and assms unfolding mulex1_def by blast

lemma mulex_on_mono:
  assumes *: "x y. x  A; y  A; P x y  Q x y"
    and "mulex_on P A M N"
  shows "mulex_on Q A M N"
proof -
  let ?rel = "λP. (restrict_to (mulex1 P) (multisets A))"
  from mulex_on P A M N have "(?rel P)++ M N" by (simp add: mulex_on_def)
  then have "(?rel Q)++ M N"
  proof (induct rule: tranclp.induct)
    case (r_into_trancl M N)
    then have "M  multisets A" and "N  multisets A" by auto
    from mulex1_mono [OF * this] and r_into_trancl
      show ?case by auto
  next
    case (trancl_into_trancl L M N)
    then have "M  multisets A" and "N  multisets A" by auto
    from mulex1_mono [OF * this] and trancl_into_trancl
      have "?rel Q M N" by auto
    with (?rel Q)++ L M show ?case by (rule tranclp.trancl_into_trancl)
  qed
  then show ?thesis by (simp add: mulex_on_def)
qed

lemma mult1_reflcl:
  assumes "(M, N)  mult1 R"
  shows "(M, N)  mult1 (R=)"
  using assms by (auto simp: mult1_def)

lemma mulex1_reflclp:
  assumes "mulex1 P M N"
  shows "mulex1 (P==) M N"
  using mulex1_mono [of UNIV P "P==" M N, OF _ _ _ assms]
  by (auto simp: multisets_def)

lemma mulex_on_reflclp:
  assumes "mulex_on P A M N"
  shows "mulex_on (P==) A M N"
  using mulex_on_mono [OF _ assms, of "P=="] by auto                  

lemma surj_on_multisets_mset:
  "Mmultisets A. xslists A. M = mset xs"
proof
  fix M
  assume "M  multisets A"
  then show "xslists A. M = mset xs"
  proof (induct M)
    case empty show ?case by simp
  next
    case (add a M)
    then obtain xs where "xs  lists A" and "M = mset xs" by auto
    then have "add_mset a M = mset (a # xs)" by simp
    moreover have "a # xs  lists A" using xs  lists A and add by auto
    ultimately show ?case by blast
  qed
qed

lemma image_mset_lists [simp]:
  "mset ` lists A = multisets A"
  using surj_on_multisets_mset [of A]
  by auto (metis mem_Collect_eq multisets_def set_mset_mset subsetI)

lemma multisets_UNIV [simp]: "multisets UNIV = UNIV"
  by (metis image_mset_lists lists_UNIV surj_mset)

lemma non_empty_multiset_induct [consumes 1, case_names singleton add]:
  assumes "M  {#}"
    and "x. P {#x#}"
    and "x M. P M  P (add_mset x M)"
  shows "P M"
  using assms by (induct M) auto

lemma mulex_on_all_strict:
  assumes "X  {#}"
  assumes "X  multisets A" and "Y  multisets A"
    and *: "y. y ∈# Y  (x. x ∈# X  P y x)"
  shows "mulex_on P A Y X"
using assms
proof (induction X arbitrary: Y rule: non_empty_multiset_induct)
  case (singleton x)
  then have "mulex1 P Y {#x#}"
    unfolding mulex1_def mult1_def
    by auto
  with singleton show ?case by (auto simp: mulex_on_def)
next
  case (add x M)
  let ?Y = "{# y ∈# Y. x. x ∈# M  P y x #}"
  let ?Z = "Y - ?Y"
  have Y: "Y = ?Z + ?Y" by (subst multiset_eq_iff) auto
  from Y  multisets A have "?Y  multisets A" by (metis multiset_partition union_multisets_iff)
  moreover have "y. y ∈# ?Y  (x. x ∈# M  P y x)" by auto
  moreover have "M  multisets A" using add by auto
  ultimately have "mulex_on P A ?Y M" using add by blast
  moreover have "mulex_on P A ?Z {#x#}"
  proof -
    have "{#x#} = {#} + {#x#}" by simp
    moreover have "?Z = {#} + ?Z" by simp
    moreover have "y. y ∈# ?Z  P y x"
      using add.prems by (auto simp add: in_diff_count split: if_splits)
    ultimately have "mulex1 P ?Z {#x#}" unfolding mulex1_def mult1_def by blast
    moreover have "{#x#}  multisets A" using add.prems by auto
    moreover have "?Z  multisets A"
      using Y  multisets A by (metis diff_union_cancelL multiset_partition union_multisetsD)
    ultimately show ?thesis by (auto simp: mulex_on_def)
  qed
  ultimately have "mulex_on P A (?Y + ?Z) (M + {#x#})" by (rule union_mulex_on_mono)
  then show ?case using Y by (simp add: ac_simps)
qed

text ‹The following lemma shows that the textbook definition (e.g.,
``Term Rewriting and All That'') is the same as the one used below.›
lemma diff_set_Ex_iff:
  "X  {#}  X ⊆# M  N = (M - X) + Y  X  {#}  (Z. M = Z + X  N = Z + Y)"
  by (auto) (metis add_diff_cancel_left' multiset_diff_union_assoc union_commute)

text ‹Show that @{const mulex_on} is equivalent to the textbook definition
of multiset-extension for transitive base orders.›
lemma mulex_on_alt_def:
  assumes trans: "transp_on A P"
  shows "mulex_on P A M N  M  multisets A  N  multisets A  (X Y Z.
    X  {#}  N = Z + X  M = Z + Y  (y. y ∈# Y  (x. x ∈# X  P y x)))"
  (is "?P M N  ?Q M N")
proof
  assume "?P M N" then show "?Q M N"
  proof (induct M N)
    case (base M N)
    then obtain a M0 K where N: "N = M0 + {#a#}"
      and M: "M = M0 + K"
      and *: "b. b ∈# K  P b a"
      and "M  multisets A" and "N  multisets A" by (auto simp: mulex1_def mult1_def)
    moreover then have "{#a#}  multisets A" and "K  multisets A" by auto
    moreover have "{#a#}  {#}" by auto
    moreover have "N = M0 + {#a#}" by fact
    moreover have "M = M0 + K" by fact
    moreover have "y. y ∈# K  (x. x ∈# {#a#}  P y x)" using * by auto
    ultimately show ?case by blast
  next
    case (step L M N)
    then obtain X Y Z
      where "L  multisets A" and "M  multisets A" and "N  multisets A"
      and "X  multisets A" and "Y  multisets A"
      and M: "M = Z + X"
      and L: "L = Z + Y" and "X  {#}"
      and Y: "y. y ∈# Y  (x. x ∈# X  P y x)"
      and "mulex1 P M N"
      by blast
    from mulex1 P M N obtain a M0 K
      where N: "N = add_mset a M0" and M': "M = M0 + K"
      and *: "b. b ∈# K  P b a" unfolding mulex1_def mult1_def by blast
    have L': "L = (M - X) + Y" by (simp add: L M)
    have K: "y. y ∈# K  (x. x ∈# {#a#}  P y x)" using * by auto

    txt ‹The remainder of the proof is adapted from the proof of Lemma 2.5.4. of
    the book ``Term Rewriting and All That.''›
    let ?X = "add_mset a (X - K)"
    let ?Y = "(K - X) + Y"
    
    have "L  multisets A" and "N  multisets A" by fact+
    moreover have "?X  {#}  (Z. N = Z + ?X  L = Z + ?Y)"
    proof -
      have "?X  {#}" by auto
      moreover have "?X ⊆# N"
        using M N M' by (simp add: add.commute [of "{#a#}"])
          (metis Multiset.diff_subset_eq_self add.commute add_diff_cancel_right)
      moreover have "L = (N - ?X) + ?Y"
      proof (rule multiset_eqI)
        fix x :: 'a
        let ?c = "λM. count M x"
        let ?ic = "λx. int (?c x)"
        from ?X ⊆# N have *: "?c {#a#} + ?c (X - K)  ?c N"
          by (auto simp add: subseteq_mset_def split: if_splits)
        from * have **: "?c (X - K)  ?c M0" unfolding N by (auto split: if_splits)
        have "?ic (N - ?X + ?Y) = int (?c N - ?c ?X) + ?ic ?Y" by simp
        also have " = int (?c N - (?c {#a#} + ?c (X - K))) + ?ic (K - X) + ?ic Y" by simp
        also have " = ?ic N - (?ic {#a#} + ?ic (X - K)) + ?ic (K - X) + ?ic Y"
          using of_nat_diff [OF *] by simp
        also have " = (?ic N - ?ic {#a#}) - ?ic (X - K) + ?ic (K - X) + ?ic Y" by simp
        also have " = (?ic N - ?ic {#a#}) + (?ic (K - X) - ?ic (X - K)) + ?ic Y" by simp
        also have " = (?ic N - ?ic {#a#}) + (?ic K - ?ic X) + ?ic Y" by simp
        also have " = (?ic N - ?ic ?X) + ?ic ?Y" by (simp add: N)
        also have " = ?ic L"
          unfolding L' M' N
          using ** by (simp add: algebra_simps)
        finally show "?c L = ?c (N - ?X + ?Y)" by simp
      qed
      ultimately show ?thesis by (metis diff_set_Ex_iff)
    qed
    moreover have "y. y ∈# ?Y  (x. x ∈# ?X  P y x)"
    proof (intro allI impI)
      fix y assume "y ∈# ?Y"
      then have "y ∈# K - X  y ∈# Y" by auto
      then show "x. x ∈# ?X  P y x"
      proof
        assume "y ∈# K - X"
        then have "y ∈# K" by (rule in_diffD)
        with K show ?thesis by auto
      next
        assume "y ∈# Y"
        with Y obtain x where "x ∈# X" and "P y x" by blast
        { assume "x ∈# X - K" with P y x have ?thesis by auto }
        moreover
        { assume "x ∈# K" with * have "P x a" by auto
          moreover have "y  A" using Y  multisets A and y ∈# Y by (auto simp: multisets_def)
          moreover have "a  A" using N  multisets A by (auto simp: N)
          moreover have "x  A" using M  multisets A and x ∈# K by (auto simp: M' multisets_def)
          ultimately have "P y a" using P y x and trans unfolding transp_on_def by blast
          then have ?thesis by force }
        moreover from x ∈# X have "x ∈# X - K  x ∈# K"
          by (auto simp add: in_diff_count not_in_iff)
        ultimately show ?thesis by auto
      qed
    qed
    ultimately show ?case by blast
  qed
next
  assume "?Q M N"
  then obtain X Y Z where "M  multisets A" and "N  multisets A"
    and "X  {#}" and N: "N = Z + X" and M: "M = Z + Y"
    and *: "y. y ∈# Y  (x. x ∈# X  P y x)" by blast
  with mulex_on_all_strict [of X A Y] have "mulex_on P A Y X" by auto
  moreover from N  multisets A have "Z  multisets A" by (auto simp: N)
  ultimately show "?P M N" unfolding M N by (metis mulex_on_union)
qed

end