src/HOL/Data_Structures/Sorting.thy

 
 lemma mset_merge_all:
   "xss \<noteq> [] \<Longrightarrow> 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"
+by(simp add: msort_bu_def mset_merge_all comp_def)
+
 lemma sorted_merge_adj:
   "\<forall>xs \<in> set xss. sorted xs \<Longrightarrow> \<forall>xs \<in> set (merge_adj xss). sorted xs"
 by(induction xss rule: merge_adj.induct) (auto simp: sorted_merge)
 
 lemma sorted_merge_all:

 apply(induction xss rule: merge_all.induct)
 using [[simp_depth_limit=3]] by (auto simp add: sorted_merge_adj)
 
 lemma sorted_msort_bu: "sorted (msort_bu xs)"
 by(simp add: msort_bu_def sorted_merge_all)
-
-lemma mset_msort_bu: "mset (msort_bu xs) = mset xs"
-by(simp add: msort_bu_def mset_merge_all comp_def)
 
 
 subsubsection "Time Complexity"
 
 fun c_merge_adj :: "('a::linorder) list list \<Rightarrow> nat" where