|
1 (* Title: RBT_Impl.thy |
|
2 Author: Markus Reiter, TU Muenchen |
|
3 Author: Alexander Krauss, TU Muenchen |
|
4 *) |
|
5 |
|
6 header {* Implementation of Red-Black Trees *} |
|
7 |
|
8 theory RBT_Impl |
|
9 imports Main |
|
10 begin |
|
11 |
|
12 text {* |
|
13 For applications, you should use theory @{text RBT} which defines |
|
14 an abstract type of red-black tree obeying the invariant. |
|
15 *} |
|
16 |
|
17 subsection {* Datatype of RB trees *} |
|
18 |
|
19 datatype color = R | B |
|
20 datatype ('a, 'b) rbt = Empty | Branch color "('a, 'b) rbt" 'a 'b "('a, 'b) rbt" |
|
21 |
|
22 lemma rbt_cases: |
|
23 obtains (Empty) "t = Empty" |
|
24 | (Red) l k v r where "t = Branch R l k v r" |
|
25 | (Black) l k v r where "t = Branch B l k v r" |
|
26 proof (cases t) |
|
27 case Empty with that show thesis by blast |
|
28 next |
|
29 case (Branch c) with that show thesis by (cases c) blast+ |
|
30 qed |
|
31 |
|
32 subsection {* Tree properties *} |
|
33 |
|
34 subsubsection {* Content of a tree *} |
|
35 |
|
36 primrec entries :: "('a, 'b) rbt \<Rightarrow> ('a \<times> 'b) list" |
|
37 where |
|
38 "entries Empty = []" |
|
39 | "entries (Branch _ l k v r) = entries l @ (k,v) # entries r" |
|
40 |
|
41 abbreviation (input) entry_in_tree :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool" |
|
42 where |
|
43 "entry_in_tree k v t \<equiv> (k, v) \<in> set (entries t)" |
|
44 |
|
45 definition keys :: "('a, 'b) rbt \<Rightarrow> 'a list" where |
|
46 "keys t = map fst (entries t)" |
|
47 |
|
48 lemma keys_simps [simp, code]: |
|
49 "keys Empty = []" |
|
50 "keys (Branch c l k v r) = keys l @ k # keys r" |
|
51 by (simp_all add: keys_def) |
|
52 |
|
53 lemma entry_in_tree_keys: |
|
54 assumes "(k, v) \<in> set (entries t)" |
|
55 shows "k \<in> set (keys t)" |
|
56 proof - |
|
57 from assms have "fst (k, v) \<in> fst ` set (entries t)" by (rule imageI) |
|
58 then show ?thesis by (simp add: keys_def) |
|
59 qed |
|
60 |
|
61 lemma keys_entries: |
|
62 "k \<in> set (keys t) \<longleftrightarrow> (\<exists>v. (k, v) \<in> set (entries t))" |
|
63 by (auto intro: entry_in_tree_keys) (auto simp add: keys_def) |
|
64 |
|
65 |
|
66 subsubsection {* Search tree properties *} |
|
67 |
|
68 definition tree_less :: "'a\<Colon>order \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool" |
|
69 where |
|
70 tree_less_prop: "tree_less k t \<longleftrightarrow> (\<forall>x\<in>set (keys t). x < k)" |
|
71 |
|
72 abbreviation tree_less_symbol (infix "|\<guillemotleft>" 50) |
|
73 where "t |\<guillemotleft> x \<equiv> tree_less x t" |
|
74 |
|
75 definition tree_greater :: "'a\<Colon>order \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool" (infix "\<guillemotleft>|" 50) |
|
76 where |
|
77 tree_greater_prop: "tree_greater k t = (\<forall>x\<in>set (keys t). k < x)" |
|
78 |
|
79 lemma tree_less_simps [simp]: |
|
80 "tree_less k Empty = True" |
|
81 "tree_less k (Branch c lt kt v rt) \<longleftrightarrow> kt < k \<and> tree_less k lt \<and> tree_less k rt" |
|
82 by (auto simp add: tree_less_prop) |
|
83 |
|
84 lemma tree_greater_simps [simp]: |
|
85 "tree_greater k Empty = True" |
|
86 "tree_greater k (Branch c lt kt v rt) \<longleftrightarrow> k < kt \<and> tree_greater k lt \<and> tree_greater k rt" |
|
87 by (auto simp add: tree_greater_prop) |
|
88 |
|
89 lemmas tree_ord_props = tree_less_prop tree_greater_prop |
|
90 |
|
91 lemmas tree_greater_nit = tree_greater_prop entry_in_tree_keys |
|
92 lemmas tree_less_nit = tree_less_prop entry_in_tree_keys |
|
93 |
|
94 lemma tree_less_eq_trans: "l |\<guillemotleft> u \<Longrightarrow> u \<le> v \<Longrightarrow> l |\<guillemotleft> v" |
|
95 and tree_less_trans: "t |\<guillemotleft> x \<Longrightarrow> x < y \<Longrightarrow> t |\<guillemotleft> y" |
|
96 and tree_greater_eq_trans: "u \<le> v \<Longrightarrow> v \<guillemotleft>| r \<Longrightarrow> u \<guillemotleft>| r" |
|
97 and tree_greater_trans: "x < y \<Longrightarrow> y \<guillemotleft>| t \<Longrightarrow> x \<guillemotleft>| t" |
|
98 by (auto simp: tree_ord_props) |
|
99 |
|
100 primrec sorted :: "('a::linorder, 'b) rbt \<Rightarrow> bool" |
|
101 where |
|
102 "sorted Empty = True" |
|
103 | "sorted (Branch c l k v r) = (l |\<guillemotleft> k \<and> k \<guillemotleft>| r \<and> sorted l \<and> sorted r)" |
|
104 |
|
105 lemma sorted_entries: |
|
106 "sorted t \<Longrightarrow> List.sorted (List.map fst (entries t))" |
|
107 by (induct t) |
|
108 (force simp: sorted_append sorted_Cons tree_ord_props |
|
109 dest!: entry_in_tree_keys)+ |
|
110 |
|
111 lemma distinct_entries: |
|
112 "sorted t \<Longrightarrow> distinct (List.map fst (entries t))" |
|
113 by (induct t) |
|
114 (force simp: sorted_append sorted_Cons tree_ord_props |
|
115 dest!: entry_in_tree_keys)+ |
|
116 |
|
117 |
|
118 subsubsection {* Tree lookup *} |
|
119 |
|
120 primrec lookup :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" |
|
121 where |
|
122 "lookup Empty k = None" |
|
123 | "lookup (Branch _ l x y r) k = (if k < x then lookup l k else if x < k then lookup r k else Some y)" |
|
124 |
|
125 lemma lookup_keys: "sorted t \<Longrightarrow> dom (lookup t) = set (keys t)" |
|
126 by (induct t) (auto simp: dom_def tree_greater_prop tree_less_prop) |
|
127 |
|
128 lemma dom_lookup_Branch: |
|
129 "sorted (Branch c t1 k v t2) \<Longrightarrow> |
|
130 dom (lookup (Branch c t1 k v t2)) |
|
131 = Set.insert k (dom (lookup t1) \<union> dom (lookup t2))" |
|
132 proof - |
|
133 assume "sorted (Branch c t1 k v t2)" |
|
134 moreover from this have "sorted t1" "sorted t2" by simp_all |
|
135 ultimately show ?thesis by (simp add: lookup_keys) |
|
136 qed |
|
137 |
|
138 lemma finite_dom_lookup [simp, intro!]: "finite (dom (lookup t))" |
|
139 proof (induct t) |
|
140 case Empty then show ?case by simp |
|
141 next |
|
142 case (Branch color t1 a b t2) |
|
143 let ?A = "Set.insert a (dom (lookup t1) \<union> dom (lookup t2))" |
|
144 have "dom (lookup (Branch color t1 a b t2)) \<subseteq> ?A" by (auto split: split_if_asm) |
|
145 moreover from Branch have "finite (insert a (dom (lookup t1) \<union> dom (lookup t2)))" by simp |
|
146 ultimately show ?case by (rule finite_subset) |
|
147 qed |
|
148 |
|
149 lemma lookup_tree_less[simp]: "t |\<guillemotleft> k \<Longrightarrow> lookup t k = None" |
|
150 by (induct t) auto |
|
151 |
|
152 lemma lookup_tree_greater[simp]: "k \<guillemotleft>| t \<Longrightarrow> lookup t k = None" |
|
153 by (induct t) auto |
|
154 |
|
155 lemma lookup_Empty: "lookup Empty = empty" |
|
156 by (rule ext) simp |
|
157 |
|
158 lemma map_of_entries: |
|
159 "sorted t \<Longrightarrow> map_of (entries t) = lookup t" |
|
160 proof (induct t) |
|
161 case Empty thus ?case by (simp add: lookup_Empty) |
|
162 next |
|
163 case (Branch c t1 k v t2) |
|
164 have "lookup (Branch c t1 k v t2) = lookup t2 ++ [k\<mapsto>v] ++ lookup t1" |
|
165 proof (rule ext) |
|
166 fix x |
|
167 from Branch have SORTED: "sorted (Branch c t1 k v t2)" by simp |
|
168 let ?thesis = "lookup (Branch c t1 k v t2) x = (lookup t2 ++ [k \<mapsto> v] ++ lookup t1) x" |
|
169 |
|
170 have DOM_T1: "!!k'. k'\<in>dom (lookup t1) \<Longrightarrow> k>k'" |
|
171 proof - |
|
172 fix k' |
|
173 from SORTED have "t1 |\<guillemotleft> k" by simp |
|
174 with tree_less_prop have "\<forall>k'\<in>set (keys t1). k>k'" by auto |
|
175 moreover assume "k'\<in>dom (lookup t1)" |
|
176 ultimately show "k>k'" using lookup_keys SORTED by auto |
|
177 qed |
|
178 |
|
179 have DOM_T2: "!!k'. k'\<in>dom (lookup t2) \<Longrightarrow> k<k'" |
|
180 proof - |
|
181 fix k' |
|
182 from SORTED have "k \<guillemotleft>| t2" by simp |
|
183 with tree_greater_prop have "\<forall>k'\<in>set (keys t2). k<k'" by auto |
|
184 moreover assume "k'\<in>dom (lookup t2)" |
|
185 ultimately show "k<k'" using lookup_keys SORTED by auto |
|
186 qed |
|
187 |
|
188 { |
|
189 assume C: "x<k" |
|
190 hence "lookup (Branch c t1 k v t2) x = lookup t1 x" by simp |
|
191 moreover from C have "x\<notin>dom [k\<mapsto>v]" by simp |
|
192 moreover have "x\<notin>dom (lookup t2)" proof |
|
193 assume "x\<in>dom (lookup t2)" |
|
194 with DOM_T2 have "k<x" by blast |
|
195 with C show False by simp |
|
196 qed |
|
197 ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps) |
|
198 } moreover { |
|
199 assume [simp]: "x=k" |
|
200 hence "lookup (Branch c t1 k v t2) x = [k \<mapsto> v] x" by simp |
|
201 moreover have "x\<notin>dom (lookup t1)" proof |
|
202 assume "x\<in>dom (lookup t1)" |
|
203 with DOM_T1 have "k>x" by blast |
|
204 thus False by simp |
|
205 qed |
|
206 ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps) |
|
207 } moreover { |
|
208 assume C: "x>k" |
|
209 hence "lookup (Branch c t1 k v t2) x = lookup t2 x" by (simp add: less_not_sym[of k x]) |
|
210 moreover from C have "x\<notin>dom [k\<mapsto>v]" by simp |
|
211 moreover have "x\<notin>dom (lookup t1)" proof |
|
212 assume "x\<in>dom (lookup t1)" |
|
213 with DOM_T1 have "k>x" by simp |
|
214 with C show False by simp |
|
215 qed |
|
216 ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps) |
|
217 } ultimately show ?thesis using less_linear by blast |
|
218 qed |
|
219 also from Branch have "lookup t2 ++ [k \<mapsto> v] ++ lookup t1 = map_of (entries (Branch c t1 k v t2))" by simp |
|
220 finally show ?case by simp |
|
221 qed |
|
222 |
|
223 lemma lookup_in_tree: "sorted t \<Longrightarrow> lookup t k = Some v \<longleftrightarrow> (k, v) \<in> set (entries t)" |
|
224 by (simp add: map_of_entries [symmetric] distinct_entries) |
|
225 |
|
226 lemma set_entries_inject: |
|
227 assumes sorted: "sorted t1" "sorted t2" |
|
228 shows "set (entries t1) = set (entries t2) \<longleftrightarrow> entries t1 = entries t2" |
|
229 proof - |
|
230 from sorted have "distinct (map fst (entries t1))" |
|
231 "distinct (map fst (entries t2))" |
|
232 by (auto intro: distinct_entries) |
|
233 with sorted show ?thesis |
|
234 by (auto intro: map_sorted_distinct_set_unique sorted_entries simp add: distinct_map) |
|
235 qed |
|
236 |
|
237 lemma entries_eqI: |
|
238 assumes sorted: "sorted t1" "sorted t2" |
|
239 assumes lookup: "lookup t1 = lookup t2" |
|
240 shows "entries t1 = entries t2" |
|
241 proof - |
|
242 from sorted lookup have "map_of (entries t1) = map_of (entries t2)" |
|
243 by (simp add: map_of_entries) |
|
244 with sorted have "set (entries t1) = set (entries t2)" |
|
245 by (simp add: map_of_inject_set distinct_entries) |
|
246 with sorted show ?thesis by (simp add: set_entries_inject) |
|
247 qed |
|
248 |
|
249 lemma entries_lookup: |
|
250 assumes "sorted t1" "sorted t2" |
|
251 shows "entries t1 = entries t2 \<longleftrightarrow> lookup t1 = lookup t2" |
|
252 using assms by (auto intro: entries_eqI simp add: map_of_entries [symmetric]) |
|
253 |
|
254 lemma lookup_from_in_tree: |
|
255 assumes "sorted t1" "sorted t2" |
|
256 and "\<And>v. (k\<Colon>'a\<Colon>linorder, v) \<in> set (entries t1) \<longleftrightarrow> (k, v) \<in> set (entries t2)" |
|
257 shows "lookup t1 k = lookup t2 k" |
|
258 proof - |
|
259 from assms have "k \<in> dom (lookup t1) \<longleftrightarrow> k \<in> dom (lookup t2)" |
|
260 by (simp add: keys_entries lookup_keys) |
|
261 with assms show ?thesis by (auto simp add: lookup_in_tree [symmetric]) |
|
262 qed |
|
263 |
|
264 |
|
265 subsubsection {* Red-black properties *} |
|
266 |
|
267 primrec color_of :: "('a, 'b) rbt \<Rightarrow> color" |
|
268 where |
|
269 "color_of Empty = B" |
|
270 | "color_of (Branch c _ _ _ _) = c" |
|
271 |
|
272 primrec bheight :: "('a,'b) rbt \<Rightarrow> nat" |
|
273 where |
|
274 "bheight Empty = 0" |
|
275 | "bheight (Branch c lt k v rt) = (if c = B then Suc (bheight lt) else bheight lt)" |
|
276 |
|
277 primrec inv1 :: "('a, 'b) rbt \<Rightarrow> bool" |
|
278 where |
|
279 "inv1 Empty = True" |
|
280 | "inv1 (Branch c lt k v rt) \<longleftrightarrow> inv1 lt \<and> inv1 rt \<and> (c = B \<or> color_of lt = B \<and> color_of rt = B)" |
|
281 |
|
282 primrec inv1l :: "('a, 'b) rbt \<Rightarrow> bool" -- {* Weaker version *} |
|
283 where |
|
284 "inv1l Empty = True" |
|
285 | "inv1l (Branch c l k v r) = (inv1 l \<and> inv1 r)" |
|
286 lemma [simp]: "inv1 t \<Longrightarrow> inv1l t" by (cases t) simp+ |
|
287 |
|
288 primrec inv2 :: "('a, 'b) rbt \<Rightarrow> bool" |
|
289 where |
|
290 "inv2 Empty = True" |
|
291 | "inv2 (Branch c lt k v rt) = (inv2 lt \<and> inv2 rt \<and> bheight lt = bheight rt)" |
|
292 |
|
293 definition is_rbt :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> bool" where |
|
294 "is_rbt t \<longleftrightarrow> inv1 t \<and> inv2 t \<and> color_of t = B \<and> sorted t" |
|
295 |
|
296 lemma is_rbt_sorted [simp]: |
|
297 "is_rbt t \<Longrightarrow> sorted t" by (simp add: is_rbt_def) |
|
298 |
|
299 theorem Empty_is_rbt [simp]: |
|
300 "is_rbt Empty" by (simp add: is_rbt_def) |
|
301 |
|
302 |
|
303 subsection {* Insertion *} |
|
304 |
|
305 fun (* slow, due to massive case splitting *) |
|
306 balance :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" |
|
307 where |
|
308 "balance (Branch R a w x b) s t (Branch R c y z d) = Branch R (Branch B a w x b) s t (Branch B c y z d)" | |
|
309 "balance (Branch R (Branch R a w x b) s t c) y z d = Branch R (Branch B a w x b) s t (Branch B c y z d)" | |
|
310 "balance (Branch R a w x (Branch R b s t c)) y z d = Branch R (Branch B a w x b) s t (Branch B c y z d)" | |
|
311 "balance a w x (Branch R b s t (Branch R c y z d)) = Branch R (Branch B a w x b) s t (Branch B c y z d)" | |
|
312 "balance a w x (Branch R (Branch R b s t c) y z d) = Branch R (Branch B a w x b) s t (Branch B c y z d)" | |
|
313 "balance a s t b = Branch B a s t b" |
|
314 |
|
315 lemma balance_inv1: "\<lbrakk>inv1l l; inv1l r\<rbrakk> \<Longrightarrow> inv1 (balance l k v r)" |
|
316 by (induct l k v r rule: balance.induct) auto |
|
317 |
|
318 lemma balance_bheight: "bheight l = bheight r \<Longrightarrow> bheight (balance l k v r) = Suc (bheight l)" |
|
319 by (induct l k v r rule: balance.induct) auto |
|
320 |
|
321 lemma balance_inv2: |
|
322 assumes "inv2 l" "inv2 r" "bheight l = bheight r" |
|
323 shows "inv2 (balance l k v r)" |
|
324 using assms |
|
325 by (induct l k v r rule: balance.induct) auto |
|
326 |
|
327 lemma balance_tree_greater[simp]: "(v \<guillemotleft>| balance a k x b) = (v \<guillemotleft>| a \<and> v \<guillemotleft>| b \<and> v < k)" |
|
328 by (induct a k x b rule: balance.induct) auto |
|
329 |
|
330 lemma balance_tree_less[simp]: "(balance a k x b |\<guillemotleft> v) = (a |\<guillemotleft> v \<and> b |\<guillemotleft> v \<and> k < v)" |
|
331 by (induct a k x b rule: balance.induct) auto |
|
332 |
|
333 lemma balance_sorted: |
|
334 fixes k :: "'a::linorder" |
|
335 assumes "sorted l" "sorted r" "l |\<guillemotleft> k" "k \<guillemotleft>| r" |
|
336 shows "sorted (balance l k v r)" |
|
337 using assms proof (induct l k v r rule: balance.induct) |
|
338 case ("2_2" a x w b y t c z s va vb vd vc) |
|
339 hence "y < z \<and> z \<guillemotleft>| Branch B va vb vd vc" |
|
340 by (auto simp add: tree_ord_props) |
|
341 hence "tree_greater y (Branch B va vb vd vc)" by (blast dest: tree_greater_trans) |
|
342 with "2_2" show ?case by simp |
|
343 next |
|
344 case ("3_2" va vb vd vc x w b y s c z) |
|
345 from "3_2" have "x < y \<and> tree_less x (Branch B va vb vd vc)" |
|
346 by simp |
|
347 hence "tree_less y (Branch B va vb vd vc)" by (blast dest: tree_less_trans) |
|
348 with "3_2" show ?case by simp |
|
349 next |
|
350 case ("3_3" x w b y s c z t va vb vd vc) |
|
351 from "3_3" have "y < z \<and> tree_greater z (Branch B va vb vd vc)" by simp |
|
352 hence "tree_greater y (Branch B va vb vd vc)" by (blast dest: tree_greater_trans) |
|
353 with "3_3" show ?case by simp |
|
354 next |
|
355 case ("3_4" vd ve vg vf x w b y s c z t va vb vii vc) |
|
356 hence "x < y \<and> tree_less x (Branch B vd ve vg vf)" by simp |
|
357 hence 1: "tree_less y (Branch B vd ve vg vf)" by (blast dest: tree_less_trans) |
|
358 from "3_4" have "y < z \<and> tree_greater z (Branch B va vb vii vc)" by simp |
|
359 hence "tree_greater y (Branch B va vb vii vc)" by (blast dest: tree_greater_trans) |
|
360 with 1 "3_4" show ?case by simp |
|
361 next |
|
362 case ("4_2" va vb vd vc x w b y s c z t dd) |
|
363 hence "x < y \<and> tree_less x (Branch B va vb vd vc)" by simp |
|
364 hence "tree_less y (Branch B va vb vd vc)" by (blast dest: tree_less_trans) |
|
365 with "4_2" show ?case by simp |
|
366 next |
|
367 case ("5_2" x w b y s c z t va vb vd vc) |
|
368 hence "y < z \<and> tree_greater z (Branch B va vb vd vc)" by simp |
|
369 hence "tree_greater y (Branch B va vb vd vc)" by (blast dest: tree_greater_trans) |
|
370 with "5_2" show ?case by simp |
|
371 next |
|
372 case ("5_3" va vb vd vc x w b y s c z t) |
|
373 hence "x < y \<and> tree_less x (Branch B va vb vd vc)" by simp |
|
374 hence "tree_less y (Branch B va vb vd vc)" by (blast dest: tree_less_trans) |
|
375 with "5_3" show ?case by simp |
|
376 next |
|
377 case ("5_4" va vb vg vc x w b y s c z t vd ve vii vf) |
|
378 hence "x < y \<and> tree_less x (Branch B va vb vg vc)" by simp |
|
379 hence 1: "tree_less y (Branch B va vb vg vc)" by (blast dest: tree_less_trans) |
|
380 from "5_4" have "y < z \<and> tree_greater z (Branch B vd ve vii vf)" by simp |
|
381 hence "tree_greater y (Branch B vd ve vii vf)" by (blast dest: tree_greater_trans) |
|
382 with 1 "5_4" show ?case by simp |
|
383 qed simp+ |
|
384 |
|
385 lemma entries_balance [simp]: |
|
386 "entries (balance l k v r) = entries l @ (k, v) # entries r" |
|
387 by (induct l k v r rule: balance.induct) auto |
|
388 |
|
389 lemma keys_balance [simp]: |
|
390 "keys (balance l k v r) = keys l @ k # keys r" |
|
391 by (simp add: keys_def) |
|
392 |
|
393 lemma balance_in_tree: |
|
394 "entry_in_tree k x (balance l v y r) \<longleftrightarrow> entry_in_tree k x l \<or> k = v \<and> x = y \<or> entry_in_tree k x r" |
|
395 by (auto simp add: keys_def) |
|
396 |
|
397 lemma lookup_balance[simp]: |
|
398 fixes k :: "'a::linorder" |
|
399 assumes "sorted l" "sorted r" "l |\<guillemotleft> k" "k \<guillemotleft>| r" |
|
400 shows "lookup (balance l k v r) x = lookup (Branch B l k v r) x" |
|
401 by (rule lookup_from_in_tree) (auto simp:assms balance_in_tree balance_sorted) |
|
402 |
|
403 primrec paint :: "color \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" |
|
404 where |
|
405 "paint c Empty = Empty" |
|
406 | "paint c (Branch _ l k v r) = Branch c l k v r" |
|
407 |
|
408 lemma paint_inv1l[simp]: "inv1l t \<Longrightarrow> inv1l (paint c t)" by (cases t) auto |
|
409 lemma paint_inv1[simp]: "inv1l t \<Longrightarrow> inv1 (paint B t)" by (cases t) auto |
|
410 lemma paint_inv2[simp]: "inv2 t \<Longrightarrow> inv2 (paint c t)" by (cases t) auto |
|
411 lemma paint_color_of[simp]: "color_of (paint B t) = B" by (cases t) auto |
|
412 lemma paint_sorted[simp]: "sorted t \<Longrightarrow> sorted (paint c t)" by (cases t) auto |
|
413 lemma paint_in_tree[simp]: "entry_in_tree k x (paint c t) = entry_in_tree k x t" by (cases t) auto |
|
414 lemma paint_lookup[simp]: "lookup (paint c t) = lookup t" by (rule ext) (cases t, auto) |
|
415 lemma paint_tree_greater[simp]: "(v \<guillemotleft>| paint c t) = (v \<guillemotleft>| t)" by (cases t) auto |
|
416 lemma paint_tree_less[simp]: "(paint c t |\<guillemotleft> v) = (t |\<guillemotleft> v)" by (cases t) auto |
|
417 |
|
418 fun |
|
419 ins :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" |
|
420 where |
|
421 "ins f k v Empty = Branch R Empty k v Empty" | |
|
422 "ins f k v (Branch B l x y r) = (if k < x then balance (ins f k v l) x y r |
|
423 else if k > x then balance l x y (ins f k v r) |
|
424 else Branch B l x (f k y v) r)" | |
|
425 "ins f k v (Branch R l x y r) = (if k < x then Branch R (ins f k v l) x y r |
|
426 else if k > x then Branch R l x y (ins f k v r) |
|
427 else Branch R l x (f k y v) r)" |
|
428 |
|
429 lemma ins_inv1_inv2: |
|
430 assumes "inv1 t" "inv2 t" |
|
431 shows "inv2 (ins f k x t)" "bheight (ins f k x t) = bheight t" |
|
432 "color_of t = B \<Longrightarrow> inv1 (ins f k x t)" "inv1l (ins f k x t)" |
|
433 using assms |
|
434 by (induct f k x t rule: ins.induct) (auto simp: balance_inv1 balance_inv2 balance_bheight) |
|
435 |
|
436 lemma ins_tree_greater[simp]: "(v \<guillemotleft>| ins f k x t) = (v \<guillemotleft>| t \<and> k > v)" |
|
437 by (induct f k x t rule: ins.induct) auto |
|
438 lemma ins_tree_less[simp]: "(ins f k x t |\<guillemotleft> v) = (t |\<guillemotleft> v \<and> k < v)" |
|
439 by (induct f k x t rule: ins.induct) auto |
|
440 lemma ins_sorted[simp]: "sorted t \<Longrightarrow> sorted (ins f k x t)" |
|
441 by (induct f k x t rule: ins.induct) (auto simp: balance_sorted) |
|
442 |
|
443 lemma keys_ins: "set (keys (ins f k v t)) = { k } \<union> set (keys t)" |
|
444 by (induct f k v t rule: ins.induct) auto |
|
445 |
|
446 lemma lookup_ins: |
|
447 fixes k :: "'a::linorder" |
|
448 assumes "sorted t" |
|
449 shows "lookup (ins f k v t) x = ((lookup t)(k |-> case lookup t k of None \<Rightarrow> v |
|
450 | Some w \<Rightarrow> f k w v)) x" |
|
451 using assms by (induct f k v t rule: ins.induct) auto |
|
452 |
|
453 definition |
|
454 insert_with_key :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" |
|
455 where |
|
456 "insert_with_key f k v t = paint B (ins f k v t)" |
|
457 |
|
458 lemma insertwk_sorted: "sorted t \<Longrightarrow> sorted (insert_with_key f k x t)" |
|
459 by (auto simp: insert_with_key_def) |
|
460 |
|
461 theorem insertwk_is_rbt: |
|
462 assumes inv: "is_rbt t" |
|
463 shows "is_rbt (insert_with_key f k x t)" |
|
464 using assms |
|
465 unfolding insert_with_key_def is_rbt_def |
|
466 by (auto simp: ins_inv1_inv2) |
|
467 |
|
468 lemma lookup_insertwk: |
|
469 assumes "sorted t" |
|
470 shows "lookup (insert_with_key f k v t) x = ((lookup t)(k |-> case lookup t k of None \<Rightarrow> v |
|
471 | Some w \<Rightarrow> f k w v)) x" |
|
472 unfolding insert_with_key_def using assms |
|
473 by (simp add:lookup_ins) |
|
474 |
|
475 definition |
|
476 insertw_def: "insert_with f = insert_with_key (\<lambda>_. f)" |
|
477 |
|
478 lemma insertw_sorted: "sorted t \<Longrightarrow> sorted (insert_with f k v t)" by (simp add: insertwk_sorted insertw_def) |
|
479 theorem insertw_is_rbt: "is_rbt t \<Longrightarrow> is_rbt (insert_with f k v t)" by (simp add: insertwk_is_rbt insertw_def) |
|
480 |
|
481 lemma lookup_insertw: |
|
482 assumes "is_rbt t" |
|
483 shows "lookup (insert_with f k v t) = (lookup t)(k \<mapsto> (if k:dom (lookup t) then f (the (lookup t k)) v else v))" |
|
484 using assms |
|
485 unfolding insertw_def |
|
486 by (rule_tac ext) (cases "lookup t k", auto simp:lookup_insertwk dom_def) |
|
487 |
|
488 definition insert :: "'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where |
|
489 "insert = insert_with_key (\<lambda>_ _ nv. nv)" |
|
490 |
|
491 lemma insert_sorted: "sorted t \<Longrightarrow> sorted (insert k v t)" by (simp add: insertwk_sorted insert_def) |
|
492 theorem insert_is_rbt [simp]: "is_rbt t \<Longrightarrow> is_rbt (insert k v t)" by (simp add: insertwk_is_rbt insert_def) |
|
493 |
|
494 lemma lookup_insert: |
|
495 assumes "is_rbt t" |
|
496 shows "lookup (insert k v t) = (lookup t)(k\<mapsto>v)" |
|
497 unfolding insert_def |
|
498 using assms |
|
499 by (rule_tac ext) (simp add: lookup_insertwk split:option.split) |
|
500 |
|
501 |
|
502 subsection {* Deletion *} |
|
503 |
|
504 lemma bheight_paintR'[simp]: "color_of t = B \<Longrightarrow> bheight (paint R t) = bheight t - 1" |
|
505 by (cases t rule: rbt_cases) auto |
|
506 |
|
507 fun |
|
508 balance_left :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" |
|
509 where |
|
510 "balance_left (Branch R a k x b) s y c = Branch R (Branch B a k x b) s y c" | |
|
511 "balance_left bl k x (Branch B a s y b) = balance bl k x (Branch R a s y b)" | |
|
512 "balance_left bl k x (Branch R (Branch B a s y b) t z c) = Branch R (Branch B bl k x a) s y (balance b t z (paint R c))" | |
|
513 "balance_left t k x s = Empty" |
|
514 |
|
515 lemma balance_left_inv2_with_inv1: |
|
516 assumes "inv2 lt" "inv2 rt" "bheight lt + 1 = bheight rt" "inv1 rt" |
|
517 shows "bheight (balance_left lt k v rt) = bheight lt + 1" |
|
518 and "inv2 (balance_left lt k v rt)" |
|
519 using assms |
|
520 by (induct lt k v rt rule: balance_left.induct) (auto simp: balance_inv2 balance_bheight) |
|
521 |
|
522 lemma balance_left_inv2_app: |
|
523 assumes "inv2 lt" "inv2 rt" "bheight lt + 1 = bheight rt" "color_of rt = B" |
|
524 shows "inv2 (balance_left lt k v rt)" |
|
525 "bheight (balance_left lt k v rt) = bheight rt" |
|
526 using assms |
|
527 by (induct lt k v rt rule: balance_left.induct) (auto simp add: balance_inv2 balance_bheight)+ |
|
528 |
|
529 lemma balance_left_inv1: "\<lbrakk>inv1l a; inv1 b; color_of b = B\<rbrakk> \<Longrightarrow> inv1 (balance_left a k x b)" |
|
530 by (induct a k x b rule: balance_left.induct) (simp add: balance_inv1)+ |
|
531 |
|
532 lemma balance_left_inv1l: "\<lbrakk> inv1l lt; inv1 rt \<rbrakk> \<Longrightarrow> inv1l (balance_left lt k x rt)" |
|
533 by (induct lt k x rt rule: balance_left.induct) (auto simp: balance_inv1) |
|
534 |
|
535 lemma balance_left_sorted: "\<lbrakk> sorted l; sorted r; tree_less k l; tree_greater k r \<rbrakk> \<Longrightarrow> sorted (balance_left l k v r)" |
|
536 apply (induct l k v r rule: balance_left.induct) |
|
537 apply (auto simp: balance_sorted) |
|
538 apply (unfold tree_greater_prop tree_less_prop) |
|
539 by force+ |
|
540 |
|
541 lemma balance_left_tree_greater: |
|
542 fixes k :: "'a::order" |
|
543 assumes "k \<guillemotleft>| a" "k \<guillemotleft>| b" "k < x" |
|
544 shows "k \<guillemotleft>| balance_left a x t b" |
|
545 using assms |
|
546 by (induct a x t b rule: balance_left.induct) auto |
|
547 |
|
548 lemma balance_left_tree_less: |
|
549 fixes k :: "'a::order" |
|
550 assumes "a |\<guillemotleft> k" "b |\<guillemotleft> k" "x < k" |
|
551 shows "balance_left a x t b |\<guillemotleft> k" |
|
552 using assms |
|
553 by (induct a x t b rule: balance_left.induct) auto |
|
554 |
|
555 lemma balance_left_in_tree: |
|
556 assumes "inv1l l" "inv1 r" "bheight l + 1 = bheight r" |
|
557 shows "entry_in_tree k v (balance_left l a b r) = (entry_in_tree k v l \<or> k = a \<and> v = b \<or> entry_in_tree k v r)" |
|
558 using assms |
|
559 by (induct l k v r rule: balance_left.induct) (auto simp: balance_in_tree) |
|
560 |
|
561 fun |
|
562 balance_right :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" |
|
563 where |
|
564 "balance_right a k x (Branch R b s y c) = Branch R a k x (Branch B b s y c)" | |
|
565 "balance_right (Branch B a k x b) s y bl = balance (Branch R a k x b) s y bl" | |
|
566 "balance_right (Branch R a k x (Branch B b s y c)) t z bl = Branch R (balance (paint R a) k x b) s y (Branch B c t z bl)" | |
|
567 "balance_right t k x s = Empty" |
|
568 |
|
569 lemma balance_right_inv2_with_inv1: |
|
570 assumes "inv2 lt" "inv2 rt" "bheight lt = bheight rt + 1" "inv1 lt" |
|
571 shows "inv2 (balance_right lt k v rt) \<and> bheight (balance_right lt k v rt) = bheight lt" |
|
572 using assms |
|
573 by (induct lt k v rt rule: balance_right.induct) (auto simp: balance_inv2 balance_bheight) |
|
574 |
|
575 lemma balance_right_inv1: "\<lbrakk>inv1 a; inv1l b; color_of a = B\<rbrakk> \<Longrightarrow> inv1 (balance_right a k x b)" |
|
576 by (induct a k x b rule: balance_right.induct) (simp add: balance_inv1)+ |
|
577 |
|
578 lemma balance_right_inv1l: "\<lbrakk> inv1 lt; inv1l rt \<rbrakk> \<Longrightarrow>inv1l (balance_right lt k x rt)" |
|
579 by (induct lt k x rt rule: balance_right.induct) (auto simp: balance_inv1) |
|
580 |
|
581 lemma balance_right_sorted: "\<lbrakk> sorted l; sorted r; tree_less k l; tree_greater k r \<rbrakk> \<Longrightarrow> sorted (balance_right l k v r)" |
|
582 apply (induct l k v r rule: balance_right.induct) |
|
583 apply (auto simp:balance_sorted) |
|
584 apply (unfold tree_less_prop tree_greater_prop) |
|
585 by force+ |
|
586 |
|
587 lemma balance_right_tree_greater: |
|
588 fixes k :: "'a::order" |
|
589 assumes "k \<guillemotleft>| a" "k \<guillemotleft>| b" "k < x" |
|
590 shows "k \<guillemotleft>| balance_right a x t b" |
|
591 using assms by (induct a x t b rule: balance_right.induct) auto |
|
592 |
|
593 lemma balance_right_tree_less: |
|
594 fixes k :: "'a::order" |
|
595 assumes "a |\<guillemotleft> k" "b |\<guillemotleft> k" "x < k" |
|
596 shows "balance_right a x t b |\<guillemotleft> k" |
|
597 using assms by (induct a x t b rule: balance_right.induct) auto |
|
598 |
|
599 lemma balance_right_in_tree: |
|
600 assumes "inv1 l" "inv1l r" "bheight l = bheight r + 1" "inv2 l" "inv2 r" |
|
601 shows "entry_in_tree x y (balance_right l k v r) = (entry_in_tree x y l \<or> x = k \<and> y = v \<or> entry_in_tree x y r)" |
|
602 using assms by (induct l k v r rule: balance_right.induct) (auto simp: balance_in_tree) |
|
603 |
|
604 fun |
|
605 combine :: "('a,'b) rbt \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" |
|
606 where |
|
607 "combine Empty x = x" |
|
608 | "combine x Empty = x" |
|
609 | "combine (Branch R a k x b) (Branch R c s y d) = (case (combine b c) of |
|
610 Branch R b2 t z c2 \<Rightarrow> (Branch R (Branch R a k x b2) t z (Branch R c2 s y d)) | |
|
611 bc \<Rightarrow> Branch R a k x (Branch R bc s y d))" |
|
612 | "combine (Branch B a k x b) (Branch B c s y d) = (case (combine b c) of |
|
613 Branch R b2 t z c2 \<Rightarrow> Branch R (Branch B a k x b2) t z (Branch B c2 s y d) | |
|
614 bc \<Rightarrow> balance_left a k x (Branch B bc s y d))" |
|
615 | "combine a (Branch R b k x c) = Branch R (combine a b) k x c" |
|
616 | "combine (Branch R a k x b) c = Branch R a k x (combine b c)" |
|
617 |
|
618 lemma combine_inv2: |
|
619 assumes "inv2 lt" "inv2 rt" "bheight lt = bheight rt" |
|
620 shows "bheight (combine lt rt) = bheight lt" "inv2 (combine lt rt)" |
|
621 using assms |
|
622 by (induct lt rt rule: combine.induct) |
|
623 (auto simp: balance_left_inv2_app split: rbt.splits color.splits) |
|
624 |
|
625 lemma combine_inv1: |
|
626 assumes "inv1 lt" "inv1 rt" |
|
627 shows "color_of lt = B \<Longrightarrow> color_of rt = B \<Longrightarrow> inv1 (combine lt rt)" |
|
628 "inv1l (combine lt rt)" |
|
629 using assms |
|
630 by (induct lt rt rule: combine.induct) |
|
631 (auto simp: balance_left_inv1 split: rbt.splits color.splits) |
|
632 |
|
633 lemma combine_tree_greater[simp]: |
|
634 fixes k :: "'a::linorder" |
|
635 assumes "k \<guillemotleft>| l" "k \<guillemotleft>| r" |
|
636 shows "k \<guillemotleft>| combine l r" |
|
637 using assms |
|
638 by (induct l r rule: combine.induct) |
|
639 (auto simp: balance_left_tree_greater split:rbt.splits color.splits) |
|
640 |
|
641 lemma combine_tree_less[simp]: |
|
642 fixes k :: "'a::linorder" |
|
643 assumes "l |\<guillemotleft> k" "r |\<guillemotleft> k" |
|
644 shows "combine l r |\<guillemotleft> k" |
|
645 using assms |
|
646 by (induct l r rule: combine.induct) |
|
647 (auto simp: balance_left_tree_less split:rbt.splits color.splits) |
|
648 |
|
649 lemma combine_sorted: |
|
650 fixes k :: "'a::linorder" |
|
651 assumes "sorted l" "sorted r" "l |\<guillemotleft> k" "k \<guillemotleft>| r" |
|
652 shows "sorted (combine l r)" |
|
653 using assms proof (induct l r rule: combine.induct) |
|
654 case (3 a x v b c y w d) |
|
655 hence ineqs: "a |\<guillemotleft> x" "x \<guillemotleft>| b" "b |\<guillemotleft> k" "k \<guillemotleft>| c" "c |\<guillemotleft> y" "y \<guillemotleft>| d" |
|
656 by auto |
|
657 with 3 |
|
658 show ?case |
|
659 by (cases "combine b c" rule: rbt_cases) |
|
660 (auto, (metis combine_tree_greater combine_tree_less ineqs ineqs tree_less_simps(2) tree_greater_simps(2) tree_greater_trans tree_less_trans)+) |
|
661 next |
|
662 case (4 a x v b c y w d) |
|
663 hence "x < k \<and> tree_greater k c" by simp |
|
664 hence "tree_greater x c" by (blast dest: tree_greater_trans) |
|
665 with 4 have 2: "tree_greater x (combine b c)" by (simp add: combine_tree_greater) |
|
666 from 4 have "k < y \<and> tree_less k b" by simp |
|
667 hence "tree_less y b" by (blast dest: tree_less_trans) |
|
668 with 4 have 3: "tree_less y (combine b c)" by (simp add: combine_tree_less) |
|
669 show ?case |
|
670 proof (cases "combine b c" rule: rbt_cases) |
|
671 case Empty |
|
672 from 4 have "x < y \<and> tree_greater y d" by auto |
|
673 hence "tree_greater x d" by (blast dest: tree_greater_trans) |
|
674 with 4 Empty have "sorted a" and "sorted (Branch B Empty y w d)" and "tree_less x a" and "tree_greater x (Branch B Empty y w d)" by auto |
|
675 with Empty show ?thesis by (simp add: balance_left_sorted) |
|
676 next |
|
677 case (Red lta va ka rta) |
|
678 with 2 4 have "x < va \<and> tree_less x a" by simp |
|
679 hence 5: "tree_less va a" by (blast dest: tree_less_trans) |
|
680 from Red 3 4 have "va < y \<and> tree_greater y d" by simp |
|
681 hence "tree_greater va d" by (blast dest: tree_greater_trans) |
|
682 with Red 2 3 4 5 show ?thesis by simp |
|
683 next |
|
684 case (Black lta va ka rta) |
|
685 from 4 have "x < y \<and> tree_greater y d" by auto |
|
686 hence "tree_greater x d" by (blast dest: tree_greater_trans) |
|
687 with Black 2 3 4 have "sorted a" and "sorted (Branch B (combine b c) y w d)" and "tree_less x a" and "tree_greater x (Branch B (combine b c) y w d)" by auto |
|
688 with Black show ?thesis by (simp add: balance_left_sorted) |
|
689 qed |
|
690 next |
|
691 case (5 va vb vd vc b x w c) |
|
692 hence "k < x \<and> tree_less k (Branch B va vb vd vc)" by simp |
|
693 hence "tree_less x (Branch B va vb vd vc)" by (blast dest: tree_less_trans) |
|
694 with 5 show ?case by (simp add: combine_tree_less) |
|
695 next |
|
696 case (6 a x v b va vb vd vc) |
|
697 hence "x < k \<and> tree_greater k (Branch B va vb vd vc)" by simp |
|
698 hence "tree_greater x (Branch B va vb vd vc)" by (blast dest: tree_greater_trans) |
|
699 with 6 show ?case by (simp add: combine_tree_greater) |
|
700 qed simp+ |
|
701 |
|
702 lemma combine_in_tree: |
|
703 assumes "inv2 l" "inv2 r" "bheight l = bheight r" "inv1 l" "inv1 r" |
|
704 shows "entry_in_tree k v (combine l r) = (entry_in_tree k v l \<or> entry_in_tree k v r)" |
|
705 using assms |
|
706 proof (induct l r rule: combine.induct) |
|
707 case (4 _ _ _ b c) |
|
708 hence a: "bheight (combine b c) = bheight b" by (simp add: combine_inv2) |
|
709 from 4 have b: "inv1l (combine b c)" by (simp add: combine_inv1) |
|
710 |
|
711 show ?case |
|
712 proof (cases "combine b c" rule: rbt_cases) |
|
713 case Empty |
|
714 with 4 a show ?thesis by (auto simp: balance_left_in_tree) |
|
715 next |
|
716 case (Red lta ka va rta) |
|
717 with 4 show ?thesis by auto |
|
718 next |
|
719 case (Black lta ka va rta) |
|
720 with a b 4 show ?thesis by (auto simp: balance_left_in_tree) |
|
721 qed |
|
722 qed (auto split: rbt.splits color.splits) |
|
723 |
|
724 fun |
|
725 del_from_left :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" and |
|
726 del_from_right :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" and |
|
727 del :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" |
|
728 where |
|
729 "del x Empty = Empty" | |
|
730 "del x (Branch c a y s b) = (if x < y then del_from_left x a y s b else (if x > y then del_from_right x a y s b else combine a b))" | |
|
731 "del_from_left x (Branch B lt z v rt) y s b = balance_left (del x (Branch B lt z v rt)) y s b" | |
|
732 "del_from_left x a y s b = Branch R (del x a) y s b" | |
|
733 "del_from_right x a y s (Branch B lt z v rt) = balance_right a y s (del x (Branch B lt z v rt))" | |
|
734 "del_from_right x a y s b = Branch R a y s (del x b)" |
|
735 |
|
736 lemma |
|
737 assumes "inv2 lt" "inv1 lt" |
|
738 shows |
|
739 "\<lbrakk>inv2 rt; bheight lt = bheight rt; inv1 rt\<rbrakk> \<Longrightarrow> |
|
740 inv2 (del_from_left x lt k v rt) \<and> bheight (del_from_left x lt k v rt) = bheight lt \<and> (color_of lt = B \<and> color_of rt = B \<and> inv1 (del_from_left x lt k v rt) \<or> (color_of lt \<noteq> B \<or> color_of rt \<noteq> B) \<and> inv1l (del_from_left x lt k v rt))" |
|
741 and "\<lbrakk>inv2 rt; bheight lt = bheight rt; inv1 rt\<rbrakk> \<Longrightarrow> |
|
742 inv2 (del_from_right x lt k v rt) \<and> bheight (del_from_right x lt k v rt) = bheight lt \<and> (color_of lt = B \<and> color_of rt = B \<and> inv1 (del_from_right x lt k v rt) \<or> (color_of lt \<noteq> B \<or> color_of rt \<noteq> B) \<and> inv1l (del_from_right x lt k v rt))" |
|
743 and del_inv1_inv2: "inv2 (del x lt) \<and> (color_of lt = R \<and> bheight (del x lt) = bheight lt \<and> inv1 (del x lt) |
|
744 \<or> color_of lt = B \<and> bheight (del x lt) = bheight lt - 1 \<and> inv1l (del x lt))" |
|
745 using assms |
|
746 proof (induct x lt k v rt and x lt k v rt and x lt rule: del_from_left_del_from_right_del.induct) |
|
747 case (2 y c _ y') |
|
748 have "y = y' \<or> y < y' \<or> y > y'" by auto |
|
749 thus ?case proof (elim disjE) |
|
750 assume "y = y'" |
|
751 with 2 show ?thesis by (cases c) (simp add: combine_inv2 combine_inv1)+ |
|
752 next |
|
753 assume "y < y'" |
|
754 with 2 show ?thesis by (cases c) auto |
|
755 next |
|
756 assume "y' < y" |
|
757 with 2 show ?thesis by (cases c) auto |
|
758 qed |
|
759 next |
|
760 case (3 y lt z v rta y' ss bb) |
|
761 thus ?case by (cases "color_of (Branch B lt z v rta) = B \<and> color_of bb = B") (simp add: balance_left_inv2_with_inv1 balance_left_inv1 balance_left_inv1l)+ |
|
762 next |
|
763 case (5 y a y' ss lt z v rta) |
|
764 thus ?case by (cases "color_of a = B \<and> color_of (Branch B lt z v rta) = B") (simp add: balance_right_inv2_with_inv1 balance_right_inv1 balance_right_inv1l)+ |
|
765 next |
|
766 case ("6_1" y a y' ss) thus ?case by (cases "color_of a = B \<and> color_of Empty = B") simp+ |
|
767 qed auto |
|
768 |
|
769 lemma |
|
770 del_from_left_tree_less: "\<lbrakk>tree_less v lt; tree_less v rt; k < v\<rbrakk> \<Longrightarrow> tree_less v (del_from_left x lt k y rt)" |
|
771 and del_from_right_tree_less: "\<lbrakk>tree_less v lt; tree_less v rt; k < v\<rbrakk> \<Longrightarrow> tree_less v (del_from_right x lt k y rt)" |
|
772 and del_tree_less: "tree_less v lt \<Longrightarrow> tree_less v (del x lt)" |
|
773 by (induct x lt k y rt and x lt k y rt and x lt rule: del_from_left_del_from_right_del.induct) |
|
774 (auto simp: balance_left_tree_less balance_right_tree_less) |
|
775 |
|
776 lemma del_from_left_tree_greater: "\<lbrakk>tree_greater v lt; tree_greater v rt; k > v\<rbrakk> \<Longrightarrow> tree_greater v (del_from_left x lt k y rt)" |
|
777 and del_from_right_tree_greater: "\<lbrakk>tree_greater v lt; tree_greater v rt; k > v\<rbrakk> \<Longrightarrow> tree_greater v (del_from_right x lt k y rt)" |
|
778 and del_tree_greater: "tree_greater v lt \<Longrightarrow> tree_greater v (del x lt)" |
|
779 by (induct x lt k y rt and x lt k y rt and x lt rule: del_from_left_del_from_right_del.induct) |
|
780 (auto simp: balance_left_tree_greater balance_right_tree_greater) |
|
781 |
|
782 lemma "\<lbrakk>sorted lt; sorted rt; tree_less k lt; tree_greater k rt\<rbrakk> \<Longrightarrow> sorted (del_from_left x lt k y rt)" |
|
783 and "\<lbrakk>sorted lt; sorted rt; tree_less k lt; tree_greater k rt\<rbrakk> \<Longrightarrow> sorted (del_from_right x lt k y rt)" |
|
784 and del_sorted: "sorted lt \<Longrightarrow> sorted (del x lt)" |
|
785 proof (induct x lt k y rt and x lt k y rt and x lt rule: del_from_left_del_from_right_del.induct) |
|
786 case (3 x lta zz v rta yy ss bb) |
|
787 from 3 have "tree_less yy (Branch B lta zz v rta)" by simp |
|
788 hence "tree_less yy (del x (Branch B lta zz v rta))" by (rule del_tree_less) |
|
789 with 3 show ?case by (simp add: balance_left_sorted) |
|
790 next |
|
791 case ("4_2" x vaa vbb vdd vc yy ss bb) |
|
792 hence "tree_less yy (Branch R vaa vbb vdd vc)" by simp |
|
793 hence "tree_less yy (del x (Branch R vaa vbb vdd vc))" by (rule del_tree_less) |
|
794 with "4_2" show ?case by simp |
|
795 next |
|
796 case (5 x aa yy ss lta zz v rta) |
|
797 hence "tree_greater yy (Branch B lta zz v rta)" by simp |
|
798 hence "tree_greater yy (del x (Branch B lta zz v rta))" by (rule del_tree_greater) |
|
799 with 5 show ?case by (simp add: balance_right_sorted) |
|
800 next |
|
801 case ("6_2" x aa yy ss vaa vbb vdd vc) |
|
802 hence "tree_greater yy (Branch R vaa vbb vdd vc)" by simp |
|
803 hence "tree_greater yy (del x (Branch R vaa vbb vdd vc))" by (rule del_tree_greater) |
|
804 with "6_2" show ?case by simp |
|
805 qed (auto simp: combine_sorted) |
|
806 |
|
807 lemma "\<lbrakk>sorted lt; sorted rt; tree_less kt lt; tree_greater kt rt; inv1 lt; inv1 rt; inv2 lt; inv2 rt; bheight lt = bheight rt; x < kt\<rbrakk> \<Longrightarrow> entry_in_tree k v (del_from_left x lt kt y rt) = (False \<or> (x \<noteq> k \<and> entry_in_tree k v (Branch c lt kt y rt)))" |
|
808 and "\<lbrakk>sorted lt; sorted rt; tree_less kt lt; tree_greater kt rt; inv1 lt; inv1 rt; inv2 lt; inv2 rt; bheight lt = bheight rt; x > kt\<rbrakk> \<Longrightarrow> entry_in_tree k v (del_from_right x lt kt y rt) = (False \<or> (x \<noteq> k \<and> entry_in_tree k v (Branch c lt kt y rt)))" |
|
809 and del_in_tree: "\<lbrakk>sorted t; inv1 t; inv2 t\<rbrakk> \<Longrightarrow> entry_in_tree k v (del x t) = (False \<or> (x \<noteq> k \<and> entry_in_tree k v t))" |
|
810 proof (induct x lt kt y rt and x lt kt y rt and x t rule: del_from_left_del_from_right_del.induct) |
|
811 case (2 xx c aa yy ss bb) |
|
812 have "xx = yy \<or> xx < yy \<or> xx > yy" by auto |
|
813 from this 2 show ?case proof (elim disjE) |
|
814 assume "xx = yy" |
|
815 with 2 show ?thesis proof (cases "xx = k") |
|
816 case True |
|
817 from 2 `xx = yy` `xx = k` have "sorted (Branch c aa yy ss bb) \<and> k = yy" by simp |
|
818 hence "\<not> entry_in_tree k v aa" "\<not> entry_in_tree k v bb" by (auto simp: tree_less_nit tree_greater_prop) |
|
819 with `xx = yy` 2 `xx = k` show ?thesis by (simp add: combine_in_tree) |
|
820 qed (simp add: combine_in_tree) |
|
821 qed simp+ |
|
822 next |
|
823 case (3 xx lta zz vv rta yy ss bb) |
|
824 def mt[simp]: mt == "Branch B lta zz vv rta" |
|
825 from 3 have "inv2 mt \<and> inv1 mt" by simp |
|
826 hence "inv2 (del xx mt) \<and> (color_of mt = R \<and> bheight (del xx mt) = bheight mt \<and> inv1 (del xx mt) \<or> color_of mt = B \<and> bheight (del xx mt) = bheight mt - 1 \<and> inv1l (del xx mt))" by (blast dest: del_inv1_inv2) |
|
827 with 3 have 4: "entry_in_tree k v (del_from_left xx mt yy ss bb) = (False \<or> xx \<noteq> k \<and> entry_in_tree k v mt \<or> (k = yy \<and> v = ss) \<or> entry_in_tree k v bb)" by (simp add: balance_left_in_tree) |
|
828 thus ?case proof (cases "xx = k") |
|
829 case True |
|
830 from 3 True have "tree_greater yy bb \<and> yy > k" by simp |
|
831 hence "tree_greater k bb" by (blast dest: tree_greater_trans) |
|
832 with 3 4 True show ?thesis by (auto simp: tree_greater_nit) |
|
833 qed auto |
|
834 next |
|
835 case ("4_1" xx yy ss bb) |
|
836 show ?case proof (cases "xx = k") |
|
837 case True |
|
838 with "4_1" have "tree_greater yy bb \<and> k < yy" by simp |
|
839 hence "tree_greater k bb" by (blast dest: tree_greater_trans) |
|
840 with "4_1" `xx = k` |
|
841 have "entry_in_tree k v (Branch R Empty yy ss bb) = entry_in_tree k v Empty" by (auto simp: tree_greater_nit) |
|
842 thus ?thesis by auto |
|
843 qed simp+ |
|
844 next |
|
845 case ("4_2" xx vaa vbb vdd vc yy ss bb) |
|
846 thus ?case proof (cases "xx = k") |
|
847 case True |
|
848 with "4_2" have "k < yy \<and> tree_greater yy bb" by simp |
|
849 hence "tree_greater k bb" by (blast dest: tree_greater_trans) |
|
850 with True "4_2" show ?thesis by (auto simp: tree_greater_nit) |
|
851 qed auto |
|
852 next |
|
853 case (5 xx aa yy ss lta zz vv rta) |
|
854 def mt[simp]: mt == "Branch B lta zz vv rta" |
|
855 from 5 have "inv2 mt \<and> inv1 mt" by simp |
|
856 hence "inv2 (del xx mt) \<and> (color_of mt = R \<and> bheight (del xx mt) = bheight mt \<and> inv1 (del xx mt) \<or> color_of mt = B \<and> bheight (del xx mt) = bheight mt - 1 \<and> inv1l (del xx mt))" by (blast dest: del_inv1_inv2) |
|
857 with 5 have 3: "entry_in_tree k v (del_from_right xx aa yy ss mt) = (entry_in_tree k v aa \<or> (k = yy \<and> v = ss) \<or> False \<or> xx \<noteq> k \<and> entry_in_tree k v mt)" by (simp add: balance_right_in_tree) |
|
858 thus ?case proof (cases "xx = k") |
|
859 case True |
|
860 from 5 True have "tree_less yy aa \<and> yy < k" by simp |
|
861 hence "tree_less k aa" by (blast dest: tree_less_trans) |
|
862 with 3 5 True show ?thesis by (auto simp: tree_less_nit) |
|
863 qed auto |
|
864 next |
|
865 case ("6_1" xx aa yy ss) |
|
866 show ?case proof (cases "xx = k") |
|
867 case True |
|
868 with "6_1" have "tree_less yy aa \<and> k > yy" by simp |
|
869 hence "tree_less k aa" by (blast dest: tree_less_trans) |
|
870 with "6_1" `xx = k` show ?thesis by (auto simp: tree_less_nit) |
|
871 qed simp |
|
872 next |
|
873 case ("6_2" xx aa yy ss vaa vbb vdd vc) |
|
874 thus ?case proof (cases "xx = k") |
|
875 case True |
|
876 with "6_2" have "k > yy \<and> tree_less yy aa" by simp |
|
877 hence "tree_less k aa" by (blast dest: tree_less_trans) |
|
878 with True "6_2" show ?thesis by (auto simp: tree_less_nit) |
|
879 qed auto |
|
880 qed simp |
|
881 |
|
882 |
|
883 definition delete where |
|
884 delete_def: "delete k t = paint B (del k t)" |
|
885 |
|
886 theorem delete_is_rbt [simp]: assumes "is_rbt t" shows "is_rbt (delete k t)" |
|
887 proof - |
|
888 from assms have "inv2 t" and "inv1 t" unfolding is_rbt_def by auto |
|
889 hence "inv2 (del k t) \<and> (color_of t = R \<and> bheight (del k t) = bheight t \<and> inv1 (del k t) \<or> color_of t = B \<and> bheight (del k t) = bheight t - 1 \<and> inv1l (del k t))" by (rule del_inv1_inv2) |
|
890 hence "inv2 (del k t) \<and> inv1l (del k t)" by (cases "color_of t") auto |
|
891 with assms show ?thesis |
|
892 unfolding is_rbt_def delete_def |
|
893 by (auto intro: paint_sorted del_sorted) |
|
894 qed |
|
895 |
|
896 lemma delete_in_tree: |
|
897 assumes "is_rbt t" |
|
898 shows "entry_in_tree k v (delete x t) = (x \<noteq> k \<and> entry_in_tree k v t)" |
|
899 using assms unfolding is_rbt_def delete_def |
|
900 by (auto simp: del_in_tree) |
|
901 |
|
902 lemma lookup_delete: |
|
903 assumes is_rbt: "is_rbt t" |
|
904 shows "lookup (delete k t) = (lookup t)|`(-{k})" |
|
905 proof |
|
906 fix x |
|
907 show "lookup (delete k t) x = (lookup t |` (-{k})) x" |
|
908 proof (cases "x = k") |
|
909 assume "x = k" |
|
910 with is_rbt show ?thesis |
|
911 by (cases "lookup (delete k t) k") (auto simp: lookup_in_tree delete_in_tree) |
|
912 next |
|
913 assume "x \<noteq> k" |
|
914 thus ?thesis |
|
915 by auto (metis is_rbt delete_is_rbt delete_in_tree is_rbt_sorted lookup_from_in_tree) |
|
916 qed |
|
917 qed |
|
918 |
|
919 |
|
920 subsection {* Union *} |
|
921 |
|
922 primrec |
|
923 union_with_key :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" |
|
924 where |
|
925 "union_with_key f t Empty = t" |
|
926 | "union_with_key f t (Branch c lt k v rt) = union_with_key f (union_with_key f (insert_with_key f k v t) lt) rt" |
|
927 |
|
928 lemma unionwk_sorted: "sorted lt \<Longrightarrow> sorted (union_with_key f lt rt)" |
|
929 by (induct rt arbitrary: lt) (auto simp: insertwk_sorted) |
|
930 theorem unionwk_is_rbt[simp]: "is_rbt lt \<Longrightarrow> is_rbt (union_with_key f lt rt)" |
|
931 by (induct rt arbitrary: lt) (simp add: insertwk_is_rbt)+ |
|
932 |
|
933 definition |
|
934 union_with where |
|
935 "union_with f = union_with_key (\<lambda>_. f)" |
|
936 |
|
937 theorem unionw_is_rbt: "is_rbt lt \<Longrightarrow> is_rbt (union_with f lt rt)" unfolding union_with_def by simp |
|
938 |
|
939 definition union where |
|
940 "union = union_with_key (%_ _ rv. rv)" |
|
941 |
|
942 theorem union_is_rbt: "is_rbt lt \<Longrightarrow> is_rbt (union lt rt)" unfolding union_def by simp |
|
943 |
|
944 lemma union_Branch[simp]: |
|
945 "union t (Branch c lt k v rt) = union (union (insert k v t) lt) rt" |
|
946 unfolding union_def insert_def |
|
947 by simp |
|
948 |
|
949 lemma lookup_union: |
|
950 assumes "is_rbt s" "sorted t" |
|
951 shows "lookup (union s t) = lookup s ++ lookup t" |
|
952 using assms |
|
953 proof (induct t arbitrary: s) |
|
954 case Empty thus ?case by (auto simp: union_def) |
|
955 next |
|
956 case (Branch c l k v r s) |
|
957 then have "sorted r" "sorted l" "l |\<guillemotleft> k" "k \<guillemotleft>| r" by auto |
|
958 |
|
959 have meq: "lookup s(k \<mapsto> v) ++ lookup l ++ lookup r = |
|
960 lookup s ++ |
|
961 (\<lambda>a. if a < k then lookup l a |
|
962 else if k < a then lookup r a else Some v)" (is "?m1 = ?m2") |
|
963 proof (rule ext) |
|
964 fix a |
|
965 |
|
966 have "k < a \<or> k = a \<or> k > a" by auto |
|
967 thus "?m1 a = ?m2 a" |
|
968 proof (elim disjE) |
|
969 assume "k < a" |
|
970 with `l |\<guillemotleft> k` have "l |\<guillemotleft> a" by (rule tree_less_trans) |
|
971 with `k < a` show ?thesis |
|
972 by (auto simp: map_add_def split: option.splits) |
|
973 next |
|
974 assume "k = a" |
|
975 with `l |\<guillemotleft> k` `k \<guillemotleft>| r` |
|
976 show ?thesis by (auto simp: map_add_def) |
|
977 next |
|
978 assume "a < k" |
|
979 from this `k \<guillemotleft>| r` have "a \<guillemotleft>| r" by (rule tree_greater_trans) |
|
980 with `a < k` show ?thesis |
|
981 by (auto simp: map_add_def split: option.splits) |
|
982 qed |
|
983 qed |
|
984 |
|
985 from Branch have is_rbt: "is_rbt (RBT_Impl.union (RBT_Impl.insert k v s) l)" |
|
986 by (auto intro: union_is_rbt insert_is_rbt) |
|
987 with Branch have IHs: |
|
988 "lookup (union (union (insert k v s) l) r) = lookup (union (insert k v s) l) ++ lookup r" |
|
989 "lookup (union (insert k v s) l) = lookup (insert k v s) ++ lookup l" |
|
990 by auto |
|
991 |
|
992 with meq show ?case |
|
993 by (auto simp: lookup_insert[OF Branch(3)]) |
|
994 |
|
995 qed |
|
996 |
|
997 |
|
998 subsection {* Modifying existing entries *} |
|
999 |
|
1000 primrec |
|
1001 map_entry :: "'a\<Colon>linorder \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" |
|
1002 where |
|
1003 "map_entry k f Empty = Empty" |
|
1004 | "map_entry k f (Branch c lt x v rt) = |
|
1005 (if k < x then Branch c (map_entry k f lt) x v rt |
|
1006 else if k > x then (Branch c lt x v (map_entry k f rt)) |
|
1007 else Branch c lt x (f v) rt)" |
|
1008 |
|
1009 lemma map_entry_color_of: "color_of (map_entry k f t) = color_of t" by (induct t) simp+ |
|
1010 lemma map_entry_inv1: "inv1 (map_entry k f t) = inv1 t" by (induct t) (simp add: map_entry_color_of)+ |
|
1011 lemma map_entry_inv2: "inv2 (map_entry k f t) = inv2 t" "bheight (map_entry k f t) = bheight t" by (induct t) simp+ |
|
1012 lemma map_entry_tree_greater: "tree_greater a (map_entry k f t) = tree_greater a t" by (induct t) simp+ |
|
1013 lemma map_entry_tree_less: "tree_less a (map_entry k f t) = tree_less a t" by (induct t) simp+ |
|
1014 lemma map_entry_sorted: "sorted (map_entry k f t) = sorted t" |
|
1015 by (induct t) (simp_all add: map_entry_tree_less map_entry_tree_greater) |
|
1016 |
|
1017 theorem map_entry_is_rbt [simp]: "is_rbt (map_entry k f t) = is_rbt t" |
|
1018 unfolding is_rbt_def by (simp add: map_entry_inv2 map_entry_color_of map_entry_sorted map_entry_inv1 ) |
|
1019 |
|
1020 theorem lookup_map_entry: |
|
1021 "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))" |
|
1022 by (induct t) (auto split: option.splits simp add: expand_fun_eq) |
|
1023 |
|
1024 |
|
1025 subsection {* Mapping all entries *} |
|
1026 |
|
1027 primrec |
|
1028 map :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'c) rbt" |
|
1029 where |
|
1030 "map f Empty = Empty" |
|
1031 | "map f (Branch c lt k v rt) = Branch c (map f lt) k (f k v) (map f rt)" |
|
1032 |
|
1033 lemma map_entries [simp]: "entries (map f t) = List.map (\<lambda>(k, v). (k, f k v)) (entries t)" |
|
1034 by (induct t) auto |
|
1035 lemma map_keys [simp]: "keys (map f t) = keys t" by (simp add: keys_def split_def) |
|
1036 lemma map_tree_greater: "tree_greater k (map f t) = tree_greater k t" by (induct t) simp+ |
|
1037 lemma map_tree_less: "tree_less k (map f t) = tree_less k t" by (induct t) simp+ |
|
1038 lemma map_sorted: "sorted (map f t) = sorted t" by (induct t) (simp add: map_tree_less map_tree_greater)+ |
|
1039 lemma map_color_of: "color_of (map f t) = color_of t" by (induct t) simp+ |
|
1040 lemma map_inv1: "inv1 (map f t) = inv1 t" by (induct t) (simp add: map_color_of)+ |
|
1041 lemma map_inv2: "inv2 (map f t) = inv2 t" "bheight (map f t) = bheight t" by (induct t) simp+ |
|
1042 theorem map_is_rbt [simp]: "is_rbt (map f t) = is_rbt t" |
|
1043 unfolding is_rbt_def by (simp add: map_inv1 map_inv2 map_sorted map_color_of) |
|
1044 |
|
1045 theorem lookup_map: "lookup (map f t) x = Option.map (f x) (lookup t x)" |
|
1046 by (induct t) auto |
|
1047 |
|
1048 |
|
1049 subsection {* Folding over entries *} |
|
1050 |
|
1051 definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" where |
|
1052 "fold f t s = foldl (\<lambda>s (k, v). f k v s) s (entries t)" |
|
1053 |
|
1054 lemma fold_simps [simp, code]: |
|
1055 "fold f Empty = id" |
|
1056 "fold f (Branch c lt k v rt) = fold f rt \<circ> f k v \<circ> fold f lt" |
|
1057 by (simp_all add: fold_def expand_fun_eq) |
|
1058 |
|
1059 |
|
1060 subsection {* Bulkloading a tree *} |
|
1061 |
|
1062 definition bulkload :: "('a \<times> 'b) list \<Rightarrow> ('a\<Colon>linorder, 'b) rbt" where |
|
1063 "bulkload xs = foldr (\<lambda>(k, v). insert k v) xs Empty" |
|
1064 |
|
1065 lemma bulkload_is_rbt [simp, intro]: |
|
1066 "is_rbt (bulkload xs)" |
|
1067 unfolding bulkload_def by (induct xs) auto |
|
1068 |
|
1069 lemma lookup_bulkload: |
|
1070 "lookup (bulkload xs) = map_of xs" |
|
1071 proof - |
|
1072 obtain ys where "ys = rev xs" by simp |
|
1073 have "\<And>t. is_rbt t \<Longrightarrow> |
|
1074 lookup (foldl (\<lambda>t (k, v). insert k v t) t ys) = lookup t ++ map_of (rev ys)" |
|
1075 by (induct ys) (simp_all add: bulkload_def split_def lookup_insert) |
|
1076 from this Empty_is_rbt have |
|
1077 "lookup (foldl (\<lambda>t (k, v). insert k v t) Empty (rev xs)) = lookup Empty ++ map_of xs" |
|
1078 by (simp add: `ys = rev xs`) |
|
1079 then show ?thesis by (simp add: bulkload_def foldl_foldr lookup_Empty split_def) |
|
1080 qed |
|
1081 |
|
1082 hide (open) const Empty insert delete entries keys bulkload lookup map_entry map fold union sorted |
|
1083 |
|
1084 end |