49 "insert x (Node h l a r) = (case cmp x a of |
49 "insert x (Node h l a r) = (case cmp x a of |
50 EQ \<Rightarrow> Node h l a r | |
50 EQ \<Rightarrow> Node h l a r | |
51 LT \<Rightarrow> balL (insert x l) a r | |
51 LT \<Rightarrow> balL (insert x l) a r | |
52 GT \<Rightarrow> balR l a (insert x r))" |
52 GT \<Rightarrow> balR l a (insert x r))" |
53 |
53 |
54 fun delete_max :: "'a avl_tree \<Rightarrow> 'a avl_tree * 'a" where |
54 fun del_max :: "'a avl_tree \<Rightarrow> 'a avl_tree * 'a" where |
55 "delete_max (Node _ l a Leaf) = (l,a)" | |
55 "del_max (Node _ l a r) = (if r = Leaf then (l,a) |
56 "delete_max (Node _ l a r) = |
56 else let (r',a') = del_max r in (balL l a r', a'))" |
57 (let (r',a') = delete_max r in (balL l a r', a'))" |
57 |
58 |
58 lemmas del_max_induct = del_max.induct[case_names Node Leaf] |
59 lemmas delete_max_induct = delete_max.induct[case_names Leaf Node] |
59 |
60 |
60 fun del_root :: "'a avl_tree \<Rightarrow> 'a avl_tree" where |
61 fun delete_root :: "'a avl_tree \<Rightarrow> 'a avl_tree" where |
61 "del_root (Node h Leaf a r) = r" | |
62 "delete_root (Node h Leaf a r) = r" | |
62 "del_root (Node h l a Leaf) = l" | |
63 "delete_root (Node h l a Leaf) = l" | |
63 "del_root (Node h l a r) = (let (l', a') = del_max l in balR l' a' r)" |
64 "delete_root (Node h l a r) = |
64 |
65 (let (l', a') = delete_max l in balR l' a' r)" |
65 lemmas del_root_cases = del_root.cases[case_names Leaf_t Node_Leaf Node_Node] |
66 |
|
67 lemmas delete_root_cases = delete_root.cases[case_names Leaf_t Node_Leaf Node_Node] |
|
68 |
66 |
69 fun delete :: "'a::cmp \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where |
67 fun delete :: "'a::cmp \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where |
70 "delete _ Leaf = Leaf" | |
68 "delete _ Leaf = Leaf" | |
71 "delete x (Node h l a r) = (case cmp x a of |
69 "delete x (Node h l a r) = (case cmp x a of |
72 EQ \<Rightarrow> delete_root (Node h l a r) | |
70 EQ \<Rightarrow> del_root (Node h l a r) | |
73 LT \<Rightarrow> balR (delete x l) a r | |
71 LT \<Rightarrow> balR (delete x l) a r | |
74 GT \<Rightarrow> balL l a (delete x r))" |
72 GT \<Rightarrow> balL l a (delete x r))" |
75 |
73 |
76 |
74 |
77 subsection {* Functional Correctness Proofs *} |
75 subsection {* Functional Correctness Proofs *} |
95 (auto simp: ins_list_simps inorder_balL inorder_balR) |
93 (auto simp: ins_list_simps inorder_balL inorder_balR) |
96 |
94 |
97 |
95 |
98 subsubsection "Proofs for delete" |
96 subsubsection "Proofs for delete" |
99 |
97 |
100 lemma inorder_delete_maxD: |
98 lemma inorder_del_maxD: |
101 "\<lbrakk> delete_max t = (t',a); t \<noteq> Leaf \<rbrakk> \<Longrightarrow> |
99 "\<lbrakk> del_max t = (t',a); t \<noteq> Leaf \<rbrakk> \<Longrightarrow> |
102 inorder t' @ [a] = inorder t" |
100 inorder t' @ [a] = inorder t" |
103 by(induction t arbitrary: t' rule: delete_max.induct) |
101 by(induction t arbitrary: t' rule: del_max.induct) |
104 (auto simp: inorder_balL split: prod.splits tree.split) |
102 (auto simp: inorder_balL split: if_splits prod.splits tree.split) |
105 |
103 |
106 lemma inorder_delete_root: |
104 lemma inorder_del_root: |
107 "inorder (delete_root (Node h l a r)) = inorder l @ inorder r" |
105 "inorder (del_root (Node h l a r)) = inorder l @ inorder r" |
108 by(induction "Node h l a r" arbitrary: l a r h rule: delete_root.induct) |
106 by(induction "Node h l a r" arbitrary: l a r h rule: del_root.induct) |
109 (auto simp: inorder_balR inorder_delete_maxD split: prod.splits) |
107 (auto simp: inorder_balL inorder_balR inorder_del_maxD split: if_splits prod.splits) |
110 |
108 |
111 theorem inorder_delete: |
109 theorem inorder_delete: |
112 "sorted(inorder t) \<Longrightarrow> inorder (delete x t) = del_list x (inorder t)" |
110 "sorted(inorder t) \<Longrightarrow> inorder (delete x t) = del_list x (inorder t)" |
113 by(induction t) |
111 by(induction t) |
114 (auto simp: del_list_simps inorder_balL inorder_balR |
112 (auto simp: del_list_simps inorder_balL inorder_balR |
115 inorder_delete_root inorder_delete_maxD split: prod.splits) |
113 inorder_del_root inorder_del_maxD split: prod.splits) |
116 |
114 |
117 |
115 |
118 subsubsection "Overall functional correctness" |
116 subsubsection "Overall functional correctness" |
119 |
117 |
120 interpretation Set_by_Ordered |
118 interpretation Set_by_Ordered |
293 qed simp_all |
291 qed simp_all |
294 |
292 |
295 |
293 |
296 subsubsection {* Deletion maintains AVL balance *} |
294 subsubsection {* Deletion maintains AVL balance *} |
297 |
295 |
298 lemma avl_delete_max: |
296 lemma avl_del_max: |
299 assumes "avl x" and "x \<noteq> Leaf" |
297 assumes "avl x" and "x \<noteq> Leaf" |
300 shows "avl (fst (delete_max x))" "height x = height(fst (delete_max x)) \<or> |
298 shows "avl (fst (del_max x))" "height x = height(fst (del_max x)) \<or> |
301 height x = height(fst (delete_max x)) + 1" |
299 height x = height(fst (del_max x)) + 1" |
302 using assms |
300 using assms |
303 proof (induct x rule: delete_max_induct) |
301 proof (induct x rule: del_max_induct) |
304 case (Node h l a rh rl b rr) |
302 case (Node h l a r) |
305 case 1 |
303 case 1 |
306 with Node have "avl l" "avl (fst (delete_max (Node rh rl b rr)))" by auto |
304 thus ?case using Node |
307 with 1 Node have "avl (balL l a (fst (delete_max (Node rh rl b rr))))" |
305 by (auto simp: height_balL height_balL2 avl_balL |
308 by (intro avl_balL) fastforce+ |
|
309 thus ?case |
|
310 by (auto simp: height_balL height_balL2 |
|
311 linorder_class.max.absorb1 linorder_class.max.absorb2 |
306 linorder_class.max.absorb1 linorder_class.max.absorb2 |
312 split:prod.split) |
307 split:prod.split) |
313 next |
308 next |
314 case (Node h l a rh rl b rr) |
309 case (Node h l a r) |
315 case 2 |
310 case 2 |
316 let ?r = "Node rh rl b rr" |
311 let ?r' = "fst (del_max r)" |
317 let ?r' = "fst (delete_max ?r)" |
312 from `avl x` Node 2 have "avl l" and "avl r" by simp_all |
318 from `avl x` Node 2 have "avl l" and "avl ?r" by simp_all |
|
319 thus ?case using Node 2 height_balL[of l ?r' a] height_balL2[of l ?r' a] |
313 thus ?case using Node 2 height_balL[of l ?r' a] height_balL2[of l ?r' a] |
320 apply (auto split:prod.splits simp del:avl.simps) by arith+ |
314 apply (auto split:prod.splits simp del:avl.simps) by arith+ |
321 qed auto |
315 qed auto |
322 |
316 |
323 lemma avl_delete_root: |
317 lemma avl_del_root: |
324 assumes "avl t" and "t \<noteq> Leaf" |
318 assumes "avl t" and "t \<noteq> Leaf" |
325 shows "avl(delete_root t)" |
319 shows "avl(del_root t)" |
326 using assms |
320 using assms |
327 proof (cases t rule:delete_root_cases) |
321 proof (cases t rule:del_root_cases) |
328 case (Node_Node h lh ll ln lr n rh rl rn rr) |
322 case (Node_Node h lh ll ln lr n rh rl rn rr) |
329 let ?l = "Node lh ll ln lr" |
323 let ?l = "Node lh ll ln lr" |
330 let ?r = "Node rh rl rn rr" |
324 let ?r = "Node rh rl rn rr" |
331 let ?l' = "fst (delete_max ?l)" |
325 let ?l' = "fst (del_max ?l)" |
332 from `avl t` and Node_Node have "avl ?r" by simp |
326 from `avl t` and Node_Node have "avl ?r" by simp |
333 from `avl t` and Node_Node have "avl ?l" by simp |
327 from `avl t` and Node_Node have "avl ?l" by simp |
334 hence "avl(?l')" "height ?l = height(?l') \<or> |
328 hence "avl(?l')" "height ?l = height(?l') \<or> |
335 height ?l = height(?l') + 1" by (rule avl_delete_max,simp)+ |
329 height ?l = height(?l') + 1" by (rule avl_del_max,simp)+ |
336 with `avl t` Node_Node have "height ?l' = height ?r \<or> height ?l' = height ?r + 1 |
330 with `avl t` Node_Node have "height ?l' = height ?r \<or> height ?l' = height ?r + 1 |
337 \<or> height ?r = height ?l' + 1 \<or> height ?r = height ?l' + 2" by fastforce |
331 \<or> height ?r = height ?l' + 1 \<or> height ?r = height ?l' + 2" by fastforce |
338 with `avl ?l'` `avl ?r` have "avl(balR ?l' (snd(delete_max ?l)) ?r)" |
332 with `avl ?l'` `avl ?r` have "avl(balR ?l' (snd(del_max ?l)) ?r)" |
339 by (rule avl_balR) |
333 by (rule avl_balR) |
340 with Node_Node show ?thesis by (auto split:prod.splits) |
334 with Node_Node show ?thesis by (auto split:prod.splits) |
341 qed simp_all |
335 qed simp_all |
342 |
336 |
343 lemma height_delete_root: |
337 lemma height_del_root: |
344 assumes "avl t" and "t \<noteq> Leaf" |
338 assumes "avl t" and "t \<noteq> Leaf" |
345 shows "height t = height(delete_root t) \<or> height t = height(delete_root t) + 1" |
339 shows "height t = height(del_root t) \<or> height t = height(del_root t) + 1" |
346 using assms |
340 using assms |
347 proof (cases t rule: delete_root_cases) |
341 proof (cases t rule: del_root_cases) |
348 case (Node_Node h lh ll ln lr n rh rl rn rr) |
342 case (Node_Node h lh ll ln lr n rh rl rn rr) |
349 let ?l = "Node lh ll ln lr" |
343 let ?l = "Node lh ll ln lr" |
350 let ?r = "Node rh rl rn rr" |
344 let ?r = "Node rh rl rn rr" |
351 let ?l' = "fst (delete_max ?l)" |
345 let ?l' = "fst (del_max ?l)" |
352 let ?t' = "balR ?l' (snd(delete_max ?l)) ?r" |
346 let ?t' = "balR ?l' (snd(del_max ?l)) ?r" |
353 from `avl t` and Node_Node have "avl ?r" by simp |
347 from `avl t` and Node_Node have "avl ?r" by simp |
354 from `avl t` and Node_Node have "avl ?l" by simp |
348 from `avl t` and Node_Node have "avl ?l" by simp |
355 hence "avl(?l')" by (rule avl_delete_max,simp) |
349 hence "avl(?l')" by (rule avl_del_max,simp) |
356 have l'_height: "height ?l = height ?l' \<or> height ?l = height ?l' + 1" using `avl ?l` by (intro avl_delete_max) auto |
350 have l'_height: "height ?l = height ?l' \<or> height ?l = height ?l' + 1" using `avl ?l` by (intro avl_del_max) auto |
357 have t_height: "height t = 1 + max (height ?l) (height ?r)" using `avl t` Node_Node by simp |
351 have t_height: "height t = 1 + max (height ?l) (height ?r)" using `avl t` Node_Node by simp |
358 have "height t = height ?t' \<or> height t = height ?t' + 1" using `avl t` Node_Node |
352 have "height t = height ?t' \<or> height t = height ?t' + 1" using `avl t` Node_Node |
359 proof(cases "height ?r = height ?l' + 2") |
353 proof(cases "height ?r = height ?l' + 2") |
360 case False |
354 case False |
361 show ?thesis using l'_height t_height False by (subst height_balR2[OF `avl ?l'` `avl ?r` False])+ arith |
355 show ?thesis using l'_height t_height False by (subst height_balR2[OF `avl ?l'` `avl ?r` False])+ arith |
362 next |
356 next |
363 case True |
357 case True |
364 show ?thesis |
358 show ?thesis |
365 proof(cases rule: disjE[OF height_balR[OF True `avl ?l'` `avl ?r`, of "snd (delete_max ?l)"]]) |
359 proof(cases rule: disjE[OF height_balR[OF True `avl ?l'` `avl ?r`, of "snd (del_max ?l)"]]) |
366 case 1 |
360 case 1 |
367 thus ?thesis using l'_height t_height True by arith |
361 thus ?thesis using l'_height t_height True by arith |
368 next |
362 next |
369 case 2 |
363 case 2 |
370 thus ?thesis using l'_height t_height True by arith |
364 thus ?thesis using l'_height t_height True by arith |