section ‹Multiset Extension of Orders (as Binary Predicates)›
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 (mulex_on P A) B"
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 P A"
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