src/HOL/Library/Table.thy
author haftmann
Sun Apr 11 16:51:06 2010 +0200 (2010-04-11)
changeset 36111 5844017e31f8
parent 35617 a6528fb99641
permissions -rw-r--r--
implementation of mappings by rbts
haftmann@35617
     1
(* Author: Florian Haftmann, TU Muenchen *)
haftmann@35617
     2
haftmann@35617
     3
header {* Tables: finite mappings implemented by red-black trees *}
haftmann@35617
     4
haftmann@35617
     5
theory Table
haftmann@36111
     6
imports Main RBT Mapping
haftmann@35617
     7
begin
haftmann@35617
     8
haftmann@35617
     9
subsection {* Type definition *}
haftmann@35617
    10
haftmann@35617
    11
typedef (open) ('a, 'b) table = "{t :: ('a\<Colon>linorder, 'b) rbt. is_rbt t}"
haftmann@35617
    12
  morphisms tree_of Table
haftmann@35617
    13
proof -
haftmann@35617
    14
  have "RBT.Empty \<in> ?table" by simp
haftmann@35617
    15
  then show ?thesis ..
haftmann@35617
    16
qed
haftmann@35617
    17
haftmann@35617
    18
lemma is_rbt_tree_of [simp, intro]:
haftmann@35617
    19
  "is_rbt (tree_of t)"
haftmann@35617
    20
  using tree_of [of t] by simp
haftmann@35617
    21
haftmann@35617
    22
lemma table_eq:
haftmann@35617
    23
  "t1 = t2 \<longleftrightarrow> tree_of t1 = tree_of t2"
haftmann@35617
    24
  by (simp add: tree_of_inject)
haftmann@35617
    25
haftmann@36111
    26
lemma [code abstype]:
haftmann@36111
    27
  "Table (tree_of t) = t"
haftmann@35617
    28
  by (simp add: tree_of_inverse)
haftmann@35617
    29
haftmann@35617
    30
haftmann@35617
    31
subsection {* Primitive operations *}
haftmann@35617
    32
haftmann@35617
    33
definition lookup :: "('a\<Colon>linorder, 'b) table \<Rightarrow> 'a \<rightharpoonup> 'b" where
haftmann@35617
    34
  [code]: "lookup t = RBT.lookup (tree_of t)"
haftmann@35617
    35
haftmann@35617
    36
definition empty :: "('a\<Colon>linorder, 'b) table" where
haftmann@35617
    37
  "empty = Table RBT.Empty"
haftmann@35617
    38
haftmann@35617
    39
lemma tree_of_empty [code abstract]:
haftmann@35617
    40
  "tree_of empty = RBT.Empty"
haftmann@35617
    41
  by (simp add: empty_def Table_inverse)
haftmann@35617
    42
haftmann@35617
    43
definition update :: "'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table" where
haftmann@35617
    44
  "update k v t = Table (RBT.insert k v (tree_of t))"
haftmann@35617
    45
haftmann@35617
    46
lemma tree_of_update [code abstract]:
haftmann@35617
    47
  "tree_of (update k v t) = RBT.insert k v (tree_of t)"
haftmann@35617
    48
  by (simp add: update_def Table_inverse)
haftmann@35617
    49
haftmann@35617
    50
definition delete :: "'a\<Colon>linorder \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table" where
haftmann@35617
    51
  "delete k t = Table (RBT.delete k (tree_of t))"
haftmann@35617
    52
haftmann@35617
    53
lemma tree_of_delete [code abstract]:
haftmann@35617
    54
  "tree_of (delete k t) = RBT.delete k (tree_of t)"
haftmann@35617
    55
  by (simp add: delete_def Table_inverse)
haftmann@35617
    56
haftmann@35617
    57
definition entries :: "('a\<Colon>linorder, 'b) table \<Rightarrow> ('a \<times> 'b) list" where
haftmann@35617
    58
  [code]: "entries t = RBT.entries (tree_of t)"
haftmann@35617
    59
haftmann@36111
    60
definition keys :: "('a\<Colon>linorder, 'b) table \<Rightarrow> 'a list" where
haftmann@36111
    61
  [code]: "keys t = RBT.keys (tree_of t)"
haftmann@36111
    62
haftmann@35617
    63
definition bulkload :: "('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) table" where
haftmann@35617
    64
  "bulkload xs = Table (RBT.bulkload xs)"
haftmann@35617
    65
haftmann@35617
    66
lemma tree_of_bulkload [code abstract]:
haftmann@35617
    67
  "tree_of (bulkload xs) = RBT.bulkload xs"
haftmann@35617
    68
  by (simp add: bulkload_def Table_inverse)
haftmann@35617
    69
haftmann@35617
    70
definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) table \<Rightarrow> ('a, 'b) table" where
haftmann@35617
    71
  "map_entry k f t = Table (RBT.map_entry k f (tree_of t))"
haftmann@35617
    72
haftmann@35617
    73
lemma tree_of_map_entry [code abstract]:
haftmann@35617
    74
  "tree_of (map_entry k f t) = RBT.map_entry k f (tree_of t)"
haftmann@35617
    75
  by (simp add: map_entry_def Table_inverse)
haftmann@35617
    76
haftmann@35617
    77
definition map :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) table \<Rightarrow> ('a, 'b) table" where
haftmann@35617
    78
  "map f t = Table (RBT.map f (tree_of t))"
haftmann@35617
    79
haftmann@35617
    80
lemma tree_of_map [code abstract]:
haftmann@35617
    81
  "tree_of (map f t) = RBT.map f (tree_of t)"
haftmann@35617
    82
  by (simp add: map_def Table_inverse)
haftmann@35617
    83
haftmann@35617
    84
definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) table \<Rightarrow> 'c \<Rightarrow> 'c" where
haftmann@35617
    85
  [code]: "fold f t = RBT.fold f (tree_of t)"
haftmann@35617
    86
haftmann@35617
    87
haftmann@35617
    88
subsection {* Derived operations *}
haftmann@35617
    89
haftmann@35617
    90
definition is_empty :: "('a\<Colon>linorder, 'b) table \<Rightarrow> bool" where
haftmann@35617
    91
  [code]: "is_empty t = (case tree_of t of RBT.Empty \<Rightarrow> True | _ \<Rightarrow> False)"
haftmann@35617
    92
haftmann@35617
    93
haftmann@35617
    94
subsection {* Abstract lookup properties *}
haftmann@35617
    95
haftmann@35617
    96
lemma lookup_Table:
haftmann@35617
    97
  "is_rbt t \<Longrightarrow> lookup (Table t) = RBT.lookup t"
haftmann@35617
    98
  by (simp add: lookup_def Table_inverse)
haftmann@35617
    99
haftmann@35617
   100
lemma lookup_tree_of:
haftmann@35617
   101
  "RBT.lookup (tree_of t) = lookup t"
haftmann@35617
   102
  by (simp add: lookup_def)
haftmann@35617
   103
haftmann@35617
   104
lemma entries_tree_of:
haftmann@35617
   105
  "RBT.entries (tree_of t) = entries t"
haftmann@35617
   106
  by (simp add: entries_def)
haftmann@35617
   107
haftmann@36111
   108
lemma keys_tree_of:
haftmann@36111
   109
  "RBT.keys (tree_of t) = keys t"
haftmann@36111
   110
  by (simp add: keys_def)
haftmann@36111
   111
haftmann@35617
   112
lemma lookup_empty [simp]:
haftmann@35617
   113
  "lookup empty = Map.empty"
haftmann@35617
   114
  by (simp add: empty_def lookup_Table expand_fun_eq)
haftmann@35617
   115
haftmann@35617
   116
lemma lookup_update [simp]:
haftmann@35617
   117
  "lookup (update k v t) = (lookup t)(k \<mapsto> v)"
haftmann@35617
   118
  by (simp add: update_def lookup_Table lookup_insert lookup_tree_of)
haftmann@35617
   119
haftmann@35617
   120
lemma lookup_delete [simp]:
haftmann@35617
   121
  "lookup (delete k t) = (lookup t)(k := None)"
haftmann@36111
   122
  by (simp add: delete_def lookup_Table RBT.lookup_delete lookup_tree_of restrict_complement_singleton_eq)
haftmann@35617
   123
haftmann@35617
   124
lemma map_of_entries [simp]:
haftmann@35617
   125
  "map_of (entries t) = lookup t"
haftmann@35617
   126
  by (simp add: entries_def map_of_entries lookup_tree_of)
haftmann@35617
   127
haftmann@36111
   128
lemma entries_lookup:
haftmann@36111
   129
  "entries t1 = entries t2 \<longleftrightarrow> lookup t1 = lookup t2"
haftmann@36111
   130
  by (simp add: entries_def lookup_def entries_lookup)
haftmann@36111
   131
haftmann@35617
   132
lemma lookup_bulkload [simp]:
haftmann@35617
   133
  "lookup (bulkload xs) = map_of xs"
haftmann@36111
   134
  by (simp add: bulkload_def lookup_Table RBT.lookup_bulkload)
haftmann@35617
   135
haftmann@35617
   136
lemma lookup_map_entry [simp]:
haftmann@35617
   137
  "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))"
haftmann@35617
   138
  by (simp add: map_entry_def lookup_Table lookup_map_entry lookup_tree_of)
haftmann@35617
   139
haftmann@35617
   140
lemma lookup_map [simp]:
haftmann@35617
   141
  "lookup (map f t) k = Option.map (f k) (lookup t k)"
haftmann@35617
   142
  by (simp add: map_def lookup_Table lookup_map lookup_tree_of)
haftmann@35617
   143
haftmann@35617
   144
lemma fold_fold:
haftmann@35617
   145
  "fold f t = (\<lambda>s. foldl (\<lambda>s (k, v). f k v s) s (entries t))"
haftmann@35617
   146
  by (simp add: fold_def expand_fun_eq RBT.fold_def entries_tree_of)
haftmann@35617
   147
haftmann@36111
   148
lemma is_empty_empty [simp]:
haftmann@36111
   149
  "is_empty t \<longleftrightarrow> t = empty"
haftmann@36111
   150
  by (simp add: table_eq is_empty_def tree_of_empty split: rbt.split)
haftmann@36111
   151
haftmann@36111
   152
lemma RBT_lookup_empty [simp]: (*FIXME*)
haftmann@36111
   153
  "RBT.lookup t = Map.empty \<longleftrightarrow> t = RBT.Empty"
haftmann@36111
   154
  by (cases t) (auto simp add: expand_fun_eq)
haftmann@36111
   155
haftmann@36111
   156
lemma lookup_empty_empty [simp]:
haftmann@36111
   157
  "lookup t = Map.empty \<longleftrightarrow> t = empty"
haftmann@36111
   158
  by (cases t) (simp add: empty_def lookup_def Table_inject Table_inverse)
haftmann@36111
   159
haftmann@36111
   160
lemma sorted_keys [iff]:
haftmann@36111
   161
  "sorted (keys t)"
haftmann@36111
   162
  by (simp add: keys_def RBT.keys_def sorted_entries)
haftmann@36111
   163
haftmann@36111
   164
lemma distinct_keys [iff]:
haftmann@36111
   165
  "distinct (keys t)"
haftmann@36111
   166
  by (simp add: keys_def RBT.keys_def distinct_entries)
haftmann@36111
   167
haftmann@36111
   168
haftmann@36111
   169
subsection {* Implementation of mappings *}
haftmann@36111
   170
haftmann@36111
   171
definition Mapping :: "('a\<Colon>linorder, 'b) table \<Rightarrow> ('a, 'b) mapping" where
haftmann@36111
   172
  "Mapping t = Mapping.Mapping (lookup t)"
haftmann@36111
   173
haftmann@36111
   174
code_datatype Mapping
haftmann@36111
   175
haftmann@36111
   176
lemma lookup_Mapping [simp, code]:
haftmann@36111
   177
  "Mapping.lookup (Mapping t) = lookup t"
haftmann@36111
   178
  by (simp add: Mapping_def)
haftmann@36111
   179
haftmann@36111
   180
lemma empty_Mapping [code]:
haftmann@36111
   181
  "Mapping.empty = Mapping empty"
haftmann@36111
   182
  by (rule mapping_eqI) simp
haftmann@36111
   183
haftmann@36111
   184
lemma is_empty_Mapping [code]:
haftmann@36111
   185
  "Mapping.is_empty (Mapping t) \<longleftrightarrow> is_empty t"
haftmann@36111
   186
  by (simp add: table_eq Mapping.is_empty_empty Mapping_def)
haftmann@36111
   187
haftmann@36111
   188
lemma update_Mapping [code]:
haftmann@36111
   189
  "Mapping.update k v (Mapping t) = Mapping (update k v t)"
haftmann@36111
   190
  by (rule mapping_eqI) simp
haftmann@36111
   191
haftmann@36111
   192
lemma delete_Mapping [code]:
haftmann@36111
   193
  "Mapping.delete k (Mapping xs) = Mapping (delete k xs)"
haftmann@36111
   194
  by (rule mapping_eqI) simp
haftmann@36111
   195
haftmann@36111
   196
lemma keys_Mapping [code]:
haftmann@36111
   197
  "Mapping.keys (Mapping t) = set (keys t)"
haftmann@36111
   198
  by (simp add: keys_def Mapping_def Mapping.keys_def lookup_def lookup_keys)
haftmann@36111
   199
haftmann@36111
   200
lemma ordered_keys_Mapping [code]:
haftmann@36111
   201
  "Mapping.ordered_keys (Mapping t) = keys t"
haftmann@36111
   202
  by (rule sorted_distinct_set_unique) (simp_all add: ordered_keys_def keys_Mapping)
haftmann@36111
   203
haftmann@36111
   204
lemma Mapping_size_card_keys: (*FIXME*)
haftmann@36111
   205
  "Mapping.size m = card (Mapping.keys m)"
haftmann@36111
   206
  by (simp add: Mapping.size_def Mapping.keys_def)
haftmann@36111
   207
haftmann@36111
   208
lemma size_Mapping [code]:
haftmann@36111
   209
  "Mapping.size (Mapping t) = length (keys t)"
haftmann@36111
   210
  by (simp add: Mapping_size_card_keys keys_Mapping distinct_card)
haftmann@36111
   211
haftmann@36111
   212
lemma tabulate_Mapping [code]:
haftmann@36111
   213
  "Mapping.tabulate ks f = Mapping (bulkload (List.map (\<lambda>k. (k, f k)) ks))"
haftmann@36111
   214
  by (rule mapping_eqI) (simp add: map_of_map_restrict)
haftmann@36111
   215
haftmann@36111
   216
lemma bulkload_Mapping [code]:
haftmann@36111
   217
  "Mapping.bulkload vs = Mapping (bulkload (List.map (\<lambda>n. (n, vs ! n)) [0..<length vs]))"
haftmann@36111
   218
  by (rule mapping_eqI) (simp add: map_of_map_restrict expand_fun_eq)
haftmann@36111
   219
haftmann@36111
   220
lemma [code, code del]: "HOL.eq (x :: (_, _) mapping) y \<longleftrightarrow> x = y" by (fact eq_equals) (*FIXME*)
haftmann@36111
   221
haftmann@36111
   222
lemma eq_Mapping [code]:
haftmann@36111
   223
  "HOL.eq (Mapping t1) (Mapping t2) \<longleftrightarrow> entries t1 = entries t2"
haftmann@36111
   224
  by (simp add: eq Mapping_def entries_lookup)
haftmann@36111
   225
haftmann@35617
   226
hide (open) const tree_of lookup empty update delete
haftmann@36111
   227
  entries keys bulkload map_entry map fold
haftmann@35617
   228
haftmann@35617
   229
end