author  nipkow 
Fri, 27 Dec 2019 10:54:15 +0100  
changeset 71555  7a0a6c56015e 
parent 70944  3fb16bed5d6c 
child 71557  857453c0db3d 
permissions  rwrr 
64951
140addd19343
removed contribution by Daniel Stuewe, too detailed.
nipkow
parents:
64950
diff
changeset

1 
(* Author: Tobias Nipkow *) 
61224  2 

3 
section \<open>RedBlack Tree Implementation of Sets\<close> 

4 

5 
theory RBT_Set 

6 
imports 

64950  7 
Complex_Main 
61224  8 
RBT 
61581  9 
Cmp 
61224  10 
Isin2 
11 
begin 

12 

68431  13 
definition empty :: "'a rbt" where 
14 
"empty = Leaf" 

15 

63411
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

16 
fun ins :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where 
61749  17 
"ins x Leaf = R Leaf x Leaf"  
18 
"ins x (B l a r) = 

61678  19 
(case cmp x a of 
64960  20 
LT \<Rightarrow> baliL (ins x l) a r  
21 
GT \<Rightarrow> baliR l a (ins x r)  

61678  22 
EQ \<Rightarrow> B l a r)"  
61749  23 
"ins x (R l a r) = 
61678  24 
(case cmp x a of 
61749  25 
LT \<Rightarrow> R (ins x l) a r  
26 
GT \<Rightarrow> R l a (ins x r)  

61678  27 
EQ \<Rightarrow> R l a r)" 
61224  28 

63411
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

29 
definition insert :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where 
61749  30 
"insert x t = paint Black (ins x t)" 
31 

66087  32 
fun color :: "'a rbt \<Rightarrow> color" where 
33 
"color Leaf = Black"  

70944
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70897
diff
changeset

34 
"color (Node _ (_, c) _) = c" 
66087  35 

36 
fun del :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where 

61749  37 
"del x Leaf = Leaf"  
70944
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70897
diff
changeset

38 
"del x (Node l (a, _) r) = 
61678  39 
(case cmp x a of 
66087  40 
LT \<Rightarrow> if l \<noteq> Leaf \<and> color l = Black 
41 
then baldL (del x l) a r else R (del x l) a r  

42 
GT \<Rightarrow> if r \<noteq> Leaf\<and> color r = Black 

43 
then baldR l a (del x r) else R l a (del x r)  

44 
EQ \<Rightarrow> combine l r)" 

61749  45 

63411
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

46 
definition delete :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where 
61749  47 
"delete x t = paint Black (del x t)" 
61224  48 

49 

50 
subsection "Functional Correctness Proofs" 

51 

61749  52 
lemma inorder_paint: "inorder(paint c t) = inorder t" 
62526  53 
by(cases t) (auto) 
61749  54 

64960  55 
lemma inorder_baliL: 
56 
"inorder(baliL l a r) = inorder l @ a # inorder r" 

57 
by(cases "(l,a,r)" rule: baliL.cases) (auto) 

58 

59 
lemma inorder_baliR: 

60 
"inorder(baliR l a r) = inorder l @ a # inorder r" 

61 
by(cases "(l,a,r)" rule: baliR.cases) (auto) 

61224  62 

61749  63 
lemma inorder_ins: 
64 
"sorted(inorder t) \<Longrightarrow> inorder(ins x t) = ins_list x (inorder t)" 

64960  65 
by(induction x t rule: ins.induct) 
66 
(auto simp: ins_list_simps inorder_baliL inorder_baliR) 

61749  67 

61224  68 
lemma inorder_insert: 
61749  69 
"sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)" 
70 
by (simp add: insert_def inorder_ins inorder_paint) 

61224  71 

64960  72 
lemma inorder_baldL: 
73 
"inorder(baldL l a r) = inorder l @ a # inorder r" 

74 
by(cases "(l,a,r)" rule: baldL.cases) 

75 
(auto simp: inorder_baliL inorder_baliR inorder_paint) 

61224  76 

64960  77 
lemma inorder_baldR: 
78 
"inorder(baldR l a r) = inorder l @ a # inorder r" 

79 
by(cases "(l,a,r)" rule: baldR.cases) 

80 
(auto simp: inorder_baliL inorder_baliR inorder_paint) 

61224  81 

82 
lemma inorder_combine: 

83 
"inorder(combine l r) = inorder l @ inorder r" 

84 
by(induction l r rule: combine.induct) 

64960  85 
(auto simp: inorder_baldL inorder_baldR split: tree.split color.split) 
61224  86 

61749  87 
lemma inorder_del: 
88 
"sorted(inorder t) \<Longrightarrow> inorder(del x t) = del_list x (inorder t)" 

66087  89 
by(induction x t rule: del.induct) 
64960  90 
(auto simp: del_list_simps inorder_combine inorder_baldL inorder_baldR) 
61224  91 

61749  92 
lemma inorder_delete: 
93 
"sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)" 

94 
by (auto simp: delete_def inorder_del inorder_paint) 

95 

61581  96 

63411
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

97 
subsection \<open>Structural invariants\<close> 
61224  98 

64952  99 
text\<open>The proofs are due to Markus Reiter and Alexander Krauss.\<close> 
61754  100 

101 
fun bheight :: "'a rbt \<Rightarrow> nat" where 

102 
"bheight Leaf = 0"  

70944
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70897
diff
changeset

103 
"bheight (Node l (x, c) r) = (if c = Black then bheight l + 1 else bheight l)" 
61754  104 

63411
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

105 
fun invc :: "'a rbt \<Rightarrow> bool" where 
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

106 
"invc Leaf = True"  
70944
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70897
diff
changeset

107 
"invc (Node l (a,c) r) = 
64947  108 
(invc l \<and> invc r \<and> (c = Red \<longrightarrow> color l = Black \<and> color r = Black))" 
61754  109 

70897  110 
text \<open>Weaker version:\<close> 
111 
abbreviation invc2 :: "'a rbt \<Rightarrow> bool" where 

112 
"invc2 t \<equiv> invc(paint Black t)" 

61754  113 

63411
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

114 
fun invh :: "'a rbt \<Rightarrow> bool" where 
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

115 
"invh Leaf = True"  
70944
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70897
diff
changeset

116 
"invh (Node l (x, c) r) = (invh l \<and> invh r \<and> bheight l = bheight r)" 
61754  117 

64953  118 
lemma invc2I: "invc t \<Longrightarrow> invc2 t" 
70944
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70897
diff
changeset

119 
by (cases t rule: tree2_cases) simp+ 
61754  120 

121 
definition rbt :: "'a rbt \<Rightarrow> bool" where 

63411
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

122 
"rbt t = (invc t \<and> invh t \<and> color t = Black)" 
61754  123 

124 
lemma color_paint_Black: "color (paint Black t) = Black" 

125 
by (cases t) auto 

126 

70897  127 
lemma paint2: "paint c2 (paint c1 t) = paint c2 t" 
61754  128 
by (cases t) auto 
129 

63411
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

130 
lemma invh_paint: "invh t \<Longrightarrow> invh (paint c t)" 
61754  131 
by (cases t) auto 
132 

64960  133 
lemma invc_baliL: 
134 
"\<lbrakk>invc2 l; invc r\<rbrakk> \<Longrightarrow> invc (baliL l a r)" 

135 
by (induct l a r rule: baliL.induct) auto 

136 

137 
lemma invc_baliR: 

138 
"\<lbrakk>invc l; invc2 r\<rbrakk> \<Longrightarrow> invc (baliR l a r)" 

139 
by (induct l a r rule: baliR.induct) auto 

140 

141 
lemma bheight_baliL: 

142 
"bheight l = bheight r \<Longrightarrow> bheight (baliL l a r) = Suc (bheight l)" 

143 
by (induct l a r rule: baliL.induct) auto 

61754  144 

64960  145 
lemma bheight_baliR: 
146 
"bheight l = bheight r \<Longrightarrow> bheight (baliR l a r) = Suc (bheight l)" 

147 
by (induct l a r rule: baliR.induct) auto 

61754  148 

64960  149 
lemma invh_baliL: 
150 
"\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk> \<Longrightarrow> invh (baliL l a r)" 

151 
by (induct l a r rule: baliL.induct) auto 

152 

153 
lemma invh_baliR: 

154 
"\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk> \<Longrightarrow> invh (baliR l a r)" 

155 
by (induct l a r rule: baliR.induct) auto 

61754  156 

70897  157 
text \<open>All in one:\<close> 
158 

159 
lemma inv_baliR: "\<lbrakk> invh l; invh r; invc l; invc2 r; bheight l = bheight r \<rbrakk> 

160 
\<Longrightarrow> invc (baliR l a r) \<and> invh (baliR l a r) \<and> bheight (baliR l a r) = Suc (bheight l)" 

161 
by (induct l a r rule: baliR.induct) auto 

162 

163 
lemma inv_baliL: "\<lbrakk> invh l; invh r; invc2 l; invc r; bheight l = bheight r \<rbrakk> 

164 
\<Longrightarrow> invc (baliL l a r) \<and> invh (baliL l a r) \<and> bheight (baliL l a r) = Suc (bheight l)" 

165 
by (induct l a r rule: baliL.induct) auto 

61754  166 

167 
subsubsection \<open>Insertion\<close> 

168 

70897  169 
lemma invc_ins: "invc t \<longrightarrow> invc2 (ins x t) \<and> (color t = Black \<longrightarrow> invc (ins x t))" 
64960  170 
by (induct x t rule: ins.induct) (auto simp: invc_baliL invc_baliR invc2I) 
61754  171 

70897  172 
lemma invh_ins: "invh t \<Longrightarrow> invh (ins x t) \<and> bheight (ins x t) = bheight t" 
64960  173 
by(induct x t rule: ins.induct) 
174 
(auto simp: invh_baliL invh_baliR bheight_baliL bheight_baliR) 

61754  175 

63411
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

176 
theorem rbt_insert: "rbt t \<Longrightarrow> rbt (insert x t)" 
70897  177 
by (simp add: invc_ins invh_ins color_paint_Black invh_paint rbt_def insert_def) 
178 

179 
text \<open>All in one variant:\<close> 

180 

181 
lemma inv_ins: "\<lbrakk> invc t; invh t \<rbrakk> \<Longrightarrow> 

182 
invc2 (ins x t) \<and> (color t = Black \<longrightarrow> invc (ins x t)) \<and> 

183 
invh(ins x t) \<and> bheight (ins x t) = bheight t" 

184 
by (induct x t rule: ins.induct) (auto simp: inv_baliL inv_baliR invc2I) 

185 

186 
theorem rbt_insert2: "rbt t \<Longrightarrow> rbt (insert x t)" 

187 
by (simp add: inv_ins color_paint_Black invh_paint rbt_def insert_def) 

61754  188 

63411
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

189 

e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

190 
subsubsection \<open>Deletion\<close> 
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

191 

e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

192 
lemma bheight_paint_Red: 
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

193 
"color t = Black \<Longrightarrow> bheight (paint Red t) = bheight t  1" 
61754  194 
by (cases t) auto 
195 

66087  196 
lemma invh_baldL_invc: 
197 
"\<lbrakk> invh l; invh r; bheight l + 1 = bheight r; invc r \<rbrakk> 

198 
\<Longrightarrow> invh (baldL l a r) \<and> bheight (baldL l a r) = bheight l + 1" 

64960  199 
by (induct l a r rule: baldL.induct) 
200 
(auto simp: invh_baliR invh_paint bheight_baliR bheight_paint_Red) 

61754  201 

66087  202 
lemma invh_baldL_Black: 
203 
"\<lbrakk> invh l; invh r; bheight l + 1 = bheight r; color r = Black \<rbrakk> 

204 
\<Longrightarrow> invh (baldL l a r) \<and> bheight (baldL l a r) = bheight r" 

64960  205 
by (induct l a r rule: baldL.induct) (auto simp add: invh_baliR bheight_baliR) 
61754  206 

66087  207 
lemma invc_baldL: "\<lbrakk>invc2 l; invc r; color r = Black\<rbrakk> \<Longrightarrow> invc (baldL l a r)" 
64960  208 
by (induct l a r rule: baldL.induct) (simp_all add: invc_baliR) 
61754  209 

66087  210 
lemma invc2_baldL: "\<lbrakk> invc2 l; invc r \<rbrakk> \<Longrightarrow> invc2 (baldL l a r)" 
70897  211 
by (induct l a r rule: baldL.induct) (auto simp: invc_baliR paint2 invc2I) 
61754  212 

66087  213 
lemma invh_baldR_invc: 
214 
"\<lbrakk> invh l; invh r; bheight l = bheight r + 1; invc l \<rbrakk> 

215 
\<Longrightarrow> invh (baldR l a r) \<and> bheight (baldR l a r) = bheight l" 

64960  216 
by(induct l a r rule: baldR.induct) 
217 
(auto simp: invh_baliL bheight_baliL invh_paint bheight_paint_Red) 

61754  218 

70757  219 
lemma invc_baldR: "\<lbrakk>invc l; invc2 r; color l = Black\<rbrakk> \<Longrightarrow> invc (baldR l a r)" 
220 
by (induct l a r rule: baldR.induct) (simp_all add: invc_baliL) 

61754  221 

70757  222 
lemma invc2_baldR: "\<lbrakk> invc l; invc2 r \<rbrakk> \<Longrightarrow>invc2 (baldR l a r)" 
70897  223 
by (induct l a r rule: baldR.induct) (auto simp: invc_baliL paint2 invc2I) 
61754  224 

63411
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

225 
lemma invh_combine: 
66087  226 
"\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk> 
227 
\<Longrightarrow> invh (combine l r) \<and> bheight (combine l r) = bheight l" 

64960  228 
by (induct l r rule: combine.induct) 
66087  229 
(auto simp: invh_baldL_Black split: tree.splits color.splits) 
61754  230 

63411
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

231 
lemma invc_combine: 
70897  232 
"\<lbrakk> invc l; invc r \<rbrakk> \<Longrightarrow> 
233 
(color l = Black \<and> color r = Black \<longrightarrow> invc (combine l r)) \<and> invc2 (combine l r)" 

64960  234 
by (induct l r rule: combine.induct) 
66087  235 
(auto simp: invc_baldL invc2I split: tree.splits color.splits) 
61754  236 

70944
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70897
diff
changeset

237 
lemma neq_LeafD: "t \<noteq> Leaf \<Longrightarrow> \<exists>l x c r. t = Node l (x,c) r" 
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70897
diff
changeset

238 
by(cases t rule: tree2_cases) auto 
66087  239 

66088  240 
lemma del_invc_invh: "invh t \<Longrightarrow> invc t \<Longrightarrow> invh (del x t) \<and> 
241 
(color t = Red \<and> bheight (del x t) = bheight t \<and> invc (del x t) \<or> 

242 
color t = Black \<and> bheight (del x t) = bheight t  1 \<and> invc2 (del x t))" 

243 
proof (induct x t rule: del.induct) 

68414  244 
case (2 x _ y c) 
66088  245 
have "x = y \<or> x < y \<or> x > y" by auto 
61754  246 
thus ?case proof (elim disjE) 
66088  247 
assume "x = y" 
63411
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

248 
with 2 show ?thesis 
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

249 
by (cases c) (simp_all add: invh_combine invc_combine) 
61754  250 
next 
66088  251 
assume "x < y" 
66087  252 
with 2 show ?thesis 
253 
by(cases c) 

254 
(auto simp: invh_baldL_invc invc_baldL invc2_baldL dest: neq_LeafD) 

61754  255 
next 
66088  256 
assume "y < x" 
66087  257 
with 2 show ?thesis 
258 
by(cases c) 

259 
(auto simp: invh_baldR_invc invc_baldR invc2_baldR dest: neq_LeafD) 

61754  260 
qed 
261 
qed auto 

262 

70757  263 
theorem rbt_delete: "rbt t \<Longrightarrow> rbt (delete x t)" 
70897  264 
by (metis delete_def rbt_def color_paint_Black del_invc_invh invc2I invh_paint) 
63411
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

265 

e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

266 
text \<open>Overall correctness:\<close> 
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

267 

68443  268 
interpretation S: Set_by_Ordered 
68431  269 
where empty = empty and isin = isin and insert = insert and delete = delete 
63411
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

270 
and inorder = inorder and inv = rbt 
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

271 
proof (standard, goal_cases) 
68431  272 
case 1 show ?case by (simp add: empty_def) 
63411
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

273 
next 
67967  274 
case 2 thus ?case by(simp add: isin_set_inorder) 
63411
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

275 
next 
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

276 
case 3 thus ?case by(simp add: inorder_insert) 
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

277 
next 
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

278 
case 4 thus ?case by(simp add: inorder_delete) 
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

279 
next 
68431  280 
case 5 thus ?case by (simp add: rbt_def empty_def) 
63411
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

281 
next 
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

282 
case 6 thus ?case by (simp add: rbt_insert) 
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

283 
next 
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

284 
case 7 thus ?case by (simp add: rbt_delete) 
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

285 
qed 
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

286 

e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

287 

e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

288 
subsection \<open>HeightSize Relation\<close> 
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

289 

64950  290 
lemma neq_Black[simp]: "(c \<noteq> Black) = (c = Red)" 
291 
by (cases c) auto 

292 

67963  293 
lemma rbt_height_bheight_if: "invc t \<Longrightarrow> invh t \<Longrightarrow> 
71555  294 
height t \<le> 2 * bheight t + (if color t = Black then 0 else 1)" 
64950  295 
by(induction t) (auto split: if_split_asm) 
296 

297 
lemma rbt_height_bheight: "rbt t \<Longrightarrow> height t / 2 \<le> bheight t " 

298 
by(auto simp: rbt_def dest: rbt_height_bheight_if) 

299 

67963  300 
lemma bheight_size_bound: "invc t \<Longrightarrow> invh t \<Longrightarrow> 2 ^ (bheight t) \<le> size1 t" 
64950  301 
by (induction t) auto 
302 

303 
lemma rbt_height_le: assumes "rbt t" shows "height t \<le> 2 * log 2 (size1 t)" 

304 
proof  

305 
have "2 powr (height t / 2) \<le> 2 powr bheight t" 

306 
using rbt_height_bheight[OF assms] by (simp) 

307 
also have "\<dots> \<le> size1 t" using assms 

308 
by (simp add: powr_realpow bheight_size_bound rbt_def) 

309 
finally have "2 powr (height t / 2) \<le> size1 t" . 

310 
hence "height t / 2 \<le> log 2 (size1 t)" 

68999  311 
by (simp add: le_log_iff size1_size del: divide_le_eq_numeral1(1)) 
64950  312 
thus ?thesis by simp 
313 
qed 

314 

61224  315 
end 