src/HOLCF/pcpo.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/pcpo.thy	Wed Jan 19 17:35:01 1994 +0100
@@ -0,0 +1,39 @@
+(*  Title: 	HOLCF/pcpo.thy
+    ID:         $Id$
+    Author: 	Franz Regensburger
+    Copyright   1993 Technische Universitaet Muenchen
+
+Definition of class pcpo (pointed complete partial order)
+
+The prototype theory for this class is porder.thy 
+
+*)
+
+Pcpo = Porder +
+
+(* Introduction of new class. The witness is type void. *)
+
+classes pcpo < po
+
+(* default class is still term *)
+(* void is the prototype in pcpo *)
+
+arities void :: pcpo
+
+consts	
+	UU	::	"'a::pcpo"		(* UU is the least element *)
+rules
+
+(* class axioms: justification is theory Porder *)
+
+minimal		"UU << x"			(* witness is minimal_void *)
+
+cpo		"is_chain(S) ==> ? x. range(S) <<| x::('a::pcpo)" 
+						(* witness is cpo_void     *)
+						(* needs explicit type     *)
+
+(* instance of UU for the prototype void *)
+
+inst_void_pcpo	"UU::void = UU_void"
+
+end