# HG changeset patch # User bulwahn # Date 1306912213 -7200 # Node ID fdb7e1d5f762e71ef2613bdc0237595d2ae02306 # Parent 28e6351b2f8e35be5643b446d36fe189e72760a9 splitting RBT theory into RBT and RBT_Mapping diff -r 28e6351b2f8e -r fdb7e1d5f762 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Jun 01 08:07:28 2011 +0200 +++ b/src/HOL/IsaMakefile Wed Jun 01 09:10:13 2011 +0200 @@ -467,7 +467,8 @@ Library/Quotient_List.thy Library/Quotient_Option.thy \ Library/Quotient_Product.thy Library/Quotient_Sum.thy \ Library/Quotient_Syntax.thy Library/Quotient_Type.thy \ - Library/RBT.thy Library/RBT_Impl.thy Library/README.html \ + Library/RBT.thy Library/RBT_Impl.thy Library/RBT_Mapping.thy \ + Library/README.html \ Library/Set_Algebras.thy Library/State_Monad.thy Library/Ramsey.thy \ Library/Reflection.thy Library/SML_Quickcheck.thy \ Library/Sublist_Order.thy Library/Sum_of_Squares.thy \ diff -r 28e6351b2f8e -r fdb7e1d5f762 src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Wed Jun 01 08:07:28 2011 +0200 +++ b/src/HOL/Library/Library.thy Wed Jun 01 09:10:13 2011 +0200 @@ -52,7 +52,7 @@ Quotient_Type Ramsey Reflection - RBT + RBT_Mapping Set_Algebras SML_Quickcheck State_Monad diff -r 28e6351b2f8e -r fdb7e1d5f762 src/HOL/Library/RBT.thy --- a/src/HOL/Library/RBT.thy Wed Jun 01 08:07:28 2011 +0200 +++ b/src/HOL/Library/RBT.thy Wed Jun 01 09:10:13 2011 +0200 @@ -4,7 +4,7 @@ (*<*) theory RBT -imports Main RBT_Impl Mapping +imports Main RBT_Impl begin subsection {* Type definition *} @@ -171,189 +171,4 @@ by (simp add: keys_def RBT_Impl.keys_def distinct_entries) -subsection {* Implementation of mappings *} - -definition Mapping :: "('a\linorder, 'b) rbt \ ('a, 'b) mapping" where - "Mapping t = Mapping.Mapping (lookup t)" - -code_datatype Mapping - -lemma lookup_Mapping [simp, code]: - "Mapping.lookup (Mapping t) = lookup t" - by (simp add: Mapping_def) - -lemma empty_Mapping [code]: - "Mapping.empty = Mapping empty" - by (rule mapping_eqI) simp - -lemma is_empty_Mapping [code]: - "Mapping.is_empty (Mapping t) \ is_empty t" - by (simp add: rbt_eq_iff Mapping.is_empty_empty Mapping_def) - -lemma insert_Mapping [code]: - "Mapping.update k v (Mapping t) = Mapping (insert k v t)" - by (rule mapping_eqI) simp - -lemma delete_Mapping [code]: - "Mapping.delete k (Mapping t) = Mapping (delete k t)" - by (rule mapping_eqI) simp - -lemma map_entry_Mapping [code]: - "Mapping.map_entry k f (Mapping t) = Mapping (map_entry k f t)" - by (rule mapping_eqI) simp - -lemma keys_Mapping [code]: - "Mapping.keys (Mapping t) = set (keys t)" - by (simp add: keys_def Mapping_def Mapping.keys_def lookup_def lookup_keys) - -lemma ordered_keys_Mapping [code]: - "Mapping.ordered_keys (Mapping t) = keys t" - by (rule sorted_distinct_set_unique) (simp_all add: ordered_keys_def keys_Mapping) - -lemma Mapping_size_card_keys: (*FIXME*) - "Mapping.size m = card (Mapping.keys m)" - by (simp add: Mapping.size_def Mapping.keys_def) - -lemma size_Mapping [code]: - "Mapping.size (Mapping t) = length (keys t)" - by (simp add: Mapping_size_card_keys keys_Mapping distinct_card) - -lemma tabulate_Mapping [code]: - "Mapping.tabulate ks f = Mapping (bulkload (List.map (\k. (k, f k)) ks))" - by (rule mapping_eqI) (simp add: map_of_map_restrict) - -lemma bulkload_Mapping [code]: - "Mapping.bulkload vs = Mapping (bulkload (List.map (\n. (n, vs ! n)) [0.. entries t1 = entries t2" - by (simp add: equal Mapping_def entries_lookup) - -lemma [code nbe]: - "HOL.equal (x :: (_, _) mapping) x \ True" - by (fact equal_refl) - - -hide_const (open) impl_of lookup empty insert delete - entries keys bulkload map_entry map fold -(*>*) - -text {* - This theory defines abstract red-black trees as an efficient - representation of finite maps, backed by the implementation - in @{theory RBT_Impl}. -*} - -subsection {* Data type and invariant *} - -text {* - The type @{typ "('k, 'v) RBT_Impl.rbt"} denotes red-black trees with - keys of type @{typ "'k"} and values of type @{typ "'v"}. To function - properly, the key type musorted belong to the @{text "linorder"} - class. - - A value @{term t} of this type is a valid red-black tree if it - satisfies the invariant @{text "is_rbt t"}. The abstract type @{typ - "('k, 'v) rbt"} always obeys this invariant, and for this reason you - should only use this in our application. Going back to @{typ "('k, - 'v) RBT_Impl.rbt"} may be necessary in proofs if not yet proven - properties about the operations must be established. - - The interpretation function @{const "RBT.lookup"} 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)$. -*} - -subsection {* Operations *} - -text {* - 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)$ -*} - - -subsection {* Invariant preservation *} - -text {* - \noindent - @{thm Empty_is_rbt}\hfill(@{text "Empty_is_rbt"}) - - \noindent - @{thm insert_is_rbt}\hfill(@{text "insert_is_rbt"}) - - \noindent - @{thm delete_is_rbt}\hfill(@{text "delete_is_rbt"}) - - \noindent - @{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"}) -*} - - -subsection {* Map Semantics *} - -text {* - \noindent - \underline{@{text "lookup_empty"}} - @{thm [display] lookup_empty} - \vspace{1ex} - - \noindent - \underline{@{text "lookup_insert"}} - @{thm [display] lookup_insert} - \vspace{1ex} - - \noindent - \underline{@{text "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} -*} - end diff -r 28e6351b2f8e -r fdb7e1d5f762 src/HOL/Library/RBT_Mapping.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/RBT_Mapping.thy Wed Jun 01 09:10:13 2011 +0200 @@ -0,0 +1,195 @@ +(* Author: Florian Haftmann, TU Muenchen *) + +header {* Implementation of mappings with Red-Black Trees *} + +(*<*) +theory RBT_Mapping +imports RBT Mapping +begin + +subsection {* Implementation of mappings *} + +definition Mapping :: "('a\linorder, 'b) rbt \ ('a, 'b) mapping" where + "Mapping t = Mapping.Mapping (lookup t)" + +code_datatype Mapping + +lemma lookup_Mapping [simp, code]: + "Mapping.lookup (Mapping t) = lookup t" + by (simp add: Mapping_def) + +lemma empty_Mapping [code]: + "Mapping.empty = Mapping empty" + by (rule mapping_eqI) simp + +lemma is_empty_Mapping [code]: + "Mapping.is_empty (Mapping t) \ is_empty t" + by (simp add: rbt_eq_iff Mapping.is_empty_empty Mapping_def) + +lemma insert_Mapping [code]: + "Mapping.update k v (Mapping t) = Mapping (insert k v t)" + by (rule mapping_eqI) simp + +lemma delete_Mapping [code]: + "Mapping.delete k (Mapping t) = Mapping (delete k t)" + by (rule mapping_eqI) simp + +lemma map_entry_Mapping [code]: + "Mapping.map_entry k f (Mapping t) = Mapping (map_entry k f t)" + by (rule mapping_eqI) simp + +lemma keys_Mapping [code]: + "Mapping.keys (Mapping t) = set (keys t)" + by (simp add: RBT.keys_def Mapping_def Mapping.keys_def lookup_def lookup_keys) + +lemma ordered_keys_Mapping [code]: + "Mapping.ordered_keys (Mapping t) = keys t" + by (rule sorted_distinct_set_unique) (simp_all add: ordered_keys_def keys_Mapping) + +lemma Mapping_size_card_keys: (*FIXME*) + "Mapping.size m = card (Mapping.keys m)" + by (simp add: Mapping.size_def Mapping.keys_def) + +lemma size_Mapping [code]: + "Mapping.size (Mapping t) = length (keys t)" + by (simp add: Mapping_size_card_keys keys_Mapping distinct_card) + +lemma tabulate_Mapping [code]: + "Mapping.tabulate ks f = Mapping (bulkload (List.map (\k. (k, f k)) ks))" + by (rule mapping_eqI) (simp add: map_of_map_restrict) + +lemma bulkload_Mapping [code]: + "Mapping.bulkload vs = Mapping (bulkload (List.map (\n. (n, vs ! n)) [0.. entries t1 = entries t2" + by (simp add: equal Mapping_def entries_lookup) + +lemma [code nbe]: + "HOL.equal (x :: (_, _) mapping) x \ True" + by (fact equal_refl) + + +hide_const (open) impl_of lookup empty insert delete + entries keys bulkload map_entry map fold +(*>*) + +text {* + This theory defines abstract red-black trees as an efficient + representation of finite maps, backed by the implementation + in @{theory RBT_Impl}. +*} + +subsection {* Data type and invariant *} + +text {* + The type @{typ "('k, 'v) RBT_Impl.rbt"} denotes red-black trees with + keys of type @{typ "'k"} and values of type @{typ "'v"}. To function + properly, the key type musorted belong to the @{text "linorder"} + class. + + A value @{term t} of this type is a valid red-black tree if it + satisfies the invariant @{text "is_rbt t"}. The abstract type @{typ + "('k, 'v) rbt"} always obeys this invariant, and for this reason you + should only use this in our application. Going back to @{typ "('k, + 'v) RBT_Impl.rbt"} may be necessary in proofs if not yet proven + properties about the operations must be established. + + The interpretation function @{const "RBT.lookup"} 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)$. +*} + +subsection {* Operations *} + +text {* + 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)$ +*} + + +subsection {* Invariant preservation *} + +text {* + \noindent + @{thm Empty_is_rbt}\hfill(@{text "Empty_is_rbt"}) + + \noindent + @{thm insert_is_rbt}\hfill(@{text "insert_is_rbt"}) + + \noindent + @{thm delete_is_rbt}\hfill(@{text "delete_is_rbt"}) + + \noindent + @{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"}) +*} + + +subsection {* Map Semantics *} + +text {* + \noindent + \underline{@{text "lookup_empty"}} + @{thm [display] lookup_empty} + \vspace{1ex} + + \noindent + \underline{@{text "lookup_insert"}} + @{thm [display] lookup_insert} + \vspace{1ex} + + \noindent + \underline{@{text "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} +*} + +end \ No newline at end of file