1.1 --- a/src/HOL/IsaMakefile	Sat Mar 06 11:21:09 2010 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Sat Mar 06 15:31:30 2010 +0100
     1.3 @@ -401,7 +401,7 @@
     1.4    Library/Ramsey.thy Library/Zorn.thy Library/Library/ROOT.ML		\
     1.5    Library/Library/document/root.tex Library/Library/document/root.bib	\
     1.6    Library/Transitive_Closure_Table.thy Library/While_Combinator.thy	\
     1.7 -  Library/Product_ord.thy Library/Char_nat.thy				\
     1.8 +  Library/Product_ord.thy Library/Char_nat.thy Library/Table.thy	\
     1.9    Library/Sublist_Order.thy Library/List_lexord.thy			\
    1.10    Library/Coinductive_List.thy Library/AssocList.thy			\
    1.11    Library/Formal_Power_Series.thy Library/Binomial.thy			\

     2.1 --- a/src/HOL/Library/Library.thy	Sat Mar 06 11:21:09 2010 +0100
     2.2 +++ b/src/HOL/Library/Library.thy	Sat Mar 06 15:31:30 2010 +0100
     2.3 @@ -58,6 +58,7 @@
     2.4    SML_Quickcheck
     2.5    State_Monad
     2.6    Sum_Of_Squares
     2.7 +  Table
     2.8    Transitive_Closure_Table
     2.9    Univ_Poly
    2.10    While_Combinator

     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Library/Table.thy	Sat Mar 06 15:31:30 2010 +0100
     3.3 @@ -0,0 +1,139 @@
     3.4 +(* Author: Florian Haftmann, TU Muenchen *)
     3.5 +
     3.6 +header {* Tables: finite mappings implemented by red-black trees *}
     3.7 +
     3.8 +theory Table
     3.9 +imports Main RBT
    3.10 +begin
    3.11 +
    3.12 +subsection {* Type definition *}
    3.13 +
    3.14 +typedef (open) ('a, 'b) table = "{t :: ('a\<Colon>linorder, 'b) rbt. is_rbt t}"
    3.15 +  morphisms tree_of Table
    3.16 +proof -
    3.17 +  have "RBT.Empty \<in> ?table" by simp
    3.18 +  then show ?thesis ..
    3.19 +qed
    3.20 +
    3.21 +lemma is_rbt_tree_of [simp, intro]:
    3.22 +  "is_rbt (tree_of t)"
    3.23 +  using tree_of [of t] by simp
    3.24 +
    3.25 +lemma table_eq:
    3.26 +  "t1 = t2 \<longleftrightarrow> tree_of t1 = tree_of t2"
    3.27 +  by (simp add: tree_of_inject)
    3.28 +
    3.29 +code_abstype Table tree_of
    3.30 +  by (simp add: tree_of_inverse)
    3.31 +
    3.32 +
    3.33 +subsection {* Primitive operations *}
    3.34 +
    3.35 +definition lookup :: "('a\<Colon>linorder, 'b) table \<Rightarrow> 'a \<rightharpoonup> 'b" where
    3.36 +  [code]: "lookup t = RBT.lookup (tree_of t)"
    3.37 +
    3.38 +definition empty :: "('a\<Colon>linorder, 'b) table" where
    3.39 +  "empty = Table RBT.Empty"
    3.40 +
    3.41 +lemma tree_of_empty [code abstract]:
    3.42 +  "tree_of empty = RBT.Empty"
    3.43 +  by (simp add: empty_def Table_inverse)
    3.44 +
    3.45 +definition update :: "'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table" where
    3.46 +  "update k v t = Table (RBT.insert k v (tree_of t))"
    3.47 +
    3.48 +lemma tree_of_update [code abstract]:
    3.49 +  "tree_of (update k v t) = RBT.insert k v (tree_of t)"
    3.50 +  by (simp add: update_def Table_inverse)
    3.51 +
    3.52 +definition delete :: "'a\<Colon>linorder \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table" where
    3.53 +  "delete k t = Table (RBT.delete k (tree_of t))"
    3.54 +
    3.55 +lemma tree_of_delete [code abstract]:
    3.56 +  "tree_of (delete k t) = RBT.delete k (tree_of t)"
    3.57 +  by (simp add: delete_def Table_inverse)
    3.58 +
    3.59 +definition entries :: "('a\<Colon>linorder, 'b) table \<Rightarrow> ('a \<times> 'b) list" where
    3.60 +  [code]: "entries t = RBT.entries (tree_of t)"
    3.61 +
    3.62 +definition bulkload :: "('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) table" where
    3.63 +  "bulkload xs = Table (RBT.bulkload xs)"
    3.64 +
    3.65 +lemma tree_of_bulkload [code abstract]:
    3.66 +  "tree_of (bulkload xs) = RBT.bulkload xs"
    3.67 +  by (simp add: bulkload_def Table_inverse)
    3.68 +
    3.69 +definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) table \<Rightarrow> ('a, 'b) table" where
    3.70 +  "map_entry k f t = Table (RBT.map_entry k f (tree_of t))"
    3.71 +
    3.72 +lemma tree_of_map_entry [code abstract]:
    3.73 +  "tree_of (map_entry k f t) = RBT.map_entry k f (tree_of t)"
    3.74 +  by (simp add: map_entry_def Table_inverse)
    3.75 +
    3.76 +definition map :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) table \<Rightarrow> ('a, 'b) table" where
    3.77 +  "map f t = Table (RBT.map f (tree_of t))"
    3.78 +
    3.79 +lemma tree_of_map [code abstract]:
    3.80 +  "tree_of (map f t) = RBT.map f (tree_of t)"
    3.81 +  by (simp add: map_def Table_inverse)
    3.82 +
    3.83 +definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) table \<Rightarrow> 'c \<Rightarrow> 'c" where
    3.84 +  [code]: "fold f t = RBT.fold f (tree_of t)"
    3.85 +
    3.86 +
    3.87 +subsection {* Derived operations *}
    3.88 +
    3.89 +definition is_empty :: "('a\<Colon>linorder, 'b) table \<Rightarrow> bool" where
    3.90 +  [code]: "is_empty t = (case tree_of t of RBT.Empty \<Rightarrow> True | _ \<Rightarrow> False)"
    3.91 +
    3.92 +
    3.93 +subsection {* Abstract lookup properties *}
    3.94 +
    3.95 +lemma lookup_Table:
    3.96 +  "is_rbt t \<Longrightarrow> lookup (Table t) = RBT.lookup t"
    3.97 +  by (simp add: lookup_def Table_inverse)
    3.98 +
    3.99 +lemma lookup_tree_of:
   3.100 +  "RBT.lookup (tree_of t) = lookup t"
   3.101 +  by (simp add: lookup_def)
   3.102 +
   3.103 +lemma entries_tree_of:
   3.104 +  "RBT.entries (tree_of t) = entries t"
   3.105 +  by (simp add: entries_def)
   3.106 +
   3.107 +lemma lookup_empty [simp]:
   3.108 +  "lookup empty = Map.empty"
   3.109 +  by (simp add: empty_def lookup_Table expand_fun_eq)
   3.110 +
   3.111 +lemma lookup_update [simp]:
   3.112 +  "lookup (update k v t) = (lookup t)(k \<mapsto> v)"
   3.113 +  by (simp add: update_def lookup_Table lookup_insert lookup_tree_of)
   3.114 +
   3.115 +lemma lookup_delete [simp]:
   3.116 +  "lookup (delete k t) = (lookup t)(k := None)"
   3.117 +  by (simp add: delete_def lookup_Table lookup_delete lookup_tree_of restrict_complement_singleton_eq)
   3.118 +
   3.119 +lemma map_of_entries [simp]:
   3.120 +  "map_of (entries t) = lookup t"
   3.121 +  by (simp add: entries_def map_of_entries lookup_tree_of)
   3.122 +
   3.123 +lemma lookup_bulkload [simp]:
   3.124 +  "lookup (bulkload xs) = map_of xs"
   3.125 +  by (simp add: bulkload_def lookup_Table lookup_bulkload)
   3.126 +
   3.127 +lemma lookup_map_entry [simp]:
   3.128 +  "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))"
   3.129 +  by (simp add: map_entry_def lookup_Table lookup_map_entry lookup_tree_of)
   3.130 +
   3.131 +lemma lookup_map [simp]:
   3.132 +  "lookup (map f t) k = Option.map (f k) (lookup t k)"
   3.133 +  by (simp add: map_def lookup_Table lookup_map lookup_tree_of)
   3.134 +
   3.135 +lemma fold_fold:
   3.136 +  "fold f t = (\<lambda>s. foldl (\<lambda>s (k, v). f k v s) s (entries t))"
   3.137 +  by (simp add: fold_def expand_fun_eq RBT.fold_def entries_tree_of)
   3.138 +
   3.139 +hide (open) const tree_of lookup empty update delete
   3.140 +  entries bulkload map_entry map fold
   3.141 +
   3.142 +end

     4.1 --- a/src/HOL/ex/Codegenerator_Candidates.thy	Sat Mar 06 11:21:09 2010 +0100
     4.2 +++ b/src/HOL/ex/Codegenerator_Candidates.thy	Sat Mar 06 15:31:30 2010 +0100
     4.3 @@ -21,6 +21,7 @@
     4.4    Product_ord
     4.5    "~~/src/HOL/ex/Records"
     4.6    SetsAndFunctions
     4.7 +  Table
     4.8    Tree
     4.9    While_Combinator
    4.10    Word