author  paulson 
Mon, 20 Mar 2000 10:26:34 +0100  
changeset 8524  f990040535c9 
parent 8414  5983668cac15 
child 8590  89675b444abe 
permissions  rwrr 
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)" 
8524
f990040535c9
a possibly (?) more perspicous simprule in the "simpset" part
paulson
parents:
8414
diff
changeset

13 
simpset "simpset() addsimps [length_filter RS le_less_trans]" 
8414  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 