src/HOL/Library/Mapping.thy
author haftmann
Mon Feb 02 13:56:22 2009 +0100 (2009-02-02)
changeset 29708 e40b70d38909
child 29814 15344c0899e1
permissions -rw-r--r--
added Mapping.thy to Library
haftmann@29708
     1
(*  Title:      HOL/Library/Mapping.thy
haftmann@29708
     2
    Author:     Florian Haftmann, TU Muenchen
haftmann@29708
     3
*)
haftmann@29708
     4
haftmann@29708
     5
header {* An abstract view on maps for code generation. *}
haftmann@29708
     6
haftmann@29708
     7
theory Mapping
haftmann@29708
     8
imports Map
haftmann@29708
     9
begin
haftmann@29708
    10
haftmann@29708
    11
subsection {* Type definition and primitive operations *}
haftmann@29708
    12
haftmann@29708
    13
datatype ('a, 'b) map = Map "'a \<rightharpoonup> 'b"
haftmann@29708
    14
haftmann@29708
    15
definition empty :: "('a, 'b) map" where
haftmann@29708
    16
  "empty = Map (\<lambda>_. None)"
haftmann@29708
    17
haftmann@29708
    18
primrec lookup :: "('a, 'b) map \<Rightarrow> 'a \<rightharpoonup> 'b" where
haftmann@29708
    19
  "lookup (Map f) = f"
haftmann@29708
    20
haftmann@29708
    21
primrec update :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) map \<Rightarrow> ('a, 'b) map" where
haftmann@29708
    22
  "update k v (Map f) = Map (f (k \<mapsto> v))"
haftmann@29708
    23
haftmann@29708
    24
primrec delete :: "'a \<Rightarrow> ('a, 'b) map \<Rightarrow> ('a, 'b) map" where
haftmann@29708
    25
  "delete k (Map f) = Map (f (k := None))"
haftmann@29708
    26
haftmann@29708
    27
primrec keys :: "('a, 'b) map \<Rightarrow> 'a set" where
haftmann@29708
    28
  "keys (Map f) = dom f"
haftmann@29708
    29
haftmann@29708
    30
haftmann@29708
    31
subsection {* Derived operations *}
haftmann@29708
    32
haftmann@29708
    33
definition size :: "('a, 'b) map \<Rightarrow> nat" where
haftmann@29708
    34
  "size m = (if finite (keys m) then card (keys m) else 0)"
haftmann@29708
    35
haftmann@29708
    36
definition tabulate :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) map" where
haftmann@29708
    37
  "tabulate ks f = Map (map_of (map (\<lambda>k. (k, f k)) ks))"
haftmann@29708
    38
haftmann@29708
    39
haftmann@29708
    40
subsection {* Properties *}
haftmann@29708
    41
haftmann@29708
    42
lemma lookup_inject:
haftmann@29708
    43
  "lookup m = lookup n \<longleftrightarrow> m = n"
haftmann@29708
    44
  by (cases m, cases n) simp
haftmann@29708
    45
haftmann@29708
    46
lemma lookup_empty [simp]:
haftmann@29708
    47
  "lookup empty = Map.empty"
haftmann@29708
    48
  by (simp add: empty_def)
haftmann@29708
    49
haftmann@29708
    50
lemma lookup_update [simp]:
haftmann@29708
    51
  "lookup (update k v m) = (lookup m) (k \<mapsto> v)"
haftmann@29708
    52
  by (cases m) simp
haftmann@29708
    53
haftmann@29708
    54
lemma lookup_delete:
haftmann@29708
    55
  "lookup (delete k m) k = None"
haftmann@29708
    56
  "k \<noteq> l \<Longrightarrow> lookup (delete k m) l = lookup m l"
haftmann@29708
    57
  by (cases m, simp)+
haftmann@29708
    58
haftmann@29708
    59
lemma lookup_tabulate:
haftmann@29708
    60
  "lookup (tabulate ks f) = (Some o f) |` set ks"
haftmann@29708
    61
  by (induct ks) (auto simp add: tabulate_def restrict_map_def expand_fun_eq)
haftmann@29708
    62
haftmann@29708
    63
lemma update_update:
haftmann@29708
    64
  "update k v (update k w m) = update k v m"
haftmann@29708
    65
  "k \<noteq> l \<Longrightarrow> update k v (update l w m) = update l w (update k v m)"
haftmann@29708
    66
  by (cases m, simp add: expand_fun_eq)+
haftmann@29708
    67
haftmann@29708
    68
lemma delete_empty [simp]:
haftmann@29708
    69
  "delete k empty = empty"
haftmann@29708
    70
  by (simp add: empty_def)
haftmann@29708
    71
haftmann@29708
    72
lemma delete_update:
haftmann@29708
    73
  "delete k (update k v m) = delete k m"
haftmann@29708
    74
  "k \<noteq> l \<Longrightarrow> delete k (update l v m) = update l v (delete k m)"
haftmann@29708
    75
  by (cases m, simp add: expand_fun_eq)+
haftmann@29708
    76
haftmann@29708
    77
lemma update_delete [simp]:
haftmann@29708
    78
  "update k v (delete k m) = update k v m"
haftmann@29708
    79
  by (cases m) simp
haftmann@29708
    80
haftmann@29708
    81
lemma keys_empty [simp]:
haftmann@29708
    82
  "keys empty = {}"
haftmann@29708
    83
  unfolding empty_def by simp
haftmann@29708
    84
haftmann@29708
    85
lemma keys_update [simp]:
haftmann@29708
    86
  "keys (update k v m) = insert k (keys m)"
haftmann@29708
    87
  by (cases m) simp
haftmann@29708
    88
haftmann@29708
    89
lemma keys_delete [simp]:
haftmann@29708
    90
  "keys (delete k m) = keys m - {k}"
haftmann@29708
    91
  by (cases m) simp
haftmann@29708
    92
haftmann@29708
    93
lemma keys_tabulate [simp]:
haftmann@29708
    94
  "keys (tabulate ks f) = set ks"
haftmann@29708
    95
  by (auto simp add: tabulate_def dest: map_of_SomeD intro!: weak_map_of_SomeI)
haftmann@29708
    96
haftmann@29708
    97
lemma size_empty [simp]:
haftmann@29708
    98
  "size empty = 0"
haftmann@29708
    99
  by (simp add: size_def keys_empty)
haftmann@29708
   100
haftmann@29708
   101
lemma size_update:
haftmann@29708
   102
  "finite (keys m) \<Longrightarrow> size (update k v m) =
haftmann@29708
   103
    (if k \<in> keys m then size m else Suc (size m))"
haftmann@29708
   104
  by (simp add: size_def keys_update)
haftmann@29708
   105
    (auto simp only: card_insert card_Suc_Diff1)
haftmann@29708
   106
haftmann@29708
   107
lemma size_delete:
haftmann@29708
   108
  "size (delete k m) = (if k \<in> keys m then size m - 1 else size m)"
haftmann@29708
   109
  by (simp add: size_def keys_delete)
haftmann@29708
   110
haftmann@29708
   111
lemma size_tabulate:
haftmann@29708
   112
  "size (tabulate ks f) = length (remdups ks)"
haftmann@29708
   113
  by (simp add: size_def keys_tabulate distinct_card [of "remdups ks", symmetric])
haftmann@29708
   114
haftmann@29708
   115
end