1(* Author: Tobias Nipkow *) 2 3section \<open>2-3-4 Tree Implementation of Sets\<close> 4 5theory Tree234_Set 6imports 7 Tree234 8 Cmp 9 Set_Specs 10begin 11 12declare sorted_wrt.simps(2)[simp del] 13 14subsection \<open>Set operations on 2-3-4 trees\<close> 15 16definition empty :: "'a tree234" where 17"empty = Leaf" 18 19fun isin :: "'a::linorder tree234 \<Rightarrow> 'a \<Rightarrow> bool" where 20"isin Leaf x = False" | 21"isin (Node2 l a r) x = 22 (case cmp x a of LT \<Rightarrow> isin l x | EQ \<Rightarrow> True | GT \<Rightarrow> isin r x)" | 23"isin (Node3 l a m b r) x = 24 (case cmp x a of LT \<Rightarrow> isin l x | EQ \<Rightarrow> True | GT \<Rightarrow> (case cmp x b of 25 LT \<Rightarrow> isin m x | EQ \<Rightarrow> True | GT \<Rightarrow> isin r x))" | 26"isin (Node4 t1 a t2 b t3 c t4) x = 27 (case cmp x b of 28 LT \<Rightarrow> 29 (case cmp x a of 30 LT \<Rightarrow> isin t1 x | 31 EQ \<Rightarrow> True | 32 GT \<Rightarrow> isin t2 x) | 33 EQ \<Rightarrow> True | 34 GT \<Rightarrow> 35 (case cmp x c of 36 LT \<Rightarrow> isin t3 x | 37 EQ \<Rightarrow> True | 38 GT \<Rightarrow> isin t4 x))" 39 40datatype 'a up\<^sub>i = T\<^sub>i "'a tree234" | Up\<^sub>i "'a tree234" 'a "'a tree234" 41 42fun tree\<^sub>i :: "'a up\<^sub>i \<Rightarrow> 'a tree234" where 43"tree\<^sub>i (T\<^sub>i t) = t" | 44"tree\<^sub>i (Up\<^sub>i l a r) = Node2 l a r" 45 46fun ins :: "'a::linorder \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>i" where 47"ins x Leaf = Up\<^sub>i Leaf x Leaf" | 48"ins x (Node2 l a r) = 49 (case cmp x a of 50 LT \<Rightarrow> (case ins x l of 51 T\<^sub>i l' => T\<^sub>i (Node2 l' a r) 52 | Up\<^sub>i l1 b l2 => T\<^sub>i (Node3 l1 b l2 a r)) | 53 EQ \<Rightarrow> T\<^sub>i (Node2 l x r) | 54 GT \<Rightarrow> (case ins x r of 55 T\<^sub>i r' => T\<^sub>i (Node2 l a r') 56 | Up\<^sub>i r1 b r2 => T\<^sub>i (Node3 l a r1 b r2)))" | 57"ins x (Node3 l a m b r) = 58 (case cmp x a of 59 LT \<Rightarrow> (case ins x l of 60 T\<^sub>i l' => T\<^sub>i (Node3 l' a m b r) 61 | Up\<^sub>i l1 c l2 => Up\<^sub>i (Node2 l1 c l2) a (Node2 m b r)) | 62 EQ \<Rightarrow> T\<^sub>i (Node3 l a m b r) | 63 GT \<Rightarrow> (case cmp x b of 64 GT \<Rightarrow> (case ins x r of 65 T\<^sub>i r' => T\<^sub>i (Node3 l a m b r') 66 | Up\<^sub>i r1 c r2 => Up\<^sub>i (Node2 l a m) b (Node2 r1 c r2)) | 67 EQ \<Rightarrow> T\<^sub>i (Node3 l a m b r) | 68 LT \<Rightarrow> (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"ins x (Node4 t1 a t2 b t3 c t4) = 72 (case cmp x b of 73 LT \<Rightarrow> 74 (case cmp x a of 75 LT \<Rightarrow> 76 (case ins x t1 of 77 T\<^sub>i t => T\<^sub>i (Node4 t a t2 b t3 c t4) | 78 Up\<^sub>i l y r => Up\<^sub>i (Node2 l y r) a (Node3 t2 b t3 c t4)) | 79 EQ \<Rightarrow> T\<^sub>i (Node4 t1 a t2 b t3 c t4) | 80 GT \<Rightarrow> 81 (case ins x t2 of 82 T\<^sub>i t => T\<^sub>i (Node4 t1 a t b t3 c t4) | 83 Up\<^sub>i l y r => Up\<^sub>i (Node2 t1 a l) y (Node3 r b t3 c t4))) | 84 EQ \<Rightarrow> T\<^sub>i (Node4 t1 a t2 b t3 c t4) | 85 GT \<Rightarrow> 86 (case cmp x c of 87 LT \<Rightarrow> 88 (case ins x t3 of 89 T\<^sub>i t => T\<^sub>i (Node4 t1 a t2 b t c t4) | 90 Up\<^sub>i l y r => Up\<^sub>i (Node2 t1 a t2) b (Node3 l y r c t4)) | 91 EQ \<Rightarrow> T\<^sub>i (Node4 t1 a t2 b t3 c t4) | 92 GT \<Rightarrow> 93 (case ins x t4 of 94 T\<^sub>i t => T\<^sub>i (Node4 t1 a t2 b t3 c t) | 95 Up\<^sub>i l y r => Up\<^sub>i (Node2 t1 a t2) b (Node3 t3 c l y r))))" 96 97hide_const insert 98 99definition insert :: "'a::linorder \<Rightarrow> 'a tree234 \<Rightarrow> 'a tree234" where 100"insert x t = tree\<^sub>i(ins x t)" 101 102datatype 'a up\<^sub>d = T\<^sub>d "'a tree234" | Up\<^sub>d "'a tree234" 103 104fun tree\<^sub>d :: "'a up\<^sub>d \<Rightarrow> 'a tree234" where 105"tree\<^sub>d (T\<^sub>d t) = t" | 106"tree\<^sub>d (Up\<^sub>d t) = t" 107 108fun node21 :: "'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where 109"node21 (T\<^sub>d l) a r = T\<^sub>d(Node2 l a r)" | 110"node21 (Up\<^sub>d l) a (Node2 lr b rr) = Up\<^sub>d(Node3 l a lr b rr)" | 111"node21 (Up\<^sub>d l) a (Node3 lr b mr c rr) = T\<^sub>d(Node2 (Node2 l a lr) b (Node2 mr c rr))" | 112"node21 (Up\<^sub>d t1) a (Node4 t2 b t3 c t4 d t5) = T\<^sub>d(Node2 (Node2 t1 a t2) b (Node3 t3 c t4 d t5))" 113 114fun node22 :: "'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a up\<^sub>d" where 115"node22 l a (T\<^sub>d r) = T\<^sub>d(Node2 l a r)" | 116"node22 (Node2 ll b rl) a (Up\<^sub>d r) = Up\<^sub>d(Node3 ll b rl a r)" | 117"node22 (Node3 ll b ml c rl) a (Up\<^sub>d r) = T\<^sub>d(Node2 (Node2 ll b ml) c (Node2 rl a r))" | 118"node22 (Node4 t1 a t2 b t3 c t4) d (Up\<^sub>d t5) = T\<^sub>d(Node2 (Node2 t1 a t2) b (Node3 t3 c t4 d t5))" 119 120fun node31 :: "'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where 121"node31 (T\<^sub>d t1) a t2 b t3 = T\<^sub>d(Node3 t1 a t2 b t3)" | 122"node31 (Up\<^sub>d t1) a (Node2 t2 b t3) c t4 = T\<^sub>d(Node2 (Node3 t1 a t2 b t3) c t4)" | 123"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)" | 124"node31 (Up\<^sub>d t1) a (Node4 t2 b t3 c t4 d t5) e t6 = T\<^sub>d(Node3 (Node2 t1 a t2) b (Node3 t3 c t4 d t5) e t6)" 125 126fun node32 :: "'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where 127"node32 t1 a (T\<^sub>d t2) b t3 = T\<^sub>d(Node3 t1 a t2 b t3)" | 128"node32 t1 a (Up\<^sub>d t2) b (Node2 t3 c t4) = T\<^sub>d(Node2 t1 a (Node3 t2 b t3 c t4))" | 129"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))" | 130"node32 t1 a (Up\<^sub>d t2) b (Node4 t3 c t4 d t5 e t6) = T\<^sub>d(Node3 t1 a (Node2 t2 b t3) c (Node3 t4 d t5 e t6))" 131 132fun node33 :: "'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a up\<^sub>d" where 133"node33 l a m b (T\<^sub>d r) = T\<^sub>d(Node3 l a m b r)" | 134"node33 t1 a (Node2 t2 b t3) c (Up\<^sub>d t4) = T\<^sub>d(Node2 t1 a (Node3 t2 b t3 c t4))" | 135"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))" | 136"node33 t1 a (Node4 t2 b t3 c t4 d t5) e (Up\<^sub>d t6) = T\<^sub>d(Node3 t1 a (Node2 t2 b t3) c (Node3 t4 d t5 e t6))" 137 138fun node41 :: "'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where 139"node41 (T\<^sub>d t1) a t2 b t3 c t4 = T\<^sub>d(Node4 t1 a t2 b t3 c t4)" | 140"node41 (Up\<^sub>d t1) a (Node2 t2 b t3) c t4 d t5 = T\<^sub>d(Node3 (Node3 t1 a t2 b t3) c t4 d t5)" | 141"node41 (Up\<^sub>d t1) a (Node3 t2 b t3 c t4) d t5 e t6 = T\<^sub>d(Node4 (Node2 t1 a t2) b (Node2 t3 c t4) d t5 e t6)" | 142"node41 (Up\<^sub>d t1) a (Node4 t2 b t3 c t4 d t5) e t6 f t7 = T\<^sub>d(Node4 (Node2 t1 a t2) b (Node3 t3 c t4 d t5) e t6 f t7)" 143 144fun node42 :: "'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where 145"node42 t1 a (T\<^sub>d t2) b t3 c t4 = T\<^sub>d(Node4 t1 a t2 b t3 c t4)" | 146"node42 (Node2 t1 a t2) b (Up\<^sub>d t3) c t4 d t5 = T\<^sub>d(Node3 (Node3 t1 a t2 b t3) c t4 d t5)" | 147"node42 (Node3 t1 a t2 b t3) c (Up\<^sub>d t4) d t5 e t6 = T\<^sub>d(Node4 (Node2 t1 a t2) b (Node2 t3 c t4) d t5 e t6)" | 148"node42 (Node4 t1 a t2 b t3 c t4) d (Up\<^sub>d t5) e t6 f t7 = T\<^sub>d(Node4 (Node2 t1 a t2) b (Node3 t3 c t4 d t5) e t6 f t7)" 149 150fun node43 :: "'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where 151"node43 t1 a t2 b (T\<^sub>d t3) c t4 = T\<^sub>d(Node4 t1 a t2 b t3 c t4)" | 152"node43 t1 a (Node2 t2 b t3) c (Up\<^sub>d t4) d t5 = T\<^sub>d(Node3 t1 a (Node3 t2 b t3 c t4) d t5)" | 153"node43 t1 a (Node3 t2 b t3 c t4) d (Up\<^sub>d t5) e t6 = T\<^sub>d(Node4 t1 a (Node2 t2 b t3) c (Node2 t4 d t5) e t6)" | 154"node43 t1 a (Node4 t2 b t3 c t4 d t5) e (Up\<^sub>d t6) f t7 = T\<^sub>d(Node4 t1 a (Node2 t2 b t3) c (Node3 t4 d t5 e t6) f t7)" 155 156fun node44 :: "'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a up\<^sub>d" where 157"node44 t1 a t2 b t3 c (T\<^sub>d t4) = T\<^sub>d(Node4 t1 a t2 b t3 c t4)" | 158"node44 t1 a t2 b (Node2 t3 c t4) d (Up\<^sub>d t5) = T\<^sub>d(Node3 t1 a t2 b (Node3 t3 c t4 d t5))" | 159"node44 t1 a t2 b (Node3 t3 c t4 d t5) e (Up\<^sub>d t6) = T\<^sub>d(Node4 t1 a t2 b (Node2 t3 c t4) d (Node2 t5 e t6))" | 160"node44 t1 a t2 b (Node4 t3 c t4 d t5 e t6) f (Up\<^sub>d t7) = T\<^sub>d(Node4 t1 a t2 b (Node2 t3 c t4) d (Node3 t5 e t6 f t7))" 161 162fun split_min :: "'a tree234 \<Rightarrow> 'a * 'a up\<^sub>d" where 163"split_min (Node2 Leaf a Leaf) = (a, Up\<^sub>d Leaf)" | 164"split_min (Node3 Leaf a Leaf b Leaf) = (a, T\<^sub>d(Node2 Leaf b Leaf))" | 165"split_min (Node4 Leaf a Leaf b Leaf c Leaf) = (a, T\<^sub>d(Node3 Leaf b Leaf c Leaf))" | 166"split_min (Node2 l a r) = (let (x,l') = split_min l in (x, node21 l' a r))" | 167"split_min (Node3 l a m b r) = (let (x,l') = split_min l in (x, node31 l' a m b r))" | 168"split_min (Node4 l a m b n c r) = (let (x,l') = split_min l in (x, node41 l' a m b n c r))" 169 170fun del :: "'a::linorder \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where 171"del k Leaf = T\<^sub>d Leaf" | 172"del k (Node2 Leaf p Leaf) = (if k=p then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf p Leaf))" | 173"del k (Node3 Leaf p Leaf q Leaf) = T\<^sub>d(if k=p then Node2 Leaf q Leaf 174 else if k=q then Node2 Leaf p Leaf else Node3 Leaf p Leaf q Leaf)" | 175"del k (Node4 Leaf a Leaf b Leaf c Leaf) = 176 T\<^sub>d(if k=a then Node3 Leaf b Leaf c Leaf else 177 if k=b then Node3 Leaf a Leaf c Leaf else 178 if k=c then Node3 Leaf a Leaf b Leaf 179 else Node4 Leaf a Leaf b Leaf c Leaf)" | 180"del k (Node2 l a r) = (case cmp k a of 181 LT \<Rightarrow> node21 (del k l) a r | 182 GT \<Rightarrow> node22 l a (del k r) | 183 EQ \<Rightarrow> let (a',t) = split_min r in node22 l a' t)" | 184"del k (Node3 l a m b r) = (case cmp k a of 185 LT \<Rightarrow> node31 (del k l) a m b r | 186 EQ \<Rightarrow> let (a',m') = split_min m in node32 l a' m' b r | 187 GT \<Rightarrow> (case cmp k b of 188 LT \<Rightarrow> node32 l a (del k m) b r | 189 EQ \<Rightarrow> let (b',r') = split_min r in node33 l a m b' r' | 190 GT \<Rightarrow> node33 l a m b (del k r)))" | 191"del k (Node4 l a m b n c r) = (case cmp k b of 192 LT \<Rightarrow> (case cmp k a of 193 LT \<Rightarrow> node41 (del k l) a m b n c r | 194 EQ \<Rightarrow> let (a',m') = split_min m in node42 l a' m' b n c r | 195 GT \<Rightarrow> node42 l a (del k m) b n c r) | 196 EQ \<Rightarrow> let (b',n') = split_min n in node43 l a m b' n' c r | 197 GT \<Rightarrow> (case cmp k c of 198 LT \<Rightarrow> node43 l a m b (del k n) c r | 199 EQ \<Rightarrow> let (c',r') = split_min r in node44 l a m b n c' r' | 200 GT \<Rightarrow> node44 l a m b n c (del k r)))" 201 202definition delete :: "'a::linorder \<Rightarrow> 'a tree234 \<Rightarrow> 'a tree234" where 203"delete x t = tree\<^sub>d(del x t)" 204 205 206subsection "Functional correctness" 207 208subsubsection \<open>Functional correctness of isin:\<close> 209 210lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> set (inorder t))" 211by (induction t) (auto simp: isin_simps ball_Un) 212 213 214subsubsection \<open>Functional correctness of insert:\<close> 215 216lemma inorder_ins: 217 "sorted(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(ins x t)) = ins_list x (inorder t)" 218by(induction t) (auto, auto simp: ins_list_simps split!: if_splits up\<^sub>i.splits) 219 220lemma inorder_insert: 221 "sorted(inorder t) \<Longrightarrow> inorder(insert a t) = ins_list a (inorder t)" 222by(simp add: insert_def inorder_ins) 223 224 225subsubsection \<open>Functional correctness of delete\<close> 226 227lemma inorder_node21: "height r > 0 \<Longrightarrow> 228 inorder (tree\<^sub>d (node21 l' a r)) = inorder (tree\<^sub>d l') @ a # inorder r" 229by(induct l' a r rule: node21.induct) auto 230 231lemma inorder_node22: "height l > 0 \<Longrightarrow> 232 inorder (tree\<^sub>d (node22 l a r')) = inorder l @ a # inorder (tree\<^sub>d r')" 233by(induct l a r' rule: node22.induct) auto 234 235lemma inorder_node31: "height m > 0 \<Longrightarrow> 236 inorder (tree\<^sub>d (node31 l' a m b r)) = inorder (tree\<^sub>d l') @ a # inorder m @ b # inorder r" 237by(induct l' a m b r rule: node31.induct) auto 238 239lemma inorder_node32: "height r > 0 \<Longrightarrow> 240 inorder (tree\<^sub>d (node32 l a m' b r)) = inorder l @ a # inorder (tree\<^sub>d m') @ b # inorder r" 241by(induct l a m' b r rule: node32.induct) auto 242 243lemma inorder_node33: "height m > 0 \<Longrightarrow> 244 inorder (tree\<^sub>d (node33 l a m b r')) = inorder l @ a # inorder m @ b # inorder (tree\<^sub>d r')" 245by(induct l a m b r' rule: node33.induct) auto 246 247lemma inorder_node41: "height m > 0 \<Longrightarrow> 248 inorder (tree\<^sub>d (node41 l' a m b n c r)) = inorder (tree\<^sub>d l') @ a # inorder m @ b # inorder n @ c # inorder r" 249by(induct l' a m b n c r rule: node41.induct) auto 250 251lemma inorder_node42: "height l > 0 \<Longrightarrow> 252 inorder (tree\<^sub>d (node42 l a m b n c r)) = inorder l @ a # inorder (tree\<^sub>d m) @ b # inorder n @ c # inorder r" 253by(induct l a m b n c r rule: node42.induct) auto 254 255lemma inorder_node43: "height m > 0 \<Longrightarrow> 256 inorder (tree\<^sub>d (node43 l a m b n c r)) = inorder l @ a # inorder m @ b # inorder(tree\<^sub>d n) @ c # inorder r" 257by(induct l a m b n c r rule: node43.induct) auto 258 259lemma inorder_node44: "height n > 0 \<Longrightarrow> 260 inorder (tree\<^sub>d (node44 l a m b n c r)) = inorder l @ a # inorder m @ b # inorder n @ c # inorder (tree\<^sub>d r)" 261by(induct l a m b n c r rule: node44.induct) auto 262 263lemmas inorder_nodes = inorder_node21 inorder_node22 264 inorder_node31 inorder_node32 inorder_node33 265 inorder_node41 inorder_node42 inorder_node43 inorder_node44 266 267lemma split_minD: 268 "split_min t = (x,t') \<Longrightarrow> bal t \<Longrightarrow> height t > 0 \<Longrightarrow> 269 x # inorder(tree\<^sub>d t') = inorder t" 270by(induction t arbitrary: t' rule: split_min.induct) 271 (auto simp: inorder_nodes split: prod.splits) 272 273lemma inorder_del: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow> 274 inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)" 275by(induction t rule: del.induct) 276 (auto simp: inorder_nodes del_list_simps split_minD split!: if_split prod.splits) 277 (* 30 secs (2016) *) 278 279lemma inorder_delete: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow> 280 inorder(delete x t) = del_list x (inorder t)" 281by(simp add: delete_def inorder_del) 282 283 284subsection \<open>Balancedness\<close> 285 286subsubsection "Proofs for insert" 287 288text\<open>First a standard proof that @{const ins} preserves @{const bal}.\<close> 289 290instantiation up\<^sub>i :: (type)height 291begin 292 293fun height_up\<^sub>i :: "'a up\<^sub>i \<Rightarrow> nat" where 294"height (T\<^sub>i t) = height t" | 295"height (Up\<^sub>i l a r) = height l" 296 297instance .. 298 299end 300 301lemma bal_ins: "bal t \<Longrightarrow> bal (tree\<^sub>i(ins a t)) \<and> height(ins a t) = height t" 302by (induct t) (auto split!: if_split up\<^sub>i.split) 303 304 305text\<open>Now an alternative proof (by Brian Huffman) that runs faster because 306two properties (balance and height) are combined in one predicate.\<close> 307 308inductive full :: "nat \<Rightarrow> 'a tree234 \<Rightarrow> bool" where 309"full 0 Leaf" | 310"\<lbrakk>full n l; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Node2 l p r)" | 311"\<lbrakk>full n l; full n m; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Node3 l p m q r)" | 312"\<lbrakk>full n l; full n m; full n m'; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Node4 l p m q m' q' r)" 313 314inductive_cases full_elims: 315 "full n Leaf" 316 "full n (Node2 l p r)" 317 "full n (Node3 l p m q r)" 318 "full n (Node4 l p m q m' q' r)" 319 320inductive_cases full_0_elim: "full 0 t" 321inductive_cases full_Suc_elim: "full (Suc n) t" 322 323lemma full_0_iff [simp]: "full 0 t \<longleftrightarrow> t = Leaf" 324 by (auto elim: full_0_elim intro: full.intros) 325 326lemma full_Leaf_iff [simp]: "full n Leaf \<longleftrightarrow> n = 0" 327 by (auto elim: full_elims intro: full.intros) 328 329lemma full_Suc_Node2_iff [simp]: 330 "full (Suc n) (Node2 l p r) \<longleftrightarrow> full n l \<and> full n r" 331 by (auto elim: full_elims intro: full.intros) 332 333lemma full_Suc_Node3_iff [simp]: 334 "full (Suc n) (Node3 l p m q r) \<longleftrightarrow> full n l \<and> full n m \<and> full n r" 335 by (auto elim: full_elims intro: full.intros) 336 337lemma full_Suc_Node4_iff [simp]: 338 "full (Suc n) (Node4 l p m q m' q' r) \<longleftrightarrow> full n l \<and> full n m \<and> full n m' \<and> full n r" 339 by (auto elim: full_elims intro: full.intros) 340 341lemma full_imp_height: "full n t \<Longrightarrow> height t = n" 342 by (induct set: full, simp_all) 343 344lemma full_imp_bal: "full n t \<Longrightarrow> bal t" 345 by (induct set: full, auto dest: full_imp_height) 346 347lemma bal_imp_full: "bal t \<Longrightarrow> full (height t) t" 348 by (induct t, simp_all) 349 350lemma bal_iff_full: "bal t \<longleftrightarrow> (\<exists>n. full n t)" 351 by (auto elim!: bal_imp_full full_imp_bal) 352 353text \<open>The @{const "insert"} function either preserves the height of the 354tree, or increases it by one. The constructor returned by the @{term 355"insert"} function determines which: A return value of the form @{term 356"T\<^sub>i t"} indicates that the height will be the same. A value of the 357form @{term "Up\<^sub>i l p r"} indicates an increase in height.\<close> 358 359primrec full\<^sub>i :: "nat \<Rightarrow> 'a up\<^sub>i \<Rightarrow> bool" where 360"full\<^sub>i n (T\<^sub>i t) \<longleftrightarrow> full n t" | 361"full\<^sub>i n (Up\<^sub>i l p r) \<longleftrightarrow> full n l \<and> full n r" 362 363lemma full\<^sub>i_ins: "full n t \<Longrightarrow> full\<^sub>i n (ins a t)" 364by (induct rule: full.induct) (auto, auto split: up\<^sub>i.split) 365 366text \<open>The @{const insert} operation preserves balance.\<close> 367 368lemma bal_insert: "bal t \<Longrightarrow> bal (insert a t)" 369unfolding bal_iff_full insert_def 370apply (erule exE) 371apply (drule full\<^sub>i_ins [of _ _ a]) 372apply (cases "ins a t") 373apply (auto intro: full.intros) 374done 375 376 377subsubsection "Proofs for delete" 378 379instantiation up\<^sub>d :: (type)height 380begin 381 382fun height_up\<^sub>d :: "'a up\<^sub>d \<Rightarrow> nat" where 383"height (T\<^sub>d t) = height t" | 384"height (Up\<^sub>d t) = height t + 1" 385 386instance .. 387 388end 389 390lemma bal_tree\<^sub>d_node21: 391 "\<lbrakk>bal r; bal (tree\<^sub>d l); height r = height l \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d (node21 l a r))" 392by(induct l a r rule: node21.induct) auto 393 394lemma bal_tree\<^sub>d_node22: 395 "\<lbrakk>bal(tree\<^sub>d r); bal l; height r = height l \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d (node22 l a r))" 396by(induct l a r rule: node22.induct) auto 397 398lemma bal_tree\<^sub>d_node31: 399 "\<lbrakk> bal (tree\<^sub>d l); bal m; bal r; height l = height r; height m = height r \<rbrakk> 400 \<Longrightarrow> bal (tree\<^sub>d (node31 l a m b r))" 401by(induct l a m b r rule: node31.induct) auto 402 403lemma bal_tree\<^sub>d_node32: 404 "\<lbrakk> bal l; bal (tree\<^sub>d m); bal r; height l = height r; height m = height r \<rbrakk> 405 \<Longrightarrow> bal (tree\<^sub>d (node32 l a m b r))" 406by(induct l a m b r rule: node32.induct) auto 407 408lemma bal_tree\<^sub>d_node33: 409 "\<lbrakk> bal l; bal m; bal(tree\<^sub>d r); height l = height r; height m = height r \<rbrakk> 410 \<Longrightarrow> bal (tree\<^sub>d (node33 l a m b r))" 411by(induct l a m b r rule: node33.induct) auto 412 413lemma bal_tree\<^sub>d_node41: 414 "\<lbrakk> bal (tree\<^sub>d l); bal m; bal n; bal r; height l = height r; height m = height r; height n = height r \<rbrakk> 415 \<Longrightarrow> bal (tree\<^sub>d (node41 l a m b n c r))" 416by(induct l a m b n c r rule: node41.induct) auto 417 418lemma bal_tree\<^sub>d_node42: 419 "\<lbrakk> bal l; bal (tree\<^sub>d m); bal n; bal r; height l = height r; height m = height r; height n = height r \<rbrakk> 420 \<Longrightarrow> bal (tree\<^sub>d (node42 l a m b n c r))" 421by(induct l a m b n c r rule: node42.induct) auto 422 423lemma bal_tree\<^sub>d_node43: 424 "\<lbrakk> bal l; bal m; bal (tree\<^sub>d n); bal r; height l = height r; height m = height r; height n = height r \<rbrakk> 425 \<Longrightarrow> bal (tree\<^sub>d (node43 l a m b n c r))" 426by(induct l a m b n c r rule: node43.induct) auto 427 428lemma bal_tree\<^sub>d_node44: 429 "\<lbrakk> bal l; bal m; bal n; bal (tree\<^sub>d r); height l = height r; height m = height r; height n = height r \<rbrakk> 430 \<Longrightarrow> bal (tree\<^sub>d (node44 l a m b n c r))" 431by(induct l a m b n c r rule: node44.induct) auto 432 433lemmas bals = bal_tree\<^sub>d_node21 bal_tree\<^sub>d_node22 434 bal_tree\<^sub>d_node31 bal_tree\<^sub>d_node32 bal_tree\<^sub>d_node33 435 bal_tree\<^sub>d_node41 bal_tree\<^sub>d_node42 bal_tree\<^sub>d_node43 bal_tree\<^sub>d_node44 436 437lemma height_node21: 438 "height r > 0 \<Longrightarrow> height(node21 l a r) = max (height l) (height r) + 1" 439by(induct l a r rule: node21.induct)(simp_all add: max.assoc) 440 441lemma height_node22: 442 "height l > 0 \<Longrightarrow> height(node22 l a r) = max (height l) (height r) + 1" 443by(induct l a r rule: node22.induct)(simp_all add: max.assoc) 444 445lemma height_node31: 446 "height m > 0 \<Longrightarrow> height(node31 l a m b r) = 447 max (height l) (max (height m) (height r)) + 1" 448by(induct l a m b r rule: node31.induct)(simp_all add: max_def) 449 450lemma height_node32: 451 "height r > 0 \<Longrightarrow> height(node32 l a m b r) = 452 max (height l) (max (height m) (height r)) + 1" 453by(induct l a m b r rule: node32.induct)(simp_all add: max_def) 454 455lemma height_node33: 456 "height m > 0 \<Longrightarrow> height(node33 l a m b r) = 457 max (height l) (max (height m) (height r)) + 1" 458by(induct l a m b r rule: node33.induct)(simp_all add: max_def) 459 460lemma height_node41: 461 "height m > 0 \<Longrightarrow> height(node41 l a m b n c r) = 462 max (height l) (max (height m) (max (height n) (height r))) + 1" 463by(induct l a m b n c r rule: node41.induct)(simp_all add: max_def) 464 465lemma height_node42: 466 "height l > 0 \<Longrightarrow> height(node42 l a m b n c r) = 467 max (height l) (max (height m) (max (height n) (height r))) + 1" 468by(induct l a m b n c r rule: node42.induct)(simp_all add: max_def) 469 470lemma height_node43: 471 "height m > 0 \<Longrightarrow> height(node43 l a m b n c r) = 472 max (height l) (max (height m) (max (height n) (height r))) + 1" 473by(induct l a m b n c r rule: node43.induct)(simp_all add: max_def) 474 475lemma height_node44: 476 "height n > 0 \<Longrightarrow> height(node44 l a m b n c r) = 477 max (height l) (max (height m) (max (height n) (height r))) + 1" 478by(induct l a m b n c r rule: node44.induct)(simp_all add: max_def) 479 480lemmas heights = height_node21 height_node22 481 height_node31 height_node32 height_node33 482 height_node41 height_node42 height_node43 height_node44 483 484lemma height_split_min: 485 "split_min t = (x, t') \<Longrightarrow> height t > 0 \<Longrightarrow> bal t \<Longrightarrow> height t' = height t" 486by(induct t arbitrary: x t' rule: split_min.induct) 487 (auto simp: heights split: prod.splits) 488 489lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t" 490by(induction x t rule: del.induct) 491 (auto simp add: heights height_split_min split!: if_split prod.split) 492 493lemma bal_split_min: 494 "\<lbrakk> split_min t = (x, t'); bal t; height t > 0 \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d t')" 495by(induct t arbitrary: x t' rule: split_min.induct) 496 (auto simp: heights height_split_min bals split: prod.splits) 497 498lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))" 499by(induction x t rule: del.induct) 500 (auto simp: bals bal_split_min height_del height_split_min split!: if_split prod.split) 501 502corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)" 503by(simp add: delete_def bal_tree\<^sub>d_del) 504 505subsection \<open>Overall Correctness\<close> 506 507interpretation S: Set_by_Ordered 508where empty = empty and isin = isin and insert = insert and delete = delete 509and inorder = inorder and inv = bal 510proof (standard, goal_cases) 511 case 2 thus ?case by(simp add: isin_set) 512next 513 case 3 thus ?case by(simp add: inorder_insert) 514next 515 case 4 thus ?case by(simp add: inorder_delete) 516next 517 case 6 thus ?case by(simp add: bal_insert) 518next 519 case 7 thus ?case by(simp add: bal_delete) 520qed (simp add: empty_def)+ 521 522end 523