splitting RBT theory into RBT and RBT_Mapping
authorbulwahn
Wed Jun 01 09:10:13 2011 +0200 (2011-06-01)
changeset 43124fdb7e1d5f762
parent 43123 28e6351b2f8e
child 43125 ddf63baabdec
splitting RBT theory into RBT and RBT_Mapping
src/HOL/IsaMakefile
src/HOL/Library/Library.thy
src/HOL/Library/RBT.thy
src/HOL/Library/RBT_Mapping.thy
     1.1 --- a/src/HOL/IsaMakefile	Wed Jun 01 08:07:28 2011 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Wed Jun 01 09:10:13 2011 +0200
     1.3 @@ -467,7 +467,8 @@
     1.4    Library/Quotient_List.thy Library/Quotient_Option.thy			\
     1.5    Library/Quotient_Product.thy Library/Quotient_Sum.thy			\
     1.6    Library/Quotient_Syntax.thy Library/Quotient_Type.thy			\
     1.7 -  Library/RBT.thy Library/RBT_Impl.thy Library/README.html		\
     1.8 +  Library/RBT.thy Library/RBT_Impl.thy Library/RBT_Mapping.thy 		\
     1.9 +  Library/README.html 							\
    1.10    Library/Set_Algebras.thy Library/State_Monad.thy Library/Ramsey.thy	\
    1.11    Library/Reflection.thy Library/SML_Quickcheck.thy 			\
    1.12    Library/Sublist_Order.thy Library/Sum_of_Squares.thy			\
     2.1 --- a/src/HOL/Library/Library.thy	Wed Jun 01 08:07:28 2011 +0200
     2.2 +++ b/src/HOL/Library/Library.thy	Wed Jun 01 09:10:13 2011 +0200
     2.3 @@ -52,7 +52,7 @@
     2.4    Quotient_Type
     2.5    Ramsey
     2.6    Reflection
     2.7 -  RBT
     2.8 +  RBT_Mapping
     2.9    Set_Algebras
    2.10    SML_Quickcheck
    2.11    State_Monad
     3.1 --- a/src/HOL/Library/RBT.thy	Wed Jun 01 08:07:28 2011 +0200
     3.2 +++ b/src/HOL/Library/RBT.thy	Wed Jun 01 09:10:13 2011 +0200
     3.3 @@ -4,7 +4,7 @@
     3.4  
     3.5  (*<*)
     3.6  theory RBT
     3.7 -imports Main RBT_Impl Mapping
     3.8 +imports Main RBT_Impl
     3.9  begin
    3.10  
    3.11  subsection {* Type definition *}
    3.12 @@ -171,189 +171,4 @@
    3.13    by (simp add: keys_def RBT_Impl.keys_def distinct_entries)
    3.14  
    3.15  
    3.16 -subsection {* Implementation of mappings *}
    3.17 -
    3.18 -definition Mapping :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) mapping" where
    3.19 -  "Mapping t = Mapping.Mapping (lookup t)"
    3.20 -
    3.21 -code_datatype Mapping
    3.22 -
    3.23 -lemma lookup_Mapping [simp, code]:
    3.24 -  "Mapping.lookup (Mapping t) = lookup t"
    3.25 -  by (simp add: Mapping_def)
    3.26 -
    3.27 -lemma empty_Mapping [code]:
    3.28 -  "Mapping.empty = Mapping empty"
    3.29 -  by (rule mapping_eqI) simp
    3.30 -
    3.31 -lemma is_empty_Mapping [code]:
    3.32 -  "Mapping.is_empty (Mapping t) \<longleftrightarrow> is_empty t"
    3.33 -  by (simp add: rbt_eq_iff Mapping.is_empty_empty Mapping_def)
    3.34 -
    3.35 -lemma insert_Mapping [code]:
    3.36 -  "Mapping.update k v (Mapping t) = Mapping (insert k v t)"
    3.37 -  by (rule mapping_eqI) simp
    3.38 -
    3.39 -lemma delete_Mapping [code]:
    3.40 -  "Mapping.delete k (Mapping t) = Mapping (delete k t)"
    3.41 -  by (rule mapping_eqI) simp
    3.42 -
    3.43 -lemma map_entry_Mapping [code]:
    3.44 -  "Mapping.map_entry k f (Mapping t) = Mapping (map_entry k f t)"
    3.45 -  by (rule mapping_eqI) simp
    3.46 -
    3.47 -lemma keys_Mapping [code]:
    3.48 -  "Mapping.keys (Mapping t) = set (keys t)"
    3.49 -  by (simp add: keys_def Mapping_def Mapping.keys_def lookup_def lookup_keys)
    3.50 -
    3.51 -lemma ordered_keys_Mapping [code]:
    3.52 -  "Mapping.ordered_keys (Mapping t) = keys t"
    3.53 -  by (rule sorted_distinct_set_unique) (simp_all add: ordered_keys_def keys_Mapping)
    3.54 -
    3.55 -lemma Mapping_size_card_keys: (*FIXME*)
    3.56 -  "Mapping.size m = card (Mapping.keys m)"
    3.57 -  by (simp add: Mapping.size_def Mapping.keys_def)
    3.58 -
    3.59 -lemma size_Mapping [code]:
    3.60 -  "Mapping.size (Mapping t) = length (keys t)"
    3.61 -  by (simp add: Mapping_size_card_keys keys_Mapping distinct_card)
    3.62 -
    3.63 -lemma tabulate_Mapping [code]:
    3.64 -  "Mapping.tabulate ks f = Mapping (bulkload (List.map (\<lambda>k. (k, f k)) ks))"
    3.65 -  by (rule mapping_eqI) (simp add: map_of_map_restrict)
    3.66 -
    3.67 -lemma bulkload_Mapping [code]:
    3.68 -  "Mapping.bulkload vs = Mapping (bulkload (List.map (\<lambda>n. (n, vs ! n)) [0..<length vs]))"
    3.69 -  by (rule mapping_eqI) (simp add: map_of_map_restrict fun_eq_iff)
    3.70 -
    3.71 -lemma equal_Mapping [code]:
    3.72 -  "HOL.equal (Mapping t1) (Mapping t2) \<longleftrightarrow> entries t1 = entries t2"
    3.73 -  by (simp add: equal Mapping_def entries_lookup)
    3.74 -
    3.75 -lemma [code nbe]:
    3.76 -  "HOL.equal (x :: (_, _) mapping) x \<longleftrightarrow> True"
    3.77 -  by (fact equal_refl)
    3.78 -
    3.79 -
    3.80 -hide_const (open) impl_of lookup empty insert delete
    3.81 -  entries keys bulkload map_entry map fold
    3.82 -(*>*)
    3.83 -
    3.84 -text {* 
    3.85 -  This theory defines abstract red-black trees as an efficient
    3.86 -  representation of finite maps, backed by the implementation
    3.87 -  in @{theory RBT_Impl}.
    3.88 -*}
    3.89 -
    3.90 -subsection {* Data type and invariant *}
    3.91 -
    3.92 -text {*
    3.93 -  The type @{typ "('k, 'v) RBT_Impl.rbt"} denotes red-black trees with
    3.94 -  keys of type @{typ "'k"} and values of type @{typ "'v"}. To function
    3.95 -  properly, the key type musorted belong to the @{text "linorder"}
    3.96 -  class.
    3.97 -
    3.98 -  A value @{term t} of this type is a valid red-black tree if it
    3.99 -  satisfies the invariant @{text "is_rbt t"}.  The abstract type @{typ
   3.100 -  "('k, 'v) rbt"} always obeys this invariant, and for this reason you
   3.101 -  should only use this in our application.  Going back to @{typ "('k,
   3.102 -  'v) RBT_Impl.rbt"} may be necessary in proofs if not yet proven
   3.103 -  properties about the operations must be established.
   3.104 -
   3.105 -  The interpretation function @{const "RBT.lookup"} returns the partial
   3.106 -  map represented by a red-black tree:
   3.107 -  @{term_type[display] "RBT.lookup"}
   3.108 -
   3.109 -  This function should be used for reasoning about the semantics of the RBT
   3.110 -  operations. Furthermore, it implements the lookup functionality for
   3.111 -  the data structure: It is executable and the lookup is performed in
   3.112 -  $O(\log n)$.  
   3.113 -*}
   3.114 -
   3.115 -subsection {* Operations *}
   3.116 -
   3.117 -text {*
   3.118 -  Currently, the following operations are supported:
   3.119 -
   3.120 -  @{term_type [display] "RBT.empty"}
   3.121 -  Returns the empty tree. $O(1)$
   3.122 -
   3.123 -  @{term_type [display] "RBT.insert"}
   3.124 -  Updates the map at a given position. $O(\log n)$
   3.125 -
   3.126 -  @{term_type [display] "RBT.delete"}
   3.127 -  Deletes a map entry at a given position. $O(\log n)$
   3.128 -
   3.129 -  @{term_type [display] "RBT.entries"}
   3.130 -  Return a corresponding key-value list for a tree.
   3.131 -
   3.132 -  @{term_type [display] "RBT.bulkload"}
   3.133 -  Builds a tree from a key-value list.
   3.134 -
   3.135 -  @{term_type [display] "RBT.map_entry"}
   3.136 -  Maps a single entry in a tree.
   3.137 -
   3.138 -  @{term_type [display] "RBT.map"}
   3.139 -  Maps all values in a tree. $O(n)$
   3.140 -
   3.141 -  @{term_type [display] "RBT.fold"}
   3.142 -  Folds over all entries in a tree. $O(n)$
   3.143 -*}
   3.144 -
   3.145 -
   3.146 -subsection {* Invariant preservation *}
   3.147 -
   3.148 -text {*
   3.149 -  \noindent
   3.150 -  @{thm Empty_is_rbt}\hfill(@{text "Empty_is_rbt"})
   3.151 -
   3.152 -  \noindent
   3.153 -  @{thm insert_is_rbt}\hfill(@{text "insert_is_rbt"})
   3.154 -
   3.155 -  \noindent
   3.156 -  @{thm delete_is_rbt}\hfill(@{text "delete_is_rbt"})
   3.157 -
   3.158 -  \noindent
   3.159 -  @{thm bulkload_is_rbt}\hfill(@{text "bulkload_is_rbt"})
   3.160 -
   3.161 -  \noindent
   3.162 -  @{thm map_entry_is_rbt}\hfill(@{text "map_entry_is_rbt"})
   3.163 -
   3.164 -  \noindent
   3.165 -  @{thm map_is_rbt}\hfill(@{text "map_is_rbt"})
   3.166 -
   3.167 -  \noindent
   3.168 -  @{thm union_is_rbt}\hfill(@{text "union_is_rbt"})
   3.169 -*}
   3.170 -
   3.171 -
   3.172 -subsection {* Map Semantics *}
   3.173 -
   3.174 -text {*
   3.175 -  \noindent
   3.176 -  \underline{@{text "lookup_empty"}}
   3.177 -  @{thm [display] lookup_empty}
   3.178 -  \vspace{1ex}
   3.179 -
   3.180 -  \noindent
   3.181 -  \underline{@{text "lookup_insert"}}
   3.182 -  @{thm [display] lookup_insert}
   3.183 -  \vspace{1ex}
   3.184 -
   3.185 -  \noindent
   3.186 -  \underline{@{text "lookup_delete"}}
   3.187 -  @{thm [display] lookup_delete}
   3.188 -  \vspace{1ex}
   3.189 -
   3.190 -  \noindent
   3.191 -  \underline{@{text "lookup_bulkload"}}
   3.192 -  @{thm [display] lookup_bulkload}
   3.193 -  \vspace{1ex}
   3.194 -
   3.195 -  \noindent
   3.196 -  \underline{@{text "lookup_map"}}
   3.197 -  @{thm [display] lookup_map}
   3.198 -  \vspace{1ex}
   3.199 -*}
   3.200 -
   3.201  end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Library/RBT_Mapping.thy	Wed Jun 01 09:10:13 2011 +0200
     4.3 @@ -0,0 +1,195 @@
     4.4 +(* Author: Florian Haftmann, TU Muenchen *)
     4.5 +
     4.6 +header {* Implementation of mappings with Red-Black Trees *}
     4.7 +
     4.8 +(*<*)
     4.9 +theory RBT_Mapping
    4.10 +imports RBT Mapping
    4.11 +begin
    4.12 +
    4.13 +subsection {* Implementation of mappings *}
    4.14 +
    4.15 +definition Mapping :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) mapping" where
    4.16 +  "Mapping t = Mapping.Mapping (lookup t)"
    4.17 +
    4.18 +code_datatype Mapping
    4.19 +
    4.20 +lemma lookup_Mapping [simp, code]:
    4.21 +  "Mapping.lookup (Mapping t) = lookup t"
    4.22 +  by (simp add: Mapping_def)
    4.23 +
    4.24 +lemma empty_Mapping [code]:
    4.25 +  "Mapping.empty = Mapping empty"
    4.26 +  by (rule mapping_eqI) simp
    4.27 +
    4.28 +lemma is_empty_Mapping [code]:
    4.29 +  "Mapping.is_empty (Mapping t) \<longleftrightarrow> is_empty t"
    4.30 +  by (simp add: rbt_eq_iff Mapping.is_empty_empty Mapping_def)
    4.31 +
    4.32 +lemma insert_Mapping [code]:
    4.33 +  "Mapping.update k v (Mapping t) = Mapping (insert k v t)"
    4.34 +  by (rule mapping_eqI) simp
    4.35 +
    4.36 +lemma delete_Mapping [code]:
    4.37 +  "Mapping.delete k (Mapping t) = Mapping (delete k t)"
    4.38 +  by (rule mapping_eqI) simp
    4.39 +
    4.40 +lemma map_entry_Mapping [code]:
    4.41 +  "Mapping.map_entry k f (Mapping t) = Mapping (map_entry k f t)"
    4.42 +  by (rule mapping_eqI) simp
    4.43 +
    4.44 +lemma keys_Mapping [code]:
    4.45 +  "Mapping.keys (Mapping t) = set (keys t)"
    4.46 +  by (simp add: RBT.keys_def Mapping_def Mapping.keys_def lookup_def lookup_keys)
    4.47 +
    4.48 +lemma ordered_keys_Mapping [code]:
    4.49 +  "Mapping.ordered_keys (Mapping t) = keys t"
    4.50 +  by (rule sorted_distinct_set_unique) (simp_all add: ordered_keys_def keys_Mapping)
    4.51 +
    4.52 +lemma Mapping_size_card_keys: (*FIXME*)
    4.53 +  "Mapping.size m = card (Mapping.keys m)"
    4.54 +  by (simp add: Mapping.size_def Mapping.keys_def)
    4.55 +
    4.56 +lemma size_Mapping [code]:
    4.57 +  "Mapping.size (Mapping t) = length (keys t)"
    4.58 +  by (simp add: Mapping_size_card_keys keys_Mapping distinct_card)
    4.59 +
    4.60 +lemma tabulate_Mapping [code]:
    4.61 +  "Mapping.tabulate ks f = Mapping (bulkload (List.map (\<lambda>k. (k, f k)) ks))"
    4.62 +  by (rule mapping_eqI) (simp add: map_of_map_restrict)
    4.63 +
    4.64 +lemma bulkload_Mapping [code]:
    4.65 +  "Mapping.bulkload vs = Mapping (bulkload (List.map (\<lambda>n. (n, vs ! n)) [0..<length vs]))"
    4.66 +  by (rule mapping_eqI) (simp add: map_of_map_restrict fun_eq_iff)
    4.67 +
    4.68 +lemma equal_Mapping [code]:
    4.69 +  "HOL.equal (Mapping t1) (Mapping t2) \<longleftrightarrow> entries t1 = entries t2"
    4.70 +  by (simp add: equal Mapping_def entries_lookup)
    4.71 +
    4.72 +lemma [code nbe]:
    4.73 +  "HOL.equal (x :: (_, _) mapping) x \<longleftrightarrow> True"
    4.74 +  by (fact equal_refl)
    4.75 +
    4.76 +
    4.77 +hide_const (open) impl_of lookup empty insert delete
    4.78 +  entries keys bulkload map_entry map fold
    4.79 +(*>*)
    4.80 +
    4.81 +text {* 
    4.82 +  This theory defines abstract red-black trees as an efficient
    4.83 +  representation of finite maps, backed by the implementation
    4.84 +  in @{theory RBT_Impl}.
    4.85 +*}
    4.86 +
    4.87 +subsection {* Data type and invariant *}
    4.88 +
    4.89 +text {*
    4.90 +  The type @{typ "('k, 'v) RBT_Impl.rbt"} denotes red-black trees with
    4.91 +  keys of type @{typ "'k"} and values of type @{typ "'v"}. To function
    4.92 +  properly, the key type musorted belong to the @{text "linorder"}
    4.93 +  class.
    4.94 +
    4.95 +  A value @{term t} of this type is a valid red-black tree if it
    4.96 +  satisfies the invariant @{text "is_rbt t"}.  The abstract type @{typ
    4.97 +  "('k, 'v) rbt"} always obeys this invariant, and for this reason you
    4.98 +  should only use this in our application.  Going back to @{typ "('k,
    4.99 +  'v) RBT_Impl.rbt"} may be necessary in proofs if not yet proven
   4.100 +  properties about the operations must be established.
   4.101 +
   4.102 +  The interpretation function @{const "RBT.lookup"} returns the partial
   4.103 +  map represented by a red-black tree:
   4.104 +  @{term_type[display] "RBT.lookup"}
   4.105 +
   4.106 +  This function should be used for reasoning about the semantics of the RBT
   4.107 +  operations. Furthermore, it implements the lookup functionality for
   4.108 +  the data structure: It is executable and the lookup is performed in
   4.109 +  $O(\log n)$.  
   4.110 +*}
   4.111 +
   4.112 +subsection {* Operations *}
   4.113 +
   4.114 +text {*
   4.115 +  Currently, the following operations are supported:
   4.116 +
   4.117 +  @{term_type [display] "RBT.empty"}
   4.118 +  Returns the empty tree. $O(1)$
   4.119 +
   4.120 +  @{term_type [display] "RBT.insert"}
   4.121 +  Updates the map at a given position. $O(\log n)$
   4.122 +
   4.123 +  @{term_type [display] "RBT.delete"}
   4.124 +  Deletes a map entry at a given position. $O(\log n)$
   4.125 +
   4.126 +  @{term_type [display] "RBT.entries"}
   4.127 +  Return a corresponding key-value list for a tree.
   4.128 +
   4.129 +  @{term_type [display] "RBT.bulkload"}
   4.130 +  Builds a tree from a key-value list.
   4.131 +
   4.132 +  @{term_type [display] "RBT.map_entry"}
   4.133 +  Maps a single entry in a tree.
   4.134 +
   4.135 +  @{term_type [display] "RBT.map"}
   4.136 +  Maps all values in a tree. $O(n)$
   4.137 +
   4.138 +  @{term_type [display] "RBT.fold"}
   4.139 +  Folds over all entries in a tree. $O(n)$
   4.140 +*}
   4.141 +
   4.142 +
   4.143 +subsection {* Invariant preservation *}
   4.144 +
   4.145 +text {*
   4.146 +  \noindent
   4.147 +  @{thm Empty_is_rbt}\hfill(@{text "Empty_is_rbt"})
   4.148 +
   4.149 +  \noindent
   4.150 +  @{thm insert_is_rbt}\hfill(@{text "insert_is_rbt"})
   4.151 +
   4.152 +  \noindent
   4.153 +  @{thm delete_is_rbt}\hfill(@{text "delete_is_rbt"})
   4.154 +
   4.155 +  \noindent
   4.156 +  @{thm bulkload_is_rbt}\hfill(@{text "bulkload_is_rbt"})
   4.157 +
   4.158 +  \noindent
   4.159 +  @{thm map_entry_is_rbt}\hfill(@{text "map_entry_is_rbt"})
   4.160 +
   4.161 +  \noindent
   4.162 +  @{thm map_is_rbt}\hfill(@{text "map_is_rbt"})
   4.163 +
   4.164 +  \noindent
   4.165 +  @{thm union_is_rbt}\hfill(@{text "union_is_rbt"})
   4.166 +*}
   4.167 +
   4.168 +
   4.169 +subsection {* Map Semantics *}
   4.170 +
   4.171 +text {*
   4.172 +  \noindent
   4.173 +  \underline{@{text "lookup_empty"}}
   4.174 +  @{thm [display] lookup_empty}
   4.175 +  \vspace{1ex}
   4.176 +
   4.177 +  \noindent
   4.178 +  \underline{@{text "lookup_insert"}}
   4.179 +  @{thm [display] lookup_insert}
   4.180 +  \vspace{1ex}
   4.181 +
   4.182 +  \noindent
   4.183 +  \underline{@{text "lookup_delete"}}
   4.184 +  @{thm [display] lookup_delete}
   4.185 +  \vspace{1ex}
   4.186 +
   4.187 +  \noindent
   4.188 +  \underline{@{text "lookup_bulkload"}}
   4.189 +  @{thm [display] lookup_bulkload}
   4.190 +  \vspace{1ex}
   4.191 +
   4.192 +  \noindent
   4.193 +  \underline{@{text "lookup_map"}}
   4.194 +  @{thm [display] lookup_map}
   4.195 +  \vspace{1ex}
   4.196 +*}
   4.197 +
   4.198 +end
   4.199 \ No newline at end of file