src/HOLCF/ssum0.thy
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 243 c22b85994e17
permissions -rw-r--r--
tidying
     1 (*  Title: 	HOLCF/ssum0.thy
     2     ID:         $Id$
     3     Author: 	Franz Regensburger
     4     Copyright   1993  Technische Universitaet Muenchen
     5 
     6 Strict sum
     7 *)
     8 
     9 Ssum0 = Cfun3 +
    10 
    11 (* new type for strict sum *)
    12 
    13 types "++" 2        (infixr 10)
    14 
    15 arities "++" :: (pcpo,pcpo)term	
    16 
    17 consts
    18   Ssum		:: "(['a,'b,bool]=>bool)set"
    19   Sinl_Rep	:: "['a,'a,'b,bool]=>bool"
    20   Sinr_Rep	:: "['b,'a,'b,bool]=>bool"
    21   Rep_Ssum	:: "('a ++ 'b) => (['a,'b,bool]=>bool)"
    22   Abs_Ssum	:: "(['a,'b,bool]=>bool) => ('a ++ 'b)"
    23   Isinl		:: "'a => ('a ++ 'b)"
    24   Isinr		:: "'b => ('a ++ 'b)"
    25   Iwhen		:: "('a->'c)=>('b->'c)=>('a ++ 'b)=> 'c"
    26 
    27 rules
    28 
    29   Sinl_Rep_def		"Sinl_Rep == (%a.%x y p.\
    30 \				(~a=UU --> x=a  & p))"
    31 
    32   Sinr_Rep_def		"Sinr_Rep == (%b.%x y p.\
    33 \				(~b=UU --> y=b  & ~p))"
    34 
    35   Ssum_def		"Ssum =={f.(? a.f=Sinl_Rep(a))|(? b.f=Sinr_Rep(b))}"
    36 
    37   (*faking a type definition... *)
    38   (* "++" is isomorphic to Ssum *)
    39 
    40   Rep_Ssum		"Rep_Ssum(p):Ssum"		
    41   Rep_Ssum_inverse	"Abs_Ssum(Rep_Ssum(p)) = p"	
    42   Abs_Ssum_inverse	"f:Ssum ==> Rep_Ssum(Abs_Ssum(f)) = f"
    43 
    44    (*defining the abstract constants*)
    45   Isinl_def	"Isinl(a) == Abs_Ssum(Sinl_Rep(a))"
    46   Isinr_def	"Isinr(b) == Abs_Ssum(Sinr_Rep(b))"
    47 
    48   Iwhen_def	"Iwhen(f)(g)(s) == @z.\
    49 \				    (s=Isinl(UU) --> z=UU)\
    50 \			&(!a. ~a=UU & s=Isinl(a) --> z=f[a])\  
    51 \			&(!b. ~b=UU & s=Isinr(b) --> z=g[b])"  
    52 
    53 end
    54