src/HOLCF/Up1.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Up1.thy	Fri Nov 29 12:22:22 1996 +0100
@@ -0,0 +1,51 @@
+(*  Title:      HOLCF/Up1.thy
+    ID:         $Id$
+    Author:     Franz Regensburger
+    Copyright   1993  Technische Universitaet Muenchen
+
+
+Lifting
+
+*)
+
+Up1 = Cfun3 + Sum + 
+
+(* new type for lifting *)
+
+types "u" 1
+
+arities "u" :: (pcpo)term       
+
+consts
+
+  Rep_Up      :: "('a)u => (void + 'a)"
+  Abs_Up      :: "(void + 'a) => ('a)u"
+
+  Iup         :: "'a => ('a)u"
+  UU_up       :: "('a)u"
+  Ifup        :: "('a->'b)=>('a)u => 'b"
+  less_up     :: "('a)u => ('a)u => bool"
+
+rules
+
+  (*faking a type definition... *)
+  (* ('a)u is isomorphic to void + 'a  *)
+
+  Rep_Up_inverse  "Abs_Up(Rep_Up(p)) = p"     
+  Abs_Up_inverse  "Rep_Up(Abs_Up(p)) = p"
+
+   (*defining the abstract constants*)
+
+defs
+
+  UU_up_def   "UU_up == Abs_Up(Inl(UU))"
+  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 "less_up(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