author | paulson |
Wed, 25 Sep 1996 15:03:13 +0200 | |
changeset 2025 | 9acc10ac1e1d |
parent 1479 | 21eb5e156d91 |
child 2278 | d63ffafce255 |
permissions | -rw-r--r-- |
1479 | 1 |
(* Title: HOLCF/cprod3.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 |
|
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 |
|
1479 | 13 |
arities "*" :: (pcpo,pcpo)pcpo (* Witness cprod2.ML *) |
243
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 |
1479 | 16 |
cpair :: "'a -> 'b -> ('a*'b)" (* continuous pairing *) |
17 |
cfst :: "('a*'b)->'a" |
|
18 |
csnd :: "('a*'b)->'b" |
|
19 |
csplit :: "('a->'b->'c)->('a*'b)->'c" |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
20 |
|
1479 | 21 |
syntax |
22 |
"@ctuple" :: "['a, args] => 'a * 'b" ("(1<_,/ _>)") |
|
1168
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 |
1479 | 26 |
"<x, y, z>" == "<x, <y, z>>" |
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 |
|
1479 | 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 |
1479 | 34 |
cpair_def "cpair == (LAM x y.(x,y))" |
35 |
cfst_def "cfst == (LAM p.fst(p))" |
|
36 |
csnd_def "csnd == (LAM p.snd(p))" |
|
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 |
|
1274 | 39 |
|
40 |
||
41 |
(* introduce syntax for |
|
42 |
||
43 |
Let <x,y> = e1; z = E2 in E3 |
|
44 |
||
45 |
and |
|
46 |
||
47 |
¤<x,y,z>.e |
|
48 |
*) |
|
49 |
||
50 |
types |
|
51 |
Cletbinds Cletbind |
|
52 |
||
53 |
consts |
|
54 |
CLet :: "'a -> ('a -> 'b) -> 'b" |
|
55 |
||
56 |
syntax |
|
57 |
(* syntax for Let *) |
|
58 |
||
59 |
"_Cbind" :: "[pttrn, 'a] => Cletbind" ("(2_ =/ _)" 10) |
|
60 |
"" :: "Cletbind => Cletbinds" ("_") |
|
61 |
"_Cbinds" :: "[Cletbind, Cletbinds] => Cletbinds" ("_;/ _") |
|
62 |
"_CLet" :: "[Cletbinds, 'a] => 'a" ("(Let (_)/ in (_))" 10) |
|
63 |
||
64 |
translations |
|
65 |
(* translation for Let *) |
|
66 |
"_CLet (_Cbinds b bs) e" == "_CLet b (_CLet bs e)" |
|
67 |
"Let x = a in e" == "CLet`a`(LAM x.e)" |
|
68 |
||
69 |
defs |
|
70 |
(* Misc Definitions *) |
|
71 |
CLet_def "CLet == LAM s. LAM f.f`s" |
|
72 |
||
73 |
||
74 |
syntax |
|
75 |
(* syntax for LAM <x,y,z>.E *) |
|
76 |
"@Cpttrn" :: "[pttrn,pttrns] => pttrn" ("<_,/_>") |
|
77 |
||
78 |
translations |
|
79 |
(* translations for LAM <x,y,z>.E *) |
|
80 |
"LAM <x,y,zs>.b" == "csplit`(LAM x.LAM <y,zs>.b)" |
|
81 |
"LAM <x,y>.b" == "csplit`(LAM x.LAM y.b)" |
|
82 |
(* reverse translation <= does not work yet !! *) |
|
83 |
||
84 |
(* start 8bit 1 *) |
|
85 |
(* end 8bit 1 *) |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
86 |
end |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
87 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
88 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
89 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
90 |