src/HOL/Library/Mapping.thy
author haftmann
Mon Mar 23 08:14:24 2009 +0100 (2009-03-23)
changeset 30663 0b6aff7451b2
parent 29831 5dc920623bb1
child 31459 ae39b7b2a68a
permissions -rw-r--r--
Main is (Complex_Main) base entry point in library theories
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@30663
     8
imports Map Main
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@29814
    36
definition replace :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) map \<Rightarrow> ('a, 'b) map" where
haftmann@29814
    37
  "replace k v m = (if lookup m k = None then m else update k v m)"
haftmann@29814
    38
haftmann@29708
    39
definition tabulate :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) map" where
haftmann@29708
    40
  "tabulate ks f = Map (map_of (map (\<lambda>k. (k, f k)) ks))"
haftmann@29708
    41
haftmann@29826
    42
definition bulkload :: "'a list \<Rightarrow> (nat, 'a) map" where
haftmann@29826
    43
  "bulkload xs = Map (\<lambda>k. if k < length xs then Some (xs ! k) else None)"
haftmann@29826
    44
haftmann@29708
    45
haftmann@29708
    46
subsection {* Properties *}
haftmann@29708
    47
haftmann@29708
    48
lemma lookup_inject:
haftmann@29708
    49
  "lookup m = lookup n \<longleftrightarrow> m = n"
haftmann@29708
    50
  by (cases m, cases n) simp
haftmann@29708
    51
haftmann@29708
    52
lemma lookup_empty [simp]:
haftmann@29708
    53
  "lookup empty = Map.empty"
haftmann@29708
    54
  by (simp add: empty_def)
haftmann@29708
    55
haftmann@29708
    56
lemma lookup_update [simp]:
haftmann@29708
    57
  "lookup (update k v m) = (lookup m) (k \<mapsto> v)"
haftmann@29708
    58
  by (cases m) simp
haftmann@29708
    59
haftmann@29708
    60
lemma lookup_delete:
haftmann@29708
    61
  "lookup (delete k m) k = None"
haftmann@29708
    62
  "k \<noteq> l \<Longrightarrow> lookup (delete k m) l = lookup m l"
haftmann@29708
    63
  by (cases m, simp)+
haftmann@29708
    64
haftmann@29708
    65
lemma lookup_tabulate:
haftmann@29708
    66
  "lookup (tabulate ks f) = (Some o f) |` set ks"
haftmann@29708
    67
  by (induct ks) (auto simp add: tabulate_def restrict_map_def expand_fun_eq)
haftmann@29708
    68
haftmann@29826
    69
lemma lookup_bulkload:
haftmann@29826
    70
  "lookup (bulkload xs) = (\<lambda>k. if k < length xs then Some (xs ! k) else None)"
haftmann@29826
    71
  unfolding bulkload_def by simp
haftmann@29826
    72
haftmann@29708
    73
lemma update_update:
haftmann@29708
    74
  "update k v (update k w m) = update k v m"
haftmann@29708
    75
  "k \<noteq> l \<Longrightarrow> update k v (update l w m) = update l w (update k v m)"
haftmann@29708
    76
  by (cases m, simp add: expand_fun_eq)+
haftmann@29708
    77
haftmann@29814
    78
lemma replace_update:
haftmann@29814
    79
  "lookup m k = None \<Longrightarrow> replace k v m = m"
haftmann@29814
    80
  "lookup m k \<noteq> None \<Longrightarrow> replace k v m = update k v m"
haftmann@29814
    81
  by (auto simp add: replace_def)
haftmann@29814
    82
haftmann@29708
    83
lemma delete_empty [simp]:
haftmann@29708
    84
  "delete k empty = empty"
haftmann@29708
    85
  by (simp add: empty_def)
haftmann@29708
    86
haftmann@29708
    87
lemma delete_update:
haftmann@29708
    88
  "delete k (update k v m) = delete k m"
haftmann@29708
    89
  "k \<noteq> l \<Longrightarrow> delete k (update l v m) = update l v (delete k m)"
haftmann@29708
    90
  by (cases m, simp add: expand_fun_eq)+
haftmann@29708
    91
haftmann@29708
    92
lemma update_delete [simp]:
haftmann@29708
    93
  "update k v (delete k m) = update k v m"
haftmann@29708
    94
  by (cases m) simp
haftmann@29708
    95
haftmann@29708
    96
lemma keys_empty [simp]:
haftmann@29708
    97
  "keys empty = {}"
haftmann@29708
    98
  unfolding empty_def by simp
haftmann@29708
    99
haftmann@29708
   100
lemma keys_update [simp]:
haftmann@29708
   101
  "keys (update k v m) = insert k (keys m)"
haftmann@29708
   102
  by (cases m) simp
haftmann@29708
   103
haftmann@29708
   104
lemma keys_delete [simp]:
haftmann@29708
   105
  "keys (delete k m) = keys m - {k}"
haftmann@29708
   106
  by (cases m) simp
haftmann@29708
   107
haftmann@29708
   108
lemma keys_tabulate [simp]:
haftmann@29708
   109
  "keys (tabulate ks f) = set ks"
haftmann@29708
   110
  by (auto simp add: tabulate_def dest: map_of_SomeD intro!: weak_map_of_SomeI)
haftmann@29708
   111
haftmann@29708
   112
lemma size_empty [simp]:
haftmann@29708
   113
  "size empty = 0"
haftmann@29708
   114
  by (simp add: size_def keys_empty)
haftmann@29708
   115
haftmann@29708
   116
lemma size_update:
haftmann@29708
   117
  "finite (keys m) \<Longrightarrow> size (update k v m) =
haftmann@29708
   118
    (if k \<in> keys m then size m else Suc (size m))"
haftmann@29708
   119
  by (simp add: size_def keys_update)
haftmann@29708
   120
    (auto simp only: card_insert card_Suc_Diff1)
haftmann@29708
   121
haftmann@29708
   122
lemma size_delete:
haftmann@29708
   123
  "size (delete k m) = (if k \<in> keys m then size m - 1 else size m)"
haftmann@29708
   124
  by (simp add: size_def keys_delete)
haftmann@29708
   125
haftmann@29708
   126
lemma size_tabulate:
haftmann@29708
   127
  "size (tabulate ks f) = length (remdups ks)"
haftmann@29708
   128
  by (simp add: size_def keys_tabulate distinct_card [of "remdups ks", symmetric])
haftmann@29708
   129
haftmann@29831
   130
lemma bulkload_tabulate:
haftmann@29826
   131
  "bulkload xs = tabulate [0..<length xs] (nth xs)"
haftmann@29831
   132
  by (rule sym)
haftmann@29831
   133
    (auto simp add: bulkload_def tabulate_def expand_fun_eq map_of_eq_None_iff map_compose [symmetric] comp_def)
haftmann@29826
   134
haftmann@29708
   135
end