src/HOL/Library/DAList.thy
changeset 46238 9ace9e5b79be
parent 46237 99c80c2f841a
child 46507 1b24c24017dd
     1.1 --- a/src/HOL/Library/DAList.thy	Tue Jan 17 09:38:30 2012 +0100
     1.2 +++ b/src/HOL/Library/DAList.thy	Tue Jan 17 10:45:42 2012 +0100
     1.3 @@ -4,7 +4,7 @@
     1.4  header {* Abstract type of association lists with unique keys *}
     1.5  
     1.6  theory DAList
     1.7 -imports AList_Impl
     1.8 +imports AList
     1.9  begin
    1.10  
    1.11  text {* This was based on some existing fragments in the AFP-Collection framework. *}
    1.12 @@ -36,34 +36,34 @@
    1.13  where [code del]: "empty = Alist []"
    1.14  
    1.15  definition update :: "'key \<Rightarrow> 'value \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    1.16 -where [code del]: "update k v xs = Alist (AList_Impl.update k v (impl_of xs))"
    1.17 +where [code del]: "update k v xs = Alist (AList.update k v (impl_of xs))"
    1.18  
    1.19  (* FIXME: we use an unoptimised delete operation. *)
    1.20  definition delete :: "'key \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    1.21 -where [code del]: "delete k xs = Alist (AList_Impl.delete k (impl_of xs))"
    1.22 +where [code del]: "delete k xs = Alist (AList.delete k (impl_of xs))"
    1.23  
    1.24  definition map_entry :: "'key \<Rightarrow> ('value \<Rightarrow> 'value) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    1.25 -where [code del]: "map_entry k f xs = Alist (AList_Impl.map_entry k f (impl_of xs))" 
    1.26 +where [code del]: "map_entry k f xs = Alist (AList.map_entry k f (impl_of xs))" 
    1.27  
    1.28  definition filter :: "('key \<times> 'value \<Rightarrow> bool) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    1.29  where [code del]: "filter P xs = Alist (List.filter P (impl_of xs))"
    1.30  
    1.31  definition map_default :: "'key => 'value => ('value => 'value) => ('key, 'value) alist => ('key, 'value) alist"
    1.32  where
    1.33 -  "map_default k v f xs = Alist (AList_Impl.map_default k v f (impl_of xs))"
    1.34 +  "map_default k v f xs = Alist (AList.map_default k v f (impl_of xs))"
    1.35  
    1.36  lemma impl_of_empty [code abstract]: "impl_of empty = []"
    1.37  by (simp add: empty_def Alist_inverse)
    1.38  
    1.39 -lemma impl_of_update [code abstract]: "impl_of (update k v xs) = AList_Impl.update k v (impl_of xs)"
    1.40 +lemma impl_of_update [code abstract]: "impl_of (update k v xs) = AList.update k v (impl_of xs)"
    1.41  by (simp add: update_def Alist_inverse distinct_update)
    1.42  
    1.43  lemma impl_of_delete [code abstract]:
    1.44 -  "impl_of (delete k al) = AList_Impl.delete k (impl_of al)"
    1.45 +  "impl_of (delete k al) = AList.delete k (impl_of al)"
    1.46  unfolding delete_def by (simp add: Alist_inverse distinct_delete)
    1.47  
    1.48  lemma impl_of_map_entry [code abstract]:
    1.49 -  "impl_of (map_entry k f xs) = AList_Impl.map_entry k f (impl_of xs)"
    1.50 +  "impl_of (map_entry k f xs) = AList.map_entry k f (impl_of xs)"
    1.51  unfolding map_entry_def by (simp add: Alist_inverse distinct_map_entry)
    1.52  
    1.53  lemma distinct_map_fst_filter:
    1.54 @@ -75,7 +75,7 @@
    1.55  unfolding filter_def by (simp add: Alist_inverse distinct_map_fst_filter)
    1.56  
    1.57  lemma impl_of_map_default [code abstract]:
    1.58 -  "impl_of (map_default k v f xs) = AList_Impl.map_default k v f (impl_of xs)"
    1.59 +  "impl_of (map_default k v f xs) = AList.map_default k v f (impl_of xs)"
    1.60  by (auto simp add: map_default_def Alist_inverse distinct_map_default)
    1.61  
    1.62  subsection {* Abstract operation properties *}
    1.63 @@ -176,4 +176,4 @@
    1.64  hide_fact (open) lookup_def empty_def update_def delete_def map_entry_def filter_def map_default_def
    1.65  hide_const (open) impl_of lookup empty update delete map_entry filter map_default 
    1.66  
    1.67 -end
    1.68 \ No newline at end of file
    1.69 +end