30738
|
1 |
(* Author: Tobias Nipkow
|
24615
|
2 |
Copyright 1994 TU Muenchen
|
|
3 |
*)
|
|
4 |
|
|
5 |
header{*Quicksort*}
|
|
6 |
|
|
7 |
theory Quicksort
|
30738
|
8 |
imports Main Multiset
|
24615
|
9 |
begin
|
|
10 |
|
|
11 |
context linorder
|
|
12 |
begin
|
|
13 |
|
28041
|
14 |
fun quicksort :: "'a list \<Rightarrow> 'a list" where
|
24615
|
15 |
"quicksort [] = []" |
|
25062
|
16 |
"quicksort (x#xs) = quicksort([y\<leftarrow>xs. ~ x\<le>y]) @ [x] @ quicksort([y\<leftarrow>xs. x\<le>y])"
|
24615
|
17 |
|
|
18 |
lemma quicksort_permutes [simp]:
|
|
19 |
"multiset_of (quicksort xs) = multiset_of xs"
|
|
20 |
by (induct xs rule: quicksort.induct) (auto simp: union_ac)
|
|
21 |
|
|
22 |
lemma set_quicksort [simp]: "set (quicksort xs) = set xs"
|
|
23 |
by(simp add: set_count_greater_0)
|
|
24 |
|
|
25 |
lemma sorted_quicksort: "sorted(quicksort xs)"
|
|
26 |
apply (induct xs rule: quicksort.induct)
|
|
27 |
apply simp
|
|
28 |
apply (simp add:sorted_Cons sorted_append not_le less_imp_le)
|
|
29 |
apply (metis leD le_cases le_less_trans)
|
|
30 |
done
|
|
31 |
|
|
32 |
end
|
|
33 |
|
|
34 |
end
|