src/HOLCF/Up1.thy

isatool expandshort;

(*  Title:      HOLCF/Up1.thy
    ID:         $Id$
    Author:     Franz Regensburger
    License:    GPL (GNU GENERAL PUBLIC LICENSE)

Lifting.
*)

Up1 = Cfun3 + Sum_Type + Datatype +

(* new type for lifting *)

typedef (Up) ('a) "u" = "{x::(unit + 'a).True}"

instance u :: (sq_ord)sq_ord

consts
  Iup         :: "'a => ('a)u"
  Ifup        :: "('a->'b)=>('a)u => 'b"

defs
  Iup_def     "Iup x == Abs_Up(Inr(x))"
  Ifup_def    "Ifup(f)(x)== case Rep_Up(x) of Inl(y) => UU | Inr(z) => f$z"
  less_up_def "(op <<) == (%x1 x2. case Rep_Up(x1) of                 
               Inl(y1) => True          
             | Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False       
                                            | Inr(z2) => y2<<z2))"
end