src/HOLCF/porder0.thy
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 298 3a0485439396
permissions -rw-r--r--
made tutorial first;
     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 The prototype theory for this class is void.thy 
     9 
    10 *)
    11 
    12 Porder0 = Void +
    13 
    14 (* Introduction of new class. The witness is type void. *)
    15 
    16 classes po < term
    17 
    18 (* default type is still term ! *)
    19 (* void is the prototype in po *)
    20 
    21 arities void :: po
    22 
    23 consts	"<<"	::	"['a,'a::po] => bool"	(infixl 55)
    24 
    25 rules
    26 
    27 (* class axioms: justification is theory Void *)
    28 
    29 refl_less	"x << x"	
    30 				(* witness refl_less_void    *)
    31 
    32 antisym_less	"[|x<<y ; y<<x |] ==> x = y"	
    33 				(* witness antisym_less_void *)
    34 
    35 trans_less	"[|x<<y ; y<<z |] ==> x<<z"
    36 				(* witness trans_less_void   *)
    37 
    38 (* instance of << for the prototype void *)
    39 
    40 inst_void_po	"(op <<)::[void,void]=>bool = less_void"
    41 
    42 end