src/HOL/Library/AList_Mapping.thy
author bulwahn
Mon, 12 Sep 2011 10:57:58 +0200
changeset 44897 787983a08bfb
child 44913 48240fb48980
permissions -rw-r--r--
moving connection of association lists to Mappings into a separate theory
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
44897
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
     1
(* Title: HOL/Library/AList_Mapping.thy
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
     2
   Author: Florian Haftmann, TU Muenchen
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
     3
*)
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
     4
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
     5
header {* Implementation of mappings with Association Lists *}
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
     6
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
     7
theory AList_Mapping
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
     8
imports AList_Impl Mapping
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
     9
begin
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    10
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    11
definition Mapping :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) mapping" where
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    12
  "Mapping xs = Mapping.Mapping (map_of xs)"
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    13
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    14
code_datatype Mapping
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    15
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    16
lemma lookup_Mapping [simp, code]:
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    17
  "Mapping.lookup (Mapping xs) = map_of xs"
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    18
  by (simp add: Mapping_def)
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    19
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    20
lemma keys_Mapping [simp, code]:
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    21
  "Mapping.keys (Mapping xs) = set (map fst xs)"
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    22
  by (simp add: keys_def dom_map_of_conv_image_fst)
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    23
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    24
lemma empty_Mapping [code]:
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    25
  "Mapping.empty = Mapping []"
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    26
  by (rule mapping_eqI) simp
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    27
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    28
lemma is_empty_Mapping [code]:
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    29
  "Mapping.is_empty (Mapping xs) \<longleftrightarrow> List.null xs"
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    30
  by (cases xs) (simp_all add: is_empty_def null_def)
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    31
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    32
lemma update_Mapping [code]:
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    33
  "Mapping.update k v (Mapping xs) = Mapping (update k v xs)"
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    34
  by (rule mapping_eqI) (simp add: update_conv')
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    35
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    36
lemma delete_Mapping [code]:
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    37
  "Mapping.delete k (Mapping xs) = Mapping (delete k xs)"
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    38
  by (rule mapping_eqI) (simp add: delete_conv')
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    39
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    40
lemma ordered_keys_Mapping [code]:
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    41
  "Mapping.ordered_keys (Mapping xs) = sort (remdups (map fst xs))"
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    42
  by (simp only: ordered_keys_def keys_Mapping sorted_list_of_set_sort_remdups) simp
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    43
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    44
lemma size_Mapping [code]:
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    45
  "Mapping.size (Mapping xs) = length (remdups (map fst xs))"
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    46
  by (simp add: size_def length_remdups_card_conv dom_map_of_conv_image_fst)
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    47
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    48
lemma tabulate_Mapping [code]:
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    49
  "Mapping.tabulate ks f = Mapping (map (\<lambda>k. (k, f k)) ks)"
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    50
  by (rule mapping_eqI) (simp add: map_of_map_restrict)
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    51
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    52
lemma bulkload_Mapping [code]:
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    53
  "Mapping.bulkload vs = Mapping (map (\<lambda>n. (n, vs ! n)) [0..<length vs])"
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    54
  by (rule mapping_eqI) (simp add: map_of_map_restrict fun_eq_iff)
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    55
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    56
lemma equal_Mapping [code]:
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    57
  "HOL.equal (Mapping xs) (Mapping ys) \<longleftrightarrow>
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    58
    (let ks = map fst xs; ls = map fst ys
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    59
    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))"
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    60
proof -
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    61
  have aux: "\<And>a b xs. (a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs"
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    62
    by (auto simp add: image_def intro!: bexI)
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    63
  show ?thesis
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    64
    by (auto intro!: map_of_eqI simp add: Let_def equal Mapping_def)
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    65
      (auto dest!: map_of_eq_dom intro: aux)
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    66
qed
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    67
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    68
lemma [code nbe]:
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    69
  "HOL.equal (x :: ('a, 'b) mapping) x \<longleftrightarrow> True"
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    70
  by (fact equal_refl)
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    71
  
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff changeset
    72
end