equal
deleted
inserted
replaced
|
1 (* Title: HOLCF/sprod3.thy |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 Class instance of ** for class pcpo |
|
7 *) |
|
8 |
|
9 Sprod3 = Sprod2 + |
|
10 |
|
11 arities "**" :: (pcpo,pcpo)pcpo (* Witness sprod2.ML *) |
|
12 |
|
13 consts |
|
14 "@spair" :: "'a => 'b => ('a**'b)" ("_##_" [101,100] 100) |
|
15 "cop @spair" :: "'a -> 'b -> ('a**'b)" ("spair") |
|
16 (* continuous strict pairing *) |
|
17 sfst :: "('a**'b)->'a" |
|
18 ssnd :: "('a**'b)->'b" |
|
19 ssplit :: "('a->'b->'c)->('a**'b)->'c" |
|
20 |
|
21 rules |
|
22 |
|
23 inst_sprod_pcpo "UU::'a**'b = Ispair(UU,UU)" |
|
24 spair_def "spair == (LAM x y.Ispair(x,y))" |
|
25 sfst_def "sfst == (LAM p.Isfst(p))" |
|
26 ssnd_def "ssnd == (LAM p.Issnd(p))" |
|
27 ssplit_def "ssplit == (LAM f. strictify[LAM p.f[sfst[p]][ssnd[p]]])" |
|
28 |
|
29 end |
|
30 |
|
31 ML |
|
32 |
|
33 (* ----------------------------------------------------------------------*) |
|
34 (* parse translations for the above mixfix *) |
|
35 (* ----------------------------------------------------------------------*) |
|
36 |
|
37 val parse_translation = [("@spair",mk_cinfixtr "@spair")]; |
|
38 |
|
39 |