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