--- a/src/HOLCF/Up1.thy Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Up1.thy Mon Feb 17 10:57:11 1997 +0100
@@ -12,40 +12,17 @@
(* new type for lifting *)
-types "u" 1
-
-arities "u" :: (pcpo)term
+typedef (Up) ('a) "u" = "{x::(unit + 'a).True}"
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
+ less_up_def "less == (%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