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;
oheimb@2278
     1
(*  Title:      HOLCF/Up1.thy
oheimb@2278
     2
    ID:         $Id$
oheimb@2278
     3
    Author:     Franz Regensburger
oheimb@2278
     4
    Copyright   1993  Technische Universitaet Muenchen
oheimb@2278
     5
oheimb@2278
     6
oheimb@2278
     7
Lifting
oheimb@2278
     8
oheimb@2278
     9
*)
oheimb@2278
    10
oheimb@2278
    11
Up1 = Cfun3 + Sum + 
oheimb@2278
    12
oheimb@2278
    13
(* new type for lifting *)
oheimb@2278
    14
slotosch@2640
    15
typedef (Up) ('a) "u" = "{x::(unit + 'a).True}"
oheimb@2278
    16
slotosch@3323
    17
instance u :: (sq_ord)sq_ord
slotosch@3323
    18
oheimb@2278
    19
consts
oheimb@2278
    20
  Iup         :: "'a => ('a)u"
oheimb@2278
    21
  Ifup        :: "('a->'b)=>('a)u => 'b"
oheimb@2278
    22
oheimb@2278
    23
defs
oheimb@2278
    24
  Iup_def     "Iup x == Abs_Up(Inr(x))"
oheimb@2278
    25
  Ifup_def    "Ifup(f)(x)== case Rep_Up(x) of Inl(y) => UU | Inr(z) => f`z"
wenzelm@3842
    26
  less_up_def "(op <<) == (%x1 x2. case Rep_Up(x1) of                 
oheimb@2278
    27
               Inl(y1) => True          
oheimb@2278
    28
             | Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False       
oheimb@2278
    29
                                            | Inr(z2) => y2<<z2))"
oheimb@2278
    30
end