improving code equations for multisets that violated the distinct AList abstraction
authorbulwahn
Wed Feb 01 15:28:02 2012 +0100 (2012-02-01)
changeset 4639468f973ffd763
parent 46393 69f2d19f7d33
child 46395 f56be74d7f51
improving code equations for multisets that violated the distinct AList abstraction
src/HOL/Library/Multiset.thy
     1.1 --- a/src/HOL/Library/Multiset.thy	Thu Feb 02 01:55:17 2012 +0100
     1.2 +++ b/src/HOL/Library/Multiset.thy	Wed Feb 01 15:28:02 2012 +0100
     1.3 @@ -1175,12 +1175,12 @@
     1.4    by (simp add: Bag_def count_of_multiset Abs_multiset_inverse)
     1.5  
     1.6  lemma Mempty_Bag [code]:
     1.7 -  "{#} = Bag (Alist [])"
     1.8 -  by (simp add: multiset_eq_iff alist.Alist_inverse)
     1.9 +  "{#} = Bag (DAList.empty)"
    1.10 +  by (simp add: multiset_eq_iff alist.Alist_inverse DAList.empty_def)
    1.11    
    1.12  lemma single_Bag [code]:
    1.13 -  "{#x#} = Bag (Alist [(x, 1)])"
    1.14 -  by (simp add: multiset_eq_iff alist.Alist_inverse)
    1.15 +  "{#x#} = Bag (DAList.update x 1 DAList.empty)"
    1.16 +  by (simp add: multiset_eq_iff alist.Alist_inverse impl_of_update impl_of_empty)
    1.17  
    1.18  lemma union_Bag [code]:
    1.19    "Bag xs + Bag ys = Bag (join (\<lambda>x (n1, n2). n1 + n2) xs ys)"