src/HOL/Library/RBT_Mapping.thy
author hoelzl
Tue Jul 19 14:37:49 2011 +0200 (2011-07-19)
changeset 43922 c6f35921056e
parent 43124 fdb7e1d5f762
child 47450 2ada2be850cb
permissions -rw-r--r--
add nat => enat coercion
     1 (* Author: Florian Haftmann, TU Muenchen *)
     2 
     3 header {* Implementation of mappings with Red-Black Trees *}
     4 
     5 (*<*)
     6 theory RBT_Mapping
     7 imports RBT Mapping
     8 begin
     9 
    10 subsection {* Implementation of mappings *}
    11 
    12 definition Mapping :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) mapping" where
    13   "Mapping t = Mapping.Mapping (lookup t)"
    14 
    15 code_datatype Mapping
    16 
    17 lemma lookup_Mapping [simp, code]:
    18   "Mapping.lookup (Mapping t) = lookup t"
    19   by (simp add: Mapping_def)
    20 
    21 lemma empty_Mapping [code]:
    22   "Mapping.empty = Mapping empty"
    23   by (rule mapping_eqI) simp
    24 
    25 lemma is_empty_Mapping [code]:
    26   "Mapping.is_empty (Mapping t) \<longleftrightarrow> is_empty t"
    27   by (simp add: rbt_eq_iff Mapping.is_empty_empty Mapping_def)
    28 
    29 lemma insert_Mapping [code]:
    30   "Mapping.update k v (Mapping t) = Mapping (insert k v t)"
    31   by (rule mapping_eqI) simp
    32 
    33 lemma delete_Mapping [code]:
    34   "Mapping.delete k (Mapping t) = Mapping (delete k t)"
    35   by (rule mapping_eqI) simp
    36 
    37 lemma map_entry_Mapping [code]:
    38   "Mapping.map_entry k f (Mapping t) = Mapping (map_entry k f t)"
    39   by (rule mapping_eqI) simp
    40 
    41 lemma keys_Mapping [code]:
    42   "Mapping.keys (Mapping t) = set (keys t)"
    43   by (simp add: RBT.keys_def Mapping_def Mapping.keys_def lookup_def lookup_keys)
    44 
    45 lemma ordered_keys_Mapping [code]:
    46   "Mapping.ordered_keys (Mapping t) = keys t"
    47   by (rule sorted_distinct_set_unique) (simp_all add: ordered_keys_def keys_Mapping)
    48 
    49 lemma Mapping_size_card_keys: (*FIXME*)
    50   "Mapping.size m = card (Mapping.keys m)"
    51   by (simp add: Mapping.size_def Mapping.keys_def)
    52 
    53 lemma size_Mapping [code]:
    54   "Mapping.size (Mapping t) = length (keys t)"
    55   by (simp add: Mapping_size_card_keys keys_Mapping distinct_card)
    56 
    57 lemma tabulate_Mapping [code]:
    58   "Mapping.tabulate ks f = Mapping (bulkload (List.map (\<lambda>k. (k, f k)) ks))"
    59   by (rule mapping_eqI) (simp add: map_of_map_restrict)
    60 
    61 lemma bulkload_Mapping [code]:
    62   "Mapping.bulkload vs = Mapping (bulkload (List.map (\<lambda>n. (n, vs ! n)) [0..<length vs]))"
    63   by (rule mapping_eqI) (simp add: map_of_map_restrict fun_eq_iff)
    64 
    65 lemma equal_Mapping [code]:
    66   "HOL.equal (Mapping t1) (Mapping t2) \<longleftrightarrow> entries t1 = entries t2"
    67   by (simp add: equal Mapping_def entries_lookup)
    68 
    69 lemma [code nbe]:
    70   "HOL.equal (x :: (_, _) mapping) x \<longleftrightarrow> True"
    71   by (fact equal_refl)
    72 
    73 
    74 hide_const (open) impl_of lookup empty insert delete
    75   entries keys bulkload map_entry map fold
    76 (*>*)
    77 
    78 text {* 
    79   This theory defines abstract red-black trees as an efficient
    80   representation of finite maps, backed by the implementation
    81   in @{theory RBT_Impl}.
    82 *}
    83 
    84 subsection {* Data type and invariant *}
    85 
    86 text {*
    87   The type @{typ "('k, 'v) RBT_Impl.rbt"} denotes red-black trees with
    88   keys of type @{typ "'k"} and values of type @{typ "'v"}. To function
    89   properly, the key type musorted belong to the @{text "linorder"}
    90   class.
    91 
    92   A value @{term t} of this type is a valid red-black tree if it
    93   satisfies the invariant @{text "is_rbt t"}.  The abstract type @{typ
    94   "('k, 'v) rbt"} always obeys this invariant, and for this reason you
    95   should only use this in our application.  Going back to @{typ "('k,
    96   'v) RBT_Impl.rbt"} may be necessary in proofs if not yet proven
    97   properties about the operations must be established.
    98 
    99   The interpretation function @{const "RBT.lookup"} returns the partial
   100   map represented by a red-black tree:
   101   @{term_type[display] "RBT.lookup"}
   102 
   103   This function should be used for reasoning about the semantics of the RBT
   104   operations. Furthermore, it implements the lookup functionality for
   105   the data structure: It is executable and the lookup is performed in
   106   $O(\log n)$.  
   107 *}
   108 
   109 subsection {* Operations *}
   110 
   111 text {*
   112   Currently, the following operations are supported:
   113 
   114   @{term_type [display] "RBT.empty"}
   115   Returns the empty tree. $O(1)$
   116 
   117   @{term_type [display] "RBT.insert"}
   118   Updates the map at a given position. $O(\log n)$
   119 
   120   @{term_type [display] "RBT.delete"}
   121   Deletes a map entry at a given position. $O(\log n)$
   122 
   123   @{term_type [display] "RBT.entries"}
   124   Return a corresponding key-value list for a tree.
   125 
   126   @{term_type [display] "RBT.bulkload"}
   127   Builds a tree from a key-value list.
   128 
   129   @{term_type [display] "RBT.map_entry"}
   130   Maps a single entry in a tree.
   131 
   132   @{term_type [display] "RBT.map"}
   133   Maps all values in a tree. $O(n)$
   134 
   135   @{term_type [display] "RBT.fold"}
   136   Folds over all entries in a tree. $O(n)$
   137 *}
   138 
   139 
   140 subsection {* Invariant preservation *}
   141 
   142 text {*
   143   \noindent
   144   @{thm Empty_is_rbt}\hfill(@{text "Empty_is_rbt"})
   145 
   146   \noindent
   147   @{thm insert_is_rbt}\hfill(@{text "insert_is_rbt"})
   148 
   149   \noindent
   150   @{thm delete_is_rbt}\hfill(@{text "delete_is_rbt"})
   151 
   152   \noindent
   153   @{thm bulkload_is_rbt}\hfill(@{text "bulkload_is_rbt"})
   154 
   155   \noindent
   156   @{thm map_entry_is_rbt}\hfill(@{text "map_entry_is_rbt"})
   157 
   158   \noindent
   159   @{thm map_is_rbt}\hfill(@{text "map_is_rbt"})
   160 
   161   \noindent
   162   @{thm union_is_rbt}\hfill(@{text "union_is_rbt"})
   163 *}
   164 
   165 
   166 subsection {* Map Semantics *}
   167 
   168 text {*
   169   \noindent
   170   \underline{@{text "lookup_empty"}}
   171   @{thm [display] lookup_empty}
   172   \vspace{1ex}
   173 
   174   \noindent
   175   \underline{@{text "lookup_insert"}}
   176   @{thm [display] lookup_insert}
   177   \vspace{1ex}
   178 
   179   \noindent
   180   \underline{@{text "lookup_delete"}}
   181   @{thm [display] lookup_delete}
   182   \vspace{1ex}
   183 
   184   \noindent
   185   \underline{@{text "lookup_bulkload"}}
   186   @{thm [display] lookup_bulkload}
   187   \vspace{1ex}
   188 
   189   \noindent
   190   \underline{@{text "lookup_map"}}
   191   @{thm [display] lookup_map}
   192   \vspace{1ex}
   193 *}
   194 
   195 end