tuned
authornipkow
Sun May 13 14:40:40 2018 +0200 (12 months ago)
changeset 6816261878d2aa6c7
parent 68161 2053ff42214b
child 68174 7c4793e39dd5
tuned
src/HOL/Data_Structures/Sorting.thy
     1.1 --- a/src/HOL/Data_Structures/Sorting.thy	Sun May 13 14:32:48 2018 +0200
     1.2 +++ b/src/HOL/Data_Structures/Sorting.thy	Sun May 13 14:40:40 2018 +0200
     1.3 @@ -323,17 +323,17 @@
     1.4  next
     1.5    case 2 thus ?case by simp
     1.6  next
     1.7 -  case (3 x y xs)
     1.8 -  let ?xs = "x # y # xs"
     1.9 -  let ?xs2 = "merge_adj ?xs"
    1.10 +  case (3 xs ys xss)
    1.11 +  let ?xss = "xs # ys # xss"
    1.12 +  let ?xss2 = "merge_adj ?xss"
    1.13    obtain k' where k': "k = Suc k'" using "3.prems"(2)
    1.14      by (metis length_Cons nat.inject nat_power_eq_Suc_0_iff nat.exhaust)
    1.15 -  have "even (length xs)" using "3.prems"(2) even_Suc_Suc_iff by fastforce
    1.16 +  have "even (length xss)" using "3.prems"(2) even_Suc_Suc_iff by fastforce
    1.17    from "3.prems"(1) length_merge_adj[OF this]
    1.18 -  have *: "\<forall>x \<in> set(merge_adj ?xs). length x = 2*m" by(auto simp: length_merge)
    1.19 -  have **: "length ?xs2 = 2 ^ k'" using "3.prems"(2) k' by auto
    1.20 -  have "c_merge_all ?xs = c_merge_adj ?xs + c_merge_all ?xs2" by simp
    1.21 -  also have "\<dots> \<le> m * 2^k + c_merge_all ?xs2"
    1.22 +  have *: "\<forall>x \<in> set(merge_adj ?xss). length x = 2*m" by(auto simp: length_merge)
    1.23 +  have **: "length ?xss2 = 2 ^ k'" using "3.prems"(2) k' by auto
    1.24 +  have "c_merge_all ?xss = c_merge_adj ?xss + c_merge_all ?xss2" by simp
    1.25 +  also have "\<dots> \<le> m * 2^k + c_merge_all ?xss2"
    1.26      using "3.prems"(2) c_merge_adj[OF "3.prems"(1)] by (auto simp: algebra_simps)
    1.27    also have "\<dots> \<le> m * 2^k + (2*m) * k' * 2^k'"
    1.28      using "3.IH"[OF * **] by simp