1476
|
1 |
(* Title: HOL/ex/sorting.thy
|
969
|
2 |
ID: $Id$
|
1476
|
3 |
Author: Tobias Nipkow
|
969
|
4 |
Copyright 1994 TU Muenchen
|
|
5 |
|
|
6 |
Specification of sorting
|
|
7 |
*)
|
|
8 |
|
8415
|
9 |
Sorting = Main +
|
969
|
10 |
consts
|
1376
|
11 |
sorted1:: [['a,'a] => bool, 'a list] => bool
|
|
12 |
sorted :: [['a,'a] => bool, 'a list] => bool
|
8415
|
13 |
multiset :: 'a list => ('a => nat)
|
969
|
14 |
|
5184
|
15 |
primrec
|
2517
|
16 |
"sorted1 le [] = True"
|
|
17 |
"sorted1 le (x#xs) = ((case xs of [] => True | y#ys => le x y) &
|
|
18 |
sorted1 le xs)"
|
969
|
19 |
|
5184
|
20 |
primrec
|
2517
|
21 |
"sorted le [] = True"
|
3465
|
22 |
"sorted le (x#xs) = ((!y:set xs. le x y) & sorted le xs)"
|
969
|
23 |
|
5184
|
24 |
primrec
|
8415
|
25 |
"multiset [] y = 0"
|
|
26 |
"multiset (x#xs) y = (if x=y then Suc(multiset xs y) else multiset xs y)"
|
969
|
27 |
|
8415
|
28 |
constdefs
|
|
29 |
total :: (['a,'a] => bool) => bool
|
|
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 |
|
969
|
35 |
end
|