author | paulson |
Fri, 21 Nov 2003 11:15:40 +0100 | |
changeset 14265 | 95b42e69436c |
parent 12114 | a8e860c86252 |
child 14857 | 252d9b36bf44 |
permissions | -rw-r--r-- |
2640 | 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 |
12030 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
5 |
|
3693
37aa547fb564
fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
wenzelm
parents:
2840
diff
changeset
|
6 |
Class instance of * for class pcpo and cpo. |
243
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 |
Cprod3 = Cprod2 + |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
10 |
|
2840
7e03e61612b0
generalized theorems and class instances for Cprod.
slotosch
parents:
2640
diff
changeset
|
11 |
instance "*" :: (cpo,cpo)cpo (cpo_cprod) |
7e03e61612b0
generalized theorems and class instances for Cprod.
slotosch
parents:
2640
diff
changeset
|
12 |
instance "*" :: (pcpo,pcpo)pcpo (least_cprod) |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
13 |
|
3693
37aa547fb564
fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
wenzelm
parents:
2840
diff
changeset
|
14 |
consts |
37aa547fb564
fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
wenzelm
parents:
2840
diff
changeset
|
15 |
cpair :: "'a -> 'b -> ('a*'b)" (* continuous pairing *) |
1479 | 16 |
cfst :: "('a*'b)->'a" |
17 |
csnd :: "('a*'b)->'b" |
|
18 |
csplit :: "('a->'b->'c)->('a*'b)->'c" |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
19 |
|
3693
37aa547fb564
fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
wenzelm
parents:
2840
diff
changeset
|
20 |
syntax |
1479 | 21 |
"@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
|
22 |
|
3693
37aa547fb564
fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
wenzelm
parents:
2840
diff
changeset
|
23 |
translations |
1479 | 24 |
"<x, y, z>" == "<x, <y, z>>" |
10834 | 25 |
"<x, y>" == "cpair$x$y" |
625 | 26 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
752
diff
changeset
|
27 |
defs |
1479 | 28 |
cpair_def "cpair == (LAM x y.(x,y))" |
3842 | 29 |
cfst_def "cfst == (LAM p. fst(p))" |
30 |
csnd_def "csnd == (LAM p. snd(p))" |
|
10834 | 31 |
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
|
32 |
|
1274 | 33 |
|
34 |
||
35 |
(* introduce syntax for |
|
36 |
||
37 |
Let <x,y> = e1; z = E2 in E3 |
|
38 |
||
39 |
and |
|
40 |
||
2394 | 41 |
LAM <x,y,z>.e |
1274 | 42 |
*) |
43 |
||
3693
37aa547fb564
fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
wenzelm
parents:
2840
diff
changeset
|
44 |
constdefs |
37aa547fb564
fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
wenzelm
parents:
2840
diff
changeset
|
45 |
CLet :: "'a -> ('a -> 'b) -> 'b" |
10834 | 46 |
"CLet == LAM s f. f$s" |
3693
37aa547fb564
fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
wenzelm
parents:
2840
diff
changeset
|
47 |
|
1274 | 48 |
|
3693
37aa547fb564
fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
wenzelm
parents:
2840
diff
changeset
|
49 |
(* syntax for Let *) |
37aa547fb564
fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
wenzelm
parents:
2840
diff
changeset
|
50 |
|
37aa547fb564
fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
wenzelm
parents:
2840
diff
changeset
|
51 |
types |
37aa547fb564
fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
wenzelm
parents:
2840
diff
changeset
|
52 |
Cletbinds Cletbind |
1274 | 53 |
|
54 |
syntax |
|
55 |
"_Cbind" :: "[pttrn, 'a] => Cletbind" ("(2_ =/ _)" 10) |
|
56 |
"" :: "Cletbind => Cletbinds" ("_") |
|
57 |
"_Cbinds" :: "[Cletbind, Cletbinds] => Cletbinds" ("_;/ _") |
|
3693
37aa547fb564
fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
wenzelm
parents:
2840
diff
changeset
|
58 |
"_CLet" :: "[Cletbinds, 'a] => 'a" ("(Let (_)/ in (_))" 10) |
1274 | 59 |
|
60 |
translations |
|
61 |
"_CLet (_Cbinds b bs) e" == "_CLet b (_CLet bs e)" |
|
10834 | 62 |
"Let x = a in e" == "CLet$a$(LAM x. e)" |
1274 | 63 |
|
3693
37aa547fb564
fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
wenzelm
parents:
2840
diff
changeset
|
64 |
|
37aa547fb564
fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
wenzelm
parents:
2840
diff
changeset
|
65 |
(* syntax for LAM <x,y,z>.e *) |
1274 | 66 |
|
67 |
syntax |
|
3693
37aa547fb564
fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
wenzelm
parents:
2840
diff
changeset
|
68 |
"_LAM" :: "[patterns, 'a => 'b] => ('a -> 'b)" ("(3LAM <_>./ _)" [0, 10] 10) |
1274 | 69 |
|
70 |
translations |
|
10834 | 71 |
"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)" |
|
73 |
"LAM <x,y>.b" == "csplit$(LAM x y. b)" |
|
3693
37aa547fb564
fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
wenzelm
parents:
2840
diff
changeset
|
74 |
|
12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
12030
diff
changeset
|
75 |
syntax (xsymbols) |
4191 | 76 |
"_LAM" :: "[patterns, 'a => 'b] => ('a -> 'b)" ("(3\\<Lambda>()<_>./ _)" [0, 10] 10) |
1274 | 77 |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
78 |
end |