1 (* Title: HOLCF/Cprod3.thy |
1 (* Title: HOLCF/Cprod3.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 Class instance of * for class pcpo |
6 Class instance of * for class pcpo and cpo. |
7 |
|
8 *) |
7 *) |
9 |
8 |
10 Cprod3 = Cprod2 + |
9 Cprod3 = Cprod2 + |
11 |
10 |
12 instance "*" :: (cpo,cpo)cpo (cpo_cprod) |
11 instance "*" :: (cpo,cpo)cpo (cpo_cprod) |
13 instance "*" :: (pcpo,pcpo)pcpo (least_cprod) |
12 instance "*" :: (pcpo,pcpo)pcpo (least_cprod) |
14 |
13 |
15 consts |
14 consts |
16 cpair :: "'a -> 'b -> ('a*'b)" (* continuous pairing *) |
15 cpair :: "'a -> 'b -> ('a*'b)" (* continuous pairing *) |
17 cfst :: "('a*'b)->'a" |
16 cfst :: "('a*'b)->'a" |
18 csnd :: "('a*'b)->'b" |
17 csnd :: "('a*'b)->'b" |
19 csplit :: "('a->'b->'c)->('a*'b)->'c" |
18 csplit :: "('a->'b->'c)->('a*'b)->'c" |
20 |
19 |
21 syntax |
20 syntax |
22 "@ctuple" :: "['a, args] => 'a * 'b" ("(1<_,/ _>)") |
21 "@ctuple" :: "['a, args] => 'a * 'b" ("(1<_,/ _>)") |
23 |
22 |
24 translations |
23 translations |
25 "<x, y, z>" == "<x, <y, z>>" |
24 "<x, y, z>" == "<x, <y, z>>" |
26 "<x, y>" == "cpair`x`y" |
25 "<x, y>" == "cpair`x`y" |
27 |
26 |
28 defs |
27 defs |
29 cpair_def "cpair == (LAM x y.(x,y))" |
28 cpair_def "cpair == (LAM x y.(x,y))" |
40 and |
39 and |
41 |
40 |
42 LAM <x,y,z>.e |
41 LAM <x,y,z>.e |
43 *) |
42 *) |
44 |
43 |
|
44 constdefs |
|
45 CLet :: "'a -> ('a -> 'b) -> 'b" |
|
46 "CLet == LAM s f.f`s" |
|
47 |
|
48 |
|
49 (* syntax for Let *) |
|
50 |
45 types |
51 types |
46 Cletbinds Cletbind |
52 Cletbinds Cletbind |
47 |
|
48 consts |
|
49 CLet :: "'a -> ('a -> 'b) -> 'b" |
|
50 |
53 |
51 syntax |
54 syntax |
52 (* syntax for Let *) |
|
53 |
|
54 "_Cbind" :: "[pttrn, 'a] => Cletbind" ("(2_ =/ _)" 10) |
55 "_Cbind" :: "[pttrn, 'a] => Cletbind" ("(2_ =/ _)" 10) |
55 "" :: "Cletbind => Cletbinds" ("_") |
56 "" :: "Cletbind => Cletbinds" ("_") |
56 "_Cbinds" :: "[Cletbind, Cletbinds] => Cletbinds" ("_;/ _") |
57 "_Cbinds" :: "[Cletbind, Cletbinds] => Cletbinds" ("_;/ _") |
57 "_CLet" :: "[Cletbinds, 'a] => 'a" ("(Let (_)/ in (_))" 10) |
58 "_CLet" :: "[Cletbinds, 'a] => 'a" ("(Let (_)/ in (_))" 10) |
58 |
59 |
59 translations |
60 translations |
60 (* translation for Let *) |
|
61 "_CLet (_Cbinds b bs) e" == "_CLet b (_CLet bs e)" |
61 "_CLet (_Cbinds b bs) e" == "_CLet b (_CLet bs e)" |
62 "Let x = a in e" == "CLet`a`(LAM x.e)" |
62 "Let x = a in e" == "CLet`a`(LAM x.e)" |
63 |
63 |
64 defs |
64 |
65 (* Misc Definitions *) |
65 (* syntax for LAM <x,y,z>.e *) |
66 CLet_def "CLet == LAM s. LAM f.f`s" |
|
67 |
66 |
68 syntax |
67 syntax |
69 (* syntax for LAM <x,y,z>.E *) |
68 "_LAM" :: "[patterns, 'a => 'b] => ('a -> 'b)" ("(3LAM <_>./ _)" [0, 10] 10) |
70 "@Cpttrn" :: "[pttrn,pttrns] => pttrn" ("<_,/_>") |
|
71 |
69 |
72 translations |
70 translations |
73 (* translations for LAM <x,y,z>.E *) |
71 "LAM <x,y,zs>.b" == "csplit`(LAM x. LAM <y,zs>.b)" |
74 "LAM <x,y,zs>.b" == "csplit`(LAM x.LAM <y,zs>.b)" |
72 "LAM <x,y>. LAM zs. b" <= "csplit`(LAM x y zs. b)" |
75 "LAM <x,y>.b" == "csplit`(LAM x.LAM y.b)" |
73 "LAM <x,y>.b" == "csplit`(LAM x y. b)" |
76 (* reverse translation <= does not work yet !! *) |
74 |
|
75 syntax (symbols) |
|
76 "_LAM" :: "[patterns, 'a => 'b] => ('a -> 'b)" ("(3\\<Lambda><_>./ _)" [0, 10] 10) |
77 |
77 |
78 end |
78 end |
79 |
|
80 |
|
81 |
|
82 |
|