author | clasohm |
Wed, 22 Mar 1995 12:42:34 +0100 | |
changeset 969 | b051e2fc2e34 |
child 1151 | c820b3cc3df0 |
permissions | -rw-r--r-- |
(* 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