src/HOL/Library/Mapping.thy
author wenzelm
Thu Feb 11 23:00:22 2010 +0100 (2010-02-11)
changeset 35115 446c5063e4fd
parent 33640 0d82107dc07a
child 35157 73cd6f78c86d
permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
haftmann@31459
     1
(* Author: Florian Haftmann, TU Muenchen *)
haftmann@29708
     2
haftmann@29708
     3
header {* An abstract view on maps for code generation. *}
haftmann@29708
     4
haftmann@29708
     5
theory Mapping
haftmann@30663
     6
imports Map Main
haftmann@29708
     7
begin
haftmann@29708
     8
haftmann@29708
     9
subsection {* Type definition and primitive operations *}
haftmann@29708
    10
haftmann@29708
    11
datatype ('a, 'b) map = Map "'a \<rightharpoonup> 'b"
haftmann@29708
    12
haftmann@29708
    13
definition empty :: "('a, 'b) map" where
haftmann@29708
    14
  "empty = Map (\<lambda>_. None)"
haftmann@29708
    15
haftmann@29708
    16
primrec lookup :: "('a, 'b) map \<Rightarrow> 'a \<rightharpoonup> 'b" where
haftmann@29708
    17
  "lookup (Map f) = f"
haftmann@29708
    18
haftmann@29708
    19
primrec update :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) map \<Rightarrow> ('a, 'b) map" where
haftmann@29708
    20
  "update k v (Map f) = Map (f (k \<mapsto> v))"
haftmann@29708
    21
haftmann@29708
    22
primrec delete :: "'a \<Rightarrow> ('a, 'b) map \<Rightarrow> ('a, 'b) map" where
haftmann@29708
    23
  "delete k (Map f) = Map (f (k := None))"
haftmann@29708
    24
haftmann@29708
    25
primrec keys :: "('a, 'b) map \<Rightarrow> 'a set" where
haftmann@29708
    26
  "keys (Map f) = dom f"
haftmann@29708
    27
haftmann@29708
    28
haftmann@29708
    29
subsection {* Derived operations *}
haftmann@29708
    30
haftmann@29708
    31
definition size :: "('a, 'b) map \<Rightarrow> nat" where
haftmann@29708
    32
  "size m = (if finite (keys m) then card (keys m) else 0)"
haftmann@29708
    33
haftmann@29814
    34
definition replace :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) map \<Rightarrow> ('a, 'b) map" where
haftmann@29814
    35
  "replace k v m = (if lookup m k = None then m else update k v m)"
haftmann@29814
    36
haftmann@29708
    37
definition tabulate :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) map" where
haftmann@29708
    38
  "tabulate ks f = Map (map_of (map (\<lambda>k. (k, f k)) ks))"
haftmann@29708
    39
haftmann@29826
    40
definition bulkload :: "'a list \<Rightarrow> (nat, 'a) map" where
haftmann@29826
    41
  "bulkload xs = Map (\<lambda>k. if k < length xs then Some (xs ! k) else None)"
haftmann@29826
    42
haftmann@29708
    43
haftmann@29708
    44
subsection {* Properties *}
haftmann@29708
    45
haftmann@29708
    46
lemma lookup_inject:
haftmann@29708
    47
  "lookup m = lookup n \<longleftrightarrow> m = n"
haftmann@29708
    48
  by (cases m, cases n) simp
haftmann@29708
    49
haftmann@29708
    50
lemma lookup_empty [simp]:
haftmann@29708
    51
  "lookup empty = Map.empty"
haftmann@29708
    52
  by (simp add: empty_def)
haftmann@29708
    53
haftmann@29708
    54
lemma lookup_update [simp]:
haftmann@29708
    55
  "lookup (update k v m) = (lookup m) (k \<mapsto> v)"
haftmann@29708
    56
  by (cases m) simp
haftmann@29708
    57
haftmann@29708
    58
lemma lookup_delete:
haftmann@29708
    59
  "lookup (delete k m) k = None"
haftmann@29708
    60
  "k \<noteq> l \<Longrightarrow> lookup (delete k m) l = lookup m l"
haftmann@29708
    61
  by (cases m, simp)+
haftmann@29708
    62
haftmann@29708
    63
lemma lookup_tabulate:
haftmann@29708
    64
  "lookup (tabulate ks f) = (Some o f) |` set ks"
haftmann@29708
    65
  by (induct ks) (auto simp add: tabulate_def restrict_map_def expand_fun_eq)
haftmann@29708
    66
haftmann@29826
    67
lemma lookup_bulkload:
haftmann@29826
    68
  "lookup (bulkload xs) = (\<lambda>k. if k < length xs then Some (xs ! k) else None)"
haftmann@29826
    69
  unfolding bulkload_def by simp
haftmann@29826
    70
haftmann@29708
    71
lemma update_update:
haftmann@29708
    72
  "update k v (update k w m) = update k v m"
haftmann@29708
    73
  "k \<noteq> l \<Longrightarrow> update k v (update l w m) = update l w (update k v m)"
haftmann@29708
    74
  by (cases m, simp add: expand_fun_eq)+
haftmann@29708
    75
haftmann@29814
    76
lemma replace_update:
haftmann@29814
    77
  "lookup m k = None \<Longrightarrow> replace k v m = m"
haftmann@29814
    78
  "lookup m k \<noteq> None \<Longrightarrow> replace k v m = update k v m"
haftmann@29814
    79
  by (auto simp add: replace_def)
haftmann@29814
    80
haftmann@29708
    81
lemma delete_empty [simp]:
haftmann@29708
    82
  "delete k empty = empty"
haftmann@29708
    83
  by (simp add: empty_def)
haftmann@29708
    84
haftmann@29708
    85
lemma delete_update:
haftmann@29708
    86
  "delete k (update k v m) = delete k m"
haftmann@29708
    87
  "k \<noteq> l \<Longrightarrow> delete k (update l v m) = update l v (delete k m)"
haftmann@29708
    88
  by (cases m, simp add: expand_fun_eq)+
haftmann@29708
    89
haftmann@29708
    90
lemma update_delete [simp]:
haftmann@29708
    91
  "update k v (delete k m) = update k v m"
haftmann@29708
    92
  by (cases m) simp
haftmann@29708
    93
haftmann@29708
    94
lemma keys_empty [simp]:
haftmann@29708
    95
  "keys empty = {}"
haftmann@29708
    96
  unfolding empty_def by simp
haftmann@29708
    97
haftmann@29708
    98
lemma keys_update [simp]:
haftmann@29708
    99
  "keys (update k v m) = insert k (keys m)"
haftmann@29708
   100
  by (cases m) simp
haftmann@29708
   101
haftmann@29708
   102
lemma keys_delete [simp]:
haftmann@29708
   103
  "keys (delete k m) = keys m - {k}"
haftmann@29708
   104
  by (cases m) simp
haftmann@29708
   105
haftmann@29708
   106
lemma keys_tabulate [simp]:
haftmann@29708
   107
  "keys (tabulate ks f) = set ks"
haftmann@29708
   108
  by (auto simp add: tabulate_def dest: map_of_SomeD intro!: weak_map_of_SomeI)
haftmann@29708
   109
haftmann@29708
   110
lemma size_empty [simp]:
haftmann@29708
   111
  "size empty = 0"
haftmann@29708
   112
  by (simp add: size_def keys_empty)
haftmann@29708
   113
haftmann@29708
   114
lemma size_update:
haftmann@29708
   115
  "finite (keys m) \<Longrightarrow> size (update k v m) =
haftmann@29708
   116
    (if k \<in> keys m then size m else Suc (size m))"
haftmann@29708
   117
  by (simp add: size_def keys_update)
haftmann@29708
   118
    (auto simp only: card_insert card_Suc_Diff1)
haftmann@29708
   119
haftmann@29708
   120
lemma size_delete:
haftmann@29708
   121
  "size (delete k m) = (if k \<in> keys m then size m - 1 else size m)"
haftmann@29708
   122
  by (simp add: size_def keys_delete)
haftmann@29708
   123
haftmann@29708
   124
lemma size_tabulate:
haftmann@29708
   125
  "size (tabulate ks f) = length (remdups ks)"
haftmann@29708
   126
  by (simp add: size_def keys_tabulate distinct_card [of "remdups ks", symmetric])
haftmann@29708
   127
haftmann@29831
   128
lemma bulkload_tabulate:
haftmann@29826
   129
  "bulkload xs = tabulate [0..<length xs] (nth xs)"
haftmann@29831
   130
  by (rule sym)
hoelzl@33640
   131
    (auto simp add: bulkload_def tabulate_def expand_fun_eq map_of_eq_None_iff comp_def)
haftmann@29826
   132
haftmann@31459
   133
haftmann@31459
   134
subsection {* Some technical code lemmas *}
haftmann@31459
   135
haftmann@31459
   136
lemma [code]:
haftmann@31459
   137
  "map_case f m = f (Mapping.lookup m)"
haftmann@31459
   138
  by (cases m) simp
haftmann@31459
   139
haftmann@31459
   140
lemma [code]:
haftmann@31459
   141
  "map_rec f m = f (Mapping.lookup m)"
haftmann@31459
   142
  by (cases m) simp
haftmann@31459
   143
haftmann@31459
   144
lemma [code]:
haftmann@31459
   145
  "Nat.size (m :: (_, _) map) = 0"
haftmann@31459
   146
  by (cases m) simp
haftmann@31459
   147
haftmann@31459
   148
lemma [code]:
haftmann@31459
   149
  "map_size f g m = 0"
haftmann@31459
   150
  by (cases m) simp
haftmann@31459
   151
haftmann@29708
   152
end