src/HOLCF/pcpo.thy
 author nipkow Wed Jan 19 17:35:01 1994 +0100 (1994-01-19) changeset 243 c22b85994e17 permissions -rw-r--r--
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
in HOL.
```     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
```