more multiset lemmas

--- a/src/HOL/Finite_Set.thy	Tue Feb 27 13:46:42 2024 +0100
+++ b/src/HOL/Finite_Set.thy	Wed Mar 06 10:39:45 2024 +0100
@@ -1032,6 +1032,22 @@
 
 text \<open>Other properties of \<^const>\<open>fold\<close>:\<close>
 
+lemma finite_set_fold_single [simp]: "Finite_Set.fold f z {x} = f x z"
+proof -
+  have "fold_graph f z {x} (f x z)"
+    by (auto intro: fold_graph.intros)
+  moreover
+  {
+    fix X y
+    have "fold_graph f z X y \<Longrightarrow> (X = {} \<longrightarrow> y = z) \<and> (X = {x} \<longrightarrow> y = f x z)"
+      by (induct rule: fold_graph.induct) auto
+  }
+  ultimately have "(THE y. fold_graph f z {x} y) = f x z"
+    by blast
+  thus ?thesis
+    by (simp add: Finite_Set.fold_def)
+qed
+
 lemma fold_graph_image:
   assumes "inj_on g A"
   shows "fold_graph f z (g ` A) = fold_graph (f \<circ> g) z A"

--- a/src/HOL/Library/Multiset.thy	Tue Feb 27 13:46:42 2024 +0100
+++ b/src/HOL/Library/Multiset.thy	Wed Mar 06 10:39:45 2024 +0100
@@ -243,6 +243,9 @@
   with that show ?thesis by blast
 qed
 
+lemma count_gt_imp_in_mset: "count M x > n \<Longrightarrow> x \<in># M"
+  using count_greater_zero_iff by fastforce
+
 
 subsubsection \<open>Union\<close>
 
@@ -393,6 +396,11 @@
 abbreviation Max_mset :: "'a::linorder multiset \<Rightarrow> 'a" where
 "Max_mset m \<equiv> Max (set_mset m)"
 
+lemma
+  Min_in_mset: "M \<noteq> {#} \<Longrightarrow> Min_mset M \<in># M" and
+  Max_in_mset: "M \<noteq> {#} \<Longrightarrow> Max_mset M \<in># M"
+  by simp+
+
 
 subsubsection \<open>Equality of multisets\<close>
 
@@ -684,6 +692,12 @@
     using A by (simp add: mset_subset_eq_add_mset_cancel)
 qed simp
 
+lemma nonempty_subseteq_mset_eq_single: "M \<noteq> {#} \<Longrightarrow> M \<subseteq># {#x#} \<Longrightarrow> M = {#x#}"
+  by (cases M) (metis single_is_union subset_mset.less_eqE)
+
+lemma nonempty_subseteq_mset_iff_single: "(M \<noteq> {#} \<and> M \<subseteq># {#x#} \<and> P) \<longleftrightarrow> M = {#x#} \<and> P"
+  by (cases M) (metis empty_not_add_mset nonempty_subseteq_mset_eq_single subset_mset.order_refl)
+
 
 subsubsection \<open>Intersection and bounded union\<close>
 
@@ -1374,6 +1388,9 @@
   unfolding \<open>M = M'\<close>
   using assms by (auto intro: filter_mset_cong0)
 
+lemma filter_eq_replicate_mset: "{#y \<in># D. y = x#} = replicate_mset (count D x) x"
+  by (induct D) (simp add: multiset_eqI)
+
 
 subsubsection \<open>Size\<close>
 
@@ -1480,6 +1497,9 @@
   "M \<subseteq># M' \<Longrightarrow> size (M' - M) = size M' - size(M::'a multiset)"
 by (metis add_diff_cancel_left' size_union mset_subset_eq_exists_conv)
 
+lemma size_lt_imp_ex_count_lt: "size M < size N \<Longrightarrow> \<exists>x \<in># N. count M x < count N x"
+  by (metis count_eq_zero_iff leD not_le_imp_less not_less_zero size_mset_mono subseteq_mset_def)
+
 
 subsection \<open>Induction and case splits\<close>
 
@@ -1644,6 +1664,9 @@
 lemma fold_mset_empty [simp]: "fold_mset f s {#} = s"
   by (simp add: fold_mset_def)
 
+lemma fold_mset_single [simp]: "fold_mset f s {#x#} = f x s"
+  by (simp add: fold_mset_def)
+
 context comp_fun_commute
 begin
 
@@ -1674,9 +1697,6 @@
   qed
 qed
 
-corollary fold_mset_single: "fold_mset f s {#x#} = f x s"
-  by simp
-
 lemma fold_mset_fun_left_comm: "f x (fold_mset f s M) = fold_mset f (f x s) M"
   by (induct M) (simp_all add: fun_left_comm)
 
@@ -1849,7 +1869,6 @@
   "image_mset f (filter_mset (\<lambda>x. P (f x)) M) = filter_mset P (image_mset f M)"
   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)
@@ -2278,7 +2297,7 @@
 qed
 
 
-subsection \<open>More properties of the replicate and repeat operations\<close>
+subsection \<open>More properties of the replicate, repeat, and image operations\<close>
 
 lemma in_replicate_mset[simp]: "x \<in># replicate_mset n y \<longleftrightarrow> n > 0 \<and> x = y"
   unfolding replicate_mset_def by (induct n) auto
@@ -2292,9 +2311,6 @@
 lemma count_le_replicate_mset_subset_eq: "n \<le> count M x \<longleftrightarrow> replicate_mset n x \<subseteq># M"
   by (auto simp add: mset_subset_eqI) (metis count_replicate_mset subseteq_mset_def)
 
-lemma filter_eq_replicate_mset: "{#y \<in># D. y = x#} = replicate_mset (count D x) x"
-  by (induct D) simp_all
-
 lemma replicate_count_mset_eq_filter_eq: "replicate (count (mset xs) k) k = filter (HOL.eq k) xs"
   by (induct xs) auto
 
@@ -2354,6 +2370,195 @@
   then show thesis using A ..
 qed
 
+lemma count_image_mset_lt_imp_lt_raw:
+  assumes
+    "finite A" and
+    "A = set_mset M \<union> set_mset N" and
+    "count (image_mset f M) b < count (image_mset f N) b"
+  shows "\<exists>x. f x = b \<and> count M x < count N x"
+  using assms
+proof (induct A arbitrary: M N b rule: finite_induct)
+  case (insert x F)
+  note fin = this(1) and x_ni_f = this(2) and ih = this(3) and x_f_eq_m_n = this(4) and
+    cnt_b = this(5)
+
+  let ?Ma = "{#y \<in># M. y \<noteq> x#}"
+  let ?Mb = "{#y \<in># M. y = x#}"
+  let ?Na = "{#y \<in># N. y \<noteq> x#}"
+  let ?Nb = "{#y \<in># N. y = x#}"
+
+  have m_part: "M = ?Mb + ?Ma" and n_part: "N = ?Nb + ?Na"
+    using multiset_partition by blast+
+
+  have f_eq_ma_na: "F = set_mset ?Ma \<union> set_mset ?Na"
+    using x_f_eq_m_n x_ni_f by auto
+
+  show ?case
+  proof (cases "count (image_mset f ?Ma) b < count (image_mset f ?Na) b")
+    case cnt_ba: True
+    obtain xa where "f xa = b" and "count ?Ma xa < count ?Na xa"
+      using ih[OF f_eq_ma_na cnt_ba] by blast
+    thus ?thesis
+      by (metis count_filter_mset not_less0)
+  next
+    case cnt_ba: False
+    have fx_eq_b: "f x = b"
+      using cnt_b cnt_ba
+      by (subst (asm) m_part, subst (asm) n_part,
+          auto simp: filter_eq_replicate_mset split: if_splits)
+    moreover have "count M x < count N x"
+      using cnt_b cnt_ba
+      by (subst (asm) m_part, subst (asm) n_part,
+          auto simp: filter_eq_replicate_mset split: if_splits)
+    ultimately show ?thesis
+      by blast
+  qed
+qed auto
+
+lemma count_image_mset_lt_imp_lt:
+  assumes cnt_b: "count (image_mset f M) b < count (image_mset f N) b"
+  shows "\<exists>x. f x = b \<and> count M x < count N x"
+  by (rule count_image_mset_lt_imp_lt_raw[of "set_mset M \<union> set_mset N", OF _ refl cnt_b]) auto
+
+lemma count_image_mset_le_imp_lt_raw:
+  assumes
+    "finite A" and
+    "A = set_mset M \<union> set_mset N" and
+    "count (image_mset f M) (f a) + count N a < count (image_mset f N) (f a) + count M a"
+  shows "\<exists>b. f b = f a \<and> count M b < count N b"
+  using assms
+proof (induct A arbitrary: M N rule: finite_induct)
+  case (insert x F)
+  note fin = this(1) and x_ni_f = this(2) and ih = this(3) and x_f_eq_m_n = this(4) and
+    cnt_lt = this(5)
+
+  let ?Ma = "{#y \<in># M. y \<noteq> x#}"
+  let ?Mb = "{#y \<in># M. y = x#}"
+  let ?Na = "{#y \<in># N. y \<noteq> x#}"
+  let ?Nb = "{#y \<in># N. y = x#}"
+
+  have m_part: "M = ?Mb + ?Ma" and n_part: "N = ?Nb + ?Na"
+    using multiset_partition by blast+
+
+  have f_eq_ma_na: "F = set_mset ?Ma \<union> set_mset ?Na"
+    using x_f_eq_m_n x_ni_f by auto
+
+  show ?case
+  proof (cases "f x = f a")
+    case fx_ne_fa: False
+
+    have cnt_fma_fa: "count (image_mset f ?Ma) (f a) = count (image_mset f M) (f a)"
+      using fx_ne_fa by (subst (2) m_part) (auto simp: filter_eq_replicate_mset)
+    have cnt_fna_fa: "count (image_mset f ?Na) (f a) = count (image_mset f N) (f a)"
+      using fx_ne_fa by (subst (2) n_part) (auto simp: filter_eq_replicate_mset)
+    have cnt_ma_a: "count ?Ma a = count M a"
+      using fx_ne_fa by (subst (2) m_part) (auto simp: filter_eq_replicate_mset)
+    have cnt_na_a: "count ?Na a = count N a"
+      using fx_ne_fa by (subst (2) n_part) (auto simp: filter_eq_replicate_mset)
+
+    obtain b where fb_eq_fa: "f b = f a" and cnt_b: "count ?Ma b < count ?Na b"
+      using ih[OF f_eq_ma_na] cnt_lt unfolding cnt_fma_fa cnt_fna_fa cnt_ma_a cnt_na_a by blast
+    have fx_ne_fb: "f x \<noteq> f b"
+      using fb_eq_fa fx_ne_fa by simp
+
+    have cnt_ma_b: "count ?Ma b = count M b"
+      using fx_ne_fb by (subst (2) m_part) auto
+    have cnt_na_b: "count ?Na b = count N b"
+      using fx_ne_fb by (subst (2) n_part) auto
+
+    show ?thesis
+      using fb_eq_fa cnt_b unfolding cnt_ma_b cnt_na_b by blast
+  next
+    case fx_eq_fa: True
+    show ?thesis
+    proof (cases "x = a")
+      case x_eq_a: True
+      have "count (image_mset f ?Ma) (f a) + count ?Na a
+        < count (image_mset f ?Na) (f a) + count ?Ma a"
+        using cnt_lt x_eq_a by (subst (asm) (1 2) m_part, subst (asm) (1 2) n_part,
+            auto simp: filter_eq_replicate_mset)
+      thus ?thesis
+        using ih[OF f_eq_ma_na] by (metis count_filter_mset nat_neq_iff)
+    next
+      case x_ne_a: False
+      show ?thesis
+      proof (cases "count M x < count N x")
+        case True
+        thus ?thesis
+          using fx_eq_fa by blast
+     next
+        case False
+        hence cnt_x: "count M x \<ge> count N x"
+          by fastforce
+        have "count M x + count (image_mset f ?Ma) (f a) + count ?Na a
+          < count N x + count (image_mset f ?Na) (f a) + count ?Ma a"
+          using cnt_lt x_ne_a fx_eq_fa by (subst (asm) (1 2) m_part, subst (asm) (1 2) n_part,
+            auto simp: filter_eq_replicate_mset)
+        hence "count (image_mset f ?Ma) (f a) + count ?Na a
+          < count (image_mset f ?Na) (f a) + count ?Ma a"
+          using cnt_x by linarith
+        thus ?thesis
+          using ih[OF f_eq_ma_na] by (metis count_filter_mset nat_neq_iff)
+      qed
+    qed
+  qed
+qed auto
+
+lemma count_image_mset_le_imp_lt:
+  assumes
+    "count (image_mset f M) (f a) \<le> count (image_mset f N) (f a)" and
+    "count M a > count N a"
+  shows "\<exists>b. f b = f a \<and> count M b < count N b"
+  using assms by (auto intro: count_image_mset_le_imp_lt_raw[of "set_mset M \<union> set_mset N"])
+
+lemma size_filter_unsat_elem:
+  assumes "x \<in># M" and "\<not> P x"
+  shows "size {#x \<in># M. P x#} < size M"
+proof -
+  have "size (filter_mset P M) \<noteq> size M"
+    using assms by (metis add.right_neutral add_diff_cancel_left' count_filter_mset mem_Collect_eq
+      multiset_partition nonempty_has_size set_mset_def size_union)
+  then show ?thesis
+    by (meson leD nat_neq_iff size_filter_mset_lesseq)
+qed
+
+lemma size_filter_ne_elem: "x \<in># M \<Longrightarrow> size {#y \<in># M. y \<noteq> x#} < size M"
+  by (simp add: size_filter_unsat_elem[of x M "\<lambda>y. y \<noteq> x"])
+
+lemma size_eq_ex_count_lt:
+  assumes
+    sz_m_eq_n: "size M = size N" and
+    m_eq_n: "M \<noteq> N"
+  shows "\<exists>x. count M x < count N x"
+proof -
+  obtain x where "count M x \<noteq> count N x"
+    using m_eq_n by (meson multiset_eqI)
+  moreover
+  {
+    assume "count M x < count N x"
+    hence ?thesis
+      by blast
+  }
+  moreover
+  {
+    assume cnt_x: "count M x > count N x"
+
+    have "size {#y \<in># M. y = x#} + size {#y \<in># M. y \<noteq> x#} =
+      size {#y \<in># N. y = x#} + size {#y \<in># N. y \<noteq> x#}"
+      using sz_m_eq_n multiset_partition by (metis size_union)
+    hence sz_m_minus_x: "size {#y \<in># M. y \<noteq> x#} < size {#y \<in># N. y \<noteq> x#}"
+      using cnt_x by (simp add: filter_eq_replicate_mset)
+    then obtain y where "count {#y \<in># M. y \<noteq> x#} y < count {#y \<in># N. y \<noteq> x#} y"
+      using size_lt_imp_ex_count_lt[OF sz_m_minus_x] by blast
+    hence "count M y < count N y"
+      by (metis count_filter_mset less_asym)
+    hence ?thesis
+      by blast
+  }
+  ultimately show ?thesis
+    by fastforce
+qed
+
 
 subsection \<open>Big operators\<close>
 
@@ -2571,7 +2776,6 @@
 lemma Union_image_single_mset[simp]: "\<Sum>\<^sub># (image_mset (\<lambda>x. {#x#}) m) = m"
 by(induction m) auto
 
-
 context comm_monoid_mult
 begin
 

--- a/src/HOL/Library/Multiset_Order.thy	Tue Feb 27 13:46:42 2024 +0100
+++ b/src/HOL/Library/Multiset_Order.thy	Wed Mar 06 10:39:45 2024 +0100
@@ -853,4 +853,63 @@
 
 end
 
+lemma add_mset_lt_left_lt: "a < b \<Longrightarrow> add_mset a A < add_mset b A"
+  by fastforce
+
+lemma add_mset_le_left_le: "a \<le> b \<Longrightarrow> add_mset a A \<le> add_mset b A" for a :: "'a :: linorder"
+  by fastforce
+
+lemma add_mset_lt_right_lt: "A < B \<Longrightarrow> add_mset a A < add_mset a B"
+  by fastforce
+
+lemma add_mset_le_right_le: "A \<le> B \<Longrightarrow> add_mset a A \<le> add_mset a B"
+  by fastforce
+
+lemma add_mset_lt_lt_lt:
+  assumes a_lt_b: "a < b" and A_le_B: "A < B"
+  shows "add_mset a A < add_mset b B"
+  by (rule less_trans[OF add_mset_lt_left_lt[OF a_lt_b] add_mset_lt_right_lt[OF A_le_B]])
+
+lemma add_mset_lt_lt_le: "a < b \<Longrightarrow> A \<le> B \<Longrightarrow> add_mset a A < add_mset b B"
+  using add_mset_lt_lt_lt le_neq_trans by fastforce
+
+lemma add_mset_lt_le_lt: "a \<le> b \<Longrightarrow> A < B \<Longrightarrow> add_mset a A < add_mset b B" for a :: "'a :: linorder"
+  using add_mset_lt_lt_lt by (metis add_mset_lt_right_lt le_less)
+
+lemma add_mset_le_le_le:
+  fixes a :: "'a :: linorder"
+  assumes a_le_b: "a \<le> b" and A_le_B: "A \<le> B"
+  shows "add_mset a A \<le> add_mset b B"
+  by (rule order.trans[OF add_mset_le_left_le[OF a_le_b] add_mset_le_right_le[OF A_le_B]])
+
+lemma Max_lt_imp_lt_mset:
+  assumes n_nemp: "N \<noteq> {#}" and max: "Max_mset M < Max_mset N" (is "?max_M < ?max_N")
+  shows "M < N"
+proof (cases "M = {#}")
+  case m_nemp: False
+
+  have max_n_in_n: "?max_N \<in># N"
+    using n_nemp by simp
+  have max_n_nin_m: "?max_N \<notin># M"
+    using max Max_ge leD by auto
+
+  have "M \<noteq> N"
+    using max by auto
+  moreover
+  {
+    fix y
+    assume "count N y < count M y"
+    hence "y \<in># M"
+      by (simp add: count_inI)
+    hence "?max_M \<ge> y"
+      by simp
+    hence "?max_N > y"
+      using max by auto
+    hence "\<exists>x > y. count M x < count N x"
+      using max_n_nin_m max_n_in_n count_inI by force
+  }
+  ultimately show ?thesis
+    unfolding less_multiset\<^sub>H\<^sub>O by blast
+qed (auto simp: n_nemp)
+
 end