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, Suc(mset(xs,y)), 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 |
|