src/HOL/IMP/Denotation.thy
author berghofe
Fri Jul 24 13:03:20 1998 +0200 (1998-07-24)
changeset 5183 89f162de39cf
parent 4897 be11be0b6ea1
child 5608 a82a038a3e7a
permissions -rw-r--r--
Adapted to new datatype package.
clasohm@1476
     1
(*  Title:      HOL/IMP/Denotation.thy
clasohm@924
     2
    ID:         $Id$
clasohm@1476
     3
    Author:     Heiko Loetzbeyer & Robert Sandner, TUM
clasohm@924
     4
    Copyright   1994 TUM
clasohm@924
     5
nipkow@1696
     6
Denotational semantics of commands
clasohm@924
     7
*)
clasohm@924
     8
nipkow@1696
     9
Denotation = Natural + 
clasohm@924
    10
clasohm@924
    11
types com_den = "(state*state)set"
nipkow@1696
    12
nipkow@1696
    13
constdefs
clasohm@1374
    14
  Gamma :: [bexp,com_den] => (com_den => com_den)
nipkow@1696
    15
           "Gamma b cd == (%phi.{(s,t). (s,t) : (phi O cd) & b(s)} Un 
nipkow@2847
    16
                                 {(s,t). s=t & ~b(s)})"
nipkow@1696
    17
    
nipkow@1696
    18
consts
nipkow@1696
    19
  C     :: com => com_den
clasohm@924
    20
berghofe@5183
    21
primrec
nipkow@1696
    22
  C_skip    "C(SKIP) = id"
nipkow@4897
    23
  C_assign  "C(x := a) = {(s,t). t = s[x:=a(s)]}"
clasohm@924
    24
  C_comp    "C(c0 ; c1) = C(c1) O C(c0)"
nipkow@1696
    25
  C_if      "C(IF b THEN c1 ELSE c2) = {(s,t). (s,t) : C(c1) & b(s)} Un
nipkow@1696
    26
                                       {(s,t). (s,t) : C(c2) & ~ b(s)}"
nipkow@1481
    27
  C_while   "C(WHILE b DO c) = lfp (Gamma b (C c))"
clasohm@924
    28
clasohm@924
    29
end
nipkow@1696
    30
nipkow@1696
    31