src/HOL/Library/AList_Mapping.thy
author paulson <lp15@cam.ac.uk>
Mon Feb 22 14:37:56 2016 +0000 (2016-02-22)
changeset 62379 340738057c8c
parent 60500 903bb1495239
child 63194 0b7bdb75f451
permissions -rw-r--r--
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
bulwahn@44897
     1
(* Title: HOL/Library/AList_Mapping.thy
bulwahn@44897
     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
bulwahn@46238
     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
bulwahn@44897
    15
lemma lookup_Mapping [simp, code]:
bulwahn@44897
    16
  "Mapping.lookup (Mapping xs) = map_of xs"
kuncar@49929
    17
  by transfer rule
bulwahn@44897
    18
bulwahn@44897
    19
lemma keys_Mapping [simp, code]:
kuncar@49929
    20
  "Mapping.keys (Mapping xs) = set (map fst xs)" 
kuncar@49929
    21
  by transfer (simp add: dom_map_of_conv_image_fst)
bulwahn@44897
    22
bulwahn@44897
    23
lemma empty_Mapping [code]:
bulwahn@44897
    24
  "Mapping.empty = Mapping []"
kuncar@49929
    25
  by transfer simp
bulwahn@44897
    26
bulwahn@44897
    27
lemma is_empty_Mapping [code]:
bulwahn@44897
    28
  "Mapping.is_empty (Mapping xs) \<longleftrightarrow> List.null xs"
kuncar@49929
    29
  by (case_tac xs) (simp_all add: is_empty_def null_def)
bulwahn@44897
    30
bulwahn@44897
    31
lemma update_Mapping [code]:
bulwahn@46238
    32
  "Mapping.update k v (Mapping xs) = Mapping (AList.update k v xs)"
kuncar@49929
    33
  by transfer (simp add: update_conv')
bulwahn@44897
    34
bulwahn@44897
    35
lemma delete_Mapping [code]:
bulwahn@46238
    36
  "Mapping.delete k (Mapping xs) = Mapping (AList.delete k xs)"
kuncar@49929
    37
  by transfer (simp add: delete_conv')
bulwahn@44897
    38
bulwahn@44897
    39
lemma ordered_keys_Mapping [code]:
bulwahn@44897
    40
  "Mapping.ordered_keys (Mapping xs) = sort (remdups (map fst xs))"
bulwahn@44897
    41
  by (simp only: ordered_keys_def keys_Mapping sorted_list_of_set_sort_remdups) simp
bulwahn@44897
    42
bulwahn@44897
    43
lemma size_Mapping [code]:
bulwahn@44897
    44
  "Mapping.size (Mapping xs) = length (remdups (map fst xs))"
bulwahn@44897
    45
  by (simp add: size_def length_remdups_card_conv dom_map_of_conv_image_fst)
bulwahn@44897
    46
bulwahn@44897
    47
lemma tabulate_Mapping [code]:
bulwahn@44897
    48
  "Mapping.tabulate ks f = Mapping (map (\<lambda>k. (k, f k)) ks)"
kuncar@49929
    49
  by transfer (simp add: map_of_map_restrict)
bulwahn@44897
    50
bulwahn@44897
    51
lemma bulkload_Mapping [code]:
bulwahn@44897
    52
  "Mapping.bulkload vs = Mapping (map (\<lambda>n. (n, vs ! n)) [0..<length vs])"
kuncar@49929
    53
  by transfer (simp add: map_of_map_restrict fun_eq_iff)
bulwahn@44897
    54
bulwahn@44897
    55
lemma equal_Mapping [code]:
bulwahn@44897
    56
  "HOL.equal (Mapping xs) (Mapping ys) \<longleftrightarrow>
bulwahn@44897
    57
    (let ks = map fst xs; ls = map fst ys
bulwahn@44897
    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))"
bulwahn@44897
    59
proof -
bulwahn@44897
    60
  have aux: "\<And>a b xs. (a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs"
bulwahn@44897
    61
    by (auto simp add: image_def intro!: bexI)
haftmann@51161
    62
  show ?thesis apply transfer
wenzelm@57850
    63
    by (auto intro!: map_of_eqI) (auto dest!: map_of_eq_dom intro: aux)
bulwahn@44897
    64
qed
bulwahn@44897
    65
bulwahn@44897
    66
lemma [code nbe]:
bulwahn@44897
    67
  "HOL.equal (x :: ('a, 'b) mapping) x \<longleftrightarrow> True"
bulwahn@44897
    68
  by (fact equal_refl)
haftmann@59487
    69
bulwahn@44913
    70
end
haftmann@59487
    71