simplified proof
authornipkow
Wed May 12 15:25:02 2010 +0200 (2010-05-12)
changeset 368676c28c702ed22
parent 36843 ce939b5fd77b
child 36868 b78d3c87fc88
simplified proof
src/HOL/Library/Multiset.thy
     1.1 --- a/src/HOL/Library/Multiset.thy	Tue May 11 21:55:41 2010 -0700
     1.2 +++ b/src/HOL/Library/Multiset.thy	Wed May 12 15:25:02 2010 +0200
     1.3 @@ -330,24 +330,8 @@
     1.4    by (simp add: multiset_eq_conv_count_eq mset_le_def)
     1.5  
     1.6  lemma mset_le_multiset_union_diff_commute:
     1.7 -  assumes "B \<le> A"
     1.8 -  shows "(A::'a multiset) - B + C = A + C - B"
     1.9 -proof -
    1.10 -  from mset_le_exists_conv [of "B" "A"] assms have "\<exists>D. A = B + D" ..
    1.11 -  from this obtain D where "A = B + D" ..
    1.12 -  then show ?thesis
    1.13 -    apply simp
    1.14 -    apply (subst add_commute)
    1.15 -    apply (subst multiset_diff_union_assoc)
    1.16 -    apply simp
    1.17 -    apply (simp add: diff_cancel)
    1.18 -    apply (subst add_assoc)
    1.19 -    apply (subst add_commute [of "B" _])
    1.20 -    apply (subst multiset_diff_union_assoc)
    1.21 -    apply simp
    1.22 -    apply (simp add: diff_cancel)
    1.23 -    done
    1.24 -qed
    1.25 +  "B \<le> A \<Longrightarrow> (A::'a multiset) - B + C = A + C - B"
    1.26 +by (simp add: multiset_eq_conv_count_eq mset_le_def)
    1.27  
    1.28  lemma mset_lessD: "A < B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
    1.29  apply (clarsimp simp: mset_le_def mset_less_def)