author | oheimb |
Fri, 28 Jan 2000 11:22:02 +0100 | |
changeset 8148 | 5ef0b624aadb |
parent 7357 | d0e16da40ea2 |
child 8882 | 9df44a4f1bf7 |
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 |
|
923 | 12 |
axclass |
13 |
ord < term |
|
14 |
||
3947 | 15 |
global |
16 |
||
3820 | 17 |
syntax |
18 |
"op <" :: ['a::ord, 'a] => bool ("op <") |
|
19 |
"op <=" :: ['a::ord, 'a] => bool ("op <=") |
|
20 |
||
923 | 21 |
consts |
2259 | 22 |
"op <" :: ['a::ord, 'a] => bool ("(_/ < _)" [50, 51] 50) |
23 |
"op <=" :: ['a::ord, 'a] => bool ("(_/ <= _)" [50, 51] 50) |
|
1370
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
965
diff
changeset
|
24 |
mono :: ['a::ord => 'b::ord] => bool (*monotonicity*) |
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
965
diff
changeset
|
25 |
min, max :: ['a::ord, 'a] => 'a |
923 | 26 |
|
2608 | 27 |
Least :: ('a::ord=>bool) => 'a (binder "LEAST " 10) |
28 |
||
3820 | 29 |
syntax (symbols) |
30 |
"op <=" :: ['a::ord, 'a] => bool ("op \\<le>") |
|
31 |
"op <=" :: ['a::ord, 'a] => bool ("(_/ \\<le> _)" [50, 51] 50) |
|
2259 | 32 |
|
33 |
||
3947 | 34 |
local |
35 |
||
923 | 36 |
defs |
37 |
mono_def "mono(f) == (!A B. A <= B --> f(A) <= f(B))" |
|
965 | 38 |
min_def "min a b == (if a <= b then a else b)" |
39 |
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
|
40 |
Least_def "Least P == @x. P(x) & (ALL y. P(y) --> x <= y)" |
2608 | 41 |
|
42 |
||
43 |
axclass order < ord |
|
44 |
order_refl "x <= x" |
|
45 |
order_trans "[| x <= y; y <= z |] ==> x <= z" |
|
46 |
order_antisym "[| x <= y; y <= x |] ==> x = y" |
|
47 |
order_less_le "x < y = (x <= y & x ~= y)" |
|
923 | 48 |
|
4640 | 49 |
axclass linorder < order |
50 |
linorder_linear "x <= y | y <= x" |
|
51 |
||
7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
6855
diff
changeset
|
52 |
|
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
6855
diff
changeset
|
53 |
(* bounded quantifiers *) |
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
6855
diff
changeset
|
54 |
|
6402 | 55 |
syntax |
7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
6855
diff
changeset
|
56 |
"_lessAll" :: [idt, 'a, bool] => bool ("(3ALL _<_./ _)" [0, 0, 10] 10) |
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
6855
diff
changeset
|
57 |
"_lessEx" :: [idt, 'a, bool] => bool ("(3EX _<_./ _)" [0, 0, 10] 10) |
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
6855
diff
changeset
|
58 |
"_leAll" :: [idt, 'a, bool] => bool ("(3ALL _<=_./ _)" [0, 0, 10] 10) |
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
6855
diff
changeset
|
59 |
"_leEx" :: [idt, 'a, bool] => bool ("(3EX _<=_./ _)" [0, 0, 10] 10) |
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
6855
diff
changeset
|
60 |
|
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
6855
diff
changeset
|
61 |
syntax (symbols) |
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
6855
diff
changeset
|
62 |
"_lessAll" :: [idt, 'a, bool] => bool ("(3\\<forall>_<_./ _)" [0, 0, 10] 10) |
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
6855
diff
changeset
|
63 |
"_lessEx" :: [idt, 'a, bool] => bool ("(3\\<exists>_<_./ _)" [0, 0, 10] 10) |
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
6855
diff
changeset
|
64 |
"_leAll" :: [idt, 'a, bool] => bool ("(3\\<forall>_<=_./ _)" [0, 0, 10] 10) |
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
6855
diff
changeset
|
65 |
"_leEx" :: [idt, 'a, bool] => bool ("(3\\<exists>_<=_./ _)" [0, 0, 10] 10) |
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
6855
diff
changeset
|
66 |
|
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
6855
diff
changeset
|
67 |
syntax (HOL) |
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
6855
diff
changeset
|
68 |
"_lessAll" :: [idt, 'a, bool] => bool ("(3! _<_./ _)" [0, 0, 10] 10) |
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
6855
diff
changeset
|
69 |
"_lessEx" :: [idt, 'a, bool] => bool ("(3? _<_./ _)" [0, 0, 10] 10) |
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
6855
diff
changeset
|
70 |
"_leAll" :: [idt, 'a, bool] => bool ("(3! _<=_./ _)" [0, 0, 10] 10) |
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
6855
diff
changeset
|
71 |
"_leEx" :: [idt, 'a, bool] => bool ("(3? _<=_./ _)" [0, 0, 10] 10) |
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
6855
diff
changeset
|
72 |
|
6402 | 73 |
translations |
7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
6855
diff
changeset
|
74 |
"ALL x<y. P" => "ALL x. x < y --> P" |
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
6855
diff
changeset
|
75 |
"EX x<y. P" => "EX x. x < y & P" |
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
6855
diff
changeset
|
76 |
"ALL x<=y. P" => "ALL x. x <= y --> P" |
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
6855
diff
changeset
|
77 |
"EX x<=y. P" => "EX x. x <= y & P" |
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
6855
diff
changeset
|
78 |
|
6402 | 79 |
|
923 | 80 |
end |