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