src/HOLCF/pcpo.thy
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 243 c22b85994e17
permissions -rw-r--r--
made tutorial first;
nipkow@243
     1
(*  Title: 	HOLCF/pcpo.thy
nipkow@243
     2
    ID:         $Id$
nipkow@243
     3
    Author: 	Franz Regensburger
nipkow@243
     4
    Copyright   1993 Technische Universitaet Muenchen
nipkow@243
     5
nipkow@243
     6
Definition of class pcpo (pointed complete partial order)
nipkow@243
     7
nipkow@243
     8
The prototype theory for this class is porder.thy 
nipkow@243
     9
nipkow@243
    10
*)
nipkow@243
    11
nipkow@243
    12
Pcpo = Porder +
nipkow@243
    13
nipkow@243
    14
(* Introduction of new class. The witness is type void. *)
nipkow@243
    15
nipkow@243
    16
classes pcpo < po
nipkow@243
    17
nipkow@243
    18
(* default class is still term *)
nipkow@243
    19
(* void is the prototype in pcpo *)
nipkow@243
    20
nipkow@243
    21
arities void :: pcpo
nipkow@243
    22
nipkow@243
    23
consts	
nipkow@243
    24
	UU	::	"'a::pcpo"		(* UU is the least element *)
nipkow@243
    25
rules
nipkow@243
    26
nipkow@243
    27
(* class axioms: justification is theory Porder *)
nipkow@243
    28
nipkow@243
    29
minimal		"UU << x"			(* witness is minimal_void *)
nipkow@243
    30
nipkow@243
    31
cpo		"is_chain(S) ==> ? x. range(S) <<| x::('a::pcpo)" 
nipkow@243
    32
						(* witness is cpo_void     *)
nipkow@243
    33
						(* needs explicit type     *)
nipkow@243
    34
nipkow@243
    35
(* instance of UU for the prototype void *)
nipkow@243
    36
nipkow@243
    37
inst_void_pcpo	"UU::void = UU_void"
nipkow@243
    38
nipkow@243
    39
end