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