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