equal
deleted
inserted
replaced
|
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 |
|
11 qsort :: "[['a,'a] => bool, 'a list] => 'a list" |
|
12 |
|
13 rules |
|
14 |
|
15 qsort_Nil "qsort le [] = []" |
|
16 qsort_Cons "qsort le (x#xs) = qsort le [y:xs . ~le x y] @ \ |
|
17 \ (x# qsort le [y:xs . le x y])" |
|
18 |
|
19 (* computational induction. |
|
20 The dependence of p on x but not xs is intentional. |
|
21 *) |
|
22 qsort_ind |
|
23 "[| P([]); \ |
|
24 \ !!x xs. [| P([y:xs . ~p x y]); P([y:xs . p x y]) |] ==> \ |
|
25 \ P(x#xs) |] \ |
|
26 \ ==> P(xs)" |
|
27 end |