969
|
1 |
(* Title: HOL/ex/qsort.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow
|
|
4 |
Copyright 1994 TU Muenchen
|
|
5 |
|
|
6 |
Quicksort
|
|
7 |
*)
|
|
8 |
|
|
9 |
Qsort = Sorting +
|
|
10 |
consts
|
1376
|
11 |
qsort :: [['a,'a] => bool, 'a list] => 'a list
|
969
|
12 |
|
|
13 |
rules
|
|
14 |
|
|
15 |
qsort_Nil "qsort le [] = []"
|
1151
|
16 |
qsort_Cons "qsort le (x#xs) = qsort le [y:xs . ~le x y] @
|
|
17 |
(x# qsort le [y:xs . le x y])"
|
969
|
18 |
|
|
19 |
(* computational induction.
|
|
20 |
The dependence of p on x but not xs is intentional.
|
|
21 |
*)
|
|
22 |
qsort_ind
|
1151
|
23 |
"[| P([]);
|
|
24 |
!!x xs. [| P([y:xs . ~p x y]); P([y:xs . p x y]) |] ==>
|
|
25 |
P(x#xs) |]
|
|
26 |
==> P(xs)"
|
969
|
27 |
end
|