| author | paulson |
| Mon, 14 Aug 1995 13:42:27 +0200 | |
| changeset 1228 | 7d6b0241afab |
| parent 1168 | 74be52691d62 |
| child 1274 | ea0668a1c0ba |
| permissions | -rw-r--r-- |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
1 |
(* Title: HOLCF/cprod3.thy |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
2 |
ID: $Id$ |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
3 |
Author: Franz Regensburger |
|
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 |
|
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
7 |
Class instance of * for class pcpo |
|
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 |
*) |
|
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 |
Cprod3 = Cprod2 + |
|
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 |
arities "*" :: (pcpo,pcpo)pcpo (* Witness cprod2.ML *) |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
14 |
|
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
15 |
consts |
|
752
b89462f9d5f1
----------------------------------------------------------------------
regensbu
parents:
625
diff
changeset
|
16 |
cpair :: "'a -> 'b -> ('a*'b)" (* continuous pairing *)
|
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
17 |
cfst :: "('a*'b)->'a"
|
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
18 |
csnd :: "('a*'b)->'b"
|
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
19 |
csplit :: "('a->'b->'c)->('a*'b)->'c"
|
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
20 |
|
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
752
diff
changeset
|
21 |
syntax |
|
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
752
diff
changeset
|
22 |
"@ctuple" :: "['a, args] => 'a * 'b" ("(1<_,/ _>)")
|
|
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
752
diff
changeset
|
23 |
|
|
752
b89462f9d5f1
----------------------------------------------------------------------
regensbu
parents:
625
diff
changeset
|
24 |
|
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
752
diff
changeset
|
25 |
translations |
|
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
752
diff
changeset
|
26 |
"<x, y, z>" == "<x, <y, z>>" |
|
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
752
diff
changeset
|
27 |
"<x, y>" == "cpair`x`y" |
| 625 | 28 |
|
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
29 |
rules |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
30 |
|
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
752
diff
changeset
|
31 |
inst_cprod_pcpo "(UU::'a*'b) = (UU,UU)" |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
32 |
|
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
752
diff
changeset
|
33 |
defs |
|
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
752
diff
changeset
|
34 |
cpair_def "cpair == (LAM x y.(x,y))" |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
35 |
cfst_def "cfst == (LAM p.fst(p))" |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
36 |
csnd_def "csnd == (LAM p.snd(p))" |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
752
diff
changeset
|
37 |
csplit_def "csplit == (LAM f p.f`(cfst`p)`(csnd`p))" |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
38 |
|
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
39 |
end |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
40 |
|
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
41 |
|
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
42 |
|
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
43 |