src/HOL/Library/Multiset.thy
changeset 52289 83ce5d2841e7
parent 51623 1194b438426a
child 54295 45a5523d4a63
     1.1 --- a/src/HOL/Library/Multiset.thy	Sun Jun 02 10:57:21 2013 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Sun Jun 02 20:44:55 2013 +0200
     1.3 @@ -137,17 +137,25 @@
     1.4    by (simp add: minus_multiset.rep_eq)
     1.5  
     1.6  lemma diff_empty [simp]: "M - {#} = M \<and> {#} - M = {#}"
     1.7 -by(simp add: multiset_eq_iff)
     1.8 +  by rule (fact Groups.diff_zero, fact Groups.zero_diff)
     1.9  
    1.10  lemma diff_cancel[simp]: "A - A = {#}"
    1.11 -by (rule multiset_eqI) simp
    1.12 +  by (fact Groups.diff_cancel)
    1.13  
    1.14  lemma diff_union_cancelR [simp]: "M + N - N = (M::'a multiset)"
    1.15 -by(simp add: multiset_eq_iff)
    1.16 +  by (fact add_diff_cancel_right')
    1.17  
    1.18  lemma diff_union_cancelL [simp]: "N + M - N = (M::'a multiset)"
    1.19 -by(simp add: multiset_eq_iff)
    1.20 +  by (fact add_diff_cancel_left')
    1.21  
    1.22 +lemma diff_right_commute:
    1.23 +  "(M::'a multiset) - N - Q = M - Q - N"
    1.24 +  by (fact diff_right_commute)
    1.25 +
    1.26 +lemma diff_add:
    1.27 +  "(M::'a multiset) - (N + Q) = M - N - Q"
    1.28 +  by (rule sym) (fact diff_diff_add)
    1.29 +  
    1.30  lemma insert_DiffM:
    1.31    "x \<in># M \<Longrightarrow> {#x#} + (M - {#x#}) = M"
    1.32    by (clarsimp simp: multiset_eq_iff)
    1.33 @@ -156,14 +164,6 @@
    1.34    "x \<in># M \<Longrightarrow> M - {#x#} + {#x#} = M"
    1.35    by (clarsimp simp: multiset_eq_iff)
    1.36  
    1.37 -lemma diff_right_commute:
    1.38 -  "(M::'a multiset) - N - Q = M - Q - N"
    1.39 -  by (auto simp add: multiset_eq_iff)
    1.40 -
    1.41 -lemma diff_add:
    1.42 -  "(M::'a multiset) - (N + Q) = M - N - Q"
    1.43 -by (simp add: multiset_eq_iff)
    1.44 -
    1.45  lemma diff_union_swap:
    1.46    "a \<noteq> b \<Longrightarrow> M - {#a#} + {#b#} = M + {#b#} - {#a#}"
    1.47    by (auto simp add: multiset_eq_iff)
    1.48 @@ -289,6 +289,9 @@
    1.49  apply (auto intro: multiset_eq_iff [THEN iffD2])
    1.50  done
    1.51  
    1.52 +instance multiset :: (type) ordered_cancel_comm_monoid_diff
    1.53 +  by default (simp, fact mset_le_exists_conv)
    1.54 +
    1.55  lemma mset_le_mono_add_right_cancel [simp]:
    1.56    "(A::'a multiset) + C \<le> B + C \<longleftrightarrow> A \<le> B"
    1.57    by (fact add_le_cancel_right)