equal
deleted
inserted
replaced
160 "(M::'a multiset) - N - Q = M - Q - N" |
160 "(M::'a multiset) - N - Q = M - Q - N" |
161 by (auto simp add: multiset_eq_iff) |
161 by (auto simp add: multiset_eq_iff) |
162 |
162 |
163 lemma diff_add: |
163 lemma diff_add: |
164 "(M::'a multiset) - (N + Q) = M - N - Q" |
164 "(M::'a multiset) - (N + Q) = M - N - Q" |
165 find_theorems solves |
|
166 by (simp add: multiset_eq_iff) |
165 by (simp add: multiset_eq_iff) |
167 |
166 |
168 lemma diff_union_swap: |
167 lemma diff_union_swap: |
169 "a \<noteq> b \<Longrightarrow> M - {#a#} + {#b#} = M + {#b#} - {#a#}" |
168 "a \<noteq> b \<Longrightarrow> M - {#a#} + {#b#} = M + {#b#} - {#a#}" |
170 by (auto simp add: multiset_eq_iff) |
169 by (auto simp add: multiset_eq_iff) |