src/HOL/Library/AList_Mapping.thy
author wenzelm
Wed Sep 12 13:42:28 2012 +0200 (2012-09-12)
changeset 49322 fbb320d02420
parent 46238 9ace9e5b79be
child 49929 70300f1b6835
permissions -rw-r--r--
tuned headers;
     1 (* Title: HOL/Library/AList_Mapping.thy
     2    Author: Florian Haftmann, TU Muenchen
     3 *)
     4 
     5 header {* Implementation of mappings with Association Lists *}
     6 
     7 theory AList_Mapping
     8 imports AList Mapping
     9 begin
    10 
    11 definition Mapping :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) mapping" where
    12   "Mapping xs = Mapping.Mapping (map_of xs)"
    13 
    14 code_datatype Mapping
    15 
    16 lemma lookup_Mapping [simp, code]:
    17   "Mapping.lookup (Mapping xs) = map_of xs"
    18   by (simp add: Mapping_def)
    19 
    20 lemma keys_Mapping [simp, code]:
    21   "Mapping.keys (Mapping xs) = set (map fst xs)"
    22   by (simp add: keys_def dom_map_of_conv_image_fst)
    23 
    24 lemma empty_Mapping [code]:
    25   "Mapping.empty = Mapping []"
    26   by (rule mapping_eqI) simp
    27 
    28 lemma is_empty_Mapping [code]:
    29   "Mapping.is_empty (Mapping xs) \<longleftrightarrow> List.null xs"
    30   by (cases xs) (simp_all add: is_empty_def null_def)
    31 
    32 lemma update_Mapping [code]:
    33   "Mapping.update k v (Mapping xs) = Mapping (AList.update k v xs)"
    34   by (rule mapping_eqI) (simp add: update_conv')
    35 
    36 lemma delete_Mapping [code]:
    37   "Mapping.delete k (Mapping xs) = Mapping (AList.delete k xs)"
    38   by (rule mapping_eqI) (simp add: delete_conv')
    39 
    40 lemma ordered_keys_Mapping [code]:
    41   "Mapping.ordered_keys (Mapping xs) = sort (remdups (map fst xs))"
    42   by (simp only: ordered_keys_def keys_Mapping sorted_list_of_set_sort_remdups) simp
    43 
    44 lemma size_Mapping [code]:
    45   "Mapping.size (Mapping xs) = length (remdups (map fst xs))"
    46   by (simp add: size_def length_remdups_card_conv dom_map_of_conv_image_fst)
    47 
    48 lemma tabulate_Mapping [code]:
    49   "Mapping.tabulate ks f = Mapping (map (\<lambda>k. (k, f k)) ks)"
    50   by (rule mapping_eqI) (simp add: map_of_map_restrict)
    51 
    52 lemma bulkload_Mapping [code]:
    53   "Mapping.bulkload vs = Mapping (map (\<lambda>n. (n, vs ! n)) [0..<length vs])"
    54   by (rule mapping_eqI) (simp add: map_of_map_restrict fun_eq_iff)
    55 
    56 lemma equal_Mapping [code]:
    57   "HOL.equal (Mapping xs) (Mapping ys) \<longleftrightarrow>
    58     (let ks = map fst xs; ls = map fst ys
    59     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))"
    60 proof -
    61   have aux: "\<And>a b xs. (a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs"
    62     by (auto simp add: image_def intro!: bexI)
    63   show ?thesis
    64     by (auto intro!: map_of_eqI simp add: Let_def equal Mapping_def)
    65       (auto dest!: map_of_eq_dom intro: aux)
    66 qed
    67 
    68 lemma [code nbe]:
    69   "HOL.equal (x :: ('a, 'b) mapping) x \<longleftrightarrow> True"
    70   by (fact equal_refl)
    71   
    72 end