# HG changeset patch
# User desharna
# Date 1655143320 -7200
# Node ID aeb797356de06ce8242b8d06957261404fe05899
# Parent  5340239ff468c5679b779327444214c83c27a0cd
added lemmas image_mset_eq_{image_mset_plus,plus,plus_image_mset}D, and multp_image_mset_image_msetD

diff -r 5340239ff468 -r aeb797356de0 NEWS
--- a/NEWS	Mon Jun 13 11:48:46 2022 +0200
+++ b/NEWS	Mon Jun 13 20:02:00 2022 +0200
@@ -88,7 +88,11 @@
       Multiset.bex_least_element
       filter_mset_cong
       filter_mset_cong0
+      image_mset_eq_image_mset_plusD
+      image_mset_eq_plusD
+      image_mset_eq_plus_image_msetD
       image_mset_filter_mset_swap
+      multp_image_mset_image_msetD
 
 * Sledgehammer:
   - Redesigned multithreading to provide more fine grained prover schedules.
diff -r 5340239ff468 -r aeb797356de0 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Jun 13 11:48:46 2022 +0200
+++ b/src/HOL/Library/Multiset.thy	Mon Jun 13 20:02:00 2022 +0200
@@ -1878,6 +1878,75 @@
   by (induction M rule: multiset_induct) simp_all
 
 
+lemma image_mset_eq_plusD:
+  "image_mset f A = B + C \<Longrightarrow> \<exists>B' C'. A = B' + C' \<and> B = image_mset f B' \<and> C = image_mset f C'"
+proof (induction A arbitrary: B C)
+  case empty
+  thus ?case by simp
+next
+  case (add x A)
+  show ?case
+  proof (cases "f x \<in># B")
+    case True
+    with add.prems have "image_mset f A = (B - {#f x#}) + C"
+      by (metis add_mset_remove_trivial image_mset_add_mset mset_subset_eq_single
+          subset_mset.add_diff_assoc2)
+    thus ?thesis
+      using add.IH add.prems by force
+  next
+    case False
+    with add.prems have "image_mset f A = B + (C - {#f x#})"
+      by (metis diff_single_eq_union diff_union_single_conv image_mset_add_mset union_iff
+          union_single_eq_member)
+    then show ?thesis
+      using add.IH add.prems by force
+  qed
+qed
+
+lemma image_mset_eq_image_mset_plusD:
+  assumes "image_mset f A = image_mset f B + C" and inj_f: "inj_on f (set_mset A \<union> set_mset B)"
+  shows "\<exists>C'. A = B + C' \<and> C = image_mset f C'"
+  using assms
+proof (induction A arbitrary: B C)
+  case empty
+  thus ?case by simp
+next
+  case (add x A)
+  show ?case
+  proof (cases "x \<in># B")
+    case True
+    with add.prems have "image_mset f A = image_mset f (B - {#x#}) + C"
+      by (smt (verit, del_insts) add.left_commute add_cancel_right_left diff_union_cancelL
+          diff_union_single_conv image_mset_union union_mset_add_mset_left
+          union_mset_add_mset_right)
+    with add.IH have "\<exists>M3'. A = B - {#x#} + M3' \<and> image_mset f M3' = C"
+      by (smt (verit, del_insts) True Un_insert_left Un_insert_right add.prems(2) inj_on_insert
+          insert_DiffM set_mset_add_mset_insert)
+    with True show ?thesis
+      by auto
+  next
+    case False
+    with add.prems(2) have "f x \<notin># image_mset f B"
+      by auto
+    with add.prems(1) have "image_mset f A = image_mset f B + (C - {#f x#})"
+      by (metis (no_types, lifting) diff_union_single_conv image_eqI image_mset_Diff
+          image_mset_single mset_subset_eq_single set_image_mset union_iff union_single_eq_diff
+          union_single_eq_member)
+    with add.prems(2) add.IH have "\<exists>M3'. A = B + M3' \<and> C - {#f x#} = image_mset f M3'"
+      by auto
+    then show ?thesis
+      by (metis add.prems(1) add_diff_cancel_left' image_mset_Diff mset_subset_eq_add_left
+          union_mset_add_mset_right)
+  qed
+qed
+
+lemma image_mset_eq_plus_image_msetD:
+  "image_mset f A = B + image_mset f C \<Longrightarrow> inj_on f (set_mset A \<union> set_mset C) \<Longrightarrow>
+  \<exists>B'. A = B' + C \<and> B = image_mset f B'"
+  unfolding add.commute[of B] add.commute[of _ C]
+  by (rule image_mset_eq_image_mset_plusD; assumption)
+
+
 subsection \<open>Further conversions\<close>
 
 primrec mset :: "'a list \<Rightarrow> 'a multiset" where
@@ -3120,6 +3189,50 @@
 lemmas subset_implies_multp = subset_implies_mult[of _ _ "{(x, y). r x y}" for r, folded multp_def]
 
 
+subsubsection \<open>Monotonicity\<close>
+
+lemma multp_image_mset_image_msetD:
+  assumes
+    "multp R (image_mset f A) (image_mset f B)" and
+    "transp R" and
+    inj_on_f: "inj_on f (set_mset A \<union> set_mset B)"
+  shows "multp (\<lambda>x y. R (f x) (f y)) A B"
+proof -
+  from assms(1,2) obtain I J K where
+    f_B_eq: "image_mset f B = I + J" and
+    f_A_eq: "image_mset f A = I + K" and
+    J_neq_mempty: "J \<noteq> {#}" and
+    ball_K_less: "\<forall>k\<in>#K. \<exists>x\<in>#J. R k x"
+    by (auto dest: multp_implies_one_step)
+
+  from f_B_eq obtain I' J' where
+    B_def: "B = I' + J'" and I_def: "I = image_mset f I'" and J_def: "J = image_mset f J'"
+    using image_mset_eq_plusD by blast
+
+  from inj_on_f have inj_on_f': "inj_on f (set_mset A \<union> set_mset I')"
+    by (rule inj_on_subset) (auto simp add: B_def)
+
+  from f_A_eq obtain K' where
+    A_def: "A = I' + K'" and K_def: "K = image_mset f K'"
+    by (auto simp: I_def dest: image_mset_eq_image_mset_plusD[OF _ inj_on_f'])
+
+  show ?thesis
+    unfolding A_def B_def
+  proof (intro one_step_implies_multp ballI)
+    from J_neq_mempty show "J' \<noteq> {#}"
+      by (simp add: J_def)
+  next
+    fix k assume "k \<in># K'"
+    with ball_K_less obtain j' where "j' \<in># J" and "R (f k) j'"
+      using K_def by auto
+    moreover then obtain j where "j \<in># J'" and "f j = j'"
+      using J_def by auto
+    ultimately show "\<exists>j\<in>#J'. R (f k) (f j)"
+      by blast
+  qed
+qed
+
+
 subsubsection \<open>The multiset extension is cancellative for multiset union\<close>
 
 lemma mult_cancel: