# HG changeset patch
# User nipkow
# Date 1273670702 -7200
# Node ID 6c28c702ed22039e1fc8afc6b2abb6ac9361cfda
# Parent  ce939b5fd77b056f755597635fa455cba72b0a17
simplified proof

diff -r ce939b5fd77b -r 6c28c702ed22 src/HOL/Library/Multiset.thy
--- 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)