src/HOL/ex/Qsort.thy

New example of recdef and permutative rewriting

(*  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