src/HOL/IMP/Denotation.thy
changeset 1696 e84bff5c519b
parent 1481 03f096efa26d
child 2847 6226b83ce2d8
     1.1 --- a/src/HOL/IMP/Denotation.thy	Sat Apr 27 12:09:21 1996 +0200
     1.2 +++ b/src/HOL/IMP/Denotation.thy	Sat Apr 27 18:47:31 1996 +0200
     1.3 @@ -3,44 +3,29 @@
     1.4      Author:     Heiko Loetzbeyer & Robert Sandner, TUM
     1.5      Copyright   1994 TUM
     1.6  
     1.7 -Denotational semantics of expressions & commands
     1.8 +Denotational semantics of commands
     1.9  *)
    1.10  
    1.11 -Denotation = Com + 
    1.12 +Denotation = Natural + 
    1.13  
    1.14  types com_den = "(state*state)set"
    1.15 -consts
    1.16 -  A     :: aexp => state => nat
    1.17 -  B     :: bexp => state => bool
    1.18 -  C     :: com => com_den
    1.19 +
    1.20 +constdefs
    1.21    Gamma :: [bexp,com_den] => (com_den => com_den)
    1.22 -
    1.23 -primrec A aexp
    1.24 -  A_nat "A(N(n)) = (%s. n)"
    1.25 -  A_loc "A(X(x)) = (%s. s(x))" 
    1.26 -  A_op1 "A(Op1 f a) = (%s. f(A a s))"
    1.27 -  A_op2 "A(Op2 f a0 a1) = (%s. f (A a0 s) (A a1 s))"
    1.28 -
    1.29 -primrec B bexp
    1.30 -  B_true  "B(true) = (%s. True)"
    1.31 -  B_false "B(false) = (%s. False)"
    1.32 -  B_op    "B(ROp f a0 a1) = (%s. f (A a0 s) (A a1 s))" 
    1.33 -  B_not   "B(noti(b)) = (%s. ~(B b s))"
    1.34 -  B_and   "B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))"
    1.35 -  B_or    "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
    1.36 -
    1.37 -defs
    1.38 -  Gamma_def     "Gamma b cd ==   
    1.39 -                   (%phi.{st. st : (phi O cd) & B b (fst st)} Un 
    1.40 -                         {st. st : id & ~B b (fst st)})"
    1.41 +           "Gamma b cd == (%phi.{(s,t). (s,t) : (phi O cd) & b(s)} Un 
    1.42 +                                 {(s,t). (s,t) : id & ~b(s)})"
    1.43 +    
    1.44 +consts
    1.45 +  C     :: com => com_den
    1.46  
    1.47  primrec C com
    1.48 -  C_skip    "C(Skip) = id"
    1.49 -  C_assign  "C(x := a) = {st . snd(st) = fst(st)[A a (fst st)/x]}"
    1.50 +  C_skip    "C(SKIP) = id"
    1.51 +  C_assign  "C(x := a) = {(s,t). t = s[a(s)/x]}"
    1.52    C_comp    "C(c0 ; c1) = C(c1) O C(c0)"
    1.53 -  C_if      "C(IF b THEN c0 ELSE c1) =   
    1.54 -                   {st. st:C(c0) & (B b (fst st))} Un 
    1.55 -                   {st. st:C(c1) & ~(B b (fst st))}"
    1.56 +  C_if      "C(IF b THEN c1 ELSE c2) = {(s,t). (s,t) : C(c1) & b(s)} Un
    1.57 +                                       {(s,t). (s,t) : C(c2) & ~ b(s)}"
    1.58    C_while   "C(WHILE b DO c) = lfp (Gamma b (C c))"
    1.59  
    1.60  end
    1.61 +
    1.62 +