# HG changeset patch
# User nipkow
# Date 1473509464 -7200
# Node ID ea7471c921f58c93af5ba5be45ba6f4892dd7f45
# Parent  2ea3725a34bde1aede225264ad7dcac777614c51
more simp

diff -r 2ea3725a34bd -r ea7471c921f5 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Sep 09 15:12:40 2016 +0200
+++ b/src/HOL/Library/Multiset.thy	Sat Sep 10 14:11:04 2016 +0200
@@ -609,9 +609,12 @@
   "add_mset x A \<subset># B \<Longrightarrow> x \<in># B \<and> A \<subset># B"
   by (rule mset_subset_eq_insertD) simp
 
-lemma mset_subset_of_empty: "A \<subset># {#} \<longleftrightarrow> False"
+lemma mset_subset_of_empty[simp]: "A \<subset># {#} \<longleftrightarrow> False"
   by (simp only: subset_mset.not_less_zero)
 
+lemma empty_subset_add_mset[simp]: "{#} <# add_mset x M"
+by(auto intro: subset_mset.gr_zeroI)
+
 lemma empty_le: "{#} \<subseteq># A"
   by (fact subset_mset.zero_le)
 
@@ -631,7 +634,7 @@
   "A - C \<subseteq># B \<longleftrightarrow> A \<subseteq># B + C"
   by (simp add: subseteq_mset_def le_diff_conv)
 
-lemma subset_eq_empty: "M \<subseteq># {#} \<longleftrightarrow> M = {#}"
+lemma subset_eq_empty[simp]: "M \<subseteq># {#} \<longleftrightarrow> M = {#}"
   by auto
 
 lemma multi_psub_of_add_self [simp]: "A \<subset># add_mset x A"
@@ -682,7 +685,7 @@
   "M - N #\<inter> M = M - N"
   by (simp add: multiset_eq_iff min_def)
 
-lemma multiset_inter_single: "a \<noteq> b \<Longrightarrow> {#a#} #\<inter> {#b#} = {#}"
+lemma multiset_inter_single[simp]: "a \<noteq> b \<Longrightarrow> {#a#} #\<inter> {#b#} = {#}"
   by (rule multiset_eqI) auto
 
 lemma multiset_union_diff_commute:
@@ -724,7 +727,7 @@
   qed
 qed
 
-lemma add_mset_inter_add_mset:
+lemma add_mset_inter_add_mset[simp]:
   "add_mset a A #\<inter> add_mset a B = add_mset a (A #\<inter> B)"
   by (metis add_mset_add_single add_mset_diff_bothsides diff_subset_eq_self multiset_inter_def
       subset_mset.diff_add_assoc2)
@@ -739,10 +742,10 @@
   "{#} = A #\<inter> add_mset b B \<longleftrightarrow> b \<notin># A \<and> {#} = A #\<inter> B"
   by (auto simp: disjunct_not_in)
 
-lemma empty_inter: "{#} #\<inter> M = {#}"
+lemma empty_inter[simp]: "{#} #\<inter> M = {#}"
   by (simp add: multiset_eq_iff)
 
-lemma inter_empty: "M #\<inter> {#} = {#}"
+lemma inter_empty[simp]: "M #\<inter> {#} = {#}"
   by (simp add: multiset_eq_iff)
 
 lemma inter_add_left1: "\<not> x \<in># N \<Longrightarrow> (add_mset x M) #\<inter> N = M #\<inter> N"