(* 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"
rules
qsort_Nil "qsort(le,[]) = []"
qsort_Cons "qsort(le,x#xs) = qsort(le,[y:xs . ~le(x,y)]) @ \
\ (x# qsort(le,[y:xs . le(x,y)]))"
(* computational induction.
The dependence of p on x but not xs is intentional.
*)
qsort_ind
"[| P([]); \
\ !!x xs. [| P([y:xs . ~p(x,y)]); P([y:xs . p(x,y)]) |] ==> \
\ P(x#xs) |] \
\ ==> P(xs)"
end