|
1 (* Title: RBT.thy |
|
2 ID: $Id$ |
|
3 Author: Markus Reiter, TU Muenchen |
|
4 Author: Alexander Krauss, TU Muenchen |
|
5 *) |
|
6 |
|
7 header {* Red-Black Trees *} |
|
8 |
|
9 (*<*) |
|
10 theory RBT |
|
11 imports Main AssocList |
|
12 begin |
|
13 |
|
14 datatype color = R | B |
|
15 datatype ('a,'b)"rbt" = Empty | Tr color "('a,'b)rbt" 'a 'b "('a,'b)rbt" |
|
16 |
|
17 (* Suchbaum-Eigenschaften *) |
|
18 |
|
19 primrec |
|
20 pin_tree :: "'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> bool" |
|
21 where |
|
22 "pin_tree k v Empty = False" |
|
23 | "pin_tree k v (Tr c l x y r) = (k = x \<and> v = y \<or> pin_tree k v l \<or> pin_tree k v r)" |
|
24 |
|
25 primrec |
|
26 keys :: "('k,'v) rbt \<Rightarrow> 'k set" |
|
27 where |
|
28 "keys Empty = {}" |
|
29 | "keys (Tr _ l k _ r) = { k } \<union> keys l \<union> keys r" |
|
30 |
|
31 lemma pint_keys: "pin_tree k v t \<Longrightarrow> k \<in> keys t" by (induct t) auto |
|
32 |
|
33 primrec tlt :: "'a\<Colon>order \<Rightarrow> ('a,'b) rbt \<Rightarrow> bool" |
|
34 where |
|
35 "tlt k Empty = True" |
|
36 | "tlt k (Tr c lt kt v rt) = (kt < k \<and> tlt k lt \<and> tlt k rt)" |
|
37 |
|
38 abbreviation tllt (infix "|\<guillemotleft>" 50) |
|
39 where "t |\<guillemotleft> x == tlt x t" |
|
40 |
|
41 primrec tgt :: "'a\<Colon>order \<Rightarrow> ('a,'b) rbt \<Rightarrow> bool" (infix "\<guillemotleft>|" 50) |
|
42 where |
|
43 "tgt k Empty = True" |
|
44 | "tgt k (Tr c lt kt v rt) = (k < kt \<and> tgt k lt \<and> tgt k rt)" |
|
45 |
|
46 lemma tlt_prop: "(t |\<guillemotleft> k) = (\<forall>x\<in>keys t. x < k)" by (induct t) auto |
|
47 lemma tgt_prop: "(k \<guillemotleft>| t) = (\<forall>x\<in>keys t. k < x)" by (induct t) auto |
|
48 lemmas tlgt_props = tlt_prop tgt_prop |
|
49 |
|
50 lemmas tgt_nit = tgt_prop pint_keys |
|
51 lemmas tlt_nit = tlt_prop pint_keys |
|
52 |
|
53 lemma tlt_trans: "\<lbrakk> t |\<guillemotleft> x; x < y \<rbrakk> \<Longrightarrow> t |\<guillemotleft> y" |
|
54 and tgt_trans: "\<lbrakk> x < y; y \<guillemotleft>| t\<rbrakk> \<Longrightarrow> x \<guillemotleft>| t" |
|
55 by (auto simp: tlgt_props) |
|
56 |
|
57 |
|
58 primrec st :: "('a::linorder, 'b) rbt \<Rightarrow> bool" |
|
59 where |
|
60 "st Empty = True" |
|
61 | "st (Tr c l k v r) = (l |\<guillemotleft> k \<and> k \<guillemotleft>| r \<and> st l \<and> st r)" |
|
62 |
|
63 primrec map_of :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" |
|
64 where |
|
65 "map_of Empty k = None" |
|
66 | "map_of (Tr _ l x y r) k = (if k < x then map_of l k else if x < k then map_of r k else Some y)" |
|
67 |
|
68 lemma map_of_tlt[simp]: "t |\<guillemotleft> k \<Longrightarrow> map_of t k = None" |
|
69 by (induct t) auto |
|
70 |
|
71 lemma map_of_tgt[simp]: "k \<guillemotleft>| t \<Longrightarrow> map_of t k = None" |
|
72 by (induct t) auto |
|
73 |
|
74 lemma mapof_keys: "st t \<Longrightarrow> dom (map_of t) = keys t" |
|
75 by (induct t) (auto simp: dom_def tgt_prop tlt_prop) |
|
76 |
|
77 lemma mapof_pit: "st t \<Longrightarrow> (map_of t k = Some v) = pin_tree k v t" |
|
78 by (induct t) (auto simp: tlt_prop tgt_prop pint_keys) |
|
79 |
|
80 lemma map_of_Empty: "map_of Empty = empty" |
|
81 by (rule ext) simp |
|
82 |
|
83 (* a kind of extensionality *) |
|
84 lemma mapof_from_pit: |
|
85 assumes st: "st t1" "st t2" |
|
86 and eq: "\<And>v. pin_tree (k\<Colon>'a\<Colon>linorder) v t1 = pin_tree k v t2" |
|
87 shows "map_of t1 k = map_of t2 k" |
|
88 proof (cases "map_of t1 k") |
|
89 case None |
|
90 then have "\<And>v. \<not> pin_tree k v t1" |
|
91 by (simp add: mapof_pit[symmetric] st) |
|
92 with None show ?thesis |
|
93 by (cases "map_of t2 k") (auto simp: mapof_pit st eq) |
|
94 next |
|
95 case (Some a) |
|
96 then show ?thesis |
|
97 apply (cases "map_of t2 k") |
|
98 apply (auto simp: mapof_pit st eq) |
|
99 by (auto simp add: mapof_pit[symmetric] st Some) |
|
100 qed |
|
101 |
|
102 subsection {* Red-black properties *} |
|
103 |
|
104 primrec treec :: "('a,'b) rbt \<Rightarrow> color" |
|
105 where |
|
106 "treec Empty = B" |
|
107 | "treec (Tr c _ _ _ _) = c" |
|
108 |
|
109 primrec inv1 :: "('a,'b) rbt \<Rightarrow> bool" |
|
110 where |
|
111 "inv1 Empty = True" |
|
112 | "inv1 (Tr c lt k v rt) = (inv1 lt \<and> inv1 rt \<and> (c = B \<or> treec lt = B \<and> treec rt = B))" |
|
113 |
|
114 (* Weaker version *) |
|
115 primrec inv1l :: "('a,'b) rbt \<Rightarrow> bool" |
|
116 where |
|
117 "inv1l Empty = True" |
|
118 | "inv1l (Tr c l k v r) = (inv1 l \<and> inv1 r)" |
|
119 lemma [simp]: "inv1 t \<Longrightarrow> inv1l t" by (cases t) simp+ |
|
120 |
|
121 primrec bh :: "('a,'b) rbt \<Rightarrow> nat" |
|
122 where |
|
123 "bh Empty = 0" |
|
124 | "bh (Tr c lt k v rt) = (if c = B then Suc (bh lt) else bh lt)" |
|
125 |
|
126 primrec inv2 :: "('a,'b) rbt \<Rightarrow> bool" |
|
127 where |
|
128 "inv2 Empty = True" |
|
129 | "inv2 (Tr c lt k v rt) = (inv2 lt \<and> inv2 rt \<and> bh lt = bh rt)" |
|
130 |
|
131 definition |
|
132 "isrbt t = (inv1 t \<and> inv2 t \<and> treec t = B \<and> st t)" |
|
133 |
|
134 lemma isrbt_st[simp]: "isrbt t \<Longrightarrow> st t" by (simp add: isrbt_def) |
|
135 |
|
136 lemma rbt_cases: |
|
137 obtains (Empty) "t = Empty" |
|
138 | (Red) l k v r where "t = Tr R l k v r" |
|
139 | (Black) l k v r where "t = Tr B l k v r" |
|
140 by (cases t, simp) (case_tac "color", auto) |
|
141 |
|
142 theorem Empty_isrbt[simp]: "isrbt Empty" |
|
143 unfolding isrbt_def by simp |
|
144 |
|
145 |
|
146 subsection {* Insertion *} |
|
147 |
|
148 fun (* slow, due to massive case splitting *) |
|
149 balance :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" |
|
150 where |
|
151 "balance (Tr R a w x b) s t (Tr R c y z d) = Tr R (Tr B a w x b) s t (Tr B c y z d)" | |
|
152 "balance (Tr R (Tr R a w x b) s t c) y z d = Tr R (Tr B a w x b) s t (Tr B c y z d)" | |
|
153 "balance (Tr R a w x (Tr R b s t c)) y z d = Tr R (Tr B a w x b) s t (Tr B c y z d)" | |
|
154 "balance a w x (Tr R b s t (Tr R c y z d)) = Tr R (Tr B a w x b) s t (Tr B c y z d)" | |
|
155 "balance a w x (Tr R (Tr R b s t c) y z d) = Tr R (Tr B a w x b) s t (Tr B c y z d)" | |
|
156 "balance a s t b = Tr B a s t b" |
|
157 |
|
158 lemma balance_inv1: "\<lbrakk>inv1l l; inv1l r\<rbrakk> \<Longrightarrow> inv1 (balance l k v r)" |
|
159 by (induct l k v r rule: balance.induct) auto |
|
160 |
|
161 lemma balance_bh: "bh l = bh r \<Longrightarrow> bh (balance l k v r) = Suc (bh l)" |
|
162 by (induct l k v r rule: balance.induct) auto |
|
163 |
|
164 lemma balance_inv2: |
|
165 assumes "inv2 l" "inv2 r" "bh l = bh r" |
|
166 shows "inv2 (balance l k v r)" |
|
167 using assms |
|
168 by (induct l k v r rule: balance.induct) auto |
|
169 |
|
170 lemma balance_tgt[simp]: "(v \<guillemotleft>| balance a k x b) = (v \<guillemotleft>| a \<and> v \<guillemotleft>| b \<and> v < k)" |
|
171 by (induct a k x b rule: balance.induct) auto |
|
172 |
|
173 lemma balance_tlt[simp]: "(balance a k x b |\<guillemotleft> v) = (a |\<guillemotleft> v \<and> b |\<guillemotleft> v \<and> k < v)" |
|
174 by (induct a k x b rule: balance.induct) auto |
|
175 |
|
176 lemma balance_st: |
|
177 fixes k :: "'a::linorder" |
|
178 assumes "st l" "st r" "l |\<guillemotleft> k" "k \<guillemotleft>| r" |
|
179 shows "st (balance l k v r)" |
|
180 using assms proof (induct l k v r rule: balance.induct) |
|
181 case ("2_2" a x w b y t c z s va vb vd vc) |
|
182 hence "y < z \<and> z \<guillemotleft>| Tr B va vb vd vc" |
|
183 by (auto simp add: tlgt_props) |
|
184 hence "tgt y (Tr B va vb vd vc)" by (blast dest: tgt_trans) |
|
185 with "2_2" show ?case by simp |
|
186 next |
|
187 case ("3_2" va vb vd vc x w b y s c z) |
|
188 from "3_2" have "x < y \<and> tlt x (Tr B va vb vd vc)" |
|
189 by (simp add: tlt.simps tgt.simps) |
|
190 hence "tlt y (Tr B va vb vd vc)" by (blast dest: tlt_trans) |
|
191 with "3_2" show ?case by simp |
|
192 next |
|
193 case ("3_3" x w b y s c z t va vb vd vc) |
|
194 from "3_3" have "y < z \<and> tgt z (Tr B va vb vd vc)" by simp |
|
195 hence "tgt y (Tr B va vb vd vc)" by (blast dest: tgt_trans) |
|
196 with "3_3" show ?case by simp |
|
197 next |
|
198 case ("3_4" vd ve vg vf x w b y s c z t va vb vii vc) |
|
199 hence "x < y \<and> tlt x (Tr B vd ve vg vf)" by simp |
|
200 hence 1: "tlt y (Tr B vd ve vg vf)" by (blast dest: tlt_trans) |
|
201 from "3_4" have "y < z \<and> tgt z (Tr B va vb vii vc)" by simp |
|
202 hence "tgt y (Tr B va vb vii vc)" by (blast dest: tgt_trans) |
|
203 with 1 "3_4" show ?case by simp |
|
204 next |
|
205 case ("4_2" va vb vd vc x w b y s c z t dd) |
|
206 hence "x < y \<and> tlt x (Tr B va vb vd vc)" by simp |
|
207 hence "tlt y (Tr B va vb vd vc)" by (blast dest: tlt_trans) |
|
208 with "4_2" show ?case by simp |
|
209 next |
|
210 case ("5_2" x w b y s c z t va vb vd vc) |
|
211 hence "y < z \<and> tgt z (Tr B va vb vd vc)" by simp |
|
212 hence "tgt y (Tr B va vb vd vc)" by (blast dest: tgt_trans) |
|
213 with "5_2" show ?case by simp |
|
214 next |
|
215 case ("5_3" va vb vd vc x w b y s c z t) |
|
216 hence "x < y \<and> tlt x (Tr B va vb vd vc)" by simp |
|
217 hence "tlt y (Tr B va vb vd vc)" by (blast dest: tlt_trans) |
|
218 with "5_3" show ?case by simp |
|
219 next |
|
220 case ("5_4" va vb vg vc x w b y s c z t vd ve vii vf) |
|
221 hence "x < y \<and> tlt x (Tr B va vb vg vc)" by simp |
|
222 hence 1: "tlt y (Tr B va vb vg vc)" by (blast dest: tlt_trans) |
|
223 from "5_4" have "y < z \<and> tgt z (Tr B vd ve vii vf)" by simp |
|
224 hence "tgt y (Tr B vd ve vii vf)" by (blast dest: tgt_trans) |
|
225 with 1 "5_4" show ?case by simp |
|
226 qed simp+ |
|
227 |
|
228 lemma keys_balance[simp]: |
|
229 "keys (balance l k v r) = { k } \<union> keys l \<union> keys r" |
|
230 by (induct l k v r rule: balance.induct) auto |
|
231 |
|
232 lemma balance_pit: |
|
233 "pin_tree k x (balance l v y r) = (pin_tree k x l \<or> k = v \<and> x = y \<or> pin_tree k x r)" |
|
234 by (induct l v y r rule: balance.induct) auto |
|
235 |
|
236 lemma map_of_balance[simp]: |
|
237 fixes k :: "'a::linorder" |
|
238 assumes "st l" "st r" "l |\<guillemotleft> k" "k \<guillemotleft>| r" |
|
239 shows "map_of (balance l k v r) x = map_of (Tr B l k v r) x" |
|
240 by (rule mapof_from_pit) (auto simp:assms balance_pit balance_st) |
|
241 |
|
242 primrec paint :: "color \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" |
|
243 where |
|
244 "paint c Empty = Empty" |
|
245 | "paint c (Tr _ l k v r) = Tr c l k v r" |
|
246 |
|
247 lemma paint_inv1l[simp]: "inv1l t \<Longrightarrow> inv1l (paint c t)" by (cases t) auto |
|
248 lemma paint_inv1[simp]: "inv1l t \<Longrightarrow> inv1 (paint B t)" by (cases t) auto |
|
249 lemma paint_inv2[simp]: "inv2 t \<Longrightarrow> inv2 (paint c t)" by (cases t) auto |
|
250 lemma paint_treec[simp]: "treec (paint B t) = B" by (cases t) auto |
|
251 lemma paint_st[simp]: "st t \<Longrightarrow> st (paint c t)" by (cases t) auto |
|
252 lemma paint_pit[simp]: "pin_tree k x (paint c t) = pin_tree k x t" by (cases t) auto |
|
253 lemma paint_mapof[simp]: "map_of (paint c t) = map_of t" by (rule ext) (cases t, auto) |
|
254 lemma paint_tgt[simp]: "(v \<guillemotleft>| paint c t) = (v \<guillemotleft>| t)" by (cases t) auto |
|
255 lemma paint_tlt[simp]: "(paint c t |\<guillemotleft> v) = (t |\<guillemotleft> v)" by (cases t) auto |
|
256 |
|
257 fun |
|
258 ins :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" |
|
259 where |
|
260 "ins f k v Empty = Tr R Empty k v Empty" | |
|
261 "ins f k v (Tr B l x y r) = (if k < x then balance (ins f k v l) x y r |
|
262 else if k > x then balance l x y (ins f k v r) |
|
263 else Tr B l x (f k y v) r)" | |
|
264 "ins f k v (Tr R l x y r) = (if k < x then Tr R (ins f k v l) x y r |
|
265 else if k > x then Tr R l x y (ins f k v r) |
|
266 else Tr R l x (f k y v) r)" |
|
267 |
|
268 lemma ins_inv1_inv2: |
|
269 assumes "inv1 t" "inv2 t" |
|
270 shows "inv2 (ins f k x t)" "bh (ins f k x t) = bh t" |
|
271 "treec t = B \<Longrightarrow> inv1 (ins f k x t)" "inv1l (ins f k x t)" |
|
272 using assms |
|
273 by (induct f k x t rule: ins.induct) (auto simp: balance_inv1 balance_inv2 balance_bh) |
|
274 |
|
275 lemma ins_tgt[simp]: "(v \<guillemotleft>| ins f k x t) = (v \<guillemotleft>| t \<and> k > v)" |
|
276 by (induct f k x t rule: ins.induct) auto |
|
277 lemma ins_tlt[simp]: "(ins f k x t |\<guillemotleft> v) = (t |\<guillemotleft> v \<and> k < v)" |
|
278 by (induct f k x t rule: ins.induct) auto |
|
279 lemma ins_st[simp]: "st t \<Longrightarrow> st (ins f k x t)" |
|
280 by (induct f k x t rule: ins.induct) (auto simp: balance_st) |
|
281 |
|
282 lemma keys_ins: "keys (ins f k v t) = { k } \<union> keys t" |
|
283 by (induct f k v t rule: ins.induct) auto |
|
284 |
|
285 lemma map_of_ins: |
|
286 fixes k :: "'a::linorder" |
|
287 assumes "st t" |
|
288 shows "map_of (ins f k v t) x = ((map_of t)(k |-> case map_of t k of None \<Rightarrow> v |
|
289 | Some w \<Rightarrow> f k w v)) x" |
|
290 using assms by (induct f k v t rule: ins.induct) auto |
|
291 |
|
292 definition |
|
293 insertwithkey :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" |
|
294 where |
|
295 "insertwithkey f k v t = paint B (ins f k v t)" |
|
296 |
|
297 lemma insertwk_st: "st t \<Longrightarrow> st (insertwithkey f k x t)" |
|
298 by (auto simp: insertwithkey_def) |
|
299 |
|
300 theorem insertwk_isrbt: |
|
301 assumes inv: "isrbt t" |
|
302 shows "isrbt (insertwithkey f k x t)" |
|
303 using assms |
|
304 unfolding insertwithkey_def isrbt_def |
|
305 by (auto simp: ins_inv1_inv2) |
|
306 |
|
307 lemma map_of_insertwk: |
|
308 assumes "st t" |
|
309 shows "map_of (insertwithkey f k v t) x = ((map_of t)(k |-> case map_of t k of None \<Rightarrow> v |
|
310 | Some w \<Rightarrow> f k w v)) x" |
|
311 unfolding insertwithkey_def using assms |
|
312 by (simp add:map_of_ins) |
|
313 |
|
314 definition |
|
315 insertw_def: "insertwith f = insertwithkey (\<lambda>_. f)" |
|
316 |
|
317 lemma insertw_st: "st t \<Longrightarrow> st (insertwith f k v t)" by (simp add: insertwk_st insertw_def) |
|
318 theorem insertw_isrbt: "isrbt t \<Longrightarrow> isrbt (insertwith f k v t)" by (simp add: insertwk_isrbt insertw_def) |
|
319 |
|
320 lemma map_of_insertw: |
|
321 assumes "isrbt t" |
|
322 shows "map_of (insertwith f k v t) = (map_of t)(k \<mapsto> (if k:dom (map_of t) then f (the (map_of t k)) v else v))" |
|
323 using assms |
|
324 unfolding insertw_def |
|
325 by (rule_tac ext) (cases "map_of t k", auto simp:map_of_insertwk dom_def) |
|
326 |
|
327 |
|
328 definition |
|
329 "insrt k v t = insertwithkey (\<lambda>_ _ nv. nv) k v t" |
|
330 |
|
331 lemma insrt_st: "st t \<Longrightarrow> st (insrt k v t)" by (simp add: insertwk_st insrt_def) |
|
332 theorem insrt_isrbt: "isrbt t \<Longrightarrow> isrbt (insrt k v t)" by (simp add: insertwk_isrbt insrt_def) |
|
333 |
|
334 lemma map_of_insert: |
|
335 assumes "isrbt t" |
|
336 shows "map_of (insrt k v t) = (map_of t)(k\<mapsto>v)" |
|
337 unfolding insrt_def |
|
338 using assms |
|
339 by (rule_tac ext) (simp add: map_of_insertwk split:option.split) |
|
340 |
|
341 |
|
342 subsection {* Deletion *} |
|
343 |
|
344 (*definition |
|
345 [simp]: "ibn t = (bh t > 0 \<and> treec t = B)" |
|
346 *) |
|
347 lemma bh_paintR'[simp]: "treec t = B \<Longrightarrow> bh (paint R t) = bh t - 1" |
|
348 by (cases t rule: rbt_cases) auto |
|
349 |
|
350 fun |
|
351 balleft :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" |
|
352 where |
|
353 "balleft (Tr R a k x b) s y c = Tr R (Tr B a k x b) s y c" | |
|
354 "balleft bl k x (Tr B a s y b) = balance bl k x (Tr R a s y b)" | |
|
355 "balleft bl k x (Tr R (Tr B a s y b) t z c) = Tr R (Tr B bl k x a) s y (balance b t z (paint R c))" | |
|
356 "balleft t k x s = Empty" |
|
357 |
|
358 lemma balleft_inv2_with_inv1: |
|
359 assumes "inv2 lt" "inv2 rt" "bh lt + 1 = bh rt" "inv1 rt" |
|
360 shows "bh (balleft lt k v rt) = bh lt + 1" |
|
361 and "inv2 (balleft lt k v rt)" |
|
362 using assms |
|
363 by (induct lt k v rt rule: balleft.induct) (auto simp: balance_inv2 balance_bh) |
|
364 |
|
365 lemma balleft_inv2_app: |
|
366 assumes "inv2 lt" "inv2 rt" "bh lt + 1 = bh rt" "treec rt = B" |
|
367 shows "inv2 (balleft lt k v rt)" |
|
368 "bh (balleft lt k v rt) = bh rt" |
|
369 using assms |
|
370 by (induct lt k v rt rule: balleft.induct) (auto simp add: balance_inv2 balance_bh)+ |
|
371 |
|
372 lemma balleft_inv1: "\<lbrakk>inv1l a; inv1 b; treec b = B\<rbrakk> \<Longrightarrow> inv1 (balleft a k x b)" |
|
373 by (induct a k x b rule: balleft.induct) (simp add: balance_inv1)+ |
|
374 |
|
375 lemma balleft_inv1l: "\<lbrakk> inv1l lt; inv1 rt \<rbrakk> \<Longrightarrow> inv1l (balleft lt k x rt)" |
|
376 by (induct lt k x rt rule: balleft.induct) (auto simp: balance_inv1) |
|
377 |
|
378 lemma balleft_st: "\<lbrakk> st l; st r; tlt k l; tgt k r \<rbrakk> \<Longrightarrow> st (balleft l k v r)" |
|
379 apply (induct l k v r rule: balleft.induct) |
|
380 apply (auto simp: balance_st) |
|
381 apply (unfold tgt_prop tlt_prop) |
|
382 by force+ |
|
383 |
|
384 lemma balleft_tgt: |
|
385 fixes k :: "'a::order" |
|
386 assumes "k \<guillemotleft>| a" "k \<guillemotleft>| b" "k < x" |
|
387 shows "k \<guillemotleft>| balleft a x t b" |
|
388 using assms |
|
389 by (induct a x t b rule: balleft.induct) auto |
|
390 |
|
391 lemma balleft_tlt: |
|
392 fixes k :: "'a::order" |
|
393 assumes "a |\<guillemotleft> k" "b |\<guillemotleft> k" "x < k" |
|
394 shows "balleft a x t b |\<guillemotleft> k" |
|
395 using assms |
|
396 by (induct a x t b rule: balleft.induct) auto |
|
397 |
|
398 lemma balleft_pit: |
|
399 assumes "inv1l l" "inv1 r" "bh l + 1 = bh r" |
|
400 shows "pin_tree k v (balleft l a b r) = (pin_tree k v l \<or> k = a \<and> v = b \<or> pin_tree k v r)" |
|
401 using assms |
|
402 by (induct l k v r rule: balleft.induct) (auto simp: balance_pit) |
|
403 |
|
404 fun |
|
405 balright :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" |
|
406 where |
|
407 "balright a k x (Tr R b s y c) = Tr R a k x (Tr B b s y c)" | |
|
408 "balright (Tr B a k x b) s y bl = balance (Tr R a k x b) s y bl" | |
|
409 "balright (Tr R a k x (Tr B b s y c)) t z bl = Tr R (balance (paint R a) k x b) s y (Tr B c t z bl)" | |
|
410 "balright t k x s = Empty" |
|
411 |
|
412 lemma balright_inv2_with_inv1: |
|
413 assumes "inv2 lt" "inv2 rt" "bh lt = bh rt + 1" "inv1 lt" |
|
414 shows "inv2 (balright lt k v rt) \<and> bh (balright lt k v rt) = bh lt" |
|
415 using assms |
|
416 by (induct lt k v rt rule: balright.induct) (auto simp: balance_inv2 balance_bh) |
|
417 |
|
418 lemma balright_inv1: "\<lbrakk>inv1 a; inv1l b; treec a = B\<rbrakk> \<Longrightarrow> inv1 (balright a k x b)" |
|
419 by (induct a k x b rule: balright.induct) (simp add: balance_inv1)+ |
|
420 |
|
421 lemma balright_inv1l: "\<lbrakk> inv1 lt; inv1l rt \<rbrakk> \<Longrightarrow>inv1l (balright lt k x rt)" |
|
422 by (induct lt k x rt rule: balright.induct) (auto simp: balance_inv1) |
|
423 |
|
424 lemma balright_st: "\<lbrakk> st l; st r; tlt k l; tgt k r \<rbrakk> \<Longrightarrow> st (balright l k v r)" |
|
425 apply (induct l k v r rule: balright.induct) |
|
426 apply (auto simp:balance_st) |
|
427 apply (unfold tlt_prop tgt_prop) |
|
428 by force+ |
|
429 |
|
430 lemma balright_tgt: |
|
431 fixes k :: "'a::order" |
|
432 assumes "k \<guillemotleft>| a" "k \<guillemotleft>| b" "k < x" |
|
433 shows "k \<guillemotleft>| balright a x t b" |
|
434 using assms by (induct a x t b rule: balright.induct) auto |
|
435 |
|
436 lemma balright_tlt: |
|
437 fixes k :: "'a::order" |
|
438 assumes "a |\<guillemotleft> k" "b |\<guillemotleft> k" "x < k" |
|
439 shows "balright a x t b |\<guillemotleft> k" |
|
440 using assms by (induct a x t b rule: balright.induct) auto |
|
441 |
|
442 lemma balright_pit: |
|
443 assumes "inv1 l" "inv1l r" "bh l = bh r + 1" "inv2 l" "inv2 r" |
|
444 shows "pin_tree x y (balright l k v r) = (pin_tree x y l \<or> x = k \<and> y = v \<or> pin_tree x y r)" |
|
445 using assms by (induct l k v r rule: balright.induct) (auto simp: balance_pit) |
|
446 |
|
447 |
|
448 text {* app *} |
|
449 |
|
450 fun |
|
451 app :: "('a,'b) rbt \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" |
|
452 where |
|
453 "app Empty x = x" |
|
454 | "app x Empty = x" |
|
455 | "app (Tr R a k x b) (Tr R c s y d) = (case (app b c) of |
|
456 Tr R b2 t z c2 \<Rightarrow> (Tr R (Tr R a k x b2) t z (Tr R c2 s y d)) | |
|
457 bc \<Rightarrow> Tr R a k x (Tr R bc s y d))" |
|
458 | "app (Tr B a k x b) (Tr B c s y d) = (case (app b c) of |
|
459 Tr R b2 t z c2 \<Rightarrow> Tr R (Tr B a k x b2) t z (Tr B c2 s y d) | |
|
460 bc \<Rightarrow> balleft a k x (Tr B bc s y d))" |
|
461 | "app a (Tr R b k x c) = Tr R (app a b) k x c" |
|
462 | "app (Tr R a k x b) c = Tr R a k x (app b c)" |
|
463 |
|
464 lemma app_inv2: |
|
465 assumes "inv2 lt" "inv2 rt" "bh lt = bh rt" |
|
466 shows "bh (app lt rt) = bh lt" "inv2 (app lt rt)" |
|
467 using assms |
|
468 by (induct lt rt rule: app.induct) |
|
469 (auto simp: balleft_inv2_app split: rbt.splits color.splits) |
|
470 |
|
471 lemma app_inv1: |
|
472 assumes "inv1 lt" "inv1 rt" |
|
473 shows "treec lt = B \<Longrightarrow> treec rt = B \<Longrightarrow> inv1 (app lt rt)" |
|
474 "inv1l (app lt rt)" |
|
475 using assms |
|
476 by (induct lt rt rule: app.induct) |
|
477 (auto simp: balleft_inv1 split: rbt.splits color.splits) |
|
478 |
|
479 lemma app_tgt[simp]: |
|
480 fixes k :: "'a::linorder" |
|
481 assumes "k \<guillemotleft>| l" "k \<guillemotleft>| r" |
|
482 shows "k \<guillemotleft>| app l r" |
|
483 using assms |
|
484 by (induct l r rule: app.induct) |
|
485 (auto simp: balleft_tgt split:rbt.splits color.splits) |
|
486 |
|
487 lemma app_tlt[simp]: |
|
488 fixes k :: "'a::linorder" |
|
489 assumes "l |\<guillemotleft> k" "r |\<guillemotleft> k" |
|
490 shows "app l r |\<guillemotleft> k" |
|
491 using assms |
|
492 by (induct l r rule: app.induct) |
|
493 (auto simp: balleft_tlt split:rbt.splits color.splits) |
|
494 |
|
495 lemma app_st: |
|
496 fixes k :: "'a::linorder" |
|
497 assumes "st l" "st r" "l |\<guillemotleft> k" "k \<guillemotleft>| r" |
|
498 shows "st (app l r)" |
|
499 using assms proof (induct l r rule: app.induct) |
|
500 case (3 a x v b c y w d) |
|
501 hence ineqs: "a |\<guillemotleft> x" "x \<guillemotleft>| b" "b |\<guillemotleft> k" "k \<guillemotleft>| c" "c |\<guillemotleft> y" "y \<guillemotleft>| d" |
|
502 by auto |
|
503 with 3 |
|
504 show ?case |
|
505 apply (cases "app b c" rule: rbt_cases) |
|
506 apply auto |
|
507 by (metis app_tgt app_tlt ineqs ineqs tlt.simps(2) tgt.simps(2) tgt_trans tlt_trans)+ |
|
508 next |
|
509 case (4 a x v b c y w d) |
|
510 hence "x < k \<and> tgt k c" by simp |
|
511 hence "tgt x c" by (blast dest: tgt_trans) |
|
512 with 4 have 2: "tgt x (app b c)" by (simp add: app_tgt) |
|
513 from 4 have "k < y \<and> tlt k b" by simp |
|
514 hence "tlt y b" by (blast dest: tlt_trans) |
|
515 with 4 have 3: "tlt y (app b c)" by (simp add: app_tlt) |
|
516 show ?case |
|
517 proof (cases "app b c" rule: rbt_cases) |
|
518 case Empty |
|
519 from 4 have "x < y \<and> tgt y d" by auto |
|
520 hence "tgt x d" by (blast dest: tgt_trans) |
|
521 with 4 Empty have "st a" and "st (Tr B Empty y w d)" and "tlt x a" and "tgt x (Tr B Empty y w d)" by auto |
|
522 with Empty show ?thesis by (simp add: balleft_st) |
|
523 next |
|
524 case (Red lta va ka rta) |
|
525 with 2 4 have "x < va \<and> tlt x a" by simp |
|
526 hence 5: "tlt va a" by (blast dest: tlt_trans) |
|
527 from Red 3 4 have "va < y \<and> tgt y d" by simp |
|
528 hence "tgt va d" by (blast dest: tgt_trans) |
|
529 with Red 2 3 4 5 show ?thesis by simp |
|
530 next |
|
531 case (Black lta va ka rta) |
|
532 from 4 have "x < y \<and> tgt y d" by auto |
|
533 hence "tgt x d" by (blast dest: tgt_trans) |
|
534 with Black 2 3 4 have "st a" and "st (Tr B (app b c) y w d)" and "tlt x a" and "tgt x (Tr B (app b c) y w d)" by auto |
|
535 with Black show ?thesis by (simp add: balleft_st) |
|
536 qed |
|
537 next |
|
538 case (5 va vb vd vc b x w c) |
|
539 hence "k < x \<and> tlt k (Tr B va vb vd vc)" by simp |
|
540 hence "tlt x (Tr B va vb vd vc)" by (blast dest: tlt_trans) |
|
541 with 5 show ?case by (simp add: app_tlt) |
|
542 next |
|
543 case (6 a x v b va vb vd vc) |
|
544 hence "x < k \<and> tgt k (Tr B va vb vd vc)" by simp |
|
545 hence "tgt x (Tr B va vb vd vc)" by (blast dest: tgt_trans) |
|
546 with 6 show ?case by (simp add: app_tgt) |
|
547 qed simp+ |
|
548 |
|
549 lemma app_pit: |
|
550 assumes "inv2 l" "inv2 r" "bh l = bh r" "inv1 l" "inv1 r" |
|
551 shows "pin_tree k v (app l r) = (pin_tree k v l \<or> pin_tree k v r)" |
|
552 using assms |
|
553 proof (induct l r rule: app.induct) |
|
554 case (4 _ _ _ b c) |
|
555 hence a: "bh (app b c) = bh b" by (simp add: app_inv2) |
|
556 from 4 have b: "inv1l (app b c)" by (simp add: app_inv1) |
|
557 |
|
558 show ?case |
|
559 proof (cases "app b c" rule: rbt_cases) |
|
560 case Empty |
|
561 with 4 a show ?thesis by (auto simp: balleft_pit) |
|
562 next |
|
563 case (Red lta ka va rta) |
|
564 with 4 show ?thesis by auto |
|
565 next |
|
566 case (Black lta ka va rta) |
|
567 with a b 4 show ?thesis by (auto simp: balleft_pit) |
|
568 qed |
|
569 qed (auto split: rbt.splits color.splits) |
|
570 |
|
571 fun |
|
572 delformLeft :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" and |
|
573 delformRight :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" and |
|
574 del :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" |
|
575 where |
|
576 "del x Empty = Empty" | |
|
577 "del x (Tr c a y s b) = (if x < y then delformLeft x a y s b else (if x > y then delformRight x a y s b else app a b))" | |
|
578 "delformLeft x (Tr B lt z v rt) y s b = balleft (del x (Tr B lt z v rt)) y s b" | |
|
579 "delformLeft x a y s b = Tr R (del x a) y s b" | |
|
580 "delformRight x a y s (Tr B lt z v rt) = balright a y s (del x (Tr B lt z v rt))" | |
|
581 "delformRight x a y s b = Tr R a y s (del x b)" |
|
582 |
|
583 lemma |
|
584 assumes "inv2 lt" "inv1 lt" |
|
585 shows |
|
586 "\<lbrakk>inv2 rt; bh lt = bh rt; inv1 rt\<rbrakk> \<Longrightarrow> |
|
587 inv2 (delformLeft x lt k v rt) \<and> bh (delformLeft x lt k v rt) = bh lt \<and> (treec lt = B \<and> treec rt = B \<and> inv1 (delformLeft x lt k v rt) \<or> (treec lt \<noteq> B \<or> treec rt \<noteq> B) \<and> inv1l (delformLeft x lt k v rt))" |
|
588 and "\<lbrakk>inv2 rt; bh lt = bh rt; inv1 rt\<rbrakk> \<Longrightarrow> |
|
589 inv2 (delformRight x lt k v rt) \<and> bh (delformRight x lt k v rt) = bh lt \<and> (treec lt = B \<and> treec rt = B \<and> inv1 (delformRight x lt k v rt) \<or> (treec lt \<noteq> B \<or> treec rt \<noteq> B) \<and> inv1l (delformRight x lt k v rt))" |
|
590 and del_inv1_inv2: "inv2 (del x lt) \<and> (treec lt = R \<and> bh (del x lt) = bh lt \<and> inv1 (del x lt) |
|
591 \<or> treec lt = B \<and> bh (del x lt) = bh lt - 1 \<and> inv1l (del x lt))" |
|
592 using assms |
|
593 proof (induct x lt k v rt and x lt k v rt and x lt rule: delformLeft_delformRight_del.induct) |
|
594 case (2 y c _ y') |
|
595 have "y = y' \<or> y < y' \<or> y > y'" by auto |
|
596 thus ?case proof (elim disjE) |
|
597 assume "y = y'" |
|
598 with 2 show ?thesis by (cases c) (simp add: app_inv2 app_inv1)+ |
|
599 next |
|
600 assume "y < y'" |
|
601 with 2 show ?thesis by (cases c) auto |
|
602 next |
|
603 assume "y' < y" |
|
604 with 2 show ?thesis by (cases c) auto |
|
605 qed |
|
606 next |
|
607 case (3 y lt z v rta y' ss bb) |
|
608 thus ?case by (cases "treec (Tr B lt z v rta) = B \<and> treec bb = B") (simp add: balleft_inv2_with_inv1 balleft_inv1 balleft_inv1l)+ |
|
609 next |
|
610 case (5 y a y' ss lt z v rta) |
|
611 thus ?case by (cases "treec a = B \<and> treec (Tr B lt z v rta) = B") (simp add: balright_inv2_with_inv1 balright_inv1 balright_inv1l)+ |
|
612 next |
|
613 case ("6_1" y a y' ss) thus ?case by (cases "treec a = B \<and> treec Empty = B") simp+ |
|
614 qed auto |
|
615 |
|
616 lemma |
|
617 delformLeft_tlt: "\<lbrakk>tlt v lt; tlt v rt; k < v\<rbrakk> \<Longrightarrow> tlt v (delformLeft x lt k y rt)" |
|
618 and delformRight_tlt: "\<lbrakk>tlt v lt; tlt v rt; k < v\<rbrakk> \<Longrightarrow> tlt v (delformRight x lt k y rt)" |
|
619 and del_tlt: "tlt v lt \<Longrightarrow> tlt v (del x lt)" |
|
620 by (induct x lt k y rt and x lt k y rt and x lt rule: delformLeft_delformRight_del.induct) |
|
621 (auto simp: balleft_tlt balright_tlt) |
|
622 |
|
623 lemma delformLeft_tgt: "\<lbrakk>tgt v lt; tgt v rt; k > v\<rbrakk> \<Longrightarrow> tgt v (delformLeft x lt k y rt)" |
|
624 and delformRight_tgt: "\<lbrakk>tgt v lt; tgt v rt; k > v\<rbrakk> \<Longrightarrow> tgt v (delformRight x lt k y rt)" |
|
625 and del_tgt: "tgt v lt \<Longrightarrow> tgt v (del x lt)" |
|
626 by (induct x lt k y rt and x lt k y rt and x lt rule: delformLeft_delformRight_del.induct) |
|
627 (auto simp: balleft_tgt balright_tgt) |
|
628 |
|
629 lemma "\<lbrakk>st lt; st rt; tlt k lt; tgt k rt\<rbrakk> \<Longrightarrow> st (delformLeft x lt k y rt)" |
|
630 and "\<lbrakk>st lt; st rt; tlt k lt; tgt k rt\<rbrakk> \<Longrightarrow> st (delformRight x lt k y rt)" |
|
631 and del_st: "st lt \<Longrightarrow> st (del x lt)" |
|
632 proof (induct x lt k y rt and x lt k y rt and x lt rule: delformLeft_delformRight_del.induct) |
|
633 case (3 x lta zz v rta yy ss bb) |
|
634 from 3 have "tlt yy (Tr B lta zz v rta)" by simp |
|
635 hence "tlt yy (del x (Tr B lta zz v rta))" by (rule del_tlt) |
|
636 with 3 show ?case by (simp add: balleft_st) |
|
637 next |
|
638 case ("4_2" x vaa vbb vdd vc yy ss bb) |
|
639 hence "tlt yy (Tr R vaa vbb vdd vc)" by simp |
|
640 hence "tlt yy (del x (Tr R vaa vbb vdd vc))" by (rule del_tlt) |
|
641 with "4_2" show ?case by simp |
|
642 next |
|
643 case (5 x aa yy ss lta zz v rta) |
|
644 hence "tgt yy (Tr B lta zz v rta)" by simp |
|
645 hence "tgt yy (del x (Tr B lta zz v rta))" by (rule del_tgt) |
|
646 with 5 show ?case by (simp add: balright_st) |
|
647 next |
|
648 case ("6_2" x aa yy ss vaa vbb vdd vc) |
|
649 hence "tgt yy (Tr R vaa vbb vdd vc)" by simp |
|
650 hence "tgt yy (del x (Tr R vaa vbb vdd vc))" by (rule del_tgt) |
|
651 with "6_2" show ?case by simp |
|
652 qed (auto simp: app_st) |
|
653 |
|
654 lemma "\<lbrakk>st lt; st rt; tlt kt lt; tgt kt rt; inv1 lt; inv1 rt; inv2 lt; inv2 rt; bh lt = bh rt; x < kt\<rbrakk> \<Longrightarrow> pin_tree k v (delformLeft x lt kt y rt) = (False \<or> (x \<noteq> k \<and> pin_tree k v (Tr c lt kt y rt)))" |
|
655 and "\<lbrakk>st lt; st rt; tlt kt lt; tgt kt rt; inv1 lt; inv1 rt; inv2 lt; inv2 rt; bh lt = bh rt; x > kt\<rbrakk> \<Longrightarrow> pin_tree k v (delformRight x lt kt y rt) = (False \<or> (x \<noteq> k \<and> pin_tree k v (Tr c lt kt y rt)))" |
|
656 and del_pit: "\<lbrakk>st t; inv1 t; inv2 t\<rbrakk> \<Longrightarrow> pin_tree k v (del x t) = (False \<or> (x \<noteq> k \<and> pin_tree k v t))" |
|
657 proof (induct x lt kt y rt and x lt kt y rt and x t rule: delformLeft_delformRight_del.induct) |
|
658 case (2 xx c aa yy ss bb) |
|
659 have "xx = yy \<or> xx < yy \<or> xx > yy" by auto |
|
660 from this 2 show ?case proof (elim disjE) |
|
661 assume "xx = yy" |
|
662 with 2 show ?thesis proof (cases "xx = k") |
|
663 case True |
|
664 from 2 `xx = yy` `xx = k` have "st (Tr c aa yy ss bb) \<and> k = yy" by simp |
|
665 hence "\<not> pin_tree k v aa" "\<not> pin_tree k v bb" by (auto simp: tlt_nit tgt_prop) |
|
666 with `xx = yy` 2 `xx = k` show ?thesis by (simp add: app_pit) |
|
667 qed (simp add: app_pit) |
|
668 qed simp+ |
|
669 next |
|
670 case (3 xx lta zz vv rta yy ss bb) |
|
671 def mt[simp]: mt == "Tr B lta zz vv rta" |
|
672 from 3 have "inv2 mt \<and> inv1 mt" by simp |
|
673 hence "inv2 (del xx mt) \<and> (treec mt = R \<and> bh (del xx mt) = bh mt \<and> inv1 (del xx mt) \<or> treec mt = B \<and> bh (del xx mt) = bh mt - 1 \<and> inv1l (del xx mt))" by (blast dest: del_inv1_inv2) |
|
674 with 3 have 4: "pin_tree k v (delformLeft xx mt yy ss bb) = (False \<or> xx \<noteq> k \<and> pin_tree k v mt \<or> (k = yy \<and> v = ss) \<or> pin_tree k v bb)" by (simp add: balleft_pit) |
|
675 thus ?case proof (cases "xx = k") |
|
676 case True |
|
677 from 3 True have "tgt yy bb \<and> yy > k" by simp |
|
678 hence "tgt k bb" by (blast dest: tgt_trans) |
|
679 with 3 4 True show ?thesis by (auto simp: tgt_nit) |
|
680 qed auto |
|
681 next |
|
682 case ("4_1" xx yy ss bb) |
|
683 show ?case proof (cases "xx = k") |
|
684 case True |
|
685 with "4_1" have "tgt yy bb \<and> k < yy" by simp |
|
686 hence "tgt k bb" by (blast dest: tgt_trans) |
|
687 with "4_1" `xx = k` |
|
688 have "pin_tree k v (Tr R Empty yy ss bb) = pin_tree k v Empty" by (auto simp: tgt_nit) |
|
689 thus ?thesis by auto |
|
690 qed simp+ |
|
691 next |
|
692 case ("4_2" xx vaa vbb vdd vc yy ss bb) |
|
693 thus ?case proof (cases "xx = k") |
|
694 case True |
|
695 with "4_2" have "k < yy \<and> tgt yy bb" by simp |
|
696 hence "tgt k bb" by (blast dest: tgt_trans) |
|
697 with True "4_2" show ?thesis by (auto simp: tgt_nit) |
|
698 qed simp |
|
699 next |
|
700 case (5 xx aa yy ss lta zz vv rta) |
|
701 def mt[simp]: mt == "Tr B lta zz vv rta" |
|
702 from 5 have "inv2 mt \<and> inv1 mt" by simp |
|
703 hence "inv2 (del xx mt) \<and> (treec mt = R \<and> bh (del xx mt) = bh mt \<and> inv1 (del xx mt) \<or> treec mt = B \<and> bh (del xx mt) = bh mt - 1 \<and> inv1l (del xx mt))" by (blast dest: del_inv1_inv2) |
|
704 with 5 have 3: "pin_tree k v (delformRight xx aa yy ss mt) = (pin_tree k v aa \<or> (k = yy \<and> v = ss) \<or> False \<or> xx \<noteq> k \<and> pin_tree k v mt)" by (simp add: balright_pit) |
|
705 thus ?case proof (cases "xx = k") |
|
706 case True |
|
707 from 5 True have "tlt yy aa \<and> yy < k" by simp |
|
708 hence "tlt k aa" by (blast dest: tlt_trans) |
|
709 with 3 5 True show ?thesis by (auto simp: tlt_nit) |
|
710 qed auto |
|
711 next |
|
712 case ("6_1" xx aa yy ss) |
|
713 show ?case proof (cases "xx = k") |
|
714 case True |
|
715 with "6_1" have "tlt yy aa \<and> k > yy" by simp |
|
716 hence "tlt k aa" by (blast dest: tlt_trans) |
|
717 with "6_1" `xx = k` show ?thesis by (auto simp: tlt_nit) |
|
718 qed simp |
|
719 next |
|
720 case ("6_2" xx aa yy ss vaa vbb vdd vc) |
|
721 thus ?case proof (cases "xx = k") |
|
722 case True |
|
723 with "6_2" have "k > yy \<and> tlt yy aa" by simp |
|
724 hence "tlt k aa" by (blast dest: tlt_trans) |
|
725 with True "6_2" show ?thesis by (auto simp: tlt_nit) |
|
726 qed simp |
|
727 qed simp |
|
728 |
|
729 |
|
730 definition delete where |
|
731 delete_def: "delete k t = paint B (del k t)" |
|
732 |
|
733 theorem delete_isrbt[simp]: assumes "isrbt t" shows "isrbt (delete k t)" |
|
734 proof - |
|
735 from assms have "inv2 t" and "inv1 t" unfolding isrbt_def by auto |
|
736 hence "inv2 (del k t) \<and> (treec t = R \<and> bh (del k t) = bh t \<and> inv1 (del k t) \<or> treec t = B \<and> bh (del k t) = bh t - 1 \<and> inv1l (del k t))" by (rule del_inv1_inv2) |
|
737 hence "inv2 (del k t) \<and> inv1l (del k t)" by (cases "treec t") auto |
|
738 with assms show ?thesis |
|
739 unfolding isrbt_def delete_def |
|
740 by (auto intro: paint_st del_st) |
|
741 qed |
|
742 |
|
743 lemma delete_pit: |
|
744 assumes "isrbt t" |
|
745 shows "pin_tree k v (delete x t) = (x \<noteq> k \<and> pin_tree k v t)" |
|
746 using assms unfolding isrbt_def delete_def |
|
747 by (auto simp: del_pit) |
|
748 |
|
749 lemma map_of_delete: |
|
750 assumes isrbt: "isrbt t" |
|
751 shows "map_of (delete k t) = (map_of t)|`(-{k})" |
|
752 proof |
|
753 fix x |
|
754 show "map_of (delete k t) x = (map_of t |` (-{k})) x" |
|
755 proof (cases "x = k") |
|
756 assume "x = k" |
|
757 with isrbt show ?thesis |
|
758 by (cases "map_of (delete k t) k") (auto simp: mapof_pit delete_pit) |
|
759 next |
|
760 assume "x \<noteq> k" |
|
761 thus ?thesis |
|
762 by auto (metis isrbt delete_isrbt delete_pit isrbt_st mapof_from_pit) |
|
763 qed |
|
764 qed |
|
765 |
|
766 subsection {* Union *} |
|
767 |
|
768 primrec |
|
769 unionwithkey :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" |
|
770 where |
|
771 "unionwithkey f t Empty = t" |
|
772 | "unionwithkey f t (Tr c lt k v rt) = unionwithkey f (unionwithkey f (insertwithkey f k v t) lt) rt" |
|
773 |
|
774 lemma unionwk_st: "st lt \<Longrightarrow> st (unionwithkey f lt rt)" |
|
775 by (induct rt arbitrary: lt) (auto simp: insertwk_st) |
|
776 theorem unionwk_isrbt[simp]: "isrbt lt \<Longrightarrow> isrbt (unionwithkey f lt rt)" |
|
777 by (induct rt arbitrary: lt) (simp add: insertwk_isrbt)+ |
|
778 |
|
779 definition |
|
780 unionwith where |
|
781 "unionwith f = unionwithkey (\<lambda>_. f)" |
|
782 |
|
783 theorem unionw_isrbt: "isrbt lt \<Longrightarrow> isrbt (unionwith f lt rt)" unfolding unionwith_def by simp |
|
784 |
|
785 definition union where |
|
786 "union = unionwithkey (%_ _ rv. rv)" |
|
787 |
|
788 theorem union_isrbt: "isrbt lt \<Longrightarrow> isrbt (union lt rt)" unfolding union_def by simp |
|
789 |
|
790 lemma union_Tr[simp]: |
|
791 "union t (Tr c lt k v rt) = union (union (insrt k v t) lt) rt" |
|
792 unfolding union_def insrt_def |
|
793 by simp |
|
794 |
|
795 lemma map_of_union: |
|
796 assumes "isrbt s" "st t" |
|
797 shows "map_of (union s t) = map_of s ++ map_of t" |
|
798 using assms |
|
799 proof (induct t arbitrary: s) |
|
800 case Empty thus ?case by (auto simp: union_def) |
|
801 next |
|
802 case (Tr c l k v r s) |
|
803 hence strl: "st r" "st l" "l |\<guillemotleft> k" "k \<guillemotleft>| r" by auto |
|
804 |
|
805 have meq: "map_of s(k \<mapsto> v) ++ map_of l ++ map_of r = |
|
806 map_of s ++ |
|
807 (\<lambda>a. if a < k then map_of l a |
|
808 else if k < a then map_of r a else Some v)" (is "?m1 = ?m2") |
|
809 proof (rule ext) |
|
810 fix a |
|
811 |
|
812 have "k < a \<or> k = a \<or> k > a" by auto |
|
813 thus "?m1 a = ?m2 a" |
|
814 proof (elim disjE) |
|
815 assume "k < a" |
|
816 with `l |\<guillemotleft> k` have "l |\<guillemotleft> a" by (rule tlt_trans) |
|
817 with `k < a` show ?thesis |
|
818 by (auto simp: map_add_def split: option.splits) |
|
819 next |
|
820 assume "k = a" |
|
821 with `l |\<guillemotleft> k` `k \<guillemotleft>| r` |
|
822 show ?thesis by (auto simp: map_add_def) |
|
823 next |
|
824 assume "a < k" |
|
825 from this `k \<guillemotleft>| r` have "a \<guillemotleft>| r" by (rule tgt_trans) |
|
826 with `a < k` show ?thesis |
|
827 by (auto simp: map_add_def split: option.splits) |
|
828 qed |
|
829 qed |
|
830 |
|
831 from Tr |
|
832 have IHs: |
|
833 "map_of (union (union (insrt k v s) l) r) = map_of (union (insrt k v s) l) ++ map_of r" |
|
834 "map_of (union (insrt k v s) l) = map_of (insrt k v s) ++ map_of l" |
|
835 by (auto intro: union_isrbt insrt_isrbt) |
|
836 |
|
837 with meq show ?case |
|
838 by (auto simp: map_of_insert[OF Tr(3)]) |
|
839 qed |
|
840 |
|
841 subsection {* Adjust *} |
|
842 |
|
843 primrec |
|
844 adjustwithkey :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" |
|
845 where |
|
846 "adjustwithkey f k Empty = Empty" |
|
847 | "adjustwithkey f k (Tr c lt x v rt) = (if k < x then (Tr c (adjustwithkey f k lt) x v rt) else if k > x then (Tr c lt x v (adjustwithkey f k rt)) else (Tr c lt x (f x v) rt))" |
|
848 |
|
849 lemma adjustwk_treec: "treec (adjustwithkey f k t) = treec t" by (induct t) simp+ |
|
850 lemma adjustwk_inv1: "inv1 (adjustwithkey f k t) = inv1 t" by (induct t) (simp add: adjustwk_treec)+ |
|
851 lemma adjustwk_inv2: "inv2 (adjustwithkey f k t) = inv2 t" "bh (adjustwithkey f k t) = bh t" by (induct t) simp+ |
|
852 lemma adjustwk_tgt: "tgt k (adjustwithkey f kk t) = tgt k t" by (induct t) simp+ |
|
853 lemma adjustwk_tlt: "tlt k (adjustwithkey f kk t) = tlt k t" by (induct t) simp+ |
|
854 lemma adjustwk_st: "st (adjustwithkey f k t) = st t" by (induct t) (simp add: adjustwk_tlt adjustwk_tgt)+ |
|
855 |
|
856 theorem adjustwk_isrbt[simp]: "isrbt (adjustwithkey f k t) = isrbt t" |
|
857 unfolding isrbt_def by (simp add: adjustwk_inv2 adjustwk_treec adjustwk_st adjustwk_inv1 ) |
|
858 |
|
859 theorem adjustwithkey_map[simp]: |
|
860 "map_of (adjustwithkey f k t) x = |
|
861 (if x = k then case map_of t x of None \<Rightarrow> None | Some y \<Rightarrow> Some (f k y) |
|
862 else map_of t x)" |
|
863 by (induct t arbitrary: x) (auto split:option.splits) |
|
864 |
|
865 definition adjust where |
|
866 "adjust f = adjustwithkey (\<lambda>_. f)" |
|
867 |
|
868 theorem adjust_isrbt[simp]: "isrbt (adjust f k t) = isrbt t" unfolding adjust_def by simp |
|
869 |
|
870 theorem adjust_map[simp]: |
|
871 "map_of (adjust f k t) x = |
|
872 (if x = k then case map_of t x of None \<Rightarrow> None | Some y \<Rightarrow> Some (f y) |
|
873 else map_of t x)" |
|
874 unfolding adjust_def by simp |
|
875 |
|
876 subsection {* Map *} |
|
877 |
|
878 primrec |
|
879 mapwithkey :: "('a::linorder \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'c) rbt" |
|
880 where |
|
881 "mapwithkey f Empty = Empty" |
|
882 | "mapwithkey f (Tr c lt k v rt) = Tr c (mapwithkey f lt) k (f k v) (mapwithkey f rt)" |
|
883 |
|
884 theorem mapwk_keys[simp]: "keys (mapwithkey f t) = keys t" by (induct t) auto |
|
885 lemma mapwk_tgt: "tgt k (mapwithkey f t) = tgt k t" by (induct t) simp+ |
|
886 lemma mapwk_tlt: "tlt k (mapwithkey f t) = tlt k t" by (induct t) simp+ |
|
887 lemma mapwk_st: "st (mapwithkey f t) = st t" by (induct t) (simp add: mapwk_tlt mapwk_tgt)+ |
|
888 lemma mapwk_treec: "treec (mapwithkey f t) = treec t" by (induct t) simp+ |
|
889 lemma mapwk_inv1: "inv1 (mapwithkey f t) = inv1 t" by (induct t) (simp add: mapwk_treec)+ |
|
890 lemma mapwk_inv2: "inv2 (mapwithkey f t) = inv2 t" "bh (mapwithkey f t) = bh t" by (induct t) simp+ |
|
891 theorem mapwk_isrbt[simp]: "isrbt (mapwithkey f t) = isrbt t" |
|
892 unfolding isrbt_def by (simp add: mapwk_inv1 mapwk_inv2 mapwk_st mapwk_treec) |
|
893 |
|
894 theorem map_of_mapwk[simp]: "map_of (mapwithkey f t) x = option_map (f x) (map_of t x)" |
|
895 by (induct t) auto |
|
896 |
|
897 definition map |
|
898 where map_def: "map f == mapwithkey (\<lambda>_. f)" |
|
899 |
|
900 theorem map_keys[simp]: "keys (map f t) = keys t" unfolding map_def by simp |
|
901 theorem map_isrbt[simp]: "isrbt (map f t) = isrbt t" unfolding map_def by simp |
|
902 theorem map_of_map[simp]: "map_of (map f t) = option_map f o map_of t" |
|
903 by (rule ext) (simp add:map_def) |
|
904 |
|
905 subsection {* Fold *} |
|
906 |
|
907 text {* The following is still incomplete... *} |
|
908 |
|
909 primrec |
|
910 foldwithkey :: "('a::linorder \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" |
|
911 where |
|
912 "foldwithkey f Empty v = v" |
|
913 | "foldwithkey f (Tr c lt k x rt) v = foldwithkey f rt (f k x (foldwithkey f lt v))" |
|
914 |
|
915 primrec alist_of |
|
916 where |
|
917 "alist_of Empty = []" |
|
918 | "alist_of (Tr _ l k v r) = alist_of l @ (k,v) # alist_of r" |
|
919 |
|
920 lemma map_of_alist_of: |
|
921 shows "st t \<Longrightarrow> Map.map_of (alist_of t) = map_of t" |
|
922 oops |
|
923 |
|
924 lemma fold_alist_fold: |
|
925 "foldwithkey f t x = foldl (\<lambda>x (k,v). f k v x) x (alist_of t)" |
|
926 by (induct t arbitrary: x) auto |
|
927 |
|
928 lemma alist_pit[simp]: "(k, v) \<in> set (alist_of t) = pin_tree k v t" |
|
929 by (induct t) auto |
|
930 |
|
931 lemma sorted_alist: |
|
932 "st t \<Longrightarrow> sorted (List.map fst (alist_of t))" |
|
933 by (induct t) |
|
934 (force simp: sorted_append sorted_Cons tlgt_props |
|
935 dest!:pint_keys)+ |
|
936 |
|
937 lemma distinct_alist: |
|
938 "st t \<Longrightarrow> distinct (List.map fst (alist_of t))" |
|
939 by (induct t) |
|
940 (force simp: sorted_append sorted_Cons tlgt_props |
|
941 dest!:pint_keys)+ |
|
942 (*>*) |
|
943 |
|
944 text {* |
|
945 This theory defines purely functional red-black trees which can be |
|
946 used as an efficient representation of finite maps. |
|
947 *} |
|
948 |
|
949 subsection {* Data type and invariant *} |
|
950 |
|
951 text {* |
|
952 The type @{typ "('k, 'v) rbt"} denotes red-black trees with keys of |
|
953 type @{typ "'k"} and values of type @{typ "'v"}. To function |
|
954 properly, the key type must belong to the @{text "linorder"} class. |
|
955 |
|
956 A value @{term t} of this type is a valid red-black tree if it |
|
957 satisfies the invariant @{text "isrbt t"}. |
|
958 This theory provides lemmas to prove that the invariant is |
|
959 satisfied throughout the computation. |
|
960 |
|
961 The interpretation function @{const "map_of"} returns the partial |
|
962 map represented by a red-black tree: |
|
963 @{term_type[display] "map_of"} |
|
964 |
|
965 This function should be used for reasoning about the semantics of the RBT |
|
966 operations. Furthermore, it implements the lookup functionality for |
|
967 the data structure: It is executable and the lookup is performed in |
|
968 $O(\log n)$. |
|
969 *} |
|
970 |
|
971 subsection {* Operations *} |
|
972 |
|
973 text {* |
|
974 Currently, the following operations are supported: |
|
975 |
|
976 @{term_type[display] "Empty"} |
|
977 Returns the empty tree. $O(1)$ |
|
978 |
|
979 @{term_type[display] "insrt"} |
|
980 Updates the map at a given position. $O(\log n)$ |
|
981 |
|
982 @{term_type[display] "delete"} |
|
983 Deletes a map entry at a given position. $O(\log n)$ |
|
984 |
|
985 @{term_type[display] "union"} |
|
986 Forms the union of two trees, preferring entries from the first one. |
|
987 |
|
988 @{term_type[display] "map"} |
|
989 Maps a function over the values of a map. $O(n)$ |
|
990 *} |
|
991 |
|
992 |
|
993 subsection {* Invariant preservation *} |
|
994 |
|
995 text {* |
|
996 \noindent |
|
997 @{thm Empty_isrbt}\hfill(@{text "Empty_isrbt"}) |
|
998 |
|
999 \noindent |
|
1000 @{thm insrt_isrbt}\hfill(@{text "insrt_isrbt"}) |
|
1001 |
|
1002 \noindent |
|
1003 @{thm delete_isrbt}\hfill(@{text "delete_isrbt"}) |
|
1004 |
|
1005 \noindent |
|
1006 @{thm union_isrbt}\hfill(@{text "union_isrbt"}) |
|
1007 |
|
1008 \noindent |
|
1009 @{thm map_isrbt}\hfill(@{text "map_isrbt"}) |
|
1010 *} |
|
1011 |
|
1012 subsection {* Map Semantics *} |
|
1013 |
|
1014 text {* |
|
1015 \noindent |
|
1016 \underline{@{text "map_of_Empty"}} |
|
1017 @{thm[display] map_of_Empty} |
|
1018 \vspace{1ex} |
|
1019 |
|
1020 \noindent |
|
1021 \underline{@{text "map_of_insert"}} |
|
1022 @{thm[display] map_of_insert} |
|
1023 \vspace{1ex} |
|
1024 |
|
1025 \noindent |
|
1026 \underline{@{text "map_of_delete"}} |
|
1027 @{thm[display] map_of_delete} |
|
1028 \vspace{1ex} |
|
1029 |
|
1030 \noindent |
|
1031 \underline{@{text "map_of_union"}} |
|
1032 @{thm[display] map_of_union} |
|
1033 \vspace{1ex} |
|
1034 |
|
1035 \noindent |
|
1036 \underline{@{text "map_of_map"}} |
|
1037 @{thm[display] map_of_map} |
|
1038 \vspace{1ex} |
|
1039 *} |
|
1040 |
|
1041 end |