|
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 |