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