src/HOLCF/void.thy
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 243 c22b85994e17
permissions -rw-r--r--
made tutorial first;
     1 (*  Title: 	HOLCF/void.thy
     2     ID:         $Id$
     3     Author: 	Franz Regensburger
     4     Copyright   1993  Technische Universitaet Muenchen
     5 
     6 Definition of type void with partial order. Void is the prototype for
     7 all types in class 'po'
     8 
     9 Type void  is defined as a set Void over type bool.
    10 *)
    11 
    12 Void = Holcfb +
    13 
    14 types void 0
    15 
    16 arities void :: term
    17 
    18 consts
    19   Void		:: "bool set"
    20   UU_void_Rep	:: "bool"	
    21   Rep_Void	:: "void => bool"
    22   Abs_Void	:: "bool => void"
    23   UU_void	:: "void"
    24   less_void	:: "[void,void] => bool"	
    25 
    26 rules
    27 
    28   (* The unique element in Void is False:bool *)
    29 
    30   UU_void_Rep_def	"UU_void_Rep == False"
    31   Void_def		"Void == {x. x = UU_void_Rep}"
    32 
    33   (*faking a type definition... *)
    34   (* void is isomorphic to Void *)
    35 
    36   Rep_Void		"Rep_Void(x):Void"		
    37   Rep_Void_inverse	"Abs_Void(Rep_Void(x)) = x"	
    38   Abs_Void_inverse	"y:Void ==> Rep_Void(Abs_Void(y)) = y"
    39 
    40    (*defining the abstract constants*)
    41 
    42   UU_void_def	"UU_void == Abs_Void(UU_void_Rep)"  
    43   less_void_def "less_void(x,y) == (Rep_Void(x) = Rep_Void(y))"  
    44 end
    45 
    46 
    47 
    48