src/HOLCF/cfun1.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/cfun1.thy
     2     ID:         $Id$
     3     Author: 	Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 Definition of the type ->  of continuous functions
     7 
     8 *)
     9 
    10 Cfun1 = Cont +
    11 
    12 
    13 (* new type of continuous functions *)
    14 
    15 types "->" 2        (infixr 5)
    16 
    17 arities "->" :: (pcpo,pcpo)term		(* No properties for ->'s range *)
    18 
    19 consts  
    20 	Cfun	:: "('a => 'b)set"
    21 	fapp	:: "('a -> 'b)=>('a => 'b)"	("(_[_])" [11,0] 1000)
    22 						(* usually Rep_Cfun *)
    23 						(* application      *)
    24 
    25 	fabs	:: "('a => 'b)=>('a -> 'b)"	(binder "LAM " 10)
    26 						(* usually Abs_Cfun *)
    27 						(* abstraction      *)
    28 
    29 	less_cfun :: "[('a -> 'b),('a -> 'b)]=>bool"
    30 
    31 rules 
    32 
    33   Cfun_def	"Cfun == {f. contX(f)}"
    34 
    35   (*faking a type definition... *)
    36   (* -> is isomorphic to Cfun   *)
    37 
    38   Rep_Cfun		"fapp(fo):Cfun"
    39   Rep_Cfun_inverse	"fabs(fapp(fo)) = fo"
    40   Abs_Cfun_inverse	"f:Cfun ==> fapp(fabs(f))=f"
    41 
    42   (*defining the abstract constants*)
    43   less_cfun_def		"less_cfun(fo1,fo2) == ( fapp(fo1) << fapp(fo2) )"
    44 
    45 end