src/HOL/Library/AList_Mapping.thy
 author Manuel Eberl Mon Mar 26 16:14:16 2018 +0200 (19 months ago) changeset 67951 655aa11359dc parent 63649 e690d6f2185b permissions -rw-r--r--
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
```     1 (*  Title:      HOL/Library/AList_Mapping.thy
```
```     2     Author:     Florian Haftmann, TU Muenchen
```
```     3 *)
```
```     4
```
```     5 section \<open>Implementation of mappings with Association Lists\<close>
```
```     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]: "Mapping.lookup (Mapping xs) = map_of xs"
```
```    16   by transfer rule
```
```    17
```
```    18 lemma keys_Mapping [simp, code]: "Mapping.keys (Mapping xs) = set (map fst xs)"
```
```    19   by transfer (simp add: dom_map_of_conv_image_fst)
```
```    20
```
```    21 lemma empty_Mapping [code]: "Mapping.empty = Mapping []"
```
```    22   by transfer simp
```
```    23
```
```    24 lemma is_empty_Mapping [code]: "Mapping.is_empty (Mapping xs) \<longleftrightarrow> List.null xs"
```
```    25   by (cases xs) (simp_all add: is_empty_def null_def)
```
```    26
```
```    27 lemma update_Mapping [code]: "Mapping.update k v (Mapping xs) = Mapping (AList.update k v xs)"
```
```    28   by transfer (simp add: update_conv')
```
```    29
```
```    30 lemma delete_Mapping [code]: "Mapping.delete k (Mapping xs) = Mapping (AList.delete k xs)"
```
```    31   by transfer (simp add: delete_conv')
```
```    32
```
```    33 lemma ordered_keys_Mapping [code]:
```
```    34   "Mapping.ordered_keys (Mapping xs) = sort (remdups (map fst xs))"
```
```    35   by (simp only: ordered_keys_def keys_Mapping sorted_list_of_set_sort_remdups) simp
```
```    36
```
```    37 lemma size_Mapping [code]: "Mapping.size (Mapping xs) = length (remdups (map fst xs))"
```
```    38   by (simp add: size_def length_remdups_card_conv dom_map_of_conv_image_fst)
```
```    39
```
```    40 lemma tabulate_Mapping [code]: "Mapping.tabulate ks f = Mapping (map (\<lambda>k. (k, f k)) ks)"
```
```    41   by transfer (simp add: map_of_map_restrict)
```
```    42
```
```    43 lemma bulkload_Mapping [code]:
```
```    44   "Mapping.bulkload vs = Mapping (map (\<lambda>n. (n, vs ! n)) [0..<length vs])"
```
```    45   by transfer (simp add: map_of_map_restrict fun_eq_iff)
```
```    46
```
```    47 lemma equal_Mapping [code]:
```
```    48   "HOL.equal (Mapping xs) (Mapping ys) \<longleftrightarrow>
```
```    49     (let ks = map fst xs; ls = map fst ys
```
```    50      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))"
```
```    51 proof -
```
```    52   have *: "(a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs" for a b xs
```
```    53     by (auto simp add: image_def intro!: bexI)
```
```    54   show ?thesis
```
```    55     apply transfer
```
```    56     apply (auto intro!: map_of_eqI)
```
```    57      apply (auto dest!: map_of_eq_dom intro: *)
```
```    58     done
```
```    59 qed
```
```    60
```
```    61 lemma map_values_Mapping [code]:
```
```    62   "Mapping.map_values f (Mapping xs) = Mapping (map (\<lambda>(x,y). (x, f x y)) xs)"
```
```    63   for f :: "'c \<Rightarrow> 'a \<Rightarrow> 'b" and xs :: "('c \<times> 'a) list"
```
```    64   apply transfer
```
```    65   apply (rule ext)
```
```    66   subgoal for f xs x by (induct xs) auto
```
```    67   done
```
```    68
```
```    69 lemma combine_with_key_code [code]:
```
```    70   "Mapping.combine_with_key f (Mapping xs) (Mapping ys) =
```
```    71      Mapping.tabulate (remdups (map fst xs @ map fst ys))
```
```    72        (\<lambda>x. the (combine_options (f x) (map_of xs x) (map_of ys x)))"
```
```    73   apply transfer
```
```    74   apply (rule ext)
```
```    75   apply (rule sym)
```
```    76   subgoal for f xs ys x
```
```    77     apply (cases "map_of xs x"; cases "map_of ys x"; simp)
```
```    78        apply (force simp: map_of_eq_None_iff combine_options_def option.the_def o_def image_iff
```
```    79         dest: map_of_SomeD split: option.splits)+
```
```    80     done
```
```    81   done
```
```    82
```
```    83 lemma combine_code [code]:
```
```    84   "Mapping.combine f (Mapping xs) (Mapping ys) =
```
```    85      Mapping.tabulate (remdups (map fst xs @ map fst ys))
```
```    86        (\<lambda>x. the (combine_options f (map_of xs x) (map_of ys x)))"
```
```    87   apply transfer
```
```    88   apply (rule ext)
```
```    89   apply (rule sym)
```
```    90   subgoal for f xs ys x
```
```    91     apply (cases "map_of xs x"; cases "map_of ys x"; simp)
```
```    92        apply (force simp: map_of_eq_None_iff combine_options_def option.the_def o_def image_iff
```
```    93         dest: map_of_SomeD split: option.splits)+
```
```    94     done
```
```    95   done
```
```    96
```
```    97 lemma map_of_filter_distinct:  (* TODO: move? *)
```
```    98   assumes "distinct (map fst xs)"
```
```    99   shows "map_of (filter P xs) x =
```
```   100     (case map_of xs x of
```
```   101       None \<Rightarrow> None
```
```   102     | Some y \<Rightarrow> if P (x,y) then Some y else None)"
```
```   103   using assms
```
```   104   by (auto simp: map_of_eq_None_iff filter_map distinct_map_filter dest: map_of_SomeD
```
```   105       simp del: map_of_eq_Some_iff intro!: map_of_is_SomeI split: option.splits)
```
```   106
```
```   107 lemma filter_Mapping [code]:
```
```   108   "Mapping.filter P (Mapping xs) = Mapping (filter (\<lambda>(k,v). P k v) (AList.clearjunk xs))"
```
```   109   apply transfer
```
```   110   apply (rule ext)
```
```   111   apply (subst map_of_filter_distinct)
```
```   112    apply (simp_all add: map_of_clearjunk split: option.split)
```
```   113   done
```
```   114
```
```   115 lemma [code nbe]: "HOL.equal (x :: ('a, 'b) mapping) x \<longleftrightarrow> True"
```
```   116   by (fact equal_refl)
```
```   117
```
```   118 end
```