src/HOLCF/Lift1.thy
 author lcp Mon, 22 Aug 1994 11:03:52 +0200 changeset 569 4dc184a3d09b parent 542 164be35c8a16 child 1150 66512c9e6bd6 permissions -rw-r--r--
HOLCF/Lift1.thy: now imports Sum
```
(*  Title: 	HOLCF/Lift1.thy
ID:         \$Id\$
Author: 	Franz Regensburger

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

```