43124
|
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 |