author nipkow Tue, 11 Sep 2018 18:12:11 +0200 changeset 68971 938f4058c07c parent 68970 b0dfe57dfa09 child 68972 96b15934a17a
simplified defns
```--- a/src/HOL/Data_Structures/Sorting.thy	Tue Sep 11 17:53:08 2018 +0200
+++ b/src/HOL/Data_Structures/Sorting.thy	Tue Sep 11 18:12:11 2018 +0200
@@ -264,7 +264,7 @@
"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)

@@ -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" |