equal
deleted
inserted
replaced
1187 by (simp add: Bag_def count_of_multiset Abs_multiset_inverse) |
1187 by (simp add: Bag_def count_of_multiset Abs_multiset_inverse) |
1188 |
1188 |
1189 lemma Mempty_Bag [code]: |
1189 lemma Mempty_Bag [code]: |
1190 "{#} = Bag (DAList.empty)" |
1190 "{#} = Bag (DAList.empty)" |
1191 by (simp add: multiset_eq_iff alist.Alist_inverse DAList.empty_def) |
1191 by (simp add: multiset_eq_iff alist.Alist_inverse DAList.empty_def) |
1192 |
1192 |
1193 lemma single_Bag [code]: |
1193 lemma single_Bag [code]: |
1194 "{#x#} = Bag (DAList.update x 1 DAList.empty)" |
1194 "{#x#} = Bag (DAList.update x 1 DAList.empty)" |
1195 by (simp add: multiset_eq_iff alist.Alist_inverse impl_of_update impl_of_empty) |
1195 by (simp add: multiset_eq_iff alist.Alist_inverse impl_of_update impl_of_empty) |
1196 |
1196 |
1197 lemma union_Bag [code]: |
1197 lemma union_Bag [code]: |