969
|
1 |
(* Title: HOL/ex/sorting.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow
|
|
4 |
Copyright 1994 TU Muenchen
|
|
5 |
|
|
6 |
Specification of sorting
|
|
7 |
*)
|
|
8 |
|
|
9 |
Sorting = List +
|
|
10 |
consts
|
|
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"
|
|
16 |
|
|
17 |
rules
|
|
18 |
|
|
19 |
sorted1_Nil "sorted1 f []"
|
|
20 |
sorted1_One "sorted1 f [x]"
|
|
21 |
sorted1_Cons "sorted1 f (Cons x (y#zs)) = (f x y & sorted1 f (y#zs))"
|
|
22 |
|
|
23 |
sorted_Nil "sorted le []"
|
|
24 |
sorted_Cons "sorted le (x#xs) = ((Alls y:xs. le x y) & sorted le xs)"
|
|
25 |
|
|
26 |
mset_Nil "mset [] y = 0"
|
|
27 |
mset_Cons "mset (x#xs) y = (if x=y then Suc(mset xs y) else mset xs y)"
|
|
28 |
|
|
29 |
total_def "total r == (!x y. r x y | r y x)"
|
|
30 |
transf_def "transf f == (!x y z. f x y & f y z --> f x z)"
|
|
31 |
end
|