src/HOLCF/Lift3.thy
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 3034 9c44acc3c6fa
child 10834 a7897aebbffc
permissions -rw-r--r--
tidying
     1 (*  Title:      HOLCF/Lift3.thy
     2     ID:         $Id$
     3     Author:     Olaf Mueller
     4     Copyright   1996 Technische Universitaet Muenchen
     5 
     6 Class Instance lift::(term)pcpo
     7 *)
     8 
     9 Lift3 = Lift2 + 
    10 
    11 instance lift :: (term)pcpo (cpo_lift,least_lift)
    12 
    13 consts 
    14  flift1      :: "('a => 'b::pcpo) => ('a lift -> 'b)"
    15  flift2      :: "('a => 'b)       => ('a lift -> 'b lift)"
    16 
    17  liftpair    ::"'a::term lift * 'b::term lift => ('a * 'b) lift"
    18 
    19 translations
    20  "UU" <= "Undef"
    21 
    22 defs
    23  flift1_def
    24   "flift1 f == (LAM x. (case x of 
    25                    Undef => UU
    26                  | Def y => (f y)))"
    27  flift2_def
    28   "flift2 f == (LAM x. (case x of 
    29                    Undef => UU
    30                  | Def y => Def (f y)))"
    31  liftpair_def
    32   "liftpair x  == (case (cfst`x) of 
    33                   Undef  => UU
    34                 | Def x1 => (case (csnd`x) of 
    35                                Undef => UU
    36                              | Def x2 => Def (x1,x2)))"
    37 
    38 end
    39