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