1(* Author: Tobias Nipkow *) 2 3section "Join-Based Implementation of Sets via RBTs" 4 5theory Set2_Join_RBT 6imports 7 Set2_Join 8 RBT_Set 9begin 10 11subsection "Code" 12 13text \<open> 14Function \<open>joinL\<close> joins two trees (and an element). 15Precondition: @{prop "bheight l \<le> bheight r"}. 16Method: 17Descend along the left spine of \<open>r\<close> 18until you find a subtree with the same \<open>bheight\<close> as \<open>l\<close>, 19then combine them into a new red node. 20\<close> 21fun joinL :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where 22"joinL l x r = 23 (if bheight l = bheight r then R l x r 24 else case r of 25 B l' x' r' \<Rightarrow> baliL (joinL l x l') x' r' | 26 R l' x' r' \<Rightarrow> R (joinL l x l') x' r')" 27 28fun joinR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where 29"joinR l x r = 30 (if bheight l \<le> bheight r then R l x r 31 else case l of 32 B l' x' r' \<Rightarrow> baliR l' x' (joinR r' x r) | 33 R l' x' r' \<Rightarrow> R l' x' (joinR r' x r))" 34 35fun join :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where 36"join l x r = 37 (if bheight l > bheight r 38 then paint Black (joinR l x r) 39 else if bheight l < bheight r 40 then paint Black (joinL l x r) 41 else B l x r)" 42 43declare joinL.simps[simp del] 44declare joinR.simps[simp del] 45 46text \<open> 47One would expect @{const joinR} to be be completely dual to @{const joinL}. 48Thus the condition should be @{prop"bheight l = bheight r"}. What we have done 49is totalize the function. On the intended domain (@{prop "bheight l \<ge> bheight r"}) 50the two versions behave exactly the same, including complexity. Thus from a programmer's 51perspective they are equivalent. However, not from a verifier's perspective: 52the total version of @{const joinR} is easier 53to reason about because lemmas about it may not require preconditions. In particular 54@{prop"set_tree (joinR l x r) = set_tree l \<union> {x} \<union> set_tree r"} 55is provable outright and hence also 56@{prop"set_tree (join l x r) = set_tree l \<union> {x} \<union> set_tree r"}. 57This is necessary because locale @{locale Set2_Join} unconditionally assumes 58exactly that. Adding preconditions to this assumptions significantly complicates 59the proofs within @{locale Set2_Join}, which we want to avoid. 60 61Why not work with the partial version of @{const joinR} and add the precondition 62@{prop "bheight l \<ge> bheight r"} to lemmas about @{const joinR}? After all, that is how 63we worked with @{const joinL}, and @{const join} ensures that @{const joinL} and @{const joinR} 64are only called under the respective precondition. But function @{const bheight} 65makes the difference: it descends along the left spine, just like @{const joinL}. 66Function @{const joinR}, however, descends along the right spine and thus @{const bheight} 67may change all the time. Thus we would need the further precondition @{prop "invh l"}. 68This is what we really wanted to avoid in order to satisfy the unconditional assumption 69in @{locale Set2_Join}. 70\<close> 71 72subsection "Properties" 73 74subsubsection "Color and height invariants" 75 76lemma invc2_joinL: 77 "\<lbrakk> invc l; invc r; bheight l \<le> bheight r \<rbrakk> \<Longrightarrow> 78 invc2 (joinL l x r) 79 \<and> (bheight l \<noteq> bheight r \<and> color r = Black \<longrightarrow> invc(joinL l x r))" 80proof (induct l x r rule: joinL.induct) 81 case (1 l x r) thus ?case 82 by(auto simp: invc_baliL invc2I joinL.simps[of l x r] split!: tree.splits if_splits) 83qed 84 85lemma invc2_joinR: 86 "\<lbrakk> invc l; invh l; invc r; invh r; bheight l \<ge> bheight r \<rbrakk> \<Longrightarrow> 87 invc2 (joinR l x r) 88 \<and> (bheight l \<noteq> bheight r \<and> color l = Black \<longrightarrow> invc(joinR l x r))" 89proof (induct l x r rule: joinR.induct) 90 case (1 l x r) thus ?case 91 by(fastforce simp: invc_baliR invc2I joinR.simps[of l x r] split!: tree.splits if_splits) 92qed 93 94lemma bheight_joinL: 95 "\<lbrakk> invh l; invh r; bheight l \<le> bheight r \<rbrakk> \<Longrightarrow> bheight (joinL l x r) = bheight r" 96proof (induct l x r rule: joinL.induct) 97 case (1 l x r) thus ?case 98 by(auto simp: bheight_baliL joinL.simps[of l x r] split!: tree.split) 99qed 100 101lemma invh_joinL: 102 "\<lbrakk> invh l; invh r; bheight l \<le> bheight r \<rbrakk> \<Longrightarrow> invh (joinL l x r)" 103proof (induct l x r rule: joinL.induct) 104 case (1 l x r) thus ?case 105 by(auto simp: invh_baliL bheight_joinL joinL.simps[of l x r] split!: tree.split color.split) 106qed 107 108lemma bheight_baliR: 109 "bheight l = bheight r \<Longrightarrow> bheight (baliR l a r) = Suc (bheight l)" 110by (cases "(l,a,r)" rule: baliR.cases) auto 111 112lemma bheight_joinR: 113 "\<lbrakk> invh l; invh r; bheight l \<ge> bheight r \<rbrakk> \<Longrightarrow> bheight (joinR l x r) = bheight l" 114proof (induct l x r rule: joinR.induct) 115 case (1 l x r) thus ?case 116 by(fastforce simp: bheight_baliR joinR.simps[of l x r] split!: tree.split) 117qed 118 119lemma invh_joinR: 120 "\<lbrakk> invh l; invh r; bheight l \<ge> bheight r \<rbrakk> \<Longrightarrow> invh (joinR l x r)" 121proof (induct l x r rule: joinR.induct) 122 case (1 l x r) thus ?case 123 by(fastforce simp: invh_baliR bheight_joinR joinR.simps[of l x r] 124 split!: tree.split color.split) 125qed 126 127(* unused *) 128lemma rbt_join: "\<lbrakk> invc l; invh l; invc r; invh r \<rbrakk> \<Longrightarrow> rbt(join l x r)" 129by(simp add: invc2_joinL invc2_joinR invc_paint_Black invh_joinL invh_joinR invh_paint rbt_def 130 color_paint_Black) 131 132text \<open>To make sure the the black height is not increased unnecessarily:\<close> 133 134lemma bheight_paint_Black: "bheight(paint Black t) \<le> bheight t + 1" 135by(cases t) auto 136 137lemma "\<lbrakk> rbt l; rbt r \<rbrakk> \<Longrightarrow> bheight(join l x r) \<le> max (bheight l) (bheight r) + 1" 138using bheight_paint_Black[of "joinL l x r"] bheight_paint_Black[of "joinR l x r"] 139 bheight_joinL[of l r x] bheight_joinR[of l r x] 140by(auto simp: max_def rbt_def) 141 142 143subsubsection "Inorder properties" 144 145text "Currently unused. Instead @{const set_tree} and @{const bst} properties are proved directly." 146 147lemma inorder_joinL: "bheight l \<le> bheight r \<Longrightarrow> inorder(joinL l x r) = inorder l @ x # inorder r" 148proof(induction l x r rule: joinL.induct) 149 case (1 l x r) 150 thus ?case by(auto simp: inorder_baliL joinL.simps[of l x r] split!: tree.splits color.splits) 151qed 152 153lemma inorder_joinR: 154 "inorder(joinR l x r) = inorder l @ x # inorder r" 155proof(induction l x r rule: joinR.induct) 156 case (1 l x r) 157 thus ?case by (force simp: inorder_baliR joinR.simps[of l x r] split!: tree.splits color.splits) 158qed 159 160lemma "inorder(join l x r) = inorder l @ x # inorder r" 161by(auto simp: inorder_joinL inorder_joinR inorder_paint split!: tree.splits color.splits if_splits 162 dest!: arg_cong[where f = inorder]) 163 164 165subsubsection "Set and bst properties" 166 167lemma set_baliL: 168 "set_tree(baliL l a r) = set_tree l \<union> {a} \<union> set_tree r" 169by(cases "(l,a,r)" rule: baliL.cases) (auto) 170 171lemma set_joinL: 172 "bheight l \<le> bheight r \<Longrightarrow> set_tree (joinL l x r) = set_tree l \<union> {x} \<union> set_tree r" 173proof(induction l x r rule: joinL.induct) 174 case (1 l x r) 175 thus ?case by(auto simp: set_baliL joinL.simps[of l x r] split!: tree.splits color.splits) 176qed 177 178lemma set_baliR: 179 "set_tree(baliR l a r) = set_tree l \<union> {a} \<union> set_tree r" 180by(cases "(l,a,r)" rule: baliR.cases) (auto) 181 182lemma set_joinR: 183 "set_tree (joinR l x r) = set_tree l \<union> {x} \<union> set_tree r" 184proof(induction l x r rule: joinR.induct) 185 case (1 l x r) 186 thus ?case by(force simp: set_baliR joinR.simps[of l x r] split!: tree.splits color.splits) 187qed 188 189lemma set_paint: "set_tree (paint c t) = set_tree t" 190by (cases t) auto 191 192lemma set_join: "set_tree (join l x r) = set_tree l \<union> {x} \<union> set_tree r" 193by(simp add: set_joinL set_joinR set_paint) 194 195lemma bst_baliL: 196 "\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < k; \<forall>x\<in>set_tree r. k < x\<rbrakk> 197 \<Longrightarrow> bst (baliL l k r)" 198by(cases "(l,k,r)" rule: baliL.cases) (auto simp: ball_Un) 199 200lemma bst_baliR: 201 "\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < k; \<forall>x\<in>set_tree r. k < x\<rbrakk> 202 \<Longrightarrow> bst (baliR l k r)" 203by(cases "(l,k,r)" rule: baliR.cases) (auto simp: ball_Un) 204 205lemma bst_joinL: 206 "\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < k; \<forall>y\<in>set_tree r. k < y; bheight l \<le> bheight r\<rbrakk> 207 \<Longrightarrow> bst (joinL l k r)" 208proof(induction l k r rule: joinL.induct) 209 case (1 l x r) 210 thus ?case 211 by(auto simp: set_baliL joinL.simps[of l x r] set_joinL ball_Un intro!: bst_baliL 212 split!: tree.splits color.splits) 213qed 214 215lemma bst_joinR: 216 "\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < k; \<forall>y\<in>set_tree r. k < y \<rbrakk> 217 \<Longrightarrow> bst (joinR l k r)" 218proof(induction l k r rule: joinR.induct) 219 case (1 l x r) 220 thus ?case 221 by(auto simp: set_baliR joinR.simps[of l x r] set_joinR ball_Un intro!: bst_baliR 222 split!: tree.splits color.splits) 223qed 224 225lemma bst_paint: "bst (paint c t) = bst t" 226by(cases t) auto 227 228lemma bst_join: 229 "\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < k; \<forall>y\<in>set_tree r. k < y \<rbrakk> 230 \<Longrightarrow> bst (join l k r)" 231by(auto simp: bst_paint bst_joinL bst_joinR) 232 233 234subsubsection "Interpretation of @{locale Set2_Join} with Red-Black Tree" 235 236global_interpretation RBT: Set2_Join 237where join = join and inv = "\<lambda>t. invc t \<and> invh t" 238defines insert_rbt = RBT.insert and delete_rbt = RBT.delete and split_rbt = RBT.split 239and join2_rbt = RBT.join2 and split_min_rbt = RBT.split_min 240proof (standard, goal_cases) 241 case 1 show ?case by (rule set_join) 242next 243 case 2 thus ?case by (rule bst_join) 244next 245 case 3 show ?case by simp 246next 247 case 4 thus ?case 248 by (simp add: invc2_joinL invc2_joinR invc_paint_Black invh_joinL invh_joinR invh_paint) 249next 250 case 5 thus ?case by simp 251qed 252 253text \<open>The invariant does not guarantee that the root node is black. This is not required 254to guarantee that the height is logarithmic in the size --- Exercise.\<close> 255 256end