tuned
authornipkow
Sun May 13 14:32:48 2018 +0200 (12 months ago)
changeset 681612053ff42214b
parent 68160 efce008331f6
child 68162 61878d2aa6c7
tuned
src/HOL/Data_Structures/Sorting.thy
     1.1 --- a/src/HOL/Data_Structures/Sorting.thy	Sun May 13 13:43:34 2018 +0200
     1.2 +++ b/src/HOL/Data_Structures/Sorting.thy	Sun May 13 14:32:48 2018 +0200
     1.3 @@ -292,23 +292,23 @@
     1.4  
     1.5  fun c_merge_adj :: "('a::linorder) list list \<Rightarrow> nat" where
     1.6  "c_merge_adj [] = 0" |
     1.7 -"c_merge_adj [x] = 0" |
     1.8 -"c_merge_adj (x # y # zs) = c_merge x y + c_merge_adj zs"
     1.9 +"c_merge_adj [xs] = 0" |
    1.10 +"c_merge_adj (xs # ys # zss) = c_merge xs ys + c_merge_adj zss"
    1.11  
    1.12  fun c_merge_all :: "('a::linorder) list list \<Rightarrow> nat" where
    1.13  "c_merge_all [] = undefined" |
    1.14 -"c_merge_all [x] = 0" |
    1.15 -"c_merge_all xs = c_merge_adj xs + c_merge_all (merge_adj xs)"
    1.16 +"c_merge_all [xs] = 0" |
    1.17 +"c_merge_all xss = c_merge_adj xss + c_merge_all (merge_adj xss)"
    1.18  
    1.19  definition c_msort_bu :: "('a::linorder) list \<Rightarrow> nat" where
    1.20  "c_msort_bu xs = (if xs = [] then 0 else c_merge_all (map (\<lambda>x. [x]) xs))"
    1.21  
    1.22  lemma length_merge_adj:
    1.23 -  "\<lbrakk> even(length xs); \<forall>x \<in> set xs. length x = m \<rbrakk> \<Longrightarrow> \<forall>x \<in> set (merge_adj xs). length x = 2*m"
    1.24 -by(induction xs rule: merge_adj.induct) (auto simp: length_merge)
    1.25 +  "\<lbrakk> even(length xss); \<forall>x \<in> set xss. length x = m \<rbrakk> \<Longrightarrow> \<forall>xs \<in> set (merge_adj xss). length xs = 2*m"
    1.26 +by(induction xss rule: merge_adj.induct) (auto simp: length_merge)
    1.27  
    1.28 -lemma c_merge_adj: "\<forall>x \<in> set xs. length x = m \<Longrightarrow> c_merge_adj xs \<le> m * length xs"
    1.29 -proof(induction xs rule: c_merge_adj.induct)
    1.30 +lemma c_merge_adj: "\<forall>xs \<in> set xss. length xs = m \<Longrightarrow> c_merge_adj xss \<le> m * length xss"
    1.31 +proof(induction xss rule: c_merge_adj.induct)
    1.32    case 1 thus ?case by simp
    1.33  next
    1.34    case 2 thus ?case by simp
    1.35 @@ -316,9 +316,9 @@
    1.36    case (3 x y) thus ?case using c_merge_ub[of x y] by (simp add: algebra_simps)
    1.37  qed
    1.38  
    1.39 -lemma c_merge_all: "\<lbrakk> \<forall>x \<in> set xs. length x = m; length xs = 2^k \<rbrakk>
    1.40 -  \<Longrightarrow> c_merge_all xs \<le> m * k * 2^k"
    1.41 -proof (induction xs arbitrary: k m rule: c_merge_all.induct)
    1.42 +lemma c_merge_all: "\<lbrakk> \<forall>xs \<in> set xss. length xs = m; length xss = 2^k \<rbrakk>
    1.43 +  \<Longrightarrow> c_merge_all xss \<le> m * k * 2^k"
    1.44 +proof (induction xss arbitrary: k m rule: c_merge_all.induct)
    1.45    case 1 thus ?case by simp
    1.46  next
    1.47    case 2 thus ?case by simp