# HG changeset patch
# User blanchet
# Date 1487941190 -3600
# Node ID 805d0a9a4e3769f5a34750386bc34d65e72e8b6a
# Parent  f6aea1a500ce7d6133583fa1809be408aa57a271
added multiset lemma

diff -r f6aea1a500ce -r 805d0a9a4e37 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Feb 24 13:59:49 2017 +0100
+++ b/src/HOL/Library/Multiset.thy	Fri Feb 24 13:59:50 2017 +0100
@@ -6,7 +6,7 @@
     Author:     Mathias Fleury, MPII
 *)
 
-section \<open>(Finite) multisets\<close>
+section \<open>(Finite) Multisets\<close>
 
 theory Multiset
 imports Cancellation
@@ -1688,6 +1688,10 @@
 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)
 
+lemma image_mset_subset_mono: "M \<subset># N \<Longrightarrow> image_mset f M \<subset># image_mset f N"
+  by (metis (no_types) Diff_eq_empty_iff_mset image_mset_Diff image_mset_is_empty_iff
+    image_mset_subseteq_mono subset_mset.less_le_not_le)
+
 syntax (ASCII)
   "_comprehension_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"  ("({#_/. _ :# _#})")
 syntax