author | paulson |
Thu, 21 Mar 1996 13:02:26 +0100 | |
changeset 1601 | 0ef6ea27ab15 |
parent 1370 | 7361ac9b024d |
child 2006 | 72754e060aa2 |
permissions | -rw-r--r-- |
923 | 1 |
(* Title: HOL/Ord.thy |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow, Cambridge University Computer Laboratory |
|
4 |
Copyright 1993 University of Cambridge |
|
5 |
||
6 |
The type class for ordered types (* FIXME improve comment *) |
|
7 |
*) |
|
8 |
||
9 |
Ord = HOL + |
|
10 |
||
11 |
axclass |
|
12 |
ord < term |
|
13 |
||
14 |
consts |
|
1370
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
965
diff
changeset
|
15 |
"<", "<=" :: ['a::ord, 'a] => bool (infixl 50) |
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
965
diff
changeset
|
16 |
mono :: ['a::ord => 'b::ord] => bool (*monotonicity*) |
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
965
diff
changeset
|
17 |
min, max :: ['a::ord, 'a] => 'a |
923 | 18 |
|
19 |
defs |
|
20 |
mono_def "mono(f) == (!A B. A <= B --> f(A) <= f(B))" |
|
965 | 21 |
min_def "min a b == (if a <= b then a else b)" |
22 |
max_def "max a b == (if a <= b then b else a)" |
|
923 | 23 |
|
24 |
end |
|
25 |