# HG changeset patch # User haftmann # Date 1270997465 -7200 # Node ID 1028cf8c0d1bcde2917ffd59ce5b76f022c9f1a1 # Parent bae883012af3a4b25b7a5fbddcce476c70c77aee constructor Mapping replaces AList diff -r bae883012af3 -r 1028cf8c0d1b src/HOL/Library/AssocList.thy --- a/src/HOL/Library/AssocList.thy Fri Apr 09 13:35:54 2010 +0200 +++ b/src/HOL/Library/AssocList.thy Sun Apr 11 16:51:05 2010 +0200 @@ -659,49 +659,49 @@ subsection {* Implementation of mappings *} -definition AList :: "('a \ 'b) list \ ('a, 'b) mapping" where - "AList xs = Mapping (map_of xs)" +definition Mapping :: "('a \ 'b) list \ ('a, 'b) mapping" where + "Mapping xs = Mapping.Mapping (map_of xs)" -code_datatype AList +code_datatype Mapping -lemma lookup_AList [simp, code]: - "Mapping.lookup (AList xs) = map_of xs" - by (simp add: AList_def) +lemma lookup_Mapping [simp, code]: + "Mapping.lookup (Mapping xs) = map_of xs" + by (simp add: Mapping_def) -lemma empty_AList [code]: - "Mapping.empty = AList []" +lemma empty_Mapping [code]: + "Mapping.empty = Mapping []" by (rule mapping_eqI) simp -lemma is_empty_AList [code]: - "Mapping.is_empty (AList xs) \ null xs" +lemma is_empty_Mapping [code]: + "Mapping.is_empty (Mapping xs) \ null xs" by (cases xs) (simp_all add: is_empty_def) -lemma update_AList [code]: - "Mapping.update k v (AList xs) = AList (update k v xs)" +lemma update_Mapping [code]: + "Mapping.update k v (Mapping xs) = Mapping (update k v xs)" by (rule mapping_eqI) (simp add: update_conv') -lemma delete_AList [code]: - "Mapping.delete k (AList xs) = AList (delete k xs)" +lemma delete_Mapping [code]: + "Mapping.delete k (Mapping xs) = Mapping (delete k xs)" by (rule mapping_eqI) (simp add: delete_conv') -lemma keys_AList [code]: - "Mapping.keys (AList xs) = set (map fst xs)" +lemma keys_Mapping [code]: + "Mapping.keys (Mapping xs) = set (map fst xs)" by (simp add: keys_def dom_map_of_conv_image_fst) -lemma ordered_keys_AList [code]: - "Mapping.ordered_keys (AList xs) = sort (remdups (map fst xs))" - by (simp only: ordered_keys_def keys_AList sorted_list_of_set_sort_remdups) +lemma ordered_keys_Mapping [code]: + "Mapping.ordered_keys (Mapping xs) = sort (remdups (map fst xs))" + by (simp only: ordered_keys_def keys_Mapping sorted_list_of_set_sort_remdups) -lemma size_AList [code]: - "Mapping.size (AList xs) = length (remdups (map fst xs))" +lemma size_Mapping [code]: + "Mapping.size (Mapping xs) = length (remdups (map fst xs))" by (simp add: size_def length_remdups_card_conv dom_map_of_conv_image_fst) -lemma tabulate_AList [code]: - "Mapping.tabulate ks f = AList (map (\k. (k, f k)) ks)" +lemma tabulate_Mapping [code]: + "Mapping.tabulate ks f = Mapping (map (\k. (k, f k)) ks)" by (rule mapping_eqI) (simp add: map_of_map_restrict) -lemma bulkload_AList [code]: - "Mapping.bulkload vs = AList (map (\n. (n, vs ! n)) [0..n. (n, vs ! n)) [0.. Mapping.keys (AList (x # xs))) in - the (Mapping.lookup (AList (x # xs)) l) + valuesum (Mapping.delete l (AList (x # xs))))" - by (simp_all add: valuesum_rec finite_dom_map_of is_empty_AList) +lemma valuesum_rec_Mapping: + shows [code]: "valuesum (Mapping []) = 0" + and "valuesum (Mapping (x # xs)) = (let l = (SOME l. l \ Mapping.keys (Mapping (x # xs))) in + the (Mapping.lookup (Mapping (x # xs)) l) + valuesum (Mapping.delete l (Mapping (x # xs))))" + by (simp_all add: valuesum_rec finite_dom_map_of is_empty_Mapping) text {* As a side effect the precondition disappears (but note this has nothing to do with choice!). @@ -76,27 +76,27 @@ *} lemma valuesum_rec_exec [code]: - "valuesum (AList (x # xs)) = (let l = fst (hd (x # xs)) in - the (Mapping.lookup (AList (x # xs)) l) + valuesum (Mapping.delete l (AList (x # xs))))" + "valuesum (Mapping (x # xs)) = (let l = fst (hd (x # xs)) in + the (Mapping.lookup (Mapping (x # xs)) l) + valuesum (Mapping.delete l (Mapping (x # xs))))" proof - - let ?M = "AList (x # xs)" + let ?M = "Mapping (x # xs)" let ?l1 = "(SOME l. l \ Mapping.keys ?M)" let ?l2 = "fst (hd (x # xs))" - have "finite (Mapping.keys ?M)" by (simp add: keys_AList) + have "finite (Mapping.keys ?M)" by (simp add: keys_Mapping) moreover have "?l1 \ Mapping.keys ?M" - by (rule someI) (auto simp add: keys_AList) + by (rule someI) (auto simp add: keys_Mapping) moreover have "?l2 \ Mapping.keys ?M" - by (simp add: keys_AList) + by (simp add: keys_Mapping) ultimately have "the (Mapping.lookup ?M ?l1) + valuesum (Mapping.delete ?l1 ?M) = the (Mapping.lookup ?M ?l2) + valuesum (Mapping.delete ?l2 ?M)" by (rule valuesum_choice) - then show ?thesis by (simp add: valuesum_rec_AList) + then show ?thesis by (simp add: valuesum_rec_Mapping) qed text {* See how it works: *} -value "valuesum (AList [(''abc'', (42::int)), (''def'', 1705)])" +value "valuesum (Mapping [(''abc'', (42::int)), (''def'', 1705)])" end