src/HOLCF/lift1.thy
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 248 0d0a6a17a02f
permissions -rw-r--r--
made tutorial first;
     1 (*  Title: 	HOLCF/lift1.thy
     2     ID:         $Id$
     3     Author: 	Franz Regensburger
     4     Copyright   1993  Technische Universitaet Muenchen
     5 
     6 
     7 Lifting
     8 
     9 *)
    10 
    11 Lift1 = Cfun3 +
    12 
    13 (* new type for lifting *)
    14 
    15 types "u" 1
    16 
    17 arities "u" :: (pcpo)term	
    18 
    19 consts
    20 
    21   Rep_Lift	:: "('a)u => (void + 'a)"
    22   Abs_Lift	:: "(void + 'a) => ('a)u"
    23 
    24   Iup           :: "'a => ('a)u"
    25   UU_lift       :: "('a)u"
    26   Ilift         :: "('a->'b)=>('a)u => 'b"
    27   less_lift     :: "('a)u => ('a)u => bool"
    28 
    29 rules
    30 
    31   (*faking a type definition... *)
    32   (* ('a)u is isomorphic to void + 'a  *)
    33 
    34   Rep_Lift_inverse	"Abs_Lift(Rep_Lift(p)) = p"	
    35   Abs_Lift_inverse	"Rep_Lift(Abs_Lift(p)) = p"
    36 
    37    (*defining the abstract constants*)
    38 
    39   UU_lift_def   "UU_lift == Abs_Lift(Inl(UU))"
    40   Iup_def       "Iup(x)  == Abs_Lift(Inr(x))"
    41 
    42   Ilift_def     "Ilift(f)(x)==\
    43 \                sum_case  (Rep_Lift(x)) (%y.UU) (%z.f[z])"
    44  
    45   less_lift_def "less_lift(x1)(x2) == \
    46 \          (sum_case (Rep_Lift(x1))\
    47 \                    (% y1.True)\
    48 \                    (% y2.sum_case (Rep_Lift(x2))\
    49 \                                   (% z1.False)\
    50 \                                   (% z2.y2<<z2)))"
    51 
    52 end
    53 
    54 
    55