236 apply (unfold Mempty_def single_def union_def) |
236 apply (unfold Mempty_def single_def union_def) |
237 apply (simp add: add_is_1 one_is_add expand_fun_eq) |
237 apply (simp add: add_is_1 one_is_add expand_fun_eq) |
238 apply (blast dest: sym) |
238 apply (blast dest: sym) |
239 done |
239 done |
240 |
240 |
241 ML"reset use_neq_simproc" |
|
242 lemma add_eq_conv_diff: |
241 lemma add_eq_conv_diff: |
243 "(M + {#a#} = N + {#b#}) = |
242 "(M + {#a#} = N + {#b#}) = |
244 (M = N \<and> a = b \<or> M = N - {#a#} + {#b#} \<and> N = M - {#b#} + {#a#})" |
243 (M = N \<and> a = b \<or> M = N - {#a#} + {#b#} \<and> N = M - {#b#} + {#a#})" |
|
244 using [[simproc del: neq]] |
245 apply (unfold single_def union_def diff_def) |
245 apply (unfold single_def union_def diff_def) |
246 apply (simp (no_asm) add: expand_fun_eq) |
246 apply (simp (no_asm) add: expand_fun_eq) |
247 apply (rule conjI, force, safe, simp_all) |
247 apply (rule conjI, force, safe, simp_all) |
248 apply (simp add: eq_sym_conv) |
248 apply (simp add: eq_sym_conv) |
249 done |
249 done |
250 ML"set use_neq_simproc" |
|
251 |
250 |
252 declare Rep_multiset_inject [symmetric, simp del] |
251 declare Rep_multiset_inject [symmetric, simp del] |
253 |
252 |
254 instance multiset :: (type) cancel_ab_semigroup_add |
253 instance multiset :: (type) cancel_ab_semigroup_add |
255 proof |
254 proof |