src/HOLCF/sprod0.thy

revised for new treatment of integers

(*  Title: 	HOLCF/sprod0.thy
    ID:         $Id$
    Author: 	Franz Regensburger
    Copyright   1993  Technische Universitaet Muenchen

Strict product
*)

Sprod0 = Cfun3 +

(* new type for strict product *)

types "**" 2        (infixr 20)

arities "**" :: (pcpo,pcpo)term	

consts
  Sprod		:: "('a => 'b => bool)set"
  Spair_Rep	:: "['a,'b] => ['a,'b] => bool"
  Rep_Sprod	:: "('a ** 'b) => ('a => 'b => bool)"
  Abs_Sprod	:: "('a => 'b => bool) => ('a ** 'b)"
  Ispair	:: "['a,'b] => ('a ** 'b)"
  Isfst		:: "('a ** 'b) => 'a"
  Issnd		:: "('a ** 'b) => 'b"  

rules

  Spair_Rep_def		"Spair_Rep == (%a b. %x y.\
\				(~a=UU & ~b=UU --> x=a  & y=b ))"

  Sprod_def		"Sprod == {f. ? a b. f = Spair_Rep(a,b)}"

  (*faking a type definition... *)
  (* "**" is isomorphic to Sprod *)

  Rep_Sprod		"Rep_Sprod(p):Sprod"		
  Rep_Sprod_inverse	"Abs_Sprod(Rep_Sprod(p)) = p"	
  Abs_Sprod_inverse	"f:Sprod ==> Rep_Sprod(Abs_Sprod(f)) = f"

   (*defining the abstract constants*)

  Ispair_def	"Ispair(a,b) == Abs_Sprod(Spair_Rep(a,b))"

  Isfst_def	"Isfst(p) == @z.\
\					(p=Ispair(UU,UU) --> z=UU)\
\		&(! a b. ~a=UU & ~b=UU & p=Ispair(a,b)   --> z=a)"  

  Issnd_def	"Issnd(p) == @z.\
\					(p=Ispair(UU,UU) --> z=UU)\
\		&(! a b. ~a=UU & ~b=UU & p=Ispair(a,b)   --> z=b)"  

end