src/HOL/IMP/Denotation.thy
author nipkow
Sat Apr 27 18:47:31 1996 +0200 (1996-04-27)
changeset 1696 e84bff5c519b
parent 1481 03f096efa26d
child 2847 6226b83ce2d8
permissions -rw-r--r--
A completely new version of IMP.
     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) : id & ~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[a(s)/x]}"
    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