src/HOL/Library/AList_Mapping.thy
 author Andreas Lochbihler Fri Sep 20 10:09:16 2013 +0200 (2013-09-20) changeset 53745 788730ab7da4 parent 51161 6ed12ae3b3e1 child 57850 34382a1f37d6 permissions -rw-r--r--
prefer Code.abort over code_abort
```     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 lift_definition Mapping :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) mapping" is map_of .
```
```    12
```
```    13 code_datatype Mapping
```
```    14
```
```    15 lemma lookup_Mapping [simp, code]:
```
```    16   "Mapping.lookup (Mapping xs) = map_of xs"
```
```    17   by transfer rule
```
```    18
```
```    19 lemma keys_Mapping [simp, code]:
```
```    20   "Mapping.keys (Mapping xs) = set (map fst xs)"
```
```    21   by transfer (simp add: dom_map_of_conv_image_fst)
```
```    22
```
```    23 lemma empty_Mapping [code]:
```
```    24   "Mapping.empty = Mapping []"
```
```    25   by transfer simp
```
```    26
```
```    27 lemma is_empty_Mapping [code]:
```
```    28   "Mapping.is_empty (Mapping xs) \<longleftrightarrow> List.null xs"
```
```    29   by (case_tac xs) (simp_all add: is_empty_def null_def)
```
```    30
```
```    31 lemma update_Mapping [code]:
```
```    32   "Mapping.update k v (Mapping xs) = Mapping (AList.update k v xs)"
```
```    33   by transfer (simp add: update_conv')
```
```    34
```
```    35 lemma delete_Mapping [code]:
```
```    36   "Mapping.delete k (Mapping xs) = Mapping (AList.delete k xs)"
```
```    37   by transfer (simp add: delete_conv')
```
```    38
```
```    39 lemma ordered_keys_Mapping [code]:
```
```    40   "Mapping.ordered_keys (Mapping xs) = sort (remdups (map fst xs))"
```
```    41   by (simp only: ordered_keys_def keys_Mapping sorted_list_of_set_sort_remdups) simp
```
```    42
```
```    43 lemma size_Mapping [code]:
```
```    44   "Mapping.size (Mapping xs) = length (remdups (map fst xs))"
```
```    45   by (simp add: size_def length_remdups_card_conv dom_map_of_conv_image_fst)
```
```    46
```
```    47 lemma tabulate_Mapping [code]:
```
```    48   "Mapping.tabulate ks f = Mapping (map (\<lambda>k. (k, f k)) ks)"
```
```    49   by transfer (simp add: map_of_map_restrict)
```
```    50
```
```    51 lemma bulkload_Mapping [code]:
```
```    52   "Mapping.bulkload vs = Mapping (map (\<lambda>n. (n, vs ! n)) [0..<length vs])"
```
```    53   by transfer (simp add: map_of_map_restrict fun_eq_iff)
```
```    54
```
```    55 lemma equal_Mapping [code]:
```
```    56   "HOL.equal (Mapping xs) (Mapping ys) \<longleftrightarrow>
```
```    57     (let ks = map fst xs; ls = map fst ys
```
```    58     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))"
```
```    59 proof -
```
```    60   have aux: "\<And>a b xs. (a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs"
```
```    61     by (auto simp add: image_def intro!: bexI)
```
```    62   show ?thesis apply transfer
```
```    63   by (auto intro!: map_of_eqI) (auto dest!: map_of_eq_dom intro: aux)
```
```    64 qed
```
```    65
```
```    66 lemma [code nbe]:
```
```    67   "HOL.equal (x :: ('a, 'b) mapping) x \<longleftrightarrow> True"
```
```    68   by (fact equal_refl)
```
```    69
```
```    70 end
```