author  wenzelm 
Sun, 13 Mar 2011 22:55:50 +0100  
changeset 41959  b460124855b8 
parent 41074  286255f131bf 
child 45990  b7b905b23b2a 
permissions  rwrr 
41959  1 
(* Title: HOL/Library/RBT_Impl.thy 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

2 
Author: Markus Reiter, TU Muenchen 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

3 
Author: Alexander Krauss, TU Muenchen 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

4 
*) 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

5 

36147
b43b22f63665
theory RBT with abstract type of redblack trees backed by implementation RBT_Impl
haftmann
parents:
35618
diff
changeset

6 
header {* Implementation of RedBlack Trees *} 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

7 

36147
b43b22f63665
theory RBT with abstract type of redblack trees backed by implementation RBT_Impl
haftmann
parents:
35618
diff
changeset

8 
theory RBT_Impl 
37458  9 
imports Main More_List 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

10 
begin 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

11 

36147
b43b22f63665
theory RBT with abstract type of redblack trees backed by implementation RBT_Impl
haftmann
parents:
35618
diff
changeset

12 
text {* 
b43b22f63665
theory RBT with abstract type of redblack trees backed by implementation RBT_Impl
haftmann
parents:
35618
diff
changeset

13 
For applications, you should use theory @{text RBT} which defines 
b43b22f63665
theory RBT with abstract type of redblack trees backed by implementation RBT_Impl
haftmann
parents:
35618
diff
changeset

14 
an abstract type of redblack tree obeying the invariant. 
b43b22f63665
theory RBT with abstract type of redblack trees backed by implementation RBT_Impl
haftmann
parents:
35618
diff
changeset

15 
*} 
b43b22f63665
theory RBT with abstract type of redblack trees backed by implementation RBT_Impl
haftmann
parents:
35618
diff
changeset

16 

35550  17 
subsection {* Datatype of RB trees *} 
18 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

19 
datatype color = R  B 
35534  20 
datatype ('a, 'b) rbt = Empty  Branch color "('a, 'b) rbt" 'a 'b "('a, 'b) rbt" 
21 

22 
lemma rbt_cases: 

23 
obtains (Empty) "t = Empty" 

24 
 (Red) l k v r where "t = Branch R l k v r" 

25 
 (Black) l k v r where "t = Branch B l k v r" 

26 
proof (cases t) 

27 
case Empty with that show thesis by blast 

28 
next 

29 
case (Branch c) with that show thesis by (cases c) blast+ 

30 
qed 

31 

35550  32 
subsection {* Tree properties *} 
35534  33 

35550  34 
subsubsection {* Content of a tree *} 
35 

36 
primrec entries :: "('a, 'b) rbt \<Rightarrow> ('a \<times> 'b) list" 

35534  37 
where 
38 
"entries Empty = []" 

39 
 "entries (Branch _ l k v r) = entries l @ (k,v) # entries r" 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

40 

35550  41 
abbreviation (input) entry_in_tree :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

42 
where 
35550  43 
"entry_in_tree k v t \<equiv> (k, v) \<in> set (entries t)" 
44 

45 
definition keys :: "('a, 'b) rbt \<Rightarrow> 'a list" where 

46 
"keys t = map fst (entries t)" 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

47 

35550  48 
lemma keys_simps [simp, code]: 
49 
"keys Empty = []" 

50 
"keys (Branch c l k v r) = keys l @ k # keys r" 

51 
by (simp_all add: keys_def) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

52 

35534  53 
lemma entry_in_tree_keys: 
35550  54 
assumes "(k, v) \<in> set (entries t)" 
55 
shows "k \<in> set (keys t)" 

56 
proof  

57 
from assms have "fst (k, v) \<in> fst ` set (entries t)" by (rule imageI) 

58 
then show ?thesis by (simp add: keys_def) 

59 
qed 

60 

35602  61 
lemma keys_entries: 
62 
"k \<in> set (keys t) \<longleftrightarrow> (\<exists>v. (k, v) \<in> set (entries t))" 

63 
by (auto intro: entry_in_tree_keys) (auto simp add: keys_def) 

64 

35550  65 

66 
subsubsection {* Search tree properties *} 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

67 

35534  68 
definition tree_less :: "'a\<Colon>order \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

69 
where 
35550  70 
tree_less_prop: "tree_less k t \<longleftrightarrow> (\<forall>x\<in>set (keys t). x < k)" 
35534  71 

72 
abbreviation tree_less_symbol (infix "\<guillemotleft>" 50) 

73 
where "t \<guillemotleft> x \<equiv> tree_less x t" 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

74 

35534  75 
definition tree_greater :: "'a\<Colon>order \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool" (infix "\<guillemotleft>" 50) 
76 
where 

35550  77 
tree_greater_prop: "tree_greater k t = (\<forall>x\<in>set (keys t). k < x)" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

78 

35534  79 
lemma tree_less_simps [simp]: 
80 
"tree_less k Empty = True" 

81 
"tree_less k (Branch c lt kt v rt) \<longleftrightarrow> kt < k \<and> tree_less k lt \<and> tree_less k rt" 

82 
by (auto simp add: tree_less_prop) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

83 

35534  84 
lemma tree_greater_simps [simp]: 
85 
"tree_greater k Empty = True" 

86 
"tree_greater k (Branch c lt kt v rt) \<longleftrightarrow> k < kt \<and> tree_greater k lt \<and> tree_greater k rt" 

87 
by (auto simp add: tree_greater_prop) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

88 

35534  89 
lemmas tree_ord_props = tree_less_prop tree_greater_prop 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

90 

35534  91 
lemmas tree_greater_nit = tree_greater_prop entry_in_tree_keys 
92 
lemmas tree_less_nit = tree_less_prop entry_in_tree_keys 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

93 

35550  94 
lemma tree_less_eq_trans: "l \<guillemotleft> u \<Longrightarrow> u \<le> v \<Longrightarrow> l \<guillemotleft> v" 
95 
and tree_less_trans: "t \<guillemotleft> x \<Longrightarrow> x < y \<Longrightarrow> t \<guillemotleft> y" 

96 
and tree_greater_eq_trans: "u \<le> v \<Longrightarrow> v \<guillemotleft> r \<Longrightarrow> u \<guillemotleft> r" 

35534  97 
and tree_greater_trans: "x < y \<Longrightarrow> y \<guillemotleft> t \<Longrightarrow> x \<guillemotleft> t" 
35550  98 
by (auto simp: tree_ord_props) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

99 

35534  100 
primrec sorted :: "('a::linorder, 'b) rbt \<Rightarrow> bool" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

101 
where 
35534  102 
"sorted Empty = True" 
103 
 "sorted (Branch c l k v r) = (l \<guillemotleft> k \<and> k \<guillemotleft> r \<and> sorted l \<and> sorted r)" 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

104 

35550  105 
lemma sorted_entries: 
106 
"sorted t \<Longrightarrow> List.sorted (List.map fst (entries t))" 

107 
by (induct t) 

108 
(force simp: sorted_append sorted_Cons tree_ord_props 

109 
dest!: entry_in_tree_keys)+ 

110 

111 
lemma distinct_entries: 

112 
"sorted t \<Longrightarrow> distinct (List.map fst (entries t))" 

113 
by (induct t) 

114 
(force simp: sorted_append sorted_Cons tree_ord_props 

115 
dest!: entry_in_tree_keys)+ 

116 

117 

118 
subsubsection {* Tree lookup *} 

119 

35534  120 
primrec lookup :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" 
121 
where 

122 
"lookup Empty k = None" 

123 
 "lookup (Branch _ l x y r) k = (if k < x then lookup l k else if x < k then lookup r k else Some y)" 

124 

35550  125 
lemma lookup_keys: "sorted t \<Longrightarrow> dom (lookup t) = set (keys t)" 
126 
by (induct t) (auto simp: dom_def tree_greater_prop tree_less_prop) 

127 

128 
lemma dom_lookup_Branch: 

129 
"sorted (Branch c t1 k v t2) \<Longrightarrow> 

130 
dom (lookup (Branch c t1 k v t2)) 

131 
= Set.insert k (dom (lookup t1) \<union> dom (lookup t2))" 

132 
proof  

133 
assume "sorted (Branch c t1 k v t2)" 

134 
moreover from this have "sorted t1" "sorted t2" by simp_all 

135 
ultimately show ?thesis by (simp add: lookup_keys) 

136 
qed 

137 

138 
lemma finite_dom_lookup [simp, intro!]: "finite (dom (lookup t))" 

139 
proof (induct t) 

140 
case Empty then show ?case by simp 

141 
next 

142 
case (Branch color t1 a b t2) 

143 
let ?A = "Set.insert a (dom (lookup t1) \<union> dom (lookup t2))" 

144 
have "dom (lookup (Branch color t1 a b t2)) \<subseteq> ?A" by (auto split: split_if_asm) 

145 
moreover from Branch have "finite (insert a (dom (lookup t1) \<union> dom (lookup t2)))" by simp 

146 
ultimately show ?case by (rule finite_subset) 

147 
qed 

148 

35534  149 
lemma lookup_tree_less[simp]: "t \<guillemotleft> k \<Longrightarrow> lookup t k = None" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

150 
by (induct t) auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

151 

35534  152 
lemma lookup_tree_greater[simp]: "k \<guillemotleft> t \<Longrightarrow> lookup t k = None" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

153 
by (induct t) auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

154 

35534  155 
lemma lookup_Empty: "lookup Empty = empty" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

156 
by (rule ext) simp 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

157 

35618  158 
lemma map_of_entries: 
159 
"sorted t \<Longrightarrow> map_of (entries t) = lookup t" 

35550  160 
proof (induct t) 
161 
case Empty thus ?case by (simp add: lookup_Empty) 

162 
next 

163 
case (Branch c t1 k v t2) 

164 
have "lookup (Branch c t1 k v t2) = lookup t2 ++ [k\<mapsto>v] ++ lookup t1" 

165 
proof (rule ext) 

166 
fix x 

167 
from Branch have SORTED: "sorted (Branch c t1 k v t2)" by simp 

168 
let ?thesis = "lookup (Branch c t1 k v t2) x = (lookup t2 ++ [k \<mapsto> v] ++ lookup t1) x" 

169 

170 
have DOM_T1: "!!k'. k'\<in>dom (lookup t1) \<Longrightarrow> k>k'" 

171 
proof  

172 
fix k' 

173 
from SORTED have "t1 \<guillemotleft> k" by simp 

174 
with tree_less_prop have "\<forall>k'\<in>set (keys t1). k>k'" by auto 

175 
moreover assume "k'\<in>dom (lookup t1)" 

176 
ultimately show "k>k'" using lookup_keys SORTED by auto 

177 
qed 

178 

179 
have DOM_T2: "!!k'. k'\<in>dom (lookup t2) \<Longrightarrow> k<k'" 

180 
proof  

181 
fix k' 

182 
from SORTED have "k \<guillemotleft> t2" by simp 

183 
with tree_greater_prop have "\<forall>k'\<in>set (keys t2). k<k'" by auto 

184 
moreover assume "k'\<in>dom (lookup t2)" 

185 
ultimately show "k<k'" using lookup_keys SORTED by auto 

186 
qed 

187 

188 
{ 

189 
assume C: "x<k" 

190 
hence "lookup (Branch c t1 k v t2) x = lookup t1 x" by simp 

191 
moreover from C have "x\<notin>dom [k\<mapsto>v]" by simp 

192 
moreover have "x\<notin>dom (lookup t2)" proof 

193 
assume "x\<in>dom (lookup t2)" 

194 
with DOM_T2 have "k<x" by blast 

195 
with C show False by simp 

196 
qed 

197 
ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps) 

198 
} moreover { 

199 
assume [simp]: "x=k" 

200 
hence "lookup (Branch c t1 k v t2) x = [k \<mapsto> v] x" by simp 

201 
moreover have "x\<notin>dom (lookup t1)" proof 

202 
assume "x\<in>dom (lookup t1)" 

203 
with DOM_T1 have "k>x" by blast 

204 
thus False by simp 

205 
qed 

206 
ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps) 

207 
} moreover { 

208 
assume C: "x>k" 

209 
hence "lookup (Branch c t1 k v t2) x = lookup t2 x" by (simp add: less_not_sym[of k x]) 

210 
moreover from C have "x\<notin>dom [k\<mapsto>v]" by simp 

211 
moreover have "x\<notin>dom (lookup t1)" proof 

212 
assume "x\<in>dom (lookup t1)" 

213 
with DOM_T1 have "k>x" by simp 

214 
with C show False by simp 

215 
qed 

216 
ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps) 

217 
} ultimately show ?thesis using less_linear by blast 

218 
qed 

219 
also from Branch have "lookup t2 ++ [k \<mapsto> v] ++ lookup t1 = map_of (entries (Branch c t1 k v t2))" by simp 

35618  220 
finally show ?case by simp 
35550  221 
qed 
222 

35602  223 
lemma lookup_in_tree: "sorted t \<Longrightarrow> lookup t k = Some v \<longleftrightarrow> (k, v) \<in> set (entries t)" 
35618  224 
by (simp add: map_of_entries [symmetric] distinct_entries) 
35602  225 

226 
lemma set_entries_inject: 

227 
assumes sorted: "sorted t1" "sorted t2" 

228 
shows "set (entries t1) = set (entries t2) \<longleftrightarrow> entries t1 = entries t2" 

229 
proof  

230 
from sorted have "distinct (map fst (entries t1))" 

231 
"distinct (map fst (entries t2))" 

232 
by (auto intro: distinct_entries) 

233 
with sorted show ?thesis 

234 
by (auto intro: map_sorted_distinct_set_unique sorted_entries simp add: distinct_map) 

235 
qed 

35550  236 

237 
lemma entries_eqI: 

238 
assumes sorted: "sorted t1" "sorted t2" 

239 
assumes lookup: "lookup t1 = lookup t2" 

35602  240 
shows "entries t1 = entries t2" 
35550  241 
proof  
242 
from sorted lookup have "map_of (entries t1) = map_of (entries t2)" 

35618  243 
by (simp add: map_of_entries) 
35602  244 
with sorted have "set (entries t1) = set (entries t2)" 
245 
by (simp add: map_of_inject_set distinct_entries) 

246 
with sorted show ?thesis by (simp add: set_entries_inject) 

247 
qed 

35550  248 

35602  249 
lemma entries_lookup: 
250 
assumes "sorted t1" "sorted t2" 

251 
shows "entries t1 = entries t2 \<longleftrightarrow> lookup t1 = lookup t2" 

35618  252 
using assms by (auto intro: entries_eqI simp add: map_of_entries [symmetric]) 
35602  253 

35550  254 
lemma lookup_from_in_tree: 
35602  255 
assumes "sorted t1" "sorted t2" 
256 
and "\<And>v. (k\<Colon>'a\<Colon>linorder, v) \<in> set (entries t1) \<longleftrightarrow> (k, v) \<in> set (entries t2)" 

35534  257 
shows "lookup t1 k = lookup t2 k" 
35602  258 
proof  
259 
from assms have "k \<in> dom (lookup t1) \<longleftrightarrow> k \<in> dom (lookup t2)" 

260 
by (simp add: keys_entries lookup_keys) 

261 
with assms show ?thesis by (auto simp add: lookup_in_tree [symmetric]) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

262 
qed 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

263 

35550  264 

265 
subsubsection {* Redblack properties *} 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

266 

35534  267 
primrec color_of :: "('a, 'b) rbt \<Rightarrow> color" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

268 
where 
35534  269 
"color_of Empty = B" 
270 
 "color_of (Branch c _ _ _ _) = c" 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

271 

35534  272 
primrec bheight :: "('a,'b) rbt \<Rightarrow> nat" 
273 
where 

274 
"bheight Empty = 0" 

275 
 "bheight (Branch c lt k v rt) = (if c = B then Suc (bheight lt) else bheight lt)" 

276 

277 
primrec inv1 :: "('a, 'b) rbt \<Rightarrow> bool" 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

278 
where 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

279 
"inv1 Empty = True" 
35534  280 
 "inv1 (Branch c lt k v rt) \<longleftrightarrow> inv1 lt \<and> inv1 rt \<and> (c = B \<or> color_of lt = B \<and> color_of rt = B)" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

281 

35534  282 
primrec inv1l :: "('a, 'b) rbt \<Rightarrow> bool"  {* Weaker version *} 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

283 
where 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

284 
"inv1l Empty = True" 
35534  285 
 "inv1l (Branch c l k v r) = (inv1 l \<and> inv1 r)" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

286 
lemma [simp]: "inv1 t \<Longrightarrow> inv1l t" by (cases t) simp+ 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

287 

35534  288 
primrec inv2 :: "('a, 'b) rbt \<Rightarrow> bool" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

289 
where 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

290 
"inv2 Empty = True" 
35534  291 
 "inv2 (Branch c lt k v rt) = (inv2 lt \<and> inv2 rt \<and> bheight lt = bheight rt)" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

292 

35534  293 
definition is_rbt :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> bool" where 
294 
"is_rbt t \<longleftrightarrow> inv1 t \<and> inv2 t \<and> color_of t = B \<and> sorted t" 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

295 

35534  296 
lemma is_rbt_sorted [simp]: 
297 
"is_rbt t \<Longrightarrow> sorted t" by (simp add: is_rbt_def) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

298 

35534  299 
theorem Empty_is_rbt [simp]: 
300 
"is_rbt Empty" by (simp add: is_rbt_def) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

301 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

302 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

303 
subsection {* Insertion *} 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

304 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

305 
fun (* slow, due to massive case splitting *) 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

306 
balance :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

307 
where 
35534  308 
"balance (Branch R a w x b) s t (Branch R c y z d) = Branch R (Branch B a w x b) s t (Branch B c y z d)"  
309 
"balance (Branch R (Branch R a w x b) s t c) y z d = Branch R (Branch B a w x b) s t (Branch B c y z d)"  

310 
"balance (Branch R a w x (Branch R b s t c)) y z d = Branch R (Branch B a w x b) s t (Branch B c y z d)"  

311 
"balance a w x (Branch R b s t (Branch R c y z d)) = Branch R (Branch B a w x b) s t (Branch B c y z d)"  

312 
"balance a w x (Branch R (Branch R b s t c) y z d) = Branch R (Branch B a w x b) s t (Branch B c y z d)"  

313 
"balance a s t b = Branch B a s t b" 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

314 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

315 
lemma balance_inv1: "\<lbrakk>inv1l l; inv1l r\<rbrakk> \<Longrightarrow> inv1 (balance l k v r)" 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

316 
by (induct l k v r rule: balance.induct) auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

317 

35534  318 
lemma balance_bheight: "bheight l = bheight r \<Longrightarrow> bheight (balance l k v r) = Suc (bheight l)" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

319 
by (induct l k v r rule: balance.induct) auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

320 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

321 
lemma balance_inv2: 
35534  322 
assumes "inv2 l" "inv2 r" "bheight l = bheight r" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

323 
shows "inv2 (balance l k v r)" 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

324 
using assms 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

325 
by (induct l k v r rule: balance.induct) auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

326 

35534  327 
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 redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

328 
by (induct a k x b rule: balance.induct) auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

329 

35534  330 
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 redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

331 
by (induct a k x b rule: balance.induct) auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

332 

35534  333 
lemma balance_sorted: 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

334 
fixes k :: "'a::linorder" 
35534  335 
assumes "sorted l" "sorted r" "l \<guillemotleft> k" "k \<guillemotleft> r" 
336 
shows "sorted (balance l k v r)" 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

337 
using assms proof (induct l k v r rule: balance.induct) 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

338 
case ("2_2" a x w b y t c z s va vb vd vc) 
35534  339 
hence "y < z \<and> z \<guillemotleft> Branch B va vb vd vc" 
340 
by (auto simp add: tree_ord_props) 

341 
hence "tree_greater y (Branch B va vb vd vc)" by (blast dest: tree_greater_trans) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

342 
with "2_2" show ?case by simp 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

343 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

344 
case ("3_2" va vb vd vc x w b y s c z) 
35534  345 
from "3_2" have "x < y \<and> tree_less x (Branch B va vb vd vc)" 
346 
by simp 

347 
hence "tree_less y (Branch B va vb vd vc)" by (blast dest: tree_less_trans) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

348 
with "3_2" show ?case by simp 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

349 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

350 
case ("3_3" x w b y s c z t va vb vd vc) 
35534  351 
from "3_3" have "y < z \<and> tree_greater z (Branch B va vb vd vc)" by simp 
352 
hence "tree_greater y (Branch B va vb vd vc)" by (blast dest: tree_greater_trans) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

353 
with "3_3" show ?case by simp 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

354 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

355 
case ("3_4" vd ve vg vf x w b y s c z t va vb vii vc) 
35534  356 
hence "x < y \<and> tree_less x (Branch B vd ve vg vf)" by simp 
357 
hence 1: "tree_less y (Branch B vd ve vg vf)" by (blast dest: tree_less_trans) 

358 
from "3_4" have "y < z \<and> tree_greater z (Branch B va vb vii vc)" by simp 

359 
hence "tree_greater y (Branch B va vb vii vc)" by (blast dest: tree_greater_trans) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

360 
with 1 "3_4" show ?case by simp 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

361 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

362 
case ("4_2" va vb vd vc x w b y s c z t dd) 
35534  363 
hence "x < y \<and> tree_less x (Branch B va vb vd vc)" by simp 
364 
hence "tree_less y (Branch B va vb vd vc)" by (blast dest: tree_less_trans) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

365 
with "4_2" show ?case by simp 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

366 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

367 
case ("5_2" x w b y s c z t va vb vd vc) 
35534  368 
hence "y < z \<and> tree_greater z (Branch B va vb vd vc)" by simp 
369 
hence "tree_greater y (Branch B va vb vd vc)" by (blast dest: tree_greater_trans) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

370 
with "5_2" show ?case by simp 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

371 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

372 
case ("5_3" va vb vd vc x w b y s c z t) 
35534  373 
hence "x < y \<and> tree_less x (Branch B va vb vd vc)" by simp 
374 
hence "tree_less y (Branch B va vb vd vc)" by (blast dest: tree_less_trans) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

375 
with "5_3" show ?case by simp 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

376 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

377 
case ("5_4" va vb vg vc x w b y s c z t vd ve vii vf) 
35534  378 
hence "x < y \<and> tree_less x (Branch B va vb vg vc)" by simp 
379 
hence 1: "tree_less y (Branch B va vb vg vc)" by (blast dest: tree_less_trans) 

380 
from "5_4" have "y < z \<and> tree_greater z (Branch B vd ve vii vf)" by simp 

381 
hence "tree_greater y (Branch B vd ve vii vf)" by (blast dest: tree_greater_trans) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

382 
with 1 "5_4" show ?case by simp 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

383 
qed simp+ 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

384 

35550  385 
lemma entries_balance [simp]: 
386 
"entries (balance l k v r) = entries l @ (k, v) # entries r" 

387 
by (induct l k v r rule: balance.induct) auto 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

388 

35550  389 
lemma keys_balance [simp]: 
390 
"keys (balance l k v r) = keys l @ k # keys r" 

391 
by (simp add: keys_def) 

392 

393 
lemma balance_in_tree: 

394 
"entry_in_tree k x (balance l v y r) \<longleftrightarrow> entry_in_tree k x l \<or> k = v \<and> x = y \<or> entry_in_tree k x r" 

395 
by (auto simp add: keys_def) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

396 

35534  397 
lemma lookup_balance[simp]: 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

398 
fixes k :: "'a::linorder" 
35534  399 
assumes "sorted l" "sorted r" "l \<guillemotleft> k" "k \<guillemotleft> r" 
400 
shows "lookup (balance l k v r) x = lookup (Branch B l k v r) x" 

35550  401 
by (rule lookup_from_in_tree) (auto simp:assms balance_in_tree balance_sorted) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

402 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

403 
primrec paint :: "color \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

404 
where 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

405 
"paint c Empty = Empty" 
35534  406 
 "paint c (Branch _ l k v r) = Branch c l k v r" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

407 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

408 
lemma paint_inv1l[simp]: "inv1l t \<Longrightarrow> inv1l (paint c t)" by (cases t) auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

409 
lemma paint_inv1[simp]: "inv1l t \<Longrightarrow> inv1 (paint B t)" by (cases t) auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

410 
lemma paint_inv2[simp]: "inv2 t \<Longrightarrow> inv2 (paint c t)" by (cases t) auto 
35534  411 
lemma paint_color_of[simp]: "color_of (paint B t) = B" by (cases t) auto 
412 
lemma paint_sorted[simp]: "sorted t \<Longrightarrow> sorted (paint c t)" by (cases t) auto 

35550  413 
lemma paint_in_tree[simp]: "entry_in_tree k x (paint c t) = entry_in_tree k x t" by (cases t) auto 
35534  414 
lemma paint_lookup[simp]: "lookup (paint c t) = lookup t" by (rule ext) (cases t, auto) 
415 
lemma paint_tree_greater[simp]: "(v \<guillemotleft> paint c t) = (v \<guillemotleft> t)" by (cases t) auto 

416 
lemma paint_tree_less[simp]: "(paint c t \<guillemotleft> v) = (t \<guillemotleft> v)" by (cases t) auto 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

417 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

418 
fun 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

419 
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 redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

420 
where 
35534  421 
"ins f k v Empty = Branch R Empty k v Empty"  
422 
"ins f k v (Branch B l x y r) = (if k < x then balance (ins f k v l) x y r 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

423 
else if k > x then balance l x y (ins f k v r) 
35534  424 
else Branch B l x (f k y v) r)"  
425 
"ins f k v (Branch R l x y r) = (if k < x then Branch R (ins f k v l) x y r 

426 
else if k > x then Branch R l x y (ins f k v r) 

427 
else Branch R l x (f k y v) r)" 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

428 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

429 
lemma ins_inv1_inv2: 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

430 
assumes "inv1 t" "inv2 t" 
35534  431 
shows "inv2 (ins f k x t)" "bheight (ins f k x t) = bheight t" 
432 
"color_of t = B \<Longrightarrow> inv1 (ins f k x t)" "inv1l (ins f k x t)" 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

433 
using assms 
35534  434 
by (induct f k x t rule: ins.induct) (auto simp: balance_inv1 balance_inv2 balance_bheight) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

435 

35534  436 
lemma ins_tree_greater[simp]: "(v \<guillemotleft> ins f k x t) = (v \<guillemotleft> t \<and> k > v)" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

437 
by (induct f k x t rule: ins.induct) auto 
35534  438 
lemma ins_tree_less[simp]: "(ins f k x t \<guillemotleft> v) = (t \<guillemotleft> v \<and> k < v)" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

439 
by (induct f k x t rule: ins.induct) auto 
35534  440 
lemma ins_sorted[simp]: "sorted t \<Longrightarrow> sorted (ins f k x t)" 
441 
by (induct f k x t rule: ins.induct) (auto simp: balance_sorted) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

442 

35550  443 
lemma keys_ins: "set (keys (ins f k v t)) = { k } \<union> set (keys t)" 
444 
by (induct f k v t rule: ins.induct) auto 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

445 

35534  446 
lemma lookup_ins: 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

447 
fixes k :: "'a::linorder" 
35534  448 
assumes "sorted t" 
449 
shows "lookup (ins f k v t) x = ((lookup t)(k > case lookup t k of None \<Rightarrow> v 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

450 
 Some w \<Rightarrow> f k w v)) x" 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

451 
using assms by (induct f k v t rule: ins.induct) auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

452 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

453 
definition 
35550  454 
insert_with_key :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

455 
where 
35550  456 
"insert_with_key f k v t = paint B (ins f k v t)" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

457 

35550  458 
lemma insertwk_sorted: "sorted t \<Longrightarrow> sorted (insert_with_key f k x t)" 
459 
by (auto simp: insert_with_key_def) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

460 

35534  461 
theorem insertwk_is_rbt: 
462 
assumes inv: "is_rbt t" 

35550  463 
shows "is_rbt (insert_with_key f k x t)" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

464 
using assms 
35550  465 
unfolding insert_with_key_def is_rbt_def 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

466 
by (auto simp: ins_inv1_inv2) 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

467 

35534  468 
lemma lookup_insertwk: 
469 
assumes "sorted t" 

35550  470 
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 redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

471 
 Some w \<Rightarrow> f k w v)) x" 
35550  472 
unfolding insert_with_key_def using assms 
35534  473 
by (simp add:lookup_ins) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

474 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

475 
definition 
35550  476 
insertw_def: "insert_with f = insert_with_key (\<lambda>_. f)" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

477 

35550  478 
lemma insertw_sorted: "sorted t \<Longrightarrow> sorted (insert_with f k v t)" by (simp add: insertwk_sorted insertw_def) 
479 
theorem insertw_is_rbt: "is_rbt t \<Longrightarrow> is_rbt (insert_with f k v t)" by (simp add: insertwk_is_rbt insertw_def) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

480 

35534  481 
lemma lookup_insertw: 
482 
assumes "is_rbt t" 

35550  483 
shows "lookup (insert_with f k v t) = (lookup t)(k \<mapsto> (if k:dom (lookup t) then f (the (lookup t k)) v else v))" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

484 
using assms 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

485 
unfolding insertw_def 
35534  486 
by (rule_tac ext) (cases "lookup t k", auto simp:lookup_insertwk dom_def) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

487 

35534  488 
definition insert :: "'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where 
35550  489 
"insert = insert_with_key (\<lambda>_ _ nv. nv)" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

490 

35534  491 
lemma insert_sorted: "sorted t \<Longrightarrow> sorted (insert k v t)" by (simp add: insertwk_sorted insert_def) 
35550  492 
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 redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

493 

35534  494 
lemma lookup_insert: 
495 
assumes "is_rbt t" 

496 
shows "lookup (insert k v t) = (lookup t)(k\<mapsto>v)" 

497 
unfolding insert_def 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

498 
using assms 
35534  499 
by (rule_tac ext) (simp add: lookup_insertwk split:option.split) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

500 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

501 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

502 
subsection {* Deletion *} 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

503 

35534  504 
lemma bheight_paintR'[simp]: "color_of t = B \<Longrightarrow> bheight (paint R t) = bheight t  1" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

505 
by (cases t rule: rbt_cases) auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

506 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

507 
fun 
35550  508 
balance_left :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

509 
where 
35550  510 
"balance_left (Branch R a k x b) s y c = Branch R (Branch B a k x b) s y c"  
511 
"balance_left bl k x (Branch B a s y b) = balance bl k x (Branch R a s y b)"  

512 
"balance_left bl k x (Branch R (Branch B a s y b) t z c) = Branch R (Branch B bl k x a) s y (balance b t z (paint R c))"  

513 
"balance_left t k x s = Empty" 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

514 

35550  515 
lemma balance_left_inv2_with_inv1: 
35534  516 
assumes "inv2 lt" "inv2 rt" "bheight lt + 1 = bheight rt" "inv1 rt" 
35550  517 
shows "bheight (balance_left lt k v rt) = bheight lt + 1" 
518 
and "inv2 (balance_left lt k v rt)" 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

519 
using assms 
35550  520 
by (induct lt k v rt rule: balance_left.induct) (auto simp: balance_inv2 balance_bheight) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

521 

35550  522 
lemma balance_left_inv2_app: 
35534  523 
assumes "inv2 lt" "inv2 rt" "bheight lt + 1 = bheight rt" "color_of rt = B" 
35550  524 
shows "inv2 (balance_left lt k v rt)" 
525 
"bheight (balance_left lt k v rt) = bheight rt" 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

526 
using assms 
35550  527 
by (induct lt k v rt rule: balance_left.induct) (auto simp add: balance_inv2 balance_bheight)+ 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

528 

35550  529 
lemma balance_left_inv1: "\<lbrakk>inv1l a; inv1 b; color_of b = B\<rbrakk> \<Longrightarrow> inv1 (balance_left a k x b)" 
530 
by (induct a k x b rule: balance_left.induct) (simp add: balance_inv1)+ 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

531 

35550  532 
lemma balance_left_inv1l: "\<lbrakk> inv1l lt; inv1 rt \<rbrakk> \<Longrightarrow> inv1l (balance_left lt k x rt)" 
533 
by (induct lt k x rt rule: balance_left.induct) (auto simp: balance_inv1) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

534 

35550  535 
lemma balance_left_sorted: "\<lbrakk> sorted l; sorted r; tree_less k l; tree_greater k r \<rbrakk> \<Longrightarrow> sorted (balance_left l k v r)" 
536 
apply (induct l k v r rule: balance_left.induct) 

35534  537 
apply (auto simp: balance_sorted) 
538 
apply (unfold tree_greater_prop tree_less_prop) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

539 
by force+ 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

540 

35550  541 
lemma balance_left_tree_greater: 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

542 
fixes k :: "'a::order" 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

543 
assumes "k \<guillemotleft> a" "k \<guillemotleft> b" "k < x" 
35550  544 
shows "k \<guillemotleft> balance_left a x t b" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

545 
using assms 
35550  546 
by (induct a x t b rule: balance_left.induct) auto 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

547 

35550  548 
lemma balance_left_tree_less: 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

549 
fixes k :: "'a::order" 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

550 
assumes "a \<guillemotleft> k" "b \<guillemotleft> k" "x < k" 
35550  551 
shows "balance_left a x t b \<guillemotleft> k" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

552 
using assms 
35550  553 
by (induct a x t b rule: balance_left.induct) auto 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

554 

35550  555 
lemma balance_left_in_tree: 
35534  556 
assumes "inv1l l" "inv1 r" "bheight l + 1 = bheight r" 
35550  557 
shows "entry_in_tree k v (balance_left l a b r) = (entry_in_tree k v l \<or> k = a \<and> v = b \<or> entry_in_tree k v r)" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

558 
using assms 
35550  559 
by (induct l k v r rule: balance_left.induct) (auto simp: balance_in_tree) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

560 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

561 
fun 
35550  562 
balance_right :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

563 
where 
35550  564 
"balance_right a k x (Branch R b s y c) = Branch R a k x (Branch B b s y c)"  
565 
"balance_right (Branch B a k x b) s y bl = balance (Branch R a k x b) s y bl"  

566 
"balance_right (Branch R a k x (Branch B b s y c)) t z bl = Branch R (balance (paint R a) k x b) s y (Branch B c t z bl)"  

567 
"balance_right t k x s = Empty" 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

568 

35550  569 
lemma balance_right_inv2_with_inv1: 
35534  570 
assumes "inv2 lt" "inv2 rt" "bheight lt = bheight rt + 1" "inv1 lt" 
35550  571 
shows "inv2 (balance_right lt k v rt) \<and> bheight (balance_right lt k v rt) = bheight lt" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

572 
using assms 
35550  573 
by (induct lt k v rt rule: balance_right.induct) (auto simp: balance_inv2 balance_bheight) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

574 

35550  575 
lemma balance_right_inv1: "\<lbrakk>inv1 a; inv1l b; color_of a = B\<rbrakk> \<Longrightarrow> inv1 (balance_right a k x b)" 
576 
by (induct a k x b rule: balance_right.induct) (simp add: balance_inv1)+ 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

577 

35550  578 
lemma balance_right_inv1l: "\<lbrakk> inv1 lt; inv1l rt \<rbrakk> \<Longrightarrow>inv1l (balance_right lt k x rt)" 
579 
by (induct lt k x rt rule: balance_right.induct) (auto simp: balance_inv1) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

580 

35550  581 
lemma balance_right_sorted: "\<lbrakk> sorted l; sorted r; tree_less k l; tree_greater k r \<rbrakk> \<Longrightarrow> sorted (balance_right l k v r)" 
582 
apply (induct l k v r rule: balance_right.induct) 

35534  583 
apply (auto simp:balance_sorted) 
584 
apply (unfold tree_less_prop tree_greater_prop) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

585 
by force+ 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

586 

35550  587 
lemma balance_right_tree_greater: 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

588 
fixes k :: "'a::order" 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

589 
assumes "k \<guillemotleft> a" "k \<guillemotleft> b" "k < x" 
35550  590 
shows "k \<guillemotleft> balance_right a x t b" 
591 
using assms by (induct a x t b rule: balance_right.induct) auto 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

592 

35550  593 
lemma balance_right_tree_less: 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

594 
fixes k :: "'a::order" 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

595 
assumes "a \<guillemotleft> k" "b \<guillemotleft> k" "x < k" 
35550  596 
shows "balance_right a x t b \<guillemotleft> k" 
597 
using assms by (induct a x t b rule: balance_right.induct) auto 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

598 

35550  599 
lemma balance_right_in_tree: 
35534  600 
assumes "inv1 l" "inv1l r" "bheight l = bheight r + 1" "inv2 l" "inv2 r" 
35550  601 
shows "entry_in_tree x y (balance_right l k v r) = (entry_in_tree x y l \<or> x = k \<and> y = v \<or> entry_in_tree x y r)" 
602 
using assms by (induct l k v r rule: balance_right.induct) (auto simp: balance_in_tree) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

603 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

604 
fun 
35550  605 
combine :: "('a,'b) rbt \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

606 
where 
35550  607 
"combine Empty x = x" 
608 
 "combine x Empty = x" 

609 
 "combine (Branch R a k x b) (Branch R c s y d) = (case (combine b c) of 

35534  610 
Branch R b2 t z c2 \<Rightarrow> (Branch R (Branch R a k x b2) t z (Branch R c2 s y d))  
611 
bc \<Rightarrow> Branch R a k x (Branch R bc s y d))" 

35550  612 
 "combine (Branch B a k x b) (Branch B c s y d) = (case (combine b c) of 
35534  613 
Branch R b2 t z c2 \<Rightarrow> Branch R (Branch B a k x b2) t z (Branch B c2 s y d)  
35550  614 
bc \<Rightarrow> balance_left a k x (Branch B bc s y d))" 
615 
 "combine a (Branch R b k x c) = Branch R (combine a b) k x c" 

616 
 "combine (Branch R a k x b) c = Branch R a k x (combine b c)" 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

617 

35550  618 
lemma combine_inv2: 
35534  619 
assumes "inv2 lt" "inv2 rt" "bheight lt = bheight rt" 
35550  620 
shows "bheight (combine lt rt) = bheight lt" "inv2 (combine lt rt)" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

621 
using assms 
35550  622 
by (induct lt rt rule: combine.induct) 
623 
(auto simp: balance_left_inv2_app split: rbt.splits color.splits) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

624 

35550  625 
lemma combine_inv1: 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

626 
assumes "inv1 lt" "inv1 rt" 
35550  627 
shows "color_of lt = B \<Longrightarrow> color_of rt = B \<Longrightarrow> inv1 (combine lt rt)" 
628 
"inv1l (combine lt rt)" 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

629 
using assms 
35550  630 
by (induct lt rt rule: combine.induct) 
631 
(auto simp: balance_left_inv1 split: rbt.splits color.splits) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

632 

35550  633 
lemma combine_tree_greater[simp]: 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

634 
fixes k :: "'a::linorder" 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

635 
assumes "k \<guillemotleft> l" "k \<guillemotleft> r" 
35550  636 
shows "k \<guillemotleft> combine l r" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

637 
using assms 
35550  638 
by (induct l r rule: combine.induct) 
639 
(auto simp: balance_left_tree_greater split:rbt.splits color.splits) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

640 

35550  641 
lemma combine_tree_less[simp]: 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

642 
fixes k :: "'a::linorder" 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

643 
assumes "l \<guillemotleft> k" "r \<guillemotleft> k" 
35550  644 
shows "combine l r \<guillemotleft> k" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

645 
using assms 
35550  646 
by (induct l r rule: combine.induct) 
647 
(auto simp: balance_left_tree_less split:rbt.splits color.splits) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

648 

35550  649 
lemma combine_sorted: 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

650 
fixes k :: "'a::linorder" 
35534  651 
assumes "sorted l" "sorted r" "l \<guillemotleft> k" "k \<guillemotleft> r" 
35550  652 
shows "sorted (combine l r)" 
653 
using assms proof (induct l r rule: combine.induct) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

654 
case (3 a x v b c y w d) 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

655 
hence ineqs: "a \<guillemotleft> x" "x \<guillemotleft> b" "b \<guillemotleft> k" "k \<guillemotleft> c" "c \<guillemotleft> y" "y \<guillemotleft> d" 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

656 
by auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

657 
with 3 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

658 
show ?case 
35550  659 
by (cases "combine b c" rule: rbt_cases) 
660 
(auto, (metis combine_tree_greater combine_tree_less ineqs ineqs tree_less_simps(2) tree_greater_simps(2) tree_greater_trans tree_less_trans)+) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

661 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

662 
case (4 a x v b c y w d) 
35534  663 
hence "x < k \<and> tree_greater k c" by simp 
664 
hence "tree_greater x c" by (blast dest: tree_greater_trans) 

35550  665 
with 4 have 2: "tree_greater x (combine b c)" by (simp add: combine_tree_greater) 
35534  666 
from 4 have "k < y \<and> tree_less k b" by simp 
667 
hence "tree_less y b" by (blast dest: tree_less_trans) 

35550  668 
with 4 have 3: "tree_less y (combine b c)" by (simp add: combine_tree_less) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

669 
show ?case 
35550  670 
proof (cases "combine b c" rule: rbt_cases) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

671 
case Empty 
35534  672 
from 4 have "x < y \<and> tree_greater y d" by auto 
673 
hence "tree_greater x d" by (blast dest: tree_greater_trans) 

674 
with 4 Empty have "sorted a" and "sorted (Branch B Empty y w d)" and "tree_less x a" and "tree_greater x (Branch B Empty y w d)" by auto 

35550  675 
with Empty show ?thesis by (simp add: balance_left_sorted) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

676 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

677 
case (Red lta va ka rta) 
35534  678 
with 2 4 have "x < va \<and> tree_less x a" by simp 
679 
hence 5: "tree_less va a" by (blast dest: tree_less_trans) 

680 
from Red 3 4 have "va < y \<and> tree_greater y d" by simp 

681 
hence "tree_greater va d" by (blast dest: tree_greater_trans) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

682 
with Red 2 3 4 5 show ?thesis by simp 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

683 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

684 
case (Black lta va ka rta) 
35534  685 
from 4 have "x < y \<and> tree_greater y d" by auto 
686 
hence "tree_greater x d" by (blast dest: tree_greater_trans) 

35550  687 
with Black 2 3 4 have "sorted a" and "sorted (Branch B (combine b c) y w d)" and "tree_less x a" and "tree_greater x (Branch B (combine b c) y w d)" by auto 
688 
with Black show ?thesis by (simp add: balance_left_sorted) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

689 
qed 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

690 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

691 
case (5 va vb vd vc b x w c) 
35534  692 
hence "k < x \<and> tree_less k (Branch B va vb vd vc)" by simp 
693 
hence "tree_less x (Branch B va vb vd vc)" by (blast dest: tree_less_trans) 

35550  694 
with 5 show ?case by (simp add: combine_tree_less) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

695 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

696 
case (6 a x v b va vb vd vc) 
35534  697 
hence "x < k \<and> tree_greater k (Branch B va vb vd vc)" by simp 
698 
hence "tree_greater x (Branch B va vb vd vc)" by (blast dest: tree_greater_trans) 

35550  699 
with 6 show ?case by (simp add: combine_tree_greater) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

700 
qed simp+ 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

701 

35550  702 
lemma combine_in_tree: 
35534  703 
assumes "inv2 l" "inv2 r" "bheight l = bheight r" "inv1 l" "inv1 r" 
35550  704 
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 redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

705 
using assms 
35550  706 
proof (induct l r rule: combine.induct) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

707 
case (4 _ _ _ b c) 
35550  708 
hence a: "bheight (combine b c) = bheight b" by (simp add: combine_inv2) 
709 
from 4 have b: "inv1l (combine b c)" by (simp add: combine_inv1) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

710 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

711 
show ?case 
35550  712 
proof (cases "combine b c" rule: rbt_cases) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

713 
case Empty 
35550  714 
with 4 a show ?thesis by (auto simp: balance_left_in_tree) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

715 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

716 
case (Red lta ka va rta) 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

717 
with 4 show ?thesis by auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

718 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

719 
case (Black lta ka va rta) 
35550  720 
with a b 4 show ?thesis by (auto simp: balance_left_in_tree) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

721 
qed 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

722 
qed (auto split: rbt.splits color.splits) 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

723 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

724 
fun 
35550  725 
del_from_left :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" and 
726 
del_from_right :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" and 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

727 
del :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

728 
where 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

729 
"del x Empty = Empty"  
35550  730 
"del x (Branch c a y s b) = (if x < y then del_from_left x a y s b else (if x > y then del_from_right x a y s b else combine a b))"  
731 
"del_from_left x (Branch B lt z v rt) y s b = balance_left (del x (Branch B lt z v rt)) y s b"  

732 
"del_from_left x a y s b = Branch R (del x a) y s b"  

733 
"del_from_right x a y s (Branch B lt z v rt) = balance_right a y s (del x (Branch B lt z v rt))"  

734 
"del_from_right x a y s b = Branch R a y s (del x b)" 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

735 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

736 
lemma 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

737 
assumes "inv2 lt" "inv1 lt" 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

738 
shows 
35534  739 
"\<lbrakk>inv2 rt; bheight lt = bheight rt; inv1 rt\<rbrakk> \<Longrightarrow> 
35550  740 
inv2 (del_from_left x lt k v rt) \<and> bheight (del_from_left x lt k v rt) = bheight lt \<and> (color_of lt = B \<and> color_of rt = B \<and> inv1 (del_from_left x lt k v rt) \<or> (color_of lt \<noteq> B \<or> color_of rt \<noteq> B) \<and> inv1l (del_from_left x lt k v rt))" 
35534  741 
and "\<lbrakk>inv2 rt; bheight lt = bheight rt; inv1 rt\<rbrakk> \<Longrightarrow> 
35550  742 
inv2 (del_from_right x lt k v rt) \<and> bheight (del_from_right x lt k v rt) = bheight lt \<and> (color_of lt = B \<and> color_of rt = B \<and> inv1 (del_from_right x lt k v rt) \<or> (color_of lt \<noteq> B \<or> color_of rt \<noteq> B) \<and> inv1l (del_from_right x lt k v rt))" 
35534  743 
and del_inv1_inv2: "inv2 (del x lt) \<and> (color_of lt = R \<and> bheight (del x lt) = bheight lt \<and> inv1 (del x lt) 
744 
\<or> color_of lt = B \<and> bheight (del x lt) = bheight lt  1 \<and> inv1l (del x lt))" 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

745 
using assms 
35550  746 
proof (induct x lt k v rt and x lt k v rt and x lt rule: del_from_left_del_from_right_del.induct) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

747 
case (2 y c _ y') 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

748 
have "y = y' \<or> y < y' \<or> y > y'" by auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

749 
thus ?case proof (elim disjE) 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

750 
assume "y = y'" 
35550  751 
with 2 show ?thesis by (cases c) (simp add: combine_inv2 combine_inv1)+ 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

752 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

753 
assume "y < y'" 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

754 
with 2 show ?thesis by (cases c) auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

755 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

756 
assume "y' < y" 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

757 
with 2 show ?thesis by (cases c) auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

758 
qed 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

759 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

760 
case (3 y lt z v rta y' ss bb) 
35550  761 
thus ?case by (cases "color_of (Branch B lt z v rta) = B \<and> color_of bb = B") (simp add: balance_left_inv2_with_inv1 balance_left_inv1 balance_left_inv1l)+ 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

762 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

763 
case (5 y a y' ss lt z v rta) 
35550  764 
thus ?case by (cases "color_of a = B \<and> color_of (Branch B lt z v rta) = B") (simp add: balance_right_inv2_with_inv1 balance_right_inv1 balance_right_inv1l)+ 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

765 
next 
35534  766 
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 redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

767 
qed auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

768 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

769 
lemma 
35550  770 
del_from_left_tree_less: "\<lbrakk>tree_less v lt; tree_less v rt; k < v\<rbrakk> \<Longrightarrow> tree_less v (del_from_left x lt k y rt)" 
771 
and del_from_right_tree_less: "\<lbrakk>tree_less v lt; tree_less v rt; k < v\<rbrakk> \<Longrightarrow> tree_less v (del_from_right x lt k y rt)" 

35534  772 
and del_tree_less: "tree_less v lt \<Longrightarrow> tree_less v (del x lt)" 
35550  773 
by (induct x lt k y rt and x lt k y rt and x lt rule: del_from_left_del_from_right_del.induct) 
774 
(auto simp: balance_left_tree_less balance_right_tree_less) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

775 

35550  776 
lemma del_from_left_tree_greater: "\<lbrakk>tree_greater v lt; tree_greater v rt; k > v\<rbrakk> \<Longrightarrow> tree_greater v (del_from_left x lt k y rt)" 
777 
and del_from_right_tree_greater: "\<lbrakk>tree_greater v lt; tree_greater v rt; k > v\<rbrakk> \<Longrightarrow> tree_greater v (del_from_right x lt k y rt)" 

35534  778 
and del_tree_greater: "tree_greater v lt \<Longrightarrow> tree_greater v (del x lt)" 
35550  779 
by (induct x lt k y rt and x lt k y rt and x lt rule: del_from_left_del_from_right_del.induct) 
780 
(auto simp: balance_left_tree_greater balance_right_tree_greater) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

781 

35550  782 
lemma "\<lbrakk>sorted lt; sorted rt; tree_less k lt; tree_greater k rt\<rbrakk> \<Longrightarrow> sorted (del_from_left x lt k y rt)" 
783 
and "\<lbrakk>sorted lt; sorted rt; tree_less k lt; tree_greater k rt\<rbrakk> \<Longrightarrow> sorted (del_from_right x lt k y rt)" 

35534  784 
and del_sorted: "sorted lt \<Longrightarrow> sorted (del x lt)" 
35550  785 
proof (induct x lt k y rt and x lt k y rt and x lt rule: del_from_left_del_from_right_del.induct) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

786 
case (3 x lta zz v rta yy ss bb) 
35534  787 
from 3 have "tree_less yy (Branch B lta zz v rta)" by simp 
788 
hence "tree_less yy (del x (Branch B lta zz v rta))" by (rule del_tree_less) 

35550  789 
with 3 show ?case by (simp add: balance_left_sorted) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

790 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

791 
case ("4_2" x vaa vbb vdd vc yy ss bb) 
35534  792 
hence "tree_less yy (Branch R vaa vbb vdd vc)" by simp 
793 
hence "tree_less yy (del x (Branch R vaa vbb vdd vc))" by (rule del_tree_less) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

794 
with "4_2" show ?case by simp 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

795 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

796 
case (5 x aa yy ss lta zz v rta) 
35534  797 
hence "tree_greater yy (Branch B lta zz v rta)" by simp 
798 
hence "tree_greater yy (del x (Branch B lta zz v rta))" by (rule del_tree_greater) 

35550  799 
with 5 show ?case by (simp add: balance_right_sorted) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

800 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

801 
case ("6_2" x aa yy ss vaa vbb vdd vc) 
35534  802 
hence "tree_greater yy (Branch R vaa vbb vdd vc)" by simp 
803 
hence "tree_greater yy (del x (Branch R vaa vbb vdd vc))" by (rule del_tree_greater) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

804 
with "6_2" show ?case by simp 
35550  805 
qed (auto simp: combine_sorted) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

806 

35550  807 
lemma "\<lbrakk>sorted lt; sorted rt; tree_less kt lt; tree_greater kt rt; inv1 lt; inv1 rt; inv2 lt; inv2 rt; bheight lt = bheight rt; x < kt\<rbrakk> \<Longrightarrow> entry_in_tree k v (del_from_left x lt kt y rt) = (False \<or> (x \<noteq> k \<and> entry_in_tree k v (Branch c lt kt y rt)))" 
808 
and "\<lbrakk>sorted lt; sorted rt; tree_less kt lt; tree_greater kt rt; inv1 lt; inv1 rt; inv2 lt; inv2 rt; bheight lt = bheight rt; x > kt\<rbrakk> \<Longrightarrow> entry_in_tree k v (del_from_right x lt kt y rt) = (False \<or> (x \<noteq> k \<and> entry_in_tree k v (Branch c lt kt y rt)))" 

809 
and del_in_tree: "\<lbrakk>sorted t; inv1 t; inv2 t\<rbrakk> \<Longrightarrow> entry_in_tree k v (del x t) = (False \<or> (x \<noteq> k \<and> entry_in_tree k v t))" 

810 
proof (induct x lt kt y rt and x lt kt y rt and x t rule: del_from_left_del_from_right_del.induct) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

811 
case (2 xx c aa yy ss bb) 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

812 
have "xx = yy \<or> xx < yy \<or> xx > yy" by auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

813 
from this 2 show ?case proof (elim disjE) 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

814 
assume "xx = yy" 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

815 
with 2 show ?thesis proof (cases "xx = k") 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

816 
case True 
35534  817 
from 2 `xx = yy` `xx = k` have "sorted (Branch c aa yy ss bb) \<and> k = yy" by simp 
818 
hence "\<not> entry_in_tree k v aa" "\<not> entry_in_tree k v bb" by (auto simp: tree_less_nit tree_greater_prop) 

35550  819 
with `xx = yy` 2 `xx = k` show ?thesis by (simp add: combine_in_tree) 
820 
qed (simp add: combine_in_tree) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

821 
qed simp+ 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

822 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

823 
case (3 xx lta zz vv rta yy ss bb) 
35534  824 
def mt[simp]: mt == "Branch B lta zz vv rta" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

825 
from 3 have "inv2 mt \<and> inv1 mt" by simp 
35534  826 
hence "inv2 (del xx mt) \<and> (color_of mt = R \<and> bheight (del xx mt) = bheight mt \<and> inv1 (del xx mt) \<or> color_of mt = B \<and> bheight (del xx mt) = bheight mt  1 \<and> inv1l (del xx mt))" by (blast dest: del_inv1_inv2) 
35550  827 
with 3 have 4: "entry_in_tree k v (del_from_left xx mt yy ss bb) = (False \<or> xx \<noteq> k \<and> entry_in_tree k v mt \<or> (k = yy \<and> v = ss) \<or> entry_in_tree k v bb)" by (simp add: balance_left_in_tree) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

828 
thus ?case proof (cases "xx = k") 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

829 
case True 
35534  830 
from 3 True have "tree_greater yy bb \<and> yy > k" by simp 
831 
hence "tree_greater k bb" by (blast dest: tree_greater_trans) 

832 
with 3 4 True show ?thesis by (auto simp: tree_greater_nit) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

833 
qed auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

834 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

835 
case ("4_1" xx yy ss bb) 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

836 
show ?case proof (cases "xx = k") 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

837 
case True 
35534  838 
with "4_1" have "tree_greater yy bb \<and> k < yy" by simp 
839 
hence "tree_greater k bb" by (blast dest: tree_greater_trans) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

840 
with "4_1" `xx = k` 
35534  841 
have "entry_in_tree k v (Branch R Empty yy ss bb) = entry_in_tree k v Empty" by (auto simp: tree_greater_nit) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

842 
thus ?thesis by auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

843 
qed simp+ 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

844 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

845 
case ("4_2" xx vaa vbb vdd vc yy ss bb) 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

846 
thus ?case proof (cases "xx = k") 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

847 
case True 
35534  848 
with "4_2" have "k < yy \<and> tree_greater yy bb" by simp 
849 
hence "tree_greater k bb" by (blast dest: tree_greater_trans) 

850 
with True "4_2" show ?thesis by (auto simp: tree_greater_nit) 

35550  851 
qed auto 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

852 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

853 
case (5 xx aa yy ss lta zz vv rta) 
35534  854 
def mt[simp]: mt == "Branch B lta zz vv rta" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

855 
from 5 have "inv2 mt \<and> inv1 mt" by simp 
35534  856 
hence "inv2 (del xx mt) \<and> (color_of mt = R \<and> bheight (del xx mt) = bheight mt \<and> inv1 (del xx mt) \<or> color_of mt = B \<and> bheight (del xx mt) = bheight mt  1 \<and> inv1l (del xx mt))" by (blast dest: del_inv1_inv2) 
35550  857 
with 5 have 3: "entry_in_tree k v (del_from_right xx aa yy ss mt) = (entry_in_tree k v aa \<or> (k = yy \<and> v = ss) \<or> False \<or> xx \<noteq> k \<and> entry_in_tree k v mt)" by (simp add: balance_right_in_tree) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

858 
thus ?case proof (cases "xx = k") 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

859 
case True 
35534  860 
from 5 True have "tree_less yy aa \<and> yy < k" by simp 
861 
hence "tree_less k aa" by (blast dest: tree_less_trans) 

862 
with 3 5 True show ?thesis by (auto simp: tree_less_nit) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

863 
qed auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

864 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

865 
case ("6_1" xx aa yy ss) 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

866 
show ?case proof (cases "xx = k") 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

867 
case True 
35534  868 
with "6_1" have "tree_less yy aa \<and> k > yy" by simp 
869 
hence "tree_less k aa" by (blast dest: tree_less_trans) 

870 
with "6_1" `xx = k` show ?thesis by (auto simp: tree_less_nit) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

871 
qed simp 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

872 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

873 
case ("6_2" xx aa yy ss vaa vbb vdd vc) 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

874 
thus ?case proof (cases "xx = k") 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

875 
case True 
35534  876 
with "6_2" have "k > yy \<and> tree_less yy aa" by simp 
877 
hence "tree_less k aa" by (blast dest: tree_less_trans) 

878 
with True "6_2" show ?thesis by (auto simp: tree_less_nit) 

35550  879 
qed auto 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

880 
qed simp 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

881 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

882 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

883 
definition delete where 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

884 
delete_def: "delete k t = paint B (del k t)" 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

885 

35550  886 
theorem delete_is_rbt [simp]: assumes "is_rbt t" shows "is_rbt (delete k t)" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

887 
proof  
35534  888 
from assms have "inv2 t" and "inv1 t" unfolding is_rbt_def by auto 
889 
hence "inv2 (del k t) \<and> (color_of t = R \<and> bheight (del k t) = bheight t \<and> inv1 (del k t) \<or> color_of t = B \<and> bheight (del k t) = bheight t  1 \<and> inv1l (del k t))" by (rule del_inv1_inv2) 

890 
hence "inv2 (del k t) \<and> inv1l (del k t)" by (cases "color_of t") auto 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

891 
with assms show ?thesis 
35534  892 
unfolding is_rbt_def delete_def 
893 
by (auto intro: paint_sorted del_sorted) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

894 
qed 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

895 

35550  896 
lemma delete_in_tree: 
35534  897 
assumes "is_rbt t" 
898 
shows "entry_in_tree k v (delete x t) = (x \<noteq> k \<and> entry_in_tree k v t)" 

899 
using assms unfolding is_rbt_def delete_def 

35550  900 
by (auto simp: del_in_tree) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

901 

35534  902 
lemma lookup_delete: 
903 
assumes is_rbt: "is_rbt t" 

904 
shows "lookup (delete k t) = (lookup t)`({k})" 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

905 
proof 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

906 
fix x 
35534  907 
show "lookup (delete k t) x = (lookup t ` ({k})) x" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

908 
proof (cases "x = k") 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

909 
assume "x = k" 
35534  910 
with is_rbt show ?thesis 
35550  911 
by (cases "lookup (delete k t) k") (auto simp: lookup_in_tree delete_in_tree) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

912 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

913 
assume "x \<noteq> k" 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

914 
thus ?thesis 
35550  915 
by auto (metis is_rbt delete_is_rbt delete_in_tree is_rbt_sorted lookup_from_in_tree) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

916 
qed 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

917 
qed 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

918 

35550  919 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

920 
subsection {* Union *} 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

921 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

922 
primrec 
35550  923 
union_with_key :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

924 
where 
35550  925 
"union_with_key f t Empty = t" 
926 
 "union_with_key f t (Branch c lt k v rt) = union_with_key f (union_with_key f (insert_with_key f k v t) lt) rt" 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

927 

35550  928 
lemma unionwk_sorted: "sorted lt \<Longrightarrow> sorted (union_with_key f lt rt)" 
35534  929 
by (induct rt arbitrary: lt) (auto simp: insertwk_sorted) 
35550  930 
theorem unionwk_is_rbt[simp]: "is_rbt lt \<Longrightarrow> is_rbt (union_with_key f lt rt)" 
35534  931 
by (induct rt arbitrary: lt) (simp add: insertwk_is_rbt)+ 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

932 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

933 
definition 
35550  934 
union_with where 
935 
"union_with f = union_with_key (\<lambda>_. f)" 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

936 

35550  937 
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 redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

938 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

939 
definition union where 
35550  940 
"union = union_with_key (%_ _ rv. rv)" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

941 

35534  942 
theorem union_is_rbt: "is_rbt lt \<Longrightarrow> is_rbt (union lt rt)" unfolding union_def by simp 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

943 

35534  944 
lemma union_Branch[simp]: 
945 
"union t (Branch c lt k v rt) = union (union (insert k v t) lt) rt" 

946 
unfolding union_def insert_def 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

947 
by simp 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

948 

35534  949 
lemma lookup_union: 
950 
assumes "is_rbt s" "sorted t" 

951 
shows "lookup (union s t) = lookup s ++ lookup t" 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

952 
using assms 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

953 
proof (induct t arbitrary: s) 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

954 
case Empty thus ?case by (auto simp: union_def) 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

955 
next 
35534  956 
case (Branch c l k v r s) 
35550  957 
then have "sorted r" "sorted l" "l \<guillemotleft> k" "k \<guillemotleft> r" by auto 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

958 

35534  959 
have meq: "lookup s(k \<mapsto> v) ++ lookup l ++ lookup r = 
960 
lookup s ++ 

961 
(\<lambda>a. if a < k then lookup l a 

962 
else if k < a then lookup r a else Some v)" (is "?m1 = ?m2") 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

963 
proof (rule ext) 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

964 
fix a 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

965 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

966 
have "k < a \<or> k = a \<or> k > a" by auto 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

967 
thus "?m1 a = ?m2 a" 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

968 
proof (elim disjE) 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

969 
assume "k < a" 
35534  970 
with `l \<guillemotleft> k` have "l \<guillemotleft> a" by (rule tree_less_trans) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

971 
with `k < a` show ?thesis 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

972 
by (auto simp: map_add_def split: option.splits) 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

973 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

974 
assume "k = a" 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

975 
with `l \<guillemotleft> k` `k \<guillemotleft> r` 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

976 
show ?thesis by (auto simp: map_add_def) 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

977 
next 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

978 
assume "a < k" 
35534  979 
from this `k \<guillemotleft> r` have "a \<guillemotleft> r" by (rule tree_greater_trans) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

980 
with `a < k` show ?thesis 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

981 
by (auto simp: map_add_def split: option.splits) 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

982 
qed 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

983 
qed 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

984 

36147
b43b22f63665
theory RBT with abstract type of redblack trees backed by implementation RBT_Impl
haftmann
parents:
35618
diff
changeset

985 
from Branch have is_rbt: "is_rbt (RBT_Impl.union (RBT_Impl.insert k v s) l)" 
35550  986 
by (auto intro: union_is_rbt insert_is_rbt) 
987 
with Branch have IHs: 

35534  988 
"lookup (union (union (insert k v s) l) r) = lookup (union (insert k v s) l) ++ lookup r" 
989 
"lookup (union (insert k v s) l) = lookup (insert k v s) ++ lookup l" 

35550  990 
by auto 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

991 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

992 
with meq show ?case 
35534  993 
by (auto simp: lookup_insert[OF Branch(3)]) 
35550  994 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

995 
qed 
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

996 

35550  997 

998 
subsection {* Modifying existing entries *} 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

999 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

1000 
primrec 
35602  1001 
map_entry :: "'a\<Colon>linorder \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

1002 
where 
35602  1003 
"map_entry k f Empty = Empty" 
1004 
 "map_entry k f (Branch c lt x v rt) = 

1005 
(if k < x then Branch c (map_entry k f lt) x v rt 

1006 
else if k > x then (Branch c lt x v (map_entry k f rt)) 

1007 
else Branch c lt x (f v) rt)" 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

1008 

35602  1009 
lemma map_entry_color_of: "color_of (map_entry k f t) = color_of t" by (induct t) simp+ 
1010 
lemma map_entry_inv1: "inv1 (map_entry k f t) = inv1 t" by (induct t) (simp add: map_entry_color_of)+ 

1011 
lemma map_entry_inv2: "inv2 (map_entry k f t) = inv2 t" "bheight (map_entry k f t) = bheight t" by (induct t) simp+ 

1012 
lemma map_entry_tree_greater: "tree_greater a (map_entry k f t) = tree_greater a t" by (induct t) simp+ 

1013 
lemma map_entry_tree_less: "tree_less a (map_entry k f t) = tree_less a t" by (induct t) simp+ 

1014 
lemma map_entry_sorted: "sorted (map_entry k f t) = sorted t" 

1015 
by (induct t) (simp_all add: map_entry_tree_less map_entry_tree_greater) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

1016 

35602  1017 
theorem map_entry_is_rbt [simp]: "is_rbt (map_entry k f t) = is_rbt t" 
1018 
unfolding is_rbt_def by (simp add: map_entry_inv2 map_entry_color_of map_entry_sorted map_entry_inv1 ) 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

1019 

35618  1020 
theorem lookup_map_entry: 
1021 
"lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))" 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

1022 
by (induct t) (auto split: option.splits simp add: fun_eq_iff) 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

1023 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

1024 

35550  1025 
subsection {* Mapping all entries *} 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

1026 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

1027 
primrec 
35602  1028 
map :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'c) rbt" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

1029 
where 
35550  1030 
"map f Empty = Empty" 
1031 
 "map f (Branch c lt k v rt) = Branch c (map f lt) k (f k v) (map f rt)" 

32237
cdc76a42fed4
added missing proof of RBT.map_of_alist_of (contributed by Peter Lammich)
krauss
parents:
30738
diff
changeset

1032 

35550  1033 
lemma map_entries [simp]: "entries (map f t) = List.map (\<lambda>(k, v). (k, f k v)) (entries t)" 
1034 
by (induct t) auto 

1035 
lemma map_keys [simp]: "keys (map f t) = keys t" by (simp add: keys_def split_def) 

1036 
lemma map_tree_greater: "tree_greater k (map f t) = tree_greater k t" by (induct t) simp+ 

1037 
lemma map_tree_less: "tree_less k (map f t) = tree_less k t" by (induct t) simp+ 

1038 
lemma map_sorted: "sorted (map f t) = sorted t" by (induct t) (simp add: map_tree_less map_tree_greater)+ 

1039 
lemma map_color_of: "color_of (map f t) = color_of t" by (induct t) simp+ 

1040 
lemma map_inv1: "inv1 (map f t) = inv1 t" by (induct t) (simp add: map_color_of)+ 

1041 
lemma map_inv2: "inv2 (map f t) = inv2 t" "bheight (map f t) = bheight t" by (induct t) simp+ 

1042 
theorem map_is_rbt [simp]: "is_rbt (map f t) = is_rbt t" 

1043 
unfolding is_rbt_def by (simp add: map_inv1 map_inv2 map_sorted map_color_of) 

32237
cdc76a42fed4
added missing proof of RBT.map_of_alist_of (contributed by Peter Lammich)
krauss
parents:
30738
diff
changeset

1044 

35618  1045 
theorem lookup_map: "lookup (map f t) x = Option.map (f x) (lookup t x)" 
1046 
by (induct t) auto 

26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

1047 

35550  1048 

1049 
subsection {* Folding over entries *} 

1050 

1051 
definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" where 

37458  1052 
"fold f t = More_List.fold (prod_case f) (entries t)" 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

1053 

35550  1054 
lemma fold_simps [simp, code]: 
1055 
"fold f Empty = id" 

1056 
"fold f (Branch c lt k v rt) = fold f rt \<circ> f k v \<circ> fold f lt" 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

1057 
by (simp_all add: fold_def fun_eq_iff) 
35534  1058 

35606  1059 

1060 
subsection {* Bulkloading a tree *} 

1061 

35618  1062 
definition bulkload :: "('a \<times> 'b) list \<Rightarrow> ('a\<Colon>linorder, 'b) rbt" where 
36147
b43b22f63665
theory RBT with abstract type of redblack trees backed by implementation RBT_Impl
haftmann
parents:
35618
diff
changeset

1063 
"bulkload xs = foldr (\<lambda>(k, v). insert k v) xs Empty" 
35606  1064 

1065 
lemma bulkload_is_rbt [simp, intro]: 

1066 
"is_rbt (bulkload xs)" 

1067 
unfolding bulkload_def by (induct xs) auto 

1068 

1069 
lemma lookup_bulkload: 

36147
b43b22f63665
theory RBT with abstract type of redblack trees backed by implementation RBT_Impl
haftmann
parents:
35618
diff
changeset

1070 
"lookup (bulkload xs) = map_of xs" 
35606  1071 
proof  
1072 
obtain ys where "ys = rev xs" by simp 

1073 
have "\<And>t. is_rbt t \<Longrightarrow> 

37458  1074 
lookup (More_List.fold (prod_case insert) ys t) = lookup t ++ map_of (rev ys)" 
1075 
by (induct ys) (simp_all add: bulkload_def lookup_insert prod_case_beta) 

35606  1076 
from this Empty_is_rbt have 
37458  1077 
"lookup (More_List.fold (prod_case insert) (rev xs) Empty) = lookup Empty ++ map_of xs" 
35606  1078 
by (simp add: `ys = rev xs`) 
37591  1079 
then show ?thesis by (simp add: bulkload_def lookup_Empty foldr_fold_rev) 
35606  1080 
qed 
1081 

41074  1082 
hide_const (open) R B Empty insert delete entries keys bulkload lookup map_entry map fold union sorted 
26192
52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

1083 

52617dca8386
new theory of redblack trees, an efficient implementation of finite maps.
krauss
parents:
diff
changeset

1084 
end 