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