# HG changeset patch # User nipkow # Date 1536767397 -7200 # Node ID 271026e97ca2f39aaf98d1f34a292a8720f8a234 # Parent a1e26440efb8c57c3610a3e99f445d84fb1e8fad tuned diff -r a1e26440efb8 -r 271026e97ca2 src/HOL/Data_Structures/Sorting.thy --- a/src/HOL/Data_Structures/Sorting.thy Wed Sep 12 16:12:50 2018 +0200 +++ b/src/HOL/Data_Structures/Sorting.thy Wed Sep 12 17:49:57 2018 +0200 @@ -309,7 +309,8 @@ "c_msort_bu xs = c_merge_all (map (\x. [x]) xs)" lemma length_merge_adj: - "\ even(length xss); \x \ set xss. length x = m \ \ \xs \ set (merge_adj xss). length xs = 2*m" + "\ even(length xss); \xs \ set xss. length xs = m \ + \ \xs \ set (merge_adj xss). length xs = 2*m" by(induction xss rule: merge_adj.induct) (auto simp: length_merge) lemma c_merge_adj: "\xs \ set xss. length xs = m \ c_merge_adj xss \ m * length xss"