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