author | wenzelm |
Mon, 16 Nov 1998 11:12:59 +0100 | |
changeset 5889 | d3ecef6b5682 |
parent 4640 | ac6cf9f18653 |
child 5953 | d6017ce6b93e |
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 |
||
5889 | 11 |
(*FIXME move to HOL.thy*) |
12 |
setup Classical.setup |
|
13 |
setup attrib_setup |
|
14 |
||
923 | 15 |
axclass |
16 |
ord < term |
|
17 |
||
3947 | 18 |
global |
19 |
||
3820 | 20 |
syntax |
21 |
"op <" :: ['a::ord, 'a] => bool ("op <") |
|
22 |
"op <=" :: ['a::ord, 'a] => bool ("op <=") |
|
23 |
||
923 | 24 |
consts |
2259 | 25 |
"op <" :: ['a::ord, 'a] => bool ("(_/ < _)" [50, 51] 50) |
26 |
"op <=" :: ['a::ord, 'a] => bool ("(_/ <= _)" [50, 51] 50) |
|
1370
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
965
diff
changeset
|
27 |
mono :: ['a::ord => 'b::ord] => bool (*monotonicity*) |
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
965
diff
changeset
|
28 |
min, max :: ['a::ord, 'a] => 'a |
923 | 29 |
|
2608 | 30 |
Least :: ('a::ord=>bool) => 'a (binder "LEAST " 10) |
31 |
||
3820 | 32 |
syntax (symbols) |
33 |
"op <=" :: ['a::ord, 'a] => bool ("op \\<le>") |
|
34 |
"op <=" :: ['a::ord, 'a] => bool ("(_/ \\<le> _)" [50, 51] 50) |
|
2259 | 35 |
|
36 |
||
3947 | 37 |
local |
38 |
||
923 | 39 |
defs |
40 |
mono_def "mono(f) == (!A B. A <= B --> f(A) <= f(B))" |
|
965 | 41 |
min_def "min a b == (if a <= b then a else b)" |
42 |
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
|
43 |
Least_def "Least P == @x. P(x) & (ALL y. P(y) --> x <= y)" |
2608 | 44 |
|
45 |
||
46 |
axclass order < ord |
|
47 |
order_refl "x <= x" |
|
48 |
order_trans "[| x <= y; y <= z |] ==> x <= z" |
|
49 |
order_antisym "[| x <= y; y <= x |] ==> x = y" |
|
50 |
order_less_le "x < y = (x <= y & x ~= y)" |
|
923 | 51 |
|
4640 | 52 |
axclass linorder < order |
53 |
linorder_linear "x <= y | y <= x" |
|
54 |
||
923 | 55 |
end |