src/HOL/Library/AList_Mapping.thy
author wenzelm
Tue May 15 13:57:39 2018 +0200 (16 months ago)
changeset 68189 6163c90694ef
parent 63649 e690d6f2185b
permissions -rw-r--r--
tuned headers;
     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