equal
deleted
inserted
replaced
|
1 (* Title: HOLCF/Pcpo.thy |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 introduction of the classes cpo and pcpo |
|
7 *) |
1 Pcpo = Porder + |
8 Pcpo = Porder + |
2 |
9 |
3 classes pcpo < po |
10 (* The class cpo of chain complete partial orders *) |
|
11 (* ********************************************** *) |
|
12 axclass cpo < po |
|
13 (* class axiom: *) |
|
14 cpo "is_chain S ==> ? x. range(S) <<| (x::'a::po)" |
4 |
15 |
5 arities void :: pcpo |
16 (* The class pcpo of pointed cpos *) |
|
17 (* ****************************** *) |
|
18 axclass pcpo < cpo |
|
19 |
|
20 least "? x.!y.x<<y" |
6 |
21 |
7 consts |
22 consts |
8 |
23 UU :: "'a::pcpo" |
9 UU :: "'a::pcpo" |
|
10 |
24 |
11 syntax (symbols) |
25 syntax (symbols) |
|
26 UU :: "'a::pcpo" ("\\<bottom>") |
12 |
27 |
13 UU :: "'a::pcpo" ("\\<bottom>") |
28 defs |
14 |
29 UU_def "UU == @x.!y.x<<y" |
15 rules |
|
16 |
|
17 minimal "UU << x" |
|
18 cpo "is_chain S ==> ? x. range(S) <<| (x::'a::pcpo)" |
|
19 |
|
20 inst_void_pcpo "(UU::void) = UU_void" |
|
21 |
30 |
22 end |
31 end |