src/HOL/Library/AList_Mapping.thy
changeset 44897 787983a08bfb
child 44913 48240fb48980
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/AList_Mapping.thy	Mon Sep 12 10:57:58 2011 +0200
     1.3 @@ -0,0 +1,72 @@
     1.4 +(* Title: HOL/Library/AList_Mapping.thy
     1.5 +   Author: Florian Haftmann, TU Muenchen
     1.6 +*)
     1.7 +
     1.8 +header {* Implementation of mappings with Association Lists *}
     1.9 +
    1.10 +theory AList_Mapping
    1.11 +imports AList_Impl Mapping
    1.12 +begin
    1.13 +
    1.14 +definition Mapping :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) mapping" where
    1.15 +  "Mapping xs = Mapping.Mapping (map_of xs)"
    1.16 +
    1.17 +code_datatype Mapping
    1.18 +
    1.19 +lemma lookup_Mapping [simp, code]:
    1.20 +  "Mapping.lookup (Mapping xs) = map_of xs"
    1.21 +  by (simp add: Mapping_def)
    1.22 +
    1.23 +lemma keys_Mapping [simp, code]:
    1.24 +  "Mapping.keys (Mapping xs) = set (map fst xs)"
    1.25 +  by (simp add: keys_def dom_map_of_conv_image_fst)
    1.26 +
    1.27 +lemma empty_Mapping [code]:
    1.28 +  "Mapping.empty = Mapping []"
    1.29 +  by (rule mapping_eqI) simp
    1.30 +
    1.31 +lemma is_empty_Mapping [code]:
    1.32 +  "Mapping.is_empty (Mapping xs) \<longleftrightarrow> List.null xs"
    1.33 +  by (cases xs) (simp_all add: is_empty_def null_def)
    1.34 +
    1.35 +lemma update_Mapping [code]:
    1.36 +  "Mapping.update k v (Mapping xs) = Mapping (update k v xs)"
    1.37 +  by (rule mapping_eqI) (simp add: update_conv')
    1.38 +
    1.39 +lemma delete_Mapping [code]:
    1.40 +  "Mapping.delete k (Mapping xs) = Mapping (delete k xs)"
    1.41 +  by (rule mapping_eqI) (simp add: delete_conv')
    1.42 +
    1.43 +lemma ordered_keys_Mapping [code]:
    1.44 +  "Mapping.ordered_keys (Mapping xs) = sort (remdups (map fst xs))"
    1.45 +  by (simp only: ordered_keys_def keys_Mapping sorted_list_of_set_sort_remdups) simp
    1.46 +
    1.47 +lemma size_Mapping [code]:
    1.48 +  "Mapping.size (Mapping xs) = length (remdups (map fst xs))"
    1.49 +  by (simp add: size_def length_remdups_card_conv dom_map_of_conv_image_fst)
    1.50 +
    1.51 +lemma tabulate_Mapping [code]:
    1.52 +  "Mapping.tabulate ks f = Mapping (map (\<lambda>k. (k, f k)) ks)"
    1.53 +  by (rule mapping_eqI) (simp add: map_of_map_restrict)
    1.54 +
    1.55 +lemma bulkload_Mapping [code]:
    1.56 +  "Mapping.bulkload vs = Mapping (map (\<lambda>n. (n, vs ! n)) [0..<length vs])"
    1.57 +  by (rule mapping_eqI) (simp add: map_of_map_restrict fun_eq_iff)
    1.58 +
    1.59 +lemma equal_Mapping [code]:
    1.60 +  "HOL.equal (Mapping xs) (Mapping ys) \<longleftrightarrow>
    1.61 +    (let ks = map fst xs; ls = map fst ys
    1.62 +    in (\<forall>l\<in>set ls. l \<in> set ks) \<and> (\<forall>k\<in>set ks. k \<in> set ls \<and> map_of xs k = map_of ys k))"
    1.63 +proof -
    1.64 +  have aux: "\<And>a b xs. (a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs"
    1.65 +    by (auto simp add: image_def intro!: bexI)
    1.66 +  show ?thesis
    1.67 +    by (auto intro!: map_of_eqI simp add: Let_def equal Mapping_def)
    1.68 +      (auto dest!: map_of_eq_dom intro: aux)
    1.69 +qed
    1.70 +
    1.71 +lemma [code nbe]:
    1.72 +  "HOL.equal (x :: ('a, 'b) mapping) x \<longleftrightarrow> True"
    1.73 +  by (fact equal_refl)
    1.74 +  
    1.75 +end
    1.76 \ No newline at end of file