src/HOL/Library/Multiset.thy
changeset 40347 429bf4388b2f
parent 40346 58af2b8327b7
child 40606 af1a0b0c6202
     1.1 --- a/src/HOL/Library/Multiset.thy	Wed Nov 03 11:50:29 2010 +0100
     1.2 +++ b/src/HOL/Library/Multiset.thy	Wed Nov 03 12:15:47 2010 +0100
     1.3 @@ -931,8 +931,48 @@
     1.4      @ sort [x\<leftarrow>xs. x > xs ! (length xs div 2)]" (is "sort ?lhs = ?rhs")
     1.5    using sort_key_by_quicksort [of "\<lambda>x. x", symmetric] by simp
     1.6  
     1.7 +text {* A stable parametrized quicksort *}
     1.8 +
     1.9 +definition part :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b list \<Rightarrow> 'b list \<times> 'b list \<times> 'b list" where
    1.10 +  "part f pivot xs = ([x \<leftarrow> xs. f x < pivot], [x \<leftarrow> xs. f x = pivot], [x \<leftarrow> xs. pivot < f x])"
    1.11 +
    1.12 +lemma part_code [code]:
    1.13 +  "part f pivot [] = ([], [], [])"
    1.14 +  "part f pivot (x # xs) = (let (lts, eqs, gts) = part f pivot xs; x' = f x in
    1.15 +     if x' < pivot then (x # lts, eqs, gts)
    1.16 +     else if x' > pivot then (lts, eqs, x # gts)
    1.17 +     else (lts, x # eqs, gts))"
    1.18 +  by (auto simp add: part_def Let_def split_def)
    1.19 +
    1.20 +lemma sort_key_by_quicksort_code [code]:
    1.21 +  "sort_key f xs = (case xs of [] \<Rightarrow> []
    1.22 +    | [x] \<Rightarrow> xs
    1.23 +    | [x, y] \<Rightarrow> (if f x \<le> f y then xs else [y, x])
    1.24 +    | _ \<Rightarrow> (let (lts, eqs, gts) = part f (f (xs ! (length xs div 2))) xs
    1.25 +       in sort_key f lts @ eqs @ sort_key f gts))"
    1.26 +proof (cases xs)
    1.27 +  case Nil then show ?thesis by simp
    1.28 +next
    1.29 +  case (Cons _ ys) note hyps = Cons show ?thesis proof (cases ys)
    1.30 +    case Nil with hyps show ?thesis by simp
    1.31 +  next
    1.32 +    case (Cons _ zs) note hyps = hyps Cons show ?thesis proof (cases zs)
    1.33 +      case Nil with hyps show ?thesis by auto
    1.34 +    next
    1.35 +      case Cons 
    1.36 +      from sort_key_by_quicksort [of f xs]
    1.37 +      have "sort_key f xs = (let (lts, eqs, gts) = part f (f (xs ! (length xs div 2))) xs
    1.38 +        in sort_key f lts @ eqs @ sort_key f gts)"
    1.39 +      by (simp only: split_def Let_def part_def fst_conv snd_conv)
    1.40 +      with hyps Cons show ?thesis by (simp only: list.cases)
    1.41 +    qed
    1.42 +  qed
    1.43 +qed
    1.44 +
    1.45  end
    1.46  
    1.47 +hide_const (open) part
    1.48 +
    1.49  lemma multiset_of_remdups_le: "multiset_of (remdups xs) \<le> multiset_of xs"
    1.50    by (induct xs) (auto intro: order_trans)
    1.51