src/HOLCF/cfun1.thy
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 243 c22b85994e17
permissions -rw-r--r--
tidying
nipkow@243
     1
(*  Title: 	HOLCF/cfun1.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 the type ->  of continuous functions
nipkow@243
     7
nipkow@243
     8
*)
nipkow@243
     9
nipkow@243
    10
Cfun1 = Cont +
nipkow@243
    11
nipkow@243
    12
nipkow@243
    13
(* new type of continuous functions *)
nipkow@243
    14
nipkow@243
    15
types "->" 2        (infixr 5)
nipkow@243
    16
nipkow@243
    17
arities "->" :: (pcpo,pcpo)term		(* No properties for ->'s range *)
nipkow@243
    18
nipkow@243
    19
consts  
nipkow@243
    20
	Cfun	:: "('a => 'b)set"
nipkow@243
    21
	fapp	:: "('a -> 'b)=>('a => 'b)"	("(_[_])" [11,0] 1000)
nipkow@243
    22
						(* usually Rep_Cfun *)
nipkow@243
    23
						(* application      *)
nipkow@243
    24
nipkow@243
    25
	fabs	:: "('a => 'b)=>('a -> 'b)"	(binder "LAM " 10)
nipkow@243
    26
						(* usually Abs_Cfun *)
nipkow@243
    27
						(* abstraction      *)
nipkow@243
    28
nipkow@243
    29
	less_cfun :: "[('a -> 'b),('a -> 'b)]=>bool"
nipkow@243
    30
nipkow@243
    31
rules 
nipkow@243
    32
nipkow@243
    33
  Cfun_def	"Cfun == {f. contX(f)}"
nipkow@243
    34
nipkow@243
    35
  (*faking a type definition... *)
nipkow@243
    36
  (* -> is isomorphic to Cfun   *)
nipkow@243
    37
nipkow@243
    38
  Rep_Cfun		"fapp(fo):Cfun"
nipkow@243
    39
  Rep_Cfun_inverse	"fabs(fapp(fo)) = fo"
nipkow@243
    40
  Abs_Cfun_inverse	"f:Cfun ==> fapp(fabs(f))=f"
nipkow@243
    41
nipkow@243
    42
  (*defining the abstract constants*)
nipkow@243
    43
  less_cfun_def		"less_cfun(fo1,fo2) == ( fapp(fo1) << fapp(fo2) )"
nipkow@243
    44
nipkow@243
    45
end