author | clasohm |
Fri, 01 Dec 1995 12:03:13 +0100 | |
changeset 1376 | 92f83b9d17e1 |
parent 1151 | c820b3cc3df0 |
child 1476 | 608483c2122a |
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