author | paulson |
Thu, 08 Jul 1999 13:48:11 +0200 | |
changeset 6921 | 78a2ce8fb8df |
parent 1476 | 608483c2122a |
child 8414 | 5983668cac15 |
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