mappings implemented by association lists
authorhaftmann
Wed Feb 17 09:48:52 2010 +0100 (2010-02-17)
changeset 3515637872c68a385
parent 35127 5b29c1660047
child 35157 73cd6f78c86d
mappings implemented by association lists
src/HOL/Library/AssocList.thy
     1.1 --- a/src/HOL/Library/AssocList.thy	Mon Feb 15 14:04:06 2010 +0100
     1.2 +++ b/src/HOL/Library/AssocList.thy	Wed Feb 17 09:48:52 2010 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Map operations implemented on association lists*}
     1.5  
     1.6  theory AssocList 
     1.7 -imports Main
     1.8 +imports Main Mapping
     1.9  begin
    1.10  
    1.11  text {*
    1.12 @@ -656,4 +656,48 @@
    1.13      (map_of xs k = None \<or> (\<exists>k'. map_of xs k = Some k' \<and> map_of ys k' = None)) " 
    1.14    by (simp add: compose_conv map_comp_None_iff)
    1.15  
    1.16 +
    1.17 +subsection {* Implementation of mappings *}
    1.18 +
    1.19 +definition AList :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) mapping" where
    1.20 +  "AList xs = Mapping (map_of xs)"
    1.21 +
    1.22 +code_datatype AList
    1.23 +
    1.24 +lemma lookup_AList [simp, code]:
    1.25 +  "Mapping.lookup (AList xs) = map_of xs"
    1.26 +  by (simp add: AList_def)
    1.27 +
    1.28 +lemma empty_AList [code]:
    1.29 +  "Mapping.empty = AList []"
    1.30 +  by (rule mapping_eqI) simp
    1.31 +
    1.32 +lemma is_empty_AList [code]:
    1.33 +  "Mapping.is_empty (AList xs) \<longleftrightarrow> null xs"
    1.34 +  by (cases xs) (simp_all add: is_empty_def)
    1.35 +
    1.36 +lemma update_AList [code]:
    1.37 +  "Mapping.update k v (AList xs) = AList (update k v xs)"
    1.38 +  by (rule mapping_eqI) (simp add: update_conv')
    1.39 +
    1.40 +lemma delete_AList [code]:
    1.41 +  "Mapping.delete k (AList xs) = AList (delete k xs)"
    1.42 +  by (rule mapping_eqI) (simp add: delete_conv')
    1.43 +
    1.44 +lemma keys_AList [code]:
    1.45 +  "Mapping.keys (AList xs) = set (map fst xs)"
    1.46 +  by (simp add: keys_def dom_map_of_conv_image_fst)
    1.47 +
    1.48 +lemma size_AList [code]:
    1.49 +  "Mapping.size (AList xs) = length (remdups (map fst xs))"
    1.50 +  by (simp add: size_def length_remdups_card_conv dom_map_of_conv_image_fst)
    1.51 +
    1.52 +lemma tabulate_AList [code]:
    1.53 +  "Mapping.tabulate ks f = AList (map (\<lambda>k. (k, f k)) ks)"
    1.54 +  by (rule mapping_eqI) (simp add: map_of_map_restrict)
    1.55 +
    1.56 +lemma bulkload_AList [code]:
    1.57 +  "Mapping.bulkload vs = AList (map (\<lambda>n. (n, vs ! n)) [0..<length vs])"
    1.58 +  by (rule mapping_eqI) (simp add: map_of_map_restrict expand_fun_eq)
    1.59 +
    1.60  end