src/HOLCF/Cfun1.thy
author wenzelm
Sat Nov 03 01:41:26 2001 +0100 (2001-11-03)
changeset 12030 46d57d0290a2
parent 10863 fef84fefd33f
child 12114 a8e860c86252
permissions -rw-r--r--
GPLed;
wenzelm@6382
     1
(*  Title:      HOLCF/Cfun1.thy
nipkow@243
     2
    ID:         $Id$
clasohm@1479
     3
    Author:     Franz Regensburger
wenzelm@12030
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
nipkow@243
     5
wenzelm@6382
     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
wenzelm@6382
    14
typedef (CFun)  ('a, 'b) "->" (infixr 0) = "{f::'a => 'b. 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
nipkow@10863
    20
	Rep_CFun  :: "('a -> 'b) => ('a => 'b)" ("_$_" [999,1000] 999)
clasohm@1479
    21
                                                (* application      *)
nipkow@10863
    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)
nipkow@10863
    30
  Rep_CFun      :: "('a -> 'b) => ('a => 'b)"  ("(_\\<cdot>_)" [999,1000] 999)
nipkow@10863
    31
nipkow@10863
    32
syntax (HTML output)
nipkow@10863
    33
  Rep_CFun      :: "('a -> 'b) => ('a => 'b)"  ("(_\\<cdot>_)" [999,1000] 999)
nipkow@10863
    34
regensbu@1168
    35
defs 
slotosch@5291
    36
  less_cfun_def "(op <<) == (% fo1 fo2. Rep_CFun fo1 << Rep_CFun fo2 )"
nipkow@243
    37
nipkow@243
    38
end