author | paulson |
Mon, 02 Jun 1997 12:15:13 +0200 | |
changeset 3385 | f59e64fe4058 |
parent 3143 | d60e49b86c6a |
child 3820 | 46b255e140dc |
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 |
||
2624 | 6 |
Type classes for order signatures and orders. |
923 | 7 |
*) |
8 |
||
9 |
Ord = HOL + |
|
10 |
||
11 |
axclass |
|
12 |
ord < term |
|
13 |
||
14 |
consts |
|
2259 | 15 |
"op <" :: ['a::ord, 'a] => bool ("(_/ < _)" [50, 51] 50) |
16 |
"op <=" :: ['a::ord, 'a] => bool ("(_/ <= _)" [50, 51] 50) |
|
1370
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
965
diff
changeset
|
17 |
mono :: ['a::ord => 'b::ord] => bool (*monotonicity*) |
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
965
diff
changeset
|
18 |
min, max :: ['a::ord, 'a] => 'a |
923 | 19 |
|
2608 | 20 |
Least :: ('a::ord=>bool) => 'a (binder "LEAST " 10) |
21 |
||
2259 | 22 |
syntax |
23 |
"op <" :: ['a::ord, 'a] => bool ("op <") |
|
24 |
"op <=" :: ['a::ord, 'a] => bool ("op <=") |
|
25 |
||
26 |
syntax (symbols) |
|
27 |
"op <=" :: ['a::ord, 'a] => bool ("(_/ \\<le> _)" [50, 51] 50) |
|
28 |
"op <=" :: ['a::ord, 'a] => bool ("op \\<le>") |
|
29 |
||
923 | 30 |
defs |
31 |
mono_def "mono(f) == (!A B. A <= B --> f(A) <= f(B))" |
|
965 | 32 |
min_def "min a b == (if a <= b then a else b)" |
33 |
max_def "max a b == (if a <= b then b else a)" |
|
3143
d60e49b86c6a
Modified def of Least, which, as Markus correctly complained, looked like
nipkow
parents:
2624
diff
changeset
|
34 |
Least_def "Least P == @x. P(x) & (ALL y. P(y) --> x <= y)" |
2608 | 35 |
|
36 |
||
37 |
axclass order < ord |
|
38 |
order_refl "x <= x" |
|
39 |
order_trans "[| x <= y; y <= z |] ==> x <= z" |
|
40 |
order_antisym "[| x <= y; y <= x |] ==> x = y" |
|
41 |
order_less_le "x < y = (x <= y & x ~= y)" |
|
923 | 42 |
|
43 |
end |