author | krauss |
Thu, 28 Aug 2008 15:33:33 +0200 | |
changeset 28041 | f496e9f343b7 |
parent 27682 | 25aceefd4786 |
child 30738 | 0842e906300c |
permissions | -rw-r--r-- |
nipkow@24615 | 1 |
(* ID: $Id$ |
nipkow@24615 | 2 |
Author: Tobias Nipkow |
nipkow@24615 | 3 |
Copyright 1994 TU Muenchen |
nipkow@24615 | 4 |
*) |
nipkow@24615 | 5 |
|
nipkow@24615 | 6 |
header{*Quicksort*} |
nipkow@24615 | 7 |
|
nipkow@24615 | 8 |
theory Quicksort |
haftmann@27368 | 9 |
imports Plain Multiset |
nipkow@24615 | 10 |
begin |
nipkow@24615 | 11 |
|
nipkow@24615 | 12 |
context linorder |
nipkow@24615 | 13 |
begin |
nipkow@24615 | 14 |
|
krauss@28041 | 15 |
fun quicksort :: "'a list \<Rightarrow> 'a list" where |
nipkow@24615 | 16 |
"quicksort [] = []" | |
haftmann@25062 | 17 |
"quicksort (x#xs) = quicksort([y\<leftarrow>xs. ~ x\<le>y]) @ [x] @ quicksort([y\<leftarrow>xs. x\<le>y])" |
nipkow@24615 | 18 |
|
nipkow@24615 | 19 |
lemma quicksort_permutes [simp]: |
nipkow@24615 | 20 |
"multiset_of (quicksort xs) = multiset_of xs" |
nipkow@24615 | 21 |
by (induct xs rule: quicksort.induct) (auto simp: union_ac) |
nipkow@24615 | 22 |
|
nipkow@24615 | 23 |
lemma set_quicksort [simp]: "set (quicksort xs) = set xs" |
nipkow@24615 | 24 |
by(simp add: set_count_greater_0) |
nipkow@24615 | 25 |
|
nipkow@24615 | 26 |
lemma sorted_quicksort: "sorted(quicksort xs)" |
nipkow@24615 | 27 |
apply (induct xs rule: quicksort.induct) |
nipkow@24615 | 28 |
apply simp |
nipkow@24615 | 29 |
apply (simp add:sorted_Cons sorted_append not_le less_imp_le) |
nipkow@24615 | 30 |
apply (metis leD le_cases le_less_trans) |
nipkow@24615 | 31 |
done |
nipkow@24615 | 32 |
|
nipkow@24615 | 33 |
end |
nipkow@24615 | 34 |
|
nipkow@24615 | 35 |
end |