# HG changeset patch # User bulwahn # Date 1332855244 -7200 # Node ID 9bfc32fc7cedfadf4fb108b2f8b13a262ed94541 # Parent 212f7a975d4950053f57aca26a641bd9f25c7935# Parent d64fa2ca54b8fda6e69ee35483018c103b0ae02a merged diff -r d64fa2ca54b8 -r 9bfc32fc7ced src/HOL/Library/DAList.thy --- a/src/HOL/Library/DAList.thy Tue Mar 27 14:49:56 2012 +0200 +++ b/src/HOL/Library/DAList.thy Tue Mar 27 15:34:04 2012 +0200 @@ -9,14 +9,22 @@ text {* This was based on some existing fragments in the AFP-Collection framework. *} +subsection {* Preliminaries *} + +lemma distinct_map_fst_filter: + "distinct (map fst xs) ==> distinct (map fst (List.filter P xs))" +by (induct xs) auto + subsection {* Type @{text "('key, 'value) alist" } *} -typedef (open) ('key, 'value) alist = "{xs :: ('key \ 'value) list. distinct (map fst xs)}" +typedef (open) ('key, 'value) alist = "{xs :: ('key \ 'value) list. (distinct o map fst) xs}" morphisms impl_of Alist proof - show "[] \ {xs. distinct (map fst xs)}" by simp + show "[] \ {xs. (distinct o map fst) xs}" by simp qed +setup_lifting type_definition_alist + lemma alist_ext: "impl_of xs = impl_of ys \ xs = ys" by(simp add: impl_of_inject) @@ -31,55 +39,46 @@ subsection {* Primitive operations *} -definition lookup :: "('key, 'value) alist \ 'key \ 'value option" -where [code]: "lookup xs = map_of (impl_of xs)" +(* FIXME: improve quotient_definition so that type annotations on the right hand sides can be removed *) + +quotient_definition lookup :: "('key, 'value) alist \ 'key \ 'value option" +where "lookup" is "map_of :: ('key * 'value) list \ 'key \ 'value option" .. -definition empty :: "('key, 'value) alist" -where [code del]: "empty = Alist []" +quotient_definition empty :: "('key, 'value) alist" +where "empty" is "[] :: ('key * 'value) list" by simp -definition update :: "'key \ 'value \ ('key, 'value) alist \ ('key, 'value) alist" -where [code del]: "update k v xs = Alist (AList.update k v (impl_of xs))" +quotient_definition update :: "'key \ 'value \ ('key, 'value) alist \ ('key, 'value) alist" +where "update" is "AList.update :: 'key \ 'value \ ('key * 'value) list \ ('key * 'value) list" +by (simp add: distinct_update) (* FIXME: we use an unoptimised delete operation. *) -definition delete :: "'key \ ('key, 'value) alist \ ('key, 'value) alist" -where [code del]: "delete k xs = Alist (AList.delete k (impl_of xs))" +quotient_definition delete :: "'key \ ('key, 'value) alist \ ('key, 'value) alist" +where "delete" is "AList.delete :: 'key \ ('key * 'value) list \ ('key * 'value) list" +by (simp add: distinct_delete) -definition map_entry :: "'key \ ('value \ 'value) \ ('key, 'value) alist \ ('key, 'value) alist" -where [code del]: "map_entry k f xs = Alist (AList.map_entry k f (impl_of xs))" +quotient_definition map_entry :: "'key \ ('value \ 'value) \ ('key, 'value) alist \ ('key, 'value) alist" +where "map_entry" is "AList.map_entry :: 'key \ ('value \ 'value) \ ('key * 'value) list \ ('key * 'value) list" +by (simp add: distinct_map_entry) -definition filter :: "('key \ 'value \ bool) \ ('key, 'value) alist \ ('key, 'value) alist" -where [code del]: "filter P xs = Alist (List.filter P (impl_of xs))" +quotient_definition filter :: "('key \ 'value \ bool) \ ('key, 'value) alist \ ('key, 'value) alist" +where "filter" is "List.filter :: ('key \ 'value \ bool) \ ('key * 'value) list \ ('key * 'value) list" +by (simp add: distinct_map_fst_filter) -definition map_default :: "'key => 'value => ('value => 'value) => ('key, 'value) alist => ('key, 'value) alist" -where - "map_default k v f xs = Alist (AList.map_default k v f (impl_of xs))" +quotient_definition map_default :: "'key => 'value => ('value => 'value) => ('key, 'value) alist => ('key, 'value) alist" +where "map_default" is "AList.map_default :: 'key => 'value => ('value => 'value) => ('key * 'value) list => ('key * 'value) list" +by (simp add: distinct_map_default) -lemma impl_of_empty [code abstract]: "impl_of empty = []" +(* FIXME: theorems are still used in Multiset; make code certificates available to the user *) +lemma impl_of_empty: "impl_of empty = []" by (simp add: empty_def Alist_inverse) -lemma impl_of_update [code abstract]: "impl_of (update k v xs) = AList.update k v (impl_of xs)" +lemma impl_of_update: "impl_of (update k v xs) = AList.update k v (impl_of xs)" by (simp add: update_def Alist_inverse distinct_update) -lemma impl_of_delete [code abstract]: - "impl_of (delete k al) = AList.delete k (impl_of al)" -unfolding delete_def by (simp add: Alist_inverse distinct_delete) - -lemma impl_of_map_entry [code abstract]: - "impl_of (map_entry k f xs) = AList.map_entry k f (impl_of xs)" -unfolding map_entry_def by (simp add: Alist_inverse distinct_map_entry) - -lemma distinct_map_fst_filter: - "distinct (map fst xs) ==> distinct (map fst (List.filter P xs))" -by (induct xs) auto - -lemma impl_of_filter [code abstract]: +lemma impl_of_filter: "impl_of (filter P xs) = List.filter P (impl_of xs)" unfolding filter_def by (simp add: Alist_inverse distinct_map_fst_filter) -lemma impl_of_map_default [code abstract]: - "impl_of (map_default k v f xs) = AList.map_default k v f (impl_of xs)" -by (auto simp add: map_default_def Alist_inverse distinct_map_default) - subsection {* Abstract operation properties *} (* FIXME: to be completed *) diff -r d64fa2ca54b8 -r 9bfc32fc7ced src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Tue Mar 27 14:49:56 2012 +0200 +++ b/src/HOL/Library/Multiset.thy Tue Mar 27 15:34:04 2012 +0200 @@ -1189,7 +1189,7 @@ lemma Mempty_Bag [code]: "{#} = Bag (DAList.empty)" by (simp add: multiset_eq_iff alist.Alist_inverse DAList.empty_def) - + lemma single_Bag [code]: "{#x#} = Bag (DAList.update x 1 DAList.empty)" by (simp add: multiset_eq_iff alist.Alist_inverse impl_of_update impl_of_empty)