321 proof (induction xss arbitrary: k m rule: c_merge_all.induct) |
321 proof (induction xss arbitrary: k m rule: c_merge_all.induct) |
322 case 1 thus ?case by simp |
322 case 1 thus ?case by simp |
323 next |
323 next |
324 case 2 thus ?case by simp |
324 case 2 thus ?case by simp |
325 next |
325 next |
326 case (3 x y xs) |
326 case (3 xs ys xss) |
327 let ?xs = "x # y # xs" |
327 let ?xss = "xs # ys # xss" |
328 let ?xs2 = "merge_adj ?xs" |
328 let ?xss2 = "merge_adj ?xss" |
329 obtain k' where k': "k = Suc k'" using "3.prems"(2) |
329 obtain k' where k': "k = Suc k'" using "3.prems"(2) |
330 by (metis length_Cons nat.inject nat_power_eq_Suc_0_iff nat.exhaust) |
330 by (metis length_Cons nat.inject nat_power_eq_Suc_0_iff nat.exhaust) |
331 have "even (length xs)" using "3.prems"(2) even_Suc_Suc_iff by fastforce |
331 have "even (length xss)" using "3.prems"(2) even_Suc_Suc_iff by fastforce |
332 from "3.prems"(1) length_merge_adj[OF this] |
332 from "3.prems"(1) length_merge_adj[OF this] |
333 have *: "\<forall>x \<in> set(merge_adj ?xs). length x = 2*m" by(auto simp: length_merge) |
333 have *: "\<forall>x \<in> set(merge_adj ?xss). length x = 2*m" by(auto simp: length_merge) |
334 have **: "length ?xs2 = 2 ^ k'" using "3.prems"(2) k' by auto |
334 have **: "length ?xss2 = 2 ^ k'" using "3.prems"(2) k' by auto |
335 have "c_merge_all ?xs = c_merge_adj ?xs + c_merge_all ?xs2" by simp |
335 have "c_merge_all ?xss = c_merge_adj ?xss + c_merge_all ?xss2" by simp |
336 also have "\<dots> \<le> m * 2^k + c_merge_all ?xs2" |
336 also have "\<dots> \<le> m * 2^k + c_merge_all ?xss2" |
337 using "3.prems"(2) c_merge_adj[OF "3.prems"(1)] by (auto simp: algebra_simps) |
337 using "3.prems"(2) c_merge_adj[OF "3.prems"(1)] by (auto simp: algebra_simps) |
338 also have "\<dots> \<le> m * 2^k + (2*m) * k' * 2^k'" |
338 also have "\<dots> \<le> m * 2^k + (2*m) * k' * 2^k'" |
339 using "3.IH"[OF * **] by simp |
339 using "3.IH"[OF * **] by simp |
340 also have "\<dots> = m * k * 2^k" |
340 also have "\<dots> = m * k * 2^k" |
341 using k' by (simp add: algebra_simps) |
341 using k' by (simp add: algebra_simps) |