src/HOLCF/sprod0.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/sprod0.thy
     2     ID:         $Id$
     3     Author: 	Franz Regensburger
     4     Copyright   1993  Technische Universitaet Muenchen
     5 
     6 Strict product
     7 *)
     8 
     9 Sprod0 = Cfun3 +
    10 
    11 (* new type for strict product *)
    12 
    13 types "**" 2        (infixr 20)
    14 
    15 arities "**" :: (pcpo,pcpo)term	
    16 
    17 consts
    18   Sprod		:: "('a => 'b => bool)set"
    19   Spair_Rep	:: "['a,'b] => ['a,'b] => bool"
    20   Rep_Sprod	:: "('a ** 'b) => ('a => 'b => bool)"
    21   Abs_Sprod	:: "('a => 'b => bool) => ('a ** 'b)"
    22   Ispair	:: "['a,'b] => ('a ** 'b)"
    23   Isfst		:: "('a ** 'b) => 'a"
    24   Issnd		:: "('a ** 'b) => 'b"  
    25 
    26 rules
    27 
    28   Spair_Rep_def		"Spair_Rep == (%a b. %x y.\
    29 \				(~a=UU & ~b=UU --> x=a  & y=b ))"
    30 
    31   Sprod_def		"Sprod == {f. ? a b. f = Spair_Rep(a,b)}"
    32 
    33   (*faking a type definition... *)
    34   (* "**" is isomorphic to Sprod *)
    35 
    36   Rep_Sprod		"Rep_Sprod(p):Sprod"		
    37   Rep_Sprod_inverse	"Abs_Sprod(Rep_Sprod(p)) = p"	
    38   Abs_Sprod_inverse	"f:Sprod ==> Rep_Sprod(Abs_Sprod(f)) = f"
    39 
    40    (*defining the abstract constants*)
    41 
    42   Ispair_def	"Ispair(a,b) == Abs_Sprod(Spair_Rep(a,b))"
    43 
    44   Isfst_def	"Isfst(p) == @z.\
    45 \					(p=Ispair(UU,UU) --> z=UU)\
    46 \		&(! a b. ~a=UU & ~b=UU & p=Ispair(a,b)   --> z=a)"  
    47 
    48   Issnd_def	"Issnd(p) == @z.\
    49 \					(p=Ispair(UU,UU) --> z=UU)\
    50 \		&(! a b. ~a=UU & ~b=UU & p=Ispair(a,b)   --> z=b)"  
    51 
    52 end
    53