src/HOLCF/Cfun1.thy
author nipkow
Sun, 22 Dec 2002 10:43:43 +0100
changeset 13763 f94b569cd610
parent 12114 a8e860c86252
child 14981 e73f8140af78
permissions -rw-r--r--
added print translations tha avoid eta contraction for important binders.

(*  Title:      HOLCF/Cfun1.thy
    ID:         $Id$
    Author:     Franz Regensburger
    License:    GPL (GNU GENERAL PUBLIC LICENSE)

Definition of the type ->  of continuous functions.

*)

Cfun1 = Cont +

default cpo

typedef (CFun)  ('a, 'b) "->" (infixr 0) = "{f::'a => 'b. cont f}" (CfunI)

(* to make << defineable *)
instance "->"  :: (cpo,cpo)sq_ord

syntax
	Rep_CFun  :: "('a -> 'b) => ('a => 'b)" ("_$_" [999,1000] 999)
                                                (* application      *)
        Abs_CFun  :: "('a => 'b) => ('a -> 'b)" (binder "LAM " 10)
                                                (* abstraction      *)
        less_cfun :: "[('a -> 'b),('a -> 'b)]=>bool"

syntax (xsymbols)
  "->"		:: [type, type] => type	("(_ \\<rightarrow>/ _)" [1,0]0)
  "LAM "	:: "[idts, 'a => 'b] => ('a -> 'b)"
					("(3\\<Lambda>_./ _)" [0, 10] 10)
  Rep_CFun      :: "('a -> 'b) => ('a => 'b)"  ("(_\\<cdot>_)" [999,1000] 999)

syntax (HTML output)
  Rep_CFun      :: "('a -> 'b) => ('a => 'b)"  ("(_\\<cdot>_)" [999,1000] 999)

defs 
  less_cfun_def "(op <<) == (% fo1 fo2. Rep_CFun fo1 << Rep_CFun fo2 )"

end