author  wenzelm 
Fri, 14 Feb 1997 15:32:00 +0100  
changeset 2624  ab311b6e5e29 
parent 2608  450c9b682a92 
child 3143  d60e49b86c6a 
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 

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)" 

2608  34 
Least_def "Least P == @x. P(x) & (ALL y. y<x > ~P(y))" 
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 