summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Fri, 04 May 2018 18:41:11 +0200 | |

changeset 68079 | 9c2088adff8b |

parent 68078 | 48e188cb1591 |

child 68082 | b25ccd85b1fd |

tuned

--- a/src/HOL/Data_Structures/Sorting.thy Fri May 04 15:59:21 2018 +0200 +++ b/src/HOL/Data_Structures/Sorting.thy Fri May 04 18:41:11 2018 +0200 @@ -312,7 +312,7 @@ "c_merge_adj (x # y # zs) = c_merge x y + c_merge_adj zs" fun c_merge_all :: "('a::linorder) list list \<Rightarrow> real" where -"c_merge_all [] = 0" | +"c_merge_all [] = undefined" | "c_merge_all [x] = 0" | "c_merge_all xs = c_merge_adj xs + c_merge_all (merge_adj xs)" @@ -347,15 +347,13 @@ by (metis length_Cons nat.inject nat_power_eq_Suc_0_iff nat.exhaust) have "even (length xs)" using "3.prems"(2) even_Suc_Suc_iff by fastforce from "3.prems"(1) length_merge_adj[OF this] - have 2: "\<forall>x \<in> set(merge_adj ?xs). length x = 2*m" by(auto simp: length_merge) - have 3: "length ?xs2 = 2 ^ k'" using "3.prems"(2) k' by auto - have 4: "length ?xs div 2 = 2 ^ k'" - using "3.prems"(2) k' by(simp add: power_eq_if[of 2 k] split: if_splits) + have *: "\<forall>x \<in> set(merge_adj ?xs). length x = 2*m" by(auto simp: length_merge) + have **: "length ?xs2 = 2 ^ k'" using "3.prems"(2) k' by auto have "c_merge_all ?xs = c_merge_adj ?xs + c_merge_all ?xs2" by simp also have "\<dots> \<le> m * 2^k + c_merge_all ?xs2" using "3.prems"(2) c_merge_adj[OF "3.prems"(1)] by (auto simp: algebra_simps) also have "\<dots> \<le> m * 2^k + (2*m) * k' * 2^k'" - using "3.IH"[OF 2 3] by simp + using "3.IH"[OF * **] by simp also have "\<dots> = m * k * 2^k" using k' by (simp add: algebra_simps) finally show ?case .