author | paulson |
Mon, 14 Aug 1995 13:42:27 +0200 | |
changeset 1228 | 7d6b0241afab |
parent 1151 | c820b3cc3df0 |
child 1376 | 92f83b9d17e1 |
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