12 |
12 |
13 lemma [code, code del]: "{#} = {#}" .. |
13 lemma [code, code del]: "{#} = {#}" .. |
14 |
14 |
15 lemma [code, code del]: "Multiset.is_empty = Multiset.is_empty" .. |
15 lemma [code, code del]: "Multiset.is_empty = Multiset.is_empty" .. |
16 |
16 |
17 lemma [code, code del]: "single = single" .. |
17 lemma [code, code del]: "add_mset = add_mset" .. |
18 |
18 |
19 lemma [code, code del]: "plus = (plus :: 'a multiset \<Rightarrow> _)" .. |
19 lemma [code, code del]: "plus = (plus :: 'a multiset \<Rightarrow> _)" .. |
20 |
20 |
21 lemma [code, code del]: "minus = (minus :: 'a multiset \<Rightarrow> _)" .. |
21 lemma [code, code del]: "minus = (minus :: 'a multiset \<Rightarrow> _)" .. |
22 |
22 |
208 also have "\<dots> \<longleftrightarrow> list_all (\<lambda>x. snd x = 0) (alist.impl_of xs)" |
208 also have "\<dots> \<longleftrightarrow> list_all (\<lambda>x. snd x = 0) (alist.impl_of xs)" |
209 by (auto simp: count_of_def list_all_def) |
209 by (auto simp: count_of_def list_all_def) |
210 finally show ?thesis by (simp add: is_empty_Bag_impl.rep_eq) |
210 finally show ?thesis by (simp add: is_empty_Bag_impl.rep_eq) |
211 qed |
211 qed |
212 |
212 |
213 lemma single_Bag [code]: "{#x#} = Bag (DAList.update x 1 DAList.empty)" |
|
214 by (simp add: multiset_eq_iff alist.Alist_inverse update.rep_eq empty.rep_eq) |
|
215 |
|
216 lemma union_Bag [code]: "Bag xs + Bag ys = Bag (join (\<lambda>x (n1, n2). n1 + n2) xs ys)" |
213 lemma union_Bag [code]: "Bag xs + Bag ys = Bag (join (\<lambda>x (n1, n2). n1 + n2) xs ys)" |
217 by (rule multiset_eqI) |
214 by (rule multiset_eqI) |
218 (simp add: count_of_join_raw alist.Alist_inverse distinct_join_raw join_def) |
215 (simp add: count_of_join_raw alist.Alist_inverse distinct_join_raw join_def) |
|
216 |
|
217 lemma add_mset_Bag [code]: "add_mset x (Bag xs) = |
|
218 Bag (join (\<lambda>x (n1, n2). n1 + n2) (DAList.update x 1 DAList.empty) xs)" |
|
219 unfolding add_mset_add_single[of x "Bag xs"] union_Bag[symmetric] |
|
220 by (simp add: multiset_eq_iff update.rep_eq empty.rep_eq) |
219 |
221 |
220 lemma minus_Bag [code]: "Bag xs - Bag ys = Bag (subtract_entries xs ys)" |
222 lemma minus_Bag [code]: "Bag xs - Bag ys = Bag (subtract_entries xs ys)" |
221 by (rule multiset_eqI) |
223 by (rule multiset_eqI) |
222 (simp add: count_of_subtract_entries_raw alist.Alist_inverse |
224 (simp add: count_of_subtract_entries_raw alist.Alist_inverse |
223 distinct_subtract_entries_raw subtract_entries_def) |
225 distinct_subtract_entries_raw subtract_entries_def) |
384 "image_mset f (Bag ms) = |
386 "image_mset f (Bag ms) = |
385 DAList_Multiset.fold (\<lambda>a n m. Bag (single_alist_entry (f a) n) + m) {#} ms" |
387 DAList_Multiset.fold (\<lambda>a n m. Bag (single_alist_entry (f a) n) + m) {#} ms" |
386 unfolding image_mset_def |
388 unfolding image_mset_def |
387 proof (rule comp_fun_commute.DAList_Multiset_fold, unfold_locales, (auto simp: ac_simps)[1]) |
389 proof (rule comp_fun_commute.DAList_Multiset_fold, unfold_locales, (auto simp: ac_simps)[1]) |
388 fix a n m |
390 fix a n m |
389 show "Bag (single_alist_entry (f a) n) + m = ((op + \<circ> single \<circ> f) a ^^ n) m" (is "?l = ?r") |
391 show "Bag (single_alist_entry (f a) n) + m = ((add_mset \<circ> f) a ^^ n) m" (is "?l = ?r") |
390 proof (rule multiset_eqI) |
392 proof (rule multiset_eqI) |
391 fix x |
393 fix x |
392 have "count ?r x = (if x = f a then n + count m x else count m x)" |
394 have "count ?r x = (if x = f a then n + count m x else count m x)" |
393 by (induct n) auto |
395 by (induct n) auto |
394 also have "\<dots> = count ?l x" |
396 also have "\<dots> = count ?l x" |