author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 10460  a8d9a79ed95e 
child 11140  a46eaedbeb2d 
permissions  rwrr 
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 

3820  15 
syntax 
16 
"op <" :: ['a::ord, 'a] => bool ("op <") 

17 
"op <=" :: ['a::ord, 'a] => bool ("op <=") 

18 

8882  19 
global 
20 

923  21 
consts 
2259  22 
"op <" :: ['a::ord, 'a] => bool ("(_/ < _)" [50, 51] 50) 
23 
"op <=" :: ['a::ord, 'a] => bool ("(_/ <= _)" [50, 51] 50) 

923  24 

8882  25 
local 
2608  26 

3820  27 
syntax (symbols) 
28 
"op <=" :: ['a::ord, 'a] => bool ("op \\<le>") 

29 
"op <=" :: ['a::ord, 'a] => bool ("(_/ \\<le> _)" [50, 51] 50) 

2259  30 

8882  31 
consts 
32 
mono :: ['a::ord => 'b::ord] => bool (*monotonicity*) 

33 
min, max :: ['a::ord, 'a] => 'a 

34 
Least :: ('a::ord=>bool) => 'a (binder "LEAST " 10) 

3947  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) 
10227  64 
"_leAll" :: [idt, 'a, bool] => bool ("(3\\<forall>_\\<le>_./ _)" [0, 0, 10] 10) 
65 
"_leEx" :: [idt, 'a, bool] => bool ("(3\\<exists>_\\<le>_./ _)" [0, 0, 10] 10) 

7238
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 