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 |
|
|
9 |
Sorting = List +
|
|
10 |
consts
|
1376
|
11 |
sorted1:: [['a,'a] => bool, 'a list] => bool
|
|
12 |
sorted :: [['a,'a] => bool, 'a list] => bool
|
|
13 |
mset :: 'a list => ('a => nat)
|
|
14 |
total :: (['a,'a] => bool) => bool
|
|
15 |
transf :: (['a,'a] => bool) => bool
|
969
|
16 |
|
2517
|
17 |
primrec sorted1 list
|
|
18 |
"sorted1 le [] = True"
|
|
19 |
"sorted1 le (x#xs) = ((case xs of [] => True | y#ys => le x y) &
|
|
20 |
sorted1 le xs)"
|
969
|
21 |
|
2517
|
22 |
primrec sorted list
|
|
23 |
"sorted le [] = True"
|
|
24 |
"sorted le (x#xs) = ((!y:set_of_list xs. le x y) & sorted le xs)"
|
969
|
25 |
|
2517
|
26 |
primrec mset list
|
|
27 |
"mset [] y = 0"
|
|
28 |
"mset (x#xs) y = (if x=y then Suc(mset xs y) else mset xs y)"
|
969
|
29 |
|
2517
|
30 |
defs
|
969
|
31 |
total_def "total r == (!x y. r x y | r y x)"
|
|
32 |
transf_def "transf f == (!x y z. f x y & f y z --> f x z)"
|
|
33 |
end
|