author  nipkow 
Fri, 23 May 1997 09:20:35 +0200  
changeset 3310  0ceaad3c3f52 
parent 2850  a66196e1668c 
child 3323  194ae2e0c193 
permissions  rwrr 
2640  1 
(* Title: HOLCF/Porder0.thy 
298  2 
ID: $Id$ 
1479  3 
Author: Franz Regensburger 
298  4 
Copyright 1993 Technische Universitaet Muenchen 
5 

6 
Definition of class porder (partial order) 

7 

8 
*) 

9 

3310
0ceaad3c3f52
Base theory is now Arith, not Nat. (because all datatypes now require Arith).
nipkow
parents:
2850
diff
changeset

10 
Porder0 = Arith + 
298  11 

2640  12 
(* first the global constant for HOLCF type classes *) 
13 
consts 

3310
0ceaad3c3f52
Base theory is now Arith, not Nat. (because all datatypes now require Arith).
nipkow
parents:
2850
diff
changeset

14 
less :: "['a,'a] => bool" 
298  15 

2640  16 
axclass po < term 
17 
(* class axioms: *) 

18 
ax_refl_less "less x x" 

19 
ax_antisym_less "[less x y; less y x ] ==> x = y" 

20 
ax_trans_less "[less x y; less y z ] ==> less x z" 

21 

22 
(* characteristic constant << on po *) 

2394  23 
consts 
2640  24 
"<<" :: "['a,'a::po] => bool" (infixl 55) 
2394  25 

26 
syntax (symbols) 

2640  27 
"op <<" :: "['a,'a::po] => bool" (infixl "\\<sqsubseteq>" 55) 
298  28 

2640  29 
defs 
30 
po_def "(op <<) == less" 

298  31 
end 
1274  32 

33 