src/HOL/ex/Qsort.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 8590 89675b444abe
child 13159 2af7b94892ce
permissions -rw-r--r--
hide many names from Datatype_Universe.

(*  Title:      HOL/ex/Qsort.thy
    ID:         $Id$
    Author:     Tobias Nipkow
    Copyright   1994 TU Muenchen

Quicksort
*)

Qsort = Sorting +

(*Version one: higher-order*)
consts qsort :: "((['a,'a] => bool) * 'a list) => 'a list"

recdef qsort "measure (size o snd)"
    simpset "simpset() addsimps [length_filter RS le_less_trans]"
    
    "qsort(le, [])   = []"
    
    "qsort(le, x#xs) = qsort(le, [y:xs . ~ le x y])  
                       @ (x # qsort(le, [y:xs . le x y]))"


(*Version two: type classes*)
consts quickSort :: "('a::linorder) list => 'a list"

recdef quickSort "measure size"
    simpset "simpset() addsimps [length_filter RS le_less_trans]"
    
    "quickSort []   = []"
    
    "quickSort (x#l) = quickSort [y:l. ~ x<=y] @ (x # quickSort [y:l. x<=y])"

end