290 |
290 |
291 subsubsection "Time Complexity" |
291 subsubsection "Time Complexity" |
292 |
292 |
293 fun c_merge_adj :: "('a::linorder) list list \<Rightarrow> nat" where |
293 fun c_merge_adj :: "('a::linorder) list list \<Rightarrow> nat" where |
294 "c_merge_adj [] = 0" | |
294 "c_merge_adj [] = 0" | |
295 "c_merge_adj [x] = 0" | |
295 "c_merge_adj [xs] = 0" | |
296 "c_merge_adj (x # y # zs) = c_merge x y + c_merge_adj zs" |
296 "c_merge_adj (xs # ys # zss) = c_merge xs ys + c_merge_adj zss" |
297 |
297 |
298 fun c_merge_all :: "('a::linorder) list list \<Rightarrow> nat" where |
298 fun c_merge_all :: "('a::linorder) list list \<Rightarrow> nat" where |
299 "c_merge_all [] = undefined" | |
299 "c_merge_all [] = undefined" | |
300 "c_merge_all [x] = 0" | |
300 "c_merge_all [xs] = 0" | |
301 "c_merge_all xs = c_merge_adj xs + c_merge_all (merge_adj xs)" |
301 "c_merge_all xss = c_merge_adj xss + c_merge_all (merge_adj xss)" |
302 |
302 |
303 definition c_msort_bu :: "('a::linorder) list \<Rightarrow> nat" where |
303 definition c_msort_bu :: "('a::linorder) list \<Rightarrow> nat" where |
304 "c_msort_bu xs = (if xs = [] then 0 else c_merge_all (map (\<lambda>x. [x]) xs))" |
304 "c_msort_bu xs = (if xs = [] then 0 else c_merge_all (map (\<lambda>x. [x]) xs))" |
305 |
305 |
306 lemma length_merge_adj: |
306 lemma length_merge_adj: |
307 "\<lbrakk> even(length xs); \<forall>x \<in> set xs. length x = m \<rbrakk> \<Longrightarrow> \<forall>x \<in> set (merge_adj xs). length x = 2*m" |
307 "\<lbrakk> even(length xss); \<forall>x \<in> set xss. length x = m \<rbrakk> \<Longrightarrow> \<forall>xs \<in> set (merge_adj xss). length xs = 2*m" |
308 by(induction xs rule: merge_adj.induct) (auto simp: length_merge) |
308 by(induction xss rule: merge_adj.induct) (auto simp: length_merge) |
309 |
309 |
310 lemma c_merge_adj: "\<forall>x \<in> set xs. length x = m \<Longrightarrow> c_merge_adj xs \<le> m * length xs" |
310 lemma c_merge_adj: "\<forall>xs \<in> set xss. length xs = m \<Longrightarrow> c_merge_adj xss \<le> m * length xss" |
311 proof(induction xs rule: c_merge_adj.induct) |
311 proof(induction xss rule: c_merge_adj.induct) |
312 case 1 thus ?case by simp |
312 case 1 thus ?case by simp |
313 next |
313 next |
314 case 2 thus ?case by simp |
314 case 2 thus ?case by simp |
315 next |
315 next |
316 case (3 x y) thus ?case using c_merge_ub[of x y] by (simp add: algebra_simps) |
316 case (3 x y) thus ?case using c_merge_ub[of x y] by (simp add: algebra_simps) |
317 qed |
317 qed |
318 |
318 |
319 lemma c_merge_all: "\<lbrakk> \<forall>x \<in> set xs. length x = m; length xs = 2^k \<rbrakk> |
319 lemma c_merge_all: "\<lbrakk> \<forall>xs \<in> set xss. length xs = m; length xss = 2^k \<rbrakk> |
320 \<Longrightarrow> c_merge_all xs \<le> m * k * 2^k" |
320 \<Longrightarrow> c_merge_all xss \<le> m * k * 2^k" |
321 proof (induction xs 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 x y xs) |