author | nipkow |
Fri, 24 Nov 2000 16:49:27 +0100 | |
changeset 10519 | ade64af4c57c |
parent 8590 | 89675b444abe |
child 13159 | 2af7b94892ce |
permissions | -rw-r--r-- |
8414 | 1 |
(* Title: HOL/ex/Qsort.thy |
969 | 2 |
ID: $Id$ |
1476 | 3 |
Author: Tobias Nipkow |
969 | 4 |
Copyright 1994 TU Muenchen |
5 |
||
6 |
Quicksort |
|
7 |
*) |
|
8 |
||
9 |
Qsort = Sorting + |
|
8590 | 10 |
|
11 |
(*Version one: higher-order*) |
|
8414 | 12 |
consts qsort :: "((['a,'a] => bool) * 'a list) => 'a list" |
969 | 13 |
|
8414 | 14 |
recdef qsort "measure (size o snd)" |
8524
f990040535c9
a possibly (?) more perspicous simprule in the "simpset" part
paulson
parents:
8414
diff
changeset
|
15 |
simpset "simpset() addsimps [length_filter RS le_less_trans]" |
8414 | 16 |
|
17 |
"qsort(le, []) = []" |
|
18 |
||
19 |
"qsort(le, x#xs) = qsort(le, [y:xs . ~ le x y]) |
|
20 |
@ (x # qsort(le, [y:xs . le x y]))" |
|
21 |
||
8590 | 22 |
|
23 |
(*Version two: type classes*) |
|
24 |
consts quickSort :: "('a::linorder) list => 'a list" |
|
25 |
||
26 |
recdef quickSort "measure size" |
|
27 |
simpset "simpset() addsimps [length_filter RS le_less_trans]" |
|
28 |
||
29 |
"quickSort [] = []" |
|
30 |
||
31 |
"quickSort (x#l) = quickSort [y:l. ~ x<=y] @ (x # quickSort [y:l. x<=y])" |
|
32 |
||
969 | 33 |
end |