src/HOLCF/Porder0.thy
author slotosch
Sun May 25 11:07:52 1997 +0200 (1997-05-25)
changeset 3323 194ae2e0c193
parent 3310 0ceaad3c3f52
child 7661 8c3190b173aa
permissions -rw-r--r--
eliminated the constant less by the introduction of the axclass sq_ord
added explicit type ::'a::po in the following theorems:
minimal2UU,antisym_less_inverse,box_less,not_less2not_eq,monofun_pair
and dist_eqI (in domain-package)
added instances
instance fun :: (term,sq_ord)sq_ord
instance "->" :: (term,sq_ord)sq_ord
instance "**" :: (sq_ord,sq_ord)sq_ord
instance "*" :: (sq_ord,sq_ord)sq_ord
instance "++" :: (pcpo,pcpo)sq_ord
instance u :: (sq_ord)sq_ord
instance lift :: (term)sq_ord
instance discr :: (term)sq_ord
     1 (*  Title:      HOLCF/Porder0.thy
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 Definition of class porder (partial order)
     7 
     8 *)
     9 
    10 Porder0 = Arith +
    11 
    12 	(* introduce a (syntactic) class for the constant << *)
    13 axclass sq_ord<term
    14 
    15 	(* characteristic constant << for po *)
    16 consts
    17   "<<"          :: "['a,'a::sq_ord] => bool"        (infixl 55)
    18 
    19 syntax (symbols)
    20   "op <<"       :: "['a,'a::sq_ord] => bool"        (infixl "\\<sqsubseteq>" 55)
    21 
    22 axclass po < sq_ord
    23         (* class axioms: *)
    24 refl_less       "x << x"        
    25 antisym_less    "[|x << y; y << x |] ==> x = y"    
    26 trans_less      "[|x << y; y << z |] ==> x << z"
    27  
    28 end 
    29 
    30