src/HOLCF/Up1.thy

Now Datatype.occs_in_prems prints the necessary warning ITSELF.

It is also easier to invoke and even works if the induction variable
is a parameter (rather than a free variable).

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