src/HOL/ex/Qsort.thy
author paulson
Fri, 10 Mar 2000 17:52:48 +0100
changeset 8414 5983668cac15
parent 1476 608483c2122a
child 8524 f990040535c9
permissions -rw-r--r--
now uses recdef instead of "rules"

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

Quicksort
*)

Qsort = Sorting +
consts qsort :: "((['a,'a] => bool) * 'a list) => 'a list"

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

end