src/HOL/IMP/Denotation.thy

 (*  Title:      HOL/IMP/Denotation.thy
     ID:         $Id$
     Author:     Heiko Loetzbeyer & Robert Sandner, TUM
     Copyright   1994 TUM
 
-Denotational semantics of expressions & commands
+Denotational semantics of commands
 *)
 
-Denotation = Com + 
+Denotation = Natural + 
 
 types com_den = "(state*state)set"
+
+constdefs
+  Gamma :: [bexp,com_den] => (com_den => com_den)
+           "Gamma b cd == (%phi.{(s,t). (s,t) : (phi O cd) & b(s)} Un 
+                                 {(s,t). (s,t) : id & ~b(s)})"
+    
 consts
-  A     :: aexp => state => nat
-  B     :: bexp => state => bool
   C     :: com => com_den
-  Gamma :: [bexp,com_den] => (com_den => com_den)
-
-primrec A aexp
-  A_nat "A(N(n)) = (%s. n)"
-  A_loc "A(X(x)) = (%s. s(x))" 
-  A_op1 "A(Op1 f a) = (%s. f(A a s))"
-  A_op2 "A(Op2 f a0 a1) = (%s. f (A a0 s) (A a1 s))"
-
-primrec B bexp
-  B_true  "B(true) = (%s. True)"
-  B_false "B(false) = (%s. False)"
-  B_op    "B(ROp f a0 a1) = (%s. f (A a0 s) (A a1 s))" 
-  B_not   "B(noti(b)) = (%s. ~(B b s))"
-  B_and   "B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))"
-  B_or    "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
-
-defs
-  Gamma_def     "Gamma b cd ==   
-                   (%phi.{st. st : (phi O cd) & B b (fst st)} Un 
-                         {st. st : id & ~B b (fst st)})"
 
 primrec C com
-  C_skip    "C(Skip) = id"
-  C_assign  "C(x := a) = {st . snd(st) = fst(st)[A a (fst st)/x]}"
+  C_skip    "C(SKIP) = id"
+  C_assign  "C(x := a) = {(s,t). t = s[a(s)/x]}"
   C_comp    "C(c0 ; c1) = C(c1) O C(c0)"
-  C_if      "C(IF b THEN c0 ELSE c1) =   
-                   {st. st:C(c0) & (B b (fst st))} Un 
-                   {st. st:C(c1) & ~(B b (fst st))}"
+  C_if      "C(IF b THEN c1 ELSE c2) = {(s,t). (s,t) : C(c1) & b(s)} Un
+                                       {(s,t). (s,t) : C(c2) & ~ b(s)}"
   C_while   "C(WHILE b DO c) = lfp (Gamma b (C c))"
 
 end
+
+