src/HOLCF/Up1.thy
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 3842 b55686a7b22c
child 6543 da7b170fc8a7
permissions -rw-r--r--
made tutorial first;
     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