--- a/src/HOL/Library/Multiset.thy Wed Nov 03 11:50:29 2010 +0100
+++ b/src/HOL/Library/Multiset.thy Wed Nov 03 12:15:47 2010 +0100
@@ -931,8 +931,48 @@
@ sort [x\<leftarrow>xs. x > xs ! (length xs div 2)]" (is "sort ?lhs = ?rhs")
using sort_key_by_quicksort [of "\<lambda>x. x", symmetric] by simp
+text {* A stable parametrized quicksort *}
+
+definition part :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b list \<Rightarrow> 'b list \<times> 'b list \<times> 'b list" where
+ "part f pivot xs = ([x \<leftarrow> xs. f x < pivot], [x \<leftarrow> xs. f x = pivot], [x \<leftarrow> xs. pivot < f x])"
+
+lemma part_code [code]:
+ "part f pivot [] = ([], [], [])"
+ "part f pivot (x # xs) = (let (lts, eqs, gts) = part f pivot xs; x' = f x in
+ if x' < pivot then (x # lts, eqs, gts)
+ else if x' > pivot then (lts, eqs, x # gts)
+ else (lts, x # eqs, gts))"
+ by (auto simp add: part_def Let_def split_def)
+
+lemma sort_key_by_quicksort_code [code]:
+ "sort_key f xs = (case xs of [] \<Rightarrow> []
+ | [x] \<Rightarrow> xs
+ | [x, y] \<Rightarrow> (if f x \<le> f y then xs else [y, x])
+ | _ \<Rightarrow> (let (lts, eqs, gts) = part f (f (xs ! (length xs div 2))) xs
+ in sort_key f lts @ eqs @ sort_key f gts))"
+proof (cases xs)
+ case Nil then show ?thesis by simp
+next
+ case (Cons _ ys) note hyps = Cons show ?thesis proof (cases ys)
+ case Nil with hyps show ?thesis by simp
+ next
+ case (Cons _ zs) note hyps = hyps Cons show ?thesis proof (cases zs)
+ case Nil with hyps show ?thesis by auto
+ next
+ case Cons
+ from sort_key_by_quicksort [of f xs]
+ have "sort_key f xs = (let (lts, eqs, gts) = part f (f (xs ! (length xs div 2))) xs
+ in sort_key f lts @ eqs @ sort_key f gts)"
+ by (simp only: split_def Let_def part_def fst_conv snd_conv)
+ with hyps Cons show ?thesis by (simp only: list.cases)
+ qed
+ qed
+qed
+
end
+hide_const (open) part
+
lemma multiset_of_remdups_le: "multiset_of (remdups xs) \<le> multiset_of xs"
by (induct xs) (auto intro: order_trans)