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