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