61232
|
1 |
(*
|
|
2 |
Author: Tobias Nipkow
|
|
3 |
Derived from AFP entry AVL.
|
|
4 |
*)
|
|
5 |
|
|
6 |
section "AVL Tree Implementation of Sets"
|
|
7 |
|
|
8 |
theory AVL_Set
|
|
9 |
imports Isin2
|
|
10 |
begin
|
|
11 |
|
|
12 |
type_synonym 'a avl_tree = "('a,nat) tree"
|
|
13 |
|
|
14 |
text {* Invariant: *}
|
|
15 |
|
|
16 |
fun avl :: "'a avl_tree \<Rightarrow> bool" where
|
|
17 |
"avl Leaf = True" |
|
|
18 |
"avl (Node h l a r) =
|
|
19 |
((height l = height r \<or> height l = height r + 1 \<or> height r = height l + 1) \<and>
|
|
20 |
h = max (height l) (height r) + 1 \<and> avl l \<and> avl r)"
|
|
21 |
|
|
22 |
fun ht :: "'a avl_tree \<Rightarrow> nat" where
|
|
23 |
"ht Leaf = 0" |
|
|
24 |
"ht (Node h l a r) = h"
|
|
25 |
|
|
26 |
definition node :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
|
|
27 |
"node l a r = Node (max (ht l) (ht r) + 1) l a r"
|
|
28 |
|
|
29 |
definition node_bal_l :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
|
|
30 |
"node_bal_l l a r = (
|
|
31 |
if ht l = ht r + 2 then (case l of
|
|
32 |
Node _ bl b br \<Rightarrow> (if ht bl < ht br
|
|
33 |
then case br of
|
|
34 |
Node _ cl c cr \<Rightarrow> node (node bl b cl) c (node cr a r)
|
|
35 |
else node bl b (node br a r)))
|
|
36 |
else node l a r)"
|
|
37 |
|
|
38 |
definition node_bal_r :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
|
|
39 |
"node_bal_r l a r = (
|
|
40 |
if ht r = ht l + 2 then (case r of
|
|
41 |
Node _ bl b br \<Rightarrow> (if ht bl > ht br
|
|
42 |
then case bl of
|
|
43 |
Node _ cl c cr \<Rightarrow> node (node l a cl) c (node cr b br)
|
|
44 |
else node (node l a bl) b br))
|
|
45 |
else node l a r)"
|
|
46 |
|
|
47 |
fun insert :: "'a::order \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
|
|
48 |
"insert x Leaf = Node 1 Leaf x Leaf" |
|
|
49 |
"insert x (Node h l a r) =
|
|
50 |
(if x=a then Node h l a r
|
|
51 |
else if x<a
|
|
52 |
then node_bal_l (insert x l) a r
|
|
53 |
else node_bal_r l a (insert x r))"
|
|
54 |
|
|
55 |
fun delete_max :: "'a avl_tree \<Rightarrow> 'a avl_tree * 'a" where
|
|
56 |
"delete_max (Node _ l a Leaf) = (l,a)" |
|
|
57 |
"delete_max (Node _ l a r) = (
|
|
58 |
let (r',a') = delete_max r in
|
|
59 |
(node_bal_l l a r', a'))"
|
|
60 |
|
|
61 |
lemmas delete_max_induct = delete_max.induct[case_names Leaf Node]
|
|
62 |
|
|
63 |
fun delete_root :: "'a avl_tree \<Rightarrow> 'a avl_tree" where
|
|
64 |
"delete_root (Node h Leaf a r) = r" |
|
|
65 |
"delete_root (Node h l a Leaf) = l" |
|
|
66 |
"delete_root (Node h l a r) =
|
|
67 |
(let (l', a') = delete_max l in node_bal_r l' a' r)"
|
|
68 |
|
|
69 |
lemmas delete_root_cases = delete_root.cases[case_names Leaf_t Node_Leaf Node_Node]
|
|
70 |
|
|
71 |
fun delete :: "'a::order \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
|
|
72 |
"delete _ Leaf = Leaf" |
|
|
73 |
"delete x (Node h l a r) = (
|
|
74 |
if x = a then delete_root (Node h l a r)
|
|
75 |
else if x < a then node_bal_r (delete x l) a r
|
|
76 |
else node_bal_l l a (delete x r))"
|
|
77 |
|
|
78 |
|
|
79 |
subsection {* Functional Correctness Proofs *}
|
|
80 |
|
|
81 |
text{* Very different from the AFP/AVL proofs *}
|
|
82 |
|
|
83 |
|
|
84 |
subsubsection "Proofs for insert"
|
|
85 |
|
|
86 |
lemma inorder_node_bal_l:
|
|
87 |
"inorder (node_bal_l l a r) = inorder l @ a # inorder r"
|
|
88 |
by (auto simp: node_def node_bal_l_def split:tree.splits)
|
|
89 |
|
|
90 |
lemma inorder_node_bal_r:
|
|
91 |
"inorder (node_bal_r l a r) = inorder l @ a # inorder r"
|
|
92 |
by (auto simp: node_def node_bal_r_def split:tree.splits)
|
|
93 |
|
|
94 |
theorem inorder_insert:
|
|
95 |
"sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
|
|
96 |
by (induct t)
|
|
97 |
(auto simp: ins_list_simps inorder_node_bal_l inorder_node_bal_r)
|
|
98 |
|
|
99 |
|
|
100 |
subsubsection "Proofs for delete"
|
|
101 |
|
|
102 |
lemma inorder_delete_maxD:
|
|
103 |
"\<lbrakk> delete_max t = (t',a); t \<noteq> Leaf \<rbrakk> \<Longrightarrow>
|
|
104 |
inorder t' @ [a] = inorder t"
|
|
105 |
by(induction t arbitrary: t' rule: delete_max.induct)
|
|
106 |
(auto simp: inorder_node_bal_l split: prod.splits tree.split)
|
|
107 |
|
|
108 |
lemma inorder_delete_root:
|
|
109 |
"inorder (delete_root (Node h l a r)) = inorder l @ inorder r"
|
|
110 |
by(induction "Node h l a r" arbitrary: l a r h rule: delete_root.induct)
|
|
111 |
(auto simp: inorder_node_bal_r inorder_delete_maxD split: prod.splits)
|
|
112 |
|
|
113 |
theorem inorder_delete:
|
|
114 |
"sorted(inorder t) \<Longrightarrow> inorder (delete x t) = del_list x (inorder t)"
|
|
115 |
by(induction t)
|
|
116 |
(auto simp: del_list_simps inorder_node_bal_l inorder_node_bal_r
|
|
117 |
inorder_delete_root inorder_delete_maxD split: prod.splits)
|
|
118 |
|
|
119 |
|
|
120 |
subsubsection "Overall functional correctness"
|
|
121 |
|
|
122 |
interpretation Set_by_Ordered
|
|
123 |
where empty = Leaf and isin = isin and insert = insert and delete = delete
|
|
124 |
and inorder = inorder and wf = "\<lambda>_. True"
|
|
125 |
proof (standard, goal_cases)
|
|
126 |
case 1 show ?case by simp
|
|
127 |
next
|
|
128 |
case 2 thus ?case by(simp add: isin_set)
|
|
129 |
next
|
|
130 |
case 3 thus ?case by(simp add: inorder_insert)
|
|
131 |
next
|
|
132 |
case 4 thus ?case by(simp add: inorder_delete)
|
61428
|
133 |
qed (rule TrueI)+
|
61232
|
134 |
|
|
135 |
|
|
136 |
subsection {* AVL invariants *}
|
|
137 |
|
|
138 |
text{* Essentially the AFP/AVL proofs *}
|
|
139 |
|
|
140 |
|
|
141 |
subsubsection {* Insertion maintains AVL balance *}
|
|
142 |
|
|
143 |
declare Let_def [simp]
|
|
144 |
|
|
145 |
lemma [simp]: "avl t \<Longrightarrow> ht t = height t"
|
|
146 |
by (induct t) simp_all
|
|
147 |
|
|
148 |
lemma height_node_bal_l:
|
|
149 |
"\<lbrakk> height l = height r + 2; avl l; avl r \<rbrakk> \<Longrightarrow>
|
|
150 |
height (node_bal_l l a r) = height r + 2 \<or>
|
|
151 |
height (node_bal_l l a r) = height r + 3"
|
|
152 |
by (cases l) (auto simp:node_def node_bal_l_def split:tree.split)
|
|
153 |
|
|
154 |
lemma height_node_bal_r:
|
|
155 |
"\<lbrakk> height r = height l + 2; avl l; avl r \<rbrakk> \<Longrightarrow>
|
|
156 |
height (node_bal_r l a r) = height l + 2 \<or>
|
|
157 |
height (node_bal_r l a r) = height l + 3"
|
|
158 |
by (cases r) (auto simp add:node_def node_bal_r_def split:tree.split)
|
|
159 |
|
|
160 |
lemma [simp]: "height(node l a r) = max (height l) (height r) + 1"
|
|
161 |
by (simp add: node_def)
|
|
162 |
|
|
163 |
lemma avl_node:
|
|
164 |
"\<lbrakk> avl l; avl r;
|
|
165 |
height l = height r \<or> height l = height r + 1 \<or> height r = height l + 1
|
|
166 |
\<rbrakk> \<Longrightarrow> avl(node l a r)"
|
|
167 |
by (auto simp add:max_def node_def)
|
|
168 |
|
|
169 |
lemma height_node_bal_l2:
|
|
170 |
"\<lbrakk> avl l; avl r; height l \<noteq> height r + 2 \<rbrakk> \<Longrightarrow>
|
|
171 |
height (node_bal_l l a r) = (1 + max (height l) (height r))"
|
|
172 |
by (cases l, cases r) (simp_all add: node_bal_l_def)
|
|
173 |
|
|
174 |
lemma height_node_bal_r2:
|
|
175 |
"\<lbrakk> avl l; avl r; height r \<noteq> height l + 2 \<rbrakk> \<Longrightarrow>
|
|
176 |
height (node_bal_r l a r) = (1 + max (height l) (height r))"
|
|
177 |
by (cases l, cases r) (simp_all add: node_bal_r_def)
|
|
178 |
|
|
179 |
lemma avl_node_bal_l:
|
|
180 |
assumes "avl l" "avl r" and "height l = height r \<or> height l = height r + 1
|
|
181 |
\<or> height r = height l + 1 \<or> height l = height r + 2"
|
|
182 |
shows "avl(node_bal_l l a r)"
|
|
183 |
proof(cases l)
|
|
184 |
case Leaf
|
|
185 |
with assms show ?thesis by (simp add: node_def node_bal_l_def)
|
|
186 |
next
|
|
187 |
case (Node ln ll lr lh)
|
|
188 |
with assms show ?thesis
|
|
189 |
proof(cases "height l = height r + 2")
|
|
190 |
case True
|
|
191 |
from True Node assms show ?thesis
|
|
192 |
by (auto simp: node_bal_l_def intro!: avl_node split: tree.split) arith+
|
|
193 |
next
|
|
194 |
case False
|
|
195 |
with assms show ?thesis by (simp add: avl_node node_bal_l_def)
|
|
196 |
qed
|
|
197 |
qed
|
|
198 |
|
|
199 |
lemma avl_node_bal_r:
|
|
200 |
assumes "avl l" and "avl r" and "height l = height r \<or> height l = height r + 1
|
|
201 |
\<or> height r = height l + 1 \<or> height r = height l + 2"
|
|
202 |
shows "avl(node_bal_r l a r)"
|
|
203 |
proof(cases r)
|
|
204 |
case Leaf
|
|
205 |
with assms show ?thesis by (simp add: node_def node_bal_r_def)
|
|
206 |
next
|
|
207 |
case (Node rn rl rr rh)
|
|
208 |
with assms show ?thesis
|
|
209 |
proof(cases "height r = height l + 2")
|
|
210 |
case True
|
|
211 |
from True Node assms show ?thesis
|
|
212 |
by (auto simp: node_bal_r_def intro!: avl_node split: tree.split) arith+
|
|
213 |
next
|
|
214 |
case False
|
|
215 |
with assms show ?thesis by (simp add: node_bal_r_def avl_node)
|
|
216 |
qed
|
|
217 |
qed
|
|
218 |
|
|
219 |
(* It appears that these two properties need to be proved simultaneously: *)
|
|
220 |
|
|
221 |
text{* Insertion maintains the AVL property: *}
|
|
222 |
|
|
223 |
theorem avl_insert_aux:
|
|
224 |
assumes "avl t"
|
|
225 |
shows "avl(insert x t)"
|
|
226 |
"(height (insert x t) = height t \<or> height (insert x t) = height t + 1)"
|
|
227 |
using assms
|
|
228 |
proof (induction t)
|
|
229 |
case (Node h l a r)
|
|
230 |
case 1
|
|
231 |
with Node show ?case
|
|
232 |
proof(cases "x = a")
|
|
233 |
case True
|
|
234 |
with Node 1 show ?thesis by simp
|
|
235 |
next
|
|
236 |
case False
|
|
237 |
with Node 1 show ?thesis
|
|
238 |
proof(cases "x<a")
|
|
239 |
case True
|
|
240 |
with Node 1 show ?thesis by (auto simp add:avl_node_bal_l)
|
|
241 |
next
|
|
242 |
case False
|
|
243 |
with Node 1 `x\<noteq>a` show ?thesis by (auto simp add:avl_node_bal_r)
|
|
244 |
qed
|
|
245 |
qed
|
|
246 |
case 2
|
|
247 |
from 2 Node show ?case
|
|
248 |
proof(cases "x = a")
|
|
249 |
case True
|
|
250 |
with Node 1 show ?thesis by simp
|
|
251 |
next
|
|
252 |
case False
|
|
253 |
with Node 1 show ?thesis
|
|
254 |
proof(cases "x<a")
|
|
255 |
case True
|
|
256 |
with Node 2 show ?thesis
|
|
257 |
proof(cases "height (insert x l) = height r + 2")
|
|
258 |
case False with Node 2 `x < a` show ?thesis by (auto simp: height_node_bal_l2)
|
|
259 |
next
|
|
260 |
case True
|
|
261 |
hence "(height (node_bal_l (insert x l) a r) = height r + 2) \<or>
|
|
262 |
(height (node_bal_l (insert x l) a r) = height r + 3)" (is "?A \<or> ?B")
|
|
263 |
using Node 2 by (intro height_node_bal_l) simp_all
|
|
264 |
thus ?thesis
|
|
265 |
proof
|
|
266 |
assume ?A
|
|
267 |
with 2 `x < a` show ?thesis by (auto)
|
|
268 |
next
|
|
269 |
assume ?B
|
|
270 |
with True 1 Node(2) `x < a` show ?thesis by (simp) arith
|
|
271 |
qed
|
|
272 |
qed
|
|
273 |
next
|
|
274 |
case False
|
|
275 |
with Node 2 show ?thesis
|
|
276 |
proof(cases "height (insert x r) = height l + 2")
|
|
277 |
case False
|
|
278 |
with Node 2 `\<not>x < a` show ?thesis by (auto simp: height_node_bal_r2)
|
|
279 |
next
|
|
280 |
case True
|
|
281 |
hence "(height (node_bal_r l a (insert x r)) = height l + 2) \<or>
|
|
282 |
(height (node_bal_r l a (insert x r)) = height l + 3)" (is "?A \<or> ?B")
|
|
283 |
using Node 2 by (intro height_node_bal_r) simp_all
|
|
284 |
thus ?thesis
|
|
285 |
proof
|
|
286 |
assume ?A
|
|
287 |
with 2 `\<not>x < a` show ?thesis by (auto)
|
|
288 |
next
|
|
289 |
assume ?B
|
|
290 |
with True 1 Node(4) `\<not>x < a` show ?thesis by (simp) arith
|
|
291 |
qed
|
|
292 |
qed
|
|
293 |
qed
|
|
294 |
qed
|
|
295 |
qed simp_all
|
|
296 |
|
|
297 |
|
|
298 |
subsubsection {* Deletion maintains AVL balance *}
|
|
299 |
|
|
300 |
lemma avl_delete_max:
|
|
301 |
assumes "avl x" and "x \<noteq> Leaf"
|
|
302 |
shows "avl (fst (delete_max x))" "height x = height(fst (delete_max x)) \<or>
|
|
303 |
height x = height(fst (delete_max x)) + 1"
|
|
304 |
using assms
|
|
305 |
proof (induct x rule: delete_max_induct)
|
|
306 |
case (Node h l a rh rl b rr)
|
|
307 |
case 1
|
|
308 |
with Node have "avl l" "avl (fst (delete_max (Node rh rl b rr)))" by auto
|
|
309 |
with 1 Node have "avl (node_bal_l l a (fst (delete_max (Node rh rl b rr))))"
|
|
310 |
by (intro avl_node_bal_l) fastforce+
|
|
311 |
thus ?case
|
|
312 |
by (auto simp: height_node_bal_l height_node_bal_l2
|
|
313 |
linorder_class.max.absorb1 linorder_class.max.absorb2
|
|
314 |
split:prod.split)
|
|
315 |
next
|
|
316 |
case (Node h l a rh rl b rr)
|
|
317 |
case 2
|
|
318 |
let ?r = "Node rh rl b rr"
|
|
319 |
let ?r' = "fst (delete_max ?r)"
|
|
320 |
from `avl x` Node 2 have "avl l" and "avl ?r" by simp_all
|
|
321 |
thus ?case using Node 2 height_node_bal_l[of l ?r' a] height_node_bal_l2[of l ?r' a]
|
|
322 |
apply (auto split:prod.splits simp del:avl.simps) by arith+
|
|
323 |
qed auto
|
|
324 |
|
|
325 |
lemma avl_delete_root:
|
|
326 |
assumes "avl t" and "t \<noteq> Leaf"
|
|
327 |
shows "avl(delete_root t)"
|
|
328 |
using assms
|
|
329 |
proof (cases t rule:delete_root_cases)
|
|
330 |
case (Node_Node h lh ll ln lr n rh rl rn rr)
|
|
331 |
let ?l = "Node lh ll ln lr"
|
|
332 |
let ?r = "Node rh rl rn rr"
|
|
333 |
let ?l' = "fst (delete_max ?l)"
|
|
334 |
from `avl t` and Node_Node have "avl ?r" by simp
|
|
335 |
from `avl t` and Node_Node have "avl ?l" by simp
|
|
336 |
hence "avl(?l')" "height ?l = height(?l') \<or>
|
|
337 |
height ?l = height(?l') + 1" by (rule avl_delete_max,simp)+
|
|
338 |
with `avl t` Node_Node have "height ?l' = height ?r \<or> height ?l' = height ?r + 1
|
|
339 |
\<or> height ?r = height ?l' + 1 \<or> height ?r = height ?l' + 2" by fastforce
|
|
340 |
with `avl ?l'` `avl ?r` have "avl(node_bal_r ?l' (snd(delete_max ?l)) ?r)"
|
|
341 |
by (rule avl_node_bal_r)
|
|
342 |
with Node_Node show ?thesis by (auto split:prod.splits)
|
|
343 |
qed simp_all
|
|
344 |
|
|
345 |
lemma height_delete_root:
|
|
346 |
assumes "avl t" and "t \<noteq> Leaf"
|
|
347 |
shows "height t = height(delete_root t) \<or> height t = height(delete_root t) + 1"
|
|
348 |
using assms
|
|
349 |
proof (cases t rule: delete_root_cases)
|
|
350 |
case (Node_Node h lh ll ln lr n rh rl rn rr)
|
|
351 |
let ?l = "Node lh ll ln lr"
|
|
352 |
let ?r = "Node rh rl rn rr"
|
|
353 |
let ?l' = "fst (delete_max ?l)"
|
|
354 |
let ?t' = "node_bal_r ?l' (snd(delete_max ?l)) ?r"
|
|
355 |
from `avl t` and Node_Node have "avl ?r" by simp
|
|
356 |
from `avl t` and Node_Node have "avl ?l" by simp
|
|
357 |
hence "avl(?l')" by (rule avl_delete_max,simp)
|
|
358 |
have l'_height: "height ?l = height ?l' \<or> height ?l = height ?l' + 1" using `avl ?l` by (intro avl_delete_max) auto
|
|
359 |
have t_height: "height t = 1 + max (height ?l) (height ?r)" using `avl t` Node_Node by simp
|
|
360 |
have "height t = height ?t' \<or> height t = height ?t' + 1" using `avl t` Node_Node
|
|
361 |
proof(cases "height ?r = height ?l' + 2")
|
|
362 |
case False
|
|
363 |
show ?thesis using l'_height t_height False by (subst height_node_bal_r2[OF `avl ?l'` `avl ?r` False])+ arith
|
|
364 |
next
|
|
365 |
case True
|
|
366 |
show ?thesis
|
|
367 |
proof(cases rule: disjE[OF height_node_bal_r[OF True `avl ?l'` `avl ?r`, of "snd (delete_max ?l)"]])
|
|
368 |
case 1
|
|
369 |
thus ?thesis using l'_height t_height True by arith
|
|
370 |
next
|
|
371 |
case 2
|
|
372 |
thus ?thesis using l'_height t_height True by arith
|
|
373 |
qed
|
|
374 |
qed
|
|
375 |
thus ?thesis using Node_Node by (auto split:prod.splits)
|
|
376 |
qed simp_all
|
|
377 |
|
|
378 |
text{* Deletion maintains the AVL property: *}
|
|
379 |
|
|
380 |
theorem avl_delete_aux:
|
|
381 |
assumes "avl t"
|
|
382 |
shows "avl(delete x t)" and "height t = (height (delete x t)) \<or> height t = height (delete x t) + 1"
|
|
383 |
using assms
|
|
384 |
proof (induct t)
|
|
385 |
case (Node h l n r)
|
|
386 |
case 1
|
|
387 |
with Node show ?case
|
|
388 |
proof(cases "x = n")
|
|
389 |
case True
|
|
390 |
with Node 1 show ?thesis by (auto simp:avl_delete_root)
|
|
391 |
next
|
|
392 |
case False
|
|
393 |
with Node 1 show ?thesis
|
|
394 |
proof(cases "x<n")
|
|
395 |
case True
|
|
396 |
with Node 1 show ?thesis by (auto simp add:avl_node_bal_r)
|
|
397 |
next
|
|
398 |
case False
|
|
399 |
with Node 1 `x\<noteq>n` show ?thesis by (auto simp add:avl_node_bal_l)
|
|
400 |
qed
|
|
401 |
qed
|
|
402 |
case 2
|
|
403 |
with Node show ?case
|
|
404 |
proof(cases "x = n")
|
|
405 |
case True
|
|
406 |
with 1 have "height (Node h l n r) = height(delete_root (Node h l n r))
|
|
407 |
\<or> height (Node h l n r) = height(delete_root (Node h l n r)) + 1"
|
|
408 |
by (subst height_delete_root,simp_all)
|
|
409 |
with True show ?thesis by simp
|
|
410 |
next
|
|
411 |
case False
|
|
412 |
with Node 1 show ?thesis
|
|
413 |
proof(cases "x<n")
|
|
414 |
case True
|
|
415 |
show ?thesis
|
|
416 |
proof(cases "height r = height (delete x l) + 2")
|
|
417 |
case False with Node 1 `x < n` show ?thesis by(auto simp: node_bal_r_def)
|
|
418 |
next
|
|
419 |
case True
|
|
420 |
hence "(height (node_bal_r (delete x l) n r) = height (delete x l) + 2) \<or>
|
|
421 |
height (node_bal_r (delete x l) n r) = height (delete x l) + 3" (is "?A \<or> ?B")
|
|
422 |
using Node 2 by (intro height_node_bal_r) auto
|
|
423 |
thus ?thesis
|
|
424 |
proof
|
|
425 |
assume ?A
|
|
426 |
with `x < n` Node 2 show ?thesis by(auto simp: node_bal_r_def)
|
|
427 |
next
|
|
428 |
assume ?B
|
|
429 |
with `x < n` Node 2 show ?thesis by(auto simp: node_bal_r_def)
|
|
430 |
qed
|
|
431 |
qed
|
|
432 |
next
|
|
433 |
case False
|
|
434 |
show ?thesis
|
|
435 |
proof(cases "height l = height (delete x r) + 2")
|
|
436 |
case False with Node 1 `\<not>x < n` `x \<noteq> n` show ?thesis by(auto simp: node_bal_l_def)
|
|
437 |
next
|
|
438 |
case True
|
|
439 |
hence "(height (node_bal_l l n (delete x r)) = height (delete x r) + 2) \<or>
|
|
440 |
height (node_bal_l l n (delete x r)) = height (delete x r) + 3" (is "?A \<or> ?B")
|
|
441 |
using Node 2 by (intro height_node_bal_l) auto
|
|
442 |
thus ?thesis
|
|
443 |
proof
|
|
444 |
assume ?A
|
|
445 |
with `\<not>x < n` `x \<noteq> n` Node 2 show ?thesis by(auto simp: node_bal_l_def)
|
|
446 |
next
|
|
447 |
assume ?B
|
|
448 |
with `\<not>x < n` `x \<noteq> n` Node 2 show ?thesis by(auto simp: node_bal_l_def)
|
|
449 |
qed
|
|
450 |
qed
|
|
451 |
qed
|
|
452 |
qed
|
|
453 |
qed simp_all
|
|
454 |
|
|
455 |
end
|