src/HOL/IMP/Denotation.thy
author nipkow
Wed Feb 07 12:22:32 1996 +0100 (1996-02-07)
changeset 1481 03f096efa26d
parent 1476 608483c2122a
child 1696 e84bff5c519b
permissions -rw-r--r--
Modified datatype com.
Added (part of) relative completeness proof for Hoare logic.
     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 expressions & commands
     7 *)
     8 
     9 Denotation = Com + 
    10 
    11 types com_den = "(state*state)set"
    12 consts
    13   A     :: aexp => state => nat
    14   B     :: bexp => state => bool
    15   C     :: com => com_den
    16   Gamma :: [bexp,com_den] => (com_den => com_den)
    17 
    18 primrec A aexp
    19   A_nat "A(N(n)) = (%s. n)"
    20   A_loc "A(X(x)) = (%s. s(x))" 
    21   A_op1 "A(Op1 f a) = (%s. f(A a s))"
    22   A_op2 "A(Op2 f a0 a1) = (%s. f (A a0 s) (A a1 s))"
    23 
    24 primrec B bexp
    25   B_true  "B(true) = (%s. True)"
    26   B_false "B(false) = (%s. False)"
    27   B_op    "B(ROp f a0 a1) = (%s. f (A a0 s) (A a1 s))" 
    28   B_not   "B(noti(b)) = (%s. ~(B b s))"
    29   B_and   "B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))"
    30   B_or    "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
    31 
    32 defs
    33   Gamma_def     "Gamma b cd ==   
    34                    (%phi.{st. st : (phi O cd) & B b (fst st)} Un 
    35                          {st. st : id & ~B b (fst st)})"
    36 
    37 primrec C com
    38   C_skip    "C(Skip) = id"
    39   C_assign  "C(x := a) = {st . snd(st) = fst(st)[A a (fst st)/x]}"
    40   C_comp    "C(c0 ; c1) = C(c1) O C(c0)"
    41   C_if      "C(IF b THEN c0 ELSE c1) =   
    42                    {st. st:C(c0) & (B b (fst st))} Un 
    43                    {st. st:C(c1) & ~(B b (fst st))}"
    44   C_while   "C(WHILE b DO c) = lfp (Gamma b (C c))"
    45 
    46 end