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