src/HOL/Library/Multiset.thy
changeset 46237 99c80c2f841a
parent 46168 bef8c811df20
child 46238 9ace9e5b79be
     1.1 --- a/src/HOL/Library/Multiset.thy	Mon Jan 16 21:50:15 2012 +0100
     1.2 +++ b/src/HOL/Library/Multiset.thy	Tue Jan 17 09:38:30 2012 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* (Finite) multisets *}
     1.5  
     1.6  theory Multiset
     1.7 -imports Main AList
     1.8 +imports Main DAList
     1.9  begin
    1.10  
    1.11  subsection {* The type of multisets *}
    1.12 @@ -1101,18 +1101,18 @@
    1.13  
    1.14  definition join
    1.15  where
    1.16 -  "join f xs ys = AList.Alist (join_raw f (AList.impl_of xs) (AList.impl_of ys))" 
    1.17 +  "join f xs ys = DAList.Alist (join_raw f (DAList.impl_of xs) (DAList.impl_of ys))" 
    1.18  
    1.19  lemma [code abstract]:
    1.20 -  "AList.impl_of (join f xs ys) = join_raw f (AList.impl_of xs) (AList.impl_of ys)"
    1.21 +  "DAList.impl_of (join f xs ys) = join_raw f (DAList.impl_of xs) (DAList.impl_of ys)"
    1.22  unfolding join_def by (simp add: Alist_inverse distinct_join_raw)
    1.23  
    1.24  definition subtract_entries
    1.25  where
    1.26 -  "subtract_entries xs ys = AList.Alist (subtract_entries_raw (AList.impl_of xs) (AList.impl_of ys))"
    1.27 +  "subtract_entries xs ys = DAList.Alist (subtract_entries_raw (DAList.impl_of xs) (DAList.impl_of ys))"
    1.28  
    1.29  lemma [code abstract]:
    1.30 -  "AList.impl_of (subtract_entries xs ys) = subtract_entries_raw (AList.impl_of xs) (AList.impl_of ys)"
    1.31 +  "DAList.impl_of (subtract_entries xs ys) = subtract_entries_raw (DAList.impl_of xs) (DAList.impl_of ys)"
    1.32  unfolding subtract_entries_def by (simp add: Alist_inverse distinct_subtract_entries_raw)
    1.33  
    1.34  text {* Implementing multisets by means of association lists *}
    1.35 @@ -1166,12 +1166,12 @@
    1.36  text {* Code equations for multiset operations *}
    1.37  
    1.38  definition Bag :: "('a, nat) alist \<Rightarrow> 'a multiset" where
    1.39 -  "Bag xs = Abs_multiset (count_of (AList.impl_of xs))"
    1.40 +  "Bag xs = Abs_multiset (count_of (DAList.impl_of xs))"
    1.41  
    1.42  code_datatype Bag
    1.43  
    1.44  lemma count_Bag [simp, code]:
    1.45 -  "count (Bag xs) = count_of (AList.impl_of xs)"
    1.46 +  "count (Bag xs) = count_of (DAList.impl_of xs)"
    1.47    by (simp add: Bag_def count_of_multiset Abs_multiset_inverse)
    1.48  
    1.49  lemma Mempty_Bag [code]:
    1.50 @@ -1192,11 +1192,11 @@
    1.51    (simp add: count_of_subtract_entries_raw alist.Alist_inverse distinct_subtract_entries_raw subtract_entries_def)
    1.52  
    1.53  lemma filter_Bag [code]:
    1.54 -  "Multiset.filter P (Bag xs) = Bag (AList.filter (P \<circ> fst) xs)"
    1.55 +  "Multiset.filter P (Bag xs) = Bag (DAList.filter (P \<circ> fst) xs)"
    1.56  by (rule multiset_eqI) (simp add: count_of_filter impl_of_filter)
    1.57  
    1.58  lemma mset_less_eq_Bag [code]:
    1.59 -  "Bag xs \<le> A \<longleftrightarrow> (\<forall>(x, n) \<in> set (AList.impl_of xs). count_of (AList.impl_of xs) x \<le> count A x)"
    1.60 +  "Bag xs \<le> A \<longleftrightarrow> (\<forall>(x, n) \<in> set (DAList.impl_of xs). count_of (DAList.impl_of xs) x \<le> count A x)"
    1.61      (is "?lhs \<longleftrightarrow> ?rhs")
    1.62  proof
    1.63    assume ?lhs then show ?rhs
    1.64 @@ -1206,8 +1206,8 @@
    1.65    show ?lhs
    1.66    proof (rule mset_less_eqI)
    1.67      fix x
    1.68 -    from `?rhs` have "count_of (AList.impl_of xs) x \<le> count A x"
    1.69 -      by (cases "x \<in> fst ` set (AList.impl_of xs)") (auto simp add: count_of_empty)
    1.70 +    from `?rhs` have "count_of (DAList.impl_of xs) x \<le> count A x"
    1.71 +      by (cases "x \<in> fst ` set (DAList.impl_of xs)") (auto simp add: count_of_empty)
    1.72      then show "count (Bag xs) x \<le> count A x"
    1.73        by (simp add: mset_le_def count_Bag)
    1.74    qed