src/HOLCF/Cfun1.thy
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 5291 5706f0ef1d43
child 6382 8b0c9205da75
permissions -rw-r--r--
made tutorial first;
clasohm@1479
     1
(*  Title:      HOLCF/cfun1.thy
nipkow@243
     2
    ID:         $Id$
clasohm@1479
     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
slotosch@2838
    12
default cpo
slotosch@2838
    13
slotosch@2640
    14
typedef (CFun)  ('a, 'b) "->" (infixr 0) = "{f. cont f}" (CfunI)
nipkow@243
    15
slotosch@3323
    16
(* to make << defineable *)
slotosch@3323
    17
instance "->"  :: (cpo,cpo)sq_ord
slotosch@3323
    18
slotosch@5291
    19
syntax
slotosch@5291
    20
	Rep_CFun  :: "('a -> 'b)=>('a => 'b)" ("_`_" [999,1000] 999)
clasohm@1479
    21
                                                (* application      *)
slotosch@5291
    22
        Abs_CFun  :: "('a => 'b)=>('a -> 'b)"     (binder "LAM " 10)
clasohm@1479
    23
                                                (* abstraction      *)
clasohm@1479
    24
        less_cfun :: "[('a -> 'b),('a -> 'b)]=>bool"
nipkow@243
    25
oheimb@2394
    26
syntax (symbols)
mueller@3394
    27
  "->"		:: [type, type] => type	("(_ \\<rightarrow>/ _)" [1,0]0)
oheimb@2394
    28
  "LAM "	:: "[idts, 'a => 'b] => ('a -> 'b)"
oheimb@2394
    29
					("(3\\<Lambda>_./ _)" [0, 10] 10)
regensbu@1168
    30
defs 
slotosch@5291
    31
  less_cfun_def "(op <<) == (% fo1 fo2. Rep_CFun fo1 << Rep_CFun fo2 )"
nipkow@243
    32
nipkow@243
    33
end