author | wenzelm |
Sat, 12 Jan 2013 14:53:56 +0100 | |
changeset 50843 | 1465521b92a1 |
parent 49929 | 70300f1b6835 |
child 51161 | 6ed12ae3b3e1 |
permissions | -rw-r--r-- |
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset
|
1 |
(* Title: HOL/Library/RBT_Mapping.thy |
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset
|
2 |
Author: Florian Haftmann and Ondrej Kuncar |
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset
|
3 |
*) |
43124 | 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 |
||
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset
|
14 |
lift_definition Mapping :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) mapping" is lookup . |
43124 | 15 |
|
16 |
code_datatype Mapping |
|
17 |
||
18 |
lemma lookup_Mapping [simp, code]: |
|
19 |
"Mapping.lookup (Mapping t) = lookup t" |
|
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset
|
20 |
by (transfer fixing: t) rule |
43124 | 21 |
|
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset
|
22 |
lemma empty_Mapping [code]: "Mapping.empty = Mapping empty" |
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset
|
23 |
proof - |
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset
|
24 |
note RBT.empty.transfer[transfer_rule del] |
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset
|
25 |
show ?thesis by transfer simp |
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset
|
26 |
qed |
43124 | 27 |
|
28 |
lemma is_empty_Mapping [code]: |
|
29 |
"Mapping.is_empty (Mapping t) \<longleftrightarrow> is_empty t" |
|
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset
|
30 |
unfolding is_empty_def by (transfer fixing: t) simp |
43124 | 31 |
|
32 |
lemma insert_Mapping [code]: |
|
33 |
"Mapping.update k v (Mapping t) = Mapping (insert k v t)" |
|
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset
|
34 |
by (transfer fixing: t) simp |
43124 | 35 |
|
36 |
lemma delete_Mapping [code]: |
|
37 |
"Mapping.delete k (Mapping t) = Mapping (delete k t)" |
|
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset
|
38 |
by (transfer fixing: t) simp |
43124 | 39 |
|
40 |
lemma map_entry_Mapping [code]: |
|
41 |
"Mapping.map_entry k f (Mapping t) = Mapping (map_entry k f t)" |
|
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset
|
42 |
apply (transfer fixing: t) by (case_tac "lookup t k") auto |
43124 | 43 |
|
44 |
lemma keys_Mapping [code]: |
|
45 |
"Mapping.keys (Mapping t) = set (keys t)" |
|
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset
|
46 |
by (transfer fixing: t) (simp add: lookup_keys) |
43124 | 47 |
|
48 |
lemma ordered_keys_Mapping [code]: |
|
49 |
"Mapping.ordered_keys (Mapping t) = keys t" |
|
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset
|
50 |
unfolding ordered_keys_def |
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset
|
51 |
by (transfer fixing: t) (auto simp add: lookup_keys intro: sorted_distinct_set_unique) |
43124 | 52 |
|
53 |
lemma Mapping_size_card_keys: (*FIXME*) |
|
54 |
"Mapping.size m = card (Mapping.keys m)" |
|
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset
|
55 |
unfolding size_def by transfer simp |
43124 | 56 |
|
57 |
lemma size_Mapping [code]: |
|
58 |
"Mapping.size (Mapping t) = length (keys t)" |
|
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset
|
59 |
unfolding size_def |
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset
|
60 |
by (transfer fixing: t) (simp add: lookup_keys distinct_card) |
43124 | 61 |
|
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset
|
62 |
context |
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset
|
63 |
notes RBT.bulkload.transfer[transfer_rule del] |
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset
|
64 |
begin |
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset
|
65 |
lemma tabulate_Mapping [code]: |
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset
|
66 |
"Mapping.tabulate ks f = Mapping (bulkload (List.map (\<lambda>k. (k, f k)) ks))" |
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset
|
67 |
by transfer (simp add: map_of_map_restrict) |
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset
|
68 |
|
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset
|
69 |
lemma bulkload_Mapping [code]: |
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset
|
70 |
"Mapping.bulkload vs = Mapping (bulkload (List.map (\<lambda>n. (n, vs ! n)) [0..<length vs]))" |
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset
|
71 |
by transfer (simp add: map_of_map_restrict fun_eq_iff) |
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset
|
72 |
end |
43124 | 73 |
|
74 |
lemma equal_Mapping [code]: |
|
75 |
"HOL.equal (Mapping t1) (Mapping t2) \<longleftrightarrow> entries t1 = entries t2" |
|
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
47450
diff
changeset
|
76 |
by (transfer fixing: t1 t2) (simp add: entries_lookup) |
43124 | 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 |
|
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
43124
diff
changeset
|
156 |
@{thm rbt_insert_is_rbt}\hfill(@{text "rbt_insert_is_rbt"}) |
43124 | 157 |
|
158 |
\noindent |
|
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
43124
diff
changeset
|
159 |
@{thm rbt_delete_is_rbt}\hfill(@{text "delete_is_rbt"}) |
43124 | 160 |
|
161 |
\noindent |
|
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
43124
diff
changeset
|
162 |
@{thm rbt_bulkload_is_rbt}\hfill(@{text "bulkload_is_rbt"}) |
43124 | 163 |
|
164 |
\noindent |
|
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
43124
diff
changeset
|
165 |
@{thm rbt_map_entry_is_rbt}\hfill(@{text "map_entry_is_rbt"}) |
43124 | 166 |
|
167 |
\noindent |
|
168 |
@{thm map_is_rbt}\hfill(@{text "map_is_rbt"}) |
|
169 |
||
170 |
\noindent |
|
47450
2ada2be850cb
move RBT implementation into type class contexts
Andreas Lochbihler
parents:
43124
diff
changeset
|
171 |
@{thm rbt_union_is_rbt}\hfill(@{text "union_is_rbt"}) |
43124 | 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 |