equal
deleted
inserted
replaced
4 Copyright 1994 TU Muenchen |
4 Copyright 1994 TU Muenchen |
5 |
5 |
6 Specification of sorting |
6 Specification of sorting |
7 *) |
7 *) |
8 |
8 |
9 Sorting = List + |
9 Sorting = Main + |
10 consts |
10 consts |
11 sorted1:: [['a,'a] => bool, 'a list] => bool |
11 sorted1:: [['a,'a] => bool, 'a list] => bool |
12 sorted :: [['a,'a] => bool, 'a list] => bool |
12 sorted :: [['a,'a] => bool, 'a list] => bool |
13 mset :: 'a list => ('a => nat) |
13 multiset :: 'a list => ('a => nat) |
14 total :: (['a,'a] => bool) => bool |
|
15 transf :: (['a,'a] => bool) => bool |
|
16 |
14 |
17 primrec |
15 primrec |
18 "sorted1 le [] = True" |
16 "sorted1 le [] = True" |
19 "sorted1 le (x#xs) = ((case xs of [] => True | y#ys => le x y) & |
17 "sorted1 le (x#xs) = ((case xs of [] => True | y#ys => le x y) & |
20 sorted1 le xs)" |
18 sorted1 le xs)" |
22 primrec |
20 primrec |
23 "sorted le [] = True" |
21 "sorted le [] = True" |
24 "sorted le (x#xs) = ((!y:set xs. le x y) & sorted le xs)" |
22 "sorted le (x#xs) = ((!y:set xs. le x y) & sorted le xs)" |
25 |
23 |
26 primrec |
24 primrec |
27 "mset [] y = 0" |
25 "multiset [] y = 0" |
28 "mset (x#xs) y = (if x=y then Suc(mset xs y) else mset xs y)" |
26 "multiset (x#xs) y = (if x=y then Suc(multiset xs y) else multiset xs y)" |
29 |
27 |
30 defs |
28 constdefs |
31 total_def "total r == (!x y. r x y | r y x)" |
29 total :: (['a,'a] => bool) => bool |
32 transf_def "transf f == (!x y z. f x y & f y z --> f x z)" |
30 "total r == (ALL x y. r x y | r y x)" |
|
31 |
|
32 transf :: (['a,'a] => bool) => bool |
|
33 "transf f == (ALL x y z. f x y & f y z --> f x z)" |
|
34 |
33 end |
35 end |