src/HOL/IMP/Denotation.thy
changeset 924 806721cfbf46
child 1151 c820b3cc3df0
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/IMP/Denotation.thy	Fri Mar 03 12:04:16 1995 +0100
     1.3 @@ -0,0 +1,46 @@
     1.4 +(*  Title: 	HOL/IMP/Denotation.thy
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
     1.7 +    Copyright   1994 TUM
     1.8 +
     1.9 +Denotational semantics of expressions & commands
    1.10 +*)
    1.11 +
    1.12 +Denotation = Com + 
    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 +  Gamma :: "[bexp,com_den] => (com_den => com_den)"
    1.20 +
    1.21 +primrec A aexp
    1.22 +  A_nat	"A(N(n)) = (%s. n)"
    1.23 +  A_loc	"A(X(x)) = (%s. s(x))" 
    1.24 +  A_op1	"A(Op1 f a) = (%s. f(A a s))"
    1.25 +  A_op2	"A(Op2 f a0 a1) = (%s. f (A a0 s) (A a1 s))"
    1.26 +
    1.27 +primrec B bexp
    1.28 +  B_true  "B(true) = (%s. True)"
    1.29 +  B_false "B(false) = (%s. False)"
    1.30 +  B_op	  "B(ROp f a0 a1) = (%s. f (A a0 s) (A a1 s))" 
    1.31 +  B_not	  "B(noti(b)) = (%s. ~(B b s))"
    1.32 +  B_and	  "B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))"
    1.33 +  B_or	  "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
    1.34 +
    1.35 +defs
    1.36 +  Gamma_def	"Gamma b cd ==   \
    1.37 +\		   (%phi.{st. st : (phi O cd) & B b (fst st)} Un \
    1.38 +\	                 {st. st : id & ~B b (fst st)})"
    1.39 +
    1.40 +primrec C com
    1.41 +  C_skip    "C(skip) = id"
    1.42 +  C_assign  "C(x := a) = {st . snd(st) = fst(st)[A a (fst st)/x]}"
    1.43 +  C_comp    "C(c0 ; c1) = C(c1) O C(c0)"
    1.44 +  C_if	    "C(ifc b then c0 else c1) =   \
    1.45 +\		   {st. st:C(c0) & (B b (fst st))} Un \
    1.46 +\	           {st. st:C(c1) & ~(B b (fst st))}"
    1.47 +  C_while   "C(while b do c) = lfp (Gamma b (C c))"
    1.48 +
    1.49 +end