# HG changeset patch # User haftmann # Date 1267865908 -3600 # Node ID 7c5b40c7e8c40a6590c914d5c48e2859dbdf2cfc # Parent 13cf538a17b1ebbf78703ca43e1948b4f854f2af added bulkload; tuned document diff -r 13cf538a17b1 -r 7c5b40c7e8c4 src/HOL/Library/RBT.thy --- 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 \ f k v \ 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 \ 'b) list \ ('a\linorder, 'b) rbt" where (*FIXME move*) + "bulkload xs = foldr (\(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 "\t. is_rbt t \ + RBT.lookup (foldl (\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 (\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} *}