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 "∀M∈multisets 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:
  "∀M∈multisets A. ∃xs∈lists A. M = mset xs"
proof
  fix M
  assume "M ∈ multisets A"
  then show "∃xs∈lists 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