--- a/src/HOL/Library/RBT.thy Sat Mar 06 07:30:21 2010 +0100
+++ b/src/HOL/Library/RBT.thy Sat Mar 06 09:58:28 2010 +0100
@@ -1054,7 +1054,30 @@
"fold f (Branch c lt k v rt) = fold f rt \<circ> f k v \<circ> fold f lt"
by (simp_all add: fold_def expand_fun_eq)
-hide (open) const Empty insert delete entries lookup map_entry map fold union sorted
+
+subsection {* Bulkloading a tree *}
+
+definition bulkload :: "('a \<times> 'b) list \<Rightarrow> ('a\<Colon>linorder, 'b) rbt" where (*FIXME move*)
+ "bulkload xs = foldr (\<lambda>(k, v). RBT.insert k v) xs RBT.Empty"
+
+lemma bulkload_is_rbt [simp, intro]:
+ "is_rbt (bulkload xs)"
+ unfolding bulkload_def by (induct xs) auto
+
+lemma lookup_bulkload:
+ "RBT.lookup (bulkload xs) = map_of xs"
+proof -
+ obtain ys where "ys = rev xs" by simp
+ have "\<And>t. is_rbt t \<Longrightarrow>
+ RBT.lookup (foldl (\<lambda>t (k, v). RBT.insert k v t) t ys) = RBT.lookup t ++ map_of (rev ys)"
+ by (induct ys) (simp_all add: bulkload_def split_def RBT.lookup_insert)
+ from this Empty_is_rbt have
+ "RBT.lookup (foldl (\<lambda>t (k, v). RBT.insert k v t) RBT.Empty (rev xs)) = RBT.lookup RBT.Empty ++ map_of xs"
+ by (simp add: `ys = rev xs`)
+ then show ?thesis by (simp add: bulkload_def foldl_foldr lookup_Empty split_def)
+qed
+
+hide (open) const Empty insert delete entries bulkload lookup map_entry map fold union sorted
(*>*)
text {*
@@ -1081,30 +1104,44 @@
This function should be used for reasoning about the semantics of the RBT
operations. Furthermore, it implements the lookup functionality for
- the data sortedructure: It is executable and the lookup is performed in
+ the data structure: It is executable and the lookup is performed in
$O(\log n)$.
*}
subsection {* Operations *}
+print_antiquotations
+
text {*
Currently, the following operations are supported:
- @{term_type[display] "RBT.Empty"}
+ @{term_type [display] "RBT.Empty"}
Returns the empty tree. $O(1)$
- @{term_type[display] "RBT.insert"}
+ @{term_type [display] "RBT.insert"}
Updates the map at a given position. $O(\log n)$
- @{term_type[display] "RBT.delete"}
+ @{term_type [display] "RBT.delete"}
Deletes a map entry at a given position. $O(\log n)$
- @{term_type[display] "RBT.union"}
- Forms the union of two trees, preferring entries from the first one.
+ @{term_type [display] "RBT.entries"}
+ Return a corresponding key-value list for a tree.
+
+ @{term_type [display] "RBT.bulkload"}
+ Builds a tree from a key-value list.
+
+ @{term_type [display] "RBT.map_entry"}
+ Maps a single entry in a tree.
- @{term_type[display] "RBT.map"}
- Maps a function over the values of a map. $O(n)$
+ @{term_type [display] "RBT.map"}
+ Maps all values in a tree. $O(n)$
+
+ @{term_type [display] "RBT.fold"}
+ Folds over all entries in a tree. $O(n)$
+
+ @{term_type [display] "RBT.union"}
+ Forms the union of two trees, preferring entries from the first one.
*}
@@ -1121,10 +1158,16 @@
@{thm delete_is_rbt}\hfill(@{text "delete_is_rbt"})
\noindent
- @{thm union_is_rbt}\hfill(@{text "union_is_rbt"})
+ @{thm bulkload_is_rbt}\hfill(@{text "bulkload_is_rbt"})
+
+ \noindent
+ @{thm map_entry_is_rbt}\hfill(@{text "map_entry_is_rbt"})
\noindent
@{thm map_is_rbt}\hfill(@{text "map_is_rbt"})
+
+ \noindent
+ @{thm union_is_rbt}\hfill(@{text "union_is_rbt"})
*}
@@ -1133,27 +1176,32 @@
text {*
\noindent
\underline{@{text "lookup_Empty"}}
- @{thm[display] lookup_Empty}
+ @{thm [display] lookup_Empty}
\vspace{1ex}
\noindent
\underline{@{text "lookup_insert"}}
- @{thm[display] lookup_insert}
+ @{thm [display] lookup_insert}
\vspace{1ex}
\noindent
\underline{@{text "lookup_delete"}}
- @{thm[display] lookup_delete}
+ @{thm [display] lookup_delete}
+ \vspace{1ex}
+
+ \noindent
+ \underline{@{text "lookup_bulkload"}}
+ @{thm [display] lookup_bulkload}
+ \vspace{1ex}
+
+ \noindent
+ \underline{@{text "lookup_map"}}
+ @{thm [display] lookup_map}
\vspace{1ex}
\noindent
\underline{@{text "lookup_union"}}
- @{thm[display] lookup_union}
- \vspace{1ex}
-
- \noindent
- \underline{@{text "lookup_map"}}
- @{thm[display] lookup_map}
+ @{thm [display] lookup_union}
\vspace{1ex}
*}