--- a/src/HOLCF/IMP/Denotational.thy Wed Mar 26 13:44:05 1997 +0100
+++ b/src/HOLCF/IMP/Denotational.thy Wed Mar 26 17:58:48 1997 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/IMP/Den2.ML
+(* Title: HOLCF/IMP/Denotational.thy
ID: $Id$
Author: Tobias Nipkow & Robert Sandner, TUM
Copyright 1996 TUM
@@ -8,15 +8,20 @@
Denotational = HOLCF + Natural +
-consts D :: "com => state lift -> state lift"
+constdefs
+ dlift :: "(('a::term) discr -> 'b::pcpo) => ('a lift -> 'b)"
+ "dlift f == (LAM x.case x of Undef => UU | Def(y) => f`(Discr y))"
+
+consts D :: "com => state discr -> state lift"
primrec D com
- "D(SKIP) = (LAM s. s)"
- "D(X := a) = flift1(%s. Def(s[a(s)/X]))"
- "D(c0 ; c1) = ((D c1) oo (D c0))"
+ "D(SKIP) = (LAM s. Def(undiscr s))"
+ "D(X := a) = (LAM s. Def((undiscr s)[a(undiscr s)/X]))"
+ "D(c0 ; c1) = (dlift(D c1) oo (D c0))"
"D(IF b THEN c1 ELSE c2) =
- flift1(%s . if b s then (D c1)`(Def s) else (D c2)`(Def s))"
+ (LAM s. if b(undiscr s) then (D c1)`s else (D c2)`s)"
"D(WHILE b DO c) =
- fix`(LAM w. flift1(%s. if b s then w`((D c)`(Def s)) else Def s))"
+ fix`(LAM w s. if b(undiscr s) then (dlift w)`((D c)`s)
+ else Def(undiscr s))"
end