310 "c_merge_adj [] = 0" | |
310 "c_merge_adj [] = 0" | |
311 "c_merge_adj [x] = 0" | |
311 "c_merge_adj [x] = 0" | |
312 "c_merge_adj (x # y # zs) = c_merge x y + c_merge_adj zs" |
312 "c_merge_adj (x # y # zs) = c_merge x y + c_merge_adj zs" |
313 |
313 |
314 fun c_merge_all :: "('a::linorder) list list \<Rightarrow> real" where |
314 fun c_merge_all :: "('a::linorder) list list \<Rightarrow> real" where |
315 "c_merge_all [] = 0" | |
315 "c_merge_all [] = undefined" | |
316 "c_merge_all [x] = 0" | |
316 "c_merge_all [x] = 0" | |
317 "c_merge_all xs = c_merge_adj xs + c_merge_all (merge_adj xs)" |
317 "c_merge_all xs = c_merge_adj xs + c_merge_all (merge_adj xs)" |
318 |
318 |
319 definition c_msort_bu :: "('a::linorder) list \<Rightarrow> real" where |
319 definition c_msort_bu :: "('a::linorder) list \<Rightarrow> real" where |
320 "c_msort_bu xs = (if xs = [] then 0 else c_merge_all (map (\<lambda>x. [x]) xs))" |
320 "c_msort_bu xs = (if xs = [] then 0 else c_merge_all (map (\<lambda>x. [x]) xs))" |
345 let ?xs2 = "merge_adj ?xs" |
345 let ?xs2 = "merge_adj ?xs" |
346 obtain k' where k': "k = Suc k'" using "3.prems"(2) |
346 obtain k' where k': "k = Suc k'" using "3.prems"(2) |
347 by (metis length_Cons nat.inject nat_power_eq_Suc_0_iff nat.exhaust) |
347 by (metis length_Cons nat.inject nat_power_eq_Suc_0_iff nat.exhaust) |
348 have "even (length xs)" using "3.prems"(2) even_Suc_Suc_iff by fastforce |
348 have "even (length xs)" using "3.prems"(2) even_Suc_Suc_iff by fastforce |
349 from "3.prems"(1) length_merge_adj[OF this] |
349 from "3.prems"(1) length_merge_adj[OF this] |
350 have 2: "\<forall>x \<in> set(merge_adj ?xs). length x = 2*m" by(auto simp: length_merge) |
350 have *: "\<forall>x \<in> set(merge_adj ?xs). length x = 2*m" by(auto simp: length_merge) |
351 have 3: "length ?xs2 = 2 ^ k'" using "3.prems"(2) k' by auto |
351 have **: "length ?xs2 = 2 ^ k'" using "3.prems"(2) k' by auto |
352 have 4: "length ?xs div 2 = 2 ^ k'" |
|
353 using "3.prems"(2) k' by(simp add: power_eq_if[of 2 k] split: if_splits) |
|
354 have "c_merge_all ?xs = c_merge_adj ?xs + c_merge_all ?xs2" by simp |
352 have "c_merge_all ?xs = c_merge_adj ?xs + c_merge_all ?xs2" by simp |
355 also have "\<dots> \<le> m * 2^k + c_merge_all ?xs2" |
353 also have "\<dots> \<le> m * 2^k + c_merge_all ?xs2" |
356 using "3.prems"(2) c_merge_adj[OF "3.prems"(1)] by (auto simp: algebra_simps) |
354 using "3.prems"(2) c_merge_adj[OF "3.prems"(1)] by (auto simp: algebra_simps) |
357 also have "\<dots> \<le> m * 2^k + (2*m) * k' * 2^k'" |
355 also have "\<dots> \<le> m * 2^k + (2*m) * k' * 2^k'" |
358 using "3.IH"[OF 2 3] by simp |
356 using "3.IH"[OF * **] by simp |
359 also have "\<dots> = m * k * 2^k" |
357 also have "\<dots> = m * k * 2^k" |
360 using k' by (simp add: algebra_simps) |
358 using k' by (simp add: algebra_simps) |
361 finally show ?case . |
359 finally show ?case . |
362 qed |
360 qed |
363 |
361 |