src/HOL/Library/RBT.thy
author bulwahn
Fri Apr 08 16:31:14 2011 +0200 (2011-04-08)
changeset 42316 12635bb655fd
parent 40612 7ae5b89d8913
child 43124 fdb7e1d5f762
permissions -rw-r--r--
deactivating other compilations in quickcheck_exhaustive momentarily that only interesting for my benchmarks and experiments
     1 (* Author: Florian Haftmann, TU Muenchen *)
     2 
     3 header {* Abstract type of Red-Black Trees *}
     4 
     5 (*<*)
     6 theory RBT
     7 imports Main RBT_Impl Mapping
     8 begin
     9 
    10 subsection {* Type definition *}
    11 
    12 typedef (open) ('a, 'b) rbt = "{t :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt. is_rbt t}"
    13   morphisms impl_of RBT
    14 proof -
    15   have "RBT_Impl.Empty \<in> ?rbt" by simp
    16   then show ?thesis ..
    17 qed
    18 
    19 lemma rbt_eq_iff:
    20   "t1 = t2 \<longleftrightarrow> impl_of t1 = impl_of t2"
    21   by (simp add: impl_of_inject)
    22 
    23 lemma rbt_eqI:
    24   "impl_of t1 = impl_of t2 \<Longrightarrow> t1 = t2"
    25   by (simp add: rbt_eq_iff)
    26 
    27 lemma is_rbt_impl_of [simp, intro]:
    28   "is_rbt (impl_of t)"
    29   using impl_of [of t] by simp
    30 
    31 lemma RBT_impl_of [simp, code abstype]:
    32   "RBT (impl_of t) = t"
    33   by (simp add: impl_of_inverse)
    34 
    35 
    36 subsection {* Primitive operations *}
    37 
    38 definition lookup :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" where
    39   [code]: "lookup t = RBT_Impl.lookup (impl_of t)"
    40 
    41 definition empty :: "('a\<Colon>linorder, 'b) rbt" where
    42   "empty = RBT RBT_Impl.Empty"
    43 
    44 lemma impl_of_empty [code abstract]:
    45   "impl_of empty = RBT_Impl.Empty"
    46   by (simp add: empty_def RBT_inverse)
    47 
    48 definition insert :: "'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
    49   "insert k v t = RBT (RBT_Impl.insert k v (impl_of t))"
    50 
    51 lemma impl_of_insert [code abstract]:
    52   "impl_of (insert k v t) = RBT_Impl.insert k v (impl_of t)"
    53   by (simp add: insert_def RBT_inverse)
    54 
    55 definition delete :: "'a\<Colon>linorder \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
    56   "delete k t = RBT (RBT_Impl.delete k (impl_of t))"
    57 
    58 lemma impl_of_delete [code abstract]:
    59   "impl_of (delete k t) = RBT_Impl.delete k (impl_of t)"
    60   by (simp add: delete_def RBT_inverse)
    61 
    62 definition entries :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) list" where
    63   [code]: "entries t = RBT_Impl.entries (impl_of t)"
    64 
    65 definition keys :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a list" where
    66   [code]: "keys t = RBT_Impl.keys (impl_of t)"
    67 
    68 definition bulkload :: "('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) rbt" where
    69   "bulkload xs = RBT (RBT_Impl.bulkload xs)"
    70 
    71 lemma impl_of_bulkload [code abstract]:
    72   "impl_of (bulkload xs) = RBT_Impl.bulkload xs"
    73   by (simp add: bulkload_def RBT_inverse)
    74 
    75 definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
    76   "map_entry k f t = RBT (RBT_Impl.map_entry k f (impl_of t))"
    77 
    78 lemma impl_of_map_entry [code abstract]:
    79   "impl_of (map_entry k f t) = RBT_Impl.map_entry k f (impl_of t)"
    80   by (simp add: map_entry_def RBT_inverse)
    81 
    82 definition map :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
    83   "map f t = RBT (RBT_Impl.map f (impl_of t))"
    84 
    85 lemma impl_of_map [code abstract]:
    86   "impl_of (map f t) = RBT_Impl.map f (impl_of t)"
    87   by (simp add: map_def RBT_inverse)
    88 
    89 definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" where
    90   [code]: "fold f t = RBT_Impl.fold f (impl_of t)"
    91 
    92 
    93 subsection {* Derived operations *}
    94 
    95 definition is_empty :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> bool" where
    96   [code]: "is_empty t = (case impl_of t of RBT_Impl.Empty \<Rightarrow> True | _ \<Rightarrow> False)"
    97 
    98 
    99 subsection {* Abstract lookup properties *}
   100 
   101 lemma lookup_RBT:
   102   "is_rbt t \<Longrightarrow> lookup (RBT t) = RBT_Impl.lookup t"
   103   by (simp add: lookup_def RBT_inverse)
   104 
   105 lemma lookup_impl_of:
   106   "RBT_Impl.lookup (impl_of t) = lookup t"
   107   by (simp add: lookup_def)
   108 
   109 lemma entries_impl_of:
   110   "RBT_Impl.entries (impl_of t) = entries t"
   111   by (simp add: entries_def)
   112 
   113 lemma keys_impl_of:
   114   "RBT_Impl.keys (impl_of t) = keys t"
   115   by (simp add: keys_def)
   116 
   117 lemma lookup_empty [simp]:
   118   "lookup empty = Map.empty"
   119   by (simp add: empty_def lookup_RBT fun_eq_iff)
   120 
   121 lemma lookup_insert [simp]:
   122   "lookup (insert k v t) = (lookup t)(k \<mapsto> v)"
   123   by (simp add: insert_def lookup_RBT lookup_insert lookup_impl_of)
   124 
   125 lemma lookup_delete [simp]:
   126   "lookup (delete k t) = (lookup t)(k := None)"
   127   by (simp add: delete_def lookup_RBT RBT_Impl.lookup_delete lookup_impl_of restrict_complement_singleton_eq)
   128 
   129 lemma map_of_entries [simp]:
   130   "map_of (entries t) = lookup t"
   131   by (simp add: entries_def map_of_entries lookup_impl_of)
   132 
   133 lemma entries_lookup:
   134   "entries t1 = entries t2 \<longleftrightarrow> lookup t1 = lookup t2"
   135   by (simp add: entries_def lookup_def entries_lookup)
   136 
   137 lemma lookup_bulkload [simp]:
   138   "lookup (bulkload xs) = map_of xs"
   139   by (simp add: bulkload_def lookup_RBT RBT_Impl.lookup_bulkload)
   140 
   141 lemma lookup_map_entry [simp]:
   142   "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))"
   143   by (simp add: map_entry_def lookup_RBT RBT_Impl.lookup_map_entry lookup_impl_of)
   144 
   145 lemma lookup_map [simp]:
   146   "lookup (map f t) k = Option.map (f k) (lookup t k)"
   147   by (simp add: map_def lookup_RBT RBT_Impl.lookup_map lookup_impl_of)
   148 
   149 lemma fold_fold:
   150   "fold f t = More_List.fold (prod_case f) (entries t)"
   151   by (simp add: fold_def fun_eq_iff RBT_Impl.fold_def entries_impl_of)
   152 
   153 lemma is_empty_empty [simp]:
   154   "is_empty t \<longleftrightarrow> t = empty"
   155   by (simp add: rbt_eq_iff is_empty_def impl_of_empty split: rbt.split)
   156 
   157 lemma RBT_lookup_empty [simp]: (*FIXME*)
   158   "RBT_Impl.lookup t = Map.empty \<longleftrightarrow> t = RBT_Impl.Empty"
   159   by (cases t) (auto simp add: fun_eq_iff)
   160 
   161 lemma lookup_empty_empty [simp]:
   162   "lookup t = Map.empty \<longleftrightarrow> t = empty"
   163   by (cases t) (simp add: empty_def lookup_def RBT_inject RBT_inverse)
   164 
   165 lemma sorted_keys [iff]:
   166   "sorted (keys t)"
   167   by (simp add: keys_def RBT_Impl.keys_def sorted_entries)
   168 
   169 lemma distinct_keys [iff]:
   170   "distinct (keys t)"
   171   by (simp add: keys_def RBT_Impl.keys_def distinct_entries)
   172 
   173 
   174 subsection {* Implementation of mappings *}
   175 
   176 definition Mapping :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) mapping" where
   177   "Mapping t = Mapping.Mapping (lookup t)"
   178 
   179 code_datatype Mapping
   180 
   181 lemma lookup_Mapping [simp, code]:
   182   "Mapping.lookup (Mapping t) = lookup t"
   183   by (simp add: Mapping_def)
   184 
   185 lemma empty_Mapping [code]:
   186   "Mapping.empty = Mapping empty"
   187   by (rule mapping_eqI) simp
   188 
   189 lemma is_empty_Mapping [code]:
   190   "Mapping.is_empty (Mapping t) \<longleftrightarrow> is_empty t"
   191   by (simp add: rbt_eq_iff Mapping.is_empty_empty Mapping_def)
   192 
   193 lemma insert_Mapping [code]:
   194   "Mapping.update k v (Mapping t) = Mapping (insert k v t)"
   195   by (rule mapping_eqI) simp
   196 
   197 lemma delete_Mapping [code]:
   198   "Mapping.delete k (Mapping t) = Mapping (delete k t)"
   199   by (rule mapping_eqI) simp
   200 
   201 lemma map_entry_Mapping [code]:
   202   "Mapping.map_entry k f (Mapping t) = Mapping (map_entry k f t)"
   203   by (rule mapping_eqI) simp
   204 
   205 lemma keys_Mapping [code]:
   206   "Mapping.keys (Mapping t) = set (keys t)"
   207   by (simp add: keys_def Mapping_def Mapping.keys_def lookup_def lookup_keys)
   208 
   209 lemma ordered_keys_Mapping [code]:
   210   "Mapping.ordered_keys (Mapping t) = keys t"
   211   by (rule sorted_distinct_set_unique) (simp_all add: ordered_keys_def keys_Mapping)
   212 
   213 lemma Mapping_size_card_keys: (*FIXME*)
   214   "Mapping.size m = card (Mapping.keys m)"
   215   by (simp add: Mapping.size_def Mapping.keys_def)
   216 
   217 lemma size_Mapping [code]:
   218   "Mapping.size (Mapping t) = length (keys t)"
   219   by (simp add: Mapping_size_card_keys keys_Mapping distinct_card)
   220 
   221 lemma tabulate_Mapping [code]:
   222   "Mapping.tabulate ks f = Mapping (bulkload (List.map (\<lambda>k. (k, f k)) ks))"
   223   by (rule mapping_eqI) (simp add: map_of_map_restrict)
   224 
   225 lemma bulkload_Mapping [code]:
   226   "Mapping.bulkload vs = Mapping (bulkload (List.map (\<lambda>n. (n, vs ! n)) [0..<length vs]))"
   227   by (rule mapping_eqI) (simp add: map_of_map_restrict fun_eq_iff)
   228 
   229 lemma equal_Mapping [code]:
   230   "HOL.equal (Mapping t1) (Mapping t2) \<longleftrightarrow> entries t1 = entries t2"
   231   by (simp add: equal Mapping_def entries_lookup)
   232 
   233 lemma [code nbe]:
   234   "HOL.equal (x :: (_, _) mapping) x \<longleftrightarrow> True"
   235   by (fact equal_refl)
   236 
   237 
   238 hide_const (open) impl_of lookup empty insert delete
   239   entries keys bulkload map_entry map fold
   240 (*>*)
   241 
   242 text {* 
   243   This theory defines abstract red-black trees as an efficient
   244   representation of finite maps, backed by the implementation
   245   in @{theory RBT_Impl}.
   246 *}
   247 
   248 subsection {* Data type and invariant *}
   249 
   250 text {*
   251   The type @{typ "('k, 'v) RBT_Impl.rbt"} denotes red-black trees with
   252   keys of type @{typ "'k"} and values of type @{typ "'v"}. To function
   253   properly, the key type musorted belong to the @{text "linorder"}
   254   class.
   255 
   256   A value @{term t} of this type is a valid red-black tree if it
   257   satisfies the invariant @{text "is_rbt t"}.  The abstract type @{typ
   258   "('k, 'v) rbt"} always obeys this invariant, and for this reason you
   259   should only use this in our application.  Going back to @{typ "('k,
   260   'v) RBT_Impl.rbt"} may be necessary in proofs if not yet proven
   261   properties about the operations must be established.
   262 
   263   The interpretation function @{const "RBT.lookup"} returns the partial
   264   map represented by a red-black tree:
   265   @{term_type[display] "RBT.lookup"}
   266 
   267   This function should be used for reasoning about the semantics of the RBT
   268   operations. Furthermore, it implements the lookup functionality for
   269   the data structure: It is executable and the lookup is performed in
   270   $O(\log n)$.  
   271 *}
   272 
   273 subsection {* Operations *}
   274 
   275 text {*
   276   Currently, the following operations are supported:
   277 
   278   @{term_type [display] "RBT.empty"}
   279   Returns the empty tree. $O(1)$
   280 
   281   @{term_type [display] "RBT.insert"}
   282   Updates the map at a given position. $O(\log n)$
   283 
   284   @{term_type [display] "RBT.delete"}
   285   Deletes a map entry at a given position. $O(\log n)$
   286 
   287   @{term_type [display] "RBT.entries"}
   288   Return a corresponding key-value list for a tree.
   289 
   290   @{term_type [display] "RBT.bulkload"}
   291   Builds a tree from a key-value list.
   292 
   293   @{term_type [display] "RBT.map_entry"}
   294   Maps a single entry in a tree.
   295 
   296   @{term_type [display] "RBT.map"}
   297   Maps all values in a tree. $O(n)$
   298 
   299   @{term_type [display] "RBT.fold"}
   300   Folds over all entries in a tree. $O(n)$
   301 *}
   302 
   303 
   304 subsection {* Invariant preservation *}
   305 
   306 text {*
   307   \noindent
   308   @{thm Empty_is_rbt}\hfill(@{text "Empty_is_rbt"})
   309 
   310   \noindent
   311   @{thm insert_is_rbt}\hfill(@{text "insert_is_rbt"})
   312 
   313   \noindent
   314   @{thm delete_is_rbt}\hfill(@{text "delete_is_rbt"})
   315 
   316   \noindent
   317   @{thm bulkload_is_rbt}\hfill(@{text "bulkload_is_rbt"})
   318 
   319   \noindent
   320   @{thm map_entry_is_rbt}\hfill(@{text "map_entry_is_rbt"})
   321 
   322   \noindent
   323   @{thm map_is_rbt}\hfill(@{text "map_is_rbt"})
   324 
   325   \noindent
   326   @{thm union_is_rbt}\hfill(@{text "union_is_rbt"})
   327 *}
   328 
   329 
   330 subsection {* Map Semantics *}
   331 
   332 text {*
   333   \noindent
   334   \underline{@{text "lookup_empty"}}
   335   @{thm [display] lookup_empty}
   336   \vspace{1ex}
   337 
   338   \noindent
   339   \underline{@{text "lookup_insert"}}
   340   @{thm [display] lookup_insert}
   341   \vspace{1ex}
   342 
   343   \noindent
   344   \underline{@{text "lookup_delete"}}
   345   @{thm [display] lookup_delete}
   346   \vspace{1ex}
   347 
   348   \noindent
   349   \underline{@{text "lookup_bulkload"}}
   350   @{thm [display] lookup_bulkload}
   351   \vspace{1ex}
   352 
   353   \noindent
   354   \underline{@{text "lookup_map"}}
   355   @{thm [display] lookup_map}
   356   \vspace{1ex}
   357 *}
   358 
   359 end