author | lcp |
Thu, 06 Apr 1995 11:49:42 +0200 | |
changeset 246 | 0f9230a24164 |
parent 48 | 21291189b51e |
permissions | -rw-r--r-- |
46 | 1 |
(* Title: HOL/ex/sorting.thy |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1994 TU Muenchen |
|
5 |
||
47 | 6 |
Specification of sorting |
46 | 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])" |
|
48
21291189b51e
changed "." to "$" and Cons to infix "#" to eliminate ambiguity
clasohm
parents:
47
diff
changeset
|
21 |
sorted1_Cons "sorted1(f,Cons(x,y#zs)) = (f(x,y) & sorted1(f,y#zs))" |
46 | 22 |
|
23 |
sorted_Nil "sorted(le,[])" |
|
48
21291189b51e
changed "." to "$" and Cons to infix "#" to eliminate ambiguity
clasohm
parents:
47
diff
changeset
|
24 |
sorted_Cons "sorted(le,x#xs) = ((Alls y:xs. le(x,y)) & sorted(le,xs))" |
46 | 25 |
|
26 |
mset_Nil "mset([],y) = 0" |
|
48
21291189b51e
changed "." to "$" and Cons to infix "#" to eliminate ambiguity
clasohm
parents:
47
diff
changeset
|
27 |
mset_Cons "mset(x#xs,y) = if(x=y, Suc(mset(xs,y)), mset(xs,y))" |
46 | 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 |