lemma insert_Mapping [code]: "Mapping.update k v (Mapping t) = Mapping (RBT.insert k v t)" by (transfer fixing: t) simp
lemma delete_Mapping [code]: "Mapping.delete k (Mapping t) = Mapping (RBT.delete k t)" by (transfer fixing: t) simp
lemma map_entry_Mapping [code]: "Mapping.map_entry k f (Mapping t) = Mapping (RBT.map_entry k f t)" apply (transfer fixing: t) apply (case_tac "RBT.lookup t k") apply auto done
lemma keys_Mapping [code]: "Mapping.keys (Mapping t) = set (RBT.keys t)" by (transfer fixing: t) (simp add: lookup_keys)
context notes RBT.bulkload.transfer[transfer_rule del] begin
lemma tabulate_Mapping [code]: "Mapping.tabulate ks f = Mapping (RBT.bulkload (List.map (\k. (k, f k)) ks))" by transfer (simp add: map_of_map_restrict)
lemma bulkload_Mapping [code]: "Mapping.bulkload vs = Mapping (RBT.bulkload (List.map (\n. (n, vs ! n)) [0.. by transfer (simp add: map_of_map_restrict fun_eq_iff)
end
lemma map_values_Mapping [code]: "Mapping.map_values f (Mapping t) = Mapping (RBT.map f t)" by (transfer fixing: t) (auto simp: fun_eq_iff)
lemma filter_Mapping [code]: "Mapping.filter P (Mapping t) = Mapping (RBT.filter P t)" by (transfer' fixing: P t) (simp add: RBT.lookup_filter fun_eq_iff)
lemma combine_with_key_Mapping [code]: "Mapping.combine_with_key f (Mapping t1) (Mapping t2) =
Mapping (RBT.combine_with_key f t1 t2)" by (transfer fixing: f t1 t2) (simp_all add: fun_eq_iff)
lemma combine_Mapping [code]: "Mapping.combine f (Mapping t1) (Mapping t2) =
Mapping (RBT.combine f t1 t2)" by (transfer fixing: f t1 t2) (simp_all add: fun_eq_iff)
lemma [code nbe]: "HOL.equal (x :: (_, _) mapping) x \ True" by (fact equal_refl)
end
(*>*)
text\<open>
This theorydefines abstract red-black trees as an efficient
representation of finite maps, backed by the implementation in\<^theory>\<open>HOL-Library.RBT_Impl\<close>. \<close>
subsection \<open>Data type and invariant\<close>
text\<open>
The type \<^typ>\<open>('k, 'v) RBT_Impl.rbt\<close> denotes red-black trees with
keys of type \<^typ>\<open>'k\<close> and values of type \<^typ>\<open>'v\<close>. To function
properly, the key type musorted belong to the \<open>linorder\<close> class.
A value\<^term>\<open>t\<close> of this type is a valid red-black tree if it
satisfies the invariant \<open>is_rbt t\<close>. The abstract type \<^typ>\<open>('k, 'v) rbt\<close> always obeys this invariant, and for this reason you
should only use this in our application. Going backto\<^typ>\<open>('k, 'v) RBT_Impl.rbt\ may be necessary in proofs if not yet proven
properties about the operations must be established.
The interpretationfunction\<^const>\<open>RBT.lookup\<close> returns the partial
map represented by a red-black tree:
@{term_type[display] "RBT.lookup"}
This function should be used for reasoning about the semantics of the RBT
operations. Furthermore, it implements the lookup functionality for
the data structure: It is executable and the lookup is performed in
$O(\log n)$. \<close>
subsection \<open>Operations\<close>
text\<open>
Currently, the following operations are supported:
@{term_type [display] "RBT.empty"}
Returns the empty tree. $O(1)$
@{term_type [display] "RBT.insert"}
Updates the map at a given position. $O(\log n)$
@{term_type [display] "RBT.delete"}
Deletes a map entry at a given position. $O(\log n)$
@{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 all values in a tree. $O(n)$
@{term_type [display] "RBT.fold"}
Folds over all entries in a tree. $O(n)$ \<close>
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
