renamed theory AList to DAList
authorbulwahn
Tue Jan 17 09:38:30 2012 +0100 (2012-01-17)
changeset 4623799c80c2f841a
parent 46236 ae79f2978a67
child 46238 9ace9e5b79be
renamed theory AList to DAList
src/HOL/IsaMakefile
src/HOL/Library/AList.thy
src/HOL/Library/DAList.thy
src/HOL/Library/Multiset.thy
     1.1 --- a/src/HOL/IsaMakefile	Mon Jan 16 21:50:15 2012 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Tue Jan 17 09:38:30 2012 +0100
     1.3 @@ -436,7 +436,7 @@
     1.4  $(OUT)/HOL-Library: $(OUT)/HOL Library/ROOT.ML				\
     1.5    $(SRC)/HOL/Tools/float_arith.ML $(SRC)/Tools/float.ML			\
     1.6    Library/Abstract_Rat.thy $(SRC)/Tools/Adhoc_Overloading.thy		\
     1.7 -  Library/AList_Impl.thy Library/AList.thy Library/AList_Mapping.thy 	\
     1.8 +  Library/AList_Impl.thy Library/AList_Mapping.thy 	\
     1.9    Library/BigO.thy Library/Binomial.thy 				\
    1.10    Library/Bit.thy Library/Boolean_Algebra.thy Library/Cardinality.thy	\
    1.11    Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy	\
    1.12 @@ -446,8 +446,8 @@
    1.13    Tools/Predicate_Compile/code_prolog.ML Library/ContNotDenum.thy	\
    1.14    Library/Cset.thy Library/Cset_Monad.thy Library/Continuity.thy	\
    1.15    Library/Convex.thy Library/Countable.thy				\
    1.16 -  Library/Dlist.thy Library/Dlist_Cset.thy Library/Efficient_Nat.thy	\
    1.17 -  Library/Eval_Witness.thy						\
    1.18 +  Library/DAList.thy Library/Dlist.thy Library/Dlist_Cset.thy \
    1.19 +  Library/Efficient_Nat.thy Library/Eval_Witness.thy						\
    1.20    Library/Extended_Real.thy Library/Extended_Nat.thy Library/Float.thy	\
    1.21    Library/Formal_Power_Series.thy Library/Fraction_Field.thy		\
    1.22    Library/FrechetDeriv.thy Library/Cset.thy Library/FuncSet.thy		\
     2.1 --- a/src/HOL/Library/AList.thy	Mon Jan 16 21:50:15 2012 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,179 +0,0 @@
     2.4 -(*  Title:      HOL/Library/AList.thy
     2.5 -    Author:     Lukas Bulwahn, TU Muenchen *)
     2.6 -
     2.7 -header {* Abstract type of association lists with unique keys *}
     2.8 -
     2.9 -theory AList
    2.10 -imports AList_Impl
    2.11 -begin
    2.12 -
    2.13 -text {* This was based on some existing fragments in the AFP-Collection framework. *}
    2.14 -
    2.15 -subsection {* Type @{text "('key, 'value) alist" } *}
    2.16 -
    2.17 -typedef (open) ('key, 'value) alist = "{xs :: ('key \<times> 'value) list. distinct (map fst xs)}"
    2.18 -morphisms impl_of Alist
    2.19 -by(rule exI[where x="[]"]) simp
    2.20 -
    2.21 -lemma alist_ext: "impl_of xs = impl_of ys \<Longrightarrow> xs = ys"
    2.22 -by(simp add: impl_of_inject)
    2.23 -
    2.24 -lemma alist_eq_iff: "xs = ys \<longleftrightarrow> impl_of xs = impl_of ys"
    2.25 -by(simp add: impl_of_inject)
    2.26 -
    2.27 -lemma impl_of_distinct [simp, intro]: "distinct (map fst (impl_of xs))"
    2.28 -using impl_of[of xs] by simp
    2.29 -
    2.30 -lemma Alist_impl_of [code abstype]: "Alist (impl_of xs) = xs"
    2.31 -by(rule impl_of_inverse)
    2.32 -
    2.33 -subsection {* Primitive operations *}
    2.34 -
    2.35 -definition lookup :: "('key, 'value) alist \<Rightarrow> 'key \<Rightarrow> 'value option"
    2.36 -where [code]: "lookup xs = map_of (impl_of xs)" 
    2.37 -
    2.38 -definition empty :: "('key, 'value) alist"
    2.39 -where [code del]: "empty = Alist []"
    2.40 -
    2.41 -definition update :: "'key \<Rightarrow> 'value \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    2.42 -where [code del]: "update k v xs = Alist (AList_Impl.update k v (impl_of xs))"
    2.43 -
    2.44 -(* FIXME: we use an unoptimised delete operation. *)
    2.45 -definition delete :: "'key \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    2.46 -where [code del]: "delete k xs = Alist (AList_Impl.delete k (impl_of xs))"
    2.47 -
    2.48 -definition map_entry :: "'key \<Rightarrow> ('value \<Rightarrow> 'value) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    2.49 -where [code del]: "map_entry k f xs = Alist (AList_Impl.map_entry k f (impl_of xs))" 
    2.50 -
    2.51 -definition filter :: "('key \<times> 'value \<Rightarrow> bool) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    2.52 -where [code del]: "filter P xs = Alist (List.filter P (impl_of xs))"
    2.53 -
    2.54 -definition map_default :: "'key => 'value => ('value => 'value) => ('key, 'value) alist => ('key, 'value) alist"
    2.55 -where
    2.56 -  "map_default k v f xs = Alist (AList_Impl.map_default k v f (impl_of xs))"
    2.57 -
    2.58 -lemma impl_of_empty [code abstract]: "impl_of empty = []"
    2.59 -by (simp add: empty_def Alist_inverse)
    2.60 -
    2.61 -lemma impl_of_update [code abstract]: "impl_of (update k v xs) = AList_Impl.update k v (impl_of xs)"
    2.62 -by (simp add: update_def Alist_inverse distinct_update)
    2.63 -
    2.64 -lemma impl_of_delete [code abstract]:
    2.65 -  "impl_of (delete k al) = AList_Impl.delete k (impl_of al)"
    2.66 -unfolding delete_def by (simp add: Alist_inverse distinct_delete)
    2.67 -
    2.68 -lemma impl_of_map_entry [code abstract]:
    2.69 -  "impl_of (map_entry k f xs) = AList_Impl.map_entry k f (impl_of xs)"
    2.70 -unfolding map_entry_def by (simp add: Alist_inverse distinct_map_entry)
    2.71 -
    2.72 -lemma distinct_map_fst_filter:
    2.73 -   "distinct (map fst xs) ==> distinct (map fst (List.filter P xs))"
    2.74 -by (induct xs) auto
    2.75 -
    2.76 -lemma impl_of_filter [code abstract]:
    2.77 -  "impl_of (filter P xs) = List.filter P (impl_of xs)"
    2.78 -unfolding filter_def by (simp add: Alist_inverse distinct_map_fst_filter)
    2.79 -
    2.80 -lemma impl_of_map_default [code abstract]:
    2.81 -  "impl_of (map_default k v f xs) = AList_Impl.map_default k v f (impl_of xs)"
    2.82 -by (auto simp add: map_default_def Alist_inverse distinct_map_default)
    2.83 -
    2.84 -subsection {* Abstract operation properties *}
    2.85 -
    2.86 -(* FIXME: to be completed *)
    2.87 -
    2.88 -lemma lookup_empty [simp]: "lookup empty k = None"
    2.89 -by(simp add: empty_def lookup_def Alist_inverse)
    2.90 -
    2.91 -lemma lookup_delete [simp]: "lookup (delete k al) = (lookup al)(k := None)"
    2.92 -by (simp add: lookup_def delete_def Alist_inverse distinct_delete delete_conv')
    2.93 -
    2.94 -subsection {* Further operations *}
    2.95 -
    2.96 -subsubsection {* Equality *}
    2.97 -
    2.98 -instantiation alist :: (equal, equal) equal begin
    2.99 -
   2.100 -definition "HOL.equal (xs :: ('a, 'b) alist) ys == impl_of xs = impl_of ys"
   2.101 -
   2.102 -instance
   2.103 -proof
   2.104 -qed (simp add: equal_alist_def impl_of_inject)
   2.105 -
   2.106 -end
   2.107 -
   2.108 -subsubsection {* Size *}
   2.109 -
   2.110 -instantiation alist :: (type, type) size begin
   2.111 -
   2.112 -definition "size (al :: ('a, 'b) alist) = length (impl_of al)"
   2.113 -
   2.114 -instance ..
   2.115 -
   2.116 -end
   2.117 -
   2.118 -subsection {* Quickcheck generators *}
   2.119 -
   2.120 -notation fcomp (infixl "\<circ>>" 60)
   2.121 -notation scomp (infixl "\<circ>\<rightarrow>" 60)
   2.122 -
   2.123 -definition (in term_syntax)
   2.124 -  valterm_empty :: "('key :: typerep, 'value :: typerep) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)"
   2.125 -where
   2.126 -  "valterm_empty = Code_Evaluation.valtermify empty"
   2.127 -
   2.128 -definition (in term_syntax)
   2.129 -  valterm_update :: "'key :: typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
   2.130 -  'value :: typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
   2.131 -  ('key, 'value) alist \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
   2.132 -  ('key, 'value) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
   2.133 -  [code_unfold]: "valterm_update k v a = Code_Evaluation.valtermify update {\<cdot>} k {\<cdot>} v {\<cdot>}a"
   2.134 -
   2.135 -fun (in term_syntax) random_aux_alist 
   2.136 -where
   2.137 -  "random_aux_alist i j = (if i = 0 then Pair valterm_empty else Quickcheck.collapse (Random.select_weight [(i, Quickcheck.random j \<circ>\<rightarrow> (%k. Quickcheck.random j \<circ>\<rightarrow> (%v. random_aux_alist (i - 1) j \<circ>\<rightarrow> (%a. Pair (valterm_update k v a))))), (1, Pair valterm_empty)]))"
   2.138 -
   2.139 -instantiation alist :: (random, random) random
   2.140 -begin
   2.141 -
   2.142 -definition random_alist
   2.143 -where
   2.144 -  "random_alist i = random_aux_alist i i"
   2.145 - 
   2.146 -instance ..
   2.147 -
   2.148 -end
   2.149 -
   2.150 -no_notation fcomp (infixl "\<circ>>" 60)
   2.151 -no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
   2.152 -
   2.153 -instantiation alist :: (exhaustive, exhaustive) exhaustive
   2.154 -begin
   2.155 -
   2.156 -fun exhaustive_alist :: "(('a, 'b) alist => (bool * term list) option) => code_numeral => (bool * term list) option"
   2.157 -where
   2.158 -  "exhaustive_alist f i = (if i = 0 then None else case f empty of Some ts => Some ts | None =>
   2.159 -     exhaustive_alist (%a. Quickcheck_Exhaustive.exhaustive (%k. Quickcheck_Exhaustive.exhaustive (%v. f (update k v a)) (i - 1)) (i - 1)) (i - 1))"
   2.160 -
   2.161 -instance ..
   2.162 -
   2.163 -end
   2.164 -
   2.165 -instantiation alist :: (full_exhaustive, full_exhaustive) full_exhaustive
   2.166 -begin
   2.167 -
   2.168 -fun full_exhaustive_alist :: "(('a, 'b) alist * (unit => term) => (bool * term list) option) => code_numeral => (bool * term list) option"
   2.169 -where
   2.170 -  "full_exhaustive_alist f i = (if i = 0 then None else case f valterm_empty of Some ts => Some ts | None =>
   2.171 -     full_exhaustive_alist (%a. Quickcheck_Exhaustive.full_exhaustive (%k. Quickcheck_Exhaustive.full_exhaustive (%v. f (valterm_update k v a)) (i - 1)) (i - 1)) (i - 1))"
   2.172 -
   2.173 -instance ..
   2.174 -
   2.175 -end
   2.176 -
   2.177 -hide_const valterm_empty valterm_update random_aux_alist
   2.178 -
   2.179 -hide_fact (open) lookup_def empty_def update_def delete_def map_entry_def filter_def map_default_def
   2.180 -hide_const (open) impl_of lookup empty update delete map_entry filter map_default 
   2.181 -
   2.182 -end
   2.183 \ No newline at end of file
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Library/DAList.thy	Tue Jan 17 09:38:30 2012 +0100
     3.3 @@ -0,0 +1,179 @@
     3.4 +(*  Title:      HOL/Library/DAList.thy
     3.5 +    Author:     Lukas Bulwahn, TU Muenchen *)
     3.6 +
     3.7 +header {* Abstract type of association lists with unique keys *}
     3.8 +
     3.9 +theory DAList
    3.10 +imports AList_Impl
    3.11 +begin
    3.12 +
    3.13 +text {* This was based on some existing fragments in the AFP-Collection framework. *}
    3.14 +
    3.15 +subsection {* Type @{text "('key, 'value) alist" } *}
    3.16 +
    3.17 +typedef (open) ('key, 'value) alist = "{xs :: ('key \<times> 'value) list. distinct (map fst xs)}"
    3.18 +morphisms impl_of Alist
    3.19 +by(rule exI[where x="[]"]) simp
    3.20 +
    3.21 +lemma alist_ext: "impl_of xs = impl_of ys \<Longrightarrow> xs = ys"
    3.22 +by(simp add: impl_of_inject)
    3.23 +
    3.24 +lemma alist_eq_iff: "xs = ys \<longleftrightarrow> impl_of xs = impl_of ys"
    3.25 +by(simp add: impl_of_inject)
    3.26 +
    3.27 +lemma impl_of_distinct [simp, intro]: "distinct (map fst (impl_of xs))"
    3.28 +using impl_of[of xs] by simp
    3.29 +
    3.30 +lemma Alist_impl_of [code abstype]: "Alist (impl_of xs) = xs"
    3.31 +by(rule impl_of_inverse)
    3.32 +
    3.33 +subsection {* Primitive operations *}
    3.34 +
    3.35 +definition lookup :: "('key, 'value) alist \<Rightarrow> 'key \<Rightarrow> 'value option"
    3.36 +where [code]: "lookup xs = map_of (impl_of xs)" 
    3.37 +
    3.38 +definition empty :: "('key, 'value) alist"
    3.39 +where [code del]: "empty = Alist []"
    3.40 +
    3.41 +definition update :: "'key \<Rightarrow> 'value \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    3.42 +where [code del]: "update k v xs = Alist (AList_Impl.update k v (impl_of xs))"
    3.43 +
    3.44 +(* FIXME: we use an unoptimised delete operation. *)
    3.45 +definition delete :: "'key \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    3.46 +where [code del]: "delete k xs = Alist (AList_Impl.delete k (impl_of xs))"
    3.47 +
    3.48 +definition map_entry :: "'key \<Rightarrow> ('value \<Rightarrow> 'value) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    3.49 +where [code del]: "map_entry k f xs = Alist (AList_Impl.map_entry k f (impl_of xs))" 
    3.50 +
    3.51 +definition filter :: "('key \<times> 'value \<Rightarrow> bool) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    3.52 +where [code del]: "filter P xs = Alist (List.filter P (impl_of xs))"
    3.53 +
    3.54 +definition map_default :: "'key => 'value => ('value => 'value) => ('key, 'value) alist => ('key, 'value) alist"
    3.55 +where
    3.56 +  "map_default k v f xs = Alist (AList_Impl.map_default k v f (impl_of xs))"
    3.57 +
    3.58 +lemma impl_of_empty [code abstract]: "impl_of empty = []"
    3.59 +by (simp add: empty_def Alist_inverse)
    3.60 +
    3.61 +lemma impl_of_update [code abstract]: "impl_of (update k v xs) = AList_Impl.update k v (impl_of xs)"
    3.62 +by (simp add: update_def Alist_inverse distinct_update)
    3.63 +
    3.64 +lemma impl_of_delete [code abstract]:
    3.65 +  "impl_of (delete k al) = AList_Impl.delete k (impl_of al)"
    3.66 +unfolding delete_def by (simp add: Alist_inverse distinct_delete)
    3.67 +
    3.68 +lemma impl_of_map_entry [code abstract]:
    3.69 +  "impl_of (map_entry k f xs) = AList_Impl.map_entry k f (impl_of xs)"
    3.70 +unfolding map_entry_def by (simp add: Alist_inverse distinct_map_entry)
    3.71 +
    3.72 +lemma distinct_map_fst_filter:
    3.73 +   "distinct (map fst xs) ==> distinct (map fst (List.filter P xs))"
    3.74 +by (induct xs) auto
    3.75 +
    3.76 +lemma impl_of_filter [code abstract]:
    3.77 +  "impl_of (filter P xs) = List.filter P (impl_of xs)"
    3.78 +unfolding filter_def by (simp add: Alist_inverse distinct_map_fst_filter)
    3.79 +
    3.80 +lemma impl_of_map_default [code abstract]:
    3.81 +  "impl_of (map_default k v f xs) = AList_Impl.map_default k v f (impl_of xs)"
    3.82 +by (auto simp add: map_default_def Alist_inverse distinct_map_default)
    3.83 +
    3.84 +subsection {* Abstract operation properties *}
    3.85 +
    3.86 +(* FIXME: to be completed *)
    3.87 +
    3.88 +lemma lookup_empty [simp]: "lookup empty k = None"
    3.89 +by(simp add: empty_def lookup_def Alist_inverse)
    3.90 +
    3.91 +lemma lookup_delete [simp]: "lookup (delete k al) = (lookup al)(k := None)"
    3.92 +by (simp add: lookup_def delete_def Alist_inverse distinct_delete delete_conv')
    3.93 +
    3.94 +subsection {* Further operations *}
    3.95 +
    3.96 +subsubsection {* Equality *}
    3.97 +
    3.98 +instantiation alist :: (equal, equal) equal begin
    3.99 +
   3.100 +definition "HOL.equal (xs :: ('a, 'b) alist) ys == impl_of xs = impl_of ys"
   3.101 +
   3.102 +instance
   3.103 +proof
   3.104 +qed (simp add: equal_alist_def impl_of_inject)
   3.105 +
   3.106 +end
   3.107 +
   3.108 +subsubsection {* Size *}
   3.109 +
   3.110 +instantiation alist :: (type, type) size begin
   3.111 +
   3.112 +definition "size (al :: ('a, 'b) alist) = length (impl_of al)"
   3.113 +
   3.114 +instance ..
   3.115 +
   3.116 +end
   3.117 +
   3.118 +subsection {* Quickcheck generators *}
   3.119 +
   3.120 +notation fcomp (infixl "\<circ>>" 60)
   3.121 +notation scomp (infixl "\<circ>\<rightarrow>" 60)
   3.122 +
   3.123 +definition (in term_syntax)
   3.124 +  valterm_empty :: "('key :: typerep, 'value :: typerep) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)"
   3.125 +where
   3.126 +  "valterm_empty = Code_Evaluation.valtermify empty"
   3.127 +
   3.128 +definition (in term_syntax)
   3.129 +  valterm_update :: "'key :: typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
   3.130 +  'value :: typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
   3.131 +  ('key, 'value) alist \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
   3.132 +  ('key, 'value) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
   3.133 +  [code_unfold]: "valterm_update k v a = Code_Evaluation.valtermify update {\<cdot>} k {\<cdot>} v {\<cdot>}a"
   3.134 +
   3.135 +fun (in term_syntax) random_aux_alist 
   3.136 +where
   3.137 +  "random_aux_alist i j = (if i = 0 then Pair valterm_empty else Quickcheck.collapse (Random.select_weight [(i, Quickcheck.random j \<circ>\<rightarrow> (%k. Quickcheck.random j \<circ>\<rightarrow> (%v. random_aux_alist (i - 1) j \<circ>\<rightarrow> (%a. Pair (valterm_update k v a))))), (1, Pair valterm_empty)]))"
   3.138 +
   3.139 +instantiation alist :: (random, random) random
   3.140 +begin
   3.141 +
   3.142 +definition random_alist
   3.143 +where
   3.144 +  "random_alist i = random_aux_alist i i"
   3.145 + 
   3.146 +instance ..
   3.147 +
   3.148 +end
   3.149 +
   3.150 +no_notation fcomp (infixl "\<circ>>" 60)
   3.151 +no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
   3.152 +
   3.153 +instantiation alist :: (exhaustive, exhaustive) exhaustive
   3.154 +begin
   3.155 +
   3.156 +fun exhaustive_alist :: "(('a, 'b) alist => (bool * term list) option) => code_numeral => (bool * term list) option"
   3.157 +where
   3.158 +  "exhaustive_alist f i = (if i = 0 then None else case f empty of Some ts => Some ts | None =>
   3.159 +     exhaustive_alist (%a. Quickcheck_Exhaustive.exhaustive (%k. Quickcheck_Exhaustive.exhaustive (%v. f (update k v a)) (i - 1)) (i - 1)) (i - 1))"
   3.160 +
   3.161 +instance ..
   3.162 +
   3.163 +end
   3.164 +
   3.165 +instantiation alist :: (full_exhaustive, full_exhaustive) full_exhaustive
   3.166 +begin
   3.167 +
   3.168 +fun full_exhaustive_alist :: "(('a, 'b) alist * (unit => term) => (bool * term list) option) => code_numeral => (bool * term list) option"
   3.169 +where
   3.170 +  "full_exhaustive_alist f i = (if i = 0 then None else case f valterm_empty of Some ts => Some ts | None =>
   3.171 +     full_exhaustive_alist (%a. Quickcheck_Exhaustive.full_exhaustive (%k. Quickcheck_Exhaustive.full_exhaustive (%v. f (valterm_update k v a)) (i - 1)) (i - 1)) (i - 1))"
   3.172 +
   3.173 +instance ..
   3.174 +
   3.175 +end
   3.176 +
   3.177 +hide_const valterm_empty valterm_update random_aux_alist
   3.178 +
   3.179 +hide_fact (open) lookup_def empty_def update_def delete_def map_entry_def filter_def map_default_def
   3.180 +hide_const (open) impl_of lookup empty update delete map_entry filter map_default 
   3.181 +
   3.182 +end
   3.183 \ No newline at end of file
     4.1 --- a/src/HOL/Library/Multiset.thy	Mon Jan 16 21:50:15 2012 +0100
     4.2 +++ b/src/HOL/Library/Multiset.thy	Tue Jan 17 09:38:30 2012 +0100
     4.3 @@ -5,7 +5,7 @@
     4.4  header {* (Finite) multisets *}
     4.5  
     4.6  theory Multiset
     4.7 -imports Main AList
     4.8 +imports Main DAList
     4.9  begin
    4.10  
    4.11  subsection {* The type of multisets *}
    4.12 @@ -1101,18 +1101,18 @@
    4.13  
    4.14  definition join
    4.15  where
    4.16 -  "join f xs ys = AList.Alist (join_raw f (AList.impl_of xs) (AList.impl_of ys))" 
    4.17 +  "join f xs ys = DAList.Alist (join_raw f (DAList.impl_of xs) (DAList.impl_of ys))" 
    4.18  
    4.19  lemma [code abstract]:
    4.20 -  "AList.impl_of (join f xs ys) = join_raw f (AList.impl_of xs) (AList.impl_of ys)"
    4.21 +  "DAList.impl_of (join f xs ys) = join_raw f (DAList.impl_of xs) (DAList.impl_of ys)"
    4.22  unfolding join_def by (simp add: Alist_inverse distinct_join_raw)
    4.23  
    4.24  definition subtract_entries
    4.25  where
    4.26 -  "subtract_entries xs ys = AList.Alist (subtract_entries_raw (AList.impl_of xs) (AList.impl_of ys))"
    4.27 +  "subtract_entries xs ys = DAList.Alist (subtract_entries_raw (DAList.impl_of xs) (DAList.impl_of ys))"
    4.28  
    4.29  lemma [code abstract]:
    4.30 -  "AList.impl_of (subtract_entries xs ys) = subtract_entries_raw (AList.impl_of xs) (AList.impl_of ys)"
    4.31 +  "DAList.impl_of (subtract_entries xs ys) = subtract_entries_raw (DAList.impl_of xs) (DAList.impl_of ys)"
    4.32  unfolding subtract_entries_def by (simp add: Alist_inverse distinct_subtract_entries_raw)
    4.33  
    4.34  text {* Implementing multisets by means of association lists *}
    4.35 @@ -1166,12 +1166,12 @@
    4.36  text {* Code equations for multiset operations *}
    4.37  
    4.38  definition Bag :: "('a, nat) alist \<Rightarrow> 'a multiset" where
    4.39 -  "Bag xs = Abs_multiset (count_of (AList.impl_of xs))"
    4.40 +  "Bag xs = Abs_multiset (count_of (DAList.impl_of xs))"
    4.41  
    4.42  code_datatype Bag
    4.43  
    4.44  lemma count_Bag [simp, code]:
    4.45 -  "count (Bag xs) = count_of (AList.impl_of xs)"
    4.46 +  "count (Bag xs) = count_of (DAList.impl_of xs)"
    4.47    by (simp add: Bag_def count_of_multiset Abs_multiset_inverse)
    4.48  
    4.49  lemma Mempty_Bag [code]:
    4.50 @@ -1192,11 +1192,11 @@
    4.51    (simp add: count_of_subtract_entries_raw alist.Alist_inverse distinct_subtract_entries_raw subtract_entries_def)
    4.52  
    4.53  lemma filter_Bag [code]:
    4.54 -  "Multiset.filter P (Bag xs) = Bag (AList.filter (P \<circ> fst) xs)"
    4.55 +  "Multiset.filter P (Bag xs) = Bag (DAList.filter (P \<circ> fst) xs)"
    4.56  by (rule multiset_eqI) (simp add: count_of_filter impl_of_filter)
    4.57  
    4.58  lemma mset_less_eq_Bag [code]:
    4.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)"
    4.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)"
    4.61      (is "?lhs \<longleftrightarrow> ?rhs")
    4.62  proof
    4.63    assume ?lhs then show ?rhs
    4.64 @@ -1206,8 +1206,8 @@
    4.65    show ?lhs
    4.66    proof (rule mset_less_eqI)
    4.67      fix x
    4.68 -    from `?rhs` have "count_of (AList.impl_of xs) x \<le> count A x"
    4.69 -      by (cases "x \<in> fst ` set (AList.impl_of xs)") (auto simp add: count_of_empty)
    4.70 +    from `?rhs` have "count_of (DAList.impl_of xs) x \<le> count A x"
    4.71 +      by (cases "x \<in> fst ` set (DAList.impl_of xs)") (auto simp add: count_of_empty)
    4.72      then show "count (Bag xs) x \<le> count A x"
    4.73        by (simp add: mset_le_def count_Bag)
    4.74    qed