src/HOLCF/Up1.thy
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 3842 b55686a7b22c
child 6543 da7b170fc8a7
permissions -rw-r--r--
tidying
     1 (*  Title:      HOLCF/Up1.thy
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     Copyright   1993  Technische Universitaet Muenchen
     5 
     6 
     7 Lifting
     8 
     9 *)
    10 
    11 Up1 = Cfun3 + Sum + 
    12 
    13 (* new type for lifting *)
    14 
    15 typedef (Up) ('a) "u" = "{x::(unit + 'a).True}"
    16 
    17 instance u :: (sq_ord)sq_ord
    18 
    19 consts
    20   Iup         :: "'a => ('a)u"
    21   Ifup        :: "('a->'b)=>('a)u => 'b"
    22 
    23 defs
    24   Iup_def     "Iup x == Abs_Up(Inr(x))"
    25   Ifup_def    "Ifup(f)(x)== case Rep_Up(x) of Inl(y) => UU | Inr(z) => f`z"
    26   less_up_def "(op <<) == (%x1 x2. case Rep_Up(x1) of                 
    27                Inl(y1) => True          
    28              | Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False       
    29                                             | Inr(z2) => y2<<z2))"
    30 end