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