1(* Author: Tobias Nipkow *) 2 3section \<open>Red-Black Tree Implementation of Sets\<close> 4 5theory RBT_Set 6imports 7 Complex_Main 8 RBT 9 Cmp 10 Isin2 11begin 12 13definition empty :: "'a rbt" where 14"empty = Leaf" 15 16fun ins :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where 17"ins x Leaf = R Leaf x Leaf" | 18"ins x (B l a r) = 19 (case cmp x a of 20 LT \<Rightarrow> baliL (ins x l) a r | 21 GT \<Rightarrow> baliR l a (ins x r) | 22 EQ \<Rightarrow> B l a r)" | 23"ins x (R l a r) = 24 (case cmp x a of 25 LT \<Rightarrow> R (ins x l) a r | 26 GT \<Rightarrow> R l a (ins x r) | 27 EQ \<Rightarrow> R l a r)" 28 29definition insert :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where 30"insert x t = paint Black (ins x t)" 31 32fun color :: "'a rbt \<Rightarrow> color" where 33"color Leaf = Black" | 34"color (Node _ _ c _) = c" 35 36fun del :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where 37"del x Leaf = Leaf" | 38"del x (Node l a _ r) = 39 (case cmp x a of 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)" 45 46definition delete :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where 47"delete x t = paint Black (del x t)" 48 49 50subsection "Functional Correctness Proofs" 51 52lemma inorder_paint: "inorder(paint c t) = inorder t" 53by(cases t) (auto) 54 55lemma inorder_baliL: 56 "inorder(baliL l a r) = inorder l @ a # inorder r" 57by(cases "(l,a,r)" rule: baliL.cases) (auto) 58 59lemma inorder_baliR: 60 "inorder(baliR l a r) = inorder l @ a # inorder r" 61by(cases "(l,a,r)" rule: baliR.cases) (auto) 62 63lemma inorder_ins: 64 "sorted(inorder t) \<Longrightarrow> inorder(ins x t) = ins_list x (inorder t)" 65by(induction x t rule: ins.induct) 66 (auto simp: ins_list_simps inorder_baliL inorder_baliR) 67 68lemma inorder_insert: 69 "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)" 70by (simp add: insert_def inorder_ins inorder_paint) 71 72lemma inorder_baldL: 73 "inorder(baldL l a r) = inorder l @ a # inorder r" 74by(cases "(l,a,r)" rule: baldL.cases) 75 (auto simp: inorder_baliL inorder_baliR inorder_paint) 76 77lemma inorder_baldR: 78 "inorder(baldR l a r) = inorder l @ a # inorder r" 79by(cases "(l,a,r)" rule: baldR.cases) 80 (auto simp: inorder_baliL inorder_baliR inorder_paint) 81 82lemma inorder_combine: 83 "inorder(combine l r) = inorder l @ inorder r" 84by(induction l r rule: combine.induct) 85 (auto simp: inorder_baldL inorder_baldR split: tree.split color.split) 86 87lemma inorder_del: 88 "sorted(inorder t) \<Longrightarrow> inorder(del x t) = del_list x (inorder t)" 89by(induction x t rule: del.induct) 90 (auto simp: del_list_simps inorder_combine inorder_baldL inorder_baldR) 91 92lemma inorder_delete: 93 "sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)" 94by (auto simp: delete_def inorder_del inorder_paint) 95 96 97subsection \<open>Structural invariants\<close> 98 99text\<open>The proofs are due to Markus Reiter and Alexander Krauss.\<close> 100 101fun bheight :: "'a rbt \<Rightarrow> nat" where 102"bheight Leaf = 0" | 103"bheight (Node l x c r) = (if c = Black then bheight l + 1 else bheight l)" 104 105fun invc :: "'a rbt \<Rightarrow> bool" where 106"invc Leaf = True" | 107"invc (Node l a c r) = 108 (invc l \<and> invc r \<and> (c = Red \<longrightarrow> color l = Black \<and> color r = Black))" 109 110fun invc2 :: "'a rbt \<Rightarrow> bool" \<comment> \<open>Weaker version\<close> where 111"invc2 Leaf = True" | 112"invc2 (Node l a c r) = (invc l \<and> invc r)" 113 114fun invh :: "'a rbt \<Rightarrow> bool" where 115"invh Leaf = True" | 116"invh (Node l x c r) = (invh l \<and> invh r \<and> bheight l = bheight r)" 117 118lemma invc2I: "invc t \<Longrightarrow> invc2 t" 119by (cases t) simp+ 120 121definition rbt :: "'a rbt \<Rightarrow> bool" where 122"rbt t = (invc t \<and> invh t \<and> color t = Black)" 123 124lemma color_paint_Black: "color (paint Black t) = Black" 125by (cases t) auto 126 127lemma paint_invc2: "invc2 t \<Longrightarrow> invc2 (paint c t)" 128by (cases t) auto 129 130lemma invc_paint_Black: "invc2 t \<Longrightarrow> invc (paint Black t)" 131by (cases t) auto 132 133lemma invh_paint: "invh t \<Longrightarrow> invh (paint c t)" 134by (cases t) auto 135 136lemma invc_baliL: 137 "\<lbrakk>invc2 l; invc r\<rbrakk> \<Longrightarrow> invc (baliL l a r)" 138by (induct l a r rule: baliL.induct) auto 139 140lemma invc_baliR: 141 "\<lbrakk>invc l; invc2 r\<rbrakk> \<Longrightarrow> invc (baliR l a r)" 142by (induct l a r rule: baliR.induct) auto 143 144lemma bheight_baliL: 145 "bheight l = bheight r \<Longrightarrow> bheight (baliL l a r) = Suc (bheight l)" 146by (induct l a r rule: baliL.induct) auto 147 148lemma bheight_baliR: 149 "bheight l = bheight r \<Longrightarrow> bheight (baliR l a r) = Suc (bheight l)" 150by (induct l a r rule: baliR.induct) auto 151 152lemma invh_baliL: 153 "\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk> \<Longrightarrow> invh (baliL l a r)" 154by (induct l a r rule: baliL.induct) auto 155 156lemma invh_baliR: 157 "\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk> \<Longrightarrow> invh (baliR l a r)" 158by (induct l a r rule: baliR.induct) auto 159 160 161subsubsection \<open>Insertion\<close> 162 163lemma invc_ins: assumes "invc t" 164 shows "color t = Black \<Longrightarrow> invc (ins x t)" "invc2 (ins x t)" 165using assms 166by (induct x t rule: ins.induct) (auto simp: invc_baliL invc_baliR invc2I) 167 168lemma invh_ins: assumes "invh t" 169 shows "invh (ins x t)" "bheight (ins x t) = bheight t" 170using assms 171by(induct x t rule: ins.induct) 172 (auto simp: invh_baliL invh_baliR bheight_baliL bheight_baliR) 173 174theorem rbt_insert: "rbt t \<Longrightarrow> rbt (insert x t)" 175by (simp add: invc_ins(2) invh_ins(1) color_paint_Black invc_paint_Black invh_paint 176 rbt_def insert_def) 177 178 179subsubsection \<open>Deletion\<close> 180 181lemma bheight_paint_Red: 182 "color t = Black \<Longrightarrow> bheight (paint Red t) = bheight t - 1" 183by (cases t) auto 184 185lemma invh_baldL_invc: 186 "\<lbrakk> invh l; invh r; bheight l + 1 = bheight r; invc r \<rbrakk> 187 \<Longrightarrow> invh (baldL l a r) \<and> bheight (baldL l a r) = bheight l + 1" 188by (induct l a r rule: baldL.induct) 189 (auto simp: invh_baliR invh_paint bheight_baliR bheight_paint_Red) 190 191lemma invh_baldL_Black: 192 "\<lbrakk> invh l; invh r; bheight l + 1 = bheight r; color r = Black \<rbrakk> 193 \<Longrightarrow> invh (baldL l a r) \<and> bheight (baldL l a r) = bheight r" 194by (induct l a r rule: baldL.induct) (auto simp add: invh_baliR bheight_baliR) 195 196lemma invc_baldL: "\<lbrakk>invc2 l; invc r; color r = Black\<rbrakk> \<Longrightarrow> invc (baldL l a r)" 197by (induct l a r rule: baldL.induct) (simp_all add: invc_baliR) 198 199lemma invc2_baldL: "\<lbrakk> invc2 l; invc r \<rbrakk> \<Longrightarrow> invc2 (baldL l a r)" 200by (induct l a r rule: baldL.induct) (auto simp: invc_baliR paint_invc2 invc2I) 201 202lemma invh_baldR_invc: 203 "\<lbrakk> invh l; invh r; bheight l = bheight r + 1; invc l \<rbrakk> 204 \<Longrightarrow> invh (baldR l a r) \<and> bheight (baldR l a r) = bheight l" 205by(induct l a r rule: baldR.induct) 206 (auto simp: invh_baliL bheight_baliL invh_paint bheight_paint_Red) 207 208lemma invc_baldR: "\<lbrakk>invc a; invc2 b; color a = Black\<rbrakk> \<Longrightarrow> invc (baldR a x b)" 209by (induct a x b rule: baldR.induct) (simp_all add: invc_baliL) 210 211lemma invc2_baldR: "\<lbrakk> invc l; invc2 r \<rbrakk> \<Longrightarrow>invc2 (baldR l x r)" 212by (induct l x r rule: baldR.induct) (auto simp: invc_baliL paint_invc2 invc2I) 213 214lemma invh_combine: 215 "\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk> 216 \<Longrightarrow> invh (combine l r) \<and> bheight (combine l r) = bheight l" 217by (induct l r rule: combine.induct) 218 (auto simp: invh_baldL_Black split: tree.splits color.splits) 219 220lemma invc_combine: 221 assumes "invc l" "invc r" 222 shows "color l = Black \<Longrightarrow> color r = Black \<Longrightarrow> invc (combine l r)" 223 "invc2 (combine l r)" 224using assms 225by (induct l r rule: combine.induct) 226 (auto simp: invc_baldL invc2I split: tree.splits color.splits) 227 228lemma neq_LeafD: "t \<noteq> Leaf \<Longrightarrow> \<exists>c l x r. t = Node c l x r" 229by(cases t) auto 230 231lemma del_invc_invh: "invh t \<Longrightarrow> invc t \<Longrightarrow> invh (del x t) \<and> 232 (color t = Red \<and> bheight (del x t) = bheight t \<and> invc (del x t) \<or> 233 color t = Black \<and> bheight (del x t) = bheight t - 1 \<and> invc2 (del x t))" 234proof (induct x t rule: del.induct) 235case (2 x _ y c) 236 have "x = y \<or> x < y \<or> x > y" by auto 237 thus ?case proof (elim disjE) 238 assume "x = y" 239 with 2 show ?thesis 240 by (cases c) (simp_all add: invh_combine invc_combine) 241 next 242 assume "x < y" 243 with 2 show ?thesis 244 by(cases c) 245 (auto simp: invh_baldL_invc invc_baldL invc2_baldL dest: neq_LeafD) 246 next 247 assume "y < x" 248 with 2 show ?thesis 249 by(cases c) 250 (auto simp: invh_baldR_invc invc_baldR invc2_baldR dest: neq_LeafD) 251 qed 252qed auto 253 254theorem rbt_delete: "rbt t \<Longrightarrow> rbt (delete k t)" 255by (metis delete_def rbt_def color_paint_Black del_invc_invh invc_paint_Black invc2I invh_paint) 256 257text \<open>Overall correctness:\<close> 258 259interpretation S: Set_by_Ordered 260where empty = empty and isin = isin and insert = insert and delete = delete 261and inorder = inorder and inv = rbt 262proof (standard, goal_cases) 263 case 1 show ?case by (simp add: empty_def) 264next 265 case 2 thus ?case by(simp add: isin_set_inorder) 266next 267 case 3 thus ?case by(simp add: inorder_insert) 268next 269 case 4 thus ?case by(simp add: inorder_delete) 270next 271 case 5 thus ?case by (simp add: rbt_def empty_def) 272next 273 case 6 thus ?case by (simp add: rbt_insert) 274next 275 case 7 thus ?case by (simp add: rbt_delete) 276qed 277 278 279subsection \<open>Height-Size Relation\<close> 280 281lemma neq_Black[simp]: "(c \<noteq> Black) = (c = Red)" 282by (cases c) auto 283 284lemma rbt_height_bheight_if: "invc t \<Longrightarrow> invh t \<Longrightarrow> 285 height t \<le> (if color t = Black then 2 * bheight t else 2 * bheight t + 1)" 286by(induction t) (auto split: if_split_asm) 287 288lemma rbt_height_bheight: "rbt t \<Longrightarrow> height t / 2 \<le> bheight t " 289by(auto simp: rbt_def dest: rbt_height_bheight_if) 290 291lemma bheight_size_bound: "invc t \<Longrightarrow> invh t \<Longrightarrow> 2 ^ (bheight t) \<le> size1 t" 292by (induction t) auto 293 294lemma rbt_height_le: assumes "rbt t" shows "height t \<le> 2 * log 2 (size1 t)" 295proof - 296 have "2 powr (height t / 2) \<le> 2 powr bheight t" 297 using rbt_height_bheight[OF assms] by (simp) 298 also have "\<dots> \<le> size1 t" using assms 299 by (simp add: powr_realpow bheight_size_bound rbt_def) 300 finally have "2 powr (height t / 2) \<le> size1 t" . 301 hence "height t / 2 \<le> log 2 (size1 t)" 302 by (simp add: le_log_iff size1_def del: divide_le_eq_numeral1(1)) 303 thus ?thesis by simp 304qed 305 306end 307