src/HOL/Data_Structures/RBT_Map.thy
 author nipkow Mon Jun 11 20:45:51 2018 +0200 (13 months ago) changeset 68415 d74ba11680d4 parent 68413 b56ed5010e69 child 68431 b294e095f64c permissions -rw-r--r--
tuned def. of del and proved preservation of rbt (finally)
 nipkow@61224 1 (* Author: Tobias Nipkow *) nipkow@61224 2 nipkow@61224 3 section \Red-Black Tree Implementation of Maps\ nipkow@61224 4 nipkow@61224 5 theory RBT_Map nipkow@61224 6 imports nipkow@61224 7 RBT_Set nipkow@61231 8 Lookup2 nipkow@61224 9 begin nipkow@61224 10 nipkow@63411 11 fun upd :: "'a::linorder \ 'b \ ('a*'b) rbt \ ('a*'b) rbt" where nipkow@61749 12 "upd x y Leaf = R Leaf (x,y) Leaf" | nipkow@61749 13 "upd x y (B l (a,b) r) = (case cmp x a of nipkow@64960 14 LT \ baliL (upd x y l) (a,b) r | nipkow@64960 15 GT \ baliR l (a,b) (upd x y r) | nipkow@61581 16 EQ \ B l (x,y) r)" | nipkow@61749 17 "upd x y (R l (a,b) r) = (case cmp x a of nipkow@61749 18 LT \ R (upd x y l) (a,b) r | nipkow@61749 19 GT \ R l (a,b) (upd x y r) | nipkow@61581 20 EQ \ R l (x,y) r)" nipkow@61224 21 nipkow@63411 22 definition update :: "'a::linorder \ 'b \ ('a*'b) rbt \ ('a*'b) rbt" where nipkow@61749 23 "update x y t = paint Black (upd x y t)" nipkow@61749 24 nipkow@68415 25 fun del :: "'a::linorder \ ('a*'b)rbt \ ('a*'b)rbt" where nipkow@61749 26 "del x Leaf = Leaf" | nipkow@68415 27 "del x (Node l (a,b) c r) = (case cmp x a of nipkow@68415 28 LT \ if l \ Leaf \ color l = Black nipkow@68415 29 then baldL (del x l) (a,b) r else R (del x l) (a,b) r | nipkow@68415 30 GT \ if r \ Leaf\ color r = Black nipkow@68415 31 then baldR l (a,b) (del x r) else R l (a,b) (del x r) | nipkow@68415 32 EQ \ combine l r)" nipkow@61749 33 nipkow@63411 34 definition delete :: "'a::linorder \ ('a*'b) rbt \ ('a*'b) rbt" where nipkow@61749 35 "delete x t = paint Black (del x t)" nipkow@61224 36 nipkow@61224 37 nipkow@61224 38 subsection "Functional Correctness Proofs" nipkow@61224 39 nipkow@61749 40 lemma inorder_upd: nipkow@61749 41 "sorted1(inorder t) \ inorder(upd x y t) = upd_list x y (inorder t)" nipkow@61749 42 by(induction x y t rule: upd.induct) nipkow@64960 43 (auto simp: upd_list_simps inorder_baliL inorder_baliR) nipkow@61749 44 nipkow@61224 45 lemma inorder_update: nipkow@61224 46 "sorted1(inorder t) \ inorder(update x y t) = upd_list x y (inorder t)" nipkow@61749 47 by(simp add: update_def inorder_upd inorder_paint) nipkow@61224 48 nipkow@61749 49 lemma inorder_del: nipkow@68415 50 "sorted1(inorder t) \ inorder(del x t) = del_list x (inorder t)" nipkow@68415 51 by(induction x t rule: del.induct) nipkow@64960 52 (auto simp: del_list_simps inorder_combine inorder_baldL inorder_baldR) nipkow@61224 53 nipkow@61224 54 lemma inorder_delete: nipkow@61749 55 "sorted1(inorder t) \ inorder(delete x t) = del_list x (inorder t)" nipkow@61749 56 by(simp add: delete_def inorder_del inorder_paint) nipkow@61224 57 nipkow@68415 58 nipkow@68415 59 subsection \Structural invariants\ nipkow@68415 60 nipkow@68415 61 subsubsection \Update\ nipkow@68415 62 nipkow@68415 63 lemma invc_upd: assumes "invc t" nipkow@68415 64 shows "color t = Black \ invc (upd x y t)" "invc2 (upd x y t)" nipkow@68415 65 using assms nipkow@68415 66 by (induct x y t rule: upd.induct) (auto simp: invc_baliL invc_baliR invc2I) nipkow@68415 67 nipkow@68415 68 lemma invh_upd: assumes "invh t" nipkow@68415 69 shows "invh (upd x y t)" "bheight (upd x y t) = bheight t" nipkow@68415 70 using assms nipkow@68415 71 by(induct x y t rule: upd.induct) nipkow@68415 72 (auto simp: invh_baliL invh_baliR bheight_baliL bheight_baliR) nipkow@68415 73 nipkow@68415 74 theorem rbt_update: "rbt t \ rbt (update x y t)" nipkow@68415 75 by (simp add: invc_upd(2) invh_upd(1) color_paint_Black invc_paint_Black invh_paint nipkow@68415 76 rbt_def update_def) nipkow@68415 77 nipkow@68415 78 nipkow@68415 79 subsubsection \Deletion\ nipkow@68415 80 nipkow@68415 81 lemma del_invc_invh: "invh t \ invc t \ invh (del x t) \ nipkow@68415 82 (color t = Red \ bheight (del x t) = bheight t \ invc (del x t) \ nipkow@68415 83 color t = Black \ bheight (del x t) = bheight t - 1 \ invc2 (del x t))" nipkow@68415 84 proof (induct x t rule: del.induct) nipkow@68415 85 case (2 x _ y _ c) nipkow@68415 86 have "x = y \ x < y \ x > y" by auto nipkow@68415 87 thus ?case proof (elim disjE) nipkow@68415 88 assume "x = y" nipkow@68415 89 with 2 show ?thesis nipkow@68415 90 by (cases c) (simp_all add: invh_combine invc_combine) nipkow@68415 91 next nipkow@68415 92 assume "x < y" nipkow@68415 93 with 2 show ?thesis nipkow@68415 94 by(cases c) nipkow@68415 95 (auto simp: invh_baldL_invc invc_baldL invc2_baldL dest: neq_LeafD) nipkow@68415 96 next nipkow@68415 97 assume "y < x" nipkow@68415 98 with 2 show ?thesis nipkow@68415 99 by(cases c) nipkow@68415 100 (auto simp: invh_baldR_invc invc_baldR invc2_baldR dest: neq_LeafD) nipkow@68415 101 qed nipkow@68415 102 qed auto nipkow@68415 103 nipkow@68415 104 theorem rbt_delete: "rbt t \ rbt (delete k t)" nipkow@68415 105 by (metis delete_def rbt_def color_paint_Black del_invc_invh invc_paint_Black invc2I invh_paint) nipkow@68415 106 nipkow@61224 107 interpretation Map_by_Ordered nipkow@61224 108 where empty = Leaf and lookup = lookup and update = update and delete = delete nipkow@68415 109 and inorder = inorder and inv = rbt nipkow@61224 110 proof (standard, goal_cases) nipkow@61224 111 case 1 show ?case by simp nipkow@61224 112 next nipkow@61790 113 case 2 thus ?case by(simp add: lookup_map_of) nipkow@61224 114 next nipkow@61224 115 case 3 thus ?case by(simp add: inorder_update) nipkow@61224 116 next nipkow@61224 117 case 4 thus ?case by(simp add: inorder_delete) nipkow@68415 118 next nipkow@68415 119 case 5 thus ?case by (simp add: rbt_Leaf) nipkow@68415 120 next nipkow@68415 121 case 6 thus ?case by (simp add: rbt_update) nipkow@68415 122 next nipkow@68415 123 case 7 thus ?case by (simp add: rbt_delete) nipkow@68415 124 qed nipkow@61224 125 nipkow@61224 126 end