# HG changeset patch
# User paulson
# Date 1536753112 -3600
# Node ID 26be7c0d65a1d67d2d92cf05d857d5cc3c78b70c
# Parent  96b15934a17af343bd5b384b87562275e100f3a1# Parent  c73ca43087c0a109722ed4fc6d1d3801b2ce4ec1
merged

diff -r c73ca43087c0 -r 26be7c0d65a1 src/HOL/Data_Structures/Sorting.thy
--- a/src/HOL/Data_Structures/Sorting.thy	Wed Sep 12 12:51:43 2018 +0100
+++ b/src/HOL/Data_Structures/Sorting.thy	Wed Sep 12 12:51:52 2018 +0100
@@ -259,12 +259,12 @@
 by (induction xs rule: merge_adj.induct) auto
 
 fun merge_all :: "('a::linorder) list list \<Rightarrow> 'a list" where
-"merge_all [] = undefined" |
+"merge_all [] = []" |
 "merge_all [xs] = xs" |
 "merge_all xss = merge_all (merge_adj xss)"
 
 definition msort_bu :: "('a::linorder) list \<Rightarrow> 'a list" where
-"msort_bu xs = (if xs = [] then [] else merge_all (map (\<lambda>x. [x]) xs))"
+"msort_bu xs = merge_all (map (\<lambda>x. [x]) xs)"
 
 
 subsubsection "Functional Correctness"
@@ -274,7 +274,7 @@
 by(induction xss rule: merge_adj.induct) (auto simp: mset_merge)
 
 lemma mset_merge_all:
-  "xss \<noteq> [] \<Longrightarrow> mset (merge_all xss) = (\<Union># (mset (map mset xss)))"
+  "mset (merge_all xss) = (\<Union># (mset (map mset xss)))"
 by(induction xss rule: merge_all.induct) (auto simp: mset_merge mset_merge_adj)
 
 lemma mset_msort_bu: "mset (msort_bu xs) = mset xs"
@@ -285,7 +285,7 @@
 by(induction xss rule: merge_adj.induct) (auto simp: sorted_merge)
 
 lemma sorted_merge_all:
-  "\<forall>xs \<in> set xss. sorted xs \<Longrightarrow> xss \<noteq> [] \<Longrightarrow> sorted (merge_all xss)"
+  "\<forall>xs \<in> set xss. sorted xs \<Longrightarrow> sorted (merge_all xss)"
 apply(induction xss rule: merge_all.induct)
 using [[simp_depth_limit=3]] by (auto simp add: sorted_merge_adj)
 
@@ -301,12 +301,12 @@
 "c_merge_adj (xs # ys # zss) = c_merge xs ys + c_merge_adj zss"
 
 fun c_merge_all :: "('a::linorder) list list \<Rightarrow> nat" where
-"c_merge_all [] = undefined" |
+"c_merge_all [] = 0" |
 "c_merge_all [xs] = 0" |
 "c_merge_all xss = c_merge_adj xss + c_merge_all (merge_adj xss)"
 
 definition c_msort_bu :: "('a::linorder) list \<Rightarrow> nat" where
-"c_msort_bu xs = (if xs = [] then 0 else c_merge_all (map (\<lambda>x. [x]) xs))"
+"c_msort_bu xs = c_merge_all (map (\<lambda>x. [x]) xs)"
 
 lemma length_merge_adj:
   "\<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"
@@ -333,9 +333,9 @@
   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 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 ?xss). length x = 2*m" by(auto simp: length_merge)
+  have "even (length ?xss)" using "3.prems"(2) k' by auto
+  from length_merge_adj[OF this "3.prems"(1)]
+  have *: "\<forall>x \<in> set(merge_adj ?xss). length x = 2*m" .
   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"