author | wenzelm |
Tue, 05 Nov 2019 14:28:00 +0100 | |
changeset 71047 | 87c132cf5860 |
parent 70755 | 3fb16bed5d6c |
child 71346 | 7a0a6c56015e |
permissions | -rw-r--r-- |
64951
140addd19343
removed contribution by Daniel Stuewe, too detailed.
nipkow
parents:
64950
diff
changeset
|
1 |
(* Author: Tobias Nipkow *) |
61224 | 2 |
|
3 |
section \<open>Red-Black 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 height-size 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 height-size 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" | |
|
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70708
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" | |
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70708
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 height-size 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 height-size 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" | |
|
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70708
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 height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
105 |
fun invc :: "'a rbt \<Rightarrow> bool" where |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
106 |
"invc Leaf = True" | |
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70708
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 |
|
70708 | 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 height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
114 |
fun invh :: "'a rbt \<Rightarrow> bool" where |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
115 |
"invh Leaf = True" | |
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70708
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" |
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70708
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 height-size 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 |
||
70708 | 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 height-size 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 |
|
70708 | 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 |
||
70708 | 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 |
|
70708 | 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 height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
176 |
theorem rbt_insert: "rbt t \<Longrightarrow> rbt (insert x t)" |
70708 | 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 height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
189 |
|
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
190 |
subsubsection \<open>Deletion\<close> |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
191 |
|
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
192 |
lemma bheight_paint_Red: |
e051eea34990
got rid of class cmp; added height-size 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)" |
70708 | 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 |
|
70571 | 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 |
|
70571 | 222 |
lemma invc2_baldR: "\<lbrakk> invc l; invc2 r \<rbrakk> \<Longrightarrow>invc2 (baldR l a r)" |
70708 | 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 height-size 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 height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
231 |
lemma invc_combine: |
70708 | 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 |
|
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70708
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:
70708
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) |
|
68413 | 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 height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
248 |
with 2 show ?thesis |
e051eea34990
got rid of class cmp; added height-size 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 |
||
70571 | 263 |
theorem rbt_delete: "rbt t \<Longrightarrow> rbt (delete x t)" |
70708 | 264 |
by (metis delete_def rbt_def color_paint_Black del_invc_invh invc2I invh_paint) |
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
265 |
|
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
266 |
text \<open>Overall correctness:\<close> |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
267 |
|
68440 | 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 height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
270 |
and inorder = inorder and inv = rbt |
e051eea34990
got rid of class cmp; added height-size 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 height-size 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 height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
275 |
next |
e051eea34990
got rid of class cmp; added height-size 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 height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
277 |
next |
e051eea34990
got rid of class cmp; added height-size 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 height-size 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 height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
281 |
next |
e051eea34990
got rid of class cmp; added height-size 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 height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
283 |
next |
e051eea34990
got rid of class cmp; added height-size 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 height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
285 |
qed |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
286 |
|
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
287 |
|
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
288 |
subsection \<open>Height-Size Relation\<close> |
e051eea34990
got rid of class cmp; added height-size 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> |
64950 | 294 |
height t \<le> (if color t = Black then 2 * bheight t else 2 * bheight t + 1)" |
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)" |
|
68998 | 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 |