src/HOL/Library/Table.thy
author haftmann
Sat Mar 06 15:31:30 2010 +0100 (2010-03-06)
changeset 35617 a6528fb99641
child 36111 5844017e31f8
permissions -rw-r--r--
added Table.thy
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@35617
     6
imports Main RBT
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@35617
    26
code_abstype Table tree_of
haftmann@35617
    27
  by (simp add: tree_of_inverse)
haftmann@35617
    28
haftmann@35617
    29
haftmann@35617
    30
subsection {* Primitive operations *}
haftmann@35617
    31
haftmann@35617
    32
definition lookup :: "('a\<Colon>linorder, 'b) table \<Rightarrow> 'a \<rightharpoonup> 'b" where
haftmann@35617
    33
  [code]: "lookup t = RBT.lookup (tree_of t)"
haftmann@35617
    34
haftmann@35617
    35
definition empty :: "('a\<Colon>linorder, 'b) table" where
haftmann@35617
    36
  "empty = Table RBT.Empty"
haftmann@35617
    37
haftmann@35617
    38
lemma tree_of_empty [code abstract]:
haftmann@35617
    39
  "tree_of empty = RBT.Empty"
haftmann@35617
    40
  by (simp add: empty_def Table_inverse)
haftmann@35617
    41
haftmann@35617
    42
definition update :: "'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table" where
haftmann@35617
    43
  "update k v t = Table (RBT.insert k v (tree_of t))"
haftmann@35617
    44
haftmann@35617
    45
lemma tree_of_update [code abstract]:
haftmann@35617
    46
  "tree_of (update k v t) = RBT.insert k v (tree_of t)"
haftmann@35617
    47
  by (simp add: update_def Table_inverse)
haftmann@35617
    48
haftmann@35617
    49
definition delete :: "'a\<Colon>linorder \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table" where
haftmann@35617
    50
  "delete k t = Table (RBT.delete k (tree_of t))"
haftmann@35617
    51
haftmann@35617
    52
lemma tree_of_delete [code abstract]:
haftmann@35617
    53
  "tree_of (delete k t) = RBT.delete k (tree_of t)"
haftmann@35617
    54
  by (simp add: delete_def Table_inverse)
haftmann@35617
    55
haftmann@35617
    56
definition entries :: "('a\<Colon>linorder, 'b) table \<Rightarrow> ('a \<times> 'b) list" where
haftmann@35617
    57
  [code]: "entries t = RBT.entries (tree_of t)"
haftmann@35617
    58
haftmann@35617
    59
definition bulkload :: "('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) table" where
haftmann@35617
    60
  "bulkload xs = Table (RBT.bulkload xs)"
haftmann@35617
    61
haftmann@35617
    62
lemma tree_of_bulkload [code abstract]:
haftmann@35617
    63
  "tree_of (bulkload xs) = RBT.bulkload xs"
haftmann@35617
    64
  by (simp add: bulkload_def Table_inverse)
haftmann@35617
    65
haftmann@35617
    66
definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) table \<Rightarrow> ('a, 'b) table" where
haftmann@35617
    67
  "map_entry k f t = Table (RBT.map_entry k f (tree_of t))"
haftmann@35617
    68
haftmann@35617
    69
lemma tree_of_map_entry [code abstract]:
haftmann@35617
    70
  "tree_of (map_entry k f t) = RBT.map_entry k f (tree_of t)"
haftmann@35617
    71
  by (simp add: map_entry_def Table_inverse)
haftmann@35617
    72
haftmann@35617
    73
definition map :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) table \<Rightarrow> ('a, 'b) table" where
haftmann@35617
    74
  "map f t = Table (RBT.map f (tree_of t))"
haftmann@35617
    75
haftmann@35617
    76
lemma tree_of_map [code abstract]:
haftmann@35617
    77
  "tree_of (map f t) = RBT.map f (tree_of t)"
haftmann@35617
    78
  by (simp add: map_def Table_inverse)
haftmann@35617
    79
haftmann@35617
    80
definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) table \<Rightarrow> 'c \<Rightarrow> 'c" where
haftmann@35617
    81
  [code]: "fold f t = RBT.fold f (tree_of t)"
haftmann@35617
    82
haftmann@35617
    83
haftmann@35617
    84
subsection {* Derived operations *}
haftmann@35617
    85
haftmann@35617
    86
definition is_empty :: "('a\<Colon>linorder, 'b) table \<Rightarrow> bool" where
haftmann@35617
    87
  [code]: "is_empty t = (case tree_of t of RBT.Empty \<Rightarrow> True | _ \<Rightarrow> False)"
haftmann@35617
    88
haftmann@35617
    89
haftmann@35617
    90
subsection {* Abstract lookup properties *}
haftmann@35617
    91
haftmann@35617
    92
lemma lookup_Table:
haftmann@35617
    93
  "is_rbt t \<Longrightarrow> lookup (Table t) = RBT.lookup t"
haftmann@35617
    94
  by (simp add: lookup_def Table_inverse)
haftmann@35617
    95
haftmann@35617
    96
lemma lookup_tree_of:
haftmann@35617
    97
  "RBT.lookup (tree_of t) = lookup t"
haftmann@35617
    98
  by (simp add: lookup_def)
haftmann@35617
    99
haftmann@35617
   100
lemma entries_tree_of:
haftmann@35617
   101
  "RBT.entries (tree_of t) = entries t"
haftmann@35617
   102
  by (simp add: entries_def)
haftmann@35617
   103
haftmann@35617
   104
lemma lookup_empty [simp]:
haftmann@35617
   105
  "lookup empty = Map.empty"
haftmann@35617
   106
  by (simp add: empty_def lookup_Table expand_fun_eq)
haftmann@35617
   107
haftmann@35617
   108
lemma lookup_update [simp]:
haftmann@35617
   109
  "lookup (update k v t) = (lookup t)(k \<mapsto> v)"
haftmann@35617
   110
  by (simp add: update_def lookup_Table lookup_insert lookup_tree_of)
haftmann@35617
   111
haftmann@35617
   112
lemma lookup_delete [simp]:
haftmann@35617
   113
  "lookup (delete k t) = (lookup t)(k := None)"
haftmann@35617
   114
  by (simp add: delete_def lookup_Table lookup_delete lookup_tree_of restrict_complement_singleton_eq)
haftmann@35617
   115
haftmann@35617
   116
lemma map_of_entries [simp]:
haftmann@35617
   117
  "map_of (entries t) = lookup t"
haftmann@35617
   118
  by (simp add: entries_def map_of_entries lookup_tree_of)
haftmann@35617
   119
haftmann@35617
   120
lemma lookup_bulkload [simp]:
haftmann@35617
   121
  "lookup (bulkload xs) = map_of xs"
haftmann@35617
   122
  by (simp add: bulkload_def lookup_Table lookup_bulkload)
haftmann@35617
   123
haftmann@35617
   124
lemma lookup_map_entry [simp]:
haftmann@35617
   125
  "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))"
haftmann@35617
   126
  by (simp add: map_entry_def lookup_Table lookup_map_entry lookup_tree_of)
haftmann@35617
   127
haftmann@35617
   128
lemma lookup_map [simp]:
haftmann@35617
   129
  "lookup (map f t) k = Option.map (f k) (lookup t k)"
haftmann@35617
   130
  by (simp add: map_def lookup_Table lookup_map lookup_tree_of)
haftmann@35617
   131
haftmann@35617
   132
lemma fold_fold:
haftmann@35617
   133
  "fold f t = (\<lambda>s. foldl (\<lambda>s (k, v). f k v s) s (entries t))"
haftmann@35617
   134
  by (simp add: fold_def expand_fun_eq RBT.fold_def entries_tree_of)
haftmann@35617
   135
haftmann@35617
   136
hide (open) const tree_of lookup empty update delete
haftmann@35617
   137
  entries bulkload map_entry map fold
haftmann@35617
   138
haftmann@35617
   139
end