author | nipkow |

Sun May 13 14:40:40 2018 +0200 (12 months ago) | |

changeset 68162 | 61878d2aa6c7 |

parent 68161 | 2053ff42214b |

child 68174 | 7c4793e39dd5 |

tuned

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