36
|
1 |
Qsort = List +
|
|
2 |
consts
|
|
3 |
sorted :: "[['a,'a] => bool, 'a list] => bool"
|
|
4 |
mset :: "'a list => ('a => nat)"
|
|
5 |
qsort :: "[['a,'a] => bool, 'a list] => 'a list"
|
|
6 |
|
|
7 |
rules
|
|
8 |
|
|
9 |
sorted_Nil "sorted(le,[])"
|
|
10 |
sorted_Cons "sorted(le,Cons(x,xs)) = ((Alls y:xs. le(x,y)) & sorted(le,xs))"
|
|
11 |
|
|
12 |
mset_Nil "mset([],y) = 0"
|
|
13 |
mset_Cons "mset(Cons(x,xs),y) = if(x=y, Suc(mset(xs,y)), mset(xs,y))"
|
|
14 |
|
|
15 |
qsort_Nil "qsort(le,[]) = []"
|
|
16 |
qsort_Cons "qsort(le,Cons(x,xs)) = qsort(le,[y:xs . ~le(x,y)]) @ \
|
|
17 |
\ Cons(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(Cons(x,xs)) |] \
|
|
26 |
\ ==> P(xs)"
|
|
27 |
end
|