author | wenzelm |
Sat, 03 Nov 2001 01:44:45 +0100 | |
changeset 12032 | 0f6417c9a187 |
parent 10835 | f4745d77e620 |
child 12338 | de0f4a63baa5 |
permissions | -rw-r--r-- |
2841
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
2798
diff
changeset
|
1 |
(* Title: HOLCF/IMP/Denotational.thy |
2798 | 2 |
ID: $Id$ |
3 |
Author: Tobias Nipkow & Robert Sandner, TUM |
|
4 |
Copyright 1996 TUM |
|
5 |
||
6 |
Denotational semantics of commands in HOLCF |
|
7 |
*) |
|
8 |
||
9 |
Denotational = HOLCF + Natural + |
|
10 |
||
2841
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
2798
diff
changeset
|
11 |
constdefs |
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
2798
diff
changeset
|
12 |
dlift :: "(('a::term) discr -> 'b::pcpo) => ('a lift -> 'b)" |
12032 | 13 |
"dlift f == (LAM x. case x of UU => UU | Def(y) => f$(Discr y))" |
2841
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
2798
diff
changeset
|
14 |
|
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
2798
diff
changeset
|
15 |
consts D :: "com => state discr -> state lift" |
2798 | 16 |
|
5192 | 17 |
primrec |
2841
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
2798
diff
changeset
|
18 |
"D(SKIP) = (LAM s. Def(undiscr s))" |
9247 | 19 |
"D(X :== a) = (LAM s. Def((undiscr s)[X ::= a(undiscr s)]))" |
2841
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
2798
diff
changeset
|
20 |
"D(c0 ; c1) = (dlift(D c1) oo (D c0))" |
2798 | 21 |
"D(IF b THEN c1 ELSE c2) = |
10835 | 22 |
(LAM s. if b(undiscr s) then (D c1)$s else (D c2)$s)" |
2798 | 23 |
"D(WHILE b DO c) = |
10835 | 24 |
fix$(LAM w s. if b(undiscr s) then (dlift w)$((D c)$s) |
2841
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
2798
diff
changeset
|
25 |
else Def(undiscr s))" |
2798 | 26 |
|
27 |
end |