# HG changeset patch
# User nipkow
# Date 1526215240 -7200
# Node ID 61878d2aa6c7a8b67d47ec10b236f6b803a3d199
# Parent  2053ff42214bb3867a4975159b531c17a6a49018
tuned

diff -r 2053ff42214b -r 61878d2aa6c7 src/HOL/Data_Structures/Sorting.thy
--- a/src/HOL/Data_Structures/Sorting.thy	Sun May 13 14:32:48 2018 +0200
+++ b/src/HOL/Data_Structures/Sorting.thy	Sun May 13 14:40:40 2018 +0200
@@ -323,17 +323,17 @@
 next
   case 2 thus ?case by simp
 next
-  case (3 x y xs)
-  let ?xs = "x # y # xs"
-  let ?xs2 = "merge_adj ?xs"
+  case (3 xs ys xss)
+  let ?xss = "xs # ys # xss"
+  let ?xss2 = "merge_adj ?xss"
   obtain k' where k': "k = Suc k'" using "3.prems"(2)
     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
+  have "even (length xss)" using "3.prems"(2) even_Suc_Suc_iff by fastforce
   from "3.prems"(1) length_merge_adj[OF this]
-  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"
+  have *: "\<forall>x \<in> set(merge_adj ?xss). length x = 2*m" by(auto simp: length_merge)
+  have **: "length ?xss2 = 2 ^ k'" using "3.prems"(2) k' by auto
+  have "c_merge_all ?xss = c_merge_adj ?xss + c_merge_all ?xss2" by simp
+  also have "\<dots> \<le> m * 2^k + c_merge_all ?xss2"
     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 * **] by simp