author nipkow Wed, 12 May 2010 15:25:02 +0200 changeset 36867 6c28c702ed22 parent 36843 ce939b5fd77b child 36868 b78d3c87fc88
simplified proof
```--- a/src/HOL/Library/Multiset.thy	Tue May 11 21:55:41 2010 -0700
+++ b/src/HOL/Library/Multiset.thy	Wed May 12 15:25:02 2010 +0200
@@ -330,24 +330,8 @@
by (simp add: multiset_eq_conv_count_eq mset_le_def)

lemma mset_le_multiset_union_diff_commute:
-  assumes "B \<le> A"
-  shows "(A::'a multiset) - B + C = A + C - B"
-proof -
-  from mset_le_exists_conv [of "B" "A"] assms have "\<exists>D. A = B + D" ..
-  from this obtain D where "A = B + D" ..
-  then show ?thesis
-    apply simp
-    apply (subst add_commute)
-    apply (subst multiset_diff_union_assoc)
-    apply simp
-    apply (simp add: diff_cancel)
-    apply (subst add_assoc)
-    apply (subst add_commute [of "B" _])
-    apply (subst multiset_diff_union_assoc)
-    apply simp
-    apply (simp add: diff_cancel)
-    done
-qed
+  "B \<le> A \<Longrightarrow> (A::'a multiset) - B + C = A + C - B"
+by (simp add: multiset_eq_conv_count_eq mset_le_def)

lemma mset_lessD: "A < B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
apply (clarsimp simp: mset_le_def mset_less_def)```