1(* Author: Tobias Nipkow *) 2 3section \<open>2-3 Tree Implementation of Sets\<close> 4 5theory Tree23_Set 6imports 7 Tree23 8 Cmp 9 Set_Specs 10begin 11 12declare sorted_wrt.simps(2)[simp del] 13 14definition empty :: "'a tree23" where 15"empty = Leaf" 16 17fun isin :: "'a::linorder tree23 \<Rightarrow> 'a \<Rightarrow> bool" where 18"isin Leaf x = False" | 19"isin (Node2 l a r) x = 20 (case cmp x a of 21 LT \<Rightarrow> isin l x | 22 EQ \<Rightarrow> True | 23 GT \<Rightarrow> isin r x)" | 24"isin (Node3 l a m b r) x = 25 (case cmp x a of 26 LT \<Rightarrow> isin l x | 27 EQ \<Rightarrow> True | 28 GT \<Rightarrow> 29 (case cmp x b of 30 LT \<Rightarrow> isin m x | 31 EQ \<Rightarrow> True | 32 GT \<Rightarrow> isin r x))" 33 34datatype 'a up\<^sub>i = T\<^sub>i "'a tree23" | Up\<^sub>i "'a tree23" 'a "'a tree23" 35 36fun tree\<^sub>i :: "'a up\<^sub>i \<Rightarrow> 'a tree23" where 37"tree\<^sub>i (T\<^sub>i t) = t" | 38"tree\<^sub>i (Up\<^sub>i l a r) = Node2 l a r" 39 40fun ins :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>i" where 41"ins x Leaf = Up\<^sub>i Leaf x Leaf" | 42"ins x (Node2 l a r) = 43 (case cmp x a of 44 LT \<Rightarrow> 45 (case ins x l of 46 T\<^sub>i l' => T\<^sub>i (Node2 l' a r) | 47 Up\<^sub>i l1 b l2 => T\<^sub>i (Node3 l1 b l2 a r)) | 48 EQ \<Rightarrow> T\<^sub>i (Node2 l x r) | 49 GT \<Rightarrow> 50 (case ins x r of 51 T\<^sub>i r' => T\<^sub>i (Node2 l a r') | 52 Up\<^sub>i r1 b r2 => T\<^sub>i (Node3 l a r1 b r2)))" | 53"ins x (Node3 l a m b r) = 54 (case cmp x a of 55 LT \<Rightarrow> 56 (case ins x l of 57 T\<^sub>i l' => T\<^sub>i (Node3 l' a m b r) | 58 Up\<^sub>i l1 c l2 => Up\<^sub>i (Node2 l1 c l2) a (Node2 m b r)) | 59 EQ \<Rightarrow> T\<^sub>i (Node3 l a m b r) | 60 GT \<Rightarrow> 61 (case cmp x b of 62 GT \<Rightarrow> 63 (case ins x r of 64 T\<^sub>i r' => T\<^sub>i (Node3 l a m b r') | 65 Up\<^sub>i r1 c r2 => Up\<^sub>i (Node2 l a m) b (Node2 r1 c r2)) | 66 EQ \<Rightarrow> T\<^sub>i (Node3 l a m b r) | 67 LT \<Rightarrow> 68 (case ins x m of 69 T\<^sub>i m' => T\<^sub>i (Node3 l a m' b r) | 70 Up\<^sub>i m1 c m2 => Up\<^sub>i (Node2 l a m1) c (Node2 m2 b r))))" 71 72hide_const insert 73 74definition insert :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where 75"insert x t = tree\<^sub>i(ins x t)" 76 77datatype 'a up\<^sub>d = T\<^sub>d "'a tree23" | Up\<^sub>d "'a tree23" 78 79fun tree\<^sub>d :: "'a up\<^sub>d \<Rightarrow> 'a tree23" where 80"tree\<^sub>d (T\<^sub>d t) = t" | 81"tree\<^sub>d (Up\<^sub>d t) = t" 82 83(* Variation: return None to signal no-change *) 84 85fun node21 :: "'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where 86"node21 (T\<^sub>d t1) a t2 = T\<^sub>d(Node2 t1 a t2)" | 87"node21 (Up\<^sub>d t1) a (Node2 t2 b t3) = Up\<^sub>d(Node3 t1 a t2 b t3)" | 88"node21 (Up\<^sub>d t1) a (Node3 t2 b t3 c t4) = T\<^sub>d(Node2 (Node2 t1 a t2) b (Node2 t3 c t4))" 89 90fun node22 :: "'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a up\<^sub>d" where 91"node22 t1 a (T\<^sub>d t2) = T\<^sub>d(Node2 t1 a t2)" | 92"node22 (Node2 t1 b t2) a (Up\<^sub>d t3) = Up\<^sub>d(Node3 t1 b t2 a t3)" | 93"node22 (Node3 t1 b t2 c t3) a (Up\<^sub>d t4) = T\<^sub>d(Node2 (Node2 t1 b t2) c (Node2 t3 a t4))" 94 95fun node31 :: "'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where 96"node31 (T\<^sub>d t1) a t2 b t3 = T\<^sub>d(Node3 t1 a t2 b t3)" | 97"node31 (Up\<^sub>d t1) a (Node2 t2 b t3) c t4 = T\<^sub>d(Node2 (Node3 t1 a t2 b t3) c t4)" | 98"node31 (Up\<^sub>d t1) a (Node3 t2 b t3 c t4) d t5 = T\<^sub>d(Node3 (Node2 t1 a t2) b (Node2 t3 c t4) d t5)" 99 100fun node32 :: "'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where 101"node32 t1 a (T\<^sub>d t2) b t3 = T\<^sub>d(Node3 t1 a t2 b t3)" | 102"node32 t1 a (Up\<^sub>d t2) b (Node2 t3 c t4) = T\<^sub>d(Node2 t1 a (Node3 t2 b t3 c t4))" | 103"node32 t1 a (Up\<^sub>d t2) b (Node3 t3 c t4 d t5) = T\<^sub>d(Node3 t1 a (Node2 t2 b t3) c (Node2 t4 d t5))" 104 105fun node33 :: "'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a up\<^sub>d" where 106"node33 l a m b (T\<^sub>d r) = T\<^sub>d(Node3 l a m b r)" | 107"node33 t1 a (Node2 t2 b t3) c (Up\<^sub>d t4) = T\<^sub>d(Node2 t1 a (Node3 t2 b t3 c t4))" | 108"node33 t1 a (Node3 t2 b t3 c t4) d (Up\<^sub>d t5) = T\<^sub>d(Node3 t1 a (Node2 t2 b t3) c (Node2 t4 d t5))" 109 110fun split_min :: "'a tree23 \<Rightarrow> 'a * 'a up\<^sub>d" where 111"split_min (Node2 Leaf a Leaf) = (a, Up\<^sub>d Leaf)" | 112"split_min (Node3 Leaf a Leaf b Leaf) = (a, T\<^sub>d(Node2 Leaf b Leaf))" | 113"split_min (Node2 l a r) = (let (x,l') = split_min l in (x, node21 l' a r))" | 114"split_min (Node3 l a m b r) = (let (x,l') = split_min l in (x, node31 l' a m b r))" 115 116text \<open>In the base cases of \<open>split_min\<close> and \<open>del\<close> it is enough to check if one subtree is a \<open>Leaf\<close>, 117in which case balancedness implies that so are the others. Exercise.\<close> 118 119fun del :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where 120"del x Leaf = T\<^sub>d Leaf" | 121"del x (Node2 Leaf a Leaf) = 122 (if x = a then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf a Leaf))" | 123"del x (Node3 Leaf a Leaf b Leaf) = 124 T\<^sub>d(if x = a then Node2 Leaf b Leaf else 125 if x = b then Node2 Leaf a Leaf 126 else Node3 Leaf a Leaf b Leaf)" | 127"del x (Node2 l a r) = 128 (case cmp x a of 129 LT \<Rightarrow> node21 (del x l) a r | 130 GT \<Rightarrow> node22 l a (del x r) | 131 EQ \<Rightarrow> let (a',t) = split_min r in node22 l a' t)" | 132"del x (Node3 l a m b r) = 133 (case cmp x a of 134 LT \<Rightarrow> node31 (del x l) a m b r | 135 EQ \<Rightarrow> let (a',m') = split_min m in node32 l a' m' b r | 136 GT \<Rightarrow> 137 (case cmp x b of 138 LT \<Rightarrow> node32 l a (del x m) b r | 139 EQ \<Rightarrow> let (b',r') = split_min r in node33 l a m b' r' | 140 GT \<Rightarrow> node33 l a m b (del x r)))" 141 142definition delete :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where 143"delete x t = tree\<^sub>d(del x t)" 144 145 146subsection "Functional Correctness" 147 148subsubsection "Proofs for isin" 149 150lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> set (inorder t))" 151by (induction t) (auto simp: isin_simps ball_Un) 152 153 154subsubsection "Proofs for insert" 155 156lemma inorder_ins: 157 "sorted(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(ins x t)) = ins_list x (inorder t)" 158by(induction t) (auto simp: ins_list_simps split: up\<^sub>i.splits) 159 160lemma inorder_insert: 161 "sorted(inorder t) \<Longrightarrow> inorder(insert a t) = ins_list a (inorder t)" 162by(simp add: insert_def inorder_ins) 163 164 165subsubsection "Proofs for delete" 166 167lemma inorder_node21: "height r > 0 \<Longrightarrow> 168 inorder (tree\<^sub>d (node21 l' a r)) = inorder (tree\<^sub>d l') @ a # inorder r" 169by(induct l' a r rule: node21.induct) auto 170 171lemma inorder_node22: "height l > 0 \<Longrightarrow> 172 inorder (tree\<^sub>d (node22 l a r')) = inorder l @ a # inorder (tree\<^sub>d r')" 173by(induct l a r' rule: node22.induct) auto 174 175lemma inorder_node31: "height m > 0 \<Longrightarrow> 176 inorder (tree\<^sub>d (node31 l' a m b r)) = inorder (tree\<^sub>d l') @ a # inorder m @ b # inorder r" 177by(induct l' a m b r rule: node31.induct) auto 178 179lemma inorder_node32: "height r > 0 \<Longrightarrow> 180 inorder (tree\<^sub>d (node32 l a m' b r)) = inorder l @ a # inorder (tree\<^sub>d m') @ b # inorder r" 181by(induct l a m' b r rule: node32.induct) auto 182 183lemma inorder_node33: "height m > 0 \<Longrightarrow> 184 inorder (tree\<^sub>d (node33 l a m b r')) = inorder l @ a # inorder m @ b # inorder (tree\<^sub>d r')" 185by(induct l a m b r' rule: node33.induct) auto 186 187lemmas inorder_nodes = inorder_node21 inorder_node22 188 inorder_node31 inorder_node32 inorder_node33 189 190lemma split_minD: 191 "split_min t = (x,t') \<Longrightarrow> bal t \<Longrightarrow> height t > 0 \<Longrightarrow> 192 x # inorder(tree\<^sub>d t') = inorder t" 193by(induction t arbitrary: t' rule: split_min.induct) 194 (auto simp: inorder_nodes split: prod.splits) 195 196lemma inorder_del: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow> 197 inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)" 198by(induction t rule: del.induct) 199 (auto simp: del_list_simps inorder_nodes split_minD split!: if_split prod.splits) 200 201lemma inorder_delete: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow> 202 inorder(delete x t) = del_list x (inorder t)" 203by(simp add: delete_def inorder_del) 204 205 206subsection \<open>Balancedness\<close> 207 208 209subsubsection "Proofs for insert" 210 211text\<open>First a standard proof that @{const ins} preserves @{const bal}.\<close> 212 213instantiation up\<^sub>i :: (type)height 214begin 215 216fun height_up\<^sub>i :: "'a up\<^sub>i \<Rightarrow> nat" where 217"height (T\<^sub>i t) = height t" | 218"height (Up\<^sub>i l a r) = height l" 219 220instance .. 221 222end 223 224lemma bal_ins: "bal t \<Longrightarrow> bal (tree\<^sub>i(ins a t)) \<and> height(ins a t) = height t" 225by (induct t) (auto split!: if_split up\<^sub>i.split) (* 15 secs in 2015 *) 226 227text\<open>Now an alternative proof (by Brian Huffman) that runs faster because 228two properties (balance and height) are combined in one predicate.\<close> 229 230inductive full :: "nat \<Rightarrow> 'a tree23 \<Rightarrow> bool" where 231"full 0 Leaf" | 232"\<lbrakk>full n l; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Node2 l p r)" | 233"\<lbrakk>full n l; full n m; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Node3 l p m q r)" 234 235inductive_cases full_elims: 236 "full n Leaf" 237 "full n (Node2 l p r)" 238 "full n (Node3 l p m q r)" 239 240inductive_cases full_0_elim: "full 0 t" 241inductive_cases full_Suc_elim: "full (Suc n) t" 242 243lemma full_0_iff [simp]: "full 0 t \<longleftrightarrow> t = Leaf" 244 by (auto elim: full_0_elim intro: full.intros) 245 246lemma full_Leaf_iff [simp]: "full n Leaf \<longleftrightarrow> n = 0" 247 by (auto elim: full_elims intro: full.intros) 248 249lemma full_Suc_Node2_iff [simp]: 250 "full (Suc n) (Node2 l p r) \<longleftrightarrow> full n l \<and> full n r" 251 by (auto elim: full_elims intro: full.intros) 252 253lemma full_Suc_Node3_iff [simp]: 254 "full (Suc n) (Node3 l p m q r) \<longleftrightarrow> full n l \<and> full n m \<and> full n r" 255 by (auto elim: full_elims intro: full.intros) 256 257lemma full_imp_height: "full n t \<Longrightarrow> height t = n" 258 by (induct set: full, simp_all) 259 260lemma full_imp_bal: "full n t \<Longrightarrow> bal t" 261 by (induct set: full, auto dest: full_imp_height) 262 263lemma bal_imp_full: "bal t \<Longrightarrow> full (height t) t" 264 by (induct t, simp_all) 265 266lemma bal_iff_full: "bal t \<longleftrightarrow> (\<exists>n. full n t)" 267 by (auto elim!: bal_imp_full full_imp_bal) 268 269text \<open>The @{const "insert"} function either preserves the height of the 270tree, or increases it by one. The constructor returned by the @{term 271"insert"} function determines which: A return value of the form @{term 272"T\<^sub>i t"} indicates that the height will be the same. A value of the 273form @{term "Up\<^sub>i l p r"} indicates an increase in height.\<close> 274 275fun full\<^sub>i :: "nat \<Rightarrow> 'a up\<^sub>i \<Rightarrow> bool" where 276"full\<^sub>i n (T\<^sub>i t) \<longleftrightarrow> full n t" | 277"full\<^sub>i n (Up\<^sub>i l p r) \<longleftrightarrow> full n l \<and> full n r" 278 279lemma full\<^sub>i_ins: "full n t \<Longrightarrow> full\<^sub>i n (ins a t)" 280by (induct rule: full.induct) (auto split: up\<^sub>i.split) 281 282text \<open>The @{const insert} operation preserves balance.\<close> 283 284lemma bal_insert: "bal t \<Longrightarrow> bal (insert a t)" 285unfolding bal_iff_full insert_def 286apply (erule exE) 287apply (drule full\<^sub>i_ins [of _ _ a]) 288apply (cases "ins a t") 289apply (auto intro: full.intros) 290done 291 292 293subsection "Proofs for delete" 294 295instantiation up\<^sub>d :: (type)height 296begin 297 298fun height_up\<^sub>d :: "'a up\<^sub>d \<Rightarrow> nat" where 299"height (T\<^sub>d t) = height t" | 300"height (Up\<^sub>d t) = height t + 1" 301 302instance .. 303 304end 305 306lemma bal_tree\<^sub>d_node21: 307 "\<lbrakk>bal r; bal (tree\<^sub>d l'); height r = height l' \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d (node21 l' a r))" 308by(induct l' a r rule: node21.induct) auto 309 310lemma bal_tree\<^sub>d_node22: 311 "\<lbrakk>bal(tree\<^sub>d r'); bal l; height r' = height l \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d (node22 l a r'))" 312by(induct l a r' rule: node22.induct) auto 313 314lemma bal_tree\<^sub>d_node31: 315 "\<lbrakk> bal (tree\<^sub>d l'); bal m; bal r; height l' = height r; height m = height r \<rbrakk> 316 \<Longrightarrow> bal (tree\<^sub>d (node31 l' a m b r))" 317by(induct l' a m b r rule: node31.induct) auto 318 319lemma bal_tree\<^sub>d_node32: 320 "\<lbrakk> bal l; bal (tree\<^sub>d m'); bal r; height l = height r; height m' = height r \<rbrakk> 321 \<Longrightarrow> bal (tree\<^sub>d (node32 l a m' b r))" 322by(induct l a m' b r rule: node32.induct) auto 323 324lemma bal_tree\<^sub>d_node33: 325 "\<lbrakk> bal l; bal m; bal(tree\<^sub>d r'); height l = height r'; height m = height r' \<rbrakk> 326 \<Longrightarrow> bal (tree\<^sub>d (node33 l a m b r'))" 327by(induct l a m b r' rule: node33.induct) auto 328 329lemmas bals = bal_tree\<^sub>d_node21 bal_tree\<^sub>d_node22 330 bal_tree\<^sub>d_node31 bal_tree\<^sub>d_node32 bal_tree\<^sub>d_node33 331 332lemma height'_node21: 333 "height r > 0 \<Longrightarrow> height(node21 l' a r) = max (height l') (height r) + 1" 334by(induct l' a r rule: node21.induct)(simp_all) 335 336lemma height'_node22: 337 "height l > 0 \<Longrightarrow> height(node22 l a r') = max (height l) (height r') + 1" 338by(induct l a r' rule: node22.induct)(simp_all) 339 340lemma height'_node31: 341 "height m > 0 \<Longrightarrow> height(node31 l a m b r) = 342 max (height l) (max (height m) (height r)) + 1" 343by(induct l a m b r rule: node31.induct)(simp_all add: max_def) 344 345lemma height'_node32: 346 "height r > 0 \<Longrightarrow> height(node32 l a m b r) = 347 max (height l) (max (height m) (height r)) + 1" 348by(induct l a m b r rule: node32.induct)(simp_all add: max_def) 349 350lemma height'_node33: 351 "height m > 0 \<Longrightarrow> height(node33 l a m b r) = 352 max (height l) (max (height m) (height r)) + 1" 353by(induct l a m b r rule: node33.induct)(simp_all add: max_def) 354 355lemmas heights = height'_node21 height'_node22 356 height'_node31 height'_node32 height'_node33 357 358lemma height_split_min: 359 "split_min t = (x, t') \<Longrightarrow> height t > 0 \<Longrightarrow> bal t \<Longrightarrow> height t' = height t" 360by(induct t arbitrary: x t' rule: split_min.induct) 361 (auto simp: heights split: prod.splits) 362 363lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t" 364by(induction x t rule: del.induct) 365 (auto simp: heights max_def height_split_min split: prod.splits) 366 367lemma bal_split_min: 368 "\<lbrakk> split_min t = (x, t'); bal t; height t > 0 \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d t')" 369by(induct t arbitrary: x t' rule: split_min.induct) 370 (auto simp: heights height_split_min bals split: prod.splits) 371 372lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))" 373by(induction x t rule: del.induct) 374 (auto simp: bals bal_split_min height_del height_split_min split: prod.splits) 375 376corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)" 377by(simp add: delete_def bal_tree\<^sub>d_del) 378 379 380subsection \<open>Overall Correctness\<close> 381 382interpretation S: Set_by_Ordered 383where empty = empty and isin = isin and insert = insert and delete = delete 384and inorder = inorder and inv = bal 385proof (standard, goal_cases) 386 case 2 thus ?case by(simp add: isin_set) 387next 388 case 3 thus ?case by(simp add: inorder_insert) 389next 390 case 4 thus ?case by(simp add: inorder_delete) 391next 392 case 6 thus ?case by(simp add: bal_insert) 393next 394 case 7 thus ?case by(simp add: bal_delete) 395qed (simp add: empty_def)+ 396 397end 398