1.1 --- a/src/HOL/Library/DAList.thy	Mon Mar 26 21:03:30 2012 +0200
     1.2 +++ b/src/HOL/Library/DAList.thy	Tue Mar 27 14:14:46 2012 +0200
     1.3 @@ -9,14 +9,22 @@
     1.4  
     1.5  text {* This was based on some existing fragments in the AFP-Collection framework. *}
     1.6  
     1.7 +subsection {* Preliminaries *}
     1.8 +
     1.9 +lemma distinct_map_fst_filter:
    1.10 +   "distinct (map fst xs) ==> distinct (map fst (List.filter P xs))"
    1.11 +by (induct xs) auto
    1.12 +
    1.13  subsection {* Type @{text "('key, 'value) alist" } *}
    1.14  
    1.15 -typedef (open) ('key, 'value) alist = "{xs :: ('key \<times> 'value) list. distinct (map fst xs)}"
    1.16 +typedef (open) ('key, 'value) alist = "{xs :: ('key \<times> 'value) list. (distinct o map fst) xs}"
    1.17    morphisms impl_of Alist
    1.18  proof
    1.19 -  show "[] \<in> {xs. distinct (map fst xs)}" by simp
    1.20 +  show "[] \<in> {xs. (distinct o map fst) xs}" by simp
    1.21  qed
    1.22  
    1.23 +setup_lifting type_definition_alist
    1.24 +
    1.25  lemma alist_ext: "impl_of xs = impl_of ys \<Longrightarrow> xs = ys"
    1.26  by(simp add: impl_of_inject)
    1.27  
    1.28 @@ -31,55 +39,46 @@
    1.29  
    1.30  subsection {* Primitive operations *}
    1.31  
    1.32 -definition lookup :: "('key, 'value) alist \<Rightarrow> 'key \<Rightarrow> 'value option"
    1.33 -where [code]: "lookup xs = map_of (impl_of xs)" 
    1.34 +(* FIXME: improve quotient_definition so that type annotations on the right hand sides can be removed *) 
    1.35  
    1.36 -definition empty :: "('key, 'value) alist"
    1.37 -where [code del]: "empty = Alist []"
    1.38 +quotient_definition lookup :: "('key, 'value) alist \<Rightarrow> 'key \<Rightarrow> 'value option"
    1.39 +where "lookup" is "map_of :: ('key * 'value) list \<Rightarrow> 'key \<Rightarrow> 'value option" ..
    1.40  
    1.41 -definition update :: "'key \<Rightarrow> 'value \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    1.42 -where [code del]: "update k v xs = Alist (AList.update k v (impl_of xs))"
    1.43 +quotient_definition empty :: "('key, 'value) alist"
    1.44 +where "empty" is "[] :: ('key * 'value) list" by simp
    1.45 +
    1.46 +quotient_definition update :: "'key \<Rightarrow> 'value \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    1.47 +where "update" is "AList.update :: 'key \<Rightarrow> 'value \<Rightarrow> ('key * 'value) list \<Rightarrow> ('key * 'value) list"
    1.48 +by (simp add: distinct_update)
    1.49  
    1.50  (* FIXME: we use an unoptimised delete operation. *)
    1.51 -definition delete :: "'key \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    1.52 -where [code del]: "delete k xs = Alist (AList.delete k (impl_of xs))"
    1.53 +quotient_definition delete :: "'key \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    1.54 +where "delete" is "AList.delete :: 'key \<Rightarrow> ('key * 'value) list \<Rightarrow> ('key * 'value) list"
    1.55 +by (simp add: distinct_delete)
    1.56  
    1.57 -definition map_entry :: "'key \<Rightarrow> ('value \<Rightarrow> 'value) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    1.58 -where [code del]: "map_entry k f xs = Alist (AList.map_entry k f (impl_of xs))" 
    1.59 +quotient_definition map_entry :: "'key \<Rightarrow> ('value \<Rightarrow> 'value) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    1.60 +where "map_entry" is "AList.map_entry :: 'key \<Rightarrow> ('value \<Rightarrow> 'value) \<Rightarrow> ('key * 'value) list \<Rightarrow> ('key * 'value) list"
    1.61 +by (simp add: distinct_map_entry)
    1.62  
    1.63 -definition filter :: "('key \<times> 'value \<Rightarrow> bool) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    1.64 -where [code del]: "filter P xs = Alist (List.filter P (impl_of xs))"
    1.65 +quotient_definition filter :: "('key \<times> 'value \<Rightarrow> bool) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    1.66 +where "filter" is "List.filter :: ('key \<times> 'value \<Rightarrow> bool) \<Rightarrow> ('key * 'value) list \<Rightarrow> ('key * 'value) list"
    1.67 +by (simp add: distinct_map_fst_filter)
    1.68  
    1.69 -definition map_default :: "'key => 'value => ('value => 'value) => ('key, 'value) alist => ('key, 'value) alist"
    1.70 -where
    1.71 -  "map_default k v f xs = Alist (AList.map_default k v f (impl_of xs))"
    1.72 +quotient_definition map_default :: "'key => 'value => ('value => 'value) => ('key, 'value) alist => ('key, 'value) alist"
    1.73 +where "map_default" is "AList.map_default :: 'key => 'value => ('value => 'value) => ('key * 'value) list => ('key * 'value) list"
    1.74 +by (simp add: distinct_map_default)
    1.75  
    1.76 -lemma impl_of_empty [code abstract]: "impl_of empty = []"
    1.77 +(* FIXME: theorems are still used in Multiset; make code certificates available to the user *)
    1.78 +lemma impl_of_empty: "impl_of empty = []"
    1.79  by (simp add: empty_def Alist_inverse)
    1.80  
    1.81 -lemma impl_of_update [code abstract]: "impl_of (update k v xs) = AList.update k v (impl_of xs)"
    1.82 +lemma impl_of_update: "impl_of (update k v xs) = AList.update k v (impl_of xs)"
    1.83  by (simp add: update_def Alist_inverse distinct_update)
    1.84  
    1.85 -lemma impl_of_delete [code abstract]:
    1.86 -  "impl_of (delete k al) = AList.delete k (impl_of al)"
    1.87 -unfolding delete_def by (simp add: Alist_inverse distinct_delete)
    1.88 -
    1.89 -lemma impl_of_map_entry [code abstract]:
    1.90 -  "impl_of (map_entry k f xs) = AList.map_entry k f (impl_of xs)"
    1.91 -unfolding map_entry_def by (simp add: Alist_inverse distinct_map_entry)
    1.92 -
    1.93 -lemma distinct_map_fst_filter:
    1.94 -   "distinct (map fst xs) ==> distinct (map fst (List.filter P xs))"
    1.95 -by (induct xs) auto
    1.96 -
    1.97 -lemma impl_of_filter [code abstract]:
    1.98 +lemma impl_of_filter:
    1.99    "impl_of (filter P xs) = List.filter P (impl_of xs)"
   1.100  unfolding filter_def by (simp add: Alist_inverse distinct_map_fst_filter)
   1.101  
   1.102 -lemma impl_of_map_default [code abstract]:
   1.103 -  "impl_of (map_default k v f xs) = AList.map_default k v f (impl_of xs)"
   1.104 -by (auto simp add: map_default_def Alist_inverse distinct_map_default)
   1.105 -
   1.106  subsection {* Abstract operation properties *}
   1.107  
   1.108  (* FIXME: to be completed *)

     2.1 --- a/src/HOL/Library/Multiset.thy	Mon Mar 26 21:03:30 2012 +0200
     2.2 +++ b/src/HOL/Library/Multiset.thy	Tue Mar 27 14:14:46 2012 +0200
     2.3 @@ -1189,7 +1189,7 @@
     2.4  lemma Mempty_Bag [code]:
     2.5    "{#} = Bag (DAList.empty)"
     2.6    by (simp add: multiset_eq_iff alist.Alist_inverse DAList.empty_def)
     2.7 -  
     2.8 +
     2.9  lemma single_Bag [code]:
    2.10    "{#x#} = Bag (DAList.update x 1 DAList.empty)"
    2.11    by (simp add: multiset_eq_iff alist.Alist_inverse impl_of_update impl_of_empty)