src/HOLCF/Sprod0.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Sprod0.thy	Wed Jan 19 17:35:01 1994 +0100
@@ -0,0 +1,53 @@
+(*  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
+