src/HOLCF/Lift3.thy

tuned;

(*  Title:      HOLCF/Lift3.thy
    ID:         $Id$
    Author:     Olaf Mueller
    Copyright   1996 Technische Universitaet Muenchen

Class Instance lift::(term)pcpo
*)

Lift3 = Lift2 + 

instance lift :: (term)pcpo (cpo_lift,least_lift)

consts 
 flift1      :: "('a => 'b::pcpo) => ('a lift -> 'b)"
 flift2      :: "('a => 'b)       => ('a lift -> 'b lift)"

 liftpair    ::"'a::term lift * 'b::term lift => ('a * 'b) lift"

translations
 "UU" <= "Undef"

defs
 flift1_def
  "flift1 f == (LAM x. (case x of 
                   Undef => UU
                 | Def y => (f y)))"
 flift2_def
  "flift2 f == (LAM x. (case x of 
                   Undef => UU
                 | Def y => Def (f y)))"
 liftpair_def
  "liftpair x  == (case (cfst$x) of 
                  Undef  => UU
                | Def x1 => (case (csnd$x) of 
                               Undef => UU
                             | Def x2 => Def (x1,x2)))"

end