src/HOL/Data_Structures/Brother12_Set.thy
 author nipkow Sun Dec 06 11:26:38 2015 +0100 (2015-12-06) changeset 61792 8dd150a50acc parent 61789 9ce1a397410a child 61809 81d34cf268d8 permissions -rw-r--r--
tuned
 nipkow@61784 1 (* Author: Tobias Nipkow *) nipkow@61784 2 nipkow@61784 3 section \A 1-2 Brother Tree Implementation of Sets\ nipkow@61784 4 nipkow@61784 5 theory Brother12_Set nipkow@61784 6 imports nipkow@61784 7 Cmp nipkow@61784 8 Set_by_Ordered nipkow@61784 9 begin nipkow@61784 10 nipkow@61784 11 subsection \Data Type and Operations\ nipkow@61784 12 nipkow@61784 13 datatype 'a bro = nipkow@61784 14 N0 | nipkow@61784 15 N1 "'a bro" | nipkow@61784 16 N2 "'a bro" 'a "'a bro" | nipkow@61784 17 (* auxiliary constructors: *) nipkow@61784 18 L2 'a | nipkow@61784 19 N3 "'a bro" 'a "'a bro" 'a "'a bro" nipkow@61784 20 nipkow@61784 21 fun inorder :: "'a bro \ 'a list" where nipkow@61784 22 "inorder N0 = []" | nipkow@61784 23 "inorder (N1 t) = inorder t" | nipkow@61784 24 "inorder (N2 l a r) = inorder l @ a # inorder r" | nipkow@61784 25 "inorder (L2 a) = [a]" | nipkow@61784 26 "inorder (N3 t1 a1 t2 a2 t3) = inorder t1 @ a1 # inorder t2 @ a2 # inorder t3" nipkow@61784 27 nipkow@61784 28 fun isin :: "'a bro \ 'a::cmp \ bool" where nipkow@61784 29 "isin N0 x = False" | nipkow@61784 30 "isin (N1 t) x = isin t x" | nipkow@61784 31 "isin (N2 l a r) x = nipkow@61784 32 (case cmp x a of nipkow@61784 33 LT \ isin l x | nipkow@61784 34 EQ \ True | nipkow@61784 35 GT \ isin r x)" nipkow@61784 36 nipkow@61784 37 fun n1 :: "'a bro \ 'a bro" where nipkow@61784 38 "n1 (L2 a) = N2 N0 a N0" | nipkow@61784 39 "n1 (N3 t1 a1 t2 a2 t3) = N2 (N2 t1 a1 t2) a2 (N1 t3)" | nipkow@61784 40 "n1 t = N1 t" nipkow@61784 41 nipkow@61784 42 hide_const (open) insert nipkow@61784 43 nipkow@61784 44 locale insert nipkow@61784 45 begin nipkow@61784 46 nipkow@61784 47 fun n2 :: "'a bro \ 'a \ 'a bro \ 'a bro" where nipkow@61784 48 "n2 (L2 a1) a2 t = N3 N0 a1 N0 a2 t" | nipkow@61784 49 "n2 (N3 t1 a1 t2 a2 t3) a3 (N1 t4) = N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4)" | nipkow@61784 50 "n2 (N3 t1 a1 t2 a2 t3) a3 t4 = N3 (N2 t1 a1 t2) a2 (N1 t3) a3 t4" | nipkow@61784 51 "n2 t1 a1 (L2 a2) = N3 t1 a1 N0 a2 N0" | nipkow@61784 52 "n2 (N1 t1) a1 (N3 t2 a2 t3 a3 t4) = N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4)" | nipkow@61784 53 "n2 t1 a1 (N3 t2 a2 t3 a3 t4) = N3 t1 a1 (N1 t2) a2 (N2 t3 a3 t4)" | nipkow@61784 54 "n2 t1 a t2 = N2 t1 a t2" nipkow@61784 55 nipkow@61784 56 fun ins :: "'a::cmp \ 'a bro \ 'a bro" where nipkow@61789 57 "ins x N0 = L2 x" | nipkow@61789 58 "ins x (N1 t) = n1 (ins x t)" | nipkow@61789 59 "ins x (N2 l a r) = nipkow@61789 60 (case cmp x a of nipkow@61789 61 LT \ n2 (ins x l) a r | nipkow@61789 62 EQ \ N2 l a r | nipkow@61789 63 GT \ n2 l a (ins x r))" nipkow@61784 64 nipkow@61784 65 fun tree :: "'a bro \ 'a bro" where nipkow@61784 66 "tree (L2 a) = N2 N0 a N0" | nipkow@61784 67 "tree (N3 t1 a1 t2 a2 t3) = N2 (N2 t1 a1 t2) a2 (N1 t3)" | nipkow@61784 68 "tree t = t" nipkow@61784 69 nipkow@61784 70 definition insert :: "'a::cmp \ 'a bro \ 'a bro" where nipkow@61784 71 "insert x t = tree(ins x t)" nipkow@61784 72 nipkow@61784 73 end nipkow@61784 74 nipkow@61784 75 locale delete nipkow@61784 76 begin nipkow@61784 77 nipkow@61784 78 fun n2 :: "'a bro \ 'a \ 'a bro \ 'a bro" where nipkow@61784 79 "n2 (N1 t1) a1 (N1 t2) = N1 (N2 t1 a1 t2)" | nipkow@61784 80 "n2 (N1 (N1 t1)) a1 (N2 (N1 t2) a2 (N2 t3 a3 t4)) = nipkow@61784 81 N1 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4))" | nipkow@61784 82 "n2 (N1 (N1 t1)) a1 (N2 (N2 t2 a2 t3) a3 (N1 t4)) = nipkow@61784 83 N1 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4))" | nipkow@61784 84 "n2 (N1 (N1 t1)) a1 (N2 (N2 t2 a2 t3) a3 (N2 t4 a4 t5)) = nipkow@61784 85 N2 (N2 (N1 t1) a1 (N2 t2 a2 t3)) a3 (N1 (N2 t4 a4 t5))" | nipkow@61784 86 "n2 (N2 (N1 t1) a1 (N2 t2 a2 t3)) a3 (N1 (N1 t4)) = nipkow@61784 87 N1 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4))" | nipkow@61784 88 "n2 (N2 (N2 t1 a1 t2) a2 (N1 t3)) a3 (N1 (N1 t4)) = nipkow@61784 89 N1 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4))" | nipkow@61784 90 "n2 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4)) a5 (N1 (N1 t5)) = nipkow@61784 91 N2 (N1 (N2 t1 a1 t2)) a2 (N2 (N2 t3 a3 t4) a5 (N1 t5))" | nipkow@61784 92 "n2 t1 a1 t2 = N2 t1 a1 t2" nipkow@61784 93 nipkow@61784 94 fun del_min :: "'a bro \ ('a \ 'a bro) option" where nipkow@61784 95 "del_min N0 = None" | nipkow@61784 96 "del_min (N1 t) = nipkow@61784 97 (case del_min t of nipkow@61784 98 None \ None | nipkow@61784 99 Some (a, t') \ Some (a, N1 t'))" | nipkow@61784 100 "del_min (N2 t1 a t2) = nipkow@61784 101 (case del_min t1 of nipkow@61784 102 None \ Some (a, N1 t2) | nipkow@61784 103 Some (b, t1') \ Some (b, n2 t1' a t2))" nipkow@61784 104 nipkow@61784 105 fun del :: "'a::cmp \ 'a bro \ 'a bro" where nipkow@61784 106 "del _ N0 = N0" | nipkow@61784 107 "del x (N1 t) = N1 (del x t)" | nipkow@61784 108 "del x (N2 l a r) = nipkow@61784 109 (case cmp x a of nipkow@61784 110 LT \ n2 (del x l) a r | nipkow@61784 111 GT \ n2 l a (del x r) | nipkow@61784 112 EQ \ (case del_min r of nipkow@61784 113 None \ N1 l | nipkow@61784 114 Some (b, r') \ n2 l b r'))" nipkow@61784 115 nipkow@61784 116 fun tree :: "'a bro \ 'a bro" where nipkow@61784 117 "tree (N1 t) = t" | nipkow@61784 118 "tree t = t" nipkow@61784 119 nipkow@61784 120 definition delete :: "'a::cmp \ 'a bro \ 'a bro" where nipkow@61784 121 "delete a t = tree (del a t)" nipkow@61784 122 nipkow@61784 123 end nipkow@61784 124 nipkow@61784 125 subsection \Invariants\ nipkow@61784 126 nipkow@61784 127 fun B :: "nat \ 'a bro set" nipkow@61784 128 and U :: "nat \ 'a bro set" where nipkow@61784 129 "B 0 = {N0}" | nipkow@61784 130 "B (Suc h) = { N2 t1 a t2 | t1 a t2. nipkow@61784 131 t1 \ B h \ U h \ t2 \ B h \ t1 \ B h \ t2 \ B h \ U h}" | nipkow@61784 132 "U 0 = {}" | nipkow@61784 133 "U (Suc h) = N1 ` B h" nipkow@61784 134 nipkow@61784 135 abbreviation "T h \ B h \ U h" nipkow@61784 136 nipkow@61784 137 fun Bp :: "nat \ 'a bro set" where nipkow@61784 138 "Bp 0 = B 0 \ L2 ` UNIV" | nipkow@61784 139 "Bp (Suc 0) = B (Suc 0) \ {N3 N0 a N0 b N0|a b. True}" | nipkow@61784 140 "Bp (Suc(Suc h)) = B (Suc(Suc h)) \ nipkow@61784 141 {N3 t1 a t2 b t3 | t1 a t2 b t3. t1 \ B (Suc h) \ t2 \ U (Suc h) \ t3 \ B (Suc h)}" nipkow@61784 142 nipkow@61784 143 fun Um :: "nat \ 'a bro set" where nipkow@61784 144 "Um 0 = {}" | nipkow@61784 145 "Um (Suc h) = N1 ` T h" nipkow@61784 146 nipkow@61784 147 nipkow@61784 148 subsection "Functional Correctness Proofs" nipkow@61784 149 nipkow@61784 150 subsubsection "Proofs for isin" nipkow@61784 151 nipkow@61784 152 lemma nipkow@61784 153 "t \ T h \ sorted(inorder t) \ isin t x = (x \ elems(inorder t))" nipkow@61784 154 by(induction h arbitrary: t) (fastforce simp: elems_simps1 split: if_splits)+ nipkow@61784 155 nipkow@61784 156 lemma isin_set: "t \ T h \ nipkow@61784 157 sorted(inorder t) \ isin t x = (x \ elems(inorder t))" nipkow@61784 158 by(induction h arbitrary: t) (auto simp: elems_simps2 split: if_splits) nipkow@61784 159 nipkow@61784 160 subsubsection "Proofs for insertion" nipkow@61784 161 nipkow@61784 162 lemma inorder_n1: "inorder(n1 t) = inorder t" nipkow@61784 163 by(induction t rule: n1.induct) (auto simp: sorted_lems) nipkow@61784 164 nipkow@61784 165 context insert nipkow@61784 166 begin nipkow@61784 167 nipkow@61784 168 lemma inorder_n2: "inorder(n2 l a r) = inorder l @ a # inorder r" nipkow@61784 169 by(cases "(l,a,r)" rule: n2.cases) (auto simp: sorted_lems) nipkow@61784 170 nipkow@61784 171 lemma inorder_tree: "inorder(tree t) = inorder t" nipkow@61784 172 by(cases t) auto nipkow@61784 173 nipkow@61784 174 lemma inorder_ins: "t \ T h \ nipkow@61784 175 sorted(inorder t) \ inorder(ins a t) = ins_list a (inorder t)" nipkow@61784 176 by(induction h arbitrary: t) (auto simp: ins_list_simps inorder_n1 inorder_n2) nipkow@61784 177 nipkow@61784 178 lemma inorder_insert: "t \ T h \ nipkow@61784 179 sorted(inorder t) \ inorder(insert a t) = ins_list a (inorder t)" nipkow@61784 180 by(simp add: insert_def inorder_ins inorder_tree) nipkow@61784 181 nipkow@61784 182 end nipkow@61784 183 nipkow@61784 184 subsubsection \Proofs for deletion\ nipkow@61784 185 nipkow@61784 186 context delete nipkow@61784 187 begin nipkow@61784 188 nipkow@61784 189 lemma inorder_tree: "inorder(tree t) = inorder t" nipkow@61784 190 by(cases t) auto nipkow@61784 191 nipkow@61784 192 lemma inorder_n2: "inorder(n2 l a r) = inorder l @ a # inorder r" nipkow@61784 193 by(induction l a r rule: n2.induct) (auto) nipkow@61784 194 nipkow@61784 195 lemma inorder_del_min: nipkow@61792 196 "t \ T h \ (del_min t = None \ inorder t = []) \ nipkow@61784 197 (del_min t = Some(a,t') \ inorder t = a # inorder t')" nipkow@61784 198 by(induction h arbitrary: t a t') (auto simp: inorder_n2 split: option.splits) nipkow@61784 199 nipkow@61784 200 lemma inorder_del: nipkow@61792 201 "t \ T h \ sorted(inorder t) \ inorder(del x t) = del_list x (inorder t)" nipkow@61792 202 by(induction h arbitrary: t) (auto simp: del_list_simps inorder_n2 nipkow@61792 203 inorder_del_min[OF UnI1] inorder_del_min[OF UnI2] split: option.splits) nipkow@61792 204 nipkow@61792 205 lemma inorder_delete: nipkow@61792 206 "t \ T h \ sorted(inorder t) \ inorder(delete x t) = del_list x (inorder t)" nipkow@61792 207 by(simp add: delete_def inorder_del inorder_tree) nipkow@61784 208 nipkow@61784 209 end nipkow@61784 210 nipkow@61784 211 nipkow@61784 212 subsection \Invariant Proofs\ nipkow@61784 213 nipkow@61789 214 subsubsection \Proofs for insertion\ nipkow@61784 215 nipkow@61784 216 lemma n1_type: "t \ Bp h \ n1 t \ T (Suc h)" nipkow@61784 217 by(cases h rule: Bp.cases) auto nipkow@61784 218 nipkow@61784 219 context insert nipkow@61784 220 begin nipkow@61784 221 nipkow@61784 222 lemma tree_type1: "t \ Bp h \ tree t \ B h \ B (Suc h)" nipkow@61784 223 by(cases h rule: Bp.cases) auto nipkow@61784 224 nipkow@61784 225 lemma tree_type2: "t \ T h \ tree t \ T h" nipkow@61784 226 by(cases h) auto nipkow@61784 227 nipkow@61784 228 lemma n2_type: nipkow@61784 229 "(t1 \ Bp h \ t2 \ T h \ n2 t1 a t2 \ Bp (Suc h)) \ nipkow@61784 230 (t1 \ T h \ t2 \ Bp h \ n2 t1 a t2 \ Bp (Suc h))" nipkow@61784 231 apply(cases h rule: Bp.cases) nipkow@61784 232 apply (auto)[2] nipkow@61784 233 apply(rule conjI impI | erule conjE exE imageE | simp | erule disjE)+ nipkow@61784 234 done nipkow@61784 235 nipkow@61784 236 lemma Bp_if_B: "t \ B h \ t \ Bp h" nipkow@61784 237 by (cases h rule: Bp.cases) simp_all nipkow@61784 238 nipkow@61784 239 text{* An automatic proof: *} nipkow@61784 240 nipkow@61784 241 lemma nipkow@61784 242 "(t \ B h \ ins x t \ Bp h) \ (t \ U h \ ins x t \ T h)" nipkow@61784 243 apply(induction h arbitrary: t) nipkow@61784 244 apply (simp) nipkow@61784 245 apply (fastforce simp: Bp_if_B n2_type dest: n1_type) nipkow@61784 246 done nipkow@61784 247 nipkow@61784 248 text{* A detailed proof: *} nipkow@61784 249 nipkow@61784 250 lemma ins_type: nipkow@61784 251 shows "t \ B h \ ins x t \ Bp h" and "t \ U h \ ins x t \ T h" nipkow@61784 252 proof(induction h arbitrary: t) nipkow@61784 253 case 0 nipkow@61784 254 { case 1 thus ?case by simp nipkow@61784 255 next nipkow@61784 256 case 2 thus ?case by simp } nipkow@61784 257 next nipkow@61784 258 case (Suc h) nipkow@61784 259 { case 1 nipkow@61784 260 then obtain t1 a t2 where [simp]: "t = N2 t1 a t2" and nipkow@61784 261 t1: "t1 \ T h" and t2: "t2 \ T h" and t12: "t1 \ B h \ t2 \ B h" nipkow@61784 262 by auto nipkow@61784 263 { assume "x < a" nipkow@61784 264 hence "?case \ n2 (ins x t1) a t2 \ Bp (Suc h)" by simp nipkow@61784 265 also have "\" nipkow@61784 266 proof cases nipkow@61784 267 assume "t1 \ B h" nipkow@61784 268 with t2 show ?thesis by (simp add: Suc.IH(1) n2_type) nipkow@61784 269 next nipkow@61784 270 assume "t1 \ B h" nipkow@61784 271 hence 1: "t1 \ U h" and 2: "t2 \ B h" using t1 t12 by auto nipkow@61784 272 show ?thesis by (metis Suc.IH(2)[OF 1] Bp_if_B[OF 2] n2_type) nipkow@61784 273 qed nipkow@61784 274 finally have ?case . nipkow@61784 275 } nipkow@61784 276 moreover nipkow@61784 277 { assume "a < x" nipkow@61784 278 hence "?case \ n2 t1 a (ins x t2) \ Bp (Suc h)" by simp nipkow@61784 279 also have "\" nipkow@61784 280 proof cases nipkow@61784 281 assume "t2 \ B h" nipkow@61784 282 with t1 show ?thesis by (simp add: Suc.IH(1) n2_type) nipkow@61784 283 next nipkow@61784 284 assume "t2 \ B h" nipkow@61784 285 hence 1: "t1 \ B h" and 2: "t2 \ U h" using t2 t12 by auto nipkow@61784 286 show ?thesis by (metis Bp_if_B[OF 1] Suc.IH(2)[OF 2] n2_type) nipkow@61784 287 qed nipkow@61784 288 } nipkow@61784 289 moreover nipkow@61784 290 { assume "x = a" nipkow@61784 291 from 1 have "t \ Bp (Suc h)" by(rule Bp_if_B) nipkow@61784 292 hence "?case" using `x = a` by simp nipkow@61784 293 } nipkow@61784 294 ultimately show ?case by auto nipkow@61784 295 next nipkow@61784 296 case 2 thus ?case using Suc(1) n1_type by fastforce } nipkow@61784 297 qed nipkow@61784 298 nipkow@61784 299 lemma insert_type: nipkow@61784 300 "t \ T h \ insert x t \ T h \ T (Suc h)" nipkow@61784 301 unfolding insert_def by (metis Un_iff ins_type tree_type1 tree_type2) nipkow@61784 302 nipkow@61784 303 end nipkow@61784 304 nipkow@61789 305 subsubsection "Proofs for deletion" nipkow@61784 306 nipkow@61784 307 lemma B_simps[simp]: nipkow@61784 308 "N1 t \ B h = False" nipkow@61784 309 "L2 y \ B h = False" nipkow@61784 310 "(N3 t1 a1 t2 a2 t3) \ B h = False" nipkow@61784 311 "N0 \ B h \ h = 0" nipkow@61784 312 by (cases h, auto)+ nipkow@61784 313 nipkow@61784 314 context delete nipkow@61784 315 begin nipkow@61784 316 nipkow@61784 317 lemma n2_type1: nipkow@61784 318 "\t1 \ Um h; t2 \ B h\ \ n2 t1 a t2 \ T (Suc h)" nipkow@61784 319 apply(cases h rule: Bp.cases) nipkow@61784 320 apply auto[2] nipkow@61784 321 apply(erule exE bexE conjE imageE | simp | erule disjE)+ nipkow@61784 322 done nipkow@61784 323 nipkow@61784 324 lemma n2_type2: nipkow@61784 325 "\t1 \ B h ; t2 \ Um h \ \ n2 t1 a t2 \ T (Suc h)" nipkow@61784 326 apply(cases h rule: Bp.cases) nipkow@61784 327 apply auto[2] nipkow@61784 328 apply(erule exE bexE conjE imageE | simp | erule disjE)+ nipkow@61784 329 done nipkow@61784 330 nipkow@61784 331 lemma n2_type3: nipkow@61784 332 "\t1 \ T h ; t2 \ T h \ \ n2 t1 a t2 \ T (Suc h)" nipkow@61784 333 apply(cases h rule: Bp.cases) nipkow@61784 334 apply auto[2] nipkow@61784 335 apply(erule exE bexE conjE imageE | simp | erule disjE)+ nipkow@61784 336 done nipkow@61784 337 nipkow@61784 338 lemma del_minNoneN0: "\t \ B h; del_min t = None\ \ t = N0" nipkow@61784 339 by (cases t) (auto split: option.splits) nipkow@61784 340 nipkow@61784 341 lemma del_minNoneN1 : "\t \ U h; del_min t = None\ \ t = N1 N0" nipkow@61784 342 by (cases h) (auto simp: del_minNoneN0 split: option.splits) nipkow@61784 343 nipkow@61784 344 lemma del_min_type: nipkow@61784 345 "t \ B h \ del_min t = Some (a, t') \ t' \ T h" nipkow@61784 346 "t \ U h \ del_min t = Some (a, t') \ t' \ Um h" nipkow@61784 347 proof (induction h arbitrary: t a t') nipkow@61784 348 case (Suc h) nipkow@61784 349 { case 1 nipkow@61784 350 then obtain t1 a t2 where [simp]: "t = N2 t1 a t2" and nipkow@61784 351 t12: "t1 \ T h" "t2 \ T h" "t1 \ B h \ t2 \ B h" nipkow@61784 352 by auto nipkow@61784 353 show ?case nipkow@61784 354 proof (cases "del_min t1") nipkow@61784 355 case None nipkow@61784 356 show ?thesis nipkow@61784 357 proof cases nipkow@61784 358 assume "t1 \ B h" nipkow@61784 359 with del_minNoneN0[OF this None] 1 show ?thesis by(auto) nipkow@61784 360 next nipkow@61784 361 assume "t1 \ B h" nipkow@61784 362 thus ?thesis using 1 None by (auto) nipkow@61784 363 qed nipkow@61784 364 next nipkow@61784 365 case [simp]: (Some bt') nipkow@61784 366 obtain b t1' where [simp]: "bt' = (b,t1')" by fastforce nipkow@61784 367 show ?thesis nipkow@61784 368 proof cases nipkow@61784 369 assume "t1 \ B h" nipkow@61784 370 from Suc.IH(1)[OF this] 1 have "t1' \ T h" by simp nipkow@61784 371 from n2_type3[OF this t12(2)] 1 show ?thesis by auto nipkow@61784 372 next nipkow@61784 373 assume "t1 \ B h" nipkow@61784 374 hence t1: "t1 \ U h" and t2: "t2 \ B h" using t12 by auto nipkow@61784 375 from Suc.IH(2)[OF t1] have "t1' \ Um h" by simp nipkow@61784 376 from n2_type1[OF this t2] 1 show ?thesis by auto nipkow@61784 377 qed nipkow@61784 378 qed nipkow@61784 379 } nipkow@61784 380 { case 2 nipkow@61784 381 then obtain t1 where [simp]: "t = N1 t1" and t1: "t1 \ B h" by auto nipkow@61784 382 show ?case nipkow@61784 383 proof (cases "del_min t1") nipkow@61784 384 case None nipkow@61784 385 with del_minNoneN0[OF t1 None] 2 show ?thesis by(auto) nipkow@61784 386 next nipkow@61784 387 case [simp]: (Some bt') nipkow@61784 388 obtain b t1' where [simp]: "bt' = (b,t1')" by fastforce nipkow@61784 389 from Suc.IH(1)[OF t1] have "t1' \ T h" by simp nipkow@61784 390 thus ?thesis using 2 by auto nipkow@61784 391 qed nipkow@61784 392 } nipkow@61784 393 qed auto nipkow@61784 394 nipkow@61784 395 lemma del_type: nipkow@61784 396 "t \ B h \ del x t \ T h" nipkow@61784 397 "t \ U h \ del x t \ Um h" nipkow@61784 398 proof (induction h arbitrary: x t) nipkow@61784 399 case (Suc h) nipkow@61784 400 { case 1 nipkow@61784 401 then obtain l a r where [simp]: "t = N2 l a r" and nipkow@61784 402 lr: "l \ T h" "r \ T h" "l \ B h \ r \ B h" by auto nipkow@61784 403 { assume "x < a" nipkow@61784 404 have ?case nipkow@61784 405 proof cases nipkow@61784 406 assume "l \ B h" nipkow@61784 407 from n2_type3[OF Suc.IH(1)[OF this] lr(2)] nipkow@61784 408 show ?thesis using `x B h" nipkow@61784 411 hence "l \ U h" "r \ B h" using lr by auto nipkow@61784 412 from n2_type1[OF Suc.IH(2)[OF this(1)] this(2)] nipkow@61784 413 show ?thesis using `x a" nipkow@61784 417 have ?case nipkow@61784 418 proof cases nipkow@61784 419 assume "r \ B h" nipkow@61784 420 from n2_type3[OF lr(1) Suc.IH(1)[OF this]] nipkow@61784 421 show ?thesis using `x>a` by(simp) nipkow@61784 422 next nipkow@61784 423 assume "r \ B h" nipkow@61784 424 hence "l \ B h" "r \ U h" using lr by auto nipkow@61784 425 from n2_type2[OF this(1) Suc.IH(2)[OF this(2)]] nipkow@61784 426 show ?thesis using `x>a` by(simp) nipkow@61784 427 qed nipkow@61784 428 } moreover nipkow@61784 429 { assume [simp]: "x=a" nipkow@61784 430 have ?case nipkow@61784 431 proof (cases "del_min r") nipkow@61784 432 case None nipkow@61784 433 show ?thesis nipkow@61784 434 proof cases nipkow@61784 435 assume "r \ B h" nipkow@61784 436 with del_minNoneN0[OF this None] lr show ?thesis by(simp) nipkow@61784 437 next nipkow@61784 438 assume "r \ B h" nipkow@61784 439 hence "r \ U h" using lr by auto nipkow@61784 440 with del_minNoneN1[OF this None] lr(3) show ?thesis by (simp) nipkow@61784 441 qed nipkow@61784 442 next nipkow@61784 443 case [simp]: (Some br') nipkow@61784 444 obtain b r' where [simp]: "br' = (b,r')" by fastforce nipkow@61784 445 show ?thesis nipkow@61784 446 proof cases nipkow@61784 447 assume "r \ B h" nipkow@61784 448 from del_min_type(1)[OF this] n2_type3[OF lr(1)] nipkow@61784 449 show ?thesis by simp nipkow@61784 450 next nipkow@61784 451 assume "r \ B h" nipkow@61784 452 hence "l \ B h" and "r \ U h" using lr by auto nipkow@61784 453 from del_min_type(2)[OF this(2)] n2_type2[OF this(1)] nipkow@61784 454 show ?thesis by simp nipkow@61784 455 qed nipkow@61784 456 qed nipkow@61784 457 } ultimately show ?case by auto nipkow@61784 458 } nipkow@61784 459 { case 2 with Suc.IH(1) show ?case by auto } nipkow@61784 460 qed auto nipkow@61784 461 nipkow@61784 462 lemma tree_type: nipkow@61784 463 "t \ Um (Suc h) \ tree t : T h" nipkow@61784 464 "t \ T (Suc h) \ tree t : T h \ T(h+1)" nipkow@61784 465 by(auto) nipkow@61784 466 nipkow@61784 467 lemma delete_type: nipkow@61784 468 "t \ T h \ delete x t \ T h \ T(h-1)" nipkow@61784 469 unfolding delete_def nipkow@61784 470 by (cases h) (simp, metis del_type tree_type Un_iff Suc_eq_plus1 diff_Suc_1) nipkow@61784 471 nipkow@61784 472 end nipkow@61784 473 nipkow@61789 474 nipkow@61784 475 subsection "Overall correctness" nipkow@61784 476 nipkow@61784 477 interpretation Set_by_Ordered nipkow@61789 478 where empty = N0 and isin = isin and insert = insert.insert nipkow@61789 479 and delete = delete.delete and inorder = inorder and inv = "\t. \h. t \ T h" nipkow@61784 480 proof (standard, goal_cases) nipkow@61784 481 case 2 thus ?case by(auto intro!: isin_set) nipkow@61784 482 next nipkow@61784 483 case 3 thus ?case by(auto intro!: insert.inorder_insert) nipkow@61784 484 next nipkow@61792 485 case 4 thus ?case by(auto intro!: delete.inorder_delete) nipkow@61784 486 next nipkow@61784 487 case 6 thus ?case using insert.insert_type by blast nipkow@61784 488 next nipkow@61784 489 case 7 thus ?case using delete.delete_type by blast nipkow@61784 490 qed auto nipkow@61784 491 nipkow@61784 492 end