merged

--- a/src/HOL/Data_Structures/Sorting.thy	Thu Sep 13 21:18:43 2018 +0200
+++ b/src/HOL/Data_Structures/Sorting.thy	Fri Sep 14 11:34:21 2018 +0200
@@ -351,4 +351,24 @@
 corollary c_msort_bu: "length xs = 2 ^ k \<Longrightarrow> c_msort_bu xs \<le> k * 2 ^ k"
 using c_merge_all[of "map (\<lambda>x. [x]) xs" 1] by (simp add: c_msort_bu_def)
 
+
+subsection "Quicksort"
+
+fun quicksort :: "('a::linorder) list \<Rightarrow> 'a list" where
+"quicksort []     = []" |
+"quicksort (x#xs) = quicksort (filter (\<lambda>y. y < x) xs) @ [x] @ quicksort (filter (\<lambda>y. x \<le> y) xs)"
+
+lemma mset_quicksort: "mset (quicksort xs) = mset xs"
+apply (induction xs rule: quicksort.induct)
+apply (auto simp: not_le)
+done
+
+lemma set_quicksort: "set (quicksort xs) = set xs"
+by(rule mset_eq_setD[OF mset_quicksort])
+
+lemma sorted_quicksort: "sorted (quicksort xs)"
+apply (induction xs rule: quicksort.induct)
+apply (auto simp add: sorted_append set_quicksort)
+done
+
 end

--- a/src/HOL/Library/Multiset.thy	Thu Sep 13 21:18:43 2018 +0200
+++ b/src/HOL/Library/Multiset.thy	Fri Sep 14 11:34:21 2018 +0200
@@ -1520,8 +1520,12 @@
 lemma multi_drop_mem_not_eq: "c \<in># B \<Longrightarrow> B - {#c#} \<noteq> B"
 by (cases "B = {#}") (auto dest: multi_member_split)
 
+lemma union_filter_mset_complement[simp]:
+  "\<forall>x. P x = (\<not> Q x) \<Longrightarrow> filter_mset P M + filter_mset Q M = M"
+by (subst multiset_eq_iff) auto
+
 lemma multiset_partition: "M = {#x \<in># M. P x#} + {#x \<in># M. \<not> P x#}"
-  by (subst multiset_eq_iff) auto
+by simp
 
 lemma mset_subset_size: "A \<subset># B \<Longrightarrow> size A < size B"
 proof (induct A arbitrary: B)
@@ -1887,9 +1891,6 @@
 apply simp
 done
 
-lemma union_mset_compl[simp]: "\<forall>x. P x = (\<not> Q x) \<Longrightarrow> filter_mset P M + filter_mset Q M = M"
-by (induction M) simp_all
-
 lemma nth_mem_mset: "i < length ls \<Longrightarrow> (ls ! i) \<in># mset ls"
 proof (induct ls arbitrary: i)
   case Nil
@@ -2924,7 +2925,7 @@
   next
     case [simp]: False
     have K: "K = {#x \<in># K. (x, a) \<in> r#} + {#x \<in># K. (x, a) \<notin> r#}"
-      by (rule multiset_partition)
+      by simp
     have "(I + K, (I + {# x \<in># K. (x, a) \<in> r #}) + J') \<in> mult r"
       using IH[of J' "{# x \<in># K. (x, a) \<notin> r#}" "I + {# x \<in># K. (x, a) \<in> r#}"]
         J Suc.prems K size_J by (auto simp: ac_simps)