src/HOLCF/IMP/Denotational.thy
author wenzelm
Tue, 28 Jul 1998 17:05:34 +0200
changeset 5210 54aaa779b6b4
parent 5192 704dd3a6d47d
child 9247 ad9f986616de
permissions -rw-r--r--
removed global_names flag;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
     2
    ID:         $Id$
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
     3
    Author:     Tobias Nipkow & Robert Sandner, TUM
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
     4
    Copyright   1996 TUM
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
     5
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
     6
Denotational semantics of commands in HOLCF
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
     7
*)
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
     8
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
     9
Denotational = HOLCF + Natural +
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    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)"
3842
b55686a7b22c fixed dots;
wenzelm
parents: 2841
diff changeset
    13
  "dlift f == (LAM x. case x of Undef => 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
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    16
5192
704dd3a6d47d Adapted to new datatype package.
berghofe
parents: 4904
diff changeset
    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))"
4904
5f6b2dd1cd11 fixed update syntax;
wenzelm
parents: 3842
diff changeset
    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
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    21
  "D(IF b THEN c1 ELSE c2) =
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents: 2798
diff changeset
    22
	(LAM s. if b(undiscr s) then (D c1)`s else (D c2)`s)"
2798
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    23
  "D(WHILE b DO c) =
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents: 2798
diff changeset
    24
	fix`(LAM w s. if b(undiscr s) then (dlift w)`((D c)`s)
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents: 2798
diff changeset
    25
                      else Def(undiscr s))"
2798
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    26
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    27
end