--- a/src/HOLCF/Lift3.thy Thu Apr 24 17:38:33 1997 +0200
+++ b/src/HOLCF/Lift3.thy Thu Apr 24 17:40:30 1997 +0200
@@ -1,6 +1,6 @@
(* Title: HOLCF/Lift3.thy
ID: $Id$
- Author: Olaf Mueller, Robert Sandner
+ Author: Olaf Mueller
Copyright 1996 Technische Universitaet Muenchen
Class Instance lift::(term)pcpo
@@ -12,20 +12,28 @@
consts
flift1 :: "('a => 'b::pcpo) => ('a lift -> 'b)"
- flift2 :: "('a => 'b) => ('a lift -> 'b lift)"
+ flift2 :: "('a => 'b) => ('a lift -> 'b lift)"
+
+ liftpair ::"'a::term lift * 'b::term lift => ('a * 'b) lift"
translations
"UU" <= "Undef"
defs
flift1_def
- "flift1 f == (LAM x. (case x of
+ "flift1 f == (LAM x. (case x of
Undef => UU
| Def y => (f y)))"
flift2_def
"flift2 f == (LAM x. (case x of
- Undef => Undef
- | Def y => Def (f y)))"
+ Undef => UU
+ | Def y => Def (f y)))"
+ liftpair_def
+ "liftpair x == (case (cfst`x) of
+ Undef => UU
+ | Def x1 => (case (csnd`x) of
+ Undef => UU
+ | Def x2 => Def (x1,x2)))"
end