haftmann@35617: (* Author: Florian Haftmann, TU Muenchen *) haftmann@35617: haftmann@36147: header {* Abstract type of Red-Black Trees *} haftmann@35617: haftmann@36147: (*<*) haftmann@36147: theory RBT haftmann@36147: imports Main RBT_Impl Mapping haftmann@35617: begin haftmann@35617: haftmann@35617: subsection {* Type definition *} haftmann@35617: haftmann@36147: typedef (open) ('a, 'b) rbt = "{t :: ('a\linorder, 'b) RBT_Impl.rbt. is_rbt t}" haftmann@36147: morphisms impl_of RBT haftmann@35617: proof - haftmann@36147: have "RBT_Impl.Empty \ ?rbt" by simp haftmann@35617: then show ?thesis .. haftmann@35617: qed haftmann@35617: haftmann@36147: lemma is_rbt_impl_of [simp, intro]: haftmann@36147: "is_rbt (impl_of t)" haftmann@36147: using impl_of [of t] by simp haftmann@35617: haftmann@36147: lemma rbt_eq: haftmann@36147: "t1 = t2 \ impl_of t1 = impl_of t2" haftmann@36147: by (simp add: impl_of_inject) haftmann@35617: haftmann@36111: lemma [code abstype]: haftmann@36147: "RBT (impl_of t) = t" haftmann@36147: by (simp add: impl_of_inverse) haftmann@35617: haftmann@35617: haftmann@35617: subsection {* Primitive operations *} haftmann@35617: haftmann@36147: definition lookup :: "('a\linorder, 'b) rbt \ 'a \ 'b" where haftmann@36147: [code]: "lookup t = RBT_Impl.lookup (impl_of t)" haftmann@35617: haftmann@36147: definition empty :: "('a\linorder, 'b) rbt" where haftmann@36147: "empty = RBT RBT_Impl.Empty" haftmann@35617: haftmann@36147: lemma impl_of_empty [code abstract]: haftmann@36147: "impl_of empty = RBT_Impl.Empty" haftmann@36147: by (simp add: empty_def RBT_inverse) haftmann@35617: haftmann@36147: definition insert :: "'a\linorder \ 'b \ ('a, 'b) rbt \ ('a, 'b) rbt" where haftmann@36147: "insert k v t = RBT (RBT_Impl.insert k v (impl_of t))" haftmann@35617: haftmann@36147: lemma impl_of_insert [code abstract]: haftmann@36147: "impl_of (insert k v t) = RBT_Impl.insert k v (impl_of t)" haftmann@36147: by (simp add: insert_def RBT_inverse) haftmann@35617: haftmann@36147: definition delete :: "'a\linorder \ ('a, 'b) rbt \ ('a, 'b) rbt" where haftmann@36147: "delete k t = RBT (RBT_Impl.delete k (impl_of t))" haftmann@35617: haftmann@36147: lemma impl_of_delete [code abstract]: haftmann@36147: "impl_of (delete k t) = RBT_Impl.delete k (impl_of t)" haftmann@36147: by (simp add: delete_def RBT_inverse) haftmann@35617: haftmann@36147: definition entries :: "('a\linorder, 'b) rbt \ ('a \ 'b) list" where haftmann@36147: [code]: "entries t = RBT_Impl.entries (impl_of t)" haftmann@35617: haftmann@36147: definition keys :: "('a\linorder, 'b) rbt \ 'a list" where haftmann@36147: [code]: "keys t = RBT_Impl.keys (impl_of t)" haftmann@36111: haftmann@36147: definition bulkload :: "('a\linorder \ 'b) list \ ('a, 'b) rbt" where haftmann@36147: "bulkload xs = RBT (RBT_Impl.bulkload xs)" haftmann@35617: haftmann@36147: lemma impl_of_bulkload [code abstract]: haftmann@36147: "impl_of (bulkload xs) = RBT_Impl.bulkload xs" haftmann@36147: by (simp add: bulkload_def RBT_inverse) haftmann@35617: haftmann@36147: definition map_entry :: "'a \ ('b \ 'b) \ ('a\linorder, 'b) rbt \ ('a, 'b) rbt" where haftmann@36147: "map_entry k f t = RBT (RBT_Impl.map_entry k f (impl_of t))" haftmann@35617: haftmann@36147: lemma impl_of_map_entry [code abstract]: haftmann@36147: "impl_of (map_entry k f t) = RBT_Impl.map_entry k f (impl_of t)" haftmann@36147: by (simp add: map_entry_def RBT_inverse) haftmann@35617: haftmann@36147: definition map :: "('a \ 'b \ 'b) \ ('a\linorder, 'b) rbt \ ('a, 'b) rbt" where haftmann@36147: "map f t = RBT (RBT_Impl.map f (impl_of t))" haftmann@35617: haftmann@36147: lemma impl_of_map [code abstract]: haftmann@36147: "impl_of (map f t) = RBT_Impl.map f (impl_of t)" haftmann@36147: by (simp add: map_def RBT_inverse) haftmann@35617: haftmann@36147: definition fold :: "('a \ 'b \ 'c \ 'c) \ ('a\linorder, 'b) rbt \ 'c \ 'c" where haftmann@36147: [code]: "fold f t = RBT_Impl.fold f (impl_of t)" haftmann@35617: haftmann@35617: haftmann@35617: subsection {* Derived operations *} haftmann@35617: haftmann@36147: definition is_empty :: "('a\linorder, 'b) rbt \ bool" where haftmann@36147: [code]: "is_empty t = (case impl_of t of RBT_Impl.Empty \ True | _ \ False)" haftmann@35617: haftmann@35617: haftmann@35617: subsection {* Abstract lookup properties *} haftmann@35617: haftmann@36147: lemma lookup_RBT: haftmann@36147: "is_rbt t \ lookup (RBT t) = RBT_Impl.lookup t" haftmann@36147: by (simp add: lookup_def RBT_inverse) haftmann@35617: haftmann@36147: lemma lookup_impl_of: haftmann@36147: "RBT_Impl.lookup (impl_of t) = lookup t" haftmann@35617: by (simp add: lookup_def) haftmann@35617: haftmann@36147: lemma entries_impl_of: haftmann@36147: "RBT_Impl.entries (impl_of t) = entries t" haftmann@35617: by (simp add: entries_def) haftmann@35617: haftmann@36147: lemma keys_impl_of: haftmann@36147: "RBT_Impl.keys (impl_of t) = keys t" haftmann@36111: by (simp add: keys_def) haftmann@36111: haftmann@35617: lemma lookup_empty [simp]: haftmann@35617: "lookup empty = Map.empty" haftmann@36147: by (simp add: empty_def lookup_RBT expand_fun_eq) haftmann@35617: haftmann@36147: lemma lookup_insert [simp]: haftmann@36147: "lookup (insert k v t) = (lookup t)(k \ v)" haftmann@36147: by (simp add: insert_def lookup_RBT lookup_insert lookup_impl_of) haftmann@35617: haftmann@35617: lemma lookup_delete [simp]: haftmann@35617: "lookup (delete k t) = (lookup t)(k := None)" haftmann@36147: by (simp add: delete_def lookup_RBT RBT_Impl.lookup_delete lookup_impl_of restrict_complement_singleton_eq) haftmann@35617: haftmann@35617: lemma map_of_entries [simp]: haftmann@35617: "map_of (entries t) = lookup t" haftmann@36147: by (simp add: entries_def map_of_entries lookup_impl_of) haftmann@35617: haftmann@36111: lemma entries_lookup: haftmann@36111: "entries t1 = entries t2 \ lookup t1 = lookup t2" haftmann@36111: by (simp add: entries_def lookup_def entries_lookup) haftmann@36111: haftmann@35617: lemma lookup_bulkload [simp]: haftmann@35617: "lookup (bulkload xs) = map_of xs" haftmann@36147: by (simp add: bulkload_def lookup_RBT RBT_Impl.lookup_bulkload) haftmann@35617: haftmann@35617: lemma lookup_map_entry [simp]: haftmann@35617: "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))" haftmann@37027: by (simp add: map_entry_def lookup_RBT RBT_Impl.lookup_map_entry lookup_impl_of) haftmann@35617: haftmann@35617: lemma lookup_map [simp]: haftmann@35617: "lookup (map f t) k = Option.map (f k) (lookup t k)" haftmann@36147: by (simp add: map_def lookup_RBT lookup_map lookup_impl_of) haftmann@35617: haftmann@35617: lemma fold_fold: haftmann@35617: "fold f t = (\s. foldl (\s (k, v). f k v s) s (entries t))" haftmann@36147: by (simp add: fold_def expand_fun_eq RBT_Impl.fold_def entries_impl_of) haftmann@35617: haftmann@36111: lemma is_empty_empty [simp]: haftmann@36111: "is_empty t \ t = empty" haftmann@36147: by (simp add: rbt_eq is_empty_def impl_of_empty split: rbt.split) haftmann@36111: haftmann@36111: lemma RBT_lookup_empty [simp]: (*FIXME*) haftmann@36147: "RBT_Impl.lookup t = Map.empty \ t = RBT_Impl.Empty" haftmann@36111: by (cases t) (auto simp add: expand_fun_eq) haftmann@36111: haftmann@36111: lemma lookup_empty_empty [simp]: haftmann@36111: "lookup t = Map.empty \ t = empty" haftmann@36147: by (cases t) (simp add: empty_def lookup_def RBT_inject RBT_inverse) haftmann@36111: haftmann@36111: lemma sorted_keys [iff]: haftmann@36111: "sorted (keys t)" haftmann@36147: by (simp add: keys_def RBT_Impl.keys_def sorted_entries) haftmann@36111: haftmann@36111: lemma distinct_keys [iff]: haftmann@36111: "distinct (keys t)" haftmann@36147: by (simp add: keys_def RBT_Impl.keys_def distinct_entries) haftmann@36111: haftmann@36111: haftmann@36111: subsection {* Implementation of mappings *} haftmann@36111: haftmann@36147: definition Mapping :: "('a\linorder, 'b) rbt \ ('a, 'b) mapping" where haftmann@36111: "Mapping t = Mapping.Mapping (lookup t)" haftmann@36111: haftmann@36111: code_datatype Mapping haftmann@36111: haftmann@36111: lemma lookup_Mapping [simp, code]: haftmann@36111: "Mapping.lookup (Mapping t) = lookup t" haftmann@36111: by (simp add: Mapping_def) haftmann@36111: haftmann@36111: lemma empty_Mapping [code]: haftmann@36111: "Mapping.empty = Mapping empty" haftmann@36111: by (rule mapping_eqI) simp haftmann@36111: haftmann@36111: lemma is_empty_Mapping [code]: haftmann@36111: "Mapping.is_empty (Mapping t) \ is_empty t" haftmann@36147: by (simp add: rbt_eq Mapping.is_empty_empty Mapping_def) haftmann@36111: haftmann@36147: lemma insert_Mapping [code]: haftmann@36147: "Mapping.update k v (Mapping t) = Mapping (insert k v t)" haftmann@36111: by (rule mapping_eqI) simp haftmann@36111: haftmann@36111: lemma delete_Mapping [code]: haftmann@37027: "Mapping.delete k (Mapping t) = Mapping (delete k t)" haftmann@37027: by (rule mapping_eqI) simp haftmann@37027: haftmann@37027: lemma map_entry_Mapping [code]: haftmann@37027: "Mapping.map_entry k f (Mapping t) = Mapping (map_entry k f t)" haftmann@36111: by (rule mapping_eqI) simp haftmann@36111: haftmann@36111: lemma keys_Mapping [code]: haftmann@36111: "Mapping.keys (Mapping t) = set (keys t)" haftmann@36111: by (simp add: keys_def Mapping_def Mapping.keys_def lookup_def lookup_keys) haftmann@36111: haftmann@36111: lemma ordered_keys_Mapping [code]: haftmann@36111: "Mapping.ordered_keys (Mapping t) = keys t" haftmann@36111: by (rule sorted_distinct_set_unique) (simp_all add: ordered_keys_def keys_Mapping) haftmann@36111: haftmann@36111: lemma Mapping_size_card_keys: (*FIXME*) haftmann@36111: "Mapping.size m = card (Mapping.keys m)" haftmann@36111: by (simp add: Mapping.size_def Mapping.keys_def) haftmann@36111: haftmann@36111: lemma size_Mapping [code]: haftmann@36111: "Mapping.size (Mapping t) = length (keys t)" haftmann@36111: by (simp add: Mapping_size_card_keys keys_Mapping distinct_card) haftmann@36111: haftmann@36111: lemma tabulate_Mapping [code]: haftmann@36111: "Mapping.tabulate ks f = Mapping (bulkload (List.map (\k. (k, f k)) ks))" haftmann@36111: by (rule mapping_eqI) (simp add: map_of_map_restrict) haftmann@36111: haftmann@36111: lemma bulkload_Mapping [code]: haftmann@36111: "Mapping.bulkload vs = Mapping (bulkload (List.map (\n. (n, vs ! n)) [0.. x = y" by (fact eq_equals) (*FIXME*) haftmann@36111: haftmann@36111: lemma eq_Mapping [code]: haftmann@36111: "HOL.eq (Mapping t1) (Mapping t2) \ entries t1 = entries t2" haftmann@36111: by (simp add: eq Mapping_def entries_lookup) haftmann@36111: wenzelm@36176: hide_const (open) impl_of lookup empty insert delete haftmann@36111: entries keys bulkload map_entry map fold haftmann@36147: (*>*) haftmann@36147: haftmann@36147: text {* haftmann@36147: This theory defines abstract red-black trees as an efficient haftmann@36147: representation of finite maps, backed by the implementation haftmann@36147: in @{theory RBT_Impl}. haftmann@36147: *} haftmann@36147: haftmann@36147: subsection {* Data type and invariant *} haftmann@36147: haftmann@36147: text {* haftmann@36147: The type @{typ "('k, 'v) RBT_Impl.rbt"} denotes red-black trees with haftmann@36147: keys of type @{typ "'k"} and values of type @{typ "'v"}. To function haftmann@36147: properly, the key type musorted belong to the @{text "linorder"} haftmann@36147: class. haftmann@36147: haftmann@36147: A value @{term t} of this type is a valid red-black tree if it haftmann@36147: satisfies the invariant @{text "is_rbt t"}. The abstract type @{typ haftmann@36147: "('k, 'v) rbt"} always obeys this invariant, and for this reason you haftmann@36147: should only use this in our application. Going back to @{typ "('k, haftmann@36147: 'v) RBT_Impl.rbt"} may be necessary in proofs if not yet proven haftmann@36147: properties about the operations must be established. haftmann@36147: haftmann@36147: The interpretation function @{const "RBT.lookup"} returns the partial haftmann@36147: map represented by a red-black tree: haftmann@36147: @{term_type[display] "RBT.lookup"} haftmann@36147: haftmann@36147: This function should be used for reasoning about the semantics of the RBT haftmann@36147: operations. Furthermore, it implements the lookup functionality for haftmann@36147: the data structure: It is executable and the lookup is performed in haftmann@36147: $O(\log n)$. haftmann@36147: *} haftmann@36147: haftmann@36147: subsection {* Operations *} haftmann@36147: haftmann@36147: text {* haftmann@36147: Currently, the following operations are supported: haftmann@36147: haftmann@36147: @{term_type [display] "RBT.empty"} haftmann@36147: Returns the empty tree. $O(1)$ haftmann@36147: haftmann@36147: @{term_type [display] "RBT.insert"} haftmann@36147: Updates the map at a given position. $O(\log n)$ haftmann@36147: haftmann@36147: @{term_type [display] "RBT.delete"} haftmann@36147: Deletes a map entry at a given position. $O(\log n)$ haftmann@36147: haftmann@36147: @{term_type [display] "RBT.entries"} haftmann@36147: Return a corresponding key-value list for a tree. haftmann@36147: haftmann@36147: @{term_type [display] "RBT.bulkload"} haftmann@36147: Builds a tree from a key-value list. haftmann@36147: haftmann@36147: @{term_type [display] "RBT.map_entry"} haftmann@36147: Maps a single entry in a tree. haftmann@36147: haftmann@36147: @{term_type [display] "RBT.map"} haftmann@36147: Maps all values in a tree. $O(n)$ haftmann@36147: haftmann@36147: @{term_type [display] "RBT.fold"} haftmann@36147: Folds over all entries in a tree. $O(n)$ haftmann@36147: *} haftmann@36147: haftmann@36147: haftmann@36147: subsection {* Invariant preservation *} haftmann@36147: haftmann@36147: text {* haftmann@36147: \noindent haftmann@36147: @{thm Empty_is_rbt}\hfill(@{text "Empty_is_rbt"}) haftmann@36147: haftmann@36147: \noindent haftmann@36147: @{thm insert_is_rbt}\hfill(@{text "insert_is_rbt"}) haftmann@36147: haftmann@36147: \noindent haftmann@36147: @{thm delete_is_rbt}\hfill(@{text "delete_is_rbt"}) haftmann@36147: haftmann@36147: \noindent haftmann@36147: @{thm bulkload_is_rbt}\hfill(@{text "bulkload_is_rbt"}) haftmann@36147: haftmann@36147: \noindent haftmann@36147: @{thm map_entry_is_rbt}\hfill(@{text "map_entry_is_rbt"}) haftmann@36147: haftmann@36147: \noindent haftmann@36147: @{thm map_is_rbt}\hfill(@{text "map_is_rbt"}) haftmann@36147: haftmann@36147: \noindent haftmann@36147: @{thm union_is_rbt}\hfill(@{text "union_is_rbt"}) haftmann@36147: *} haftmann@36147: haftmann@36147: haftmann@36147: subsection {* Map Semantics *} haftmann@36147: haftmann@36147: text {* haftmann@36147: \noindent haftmann@36147: \underline{@{text "lookup_empty"}} haftmann@36147: @{thm [display] lookup_empty} haftmann@36147: \vspace{1ex} haftmann@36147: haftmann@36147: \noindent haftmann@36147: \underline{@{text "lookup_insert"}} haftmann@36147: @{thm [display] lookup_insert} haftmann@36147: \vspace{1ex} haftmann@36147: haftmann@36147: \noindent haftmann@36147: \underline{@{text "lookup_delete"}} haftmann@36147: @{thm [display] lookup_delete} haftmann@36147: \vspace{1ex} haftmann@36147: haftmann@36147: \noindent haftmann@36147: \underline{@{text "lookup_bulkload"}} haftmann@36147: @{thm [display] lookup_bulkload} haftmann@36147: \vspace{1ex} haftmann@36147: haftmann@36147: \noindent haftmann@36147: \underline{@{text "lookup_map"}} haftmann@36147: @{thm [display] lookup_map} haftmann@36147: \vspace{1ex} haftmann@36147: *} haftmann@35617: haftmann@35617: end