# HG changeset patch
# User haftmann
# Date 1619171414 0
# Node ID 5c4a09c4bc9c48f7fd7d6ff825ffa9e906b2a5d0
# Parent  e60333aa18cafe80545dc9b2c19ad746177c15b6
collecting more lemmas concerning multisets

diff -r e60333aa18ca -r 5c4a09c4bc9c src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Tue Apr 20 22:53:24 2021 +0200
+++ b/src/HOL/Fun.thy	Fri Apr 23 09:50:14 2021 +0000
@@ -675,6 +675,23 @@
   shows "bij_betw (\<lambda>x. if x \<in> A then f x else g x) (A \<union> B) (C \<union> D)"
   using assms by (auto simp: inj_on_disjoint_Un bij_betw_def)
 
+lemma involuntory_imp_bij:
+  \<open>bij f\<close> if \<open>\<And>x. f (f x) = x\<close>
+proof (rule bijI)
+  from that show \<open>surj f\<close>
+    by (rule surjI)
+  show \<open>inj f\<close>
+  proof (rule injI)
+    fix x y
+    assume \<open>f x = f y\<close>
+    then have \<open>f (f x) = f (f y)\<close>
+      by simp
+    then show \<open>x = y\<close>
+      by (simp add: that)
+  qed
+qed
+
+
 subsubsection \<open>Important examples\<close>
 
 context cancel_semigroup_add
diff -r e60333aa18ca -r 5c4a09c4bc9c src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Tue Apr 20 22:53:24 2021 +0200
+++ b/src/HOL/Library/Multiset.thy	Fri Apr 23 09:50:14 2021 +0000
@@ -1713,7 +1713,8 @@
   finally show ?thesis by simp
 qed
 
-lemma count_image_mset: "count (image_mset f A) x = (\<Sum>y\<in>f -` {x} \<inter> set_mset A. count A y)"
+lemma count_image_mset:
+  \<open>count (image_mset f A) x = (\<Sum>y\<in>f -` {x} \<inter> set_mset A. count A y)\<close>
 proof (induction A)
   case empty
   then show ?case by simp
@@ -1725,6 +1726,10 @@
     by (auto simp: sum.distrib intro!: sum.mono_neutral_left)
 qed
 
+lemma count_image_mset':
+  \<open>count (image_mset f X) y = (\<Sum>x | x \<in># X \<and> y = f x. count X x)\<close>
+  by (auto simp add: count_image_mset simp flip: singleton_conv2 simp add: Collect_conj_eq ac_simps)
+
 lemma image_mset_subseteq_mono: "A \<subseteq># B \<Longrightarrow> image_mset f A \<subseteq># image_mset f B"
   by (metis image_mset_union subset_mset.le_iff_add)
 
@@ -3789,6 +3794,10 @@
 lemma rel_mset_size: "rel_mset R M N \<Longrightarrow> size M = size N"
   unfolding multiset.rel_compp_Grp Grp_def by auto
 
+lemma rel_mset_Zero_iff [simp]:
+  shows "rel_mset rel {#} Y \<longleftrightarrow> Y = {#}" and "rel_mset rel X {#} \<longleftrightarrow> X = {#}"
+  by (auto simp add: rel_mset_Zero dest: rel_mset_size)
+
 lemma multiset_induct2[case_names empty addL addR]:
   assumes empty: "P {#} {#}"
     and addL: "\<And>a M N. P M N \<Longrightarrow> P (add_mset a M) N"