--- a/src/HOLCF/Sprod0.thy Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Sprod0.thy Mon Feb 17 10:57:11 1997 +0100
@@ -1,57 +1,36 @@
-(* Title: HOLCF/sprod0.thy
+(* Title: HOLCF/Sprod0.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
-Strict product
+Strict product with typedef
*)
Sprod0 = Cfun3 +
-(* new type for strict product *)
+constdefs
+ Spair_Rep :: ['a,'b] => ['a,'b] => bool
+ "Spair_Rep == (%a b. %x y.(~a=UU & ~b=UU --> x=a & y=b ))"
-types "**" 2 (infixr 20)
-
-arities "**" :: (pcpo,pcpo)term
+typedef (Sprod) ('a, 'b) "**" (infixr 20) = "{f. ? a b. f = Spair_Rep a b}"
syntax (symbols)
-
- "**" :: [type, type] => type ("(_ \\<otimes>/ _)" [21,20] 20)
+ "**" :: [type, type] => type ("(_ \\<otimes>/ _)" [21,20] 20)
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"
defs
- 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}"
-
-rules
- (*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"
-
-defs
(*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)
+ 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)
+ Issnd_def "Issnd(p) == @z. (p=Ispair UU UU --> z=UU)
&(! a b. ~a=UU & ~b=UU & p=Ispair a b --> z=b)"