--- a/src/HOL/IsaMakefile Sat Mar 06 17:53:04 2010 +0100
+++ b/src/HOL/IsaMakefile Sat Mar 06 20:16:31 2010 +0100
@@ -401,7 +401,7 @@
Library/Ramsey.thy Library/Zorn.thy Library/Library/ROOT.ML \
Library/Library/document/root.tex Library/Library/document/root.bib \
Library/Transitive_Closure_Table.thy Library/While_Combinator.thy \
- Library/Product_ord.thy Library/Char_nat.thy \
+ Library/Product_ord.thy Library/Char_nat.thy Library/Table.thy \
Library/Sublist_Order.thy Library/List_lexord.thy \
Library/Coinductive_List.thy Library/AssocList.thy \
Library/Formal_Power_Series.thy Library/Binomial.thy \
--- a/src/HOL/Library/Library.thy Sat Mar 06 17:53:04 2010 +0100
+++ b/src/HOL/Library/Library.thy Sat Mar 06 20:16:31 2010 +0100
@@ -58,6 +58,7 @@
SML_Quickcheck
State_Monad
Sum_Of_Squares
+ Table
Transitive_Closure_Table
Univ_Poly
While_Combinator
--- a/src/HOL/Library/RBT.thy Sat Mar 06 17:53:04 2010 +0100
+++ b/src/HOL/Library/RBT.thy Sat Mar 06 20:16:31 2010 +0100
@@ -151,8 +151,8 @@
lemma lookup_Empty: "lookup Empty = empty"
by (rule ext) simp
-lemma lookup_map_of_entries:
- "sorted t \<Longrightarrow> lookup t = map_of (entries t)"
+lemma map_of_entries:
+ "sorted t \<Longrightarrow> map_of (entries t) = lookup t"
proof (induct t)
case Empty thus ?case by (simp add: lookup_Empty)
next
@@ -213,11 +213,11 @@
} ultimately show ?thesis using less_linear by blast
qed
also from Branch have "lookup t2 ++ [k \<mapsto> v] ++ lookup t1 = map_of (entries (Branch c t1 k v t2))" by simp
- finally show ?case .
+ finally show ?case by simp
qed
lemma lookup_in_tree: "sorted t \<Longrightarrow> lookup t k = Some v \<longleftrightarrow> (k, v) \<in> set (entries t)"
- by (simp_all add: lookup_map_of_entries distinct_entries)
+ by (simp add: map_of_entries [symmetric] distinct_entries)
lemma set_entries_inject:
assumes sorted: "sorted t1" "sorted t2"
@@ -236,7 +236,7 @@
shows "entries t1 = entries t2"
proof -
from sorted lookup have "map_of (entries t1) = map_of (entries t2)"
- by (simp add: lookup_map_of_entries)
+ by (simp add: map_of_entries)
with sorted have "set (entries t1) = set (entries t2)"
by (simp add: map_of_inject_set distinct_entries)
with sorted show ?thesis by (simp add: set_entries_inject)
@@ -245,7 +245,7 @@
lemma entries_lookup:
assumes "sorted t1" "sorted t2"
shows "entries t1 = entries t2 \<longleftrightarrow> lookup t1 = lookup t2"
- using assms by (auto intro: entries_eqI simp add: lookup_map_of_entries)
+ using assms by (auto intro: entries_eqI simp add: map_of_entries [symmetric])
lemma lookup_from_in_tree:
assumes "sorted t1" "sorted t2"
@@ -1013,11 +1013,9 @@
theorem map_entry_is_rbt [simp]: "is_rbt (map_entry k f t) = is_rbt t"
unfolding is_rbt_def by (simp add: map_entry_inv2 map_entry_color_of map_entry_sorted map_entry_inv1 )
-theorem map_entry_map [simp]:
- "lookup (map_entry k f t) x =
- (if x = k then case lookup t x of None \<Rightarrow> None | Some y \<Rightarrow> Some (f y)
- else lookup t x)"
- by (induct t arbitrary: x) (auto split:option.splits)
+theorem lookup_map_entry:
+ "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))"
+ by (induct t) (auto split: option.splits simp add: expand_fun_eq)
subsection {* Mapping all entries *}
@@ -1040,8 +1038,8 @@
theorem map_is_rbt [simp]: "is_rbt (map f t) = is_rbt t"
unfolding is_rbt_def by (simp add: map_inv1 map_inv2 map_sorted map_color_of)
-theorem lookup_map [simp]: "lookup (map f t) x = Option.map (f x) (lookup t x)"
-by (induct t) auto
+theorem lookup_map: "lookup (map f t) x = Option.map (f x) (lookup t x)"
+ by (induct t) auto
subsection {* Folding over entries *}
@@ -1057,7 +1055,7 @@
subsection {* Bulkloading a tree *}
-definition bulkload :: "('a \<times> 'b) list \<Rightarrow> ('a\<Colon>linorder, 'b) rbt" where (*FIXME move*)
+definition bulkload :: "('a \<times> 'b) list \<Rightarrow> ('a\<Colon>linorder, 'b) rbt" where
"bulkload xs = foldr (\<lambda>(k, v). RBT.insert k v) xs RBT.Empty"
lemma bulkload_is_rbt [simp, intro]:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Table.thy Sat Mar 06 20:16:31 2010 +0100
@@ -0,0 +1,139 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Tables: finite mappings implemented by red-black trees *}
+
+theory Table
+imports Main RBT
+begin
+
+subsection {* Type definition *}
+
+typedef (open) ('a, 'b) table = "{t :: ('a\<Colon>linorder, 'b) rbt. is_rbt t}"
+ morphisms tree_of Table
+proof -
+ have "RBT.Empty \<in> ?table" by simp
+ then show ?thesis ..
+qed
+
+lemma is_rbt_tree_of [simp, intro]:
+ "is_rbt (tree_of t)"
+ using tree_of [of t] by simp
+
+lemma table_eq:
+ "t1 = t2 \<longleftrightarrow> tree_of t1 = tree_of t2"
+ by (simp add: tree_of_inject)
+
+code_abstype Table tree_of
+ by (simp add: tree_of_inverse)
+
+
+subsection {* Primitive operations *}
+
+definition lookup :: "('a\<Colon>linorder, 'b) table \<Rightarrow> 'a \<rightharpoonup> 'b" where
+ [code]: "lookup t = RBT.lookup (tree_of t)"
+
+definition empty :: "('a\<Colon>linorder, 'b) table" where
+ "empty = Table RBT.Empty"
+
+lemma tree_of_empty [code abstract]:
+ "tree_of empty = RBT.Empty"
+ by (simp add: empty_def Table_inverse)
+
+definition update :: "'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table" where
+ "update k v t = Table (RBT.insert k v (tree_of t))"
+
+lemma tree_of_update [code abstract]:
+ "tree_of (update k v t) = RBT.insert k v (tree_of t)"
+ by (simp add: update_def Table_inverse)
+
+definition delete :: "'a\<Colon>linorder \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table" where
+ "delete k t = Table (RBT.delete k (tree_of t))"
+
+lemma tree_of_delete [code abstract]:
+ "tree_of (delete k t) = RBT.delete k (tree_of t)"
+ by (simp add: delete_def Table_inverse)
+
+definition entries :: "('a\<Colon>linorder, 'b) table \<Rightarrow> ('a \<times> 'b) list" where
+ [code]: "entries t = RBT.entries (tree_of t)"
+
+definition bulkload :: "('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) table" where
+ "bulkload xs = Table (RBT.bulkload xs)"
+
+lemma tree_of_bulkload [code abstract]:
+ "tree_of (bulkload xs) = RBT.bulkload xs"
+ by (simp add: bulkload_def Table_inverse)
+
+definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) table \<Rightarrow> ('a, 'b) table" where
+ "map_entry k f t = Table (RBT.map_entry k f (tree_of t))"
+
+lemma tree_of_map_entry [code abstract]:
+ "tree_of (map_entry k f t) = RBT.map_entry k f (tree_of t)"
+ by (simp add: map_entry_def Table_inverse)
+
+definition map :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) table \<Rightarrow> ('a, 'b) table" where
+ "map f t = Table (RBT.map f (tree_of t))"
+
+lemma tree_of_map [code abstract]:
+ "tree_of (map f t) = RBT.map f (tree_of t)"
+ by (simp add: map_def Table_inverse)
+
+definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) table \<Rightarrow> 'c \<Rightarrow> 'c" where
+ [code]: "fold f t = RBT.fold f (tree_of t)"
+
+
+subsection {* Derived operations *}
+
+definition is_empty :: "('a\<Colon>linorder, 'b) table \<Rightarrow> bool" where
+ [code]: "is_empty t = (case tree_of t of RBT.Empty \<Rightarrow> True | _ \<Rightarrow> False)"
+
+
+subsection {* Abstract lookup properties *}
+
+lemma lookup_Table:
+ "is_rbt t \<Longrightarrow> lookup (Table t) = RBT.lookup t"
+ by (simp add: lookup_def Table_inverse)
+
+lemma lookup_tree_of:
+ "RBT.lookup (tree_of t) = lookup t"
+ by (simp add: lookup_def)
+
+lemma entries_tree_of:
+ "RBT.entries (tree_of t) = entries t"
+ by (simp add: entries_def)
+
+lemma lookup_empty [simp]:
+ "lookup empty = Map.empty"
+ by (simp add: empty_def lookup_Table expand_fun_eq)
+
+lemma lookup_update [simp]:
+ "lookup (update k v t) = (lookup t)(k \<mapsto> v)"
+ by (simp add: update_def lookup_Table lookup_insert lookup_tree_of)
+
+lemma lookup_delete [simp]:
+ "lookup (delete k t) = (lookup t)(k := None)"
+ by (simp add: delete_def lookup_Table lookup_delete lookup_tree_of restrict_complement_singleton_eq)
+
+lemma map_of_entries [simp]:
+ "map_of (entries t) = lookup t"
+ by (simp add: entries_def map_of_entries lookup_tree_of)
+
+lemma lookup_bulkload [simp]:
+ "lookup (bulkload xs) = map_of xs"
+ by (simp add: bulkload_def lookup_Table lookup_bulkload)
+
+lemma lookup_map_entry [simp]:
+ "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))"
+ by (simp add: map_entry_def lookup_Table lookup_map_entry lookup_tree_of)
+
+lemma lookup_map [simp]:
+ "lookup (map f t) k = Option.map (f k) (lookup t k)"
+ by (simp add: map_def lookup_Table lookup_map lookup_tree_of)
+
+lemma fold_fold:
+ "fold f t = (\<lambda>s. foldl (\<lambda>s (k, v). f k v s) s (entries t))"
+ by (simp add: fold_def expand_fun_eq RBT.fold_def entries_tree_of)
+
+hide (open) const tree_of lookup empty update delete
+ entries bulkload map_entry map fold
+
+end
--- a/src/HOL/Map.thy Sat Mar 06 17:53:04 2010 +0100
+++ b/src/HOL/Map.thy Sat Mar 06 20:16:31 2010 +0100
@@ -398,6 +398,10 @@
"map_of (map (\<lambda>k. (k, f k)) ks) = (Some \<circ> f) |` set ks"
by (induct ks) (simp_all add: expand_fun_eq restrict_map_insert)
+lemma restrict_complement_singleton_eq:
+ "f |` (- {x}) = f(x := None)"
+ by (simp add: restrict_map_def expand_fun_eq)
+
subsection {* @{term [source] map_upds} *}
@@ -707,4 +711,3 @@
qed
end
-
--- a/src/HOL/ex/Codegenerator_Candidates.thy Sat Mar 06 17:53:04 2010 +0100
+++ b/src/HOL/ex/Codegenerator_Candidates.thy Sat Mar 06 20:16:31 2010 +0100
@@ -21,6 +21,7 @@
Product_ord
"~~/src/HOL/ex/Records"
SetsAndFunctions
+ Table
Tree
While_Combinator
Word