author | oheimb |
Fri, 20 Dec 1996 10:33:54 +0100 | |
changeset 2458 | 566a0fc5a3e0 |
parent 2394 | 91d8abf108be |
child 2640 | ee4dfce170a0 |
permissions | -rw-r--r-- |
1479 | 1 |
(* Title: HOLCF/sprod0.thy |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
2 |
ID: $Id$ |
1479 | 3 |
Author: Franz Regensburger |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
4 |
Copyright 1993 Technische Universitaet Muenchen |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
5 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
6 |
Strict product |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
7 |
*) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
8 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
9 |
Sprod0 = Cfun3 + |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
10 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
11 |
(* new type for strict product *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
12 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
13 |
types "**" 2 (infixr 20) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
14 |
|
1479 | 15 |
arities "**" :: (pcpo,pcpo)term |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
16 |
|
2394 | 17 |
syntax (symbols) |
18 |
||
19 |
"**" :: [type, type] => type ("(_ \\<otimes>/ _)" [21,20] 20) |
|
20 |
||
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
21 |
consts |
1479 | 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)" |
|
27 |
Isfst :: "('a ** 'b) => 'a" |
|
28 |
Issnd :: "('a ** 'b) => 'b" |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
29 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1150
diff
changeset
|
30 |
defs |
1479 | 31 |
Spair_Rep_def "Spair_Rep == (%a b. %x y. |
32 |
(~a=UU & ~b=UU --> x=a & y=b ))" |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
33 |
|
1479 | 34 |
Sprod_def "Sprod == {f. ? a b. f = Spair_Rep a b}" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
35 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1150
diff
changeset
|
36 |
rules |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
37 |
(*faking a type definition... *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
38 |
(* "**" is isomorphic to Sprod *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
39 |
|
1479 | 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" |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
43 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1150
diff
changeset
|
44 |
defs |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
45 |
(*defining the abstract constants*) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
46 |
|
1479 | 47 |
Ispair_def "Ispair a b == Abs_Sprod(Spair_Rep a b)" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
48 |
|
1479 | 49 |
Isfst_def "Isfst(p) == @z. |
50 |
(p=Ispair UU UU --> z=UU) |
|
51 |
&(! a b. ~a=UU & ~b=UU & p=Ispair a b --> z=a)" |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
52 |
|
1479 | 53 |
Issnd_def "Issnd(p) == @z. |
54 |
(p=Ispair UU UU --> z=UU) |
|
55 |
&(! a b. ~a=UU & ~b=UU & p=Ispair a b --> z=b)" |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
56 |
|
1274 | 57 |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
58 |
end |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
59 |