src/HOLCF/Up1.thy

Eliminated the prediates flat,chfin
Changed theorems with flat(x::'a) to (x::'a::flat)
Since flat<chfin theorems adm_flat,adm_flatdom are eliminated.
Use adm_chain_finite and adm_chfindom instead!
Examples do not use flat_flat any more

(*  Title:      HOLCF/Up1.thy
    ID:         $Id$
    Author:     Franz Regensburger
    Copyright   1993  Technische Universitaet Muenchen


Lifting

*)

Up1 = Cfun3 + Sum + 

(* 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