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;
     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