src/HOL/IMP/Denotation.thy
author nipkow
Wed Nov 24 12:12:36 1999 +0100 (1999-11-24)
changeset 8029 05446a898852
parent 5608 a82a038a3e7a
child 9241 f961c1fdff50
permissions -rw-r--r--
Basis now Main.
     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
    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