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