equal
deleted
inserted
replaced
1 (* Title: HOLCF/pcpo.thy |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 Definition of class pcpo (pointed complete partial order) |
|
7 |
|
8 The prototype theory for this class is porder.thy |
|
9 |
|
10 *) |
|
11 |
|
12 Pcpo = Porder + |
|
13 |
|
14 (* Introduction of new class. The witness is type void. *) |
|
15 |
|
16 classes pcpo < po |
|
17 |
|
18 (* default class is still term *) |
|
19 (* void is the prototype in pcpo *) |
|
20 |
|
21 arities void :: pcpo |
|
22 |
|
23 consts |
|
24 UU :: "'a::pcpo" (* UU is the least element *) |
|
25 rules |
|
26 |
|
27 (* class axioms: justification is theory Porder *) |
|
28 |
|
29 minimal "UU << x" (* witness is minimal_void *) |
|
30 |
|
31 cpo "is_chain(S) ==> ? x. range(S) <<| x::('a::pcpo)" |
|
32 (* witness is cpo_void *) |
|
33 (* needs explicit type *) |
|
34 |
|
35 (* instance of UU for the prototype void *) |
|
36 |
|
37 inst_void_pcpo "UU::void = UU_void" |
|
38 |
|
39 end |
|