author | paulson |
Fri, 10 Mar 2000 17:52:48 +0100 | |
changeset 8414 | 5983668cac15 |
parent 1476 | 608483c2122a |
child 8524 | f990040535c9 |
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 + |
|
8414 | 10 |
consts qsort :: "((['a,'a] => bool) * 'a list) => 'a list" |
969 | 11 |
|
8414 | 12 |
recdef qsort "measure (size o snd)" |
13 |
simpset "simpset() addsimps [less_Suc_eq_le]" |
|
14 |
||
15 |
"qsort(le, []) = []" |
|
16 |
||
17 |
"qsort(le, x#xs) = qsort(le, [y:xs . ~ le x y]) |
|
18 |
@ (x # qsort(le, [y:xs . le x y]))" |
|
19 |
||
969 | 20 |
end |