src/HOLCF/Lift1.thy

Added Krzysztof's theorem LeastI2. Proof of sum_eqpoll_cong
uses lemma sum_bij; proof of prod_eqpoll_cong uses lemma prod_bij.

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


Lifting

*)

Lift1 = Cfun3 + Sum + 

(* new type for lifting *)

types "u" 1

arities "u" :: (pcpo)term	

consts

  Rep_Lift	:: "('a)u => (void + 'a)"
  Abs_Lift	:: "(void + 'a) => ('a)u"

  Iup           :: "'a => ('a)u"
  UU_lift       :: "('a)u"
  Ilift         :: "('a->'b)=>('a)u => 'b"
  less_lift     :: "('a)u => ('a)u => bool"

rules

  (*faking a type definition... *)
  (* ('a)u is isomorphic to void + 'a  *)

  Rep_Lift_inverse	"Abs_Lift(Rep_Lift(p)) = p"	
  Abs_Lift_inverse	"Rep_Lift(Abs_Lift(p)) = p"

   (*defining the abstract constants*)

  UU_lift_def   "UU_lift == Abs_Lift(Inl(UU))"
  Iup_def       "Iup(x)  == Abs_Lift(Inr(x))"

  Ilift_def     "Ilift(f)(x)== \
\                case Rep_Lift(x) of Inl(y) => UU | Inr(z) => f[z]"
 
  less_lift_def "less_lift(x1)(x2) == 		\
\          (case Rep_Lift(x1) of 		\
\               Inl(y1) => True 		\
\             | Inr(y2) => 			\
\                   (case Rep_Lift(x2) of Inl(z1) => False	\
\                                       | Inr(z2) => y2<<z2))"

end