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