# HG changeset patch
# User haftmann
# Date 1288782947 -3600
# Node ID 429bf4388b2f4ef62fd74ad2b6f7fa37ecd745d9
# Parent  58af2b8327b77850b7df9a5ea57ed75836335257
added code lemmas for stable parametrized quicksort

diff -r 58af2b8327b7 -r 429bf4388b2f src/HOL/Library/Multiset.thy
--- 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)