1 (* Title: HOL/ex/Qsort.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 1994 TU Muenchen |
|
5 *) |
|
6 |
|
7 header{*Quicksort*} |
|
8 |
|
9 theory Qsort |
|
10 imports Sorting |
|
11 begin |
|
12 |
|
13 subsection{*Version 1: higher-order*} |
|
14 |
|
15 consts qsort :: "('a \<Rightarrow> 'a => bool) * 'a list \<Rightarrow> 'a list" |
|
16 |
|
17 recdef qsort "measure (size o snd)" |
|
18 "qsort(le, []) = []" |
|
19 "qsort(le, x#xs) = qsort(le, [y\<leftarrow>xs . ~ le x y]) @ [x] @ |
|
20 qsort(le, [y\<leftarrow>xs . le x y])" |
|
21 (hints recdef_simp: length_filter_le[THEN le_less_trans]) |
|
22 |
|
23 lemma qsort_permutes [simp]: |
|
24 "multiset_of (qsort(le,xs)) = multiset_of xs" |
|
25 by (induct le xs rule: qsort.induct) (auto simp: union_ac) |
|
26 |
|
27 lemma set_qsort [simp]: "set (qsort(le,xs)) = set xs"; |
|
28 by(simp add: set_count_greater_0) |
|
29 |
|
30 lemma sorted_qsort: |
|
31 "total(le) ==> transf(le) ==> sorted le (qsort(le,xs))" |
|
32 apply (induct le xs rule: qsort.induct) |
|
33 apply simp |
|
34 apply simp |
|
35 apply(unfold Sorting.total_def Sorting.transf_def) |
|
36 apply blast |
|
37 done |
|
38 |
|
39 |
|
40 subsection{*Version 2:type classes*} |
|
41 |
|
42 consts quickSort :: "('a::linorder) list => 'a list" |
|
43 |
|
44 recdef quickSort "measure size" |
|
45 "quickSort [] = []" |
|
46 "quickSort (x#l) = quickSort [y\<leftarrow>l. ~ x\<le>y] @ [x] @ quickSort [y\<leftarrow>l. x\<le>y]" |
|
47 (hints recdef_simp: length_filter_le[THEN le_less_trans]) |
|
48 |
|
49 lemma quickSort_permutes[simp]: |
|
50 "multiset_of (quickSort xs) = multiset_of xs" |
|
51 by (induct xs rule: quickSort.induct) (auto simp: union_ac) |
|
52 |
|
53 lemma set_quickSort[simp]: "set (quickSort xs) = set xs" |
|
54 by(simp add: set_count_greater_0) |
|
55 |
|
56 theorem sorted_quickSort: "sorted (op \<le>) (quickSort xs)" |
|
57 by (induct xs rule: quickSort.induct, auto) |
|
58 |
|
59 end |
|